From e4851cf59eed8d39a4b95e1ce8181b52e5c66d78 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 10 Oct 2018 14:31:49 +0200 Subject: [SMTChecker] Inline calls to internal functions --- libsolidity/formal/SMTChecker.cpp | 283 +++++++++++++++++++++++++++++--------- libsolidity/formal/SMTChecker.h | 28 +++- 2 files changed, 243 insertions(+), 68 deletions(-) (limited to 'libsolidity') diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index a7973852..1e27dc33 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -71,29 +71,41 @@ bool SMTChecker::visit(FunctionDefinition const& _function) _function.location(), "Assertion checker does not yet support constructors and functions with modifiers." ); - m_currentFunction = &_function; - m_interface->reset(); - m_pathConditions.clear(); + m_functionPath.push_back(&_function); + // Not visited by a function call + if (isRootFunction()) + { + m_interface->reset(); + m_pathConditions.clear(); + m_expressions.clear(); + resetStateVariables(); + initializeLocalVariables(_function); + } + m_loopExecutionHappened = false; - resetStateVariables(); - initializeLocalVariables(_function); return true; } void SMTChecker::endVisit(FunctionDefinition const&) { - // TODO we could check for "reachability", i.e. satisfiability here. - // We only handle local variables, so we clear at the beginning of the function. - // If we add storage variables, those should be cleared differently. - removeLocalVariables(); - m_currentFunction = nullptr; + // If _function was visited from a function call we don't remove + // the local variables just yet, since we might need them for + // future calls. + // Otherwise we remove any local variables from the context and + // keep the state variables. + if (isRootFunction()) + removeLocalVariables(); + m_functionPath.pop_back(); } bool SMTChecker::visit(IfStatement const& _node) { _node.condition().accept(*this); - checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE."); + // We ignore called functions here because they have + // specific input values. + if (isRootFunction()) + checkBooleanNotConstant(_node.condition(), "Condition is always $VALUE."); auto countersEndTrue = visitBranch(_node.trueStatement(), expr(_node.condition())); vector touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement()); @@ -122,12 +134,14 @@ bool SMTChecker::visit(WhileStatement const& _node) visitBranch(_node.body()); // TODO the assertions generated in the body should still be active in the condition _node.condition().accept(*this); - checkBooleanNotConstant(_node.condition(), "Do-while loop condition is always $VALUE."); + if (isRootFunction()) + checkBooleanNotConstant(_node.condition(), "Do-while loop condition is always $VALUE."); } else { _node.condition().accept(*this); - checkBooleanNotConstant(_node.condition(), "While loop condition is always $VALUE."); + if (isRootFunction()) + checkBooleanNotConstant(_node.condition(), "While loop condition is always $VALUE."); visitBranch(_node.body(), expr(_node.condition())); } @@ -158,7 +172,8 @@ bool SMTChecker::visit(ForStatement const& _node) if (_node.condition()) { _node.condition()->accept(*this); - checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE."); + if (isRootFunction()) + checkBooleanNotConstant(*_node.condition(), "For loop condition is always $VALUE."); } VariableSequenceCounters sequenceCountersStart = m_variables; @@ -198,10 +213,6 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl) ); } -void SMTChecker::endVisit(ExpressionStatement const&) -{ -} - void SMTChecker::endVisit(Assignment const& _assignment) { if (_assignment.assignmentOperator() != Token::Value::Assign) @@ -240,7 +251,7 @@ void SMTChecker::endVisit(TupleExpression const& _tuple) if (_tuple.isInlineArray() || _tuple.components().size() != 1) m_errorReporter.warning( _tuple.location(), - "Assertion checker does not yet implement tules and inline arrays." + "Assertion checker does not yet implement tuples and inline arrays." ); else defineExpr(_tuple, expr(*_tuple.components()[0])); @@ -352,18 +363,95 @@ void SMTChecker::endVisit(FunctionCall const& _funCall) std::vector> const args = _funCall.arguments(); if (funType.kind() == FunctionType::Kind::Assert) - { - solAssert(args.size() == 1, ""); - solAssert(args[0]->annotation().type->category() == Type::Category::Bool, ""); - checkCondition(!(expr(*args[0])), _funCall.location(), "Assertion violation"); - addPathImpliedExpression(expr(*args[0])); - } + visitAssert(_funCall); else if (funType.kind() == FunctionType::Kind::Require) + visitRequire(_funCall); + else if (funType.kind() == FunctionType::Kind::Internal) + inlineFunctionCall(_funCall); + else { - solAssert(args.size() == 1, ""); - solAssert(args[0]->annotation().type->category() == Type::Category::Bool, ""); + m_errorReporter.warning( + _funCall.location(), + "Assertion checker does not yet implement this type of function call." + ); + } +} + +void SMTChecker::visitAssert(FunctionCall const& _funCall) +{ + auto const& args = _funCall.arguments(); + solAssert(args.size() == 1, ""); + solAssert(args[0]->annotation().type->category() == Type::Category::Bool, ""); + checkCondition(!(expr(*args[0])), _funCall.location(), "Assertion violation"); + addPathImpliedExpression(expr(*args[0])); +} + +void SMTChecker::visitRequire(FunctionCall const& _funCall) +{ + auto const& args = _funCall.arguments(); + solAssert(args.size() == 1, ""); + solAssert(args[0]->annotation().type->category() == Type::Category::Bool, ""); + if (isRootFunction()) checkBooleanNotConstant(*args[0], "Condition is always $VALUE."); - addPathImpliedExpression(expr(*args[0])); + addPathImpliedExpression(expr(*args[0])); +} + +void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall) +{ + FunctionDefinition const* _funDef = nullptr; + Expression const* _calledExpr = &_funCall.expression(); + + if (TupleExpression const* _fun = dynamic_cast(&_funCall.expression())) + { + solAssert(_fun->components().size() == 1, ""); + _calledExpr = _fun->components().at(0).get(); + } + + if (Identifier const* _fun = dynamic_cast(_calledExpr)) + _funDef = dynamic_cast(_fun->annotation().referencedDeclaration); + else if (MemberAccess const* _fun = dynamic_cast(_calledExpr)) + _funDef = dynamic_cast(_fun->annotation().referencedDeclaration); + else + { + m_errorReporter.warning( + _funCall.location(), + "Assertion checker does not yet implement this type of function call." + ); + return; + } + solAssert(_funDef, ""); + + if (visitedFunction(_funDef)) + m_errorReporter.warning( + _funCall.location(), + "Assertion checker does not support recursive function calls.", + SecondarySourceLocation().append("Starting from function:", _funDef->location()) + ); + else if (_funDef && _funDef->isImplemented()) + { + vector funArgs; + for (auto arg: _funCall.arguments()) + funArgs.push_back(expr(*arg)); + initializeFunctionCallParameters(*_funDef, funArgs); + _funDef->accept(*this); + auto const& returnParams = _funDef->returnParameters(); + if (_funDef->returnParameters().size()) + { + if (returnParams.size() > 1) + m_errorReporter.warning( + _funCall.location(), + "Assertion checker does not yet support calls to functions that return more than one value." + ); + else + defineExpr(_funCall, currentValue(*returnParams[0])); + } + } + else + { + m_errorReporter.warning( + _funCall.location(), + "Assertion checker does not support calls to functions without implementation." + ); } } @@ -388,6 +476,7 @@ void SMTChecker::endVisit(Identifier const& _identifier) { if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require) return; + createExpr(_identifier); } } @@ -412,6 +501,21 @@ void SMTChecker::endVisit(Literal const& _literal) ); } +void SMTChecker::endVisit(Return const& _return) +{ + if (hasExpr(*_return.expression())) + { + auto returnParams = m_functionPath.back()->returnParameters(); + if (returnParams.size() > 1) + m_errorReporter.warning( + _return.location(), + "Assertion checker does not yet support more than one return value." + ); + else if (returnParams.size() == 1) + m_interface->addAssertion(expr(*_return.expression()) == newValue(*returnParams[0])); + } +} + void SMTChecker::arithmeticOperation(BinaryOperation const& _op) { switch (_op.getOperator()) @@ -578,7 +682,7 @@ void SMTChecker::checkCondition( vector expressionsToEvaluate; vector expressionNames; - if (m_currentFunction) + if (m_functionPath.size()) { if (_additionalValue) { @@ -607,7 +711,7 @@ void SMTChecker::checkCondition( { std::ostringstream message; message << _description << " happens here"; - if (m_currentFunction) + if (m_functionPath.size()) { std::ostringstream modelMessage; modelMessage << " for:\n"; @@ -723,6 +827,30 @@ smt::CheckResult SMTChecker::checkSatisfiable() return checkSatisfiableAndGenerateModel({}).first; } +void SMTChecker::initializeFunctionCallParameters(FunctionDefinition const& _function, vector const& _callArgs) +{ + auto const& funParams = _function.parameters(); + solAssert(funParams.size() == _callArgs.size(), ""); + for (unsigned i = 0; i < funParams.size(); ++i) + if (createVariable(*funParams[i])) + m_interface->addAssertion(_callArgs[i] == newValue(*funParams[i])); + + for (auto const& variable: _function.localVariables()) + if (createVariable(*variable)) + { + newValue(*variable); + setZeroValue(*variable); + } + + if (_function.returnParameterList()) + for (auto const& retParam: _function.returnParameters()) + if (createVariable(*retParam)) + { + newValue(*retParam); + setZeroValue(*retParam); + } +} + void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function) { for (auto const& variable: _function.localVariables()) @@ -739,6 +867,17 @@ void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function) setZeroValue(*retParam); } +void SMTChecker::removeLocalVariables() +{ + for (auto it = m_variables.begin(); it != m_variables.end(); ) + { + if (it->first->isLocalVariable()) + it = m_variables.erase(it); + else + ++it; + } +} + void SMTChecker::resetStateVariables() { for (auto const& variable: m_variables) @@ -779,7 +918,10 @@ void SMTChecker::mergeVariables(vector const& _varia bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) { - if (SSAVariable::isSupportedType(_varDecl.type()->category())) + // This might be the case for multiple calls to the same function. + if (hasVariable(_varDecl)) + return true; + else if (SSAVariable::isSupportedType(_varDecl.type()->category())) { solAssert(m_variables.count(&_varDecl) == 0, ""); m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface)); @@ -838,40 +980,54 @@ void SMTChecker::setUnknownValue(VariableDeclaration const& _decl) smt::Expression SMTChecker::expr(Expression const& _e) { - if (!m_expressions.count(&_e)) + if (!hasExpr(_e)) { m_errorReporter.warning(_e.location(), "Internal error: Expression undefined for SMT solver." ); createExpr(_e); } - return m_expressions.at(&_e); + return prev(m_expressions.upper_bound(&_e))->second; +} + +bool SMTChecker::hasExpr(Expression const& _e) const +{ + return m_expressions.count(&_e); +} + +bool SMTChecker::hasVariable(VariableDeclaration const& _var) const +{ + return m_variables.count(&_var); } void SMTChecker::createExpr(Expression const& _e) { - if (m_expressions.count(&_e)) - m_errorReporter.warning(_e.location(), "Internal error: Expression created twice in SMT solver." ); - else + solAssert(_e.annotation().type, ""); + string exprSymbol = uniqueSymbol(_e) + "_" + to_string(m_expressions.count(&_e)); + switch (_e.annotation().type->category()) { - 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::Address: - 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: - solUnimplementedAssert(false, "Type not implemented."); - } + case Type::Category::RationalNumber: + { + if (RationalNumberType const* rational = dynamic_cast(_e.annotation().type.get())) + solAssert(!rational->isFractional(), ""); + m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol)); + break; + } + case Type::Category::Address: + case Type::Category::Integer: + m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol)); + break; + case Type::Category::Bool: + m_expressions.emplace(&_e, m_interface->newBool(exprSymbol)); + break; + case Type::Category::Function: + // This should be replaced by a `non-deterministic` type in the future. + m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol)); + break; + default: + m_expressions.emplace(&_e, m_interface->newInteger(exprSymbol)); + m_errorReporter.warning( + _e.location(), + "Assertion checker does not yet implement this type." + ); } } @@ -909,13 +1065,12 @@ void SMTChecker::addPathImpliedExpression(smt::Expression const& _e) m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), _e)); } -void SMTChecker::removeLocalVariables() +bool SMTChecker::isRootFunction() { - for (auto it = m_variables.begin(); it != m_variables.end(); ) - { - if (it->first->isLocalVariable()) - it = m_variables.erase(it); - else - ++it; - } + return m_functionPath.size() == 1; +} + +bool SMTChecker::visitedFunction(FunctionDefinition const* _funDef) +{ + return contains(m_functionPath, _funDef); } diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 6cf4e48a..bef6ea0c 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -59,7 +59,6 @@ private: virtual bool visit(WhileStatement const& _node) override; virtual bool visit(ForStatement const& _node) override; virtual void endVisit(VariableDeclarationStatement const& _node) override; - virtual void endVisit(ExpressionStatement const& _node) override; virtual void endVisit(Assignment const& _node) override; virtual void endVisit(TupleExpression const& _node) override; virtual void endVisit(UnaryOperation const& _node) override; @@ -67,11 +66,18 @@ private: virtual void endVisit(FunctionCall const& _node) override; virtual void endVisit(Identifier const& _node) override; virtual void endVisit(Literal const& _node) override; + virtual void endVisit(Return const& _node) override; void arithmeticOperation(BinaryOperation const& _op); void compareOperation(BinaryOperation const& _op); void booleanOperation(BinaryOperation const& _op); + void visitAssert(FunctionCall const&); + void visitRequire(FunctionCall const&); + /// Visits the FunctionDefinition of the called function + /// if available and inlines the return value. + void inlineFunctionCall(FunctionCall const&); + /// Division expression in the given type. Requires special treatment because /// of rounding for signed division. smt::Expression division(smt::Expression _left, smt::Expression _right, IntegerType const& _type); @@ -113,6 +119,7 @@ private: smt::CheckResult checkSatisfiable(); void initializeLocalVariables(FunctionDefinition const& _function); + void initializeFunctionCallParameters(FunctionDefinition const& _function, std::vector const& _callArgs); void resetStateVariables(); void resetVariables(std::vector _variables); /// Given two different branches and the touched variables, @@ -147,6 +154,8 @@ private: smt::Expression expr(Expression const& _e); /// Creates the expression (value can be arbitrary) void createExpr(Expression const& _e); + /// Checks if expression was created + bool hasExpr(Expression const& _e) const; /// Creates the expression and sets its value. void defineExpr(Expression const& _e, smt::Expression _value); @@ -161,18 +170,29 @@ private: /// Add to the solver: the given expression implied by the current path conditions void addPathImpliedExpression(smt::Expression const& _e); - /// Removes the local variables of a function. + /// Removes local variables from the context. void removeLocalVariables(); + /// Checks if VariableDeclaration was seen. + bool hasVariable(VariableDeclaration const& _e) const; + std::shared_ptr m_interface; std::shared_ptr m_variableUsage; bool m_loopExecutionHappened = false; - std::map m_expressions; + /// An Expression may have multiple smt::Expression due to + /// repeated calls to the same function. + std::multimap m_expressions; std::map m_variables; std::vector m_pathConditions; ErrorReporter& m_errorReporter; - FunctionDefinition const* m_currentFunction = nullptr; + /// Stores the current path of function calls. + std::vector m_functionPath; + /// Returns true if the current function was not visited by + /// a function call. + bool isRootFunction(); + /// Returns true if _funDef was already visited. + bool visitedFunction(FunctionDefinition const* _funDef); }; } -- cgit