From a2569833203a952f265acc3511ace52cd9cec4c0 Mon Sep 17 00:00:00 2001 From: chriseth Date: Thu, 5 Oct 2017 19:39:29 +0200 Subject: Fix expression creation problems. --- libsolidity/formal/SMTChecker.cpp | 49 ++++++++++++++++++++++++--------------- 1 file changed, 30 insertions(+), 19 deletions(-) (limited to 'libsolidity/formal') diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index c20c63c6..a22e35d6 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -207,7 +207,10 @@ void SMTChecker::endVisit(Assignment const& _assignment) { Declaration const* decl = identifier->annotation().referencedDeclaration; if (knownVariable(*decl)) + { assignment(*decl, _assignment.rightHandSide(), _assignment.location()); + defineExpr(_assignment, expr(_assignment.rightHandSide())); + } else m_errorReporter.warning( _assignment.location(), @@ -778,31 +781,39 @@ smt::Expression SMTChecker::maxValue(IntegerType const& _t) smt::Expression SMTChecker::expr(Expression const& _e) { - solAssert(m_expressions.count(&_e), ""); + if (!m_expressions.count(&_e)) + { + m_errorReporter.warning(_e.location(), "Internal error: Expression undefined for SMT solver." ); + createExpr(_e); + } return m_expressions.at(&_e); } void SMTChecker::createExpr(Expression const& _e) { - solAssert(!m_expressions.count(&_e), ""); - solAssert(_e.annotation().type, ""); - switch (_e.annotation().type->category()) - { - case Type::Category::RationalNumber: + if (m_expressions.count(&_e)) + m_errorReporter.warning(_e.location(), "Internal error: Expression created twice in SMT solver." ); + else { - if (RationalNumberType const* rational = dynamic_cast(_e.annotation().type.get())) - solAssert(!rational->isFractional(), ""); - m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); - break; - } - case Type::Category::Integer: - m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); - break; - case Type::Category::Bool: - m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e))); - break; - default: - solAssert(false, "Type not implemented."); + solAssert(_e.annotation().type, ""); + switch (_e.annotation().type->category()) + { + case Type::Category::RationalNumber: + { + if (RationalNumberType const* rational = dynamic_cast(_e.annotation().type.get())) + solAssert(!rational->isFractional(), ""); + m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); + break; + } + case Type::Category::Integer: + m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); + break; + case Type::Category::Bool: + m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e))); + break; + default: + solAssert(false, "Type not implemented."); + } } } -- cgit