diff options
Diffstat (limited to 'libsolidity/formal')
25 files changed, 1265 insertions, 712 deletions
diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp index dba5823a..6cb91483 100644 --- a/libsolidity/formal/CVC4Interface.cpp +++ b/libsolidity/formal/CVC4Interface.cpp @@ -37,6 +37,7 @@ void CVC4Interface::reset() m_functions.clear(); m_solver.reset(); m_solver.setOption("produce-models", true); + m_solver.setTimeLimit(queryTimeout); } void CVC4Interface::push() @@ -49,23 +50,25 @@ void CVC4Interface::pop() m_solver.pop(); } -Expression CVC4Interface::newFunction(string _name, Sort _domain, Sort _codomain) +void CVC4Interface::declareFunction(string _name, Sort _domain, Sort _codomain) { - CVC4::Type fType = m_context.mkFunctionType(cvc4Sort(_domain), cvc4Sort(_codomain)); - m_functions.insert({_name, m_context.mkVar(_name.c_str(), fType)}); - return SolverInterface::newFunction(move(_name), _domain, _codomain); + if (!m_functions.count(_name)) + { + CVC4::Type fType = m_context.mkFunctionType(cvc4Sort(_domain), cvc4Sort(_codomain)); + m_functions.insert({_name, m_context.mkVar(_name.c_str(), fType)}); + } } -Expression CVC4Interface::newInteger(string _name) +void CVC4Interface::declareInteger(string _name) { - m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.integerType())}); - return SolverInterface::newInteger(move(_name)); + if (!m_constants.count(_name)) + m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.integerType())}); } -Expression CVC4Interface::newBool(string _name) +void CVC4Interface::declareBool(string _name) { - m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.booleanType())}); - return SolverInterface::newBool(std::move(_name)); + if (!m_constants.count(_name)) + m_constants.insert({_name, m_context.mkVar(_name.c_str(), m_context.booleanType())}); } void CVC4Interface::addAssertion(Expression const& _expr) @@ -109,13 +112,13 @@ pair<CheckResult, vector<string>> CVC4Interface::check(vector<Expression> const& solAssert(false, ""); } - if (result != CheckResult::UNSATISFIABLE && !_expressionsToEvaluate.empty()) + if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty()) { for (Expression const& e: _expressionsToEvaluate) values.push_back(toString(m_solver.getValue(toCVC4Expr(e)))); } } - catch (CVC4::Exception & e) + catch (CVC4::Exception const&) { result = CheckResult::ERROR; values.clear(); diff --git a/libsolidity/formal/CVC4Interface.h b/libsolidity/formal/CVC4Interface.h index cfaeb412..cd6d761d 100644 --- a/libsolidity/formal/CVC4Interface.h +++ b/libsolidity/formal/CVC4Interface.h @@ -21,8 +21,19 @@ #include <boost/noncopyable.hpp> +#if defined(__GLIBC__) +// The CVC4 headers includes the deprecated system headers <ext/hash_map> +// and <ext/hash_set>. These headers cause a warning that will break the +// build, unless _GLIBCXX_PERMIT_BACKWARD_HASH is set. +#define _GLIBCXX_PERMIT_BACKWARD_HASH +#endif + #include <cvc4/cvc4.h> +#if defined(__GLIBC__) +#undef _GLIBCXX_PERMIT_BACKWARD_HASH +#endif + namespace dev { namespace solidity @@ -40,9 +51,9 @@ public: void push() override; void pop() override; - Expression newFunction(std::string _name, Sort _domain, Sort _codomain) override; - Expression newInteger(std::string _name) override; - Expression newBool(std::string _name) override; + void declareFunction(std::string _name, Sort _domain, Sort _codomain) override; + void declareInteger(std::string _name) override; + void declareBool(std::string _name) override; void addAssertion(Expression const& _expr) override; std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override; diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 425c5c1e..cc580021 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -17,17 +17,10 @@ #include <libsolidity/formal/SMTChecker.h> -#ifdef HAVE_Z3 -#include <libsolidity/formal/Z3Interface.h> -#elif HAVE_CVC4 -#include <libsolidity/formal/CVC4Interface.h> -#else -#include <libsolidity/formal/SMTLib2Interface.h> -#endif - -#include <libsolidity/formal/SSAVariable.h> -#include <libsolidity/formal/SymbolicIntVariable.h> +#include <libsolidity/formal/SMTPortfolio.h> + #include <libsolidity/formal/VariableUsage.h> +#include <libsolidity/formal/SymbolicTypes.h> #include <libsolidity/interface/ErrorReporter.h> @@ -39,21 +32,15 @@ using namespace dev; using namespace dev::solidity; SMTChecker::SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readFileCallback): -#ifdef HAVE_Z3 - m_interface(make_shared<smt::Z3Interface>()), -#elif HAVE_CVC4 - m_interface(make_shared<smt::CVC4Interface>()), -#else - m_interface(make_shared<smt::SMTLib2Interface>(_readFileCallback)), -#endif + m_interface(make_shared<smt::SMTPortfolio>(_readFileCallback)), m_errorReporter(_errorReporter) { - (void)_readFileCallback; } -void SMTChecker::analyze(SourceUnit const& _source) +void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _scanner) { m_variableUsage = make_shared<VariableUsage>(_source); + m_scanner = _scanner; if (_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker)) _source.accept(*this); } @@ -68,7 +55,7 @@ bool SMTChecker::visit(ContractDefinition const& _contract) void SMTChecker::endVisit(ContractDefinition const&) { - m_stateVariables.clear(); + m_variables.clear(); } void SMTChecker::endVisit(VariableDeclaration const& _varDecl) @@ -84,45 +71,54 @@ 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_variables.clear(); - m_variables.insert(m_stateVariables.begin(), m_stateVariables.end()); - 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; - initializeLocalVariables(_function); - resetStateVariables(); return true; } void SMTChecker::endVisit(FunctionDefinition const&) { - // TOOD 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. - 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<Declaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement()); - decltype(countersEndTrue) countersEndFalse; + auto indicesEndTrue = visitBranch(_node.trueStatement(), expr(_node.condition())); + vector<VariableDeclaration const*> touchedVariables = m_variableUsage->touchedVariables(_node.trueStatement()); + decltype(indicesEndTrue) indicesEndFalse; if (_node.falseStatement()) { - countersEndFalse = visitBranch(*_node.falseStatement(), !expr(_node.condition())); + indicesEndFalse = visitBranch(*_node.falseStatement(), !expr(_node.condition())); touchedVariables += m_variableUsage->touchedVariables(*_node.falseStatement()); } else - { - countersEndFalse = m_variables; - } + indicesEndFalse = copyVariableIndices(); - mergeVariables(touchedVariables, expr(_node.condition()), countersEndTrue, countersEndFalse); + mergeVariables(touchedVariables, expr(_node.condition()), indicesEndTrue, indicesEndFalse); return false; } @@ -136,12 +132,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())); } @@ -172,10 +170,10 @@ 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; m_interface->push(); if (_node.condition()) m_interface->addAssertion(expr(*_node.condition())); @@ -186,7 +184,6 @@ bool SMTChecker::visit(ForStatement const& _node) m_interface->pop(); m_loopExecutionHappened = true; - std::swap(sequenceCountersStart, m_variables); resetVariables(touchedVariables); @@ -212,28 +209,24 @@ void SMTChecker::endVisit(VariableDeclarationStatement const& _varDecl) ); } -void SMTChecker::endVisit(ExpressionStatement const&) -{ -} - void SMTChecker::endVisit(Assignment const& _assignment) { - if (_assignment.assignmentOperator() != Token::Value::Assign) + if (_assignment.assignmentOperator() != Token::Assign) m_errorReporter.warning( _assignment.location(), "Assertion checker does not yet implement compound assignment." ); - else if (!SSAVariable::isSupportedType(_assignment.annotation().type->category())) + else if (!isSupportedType(_assignment.annotation().type->category())) m_errorReporter.warning( _assignment.location(), "Assertion checker does not yet implement type " + _assignment.annotation().type->toString() ); else if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_assignment.leftHandSide())) { - Declaration const* decl = identifier->annotation().referencedDeclaration; - if (knownVariable(*decl)) + VariableDeclaration const& decl = dynamic_cast<VariableDeclaration const&>(*identifier->annotation().referencedDeclaration); + if (knownVariable(decl)) { - assignment(*decl, _assignment.rightHandSide(), _assignment.location()); + assignment(decl, _assignment.rightHandSide(), _assignment.location()); defineExpr(_assignment, expr(_assignment.rightHandSide())); } else @@ -254,7 +247,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])); @@ -263,17 +256,17 @@ void SMTChecker::endVisit(TupleExpression const& _tuple) void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _type, SourceLocation const& _location) { checkCondition( - _value < SymbolicIntVariable::minValue(_type), + _value < minValue(_type), _location, "Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")", - "value", + "<result>", &_value ); checkCondition( - _value > SymbolicIntVariable::maxValue(_type), + _value > maxValue(_type), _location, "Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")", - "value", + "<result>", &_value ); } @@ -284,7 +277,7 @@ void SMTChecker::endVisit(UnaryOperation const& _op) { case Token::Not: // ! { - solAssert(SSAVariable::isBool(_op.annotation().type->category()), ""); + solAssert(isBool(_op.annotation().type->category()), ""); defineExpr(_op, !expr(_op.subExpression())); break; } @@ -292,16 +285,16 @@ void SMTChecker::endVisit(UnaryOperation const& _op) case Token::Dec: // -- (pre- or postfix) { - solAssert(SSAVariable::isInteger(_op.annotation().type->category()), ""); + solAssert(isInteger(_op.annotation().type->category()), ""); solAssert(_op.subExpression().annotation().lValueRequested, ""); if (Identifier const* identifier = dynamic_cast<Identifier const*>(&_op.subExpression())) { - Declaration const* decl = identifier->annotation().referencedDeclaration; - if (knownVariable(*decl)) + VariableDeclaration const& decl = dynamic_cast<VariableDeclaration const&>(*identifier->annotation().referencedDeclaration); + if (knownVariable(decl)) { - auto innerValue = currentValue(*decl); + auto innerValue = currentValue(decl); auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1; - assignment(*decl, newValue, _op.location()); + assignment(decl, newValue, _op.location()); defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue); } else @@ -337,11 +330,11 @@ void SMTChecker::endVisit(UnaryOperation const& _op) void SMTChecker::endVisit(BinaryOperation const& _op) { - if (Token::isArithmeticOp(_op.getOperator())) + if (TokenTraits::isArithmeticOp(_op.getOperator())) arithmeticOperation(_op); - else if (Token::isCompareOp(_op.getOperator())) + else if (TokenTraits::isCompareOp(_op.getOperator())) compareOperation(_op); - else if (Token::isBooleanOp(_op.getOperator())) + else if (TokenTraits::isBooleanOp(_op.getOperator())) booleanOperation(_op); else m_errorReporter.warning( @@ -366,49 +359,162 @@ void SMTChecker::endVisit(FunctionCall const& _funCall) std::vector<ASTPointer<Expression const>> 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::GasLeft) + visitGasLeft(_funCall); + else if (funType.kind() == FunctionType::Kind::BlockHash) + visitBlockHash(_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::visitGasLeft(FunctionCall const& _funCall) +{ + string gasLeft = "gasleft()"; + // We increase the variable index since gasleft changes + // inside a tx. + defineSpecialVariable(gasLeft, _funCall, true); + auto const& symbolicVar = m_specialVariables.at(gasLeft); + unsigned index = symbolicVar->index(); + // We set the current value to unknown anyway to add type constraints. + symbolicVar->setUnknownValue(); + if (index > 0) + m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1)); +} + +void SMTChecker::visitBlockHash(FunctionCall const& _funCall) +{ + string blockHash = "blockhash()"; + // TODO Define blockhash as an uninterpreted function + defineSpecialVariable(blockHash, _funCall); +} + +void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall) +{ + FunctionDefinition const* _funDef = nullptr; + Expression const* _calledExpr = &_funCall.expression(); + + if (TupleExpression const* _fun = dynamic_cast<TupleExpression const*>(&_funCall.expression())) + { + solAssert(_fun->components().size() == 1, ""); + _calledExpr = _fun->components().at(0).get(); + } + + if (Identifier const* _fun = dynamic_cast<Identifier const*>(_calledExpr)) + _funDef = dynamic_cast<FunctionDefinition const*>(_fun->annotation().referencedDeclaration); + else if (MemberAccess const* _fun = dynamic_cast<MemberAccess const*>(_calledExpr)) + _funDef = dynamic_cast<FunctionDefinition const*>(_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<smt::Expression> 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." + ); } } void SMTChecker::endVisit(Identifier const& _identifier) { - Declaration const* decl = _identifier.annotation().referencedDeclaration; - solAssert(decl, ""); if (_identifier.annotation().lValueRequested) { // Will be translated as part of the node that requested the lvalue. } - else if (SSAVariable::isSupportedType(_identifier.annotation().type->category())) - defineExpr(_identifier, currentValue(*decl)); else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get())) { - if (fun->kind() == FunctionType::Kind::Assert || fun->kind() == FunctionType::Kind::Require) + if ( + fun->kind() == FunctionType::Kind::Assert || + fun->kind() == FunctionType::Kind::Require || + fun->kind() == FunctionType::Kind::GasLeft || + fun->kind() == FunctionType::Kind::BlockHash + ) return; + createExpr(_identifier); + } + else if (isSupportedType(_identifier.annotation().type->category())) + { + if (VariableDeclaration const* decl = dynamic_cast<VariableDeclaration const*>(_identifier.annotation().referencedDeclaration)) + defineExpr(_identifier, currentValue(*decl)); + else if (_identifier.name() == "now") + defineSpecialVariable(_identifier.name(), _identifier); + else + // TODO: handle MagicVariableDeclaration here + m_errorReporter.warning( + _identifier.location(), + "Assertion checker does not yet support the type of this variable." + ); } } void SMTChecker::endVisit(Literal const& _literal) { Type const& type = *_literal.annotation().type; - if (type.category() == Type::Category::Integer || type.category() == Type::Category::RationalNumber) - { - if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(&type)) - solAssert(!rational->isFractional(), ""); + if (isNumber(type.category())) defineExpr(_literal, smt::Expression(type.literalValue(&_literal))); - } - else if (type.category() == Type::Category::Bool) + else if (isBool(type.category())) defineExpr(_literal, smt::Expression(_literal.token() == Token::TrueLiteral ? true : false)); else m_errorReporter.warning( @@ -419,6 +525,69 @@ void SMTChecker::endVisit(Literal const& _literal) ); } +void SMTChecker::endVisit(Return const& _return) +{ + if (knownExpr(*_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])); + } +} + +bool SMTChecker::visit(MemberAccess const& _memberAccess) +{ + auto const& exprType = _memberAccess.expression().annotation().type; + solAssert(exprType, ""); + if (exprType->category() == Type::Category::Magic) + { + auto identifier = dynamic_cast<Identifier const*>(&_memberAccess.expression()); + string accessedName; + if (identifier) + accessedName = identifier->name(); + else + m_errorReporter.warning( + _memberAccess.location(), + "Assertion checker does not yet support this expression." + ); + defineSpecialVariable(accessedName + "." + _memberAccess.memberName(), _memberAccess); + return false; + } + else + m_errorReporter.warning( + _memberAccess.location(), + "Assertion checker does not yet support this expression." + ); + + return true; +} + +void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _expr, bool _increaseIndex) +{ + if (!knownSpecialVariable(_name)) + { + auto result = newSymbolicVariable(*_expr.annotation().type, _name, *m_interface); + m_specialVariables.emplace(_name, result.second); + result.second->setUnknownValue(); + if (result.first) + m_errorReporter.warning( + _expr.location(), + "Assertion checker does not yet support this special variable." + ); + } + else if (_increaseIndex) + m_specialVariables.at(_name)->increaseIndex(); + // The default behavior is not to increase the index since + // most of the special values stay the same throughout a tx. + defineExpr(_expr, m_specialVariables.at(_name)->currentValue()); +} + + void SMTChecker::arithmeticOperation(BinaryOperation const& _op) { switch (_op.getOperator()) @@ -429,11 +598,18 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op) case Token::Div: { solAssert(_op.annotation().commonType, ""); - solAssert(_op.annotation().commonType->category() == Type::Category::Integer, ""); + if (_op.annotation().commonType->category() != Type::Category::Integer) + { + m_errorReporter.warning( + _op.location(), + "Assertion checker does not yet implement this operator on non-integer types." + ); + break; + } auto const& intType = dynamic_cast<IntegerType const&>(*_op.annotation().commonType); smt::Expression left(expr(_op.leftExpression())); smt::Expression right(expr(_op.rightExpression())); - Token::Value op = _op.getOperator(); + Token op = _op.getOperator(); smt::Expression value( op == Token::Add ? left + right : op == Token::Sub ? left - right : @@ -443,7 +619,7 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op) if (_op.getOperator() == Token::Div) { - checkCondition(right == 0, _op.location(), "Division by zero", "value", &right); + checkCondition(right == 0, _op.location(), "Division by zero", "<result>", &right); m_interface->addAssertion(right != 0); } @@ -463,13 +639,13 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op) void SMTChecker::compareOperation(BinaryOperation const& _op) { solAssert(_op.annotation().commonType, ""); - if (SSAVariable::isSupportedType(_op.annotation().commonType->category())) + if (isSupportedType(_op.annotation().commonType->category())) { smt::Expression left(expr(_op.leftExpression())); smt::Expression right(expr(_op.rightExpression())); - Token::Value op = _op.getOperator(); + Token op = _op.getOperator(); shared_ptr<smt::Expression> value; - if (SSAVariable::isInteger(_op.annotation().commonType->category())) + if (isNumber(_op.annotation().commonType->category())) { value = make_shared<smt::Expression>( op == Token::Equal ? (left == right) : @@ -482,14 +658,10 @@ void SMTChecker::compareOperation(BinaryOperation const& _op) } else // Bool { - solUnimplementedAssert(SSAVariable::isBool(_op.annotation().commonType->category()), "Operation not yet supported"); + solUnimplementedAssert(isBool(_op.annotation().commonType->category()), "Operation not yet supported"); value = make_shared<smt::Expression>( op == Token::Equal ? (left == right) : - op == Token::NotEqual ? (left != right) : - op == Token::LessThan ? (!left && right) : - op == Token::LessThanOrEqual ? (!left || right) : - op == Token::GreaterThan ? (left && !right) : - /*op == Token::GreaterThanOrEqual*/ (left || !right) + /*op == Token::NotEqual*/ (left != right) ); } // TODO: check that other values for op are not possible. @@ -534,37 +706,37 @@ smt::Expression SMTChecker::division(smt::Expression _left, smt::Expression _rig return _left / _right; } -void SMTChecker::assignment(Declaration const& _variable, Expression const& _value, SourceLocation const& _location) +void SMTChecker::assignment(VariableDeclaration const& _variable, Expression const& _value, SourceLocation const& _location) { assignment(_variable, expr(_value), _location); } -void SMTChecker::assignment(Declaration const& _variable, smt::Expression const& _value, SourceLocation const& _location) +void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expression const& _value, SourceLocation const& _location) { TypePointer type = _variable.type(); if (auto const* intType = dynamic_cast<IntegerType const*>(type.get())) checkUnderOverflow(_value, *intType, _location); + else if (dynamic_cast<AddressType const*>(type.get())) + checkUnderOverflow(_value, IntegerType(160), _location); m_interface->addAssertion(newValue(_variable) == _value); } -SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition) +SMTChecker::VariableIndices SMTChecker::visitBranch(Statement const& _statement, smt::Expression _condition) { return visitBranch(_statement, &_condition); } -SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition) +SMTChecker::VariableIndices SMTChecker::visitBranch(Statement const& _statement, smt::Expression const* _condition) { - VariableSequenceCounters beforeVars = m_variables; - + auto indicesBeforeBranch = copyVariableIndices(); if (_condition) pushPathCondition(*_condition); _statement.accept(*this); if (_condition) popPathCondition(); - - std::swap(m_variables, beforeVars); - - return beforeVars; + auto indicesAfterBranch = copyVariableIndices(); + resetVariableIndices(indicesBeforeBranch); + return indicesAfterBranch; } void SMTChecker::checkCondition( @@ -580,31 +752,24 @@ void SMTChecker::checkCondition( vector<smt::Expression> expressionsToEvaluate; vector<string> expressionNames; - if (m_currentFunction) + if (m_functionPath.size()) { + solAssert(m_scanner, ""); if (_additionalValue) { expressionsToEvaluate.emplace_back(*_additionalValue); expressionNames.push_back(_additionalValueName); } - for (auto const& param: m_currentFunction->parameters()) - if (knownVariable(*param)) - { - expressionsToEvaluate.emplace_back(currentValue(*param)); - expressionNames.push_back(param->name()); - } - for (auto const& var: m_currentFunction->localVariables()) - if (knownVariable(*var)) - { - expressionsToEvaluate.emplace_back(currentValue(*var)); - expressionNames.push_back(var->name()); - } - for (auto const& var: m_stateVariables) - if (knownVariable(*var.first)) - { - expressionsToEvaluate.emplace_back(currentValue(*var.first)); - expressionNames.push_back(var.first->name()); - } + for (auto const& var: m_variables) + { + expressionsToEvaluate.emplace_back(currentValue(*var.first)); + expressionNames.push_back(var.first->name()); + } + for (auto const& var: m_specialVariables) + { + expressionsToEvaluate.emplace_back(var.second->currentValue()); + expressionNames.push_back(var.first); + } } smt::CheckResult result; vector<string> values; @@ -621,17 +786,25 @@ void SMTChecker::checkCondition( { std::ostringstream message; message << _description << " happens here"; - if (m_currentFunction) + if (m_functionPath.size()) { - message << " for:\n"; + std::ostringstream modelMessage; + modelMessage << " for:\n"; solAssert(values.size() == expressionNames.size(), ""); + map<string, string> sortedModel; for (size_t i = 0; i < values.size(); ++i) if (expressionsToEvaluate.at(i).name != values.at(i)) - message << " " << expressionNames.at(i) << " = " << values.at(i) << "\n"; + sortedModel[expressionNames.at(i)] = values.at(i); + + for (auto const& eval: sortedModel) + modelMessage << " " << eval.first << " = " << eval.second << "\n"; + m_errorReporter.warning(_location, message.str() + loopComment, SecondarySourceLocation().append(modelMessage.str(), SourceLocation())); } else + { message << "."; - m_errorReporter.warning(_location, message.str() + loopComment); + m_errorReporter.warning(_location, message.str() + loopComment); + } break; } case smt::CheckResult::UNSATISFIABLE: @@ -639,11 +812,12 @@ void SMTChecker::checkCondition( case smt::CheckResult::UNKNOWN: m_errorReporter.warning(_location, _description + " might happen here." + loopComment); break; + case smt::CheckResult::CONFLICTING: + m_errorReporter.warning(_location, "At least two SMT solvers provided conflicting answers. Results might not be sound."); + break; case smt::CheckResult::ERROR: m_errorReporter.warning(_location, "Error trying to invoke SMT solver."); break; - default: - solAssert(false, ""); } m_interface->pop(); } @@ -666,6 +840,8 @@ void SMTChecker::checkBooleanNotConstant(Expression const& _condition, string co if (positiveResult == smt::CheckResult::ERROR || negatedResult == smt::CheckResult::ERROR) m_errorReporter.warning(_condition.location(), "Error trying to invoke SMT solver."); + else if (positiveResult == smt::CheckResult::CONFLICTING || negatedResult == smt::CheckResult::CONFLICTING) + m_errorReporter.warning(_condition.location(), "At least two SMT solvers provided conflicting answers. Results might not be sound."); else if (positiveResult == smt::CheckResult::SATISFIABLE && negatedResult == smt::CheckResult::SATISFIABLE) { // everything fine. @@ -726,6 +902,30 @@ smt::CheckResult SMTChecker::checkSatisfiable() return checkSatisfiableAndGenerateModel({}).first; } +void SMTChecker::initializeFunctionCallParameters(FunctionDefinition const& _function, vector<smt::Expression> 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()) @@ -742,16 +942,30 @@ 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_stateVariables) + for (auto const& variable: m_variables) { - newValue(*variable.first); - setUnknownValue(*variable.first); + if (variable.first->isStateVariable()) + { + newValue(*variable.first); + setUnknownValue(*variable.first); + } } } -void SMTChecker::resetVariables(vector<Declaration const*> _variables) +void SMTChecker::resetVariables(vector<VariableDeclaration const*> _variables) { for (auto const* decl: _variables) { @@ -760,38 +974,33 @@ void SMTChecker::resetVariables(vector<Declaration const*> _variables) } } -void SMTChecker::mergeVariables(vector<Declaration const*> const& _variables, smt::Expression const& _condition, VariableSequenceCounters const& _countersEndTrue, VariableSequenceCounters const& _countersEndFalse) +void SMTChecker::mergeVariables(vector<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse) { - set<Declaration const*> uniqueVars(_variables.begin(), _variables.end()); + set<VariableDeclaration const*> uniqueVars(_variables.begin(), _variables.end()); for (auto const* decl: uniqueVars) { - int trueCounter = _countersEndTrue.at(decl).index(); - int falseCounter = _countersEndFalse.at(decl).index(); - solAssert(trueCounter != falseCounter, ""); + solAssert(_indicesEndTrue.count(decl) && _indicesEndFalse.count(decl), ""); + int trueIndex = _indicesEndTrue.at(decl); + int falseIndex = _indicesEndFalse.at(decl); + solAssert(trueIndex != falseIndex, ""); m_interface->addAssertion(newValue(*decl) == smt::Expression::ite( _condition, - valueAtSequence(*decl, trueCounter), - valueAtSequence(*decl, falseCounter)) + valueAtIndex(*decl, trueIndex), + valueAtIndex(*decl, falseIndex)) ); } } bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) { - if (SSAVariable::isSupportedType(_varDecl.type()->category())) - { - solAssert(m_variables.count(&_varDecl) == 0, ""); - solAssert(m_stateVariables.count(&_varDecl) == 0, ""); - if (_varDecl.isLocalVariable()) - m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface)); - else - { - solAssert(_varDecl.isStateVariable(), ""); - m_stateVariables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface)); - } + // This might be the case for multiple calls to the same function. + if (knownVariable(_varDecl)) return true; - } - else + auto const& type = _varDecl.type(); + solAssert(m_variables.count(&_varDecl) == 0, ""); + auto result = newSymbolicVariable(*type, _varDecl.name() + "_" + to_string(_varDecl.id()), *m_interface); + m_variables.emplace(&_varDecl, result.second); + if (result.first) { m_errorReporter.warning( _varDecl.location(), @@ -799,84 +1008,78 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) ); return false; } + return true; } -string SMTChecker::uniqueSymbol(Expression const& _expr) -{ - return "expr_" + to_string(_expr.id()); -} - -bool SMTChecker::knownVariable(Declaration const& _decl) +bool SMTChecker::knownVariable(VariableDeclaration const& _decl) { return m_variables.count(&_decl); } -smt::Expression SMTChecker::currentValue(Declaration const& _decl) +smt::Expression SMTChecker::currentValue(VariableDeclaration const& _decl) { solAssert(knownVariable(_decl), ""); - return m_variables.at(&_decl)(); + return m_variables.at(&_decl)->currentValue(); } -smt::Expression SMTChecker::valueAtSequence(Declaration const& _decl, int _sequence) +smt::Expression SMTChecker::valueAtIndex(VariableDeclaration const& _decl, int _index) { solAssert(knownVariable(_decl), ""); - return m_variables.at(&_decl)(_sequence); + return m_variables.at(&_decl)->valueAtIndex(_index); } -smt::Expression SMTChecker::newValue(Declaration const& _decl) +smt::Expression SMTChecker::newValue(VariableDeclaration const& _decl) { solAssert(knownVariable(_decl), ""); - ++m_variables.at(&_decl); - return m_variables.at(&_decl)(); + return m_variables.at(&_decl)->increaseIndex(); } -void SMTChecker::setZeroValue(Declaration const& _decl) +void SMTChecker::setZeroValue(VariableDeclaration const& _decl) { solAssert(knownVariable(_decl), ""); - m_variables.at(&_decl).setZeroValue(); + m_variables.at(&_decl)->setZeroValue(); } -void SMTChecker::setUnknownValue(Declaration const& _decl) +void SMTChecker::setUnknownValue(VariableDeclaration const& _decl) { solAssert(knownVariable(_decl), ""); - m_variables.at(&_decl).setUnknownValue(); + m_variables.at(&_decl)->setUnknownValue(); } smt::Expression SMTChecker::expr(Expression const& _e) { - if (!m_expressions.count(&_e)) + if (!knownExpr(_e)) { m_errorReporter.warning(_e.location(), "Internal error: Expression undefined for SMT solver." ); createExpr(_e); } - return m_expressions.at(&_e); + return m_expressions.at(&_e)->currentValue(); +} + +bool SMTChecker::knownExpr(Expression const& _e) const +{ + return m_expressions.count(&_e); +} + +bool SMTChecker::knownSpecialVariable(string const& _var) const +{ + return m_specialVariables.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." ); + solAssert(_e.annotation().type, ""); + if (knownExpr(_e)) + m_expressions.at(&_e)->increaseIndex(); else { - solAssert(_e.annotation().type, ""); - switch (_e.annotation().type->category()) - { - case Type::Category::RationalNumber: - { - if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_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: - solUnimplementedAssert(false, "Type not implemented."); - } + auto result = newSymbolicVariable(*_e.annotation().type, "expr_" + to_string(_e.id()), *m_interface); + m_expressions.emplace(&_e, result.second); + if (result.first) + m_errorReporter.warning( + _e.location(), + "Assertion checker does not yet implement this type." + ); } } @@ -899,7 +1102,7 @@ void SMTChecker::pushPathCondition(smt::Expression const& _e) smt::Expression SMTChecker::currentPathConditions() { - if (m_pathConditions.size() == 0) + if (m_pathConditions.empty()) return smt::Expression(true); return m_pathConditions.back(); } @@ -913,3 +1116,27 @@ void SMTChecker::addPathImpliedExpression(smt::Expression const& _e) { m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), _e)); } + +bool SMTChecker::isRootFunction() +{ + return m_functionPath.size() == 1; +} + +bool SMTChecker::visitedFunction(FunctionDefinition const* _funDef) +{ + return contains(m_functionPath, _funDef); +} + +SMTChecker::VariableIndices SMTChecker::copyVariableIndices() +{ + VariableIndices indices; + for (auto const& var: m_variables) + indices.emplace(var.first, var.second->index()); + return indices; +} + +void SMTChecker::resetVariableIndices(VariableIndices const& _indices) +{ + for (auto const& var: _indices) + m_variables.at(var.first)->index() = var.second; +} diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 50d40ab9..a7f955dd 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -19,14 +19,15 @@ #include <libsolidity/formal/SolverInterface.h> - -#include <libsolidity/formal/SSAVariable.h> +#include <libsolidity/formal/SymbolicVariables.h> #include <libsolidity/ast/ASTVisitor.h> #include <libsolidity/interface/ReadFile.h> -#include <map> +#include <libsolidity/parsing/Scanner.h> + +#include <unordered_map> #include <string> #include <vector> @@ -43,7 +44,7 @@ class SMTChecker: private ASTConstVisitor public: SMTChecker(ErrorReporter& _errorReporter, ReadCallback::Callback const& _readCallback); - void analyze(SourceUnit const& _sources); + void analyze(SourceUnit const& _sources, std::shared_ptr<Scanner> const& _scanner); private: // TODO: Check that we do not have concurrent reads and writes to a variable, @@ -59,7 +60,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,26 +67,38 @@ 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; + virtual bool visit(MemberAccess 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&); + void visitGasLeft(FunctionCall const&); + void visitBlockHash(FunctionCall const&); + /// Visits the FunctionDefinition of the called function + /// if available and inlines the return value. + void inlineFunctionCall(FunctionCall const&); + + void defineSpecialVariable(std::string const& _name, Expression const& _expr, bool _increaseIndex = false); + /// 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); - void assignment(Declaration const& _variable, Expression const& _value, SourceLocation const& _location); - void assignment(Declaration const& _variable, smt::Expression const& _value, SourceLocation const& _location); + void assignment(VariableDeclaration const& _variable, Expression const& _value, SourceLocation const& _location); + void assignment(VariableDeclaration const& _variable, smt::Expression const& _value, SourceLocation const& _location); /// Maps a variable to an SSA index. - using VariableSequenceCounters = std::map<Declaration const*, SSAVariable>; + using VariableIndices = std::unordered_map<VariableDeclaration const*, int>; /// Visits the branch given by the statement, pushes and pops the current path conditions. /// @param _condition if present, asserts that this condition is true within the branch. - /// @returns the variable sequence counter after visiting the branch. - VariableSequenceCounters visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr); - VariableSequenceCounters visitBranch(Statement const& _statement, smt::Expression _condition); + /// @returns the variable indices after visiting the branch. + VariableIndices visitBranch(Statement const& _statement, smt::Expression const* _condition = nullptr); + VariableIndices visitBranch(Statement const& _statement, smt::Expression _condition); /// Check that a condition can be satisfied. void checkCondition( @@ -113,43 +125,47 @@ private: smt::CheckResult checkSatisfiable(); void initializeLocalVariables(FunctionDefinition const& _function); + void initializeFunctionCallParameters(FunctionDefinition const& _function, std::vector<smt::Expression> const& _callArgs); void resetStateVariables(); - void resetVariables(std::vector<Declaration const*> _variables); + void resetVariables(std::vector<VariableDeclaration const*> _variables); /// Given two different branches and the touched variables, /// merge the touched variables into after-branch ite variables /// using the branch condition as guard. - void mergeVariables(std::vector<Declaration const*> const& _variables, smt::Expression const& _condition, VariableSequenceCounters const& _countersEndTrue, VariableSequenceCounters const& _countersEndFalse); + void mergeVariables(std::vector<VariableDeclaration const*> const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse); /// Tries to create an uninitialized variable and returns true on success. /// This fails if the type is not supported. bool createVariable(VariableDeclaration const& _varDecl); - static std::string uniqueSymbol(Expression const& _expr); - /// @returns true if _delc is a variable that is known at the current point, i.e. - /// has a valid sequence number - bool knownVariable(Declaration const& _decl); + /// has a valid index + bool knownVariable(VariableDeclaration const& _decl); /// @returns an expression denoting the value of the variable declared in @a _decl /// at the current point. - smt::Expression currentValue(Declaration const& _decl); + smt::Expression currentValue(VariableDeclaration const& _decl); /// @returns an expression denoting the value of the variable declared in @a _decl - /// at the given sequence point. Does not ensure that this sequence point exists. - smt::Expression valueAtSequence(Declaration const& _decl, int _sequence); - /// Allocates a new sequence number for the declaration, updates the current - /// sequence number to this value and returns the expression. - smt::Expression newValue(Declaration const& _decl); + /// at the given index. Does not ensure that this index exists. + smt::Expression valueAtIndex(VariableDeclaration const& _decl, int _index); + /// Allocates a new index for the declaration, updates the current + /// index to this value and returns the expression. + smt::Expression newValue(VariableDeclaration const& _decl); /// Sets the value of the declaration to zero. - void setZeroValue(Declaration const& _decl); + void setZeroValue(VariableDeclaration const& _decl); /// Resets the variable to an unknown value (in its range). - void setUnknownValue(Declaration const& decl); + void setUnknownValue(VariableDeclaration const& decl); /// Returns the expression corresponding to the AST node. Throws if the expression does not exist. smt::Expression expr(Expression const& _e); /// Creates the expression (value can be arbitrary) void createExpr(Expression const& _e); + /// Checks if expression was created + bool knownExpr(Expression const& _e) const; /// Creates the expression and sets its value. void defineExpr(Expression const& _e, smt::Expression _value); + /// Checks if special variable was seen. + bool knownSpecialVariable(std::string const& _var) const; + /// Adds a new path condition void pushPathCondition(smt::Expression const& _e); /// Remove the last path condition @@ -161,16 +177,33 @@ private: /// Add to the solver: the given expression implied by the current path conditions void addPathImpliedExpression(smt::Expression const& _e); + /// Removes local variables from the context. + void removeLocalVariables(); + + /// Copy the SSA indices of m_variables. + VariableIndices copyVariableIndices(); + /// Resets the variable indices. + void resetVariableIndices(VariableIndices const& _indices); + std::shared_ptr<smt::SolverInterface> m_interface; std::shared_ptr<VariableUsage> m_variableUsage; bool m_loopExecutionHappened = false; - std::map<Expression const*, smt::Expression> m_expressions; - std::map<Declaration const*, SSAVariable> m_variables; - std::map<Declaration const*, SSAVariable> m_stateVariables; + /// An Expression may have multiple smt::Expression due to + /// repeated calls to the same function. + std::unordered_map<Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions; + std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables; + std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> m_specialVariables; std::vector<smt::Expression> m_pathConditions; ErrorReporter& m_errorReporter; - - FunctionDefinition const* m_currentFunction = nullptr; + std::shared_ptr<Scanner> m_scanner; + + /// Stores the current path of function calls. + std::vector<FunctionDefinition const*> 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); }; } diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp index 0e00665a..a6c1f87c 100644 --- a/libsolidity/formal/SMTLib2Interface.cpp +++ b/libsolidity/formal/SMTLib2Interface.cpp @@ -47,6 +47,8 @@ void SMTLib2Interface::reset() { m_accumulatedOutput.clear(); m_accumulatedOutput.emplace_back(); + m_constants.clear(); + m_functions.clear(); write("(set-option :produce-models true)"); write("(set-logic QF_UFLIA)"); } @@ -62,30 +64,40 @@ void SMTLib2Interface::pop() m_accumulatedOutput.pop_back(); } -Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codomain) +void SMTLib2Interface::declareFunction(string _name, Sort _domain, Sort _codomain) { - write( - "(declare-fun |" + - _name + - "| (" + - (_domain == Sort::Int ? "Int" : "Bool") + - ") " + - (_codomain == Sort::Int ? "Int" : "Bool") + - ")" - ); - return SolverInterface::newFunction(move(_name), _domain, _codomain); + // TODO Use domain and codomain as key as well + if (!m_functions.count(_name)) + { + m_functions.insert(_name); + write( + "(declare-fun |" + + _name + + "| (" + + (_domain == Sort::Int ? "Int" : "Bool") + + ") " + + (_codomain == Sort::Int ? "Int" : "Bool") + + ")" + ); + } } -Expression SMTLib2Interface::newInteger(string _name) +void SMTLib2Interface::declareInteger(string _name) { - write("(declare-const |" + _name + "| Int)"); - return SolverInterface::newInteger(move(_name)); + if (!m_constants.count(_name)) + { + m_constants.insert(_name); + write("(declare-const |" + _name + "| Int)"); + } } -Expression SMTLib2Interface::newBool(string _name) +void SMTLib2Interface::declareBool(string _name) { - write("(declare-const |" + _name + "| Bool)"); - return SolverInterface::newBool(std::move(_name)); + if (!m_constants.count(_name)) + { + m_constants.insert(_name); + write("(declare-const |" + _name + "| Bool)"); + } } void SMTLib2Interface::addAssertion(Expression const& _expr) @@ -112,7 +124,7 @@ pair<CheckResult, vector<string>> SMTLib2Interface::check(vector<Expression> con result = CheckResult::ERROR; vector<string> values; - if (result != CheckResult::UNSATISFIABLE && result != CheckResult::ERROR) + if (result == CheckResult::SATISFIABLE && result != CheckResult::ERROR) values = parseValues(find(response.cbegin(), response.cend(), '\n'), response.cend()); return make_pair(result, values); } @@ -146,7 +158,7 @@ string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _ { auto const& e = _expressionsToEvaluate.at(i); solAssert(e.sort == Sort::Int || e.sort == Sort::Bool, "Invalid sort for expression to evaluate."); - command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort == Sort::Int ? "Int" : "Bool") + "\n"; + command += "(declare-const |EVALEXPR_" + to_string(i) + "| " + (e.sort == Sort::Int ? "Int" : "Bool") + ")\n"; command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n"; } command += "(check-sat)\n"; diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h index 63188acd..eb876a7f 100644 --- a/libsolidity/formal/SMTLib2Interface.h +++ b/libsolidity/formal/SMTLib2Interface.h @@ -30,6 +30,7 @@ #include <string> #include <vector> #include <cstdio> +#include <set> namespace dev { @@ -48,9 +49,9 @@ public: void push() override; void pop() override; - Expression newFunction(std::string _name, Sort _domain, Sort _codomain) override; - Expression newInteger(std::string _name) override; - Expression newBool(std::string _name) override; + void declareFunction(std::string _name, Sort _domain, Sort _codomain) override; + void declareInteger(std::string _name) override; + void declareBool(std::string _name) override; void addAssertion(Expression const& _expr) override; std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override; @@ -68,6 +69,8 @@ private: ReadCallback::Callback m_queryCallback; std::vector<std::string> m_accumulatedOutput; + std::set<std::string> m_constants; + std::set<std::string> m_functions; }; } diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp new file mode 100644 index 00000000..8b9fe9ce --- /dev/null +++ b/libsolidity/formal/SMTPortfolio.cpp @@ -0,0 +1,152 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see <http://www.gnu.org/licenses/>. +*/ + +#include <libsolidity/formal/SMTPortfolio.h> + +#ifdef HAVE_Z3 +#include <libsolidity/formal/Z3Interface.h> +#endif +#ifdef HAVE_CVC4 +#include <libsolidity/formal/CVC4Interface.h> +#endif +#if !defined (HAVE_Z3) && !defined (HAVE_CVC4) +#include <libsolidity/formal/SMTLib2Interface.h> +#endif + +using namespace std; +using namespace dev; +using namespace dev::solidity; +using namespace dev::solidity::smt; + +SMTPortfolio::SMTPortfolio(ReadCallback::Callback const& _readCallback) +{ +#ifdef HAVE_Z3 + m_solvers.emplace_back(make_shared<smt::Z3Interface>()); +#endif +#ifdef HAVE_CVC4 + m_solvers.emplace_back(make_shared<smt::CVC4Interface>()); +#endif +#if !defined (HAVE_Z3) && !defined (HAVE_CVC4) + m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_readCallback)), +#endif + (void)_readCallback; +} + +void SMTPortfolio::reset() +{ + for (auto s : m_solvers) + s->reset(); +} + +void SMTPortfolio::push() +{ + for (auto s : m_solvers) + s->push(); +} + +void SMTPortfolio::pop() +{ + for (auto s : m_solvers) + s->pop(); +} + +void SMTPortfolio::declareFunction(string _name, Sort _domain, Sort _codomain) +{ + for (auto s : m_solvers) + s->declareFunction(_name, _domain, _codomain); +} + +void SMTPortfolio::declareInteger(string _name) +{ + for (auto s : m_solvers) + s->declareInteger(_name); +} + +void SMTPortfolio::declareBool(string _name) +{ + for (auto s : m_solvers) + s->declareBool(_name); +} + +void SMTPortfolio::addAssertion(Expression const& _expr) +{ + for (auto s : m_solvers) + s->addAssertion(_expr); +} + +/* + * Broadcasts the SMT query to all solvers and returns a single result. + * This comment explains how this result is decided. + * + * When a solver is queried, there are four possible answers: + * SATISFIABLE (SAT), UNSATISFIABLE (UNSAT), UNKNOWN, CONFLICTING, ERROR + * We say that a solver _answered_ the query if it returns either: + * SAT or UNSAT + * A solver did not answer the query if it returns either: + * UNKNOWN (it tried but couldn't solve it) or ERROR (crash, internal error, API error, etc). + * + * Ideally all solvers answer the query and agree on what the answer is + * (all say SAT or all say UNSAT). + * + * The actual logic as as follows: + * 1) If at least one solver answers the query, all the non-answer results are ignored. + * Here SAT/UNSAT is preferred over UNKNOWN since it's an actual answer, and over ERROR + * because one buggy solver/integration shouldn't break the portfolio. + * + * 2) If at least one solver answers SAT and at least one answers UNSAT, at least one of them is buggy + * and the result is CONFLICTING. + * In the future if we have more than 2 solvers enabled we could go with the majority. + * + * 3) If NO solver answers the query: + * If at least one solver returned UNKNOWN (where the rest returned ERROR), the result is UNKNOWN. + * This is preferred over ERROR since the SMTChecker might decide to abstract the query + * when it is told that this is a hard query to solve. + * + * If all solvers return ERROR, the result is ERROR. +*/ +pair<CheckResult, vector<string>> SMTPortfolio::check(vector<Expression> const& _expressionsToEvaluate) +{ + CheckResult lastResult = CheckResult::ERROR; + vector<string> finalValues; + for (auto s : m_solvers) + { + CheckResult result; + vector<string> values; + tie(result, values) = s->check(_expressionsToEvaluate); + if (solverAnswered(result)) + { + if (!solverAnswered(lastResult)) + { + lastResult = result; + finalValues = std::move(values); + } + else if (lastResult != result) + { + lastResult = CheckResult::CONFLICTING; + break; + } + } + else if (result == CheckResult::UNKNOWN && lastResult == CheckResult::ERROR) + lastResult = result; + } + return make_pair(lastResult, finalValues); +} + +bool SMTPortfolio::solverAnswered(CheckResult result) +{ + return result == CheckResult::SATISFIABLE || result == CheckResult::UNSATISFIABLE; +} diff --git a/libsolidity/formal/SMTPortfolio.h b/libsolidity/formal/SMTPortfolio.h new file mode 100644 index 00000000..96c7ff57 --- /dev/null +++ b/libsolidity/formal/SMTPortfolio.h @@ -0,0 +1,67 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see <http://www.gnu.org/licenses/>. +*/ + +#pragma once + + +#include <libsolidity/formal/SolverInterface.h> + +#include <libsolidity/interface/ReadFile.h> + +#include <boost/noncopyable.hpp> + +#include <vector> + +namespace dev +{ +namespace solidity +{ +namespace smt +{ + +/** + * The SMTPortfolio wraps all available solvers within a single interface, + * propagating the functionalities to all solvers. + * It also checks whether different solvers give conflicting answers + * to SMT queries. + */ +class SMTPortfolio: public SolverInterface, public boost::noncopyable +{ +public: + SMTPortfolio(ReadCallback::Callback const& _readCallback); + + void reset() override; + + void push() override; + void pop() override; + + void declareFunction(std::string _name, Sort _domain, Sort _codomain) override; + void declareInteger(std::string _name) override; + void declareBool(std::string _name) override; + + void addAssertion(Expression const& _expr) override; + std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override; + +private: + static bool solverAnswered(CheckResult result); + + std::vector<std::shared_ptr<smt::SolverInterface>> m_solvers; +}; + +} +} +} diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp index f3213e03..36e15508 100644 --- a/libsolidity/formal/SSAVariable.cpp +++ b/libsolidity/formal/SSAVariable.cpp @@ -17,70 +17,17 @@ #include <libsolidity/formal/SSAVariable.h> -#include <libsolidity/formal/SymbolicBoolVariable.h> -#include <libsolidity/formal/SymbolicIntVariable.h> - -#include <libsolidity/ast/AST.h> - using namespace std; -using namespace dev; using namespace dev::solidity; -SSAVariable::SSAVariable( - Declaration const& _decl, - smt::SolverInterface& _interface -) +SSAVariable::SSAVariable() { resetIndex(); - - if (isInteger(_decl.type()->category())) - m_symbolicVar = make_shared<SymbolicIntVariable>(_decl, _interface); - else if (isBool(_decl.type()->category())) - m_symbolicVar = make_shared<SymbolicBoolVariable>(_decl, _interface); - else - { - solAssert(false, ""); - } -} - -bool SSAVariable::isSupportedType(Type::Category _category) -{ - return isInteger(_category) || isBool(_category); -} - -bool SSAVariable::isInteger(Type::Category _category) -{ - return _category == Type::Category::Integer; -} - -bool SSAVariable::isBool(Type::Category _category) -{ - return _category == Type::Category::Bool; } void SSAVariable::resetIndex() { - m_currentSequenceCounter = 0; - m_nextFreeSequenceCounter.reset (new int); - *m_nextFreeSequenceCounter = 1; -} - -int SSAVariable::index() const -{ - return m_currentSequenceCounter; -} - -int SSAVariable::next() const -{ - return *m_nextFreeSequenceCounter; -} - -void SSAVariable::setZeroValue() -{ - m_symbolicVar->setZeroValue(index()); -} - -void SSAVariable::setUnknownValue() -{ - m_symbolicVar->setUnknownValue(index()); + m_currentIndex = 0; + m_nextFreeIndex.reset (new unsigned); + *m_nextFreeIndex = 1; } diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h index bf5dae3b..46935472 100644 --- a/libsolidity/formal/SSAVariable.h +++ b/libsolidity/formal/SSAVariable.h @@ -17,8 +17,6 @@ #pragma once -#include <libsolidity/formal/SymbolicVariable.h> - #include <memory> namespace dev @@ -26,64 +24,29 @@ namespace dev namespace solidity { -class Declaration; - /** * This class represents the SSA representation of a program variable. */ class SSAVariable { public: - /// @param _decl Used to determine the type and forwarded to the symbolic var. - /// @param _interface Forwarded to the symbolic var such that it can give constraints to the solver. - SSAVariable( - Declaration const& _decl, - smt::SolverInterface& _interface - ); - + SSAVariable(); void resetIndex(); /// This function returns the current index of this SSA variable. - int index() const; - /// This function returns the next free index of this SSA variable. - int next() const; - - int operator++() - { - return m_currentSequenceCounter = (*m_nextFreeSequenceCounter)++; - } - - smt::Expression operator()() const - { - return valueAtSequence(index()); - } + unsigned index() const { return m_currentIndex; } + unsigned& index() { return m_currentIndex; } - smt::Expression operator()(int _seq) const + unsigned operator++() { - return valueAtSequence(_seq); + return m_currentIndex = (*m_nextFreeIndex)++; } - /// These two functions forward the call to the symbolic var - /// which generates the constraints according to the type. - void setZeroValue(); - void setUnknownValue(); - - /// So far Int and Bool are supported. - static bool isSupportedType(Type::Category _category); - static bool isInteger(Type::Category _category); - static bool isBool(Type::Category _category); - private: - smt::Expression valueAtSequence(int _seq) const - { - return (*m_symbolicVar)(_seq); - } - - std::shared_ptr<SymbolicVariable> m_symbolicVar = nullptr; - int m_currentSequenceCounter; - /// The next free sequence counter is a shared pointer because we want + unsigned m_currentIndex; + /// The next free index is a shared pointer because we want /// the copy and the copied to share it. - std::shared_ptr<int> m_nextFreeSequenceCounter; + std::shared_ptr<unsigned> m_nextFreeIndex; }; } diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h index 16796684..af1cc8e4 100644 --- a/libsolidity/formal/SolverInterface.h +++ b/libsolidity/formal/SolverInterface.h @@ -39,7 +39,7 @@ namespace smt enum class CheckResult { - SATISFIABLE, UNSATISFIABLE, UNKNOWN, ERROR + SATISFIABLE, UNSATISFIABLE, UNKNOWN, CONFLICTING, ERROR }; enum class Sort @@ -171,8 +171,8 @@ public: } } - std::string const name; - std::vector<Expression> const arguments; + std::string name; + std::vector<Expression> arguments; Sort sort; private: @@ -199,8 +199,10 @@ public: virtual void push() = 0; virtual void pop() = 0; - virtual Expression newFunction(std::string _name, Sort _domain, Sort _codomain) + virtual void declareFunction(std::string _name, Sort _domain, Sort _codomain) = 0; + Expression newFunction(std::string _name, Sort _domain, Sort _codomain) { + declareFunction(_name, _domain, _codomain); solAssert(_domain == Sort::Int, "Function sort not supported."); // Subclasses should do something here switch (_codomain) @@ -214,14 +216,18 @@ public: break; } } - virtual Expression newInteger(std::string _name) + virtual void declareInteger(std::string _name) = 0; + Expression newInteger(std::string _name) { // Subclasses should do something here + declareInteger(_name); return Expression(std::move(_name), {}, Sort::Int); } - virtual Expression newBool(std::string _name) + virtual void declareBool(std::string _name) = 0; + Expression newBool(std::string _name) { // Subclasses should do something here + declareBool(_name); return Expression(std::move(_name), {}, Sort::Bool); } @@ -231,8 +237,11 @@ public: /// is available. Throws SMTSolverError on error. virtual std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) = 0; -}; +protected: + // SMT query timeout in milliseconds. + static int const queryTimeout = 10000; +}; } } diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp deleted file mode 100644 index 5cf22d7d..00000000 --- a/libsolidity/formal/SymbolicBoolVariable.cpp +++ /dev/null @@ -1,47 +0,0 @@ -/* - This file is part of solidity. - - solidity is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - solidity is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with solidity. If not, see <http://www.gnu.org/licenses/>. -*/ - -#include <libsolidity/formal/SymbolicBoolVariable.h> - -#include <libsolidity/ast/AST.h> - -using namespace std; -using namespace dev; -using namespace dev::solidity; - -SymbolicBoolVariable::SymbolicBoolVariable( - Declaration const& _decl, - smt::SolverInterface&_interface -): - SymbolicVariable(_decl, _interface) -{ - solAssert(m_declaration.type()->category() == Type::Category::Bool, ""); -} - -smt::Expression SymbolicBoolVariable::valueAtSequence(int _seq) const -{ - return m_interface.newBool(uniqueSymbol(_seq)); -} - -void SymbolicBoolVariable::setZeroValue(int _seq) -{ - m_interface.addAssertion(valueAtSequence(_seq) == smt::Expression(false)); -} - -void SymbolicBoolVariable::setUnknownValue(int) -{ -} diff --git a/libsolidity/formal/SymbolicBoolVariable.h b/libsolidity/formal/SymbolicBoolVariable.h deleted file mode 100644 index 678f97d9..00000000 --- a/libsolidity/formal/SymbolicBoolVariable.h +++ /dev/null @@ -1,50 +0,0 @@ -/* - This file is part of solidity. - - solidity is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - solidity is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with solidity. If not, see <http://www.gnu.org/licenses/>. -*/ - -#pragma once - -#include <libsolidity/formal/SymbolicVariable.h> - -#include <libsolidity/ast/Types.h> - -namespace dev -{ -namespace solidity -{ - -/** - * Specialization of SymbolicVariable for Bool - */ -class SymbolicBoolVariable: public SymbolicVariable -{ -public: - SymbolicBoolVariable( - Declaration const& _decl, - smt::SolverInterface& _interface - ); - - /// Sets the var to false. - void setZeroValue(int _seq); - /// Does nothing since the SMT solver already knows the valid values. - void setUnknownValue(int _seq); - -protected: - smt::Expression valueAtSequence(int _seq) const; -}; - -} -} diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp deleted file mode 100644 index 5e71fdcc..00000000 --- a/libsolidity/formal/SymbolicIntVariable.cpp +++ /dev/null @@ -1,60 +0,0 @@ -/* - This file is part of solidity. - - solidity is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - solidity is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with solidity. If not, see <http://www.gnu.org/licenses/>. -*/ - -#include <libsolidity/formal/SymbolicIntVariable.h> - -#include <libsolidity/ast/AST.h> - -using namespace std; -using namespace dev; -using namespace dev::solidity; - -SymbolicIntVariable::SymbolicIntVariable( - Declaration const& _decl, - smt::SolverInterface& _interface -): - SymbolicVariable(_decl, _interface) -{ - solAssert(m_declaration.type()->category() == Type::Category::Integer, ""); -} - -smt::Expression SymbolicIntVariable::valueAtSequence(int _seq) const -{ - return m_interface.newInteger(uniqueSymbol(_seq)); -} - -void SymbolicIntVariable::setZeroValue(int _seq) -{ - m_interface.addAssertion(valueAtSequence(_seq) == 0); -} - -void SymbolicIntVariable::setUnknownValue(int _seq) -{ - auto const& intType = dynamic_cast<IntegerType const&>(*m_declaration.type()); - m_interface.addAssertion(valueAtSequence(_seq) >= minValue(intType)); - m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(intType)); -} - -smt::Expression SymbolicIntVariable::minValue(IntegerType const& _t) -{ - return smt::Expression(_t.minValue()); -} - -smt::Expression SymbolicIntVariable::maxValue(IntegerType const& _t) -{ - return smt::Expression(_t.maxValue()); -} diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h deleted file mode 100644 index d591e8db..00000000 --- a/libsolidity/formal/SymbolicIntVariable.h +++ /dev/null @@ -1,53 +0,0 @@ -/* - This file is part of solidity. - - solidity is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - solidity is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with solidity. If not, see <http://www.gnu.org/licenses/>. -*/ - -#pragma once - -#include <libsolidity/formal/SymbolicVariable.h> - -#include <libsolidity/ast/Types.h> - -namespace dev -{ -namespace solidity -{ - -/** - * Specialization of SymbolicVariable for Integers - */ -class SymbolicIntVariable: public SymbolicVariable -{ -public: - SymbolicIntVariable( - Declaration const& _decl, - smt::SolverInterface& _interface - ); - - /// Sets the var to 0. - void setZeroValue(int _seq); - /// Sets the variable to the full valid value range. - void setUnknownValue(int _seq); - - static smt::Expression minValue(IntegerType const& _t); - static smt::Expression maxValue(IntegerType const& _t); - -protected: - smt::Expression valueAtSequence(int _seq) const; -}; - -} -} diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp new file mode 100644 index 00000000..3eb1c1ce --- /dev/null +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -0,0 +1,127 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see <http://www.gnu.org/licenses/>. +*/ + +#include <libsolidity/formal/SymbolicTypes.h> + +#include <libsolidity/ast/Types.h> + +#include <memory> + +using namespace std; +using namespace dev::solidity; + +bool dev::solidity::isSupportedType(Type::Category _category) +{ + return isNumber(_category) || + isBool(_category) || + isFunction(_category); +} + +pair<bool, shared_ptr<SymbolicVariable>> dev::solidity::newSymbolicVariable( + Type const& _type, + std::string const& _uniqueName, + smt::SolverInterface& _solver +) +{ + bool abstract = false; + shared_ptr<SymbolicVariable> var; + TypePointer type = _type.shared_from_this(); + if (!isSupportedType(_type)) + { + abstract = true; + var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver); + } + else if (isBool(_type.category())) + var = make_shared<SymbolicBoolVariable>(type, _uniqueName, _solver); + else if (isFunction(_type.category())) + var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver); + else if (isInteger(_type.category())) + var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver); + else if (isFixedBytes(_type.category())) + { + auto fixedBytesType = dynamic_cast<FixedBytesType const*>(type.get()); + solAssert(fixedBytesType, ""); + var = make_shared<SymbolicFixedBytesVariable>(fixedBytesType->numBytes(), _uniqueName, _solver); + } + else if (isAddress(_type.category())) + var = make_shared<SymbolicAddressVariable>(_uniqueName, _solver); + else if (isRational(_type.category())) + { + auto rational = dynamic_cast<RationalNumberType const*>(&_type); + solAssert(rational, ""); + if (rational->isFractional()) + var = make_shared<SymbolicIntVariable>(make_shared<IntegerType>(256), _uniqueName, _solver); + else + var = make_shared<SymbolicIntVariable>(type, _uniqueName, _solver); + } + else + solAssert(false, ""); + return make_pair(abstract, var); +} + +bool dev::solidity::isSupportedType(Type const& _type) +{ + return isSupportedType(_type.category()); +} + +bool dev::solidity::isInteger(Type::Category _category) +{ + return _category == Type::Category::Integer; +} + +bool dev::solidity::isRational(Type::Category _category) +{ + return _category == Type::Category::RationalNumber; +} + +bool dev::solidity::isFixedBytes(Type::Category _category) +{ + return _category == Type::Category::FixedBytes; +} + +bool dev::solidity::isAddress(Type::Category _category) +{ + return _category == Type::Category::Address; +} + +bool dev::solidity::isNumber(Type::Category _category) +{ + return isInteger(_category) || + isRational(_category) || + isFixedBytes(_category) || + isAddress(_category); +} + +bool dev::solidity::isBool(Type::Category _category) +{ + return _category == Type::Category::Bool; +} + +bool dev::solidity::isFunction(Type::Category _category) +{ + return _category == Type::Category::Function; +} + +smt::Expression dev::solidity::minValue(IntegerType const& _type) +{ + return smt::Expression(_type.minValue()); +} + +smt::Expression dev::solidity::maxValue(IntegerType const& _type) +{ + return smt::Expression(_type.maxValue()); +} diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h new file mode 100644 index 00000000..dcdd9ea4 --- /dev/null +++ b/libsolidity/formal/SymbolicTypes.h @@ -0,0 +1,53 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see <http://www.gnu.org/licenses/>. +*/ + +#pragma once + +#include <libsolidity/formal/SolverInterface.h> +#include <libsolidity/formal/SymbolicVariables.h> + +#include <libsolidity/ast/AST.h> +#include <libsolidity/ast/Types.h> + +namespace dev +{ +namespace solidity +{ + +/// So far int, bool and address are supported. +/// Returns true if type is supported. +bool isSupportedType(Type::Category _category); +bool isSupportedType(Type const& _type); + +bool isInteger(Type::Category _category); +bool isRational(Type::Category _category); +bool isFixedBytes(Type::Category _category); +bool isAddress(Type::Category _category); +bool isNumber(Type::Category _category); +bool isBool(Type::Category _category); +bool isFunction(Type::Category _category); + +/// Returns a new symbolic variable, according to _type. +/// Also returns whether the type is abstract or not, +/// which is true for unsupported types. +std::pair<bool, std::shared_ptr<SymbolicVariable>> newSymbolicVariable(Type const& _type, std::string const& _uniqueName, smt::SolverInterface& _solver); + +smt::Expression minValue(IntegerType const& _type); +smt::Expression maxValue(IntegerType const& _type); + +} +} diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp deleted file mode 100644 index caefa3a3..00000000 --- a/libsolidity/formal/SymbolicVariable.cpp +++ /dev/null @@ -1,40 +0,0 @@ -/* - This file is part of solidity. - - solidity is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - solidity is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with solidity. If not, see <http://www.gnu.org/licenses/>. -*/ - -#include <libsolidity/formal/SymbolicVariable.h> - -#include <libsolidity/ast/AST.h> - -using namespace std; -using namespace dev; -using namespace dev::solidity; - -SymbolicVariable::SymbolicVariable( - Declaration const& _decl, - smt::SolverInterface& _interface -): - m_declaration(_decl), - m_interface(_interface) -{ -} - -string SymbolicVariable::uniqueSymbol(int _seq) const -{ - return m_declaration.name() + "_" + to_string(m_declaration.id()) + "_" + to_string(_seq); -} - - diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h deleted file mode 100644 index e29ded26..00000000 --- a/libsolidity/formal/SymbolicVariable.h +++ /dev/null @@ -1,66 +0,0 @@ -/* - This file is part of solidity. - - solidity is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - solidity is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with solidity. If not, see <http://www.gnu.org/licenses/>. -*/ - -#pragma once - -#include <libsolidity/formal/SolverInterface.h> - -#include <libsolidity/ast/AST.h> - -#include <memory> - -namespace dev -{ -namespace solidity -{ - -class Declaration; - -/** - * This class represents the symbolic version of a program variable. - */ -class SymbolicVariable -{ -public: - SymbolicVariable( - Declaration const& _decl, - smt::SolverInterface& _interface - ); - virtual ~SymbolicVariable() = default; - - smt::Expression operator()(int _seq) const - { - return valueAtSequence(_seq); - } - - std::string uniqueSymbol(int _seq) const; - - /// Sets the var to the default value of its type. - virtual void setZeroValue(int _seq) = 0; - /// The unknown value is the full range of valid values, - /// and that's sub-type dependent. - virtual void setUnknownValue(int _seq) = 0; - -protected: - virtual smt::Expression valueAtSequence(int _seq) const = 0; - - Declaration const& m_declaration; - smt::SolverInterface& m_interface; -}; - -} -} diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp new file mode 100644 index 00000000..85818ba0 --- /dev/null +++ b/libsolidity/formal/SymbolicVariables.cpp @@ -0,0 +1,112 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see <http://www.gnu.org/licenses/>. +*/ + +#include <libsolidity/formal/SymbolicVariables.h> + +#include <libsolidity/formal/SymbolicTypes.h> + +#include <libsolidity/ast/AST.h> + +using namespace std; +using namespace dev; +using namespace dev::solidity; + +SymbolicVariable::SymbolicVariable( + TypePointer _type, + string const& _uniqueName, + smt::SolverInterface& _interface +): + m_type(move(_type)), + m_uniqueName(_uniqueName), + m_interface(_interface), + m_ssa(make_shared<SSAVariable>()) +{ +} + +string SymbolicVariable::uniqueSymbol(unsigned _index) const +{ + return m_uniqueName + "_" + to_string(_index); +} + +SymbolicBoolVariable::SymbolicBoolVariable( + TypePointer _type, + string const& _uniqueName, + smt::SolverInterface&_interface +): + SymbolicVariable(move(_type), _uniqueName, _interface) +{ + solAssert(m_type->category() == Type::Category::Bool, ""); +} + +smt::Expression SymbolicBoolVariable::valueAtIndex(int _index) const +{ + return m_interface.newBool(uniqueSymbol(_index)); +} + +void SymbolicBoolVariable::setZeroValue() +{ + m_interface.addAssertion(currentValue() == smt::Expression(false)); +} + +void SymbolicBoolVariable::setUnknownValue() +{ +} + +SymbolicIntVariable::SymbolicIntVariable( + TypePointer _type, + string const& _uniqueName, + smt::SolverInterface& _interface +): + SymbolicVariable(move(_type), _uniqueName, _interface) +{ + solAssert(isNumber(m_type->category()), ""); +} + +smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const +{ + return m_interface.newInteger(uniqueSymbol(_index)); +} + +void SymbolicIntVariable::setZeroValue() +{ + m_interface.addAssertion(currentValue() == 0); +} + +void SymbolicIntVariable::setUnknownValue() +{ + auto intType = dynamic_cast<IntegerType const*>(m_type.get()); + solAssert(intType, ""); + m_interface.addAssertion(currentValue() >= minValue(*intType)); + m_interface.addAssertion(currentValue() <= maxValue(*intType)); +} + +SymbolicAddressVariable::SymbolicAddressVariable( + string const& _uniqueName, + smt::SolverInterface& _interface +): + SymbolicIntVariable(make_shared<IntegerType>(160), _uniqueName, _interface) +{ +} + +SymbolicFixedBytesVariable::SymbolicFixedBytesVariable( + unsigned _numBytes, + string const& _uniqueName, + smt::SolverInterface& _interface +): + SymbolicIntVariable(make_shared<IntegerType>(_numBytes * 8), _uniqueName, _interface) +{ +} diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h new file mode 100644 index 00000000..4fd9b245 --- /dev/null +++ b/libsolidity/formal/SymbolicVariables.h @@ -0,0 +1,149 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see <http://www.gnu.org/licenses/>. +*/ + +#pragma once + +#include <libsolidity/formal/SSAVariable.h> + +#include <libsolidity/formal/SolverInterface.h> + +#include <libsolidity/ast/Types.h> + +#include <memory> + +namespace dev +{ +namespace solidity +{ + +class Type; + +/** + * This abstract class represents the symbolic version of a program variable. + */ +class SymbolicVariable +{ +public: + SymbolicVariable( + TypePointer _type, + std::string const& _uniqueName, + smt::SolverInterface& _interface + ); + + virtual ~SymbolicVariable() = default; + + smt::Expression currentValue() const + { + return valueAtIndex(m_ssa->index()); + } + + virtual smt::Expression valueAtIndex(int _index) const = 0; + + smt::Expression increaseIndex() + { + ++(*m_ssa); + return currentValue(); + } + + unsigned index() const { return m_ssa->index(); } + unsigned& index() { return m_ssa->index(); } + + /// Sets the var to the default value of its type. + /// Inherited types must implement. + virtual void setZeroValue() = 0; + /// The unknown value is the full range of valid values. + /// It is sub-type dependent, but not mandatory. + virtual void setUnknownValue() {} + +protected: + std::string uniqueSymbol(unsigned _index) const; + + TypePointer m_type = nullptr; + std::string m_uniqueName; + smt::SolverInterface& m_interface; + std::shared_ptr<SSAVariable> m_ssa = nullptr; +}; + +/** + * Specialization of SymbolicVariable for Bool + */ +class SymbolicBoolVariable: public SymbolicVariable +{ +public: + SymbolicBoolVariable( + TypePointer _type, + std::string const& _uniqueName, + smt::SolverInterface& _interface + ); + + /// Sets the var to false. + void setZeroValue(); + /// Does nothing since the SMT solver already knows the valid values for Bool. + void setUnknownValue(); + +protected: + smt::Expression valueAtIndex(int _index) const; +}; + +/** + * Specialization of SymbolicVariable for Integers + */ +class SymbolicIntVariable: public SymbolicVariable +{ +public: + SymbolicIntVariable( + TypePointer _type, + std::string const& _uniqueName, + smt::SolverInterface& _interface + ); + + /// Sets the var to 0. + void setZeroValue(); + /// Sets the variable to the full valid value range. + void setUnknownValue(); + +protected: + smt::Expression valueAtIndex(int _index) const; +}; + +/** + * Specialization of SymbolicVariable for Address + */ +class SymbolicAddressVariable: public SymbolicIntVariable +{ +public: + SymbolicAddressVariable( + std::string const& _uniqueName, + smt::SolverInterface& _interface + ); +}; + +/** + * Specialization of SymbolicVariable for FixedBytes + */ +class SymbolicFixedBytesVariable: public SymbolicIntVariable +{ +public: + SymbolicFixedBytesVariable( + unsigned _numBytes, + std::string const& _uniqueName, + smt::SolverInterface& _interface + ); +}; + +} +} diff --git a/libsolidity/formal/VariableUsage.cpp b/libsolidity/formal/VariableUsage.cpp index c2dea844..9282a560 100644 --- a/libsolidity/formal/VariableUsage.cpp +++ b/libsolidity/formal/VariableUsage.cpp @@ -50,12 +50,12 @@ VariableUsage::VariableUsage(ASTNode const& _node) _node.accept(reducer); } -vector<Declaration const*> VariableUsage::touchedVariables(ASTNode const& _node) const +vector<VariableDeclaration const*> VariableUsage::touchedVariables(ASTNode const& _node) const { if (!m_children.count(&_node) && !m_touchedVariable.count(&_node)) return {}; - set<Declaration const*> touched; + set<VariableDeclaration const*> touched; vector<ASTNode const*> toVisit; toVisit.push_back(&_node); diff --git a/libsolidity/formal/VariableUsage.h b/libsolidity/formal/VariableUsage.h index 62561cce..dda13de2 100644 --- a/libsolidity/formal/VariableUsage.h +++ b/libsolidity/formal/VariableUsage.h @@ -27,7 +27,7 @@ namespace solidity { class ASTNode; -class Declaration; +class VariableDeclaration; /** * This class collects information about which local variables of value type @@ -38,11 +38,11 @@ class VariableUsage public: explicit VariableUsage(ASTNode const& _node); - std::vector<Declaration const*> touchedVariables(ASTNode const& _node) const; + std::vector<VariableDeclaration const*> touchedVariables(ASTNode const& _node) const; private: // Variable touched by a specific AST node. - std::map<ASTNode const*, Declaration const*> m_touchedVariable; + std::map<ASTNode const*, VariableDeclaration const*> m_touchedVariable; std::map<ASTNode const*, std::vector<ASTNode const*>> m_children; }; diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp index 41943c92..9a0ccf48 100644 --- a/libsolidity/formal/Z3Interface.cpp +++ b/libsolidity/formal/Z3Interface.cpp @@ -28,7 +28,10 @@ using namespace dev::solidity::smt; Z3Interface::Z3Interface(): m_solver(m_context) { + // This needs to be set globally. z3::set_param("rewriter.pull_cheap_ite", true); + // This needs to be set in the context. + m_context.set("timeout", queryTimeout); } void Z3Interface::reset() @@ -48,22 +51,22 @@ void Z3Interface::pop() m_solver.pop(); } -Expression Z3Interface::newFunction(string _name, Sort _domain, Sort _codomain) +void Z3Interface::declareFunction(string _name, Sort _domain, Sort _codomain) { - m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))}); - return SolverInterface::newFunction(move(_name), _domain, _codomain); + if (!m_functions.count(_name)) + m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))}); } -Expression Z3Interface::newInteger(string _name) +void Z3Interface::declareInteger(string _name) { - m_constants.insert({_name, m_context.int_const(_name.c_str())}); - return SolverInterface::newInteger(move(_name)); + if (!m_constants.count(_name)) + m_constants.insert({_name, m_context.int_const(_name.c_str())}); } -Expression Z3Interface::newBool(string _name) +void Z3Interface::declareBool(string _name) { - m_constants.insert({_name, m_context.bool_const(_name.c_str())}); - return SolverInterface::newBool(std::move(_name)); + if (!m_constants.count(_name)) + m_constants.insert({_name, m_context.bool_const(_name.c_str())}); } void Z3Interface::addAssertion(Expression const& _expr) @@ -88,11 +91,9 @@ pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _ case z3::check_result::unknown: result = CheckResult::UNKNOWN; break; - default: - solAssert(false, ""); } - if (result != CheckResult::UNSATISFIABLE && !_expressionsToEvaluate.empty()) + if (result == CheckResult::SATISFIABLE && !_expressionsToEvaluate.empty()) { z3::model m = m_solver.get_model(); for (Expression const& e: _expressionsToEvaluate) diff --git a/libsolidity/formal/Z3Interface.h b/libsolidity/formal/Z3Interface.h index 354ded25..84880ff3 100644 --- a/libsolidity/formal/Z3Interface.h +++ b/libsolidity/formal/Z3Interface.h @@ -40,9 +40,9 @@ public: void push() override; void pop() override; - Expression newFunction(std::string _name, Sort _domain, Sort _codomain) override; - Expression newInteger(std::string _name) override; - Expression newBool(std::string _name) override; + void declareFunction(std::string _name, Sort _domain, Sort _codomain) override; + void declareInteger(std::string _name) override; + void declareBool(std::string _name) override; void addAssertion(Expression const& _expr) override; std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override; |