diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index dbd287876..2ececeeba 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -34,10 +34,10 @@ using namespace langutil; using namespace dev::solidity; SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map const& _smtlib2Responses): - m_interface(make_unique(_smtlib2Responses)), + m_interface(_smtlib2Responses), m_errorReporterReference(_errorReporter), m_errorReporter(m_smtErrors), - m_context(*m_interface) + m_context(m_interface) { #if defined (HAVE_Z3) || defined (HAVE_CVC4) if (!_smtlib2Responses.empty()) @@ -56,11 +56,11 @@ void SMTChecker::analyze(SourceUnit const& _source, shared_ptr const& _ if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker)) _source.accept(*this); - solAssert(m_interface->solvers() > 0, ""); + solAssert(m_interface.solvers() > 0, ""); // If this check is true, Z3 and CVC4 are not available // and the query answers were not provided, since SMTPortfolio // guarantees that SmtLib2Interface is the first solver. - if (!m_interface->unhandledQueries().empty() && m_interface->solvers() == 1) + if (!m_interface.unhandledQueries().empty() && m_interface.solvers() == 1) { if (!m_noSolverWarning) { @@ -106,7 +106,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function) // Not visited by a function call if (m_callStack.empty()) { - m_interface->reset(); + m_interface.reset(); m_context.reset(); m_pathConditions.clear(); m_callStack.clear(); @@ -302,13 +302,13 @@ bool SMTChecker::visit(ForStatement const& _node) checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE."); } - m_interface->push(); + m_interface.push(); if (_node.condition()) - m_interface->addAssertion(expr(*_node.condition())); + m_interface.addAssertion(expr(*_node.condition())); _node.body().accept(*this); if (_node.loopExpression()) _node.loopExpression()->accept(*this); - m_interface->pop(); + m_interface.pop(); auto indicesAfterLoop = copyVariableIndices(); // We reset the execution to before the loop @@ -693,7 +693,7 @@ void SMTChecker::endVisit(FunctionCall const& _funCall) solAssert(value, ""); smt::Expression thisBalance = m_context.balance(); - setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), *m_interface); + setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), m_interface); checkCondition(thisBalance < expr(*value), _funCall.location(), "Insufficient funds", "address(this).balance", &thisBalance); m_context.transfer(m_context.thisAddress(), expr(address), expr(*value)); @@ -737,7 +737,7 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall) // We set the current value to unknown anyway to add type constraints. m_context.setUnknownValue(*symbolicVar); if (index > 0) - m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1)); + m_interface.addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1)); } void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall) @@ -819,7 +819,7 @@ void SMTChecker::abstractFunctionCall(FunctionCall const& _funCall) smtArguments.push_back(expr(*arg)); defineExpr(_funCall, (*m_context.expression(_funCall.expression()))(smtArguments)); m_uninterpretedTerms.insert(&_funCall); - setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, *m_interface); + setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, m_interface); } void SMTChecker::endVisit(Identifier const& _identifier) @@ -911,7 +911,7 @@ void SMTChecker::endVisit(Literal const& _literal) auto stringType = TypeProvider::stringMemory(); auto stringLit = dynamic_cast(_literal.annotation().type); solAssert(stringLit, ""); - auto result = smt::newSymbolicVariable(*stringType, stringLit->richIdentifier(), *m_interface); + auto result = smt::newSymbolicVariable(*stringType, stringLit->richIdentifier(), m_interface); m_context.createExpression(_literal, result.second); } m_errorReporter.warning( @@ -936,10 +936,10 @@ void SMTChecker::endVisit(Return const& _return) solAssert(components.size() == returnParams.size(), ""); for (unsigned i = 0; i < returnParams.size(); ++i) if (components.at(i)) - m_interface->addAssertion(expr(*components.at(i)) == m_context.newValue(*returnParams.at(i))); + m_interface.addAssertion(expr(*components.at(i)) == m_context.newValue(*returnParams.at(i))); } else if (returnParams.size() == 1) - m_interface->addAssertion(expr(*_return.expression()) == m_context.newValue(*returnParams.front())); + m_interface.addAssertion(expr(*_return.expression()) == m_context.newValue(*returnParams.front())); } } @@ -981,7 +981,7 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess) if (_memberAccess.memberName() == "balance") { defineExpr(_memberAccess, m_context.balance(expr(_memberAccess.expression()))); - setSymbolicUnknownValue(*m_context.expression(_memberAccess), *m_interface); + setSymbolicUnknownValue(*m_context.expression(_memberAccess), m_interface); m_uninterpretedTerms.insert(&_memberAccess); return false; } @@ -1028,7 +1028,7 @@ void SMTChecker::endVisit(IndexAccess const& _indexAccess) setSymbolicUnknownValue( expr(_indexAccess), _indexAccess.annotation().type, - *m_interface + m_interface ); m_uninterpretedTerms.insert(&_indexAccess); } @@ -1080,7 +1080,7 @@ void SMTChecker::arrayIndexAssignment(Expression const& _expr, smt::Expression c expr(*indexAccess.indexExpression()), _rightHandSide ); - m_interface->addAssertion(m_context.newValue(*varDecl) == store); + m_interface.addAssertion(m_context.newValue(*varDecl) == store); // Update the SMT select value after the assignment, // necessary for sound models. defineExpr(indexAccess, smt::Expression::select( @@ -1211,7 +1211,7 @@ smt::Expression SMTChecker::arithmeticOperation( if (_op == Token::Div || _op == Token::Mod) { checkCondition(_right == 0, _location, "Division by zero", "", &_right); - m_interface->addAssertion(_right != 0); + m_interface.addAssertion(_right != 0); } addOverflowTarget( @@ -1393,7 +1393,7 @@ void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expressio addOverflowTarget(OverflowTarget::Type::All, TypeProvider::uint(160), _value, _location); else if (type->category() == Type::Category::Mapping) arrayAssignment(); - m_interface->addAssertion(m_context.newValue(_variable) == _value); + m_interface.addAssertion(m_context.newValue(_variable) == _value); } SMTChecker::VariableIndices SMTChecker::visitBranch(ASTNode const* _statement, smt::Expression _condition) @@ -1422,7 +1422,7 @@ void SMTChecker::checkCondition( smt::Expression const* _additionalValue ) { - m_interface->push(); + m_interface.push(); addPathConjoinedExpression(_condition); vector expressionsToEvaluate; @@ -1534,7 +1534,7 @@ void SMTChecker::checkCondition( m_errorReporter.warning(_location, "Error trying to invoke SMT solver."); break; } - m_interface->pop(); + m_interface.pop(); } void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string const& _description) @@ -1543,15 +1543,15 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co if (dynamic_cast(&_condition)) return; - m_interface->push(); + m_interface.push(); addPathConjoinedExpression(expr(_condition)); auto positiveResult = checkSatisfiable(); - m_interface->pop(); + m_interface.pop(); - m_interface->push(); + m_interface.push(); addPathConjoinedExpression(!expr(_condition)); auto negatedResult = checkSatisfiable(); - m_interface->pop(); + m_interface.pop(); if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR) m_errorReporter.warning(_condition.location(), "Error trying to invoke SMT solver."); @@ -1596,7 +1596,7 @@ SMTChecker::checkSatisfiableAndGenerateModel(vector const& _exp vector values; try { - tie(result, values) = m_interface->check(_expressionsToEvaluate); + tie(result, values) = m_interface.check(_expressionsToEvaluate); } catch (smt::SolverError const& _e) { @@ -1632,7 +1632,7 @@ void SMTChecker::initializeFunctionCallParameters(CallableDeclaration const& _fu for (unsigned i = 0; i < funParams.size(); ++i) if (createVariable(*funParams[i])) { - m_interface->addAssertion(_callArgs[i] == m_context.newValue(*funParams[i])); + m_interface.addAssertion(_callArgs[i] == m_context.newValue(*funParams[i])); if (funParams[i]->annotation().type->category() == Type::Category::Mapping) m_arrayAssignmentHappened = true; } @@ -1698,7 +1698,7 @@ void SMTChecker::mergeVariables(set const& _variable int trueIndex = _indicesEndTrue.at(decl); int falseIndex = _indicesEndFalse.at(decl); solAssert(trueIndex != falseIndex, ""); - m_interface->addAssertion(m_context.newValue(*decl) == smt::Expression::ite( + m_interface.addAssertion(m_context.newValue(*decl) == smt::Expression::ite( _condition, valueAtIndex(*decl, trueIndex), valueAtIndex(*decl, falseIndex)) @@ -1758,7 +1758,7 @@ void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value) { createExpr(_e); solAssert(smt::smtKind(_e.annotation().type->category()) != smt::Kind::Function, "Equality operator applied to type that is not fully supported"); - m_interface->addAssertion(expr(_e) == _value); + m_interface.addAssertion(expr(_e) == _value); } void SMTChecker::popPathCondition() @@ -1807,12 +1807,12 @@ void SMTChecker::pushCallStack(CallStackEntry _entry) void SMTChecker::addPathConjoinedExpression(smt::Expression const& _e) { - m_interface->addAssertion(currentPathConditions() && _e); + m_interface.addAssertion(currentPathConditions() && _e); } void SMTChecker::addPathImpliedExpression(smt::Expression const& _e) { - m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), _e)); + m_interface.addAssertion(smt::Expression::implies(currentPathConditions(), _e)); } bool SMTChecker::isRootFunction() diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 54254c3a6..661dff342 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -19,7 +19,7 @@ #include -#include +#include #include #include @@ -53,7 +53,7 @@ public: /// This is used if the SMT solver is not directly linked into this binary. /// @returns a list of inputs to the SMT solver that were not part of the argument to /// the constructor. - std::vector unhandledQueries() { return m_interface->unhandledQueries(); } + std::vector unhandledQueries() { return m_interface.unhandledQueries(); } /// @returns the FunctionDefinition of a called function if possible and should inline, /// otherwise nullptr. @@ -91,6 +91,10 @@ private: void endVisit(IndexAccess const& _node) override; bool visit(InlineAssembly const& _node) override; + smt::Expression assertions() { return m_interface.assertions(); } + void push() { m_interface.push(); } + void pop() { m_interface.pop(); } + /// Do not visit subtree if node is a RationalNumber. /// Symbolic _expr is the rational literal. bool shortcutRationalNumber(Expression const& _expr); @@ -270,7 +274,7 @@ private: /// @returns the VariableDeclaration referenced by an Identifier or nullptr. VariableDeclaration const* identifierToVariable(Expression const& _expr); - std::unique_ptr m_interface; + smt::SMTPortfolio m_interface; smt::VariableUsage m_variableUsage; bool m_loopExecutionHappened = false; bool m_arrayAssignmentHappened = false;