From 5160f89c1bae4978e9de0a5711b90747fb1a1a95 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Thu, 14 May 2020 20:09:52 +0200 Subject: [PATCH] [SMTChecker] Support to external calls to unknown code --- Changelog.md | 2 + libsolidity/formal/CHC.cpp | 150 +++++++++++++++--- libsolidity/formal/CHC.h | 17 +- .../external_calls/external.sol | 20 +++ .../external_calls/external_hash.sol | 29 ++++ .../external_hash_known_code_pure.sol | 29 ++++ .../external_hash_known_code_state.sol | 38 +++++ ...ernal_hash_known_code_state_reentrancy.sol | 32 ++++ ...h_known_code_state_reentrancy_indirect.sol | 47 ++++++ ...ash_known_code_state_reentrancy_unsafe.sol | 39 +++++ .../external_hash_known_code_state_unsafe.sol | 43 +++++ .../external_calls/external_inc.sol | 22 +++ .../external_calls/external_inc1_inc2.sol | 28 ++++ .../external_calls/external_safe.sol | 18 +++ .../external_calls/external_single_inc.sol | 26 +++ .../smtCheckerTests/external_calls/mutex.sol | 28 ++++ .../external_calls/mutex_f_no_guard.sol | 30 ++++ .../functions/functions_external_1.sol | 1 - .../functions/functions_external_3.sol | 1 - .../functions/functions_external_4.sol | 1 - .../loops/for_1_false_positive.sol | 2 + .../types/address_staticcall.sol | 3 - 22 files changed, 571 insertions(+), 35 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_inc.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_inc1_inc2.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_safe.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_single_inc.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/mutex.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/mutex_f_no_guard.sol diff --git a/Changelog.md b/Changelog.md index 4a590a5f3..02da20254 100644 --- a/Changelog.md +++ b/Changelog.md @@ -10,6 +10,8 @@ Compiler Features: * Commandline Interface: Prevent some incompatible commandline options from being used together. * NatSpec: Support NatSpec comments on events. * Yul Optimizer: Store knowledge about storage / memory after ``a := sload(x)`` / ``a := mload(x)``. + * SMTChecker: Support to external calls to unknown code and to known view/pure functions. + Bugfixes: * NatSpec: Do not consider ``////`` and ``/***`` as NatSpec comments. diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 791a4f41d..2609e356e 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -197,8 +197,11 @@ void CHC::endVisit(ContractDefinition const& _contract) bool CHC::visit(FunctionDefinition const& _function) { - if (!shouldVisit(_function)) + if (!_function.isImplemented()) + { + connectBlocks(genesis(), summary(_function)); return false; + } // This is the case for base constructor inlining. if (m_currentFunction) @@ -243,7 +246,7 @@ bool CHC::visit(FunctionDefinition const& _function) void CHC::endVisit(FunctionDefinition const& _function) { - if (!shouldVisit(_function)) + if (!_function.isImplemented()) return; // This is the case for base constructor inlining. @@ -474,11 +477,14 @@ void CHC::endVisit(FunctionCall const& _funCall) internalFunctionCall(_funCall); break; case FunctionType::Kind::External: + case FunctionType::Kind::BareStaticCall: + externalFunctionCall(_funCall); + SMTEncoder::endVisit(_funCall); + break; 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: @@ -574,6 +580,33 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall) m_context.addAssertion(m_error.currentValue() == previousError); } +void CHC::externalFunctionCall(FunctionCall const& _funCall) +{ + solAssert(m_currentContract, ""); + + FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); + auto kind = funType.kind(); + solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, ""); + + auto const* function = functionCallToDefinition(_funCall); + if (!function) + return; + + auto preCallState = currentStateVariables(); + bool noStateChanges = kind == FunctionType::Kind::BareStaticCall || + function->stateMutability() == StateMutability::Pure || + function->stateMutability() == StateMutability::View; + if (!noStateChanges) + for (auto const* var: m_stateVariables) + m_context.variable(*var)->increaseIndex(); + + auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + currentStateVariables()); + m_context.addAssertion(nondet); + m_context.addAssertion(predicate(_funCall)); + + m_context.addAssertion(m_error.currentValue() == 0); +} + void CHC::unknownFunctionCall(FunctionCall const&) { /// Function calls are not handled at the moment, @@ -651,11 +684,6 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c } } -bool CHC::shouldVisit(FunctionDefinition const& _function) const -{ - return _function.isImplemented(); -} - void CHC::setCurrentBlock( smt::SymbolicFunctionVariable const& _block, vector const* _arguments @@ -710,10 +738,14 @@ smtutil::SortPointer CHC::constructorSort() smtutil::SortPointer CHC::interfaceSort() { - return make_shared( - m_stateSorts, - smtutil::SortProvider::boolSort - ); + solAssert(m_currentContract, ""); + return interfaceSort(*m_currentContract); +} + +smtutil::SortPointer CHC::nondetInterfaceSort() +{ + solAssert(m_currentContract, ""); + return nondetInterfaceSort(*m_currentContract); } smtutil::SortPointer CHC::interfaceSort(ContractDefinition const& _contract) @@ -724,6 +756,15 @@ smtutil::SortPointer CHC::interfaceSort(ContractDefinition const& _contract) ); } +smtutil::SortPointer CHC::nondetInterfaceSort(ContractDefinition const& _contract) +{ + auto sorts = stateSorts(_contract); + return make_shared( + sorts + sorts, + smtutil::SortProvider::boolSort + ); +} + smtutil::SortPointer CHC::arity0FunctionSort() { return make_shared( @@ -802,11 +843,47 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source) { string suffix = base->name() + "_" + to_string(base->id()); m_interfaces[base] = createSymbolicBlock(interfaceSort(*base), "interface_" + suffix); + m_nondetInterfaces[base] = createSymbolicBlock(nondetInterfaceSort(*base), "nondet_interface_" + suffix); + for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*base)) if (!m_context.knownVariable(*var)) createVariable(*var); + + /// Base nondeterministic interface that allows + /// 0 steps to be taken, used as base for the inductive + /// rule for each function. + auto const& iface = *m_nondetInterfaces.at(base); + auto state0 = stateVariablesAtIndex(0, *base); + addRule(iface(state0 + state0), "base_nondet"); + for (auto const* function: base->definedFunctions()) + { + for (auto var: function->parameters()) + createVariable(*var); + for (auto var: function->returnParameters()) + createVariable(*var); + for (auto const* var: function->localVariables()) + createVariable(*var); + m_summaries[contract].emplace(function, createSummaryBlock(*function, *contract)); + + if (!base->isLibrary() && !base->isInterface() && !function->isConstructor()) + { + auto state1 = stateVariablesAtIndex(1, *base); + auto state2 = stateVariablesAtIndex(2, *base); + + auto nondetPre = iface(state0 + state1); + auto nondetPost = iface(state0 + state2); + + vector args{m_error.currentValue()}; + args += state1 + + applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) + + state2 + + applyMap(function->returnParameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }); + + connectBlocks(nondetPre, nondetPost, (*m_summaries.at(base).at(function))(args)); + } + } } } @@ -842,15 +919,21 @@ smtutil::Expression CHC::summary(ContractDefinition const&) ); } -smtutil::Expression CHC::summary(FunctionDefinition const& _function) +smtutil::Expression CHC::summary(FunctionDefinition const& _function, ContractDefinition const& _contract) { vector args{m_error.currentValue()}; auto contract = _function.annotation().contract; - args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : initialStateVariables(); + args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : initialStateVariables(_contract); args += applyMap(_function.parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }); - args += contract->isLibrary() ? stateVariablesAtIndex(1, *contract) : currentStateVariables(); + args += contract->isLibrary() ? stateVariablesAtIndex(1, *contract) : currentStateVariables(_contract); args += applyMap(_function.returnParameters(), [this](auto _var) { return currentValue(*_var); }); - return (*m_summaries.at(m_currentContract).at(&_function))(args); + return (*m_summaries.at(&_contract).at(&_function))(args); +} + +smtutil::Expression CHC::summary(FunctionDefinition const& _function) +{ + solAssert(m_currentContract, ""); + return summary(_function, *m_currentContract); } unique_ptr CHC::createBlock(ASTNode const* _node, string const& _prefix) @@ -893,13 +976,18 @@ vector CHC::initialStateVariables() return stateVariablesAtIndex(0); } -vector CHC::stateVariablesAtIndex(unsigned _index) +vector CHC::initialStateVariables(ContractDefinition const& _contract) { - solAssert(m_currentContract, ""); - return applyMap(m_stateVariables, [&](auto _var) { return valueAtIndex(*_var, _index); }); + return stateVariablesAtIndex(0, _contract); } -vector CHC::stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract) +vector CHC::stateVariablesAtIndex(int _index) +{ + solAssert(m_currentContract, ""); + return stateVariablesAtIndex(_index, *m_currentContract); +} + +vector CHC::stateVariablesAtIndex(int _index, ContractDefinition const& _contract) { return applyMap( stateVariablesIncludingInheritedAndPrivate(_contract), @@ -910,7 +998,12 @@ vector CHC::stateVariablesAtIndex(unsigned _index, Contract vector CHC::currentStateVariables() { solAssert(m_currentContract, ""); - return applyMap(m_stateVariables, [this](auto _var) { return currentValue(*_var); }); + return currentStateVariables(*m_currentContract); +} + +vector CHC::currentStateVariables(ContractDefinition const& _contract) +{ + return applyMap(stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); }); } vector CHC::currentFunctionVariables() @@ -978,12 +1071,17 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall) m_error.increaseIndex(); vector args{m_error.currentValue()}; auto const* contract = function->annotation().contract; + FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); + bool otherContract = contract->isLibrary() || + funType.kind() == FunctionType::Kind::External || + funType.kind() == FunctionType::Kind::BareStaticCall; - args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : currentStateVariables(); + args += otherContract ? stateVariablesAtIndex(0, *contract) : currentStateVariables(); args += symbolicArguments(_funCall); - for (auto const& var: m_stateVariables) - m_context.variable(*var)->increaseIndex(); - args += contract->isLibrary() ? stateVariablesAtIndex(1, *contract) : currentStateVariables(); + if (!otherContract) + for (auto const& var: m_stateVariables) + m_context.variable(*var)->increaseIndex(); + args += otherContract ? stateVariablesAtIndex(1, *contract) : currentStateVariables(); auto const& returnParams = function->returnParameters(); for (auto param: returnParams) @@ -993,7 +1091,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall) createVariable(*param); args += applyMap(function->returnParameters(), [this](auto _var) { return currentValue(*_var); }); - if (contract->isLibrary()) + if (otherContract) return (*m_summaries.at(contract).at(function))(args); solAssert(m_currentContract, ""); diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index b52ce6667..dcba90606 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -77,6 +77,7 @@ private: void visitAssert(FunctionCall const& _funCall); void internalFunctionCall(FunctionCall const& _funCall); + void externalFunctionCall(FunctionCall const& _funCall); void unknownFunctionCall(FunctionCall const& _funCall); void makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) override; //@} @@ -95,7 +96,6 @@ private: void resetContractAnalysis(); void eraseKnowledge(); void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override; - bool shouldVisit(FunctionDefinition const& _function) const; void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector const* _arguments = nullptr); std::set transactionAssertions(ASTNode const* _txRoot); static std::vector stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract); @@ -106,7 +106,9 @@ private: static std::vector stateSorts(ContractDefinition const& _contract); smtutil::SortPointer constructorSort(); smtutil::SortPointer interfaceSort(); + smtutil::SortPointer nondetInterfaceSort(); static smtutil::SortPointer interfaceSort(ContractDefinition const& _const); + static smtutil::SortPointer nondetInterfaceSort(ContractDefinition const& _const); smtutil::SortPointer arity0FunctionSort(); smtutil::SortPointer sort(FunctionDefinition const& _function); smtutil::SortPointer sort(ASTNode const* _block); @@ -149,10 +151,12 @@ private: /// @returns the symbolic values of the state variables at the beginning /// of the current transaction. std::vector initialStateVariables(); - std::vector stateVariablesAtIndex(unsigned _index); - std::vector stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract); + std::vector initialStateVariables(ContractDefinition const& _contract); + std::vector stateVariablesAtIndex(int _index); + std::vector stateVariablesAtIndex(int _index, ContractDefinition const& _contract); /// @returns the current symbolic values of the current state variables. std::vector currentStateVariables(); + std::vector currentStateVariables(ContractDefinition const& _contract); /// @returns the current symbolic values of the current function's /// input and output parameters. @@ -173,6 +177,7 @@ private: smtutil::Expression summary(ContractDefinition const& _contract); /// @returns a predicate that defines a function summary. smtutil::Expression summary(FunctionDefinition const& _function); + smtutil::Expression summary(FunctionDefinition const& _function, ContractDefinition const& _contract); //@} /// Solver related. @@ -212,6 +217,12 @@ private: /// Single entry block for all functions. std::map> m_interfaces; + /// Nondeterministic interfaces. + /// These are used when the analyzed contract makes external calls to unknown code, + /// which means that the analyzed contract can potentially be called + /// nondeterministically. + std::map> m_nondetInterfaces; + /// Artificial Error predicate. /// Single error block for all assertions. std::unique_ptr m_errorPredicate; diff --git a/test/libsolidity/smtCheckerTests/external_calls/external.sol b/test/libsolidity/smtCheckerTests/external_calls/external.sol new file mode 100644 index 000000000..9fbde057a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external.sol @@ -0,0 +1,20 @@ +pragma experimental SMTChecker; + +abstract contract D { + function d() external virtual; +} + +contract C { + uint x; + D d; + function f() public { + if (x < 10) + ++x; + } + function g() public { + d.d(); + assert(x < 10); + } +} +// ---- +// Warning 4661: (200-214): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash.sol new file mode 100644 index 000000000..c0e9a7965 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash.sol @@ -0,0 +1,29 @@ +pragma experimental SMTChecker; + +abstract contract Crypto { + function hash(bytes32) external pure virtual returns (bytes32); +} + +contract C { + address owner; + bytes32 sig_1; + bytes32 sig_2; + Crypto d; + + constructor() public { + owner = msg.sender; + } + + function f1(bytes32 _msg) public { + address prevOwner = owner; + sig_1 = d.hash(_msg); + sig_2 = d.hash(_msg); + assert(prevOwner == owner); + } + + function inv() public view { + assert(sig_1 == sig_2); + } +} +// ---- +// Warning 4661: (430-452): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure.sol new file mode 100644 index 000000000..cd08791e0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure.sol @@ -0,0 +1,29 @@ +pragma experimental SMTChecker; + +contract Crypto { + function hash(bytes32) external pure returns (bytes32) { + return bytes32(0); + } +} + +contract C { + address owner; + bytes32 sig_1; + bytes32 sig_2; + Crypto d; + + constructor() public { + owner = msg.sender; + } + + function f1(bytes32 _msg) public { + address prevOwner = owner; + sig_1 = d.hash(_msg); + sig_2 = d.hash(_msg); + assert(prevOwner == owner); + } + + function inv() public view { + assert(sig_1 == sig_2); + } +} diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol new file mode 100644 index 000000000..3f6244e1e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol @@ -0,0 +1,38 @@ +pragma experimental SMTChecker; + +contract State { + uint x; + function f() public returns (uint) { + if (x == 0) x = 1; + else if (x == 1) x = 2; + else if (x == 2) x = 0; + return x; + } +} + +contract C { + address owner; + uint y; + uint z; + State s; + + constructor() public { + owner = msg.sender; + } + + function f() public { + address prevOwner = owner; + y = s.f(); + z = s.f(); + assert(prevOwner == owner); + } + + function inv() public view { + // This is safe but external calls do not yet support the state + // of the called contract. + assert(owner == address(0) || y != z); + } +} +// ---- +// Warning 5084: (551-561): Type conversion is not yet fully supported and might yield false positives. +// Warning 4661: (535-572): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol new file mode 100644 index 000000000..2439fc864 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol @@ -0,0 +1,32 @@ +pragma experimental SMTChecker; + +contract State { + uint x; + C c; + function f() public view returns (uint) { + return c.g(); + } +} + +contract C { + address owner; + uint y; + State s; + + constructor() public { + owner = msg.sender; + } + + function f() public view { + address prevOwner = owner; + uint z = s.f(); + assert(z == y); + assert(prevOwner == owner); + } + + function g() public view returns (uint) { + return y; + } +} +// ---- +// Warning 4661: (306-320): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol new file mode 100644 index 000000000..9a8f9ed8e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol @@ -0,0 +1,47 @@ +pragma experimental SMTChecker; + +contract Other { + C c; + function h() public { + c.setOwner(address(0)); + } +} + +contract State { + uint x; + Other o; + C c; + function f() public returns (uint) { + o.h(); + return c.g(); + } +} + +contract C { + address owner; + uint y; + State s; + + constructor() public { + owner = msg.sender; + } + + function setOwner(address _owner) public { + owner = _owner; + } + + function f() public { + address prevOwner = owner; + uint z = s.f(); + assert(z == y); + assert(prevOwner == owner); + } + + function g() public view returns (uint) { + return y; + } +} +// ---- +// Warning 5084: (92-102): Type conversion is not yet fully supported and might yield false positives. +// Warning 4661: (459-473): Assertion violation happens here +// Warning 4661: (477-503): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe.sol new file mode 100644 index 000000000..c60b6b05d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe.sol @@ -0,0 +1,39 @@ +pragma experimental SMTChecker; + +contract State { + uint x; + C c; + function f() public returns (uint) { + c.setOwner(address(0)); + return c.g(); + } +} + +contract C { + address owner; + uint y; + State s; + + constructor() public { + owner = msg.sender; + } + + function setOwner(address _owner) public { + owner = _owner; + } + + function f() public { + address prevOwner = owner; + uint z = s.f(); + assert(z == y); + assert(prevOwner == owner); + } + + function g() public view returns (uint) { + return y; + } +} +// ---- +// Warning 5084: (116-126): Type conversion is not yet fully supported and might yield false positives. +// Warning 4661: (388-402): Assertion violation happens here +// Warning 4661: (406-432): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe.sol new file mode 100644 index 000000000..336d75b97 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe.sol @@ -0,0 +1,43 @@ +pragma experimental SMTChecker; + +contract State { + uint x; + function f() public returns (uint) { + if (x == 0) x = 1; + else if (x == 1) x = 2; + else if (x == 2) x = 0; + return x; + } +} + +contract C { + address owner; + uint y; + uint z; + State s; + + constructor() public { + owner = msg.sender; + } + + function setOwner(address _owner) public { + owner = _owner; + } + + function f() public { + address prevOwner = owner; + y = s.f(); + z = s.f(); + assert(prevOwner == owner); + } + + function inv() public view { + // This is safe but external calls do not yet support the state + // of the called contract. + assert(owner == address(0) || y != z); + } +} +// ---- +// Warning 4661: (442-468): Assertion violation happens here +// Warning 5084: (617-627): Type conversion is not yet fully supported and might yield false positives. +// Warning 4661: (601-638): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol b/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol new file mode 100644 index 000000000..d4d2489b0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; + +abstract contract D { + function d() external virtual; +} + +contract C { + uint x; + D d; + + function inc() public { + ++x; + } + + function f() public { + d.d(); + assert(x < 10); + } +} +// ---- +// Warning 2661: (146-149): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning 4661: (189-203): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_inc1_inc2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_inc1_inc2.sol new file mode 100644 index 000000000..2787b4158 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_inc1_inc2.sol @@ -0,0 +1,28 @@ +pragma experimental SMTChecker; + +abstract contract D { + function d() external virtual; +} + +contract C { + uint x; + uint y; + D d; + + function inc2() public { + if (y == 1) + x = 1; + } + function inc1() public { + if (x == 0) + y = 1; + } + + function f() public { + uint oldX = x; + d.d(); + assert(oldX == x); + } +} +// ---- +// Warning 4661: (286-303): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol b/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol new file mode 100644 index 000000000..6a2b66491 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +abstract contract D { + function d() external virtual; +} + +contract C { + uint x; + D d; + function f() public { + if (x < 10) + ++x; + } + function g() public { + d.d(); + assert(x < 11); + } +} diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_single_inc.sol b/test/libsolidity/smtCheckerTests/external_calls/external_single_inc.sol new file mode 100644 index 000000000..247c45f32 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_single_inc.sol @@ -0,0 +1,26 @@ +pragma experimental SMTChecker; + +abstract contract D { + function d() external virtual; +} + +contract C { + uint x; + uint y; + D d; + + function inc() public { + if (y == 1) + x = 1; + if (x == 0) + y = 1; + } + + function f() public { + uint oldX = x; + d.d(); + assert(oldX == x); + } +} +// ---- +// Warning 4661: (256-273): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/external_calls/mutex.sol b/test/libsolidity/smtCheckerTests/external_calls/mutex.sol new file mode 100644 index 000000000..1173da3f8 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/mutex.sol @@ -0,0 +1,28 @@ +pragma experimental SMTChecker; + +abstract contract D { + function d() external virtual; +} + +contract C { + uint x; + D d; + + bool lock; + modifier mutex { + require(!lock); + lock = true; + _; + lock = false; + } + + function set(uint _x) mutex public { + x = _x; + } + + function f() mutex public { + uint y = x; + d.d(); + assert(y == x); + } +} diff --git a/test/libsolidity/smtCheckerTests/external_calls/mutex_f_no_guard.sol b/test/libsolidity/smtCheckerTests/external_calls/mutex_f_no_guard.sol new file mode 100644 index 000000000..08f3c7b76 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/mutex_f_no_guard.sol @@ -0,0 +1,30 @@ +pragma experimental SMTChecker; + +abstract contract D { + function d() external virtual; +} + +contract C { + uint x; + D d; + + bool lock; + modifier mutex { + require(!lock); + lock = true; + _; + lock = false; + } + + function set(uint _x) mutex public { + x = _x; + } + + function f() public { + uint y = x; + d.d(); + assert(y == x); + } +} +// ---- +// Warning 4661: (307-321): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol index cce33f8a6..beb95617f 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol @@ -17,4 +17,3 @@ contract C } } // ---- -// Warning 4661: (257-271): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol index 15f1f6001..589d17165 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol @@ -18,4 +18,3 @@ contract C } } // ---- -// Warning 4661: (355-379): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_4.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_4.sol index 02813f1d7..f650ce824 100644 --- a/test/libsolidity/smtCheckerTests/functions/functions_external_4.sol +++ b/test/libsolidity/smtCheckerTests/functions/functions_external_4.sol @@ -16,4 +16,3 @@ contract D } } // ---- -// Warning 4661: (191-206): 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 b05b47f53..ee6933d17 100644 --- a/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol +++ b/test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol @@ -14,4 +14,6 @@ contract C } } // ---- +// Warning 1218: (296-309): Error trying to invoke SMT solver. // Warning 2661: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here +// Warning 4661: (296-309): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/address_staticcall.sol b/test/libsolidity/smtCheckerTests/types/address_staticcall.sol index e4644ed8a..55e0b7427 100644 --- a/test/libsolidity/smtCheckerTests/types/address_staticcall.sol +++ b/test/libsolidity/smtCheckerTests/types/address_staticcall.sol @@ -20,6 +20,3 @@ contract C // ---- // Warning 2072: (224-240): Unused local variable. // Warning 4661: (266-281): Assertion violation happens here -// Warning 4661: (285-299): Assertion violation happens here -// Warning 4661: (303-322): Assertion violation happens here -// Warning 4661: (326-350): Assertion violation happens here