From e1c238e25f65f071539118a1aff94f2444debdc7 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 20 Aug 2019 15:03:45 +0200 Subject: [PATCH] [SMTChecker] Add loop support --- Changelog.md | 1 + libsolidity/formal/CHC.cpp | 361 ++++++++++++------ libsolidity/formal/CHC.h | 59 ++- libsolidity/formal/SMTEncoder.cpp | 11 +- libsolidity/formal/SMTEncoder.h | 2 + libsolidity/formal/SymbolicTypes.cpp | 1 - libsolidity/formal/Z3CHCInterface.cpp | 3 +- .../smtCheckerTests/invariants/loop_array.sol | 19 + .../invariants/loop_array_for.sol | 16 + .../smtCheckerTests/invariants/loop_basic.sol | 11 + .../invariants/loop_basic_for.sol | 10 + .../invariants/loop_nested.sol | 17 + .../invariants/loop_nested_for.sol | 14 + .../loops/do_while_1_false_positives.sol | 1 - .../loops/for_1_false_positive.sol | 6 +- .../smtCheckerTests/loops/for_loop_6.sol | 1 - ...r_loop_array_assignment_storage_memory.sol | 1 - ..._loop_array_assignment_storage_storage.sol | 1 - .../loops/for_loop_trivial_condition_3.sol | 1 - .../smtCheckerTests/loops/while_1.sol | 1 - .../smtCheckerTests/loops/while_1_break.sol | 21 + .../loops/while_1_break_fail.sol | 19 + .../loops/while_1_continue.sol | 22 ++ .../loops/while_1_continue_fail.sol | 21 + .../loops/while_1_infinite.sol | 21 + .../smtCheckerTests/loops/while_2.sol | 13 + .../smtCheckerTests/loops/while_2_break.sol | 19 + .../loops/while_2_break_fail.sol | 16 + .../smtCheckerTests/loops/while_2_fail.sol | 1 - ...e_loop_array_assignment_memory_storage.sol | 6 +- ...e_loop_array_assignment_storage_memory.sol | 1 - ..._loop_array_assignment_storage_storage.sol | 1 - .../loops/while_loop_simple_4.sol | 1 - .../smtCheckerTestsJSON/multi.json | 1 - 34 files changed, 539 insertions(+), 161 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/invariants/loop_array.sol create mode 100644 test/libsolidity/smtCheckerTests/invariants/loop_array_for.sol create mode 100644 test/libsolidity/smtCheckerTests/invariants/loop_basic.sol create mode 100644 test/libsolidity/smtCheckerTests/invariants/loop_basic_for.sol create mode 100644 test/libsolidity/smtCheckerTests/invariants/loop_nested.sol create mode 100644 test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_1_break.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_1_break_fail.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_1_continue.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_1_continue_fail.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_1_infinite.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_2.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_2_break.sol create mode 100644 test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol diff --git a/Changelog.md b/Changelog.md index 6b92a54f2..c5653bf42 100644 --- a/Changelog.md +++ b/Changelog.md @@ -7,6 +7,7 @@ Language Features: Compiler Features: * ABI Output: Change sorting order of functions from selector to kind, name. * Optimizer: Add rule that replaces the BYTE opcode by 0 if the first argument is larger than 31. + * SMTChecker: Add loop support to the CHC engine. * Yul Optimizer: Take side-effect-freeness of user-defined functions into account. * Yul Optimizer: Remove redundant mload/sload operations. diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index a65dd61f1..867be77dd 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -74,8 +74,10 @@ bool CHC::visit(ContractDefinition const& _contract) else m_stateSorts.push_back(smt::smtSort(*var->type())); + clearIndices(); + string interfaceName = "interface_" + _contract.name() + "_" + to_string(_contract.id()); - m_interfacePredicate = createBlock(interfaceSort(), interfaceName); + m_interfacePredicate = createSymbolicBlock(interfaceSort(), interfaceName); // TODO create static instances for Bool/Int sorts in SolverInterface. auto boolSort = make_shared(smt::Kind::Bool); @@ -83,7 +85,7 @@ bool CHC::visit(ContractDefinition const& _contract) vector(), boolSort ); - m_errorPredicate = createBlock(errorFunctionSort, "error"); + m_errorPredicate = createSymbolicBlock(errorFunctionSort, "error"); // If the contract has a constructor it is handled as a function. // Otherwise we zero-initialize all state vars. @@ -91,7 +93,9 @@ bool CHC::visit(ContractDefinition const& _contract) if (!_contract.constructor()) { string constructorName = "constructor_" + _contract.name() + "_" + to_string(_contract.id()); - m_constructorPredicate = createBlock(constructorSort(), constructorName); + m_constructorPredicate = createSymbolicBlock(constructorSort(), constructorName); + smt::Expression constructorPred = (*m_constructorPredicate)({}); + addRule(constructorPred, constructorName); for (auto const& var: m_stateVariables) { @@ -101,14 +105,7 @@ bool CHC::visit(ContractDefinition const& _contract) m_context.setZeroValue(*symbVar); } - smt::Expression constructorAppl = (*m_constructorPredicate)({}); - m_interface->addRule(constructorAppl, constructorName); - - smt::Expression constructorInterface = smt::Expression::implies( - constructorAppl && m_context.assertions(), - interface() - ); - m_interface->addRule(constructorInterface, constructorName + "_to_" + interfaceName); + connectBlocks(constructorPred, interface()); } return true; @@ -119,10 +116,13 @@ void CHC::endVisit(ContractDefinition const& _contract) if (!shouldVisit(_contract)) return; - auto errorAppl = (*m_errorPredicate)({}); - for (auto const& target: m_verificationTargets) + for (unsigned i = 0; i < m_verificationTargets.size(); ++i) + { + auto const& target = m_verificationTargets.at(i); + auto errorAppl = error(i + 1); if (query(errorAppl, target->location())) m_safeAssertions.insert(target); + } SMTEncoder::endVisit(_contract); } @@ -139,39 +139,25 @@ bool CHC::visit(FunctionDefinition const& _function) // Store the constraints related to variable initialization. smt::Expression const& initAssertions = m_context.assertions(); - - createFunctionBlock(*m_currentFunction); - - // Rule Interface -> FunctionEntry, uses no constraints. - smt::Expression interfaceFunction = smt::Expression::implies( - interface(), - predicateCurrent(m_currentFunction) - ); - m_interface->addRule( - interfaceFunction, - m_interfacePredicate->currentName() + "_to_" + m_predicates.at(m_currentFunction)->currentName() - ); - - pushBlock(predicateCurrent(m_currentFunction)); - - createFunctionBlock(m_currentFunction->body()); - - // Rule FunctionEntry -> FunctionBody, also no constraints. - smt::Expression functionBody = smt::Expression::implies( - predicateEntry(m_currentFunction), - predicateBodyCurrent(&m_currentFunction->body()) - ); - m_interface->addRule( - functionBody, - m_predicates.at(m_currentFunction)->currentName() + "_to_" + m_predicates.at(&m_currentFunction->body())->currentName() - ); - - pushBlock(predicateBodyCurrent(&m_currentFunction->body())); - // We need to re-add the constraints that were created for initialization of variables. - m_context.addAssertion(initAssertions); + m_context.pushSolver(); solAssert(m_functionBlocks == 0, ""); - m_functionBlocks = 2; + + createBlock(m_currentFunction); + createBlock(&m_currentFunction->body(), "block_"); + + auto functionPred = predicate(m_currentFunction); + auto bodyPred = predicate(&m_currentFunction->body()); + + connectBlocks(interface(), functionPred); + connectBlocks(functionPred, bodyPred); + + m_context.popSolver(); + + pushBlock(&m_currentFunction->body()); + + // We need to re-add the constraints that were created for initialization of variables. + m_context.addAssertion(initAssertions); SMTEncoder::visit(*m_currentFunction); @@ -185,35 +171,22 @@ void CHC::endVisit(FunctionDefinition const& _function) solAssert(m_currentFunction == &_function, "Inlining internal function calls not yet implemented"); - // Create Function Exit block. - createFunctionBlock(*m_currentFunction); - - // Rule FunctionBody -> FunctionExit. - smt::Expression bodyFunction = smt::Expression::implies( - predicateEntry(&_function.body()) && m_context.assertions(), - predicateCurrent(&_function) - ); - m_interface->addRule( - bodyFunction, - m_predicates.at(&_function.body())->currentName() + "_to_" + m_predicates.at(&_function.body())->currentName() - ); + // Function Exit block. + createBlock(m_currentFunction); + connectBlocks(m_path.back(), predicate(&_function)); // Rule FunctionExit -> Interface, uses no constraints. - smt::Expression functionInterface = smt::Expression::implies( - predicateCurrent(&_function), - interface() - ); - m_interface->addRule( - functionInterface, - m_predicates.at(&_function)->currentName() + "_to_" + m_interfacePredicate->currentName() - ); + clearIndices(); + m_context.pushSolver(); + connectBlocks(predicate(&_function), interface()); + m_context.popSolver(); m_currentFunction = nullptr; solAssert(m_path.size() == m_functionBlocks, ""); - for (unsigned i = 0; i < m_path.size(); ++i) - m_context.popSolver(); - m_functionBlocks = 0; - m_path.clear(); + while (m_functionBlocks > 0) + popBlock(); + + solAssert(m_path.empty(), ""); SMTEncoder::endVisit(_function); } @@ -237,15 +210,51 @@ bool CHC::visit(IfStatement const& _if) bool CHC::visit(WhileStatement const& _while) { - eraseKnowledge(); - m_context.resetVariables(touchedVariables(_while)); + bool unknownFunctionCallWasSeen = m_unknownFunctionCallSeen; + m_unknownFunctionCallSeen = false; + + solAssert(m_currentFunction, ""); + + if (_while.isDoWhile()) + _while.body().accept(*this); + + visitLoop( + _while, + &_while.condition(), + _while.body(), + nullptr + ); + + if (m_unknownFunctionCallSeen) + eraseKnowledge(); + + m_unknownFunctionCallSeen = unknownFunctionCallWasSeen; + return false; } bool CHC::visit(ForStatement const& _for) { - eraseKnowledge(); - m_context.resetVariables(touchedVariables(_for)); + bool unknownFunctionCallWasSeen = m_unknownFunctionCallSeen; + m_unknownFunctionCallSeen = false; + + solAssert(m_currentFunction, ""); + + if (auto init = _for.initializationExpression()) + init->accept(*this); + + visitLoop( + _for, + _for.condition(), + _for.body(), + _for.loopExpression() + ); + + if (m_unknownFunctionCallSeen) + eraseKnowledge(); + + m_unknownFunctionCallSeen = unknownFunctionCallWasSeen; + return false; } @@ -292,6 +301,18 @@ void CHC::endVisit(FunctionCall const& _funCall) createReturnedExpressions(_funCall); } +void CHC::endVisit(Break const&) +{ + solAssert(m_breakDest, ""); + m_breakSeen = true; +} + +void CHC::endVisit(Continue const&) +{ + solAssert(m_continueDest, ""); + m_continueSeen = true; +} + void CHC::visitAssert(FunctionCall const& _funCall) { auto const& args = _funCall.arguments(); @@ -300,13 +321,10 @@ void CHC::visitAssert(FunctionCall const& _funCall) solAssert(!m_path.empty(), ""); + createErrorBlock(); + smt::Expression assertNeg = !(m_context.expression(*args.front())->currentValue()); - smt::Expression assertionError = smt::Expression::implies( - m_path.back() && m_context.assertions() && currentPathConditions() && assertNeg, - error() - ); - string predicateName = "assert_" + to_string(_funCall.id()); - m_interface->addRule(assertionError, predicateName + "_to_error"); + connectBlocks(m_path.back(), error(), currentPathConditions() && assertNeg); m_verificationTargets.push_back(&_funCall); } @@ -323,6 +341,85 @@ void CHC::unknownFunctionCall(FunctionCall const&) m_unknownFunctionCallSeen = true; } +void CHC::visitLoop( + BreakableStatement const& _loop, + Expression const* _condition, + Statement const& _body, + ASTNode const* _postLoop +) +{ + bool breakWasSeen = m_breakSeen; + bool continueWasSeen = m_continueSeen; + m_breakSeen = false; + m_continueSeen = false; + + solAssert(m_currentFunction, ""); + auto const& functionBody = m_currentFunction->body(); + + createBlock(&_loop, "loop_header_"); + createBlock(&_body, "loop_body_"); + createBlock(&functionBody, "block_"); + + connectBlocks(m_path.back(), predicate(&_loop)); + + // We need to save the next block here because new blocks + // might be created inside the loop body. + // This will be m_path.back() in the end of this function. + pushBlock(&functionBody); + + smt::Expression loopHeader = predicate(&_loop); + pushBlock(&_loop); + + if (_condition) + _condition->accept(*this); + auto condition = _condition ? expr(*_condition) : smt::Expression(true); + + connectBlocks(loopHeader, predicate(&_body), condition); + connectBlocks(loopHeader, predicate(&functionBody), !condition); + + // Loop body visit. + pushBlock(&_body); + + m_breakDest = &functionBody; + m_continueDest = _postLoop ? _postLoop : &_loop; + + auto functionBlocks = m_functionBlocks; + _body.accept(*this); + if (_postLoop) + { + createBlock(_postLoop, "loop_post_"); + connectBlocks(m_path.back(), predicate(_postLoop)); + pushBlock(_postLoop); + _postLoop->accept(*this); + } + + // Back edge. + connectBlocks(m_path.back(), predicate(&_loop)); + + // Pop all function blocks created by nested inner loops + // to adjust the assertion context. + for (unsigned i = m_functionBlocks; i > functionBlocks; --i) + popBlock(); + m_functionBlocks = functionBlocks; + + // Loop body + popBlock(); + // Loop header + popBlock(); + + // New function block starts with indices = 0 + clearIndices(); + + if (m_breakSeen || m_continueSeen) + { + eraseKnowledge(); + m_context.resetVariables([](VariableDeclaration const&) { return true; }); + } + + m_breakSeen = breakWasSeen; + m_continueSeen = continueWasSeen; +} + void CHC::reset() { m_stateSorts.clear(); @@ -330,6 +427,8 @@ void CHC::reset() m_verificationTargets.clear(); m_safeAssertions.clear(); m_unknownFunctionCallSeen = false; + m_breakSeen = false; + m_continueSeen = false; } void CHC::eraseKnowledge() @@ -352,22 +451,26 @@ bool CHC::shouldVisit(FunctionDefinition const& _function) const { if ( _function.isPublic() && - _function.isImplemented() + _function.isImplemented() && + !_function.isConstructor() ) return true; return false; } -void CHC::pushBlock(smt::Expression const& _block) +void CHC::pushBlock(ASTNode const* _node) { + clearIndices(); m_context.pushSolver(); - m_path.push_back(_block); + m_path.push_back(predicate(_node)); + ++m_functionBlocks; } void CHC::popBlock() { m_context.popSolver(); m_path.pop_back(); + --m_functionBlocks; } smt::SortPointer CHC::constructorSort() @@ -404,12 +507,13 @@ smt::SortPointer CHC::sort(FunctionDefinition const& _function) return m_nodeSorts[&_function] = move(sort); } -smt::SortPointer CHC::sort(Block const& _block) +smt::SortPointer CHC::sort(ASTNode const* _node) { - if (m_nodeSorts.count(&_block)) - return m_nodeSorts.at(&_block); + if (m_nodeSorts.count(_node)) + return m_nodeSorts.at(_node); - solAssert(_block.scope() == m_currentFunction, ""); + if (auto funDef = dynamic_cast(_node)) + return sort(*funDef); auto fSort = dynamic_pointer_cast(sort(*m_currentFunction)); solAssert(fSort, ""); @@ -422,10 +526,10 @@ smt::SortPointer CHC::sort(Block const& _block) fSort->domain + varSorts, boolSort ); - return m_nodeSorts[&_block] = move(functionBodySort); + return m_nodeSorts[_node] = move(functionBodySort); } -unique_ptr CHC::createBlock(smt::SortPointer _sort, string const& _name) +unique_ptr CHC::createSymbolicBlock(smt::SortPointer _sort, string const& _name) { auto block = make_unique( _sort, @@ -462,33 +566,36 @@ smt::Expression CHC::error() return (*m_errorPredicate)({}); } -void CHC::createFunctionBlock(FunctionDefinition const& _function) +smt::Expression CHC::error(unsigned _idx) { - if (m_predicates.count(&_function)) - { - m_predicates.at(&_function)->increaseIndex(); - m_interface->registerRelation(m_predicates.at(&_function)->currentValue()); - } - else - m_predicates[&_function] = createBlock( - sort(_function), - predicateName(_function) - ); + return m_errorPredicate->valueAtIndex(_idx)({}); } -void CHC::createFunctionBlock(Block const& _block) +void CHC::createBlock(ASTNode const* _node, string const& _prefix) { - solAssert(_block.scope() == m_currentFunction, ""); - if (m_predicates.count(&_block)) + if (m_predicates.count(_node)) { - m_predicates.at(&_block)->increaseIndex(); - m_interface->registerRelation(m_predicates.at(&_block)->currentValue()); + m_predicates.at(_node)->increaseIndex(); + m_interface->registerRelation(m_predicates.at(_node)->currentValue()); } else - m_predicates[&_block] = createBlock( - sort(_block), - predicateName(*m_currentFunction) + "_body" - ); + m_predicates[_node] = createSymbolicBlock(sort(_node), _prefix + predicateName(_node)); +} + +void CHC::createErrorBlock() +{ + solAssert(m_errorPredicate, ""); + m_errorPredicate->increaseIndex(); + m_interface->registerRelation(m_errorPredicate->currentValue()); +} + +void CHC::connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints) +{ + smt::Expression edge = smt::Expression::implies( + _from && m_context.assertions() && _constraints, + _to + ); + addRule(edge, _from.name + "_to_" + _to.name); } vector CHC::currentFunctionVariables() @@ -511,30 +618,44 @@ vector CHC::currentBlockVariables() return currentFunctionVariables() + paramExprs; } -string CHC::predicateName(FunctionDefinition const& _function) +void CHC::clearIndices() { - string functionName = _function.isConstructor() ? - "constructor" : - _function.isFallback() ? - "fallback" : - "function_" + _function.name(); - return functionName + "_" + to_string(_function.id()); + for (auto const& var: m_stateVariables) + m_context.variable(*var)->resetIndex(); + if (m_currentFunction) + { + for (auto const& var: m_currentFunction->parameters() + m_currentFunction->returnParameters()) + m_context.variable(*var)->resetIndex(); + for (auto const& var: m_currentFunction->localVariables()) + m_context.variable(*var)->resetIndex(); + } } -smt::Expression CHC::predicateCurrent(ASTNode const* _node) +string CHC::predicateName(ASTNode const* _node) { - return (*m_predicates.at(_node))(currentFunctionVariables()); + string prefix; + if (auto funDef = dynamic_cast(_node)) + { + prefix = funDef->isConstructor() ? + "constructor" : + funDef->isFallback() ? + "fallback" : + "function_" + funDef->name(); + prefix += "_"; + } + return prefix + to_string(_node->id()); } -smt::Expression CHC::predicateBodyCurrent(ASTNode const* _node) +smt::Expression CHC::predicate(ASTNode const* _node) { + if (dynamic_cast(_node)) + return (*m_predicates.at(_node))(currentFunctionVariables()); return (*m_predicates.at(_node))(currentBlockVariables()); } -smt::Expression CHC::predicateEntry(ASTNode const* _node) +void CHC::addRule(smt::Expression const& _rule, string const& _ruleName) { - solAssert(!m_path.empty(), ""); - return (*m_predicates.at(_node))(m_path.back().arguments); + m_interface->addRule(_rule, _ruleName); } bool CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _location) diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index a31b3aab1..5b40b4c8e 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -61,9 +61,17 @@ private: bool visit(WhileStatement const&) override; bool visit(ForStatement const&) override; void endVisit(FunctionCall const& _node) override; + void endVisit(Break const& _node) override; + void endVisit(Continue const& _node) override; void visitAssert(FunctionCall const& _funCall); void unknownFunctionCall(FunctionCall const& _funCall); + void visitLoop( + BreakableStatement const& _loop, + Expression const* _condition, + Statement const& _body, + ASTNode const* _postLoop + ); //@} /// Helpers. @@ -72,7 +80,7 @@ private: void eraseKnowledge(); bool shouldVisit(ContractDefinition const& _contract) const; bool shouldVisit(FunctionDefinition const& _function) const; - void pushBlock(smt::Expression const& _block); + void pushBlock(ASTNode const* _node); void popBlock(); //@} @@ -81,13 +89,13 @@ private: smt::SortPointer constructorSort(); smt::SortPointer interfaceSort(); smt::SortPointer sort(FunctionDefinition const& _function); - smt::SortPointer sort(Block const& _block); + smt::SortPointer sort(ASTNode const* _block); //@} /// Predicate helpers. //@{ /// @returns a new block of given _sort and _name. - std::unique_ptr createBlock(smt::SortPointer _sort, std::string const& _name); + std::unique_ptr createSymbolicBlock(smt::SortPointer _sort, std::string const& _name); /// Constructor predicate over current variables. smt::Expression constructor(); @@ -95,16 +103,17 @@ private: smt::Expression interface(); /// Error predicate over current variables. smt::Expression error(); + smt::Expression error(unsigned _idx); - /// Creates a block for the given _function or increases its SSA index + /// Creates a block for the given _node or increases its SSA index /// if the block already exists which in practice creates a new function. - /// The predicate parameters are _function input and output parameters. - void createFunctionBlock(FunctionDefinition const& _function); - /// Creates a block for the given _function or increases its SSA index - /// if the block already exists which in practice creates a new function. - /// The predicate parameters are m_currentFunction input, output - /// and local variables. - void createFunctionBlock(Block const& _block); + void createBlock(ASTNode const* _node, std::string const& _prefix = ""); + + /// Creates a new error block to be used by an assertion. + /// Also registers the predicate. + void createErrorBlock(); + + void connectBlocks(smt::Expression const& _from, smt::Expression const& _to, smt::Expression const& _constraints = smt::Expression(true)); /// @returns the current symbolic values of the current function's /// input and output parameters. @@ -113,19 +122,20 @@ private: /// local variables. std::vector currentBlockVariables(); - /// @returns the predicate name for a given function. - std::string predicateName(FunctionDefinition const& _function); - /// @returns a predicate application over the current function's parameters. - smt::Expression predicateCurrent(ASTNode const* _node); - /// @returns a predicate application over the current function's parameters plus local variables. - smt::Expression predicateBodyCurrent(ASTNode const* _node); - /// Predicate for block _node over the variables at the latest - /// block entry. - smt::Expression predicateEntry(ASTNode const* _node); + /// Sets the SSA indices of the variables in scope to 0. + /// Used when starting a new block. + void clearIndices(); + + /// @returns the predicate name for a given node. + std::string predicateName(ASTNode const* _node); + /// @returns a predicate application over the current scoped variables. + smt::Expression predicate(ASTNode const* _node); //@} /// Solver related. //@{ + /// Adds Horn rule to the solver. + void addRule(smt::Expression const& _rule, std::string const& _ruleName); /// @returns true if query is unsatisfiable (safe). bool query(smt::Expression const& _query, langutil::SourceLocation const& _location); //@} @@ -179,6 +189,15 @@ private: std::vector m_path; /// Whether a function call was seen in the current scope. bool m_unknownFunctionCallSeen = false; + /// Whether a break statement was seen in the current scope. + bool m_breakSeen = false; + /// Whether a continue statement was seen in the current scope. + bool m_continueSeen = false; + + /// Block where a loop break should go to. + ASTNode const* m_breakDest; + /// Block where a loop continue should go to. + ASTNode const* m_continueDest; //@} /// CHC solver. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 421bfb3b6..321db653b 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -953,18 +953,21 @@ pair SMTEncoder::arithmeticOperation( smt::Expression intValueRange = (0 - smt::minValue(intType)) + smt::maxValue(intType) + 1; auto value = smt::Expression::ite( - valueNoMod > smt::maxValue(intType) || valueNoMod < smt::minValue(intType), + valueNoMod > smt::maxValue(intType), valueNoMod % intValueRange, - valueNoMod + smt::Expression::ite( + valueNoMod < smt::minValue(intType), + valueNoMod % intValueRange, + valueNoMod + ) ); + if (intType.isSigned()) - { value = smt::Expression::ite( value > smt::maxValue(intType), value - intValueRange, value ); - } return {value, valueNoMod}; } diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 6ccbe9bcc..04984d090 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -87,6 +87,8 @@ protected: bool visit(MemberAccess const& _node) override; void endVisit(IndexAccess const& _node) override; bool visit(InlineAssembly const& _node) override; + void endVisit(Break const&) override {} + void endVisit(Continue const&) override {} /// Do not visit subtree if node is a RationalNumber. /// Symbolic _expr is the rational literal. diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp index c6f964b0a..ab23b8712 100644 --- a/libsolidity/formal/SymbolicTypes.cpp +++ b/libsolidity/formal/SymbolicTypes.cpp @@ -295,7 +295,6 @@ Expression zeroValue(solidity::TypePointer const& _type) auto mappingType = dynamic_cast(_type); solAssert(mappingType, ""); return Expression::const_array(Expression(mappingType), zeroValue(mappingType->valueType())); - } solAssert(false, ""); } diff --git a/libsolidity/formal/Z3CHCInterface.cpp b/libsolidity/formal/Z3CHCInterface.cpp index 909a34b02..100a1fb7d 100644 --- a/libsolidity/formal/Z3CHCInterface.cpp +++ b/libsolidity/formal/Z3CHCInterface.cpp @@ -41,6 +41,7 @@ Z3CHCInterface::Z3CHCInterface(): // These are useful for solving problems with arrays and loops. // Use quantified lemma generalizer. p.set("fp.spacer.q3.use_qgen", true); + p.set("fp.spacer.mbqi", false); // Ground pobs by using values from a model. p.set("fp.spacer.ground_pobs", false); m_solver.set(p); @@ -100,7 +101,7 @@ pair> Z3CHCInterface::query(Expression const& _expr) } // TODO retrieve model / invariants } - catch (z3::exception const& _e) + catch (z3::exception const&) { result = CheckResult::ERROR; values.clear(); diff --git a/test/libsolidity/smtCheckerTests/invariants/loop_array.sol b/test/libsolidity/smtCheckerTests/invariants/loop_array.sol new file mode 100644 index 000000000..0f6937d36 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/invariants/loop_array.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; + +contract Simple { + uint[] a; + function f(uint n) public { + uint i; + while (i < n) + { + a[i] = i; + ++i; + } + require(n > 1); + // Assertion is safe but current solver version cannot solve it. + // Keep test for next solver release. + assert(a[n-1] > a[n-2]); + } +} +// ---- +// Warning: (273-296): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/invariants/loop_array_for.sol b/test/libsolidity/smtCheckerTests/invariants/loop_array_for.sol new file mode 100644 index 000000000..1bd8c7517 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/invariants/loop_array_for.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract Simple { + uint[] a; + function f(uint n) public { + uint i; + for (i = 0; i < n; ++i) + a[i] = i; + require(n > 1); + // Assertion is safe but current solver version cannot solve it. + // Keep test for next solver release. + assert(a[n-1] > a[n-2]); + } +} +// ---- +// Warning: (267-290): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/invariants/loop_basic.sol b/test/libsolidity/smtCheckerTests/invariants/loop_basic.sol new file mode 100644 index 000000000..9bfdaf643 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/invariants/loop_basic.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; + +contract Simple { + function f(uint x) public pure { + uint y; + require(x > 0); + while (y < x) + ++y; + assert(y == x); + } +} diff --git a/test/libsolidity/smtCheckerTests/invariants/loop_basic_for.sol b/test/libsolidity/smtCheckerTests/invariants/loop_basic_for.sol new file mode 100644 index 000000000..55019cf0c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/invariants/loop_basic_for.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract Simple { + function f(uint x) public pure { + uint y; + for (y = 0; y < x; ++y) {} + assert(y == x); + } +} +// ---- diff --git a/test/libsolidity/smtCheckerTests/invariants/loop_nested.sol b/test/libsolidity/smtCheckerTests/invariants/loop_nested.sol new file mode 100644 index 000000000..b17140a0d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/invariants/loop_nested.sol @@ -0,0 +1,17 @@ +pragma experimental SMTChecker; + +contract Simple { + function f() public pure { + uint x = 10; + uint y; + while (y < x) + { + ++y; + x = 0; + while (x < 10) + ++x; + assert(x == 10); + } + assert(y == x); + } +} diff --git a/test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol b/test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol new file mode 100644 index 000000000..ac7f0f7d1 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/invariants/loop_nested_for.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract Simple { + function f() public pure { + uint x; + uint y; + for (x = 10; y < x; ++y) + { + for (x = 0; x < 10; ++x) {} + assert(x == 10); + } + assert(y == x); + } +} diff --git a/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol b/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol index 4690af4e6..c5f5cf44d 100644 --- a/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol +++ b/test/libsolidity/smtCheckerTests/loops/do_while_1_false_positives.sol @@ -15,4 +15,3 @@ contract C } // ---- // Warning: (150-155): Overflow (resulting value larger than 2**256 - 1) happens here -// Warning: (269-282): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol index d90667dec..11cd22d11 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol @@ -8,10 +8,12 @@ contract C // Overflows due to resetting x. x = x + 1; } - // The assertion is true but x is touched and reset. + // Assertion is safe but current solver version cannot solve it. + // Keep test for next solver release. assert(x > 0); } } // ---- +// Warning: (296-309): Error trying to invoke SMT solver. // Warning: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here -// Warning: (244-257): Assertion violation happens here +// Warning: (296-309): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol index b0c3cae4c..9c54822e3 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_6.sol @@ -10,4 +10,3 @@ contract C { } } // ---- -// Warning: (213-226): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol index d545202f1..d7d88424a 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol @@ -18,5 +18,4 @@ contract LoopFor2 { } } // ---- -// Warning: (265-285): Assertion violation happens here // Warning: (312-331): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol index 0c3f84996..a6793af13 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol @@ -18,6 +18,5 @@ contract LoopFor2 { } } // ---- -// Warning: (266-286): Assertion violation happens here // Warning: (290-309): Assertion violation happens here // Warning: (313-332): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol index eec59ded8..bb928e2c1 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_loop_trivial_condition_3.sol @@ -15,4 +15,3 @@ contract C { } // ---- // Warning: (115-121): Unused local variable. -// Warning: (356-370): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_1.sol b/test/libsolidity/smtCheckerTests/loops/while_1.sol index 871ed9298..cb7fc5272 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_1.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_1.sol @@ -14,4 +14,3 @@ contract C } } // ---- -// Warning: (177-190): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_1_break.sol b/test/libsolidity/smtCheckerTests/loops/while_1_break.sol new file mode 100644 index 000000000..b406a336d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_1_break.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x, bool b) public pure { + require(x < 10); + while (x < 10) { + if (b) + ++x; + else { + x = 20; + break; + } + } + // Assertion is safe but break is unsupported for now + // so knowledge is erased. + assert(x >= 10); + } +} +// ---- +// Warning: (274-289): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_1_break_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_1_break_fail.sol new file mode 100644 index 000000000..f187eac3e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_1_break_fail.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x, bool b) public pure { + require(x < 10); + while (x < 10) { + if (b) + ++x; + else { + break; + } + } + // Fails because the loop might break. + assert(x >= 10); + } +} +// ---- +// Warning: (218-233): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_1_continue.sol b/test/libsolidity/smtCheckerTests/loops/while_1_continue.sol new file mode 100644 index 000000000..72e2dfd78 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_1_continue.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x, bool b) public pure { + require(x < 100); + while (x < 10) { + if (b) { + x = 15; + continue; + } + else + x = 20; + + } + // Should be safe, but fails due to continue being unsupported + // and erasing all knowledge. + assert(x >= 15); + } +} +// ---- +// Warning: (294-309): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_1_continue_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_1_continue_fail.sol new file mode 100644 index 000000000..389942906 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_1_continue_fail.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x, bool b) public pure { + require(x < 100); + while (x < 10) { + if (b) { + x = 15; + continue; + } + else + x = 20; + + } + // Fails due to the if. + assert(x >= 17); + } +} +// ---- +// Warning: (223-238): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_1_infinite.sol b/test/libsolidity/smtCheckerTests/loops/while_1_infinite.sol new file mode 100644 index 000000000..54b32b432 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_1_infinite.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x, bool b) public pure { + require(x < 100); + while (x < 10) { + if (b) + x = x + 1; + else + x = 0; + } + // CHC proves it safe because + // 1- if it doesn't go in the loop in the first place, x >= 10 + // 2- if it goes in the loop and b == true, x increases until >= 10 + // 3- if it goes in the loop and b == false, it's an infinite loop, therefore + // the assertion and the error are unreachable. + assert(x > 0); + } +} +// ---- diff --git a/test/libsolidity/smtCheckerTests/loops/while_2.sol b/test/libsolidity/smtCheckerTests/loops/while_2.sol new file mode 100644 index 000000000..00a71aca6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_2.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; +contract C { + function f(uint x) public pure { + x = 2; + while (x > 1) { + if (x > 10) + x = 2; + else + --x; + } + assert(x < 2); + } +} diff --git a/test/libsolidity/smtCheckerTests/loops/while_2_break.sol b/test/libsolidity/smtCheckerTests/loops/while_2_break.sol new file mode 100644 index 000000000..8fde4b06d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_2_break.sol @@ -0,0 +1,19 @@ +pragma experimental SMTChecker; + +contract C +{ + function f() public pure { + uint x = 0; + while (x == 0) { + ++x; + break; + ++x; + } + // Assertion is safe but break is unsupported for now + // so knowledge is erased. + assert(x == 1); + } +} +// ---- +// Warning: (128-131): Unreachable code. +// Warning: (224-238): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol new file mode 100644 index 000000000..efd9bb18b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x) public pure { + while (x == 0) { + ++x; + break; + ++x; + } + assert(x == 2); + } +} +// ---- +// Warning: (120-123): Unreachable code. +// Warning: (131-145): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_2_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_2_fail.sol index 4c52287db..3c3e50468 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_2_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_2_fail.sol @@ -12,4 +12,3 @@ contract C { } } // ---- -// Warning: (158-172): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol index 466cb9211..70bd231bb 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol @@ -13,11 +13,13 @@ contract LoopFor2 { c[i] = b[i]; ++i; } + // Fails due to aliasing, since both b and c are + // memory references of same type. assert(b[0] == c[0]); assert(a[0] == 900); assert(b[0] == 900); } } // ---- -// Warning: (274-294): Assertion violation happens here -// Warning: (321-340): Assertion violation happens here +// Warning: (362-382): Assertion violation happens here +// Warning: (409-428): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_memory.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_memory.sol index 74a53a3ba..6cb6cd6d9 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_memory.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_memory.sol @@ -20,5 +20,4 @@ contract LoopFor2 { } } // ---- -// Warning: (265-285): Assertion violation happens here // Warning: (312-331): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol index bbc9a2661..7670ddb6d 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol @@ -20,6 +20,5 @@ contract LoopFor2 { } } // ---- -// Warning: (266-286): Assertion violation happens here // Warning: (290-309): Assertion violation happens here // Warning: (313-332): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol index 5a3aee9ef..792a90e23 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_simple_4.sol @@ -8,4 +8,3 @@ contract C { } } // ---- -// Warning: (199-213): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.json b/test/libsolidity/smtCheckerTestsJSON/multi.json index b848f6338..e66b17ab0 100644 --- a/test/libsolidity/smtCheckerTestsJSON/multi.json +++ b/test/libsolidity/smtCheckerTestsJSON/multi.json @@ -4,7 +4,6 @@ "smtlib2responses": { "0x047d0c67d7e03c5ac96ca227d1e19ba63257f4ab19cef30029413219ec8963af": "sat\n((|EVALEXPR_0| 0))\n", - "0x21d5b49d1416d788fe34b1d2a10a99ea92b007e17a977604afd7b2ff01a055cd": "unsat\n", "0xada7569fb01a9b3e2823517ed40dcc99b11fb1e433e6e3ec8a8713f6f95753d3": "sat\n((|EVALEXPR_0| 1))\n" } }