diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index d56c45e3c..dd1e5136c 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -441,26 +441,7 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall) } else { - vector funArgs; - Expression const* calledExpr = &_funCall.expression(); - auto const& funType = dynamic_cast(calledExpr->annotation().type); - solAssert(funType, ""); - - auto const& functionParams = funDef->parameters(); - auto const& arguments = _funCall.arguments(); - unsigned firstParam = 0; - if (funType->bound()) - { - auto const& boundFunction = dynamic_cast(calledExpr); - solAssert(boundFunction, ""); - funArgs.push_back(expr(boundFunction->expression(), functionParams.front()->type())); - firstParam = 1; - } - - solAssert((arguments.size() + firstParam) == functionParams.size(), ""); - for (unsigned i = 0; i < arguments.size(); ++i) - funArgs.push_back(expr(*arguments.at(i), functionParams.at(i + firstParam)->type())); - initializeFunctionCallParameters(*funDef, funArgs); + initializeFunctionCallParameters(*funDef, symbolicArguments(_funCall)); // The reason why we need to pushCallStack here instead of visit(FunctionDefinition) // is that there we don't have `_funCall`. @@ -575,7 +556,7 @@ void BMC::checkVerificationTargets(smt::Expression const& _constraints) checkVerificationTarget(target, _constraints); } -void BMC::checkVerificationTarget(VerificationTarget& _target, smt::Expression const& _constraints) +void BMC::checkVerificationTarget(BMCVerificationTarget& _target, smt::Expression const& _constraints) { switch (_target.type) { @@ -606,7 +587,7 @@ void BMC::checkVerificationTarget(VerificationTarget& _target, smt::Expression c } } -void BMC::checkConstantCondition(VerificationTarget& _target) +void BMC::checkConstantCondition(BMCVerificationTarget& _target) { checkBooleanNotConstant( *_target.expression, @@ -617,7 +598,7 @@ void BMC::checkConstantCondition(VerificationTarget& _target) ); } -void BMC::checkUnderflow(VerificationTarget& _target, smt::Expression const& _constraints) +void BMC::checkUnderflow(BMCVerificationTarget& _target, smt::Expression const& _constraints) { solAssert( _target.type == VerificationTarget::Type::Underflow || @@ -637,7 +618,7 @@ void BMC::checkUnderflow(VerificationTarget& _target, smt::Expression const& _co ); } -void BMC::checkOverflow(VerificationTarget& _target, smt::Expression const& _constraints) +void BMC::checkOverflow(BMCVerificationTarget& _target, smt::Expression const& _constraints) { solAssert( _target.type == VerificationTarget::Type::Overflow || @@ -657,7 +638,7 @@ void BMC::checkOverflow(VerificationTarget& _target, smt::Expression const& _con ); } -void BMC::checkDivByZero(VerificationTarget& _target) +void BMC::checkDivByZero(BMCVerificationTarget& _target) { solAssert(_target.type == VerificationTarget::Type::DivByZero, ""); checkCondition( @@ -671,7 +652,7 @@ void BMC::checkDivByZero(VerificationTarget& _target) ); } -void BMC::checkBalance(VerificationTarget& _target) +void BMC::checkBalance(BMCVerificationTarget& _target) { solAssert(_target.type == VerificationTarget::Type::Balance, ""); checkCondition( @@ -684,7 +665,7 @@ void BMC::checkBalance(VerificationTarget& _target) ); } -void BMC::checkAssert(VerificationTarget& _target) +void BMC::checkAssert(BMCVerificationTarget& _target) { solAssert(_target.type == VerificationTarget::Type::Assert, ""); if (!m_safeAssertions.count(_target.expression)) @@ -703,10 +684,12 @@ void BMC::addVerificationTarget( Expression const* _expression ) { - VerificationTarget target{ - _type, - _value, - currentPathConditions() && m_context.assertions(), + BMCVerificationTarget target{ + { + _type, + _value, + currentPathConditions() && m_context.assertions() + }, _expression, m_callStack, modelExpressions() diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h index 387e84d4a..f4b427ede 100644 --- a/libsolidity/formal/BMC.h +++ b/libsolidity/formal/BMC.h @@ -117,24 +117,21 @@ private: /// Verification targets. //@{ - struct VerificationTarget + struct BMCVerificationTarget: VerificationTarget { - enum class Type { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert } type; - smt::Expression value; - smt::Expression constraints; Expression const* expression; std::vector callStack; std::pair, std::vector> modelExpressions; }; void checkVerificationTargets(smt::Expression const& _constraints); - void checkVerificationTarget(VerificationTarget& _target, smt::Expression const& _constraints = smt::Expression(true)); - void checkConstantCondition(VerificationTarget& _target); - void checkUnderflow(VerificationTarget& _target, smt::Expression const& _constraints); - void checkOverflow(VerificationTarget& _target, smt::Expression const& _constraints); - void checkDivByZero(VerificationTarget& _target); - void checkBalance(VerificationTarget& _target); - void checkAssert(VerificationTarget& _target); + void checkVerificationTarget(BMCVerificationTarget& _target, smt::Expression const& _constraints = smt::Expression(true)); + void checkConstantCondition(BMCVerificationTarget& _target); + void checkUnderflow(BMCVerificationTarget& _target, smt::Expression const& _constraints); + void checkOverflow(BMCVerificationTarget& _target, smt::Expression const& _constraints); + void checkDivByZero(BMCVerificationTarget& _target); + void checkBalance(BMCVerificationTarget& _target); + void checkAssert(BMCVerificationTarget& _target); void addVerificationTarget( VerificationTarget::Type _type, smt::Expression const& _value, @@ -179,7 +176,7 @@ private: /// ErrorReporter that comes from CompilerStack. langutil::ErrorReporter& m_outerErrorReporter; - std::vector m_verificationTargets; + std::vector m_verificationTargets; /// Assertions that are known to be safe. std::set m_safeAssertions; diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index cfe3efb8b..25201474b 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -505,6 +505,23 @@ void CHC::eraseKnowledge() m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.hasReferenceOrMappingType(); }); } +void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function) +{ + SMTEncoder::clearIndices(_contract, _function); + for (auto const* var: m_stateVariables) + /// SSA index 0 is reserved for state variables at the beginning + /// of the current transaction. + m_context.variable(*var)->increaseIndex(); + if (_function) + { + for (auto const& var: _function->parameters() + _function->returnParameters()) + m_context.variable(*var)->increaseIndex(); + for (auto const& var: _function->localVariables()) + m_context.variable(*var)->increaseIndex(); + } +} + + bool CHC::shouldVisit(ContractDefinition const& _contract) const { if ( diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index a732d2ff2..6f912fbd8 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -83,6 +83,7 @@ private: //@{ void reset(); void eraseKnowledge(); + void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override; bool shouldVisit(ContractDefinition const& _contract) const; bool shouldVisit(FunctionDefinition const& _function) const; void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector const* _arguments = nullptr); diff --git a/libsolidity/formal/ModelChecker.h b/libsolidity/formal/ModelChecker.h index f22ca59b8..ac19ba270 100644 --- a/libsolidity/formal/ModelChecker.h +++ b/libsolidity/formal/ModelChecker.h @@ -46,7 +46,7 @@ public: /// should be used, even if all are available. The default choice is to use all. ModelChecker( langutil::ErrorReporter& _errorReporter, - std::map const& _smtlib2Responses, + std::map const& _smtlib2Responses, ReadCallback::Callback const& _smtCallback = ReadCallback::Callback(), smt::SMTSolverChoice _enabledSolvers = smt::SMTSolverChoice::All() ); diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 2c86eae0b..ac81a5d87 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -1682,3 +1682,31 @@ void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall) else if (returnParams.size() == 1) defineExpr(_funCall, currentValue(*returnParams.front())); } + +vector SMTEncoder::symbolicArguments(FunctionCall const& _funCall) +{ + auto const* function = functionCallToDefinition(_funCall); + solAssert(function, ""); + + vector args; + Expression const* calledExpr = &_funCall.expression(); + auto const& funType = dynamic_cast(calledExpr->annotation().type); + solAssert(funType, ""); + + auto const& functionParams = function->parameters(); + auto const& arguments = _funCall.arguments(); + unsigned firstParam = 0; + if (funType->bound()) + { + auto const& boundFunction = dynamic_cast(calledExpr); + solAssert(boundFunction, ""); + args.push_back(expr(boundFunction->expression(), functionParams.front()->type())); + firstParam = 1; + } + + solAssert((arguments.size() + firstParam) == functionParams.size(), ""); + for (unsigned i = 0; i < arguments.size(); ++i) + args.push_back(expr(*arguments.at(i), functionParams.at(i + firstParam)->type())); + + return args; +} diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index eddab0eb1..21bf094c0 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -217,7 +217,7 @@ protected: /// Resets the variable indices. void resetVariableIndices(VariableIndices const& _indices); /// Used when starting a new block. - void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr); + virtual void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr); /// @returns variables that are touched in _node's subtree. @@ -230,9 +230,21 @@ protected: /// and set them as the components of the symbolic tuple. void createReturnedExpressions(FunctionCall const& _funCall); + /// @returns the symbolic arguments for a function call, + /// taking into account bound functions and + /// type conversion. + std::vector symbolicArguments(FunctionCall const& _funCall); + /// @returns a note to be added to warnings. std::string extraComment(); + struct VerificationTarget + { + enum class Type { ConstantCondition, Underflow, Overflow, UnderOverflow, DivByZero, Balance, Assert } type; + smt::Expression value; + smt::Expression constraints; + }; + smt::VariableUsage m_variableUsage; bool m_arrayAssignmentHappened = false; // True if the "No SMT solver available" warning was already created.