From 1a70a46f9bd0658ecdc737a0531cd1b0c5724a4b Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 17 Jul 2019 18:01:14 +0200 Subject: [PATCH] [CHC] Add function blocks and check asserts --- Changelog.md | 2 + libsolidity/formal/CHC.cpp | 286 +++++++++++++++++- libsolidity/formal/CHC.h | 49 ++- .../invariants/state_machine_1.sol | 32 ++ .../invariants/state_machine_1_fail.sol | 32 ++ .../modifier_code_after_placeholder.sol | 4 + .../modifiers/modifier_multi.sol | 4 + .../modifiers/modifier_two_placeholders.sol | 4 + 8 files changed, 401 insertions(+), 12 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol create mode 100644 test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol diff --git a/Changelog.md b/Changelog.md index 14f6652f6..f4ee60640 100644 --- a/Changelog.md +++ b/Changelog.md @@ -24,9 +24,11 @@ Compiler Features: * Standard JSON Interface: Provide secondary error locations (e.g. the source position of other conflicting declarations). * SMTChecker: Do not erase knowledge about storage pointers if another storage pointer is assigned. * SMTChecker: Support string literal type. + * SMTChecker: New Horn-based algorithm that proves assertions via multi-transaction contract invariants. * Standard JSON Interface: Provide AST even on errors if ``--error-recovery`` commandline switch or StandardCompiler `settings.parserErrorRecovery` is true. * Yul Optimizer: Do not inline function if it would result in expressions being duplicated that are not cheap. + Bugfixes: * ABI decoder: Ensure that decoded arrays always point to distinct memory locations. * Code Generator: Treat dynamically encoded but statically sized arrays and structs in calldata properly. diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index e3a740b53..a65dd61f1 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -135,6 +135,44 @@ bool CHC::visit(FunctionDefinition const& _function) solAssert(!m_currentFunction, "Inlining internal function calls not yet implemented"); m_currentFunction = &_function; + initFunction(_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); + + solAssert(m_functionBlocks == 0, ""); + m_functionBlocks = 2; + SMTEncoder::visit(*m_currentFunction); return false; @@ -146,7 +184,36 @@ void CHC::endVisit(FunctionDefinition const& _function) return; 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() + ); + + // 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() + ); + 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(); SMTEncoder::endVisit(_function); } @@ -155,8 +222,30 @@ bool CHC::visit(IfStatement const& _if) { solAssert(m_currentFunction, ""); + bool unknownFunctionCallWasSeen = m_unknownFunctionCallSeen; + m_unknownFunctionCallSeen = false; + SMTEncoder::visit(_if); + if (m_unknownFunctionCallSeen) + eraseKnowledge(); + + m_unknownFunctionCallSeen = unknownFunctionCallWasSeen; + + return false; +} + +bool CHC::visit(WhileStatement const& _while) +{ + eraseKnowledge(); + m_context.resetVariables(touchedVariables(_while)); + return false; +} + +bool CHC::visit(ForStatement const& _for) +{ + eraseKnowledge(); + m_context.resetVariables(touchedVariables(_for)); return false; } @@ -164,20 +253,74 @@ void CHC::endVisit(FunctionCall const& _funCall) { solAssert(_funCall.annotation().kind != FunctionCallKind::Unset, ""); - if (_funCall.annotation().kind == FunctionCallKind::FunctionCall) + if (_funCall.annotation().kind != FunctionCallKind::FunctionCall) { - FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); - if (funType.kind() == FunctionType::Kind::Assert) - visitAssert(_funCall); + SMTEncoder::endVisit(_funCall); + return; } - SMTEncoder::endVisit(_funCall); + FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); + switch (funType.kind()) + { + case FunctionType::Kind::Assert: + visitAssert(_funCall); + SMTEncoder::endVisit(_funCall); + break; + case FunctionType::Kind::Internal: + case FunctionType::Kind::External: + case FunctionType::Kind::DelegateCall: + case FunctionType::Kind::BareCall: + case FunctionType::Kind::BareCallCode: + case FunctionType::Kind::BareDelegateCall: + case FunctionType::Kind::BareStaticCall: + case FunctionType::Kind::Creation: + case FunctionType::Kind::KECCAK256: + case FunctionType::Kind::ECRecover: + case FunctionType::Kind::SHA256: + case FunctionType::Kind::RIPEMD160: + case FunctionType::Kind::BlockHash: + case FunctionType::Kind::AddMod: + case FunctionType::Kind::MulMod: + SMTEncoder::endVisit(_funCall); + unknownFunctionCall(_funCall); + break; + default: + SMTEncoder::endVisit(_funCall); + break; + } createReturnedExpressions(_funCall); } -void CHC::visitAssert(FunctionCall const&) +void CHC::visitAssert(FunctionCall const& _funCall) { + auto const& args = _funCall.arguments(); + solAssert(args.size() == 1, ""); + solAssert(args.front()->annotation().type->category() == Type::Category::Bool, ""); + + solAssert(!m_path.empty(), ""); + + 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"); + + m_verificationTargets.push_back(&_funCall); +} + +void CHC::unknownFunctionCall(FunctionCall const&) +{ + /// Function calls are not handled at the moment, + /// so always erase knowledge. + /// TODO remove when function calls get predicates/blocks. + eraseKnowledge(); + + /// Used to erase outer scope knowledge in loops and ifs. + /// TODO remove when function calls get predicates/blocks. + m_unknownFunctionCallSeen = true; } void CHC::reset() @@ -186,6 +329,13 @@ void CHC::reset() m_stateVariables.clear(); m_verificationTargets.clear(); m_safeAssertions.clear(); + m_unknownFunctionCallSeen = false; +} + +void CHC::eraseKnowledge() +{ + resetStateVariables(); + m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.hasReferenceOrMappingType(); }); } bool CHC::shouldVisit(ContractDefinition const& _contract) const @@ -208,13 +358,25 @@ bool CHC::shouldVisit(FunctionDefinition const& _function) const return false; } +void CHC::pushBlock(smt::Expression const& _block) +{ + m_context.pushSolver(); + m_path.push_back(_block); +} + +void CHC::popBlock() +{ + m_context.popSolver(); + m_path.pop_back(); +} + smt::SortPointer CHC::constructorSort() { solAssert(m_currentContract, ""); auto boolSort = make_shared(smt::Kind::Bool); if (!m_currentContract->constructor()) return make_shared(vector{}, boolSort); - return functionSort(*m_currentContract->constructor()); + return sort(*m_currentContract->constructor()); } smt::SortPointer CHC::interfaceSort() @@ -226,14 +388,41 @@ smt::SortPointer CHC::interfaceSort() ); } -smt::SortPointer CHC::functionSort(FunctionDefinition const& _function) +smt::SortPointer CHC::sort(FunctionDefinition const& _function) { + if (m_nodeSorts.count(&_function)) + return m_nodeSorts.at(&_function); + auto boolSort = make_shared(smt::Kind::Bool); - auto const& funType = dynamic_cast(*_function.type()); - return make_shared( - smt::smtSort(funType.parameterTypes()), + vector varSorts; + for (auto const& var: _function.parameters() + _function.returnParameters()) + varSorts.push_back(smt::smtSort(*var->type())); + auto sort = make_shared( + m_stateSorts + varSorts, boolSort ); + return m_nodeSorts[&_function] = move(sort); +} + +smt::SortPointer CHC::sort(Block const& _block) +{ + if (m_nodeSorts.count(&_block)) + return m_nodeSorts.at(&_block); + + solAssert(_block.scope() == m_currentFunction, ""); + + auto fSort = dynamic_pointer_cast(sort(*m_currentFunction)); + solAssert(fSort, ""); + + auto boolSort = make_shared(smt::Kind::Bool); + vector varSorts; + for (auto const& var: m_currentFunction->localVariables()) + varSorts.push_back(smt::smtSort(*var->type())); + auto functionBodySort = make_shared( + fSort->domain + varSorts, + boolSort + ); + return m_nodeSorts[&_block] = move(functionBodySort); } unique_ptr CHC::createBlock(smt::SortPointer _sort, string const& _name) @@ -273,6 +462,81 @@ smt::Expression CHC::error() return (*m_errorPredicate)({}); } +void CHC::createFunctionBlock(FunctionDefinition const& _function) +{ + 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) + ); +} + +void CHC::createFunctionBlock(Block const& _block) +{ + solAssert(_block.scope() == m_currentFunction, ""); + if (m_predicates.count(&_block)) + { + m_predicates.at(&_block)->increaseIndex(); + m_interface->registerRelation(m_predicates.at(&_block)->currentValue()); + } + else + m_predicates[&_block] = createBlock( + sort(_block), + predicateName(*m_currentFunction) + "_body" + ); +} + +vector CHC::currentFunctionVariables() +{ + solAssert(m_currentFunction, ""); + vector paramExprs; + for (auto const& var: m_stateVariables) + paramExprs.push_back(m_context.variable(*var)->currentValue()); + for (auto const& var: m_currentFunction->parameters() + m_currentFunction->returnParameters()) + paramExprs.push_back(m_context.variable(*var)->currentValue()); + return paramExprs; +} + +vector CHC::currentBlockVariables() +{ + solAssert(m_currentFunction, ""); + vector paramExprs; + for (auto const& var: m_currentFunction->localVariables()) + paramExprs.push_back(m_context.variable(*var)->currentValue()); + return currentFunctionVariables() + paramExprs; +} + +string CHC::predicateName(FunctionDefinition const& _function) +{ + string functionName = _function.isConstructor() ? + "constructor" : + _function.isFallback() ? + "fallback" : + "function_" + _function.name(); + return functionName + "_" + to_string(_function.id()); +} + +smt::Expression CHC::predicateCurrent(ASTNode const* _node) +{ + return (*m_predicates.at(_node))(currentFunctionVariables()); +} + +smt::Expression CHC::predicateBodyCurrent(ASTNode const* _node) +{ + return (*m_predicates.at(_node))(currentBlockVariables()); +} + +smt::Expression CHC::predicateEntry(ASTNode const* _node) +{ + solAssert(!m_path.empty(), ""); + return (*m_predicates.at(_node))(m_path.back().arguments); +} + bool CHC::query(smt::Expression const& _query, langutil::SourceLocation const& _location) { smt::CheckResult result; diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index d8108933a..a31b3aab1 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -58,23 +58,30 @@ private: bool visit(FunctionDefinition const& _node) override; void endVisit(FunctionDefinition const& _node) override; bool visit(IfStatement const& _node) override; + bool visit(WhileStatement const&) override; + bool visit(ForStatement const&) override; void endVisit(FunctionCall const& _node) override; void visitAssert(FunctionCall const& _funCall); + void unknownFunctionCall(FunctionCall const& _funCall); //@} /// Helpers. //@{ void reset(); + void eraseKnowledge(); bool shouldVisit(ContractDefinition const& _contract) const; bool shouldVisit(FunctionDefinition const& _function) const; + void pushBlock(smt::Expression const& _block); + void popBlock(); //@} /// Sort helpers. //@{ smt::SortPointer constructorSort(); smt::SortPointer interfaceSort(); - smt::SortPointer functionSort(FunctionDefinition const& _function); + smt::SortPointer sort(FunctionDefinition const& _function); + smt::SortPointer sort(Block const& _block); //@} /// Predicate helpers. @@ -88,6 +95,33 @@ private: smt::Expression interface(); /// Error predicate over current variables. smt::Expression error(); + + /// 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 _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); + + /// @returns the current symbolic values of the current function's + /// input and output parameters. + std::vector currentFunctionVariables(); + /// @returns the samve as currentFunctionVariables plus + /// 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); //@} /// Solver related. @@ -109,6 +143,9 @@ private: /// Artificial Error predicate. /// Single error block for all assertions. std::unique_ptr m_errorPredicate; + + /// Maps AST nodes to their predicates. + std::unordered_map> m_predicates; //@} /// Variables. @@ -119,6 +156,9 @@ private: /// State variables. /// Used to create all predicates. std::vector m_stateVariables; + + /// Input sorts for AST nodes. + std::map m_nodeSorts; //@} /// Verification targets. @@ -132,6 +172,13 @@ private: /// Control-flow. //@{ FunctionDefinition const* m_currentFunction = nullptr; + + /// Number of basic blocks created for the body of the current function. + unsigned m_functionBlocks = 0; + /// The current control flow path. + std::vector m_path; + /// Whether a function call was seen in the current scope. + bool m_unknownFunctionCallSeen = false; //@} /// CHC solver. diff --git a/test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol b/test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol new file mode 100644 index 000000000..9cc43504c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/invariants/state_machine_1.sol @@ -0,0 +1,32 @@ +pragma experimental SMTChecker; + +contract C { + uint x; + + function f() public { + if (x == 0) + x = 1; + } + + function g() public { + if (x == 1) + x = 2; + } + + function h() public { + if (x == 2) + x = 0; + } + + // This function shows that (x < 9) is not inductive and + // a stronger invariant is needed to be found. + // (x < 3) is the one found in the end. + function j() public { + if (x == 7) + x = 100; + } + + function i() public view { + assert(x < 9); + } +} diff --git a/test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol b/test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol new file mode 100644 index 000000000..7699337a1 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/invariants/state_machine_1_fail.sol @@ -0,0 +1,32 @@ +pragma experimental SMTChecker; + +contract C { + uint x; + + function f() public { + if (x == 0) + x = 1; + } + + function g() public { + if (x == 1) + x = 2; + } + + function h() public { + if (x == 2) + x = 0; + } + + function j() public { + if (x < 2) + x = 100; + } + + // Fails due to j. + function i() public view { + assert(x < 2); + } +} +// ---- +// Warning: (311-324): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol index 5ccaec149..7a420c28f 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_code_after_placeholder.sol @@ -15,6 +15,10 @@ contract C assert(x > 0); x = x + 1; } + + function g(uint _x) public { + x = _x; + } } // ---- // Warning: (136-149): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_multi.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_multi.sol index 8a508cd68..241a367ea 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_multi.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_multi.sol @@ -20,6 +20,10 @@ contract C function f() m n public { x = x + 1; } + + function g(uint _x) public { + x = _x; + } } // ---- // Warning: (170-183): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/modifiers/modifier_two_placeholders.sol b/test/libsolidity/smtCheckerTests/modifiers/modifier_two_placeholders.sol index 288506607..65b07f881 100644 --- a/test/libsolidity/smtCheckerTests/modifiers/modifier_two_placeholders.sol +++ b/test/libsolidity/smtCheckerTests/modifiers/modifier_two_placeholders.sol @@ -17,6 +17,10 @@ contract C function f() m public { x = x + 1; } + + function g(uint _x) public { + x = _x; + } } // ---- // Warning: (156-170): Assertion violation happens here