From 7f8ceaadab0c265674b591aa50cfeb8910628b9f Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Thu, 20 Dec 2018 18:11:20 +0100 Subject: [PATCH] [SMTChecker] Clear state knowledge after external function calls --- Changelog.md | 1 + libsolidity/formal/SMTChecker.cpp | 36 +++++++++++++------ libsolidity/formal/SMTChecker.h | 3 ++ ...unction_call_does_not_clear_local_vars.sol | 1 - .../functions/functions_external_1.sol | 21 +++++++++++ .../functions/functions_external_2.sol | 21 +++++++++++ .../functions/functions_external_3.sol | 22 ++++++++++++ 7 files changed, 93 insertions(+), 12 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_external_1.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_external_2.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_external_3.sol diff --git a/Changelog.md b/Changelog.md index d3bb8e105..53097159d 100644 --- a/Changelog.md +++ b/Changelog.md @@ -7,6 +7,7 @@ Language Features: Compiler Features: * Control Flow Graph: Warn about unreachable code. * SMTChecker: Support basic typecasts without truncation. + * SMTChecker: Support external function calls and erase all knowledge regarding storage variables and references. Bugfixes: diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 387152890..500b610f6 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -418,6 +418,10 @@ void SMTChecker::endVisit(FunctionCall const& _funCall) case FunctionType::Kind::Internal: inlineFunctionCall(_funCall); break; + case FunctionType::Kind::External: + resetStateVariables(); + resetStorageReferences(); + break; case FunctionType::Kind::KECCAK256: case FunctionType::Kind::ECRecover: case FunctionType::Kind::SHA256: @@ -1194,25 +1198,35 @@ void SMTChecker::removeLocalVariables() } } +void SMTChecker::resetVariable(VariableDeclaration const& _variable) +{ + newValue(_variable); + setUnknownValue(_variable); +} + void SMTChecker::resetStateVariables() { - for (auto const& variable: m_variables) - { - if (variable.first->isStateVariable()) - { - newValue(*variable.first); - setUnknownValue(*variable.first); - } - } + resetVariables([&](VariableDeclaration const& _variable) { return _variable.isStateVariable(); }); +} + +void SMTChecker::resetStorageReferences() +{ + resetVariables([&](VariableDeclaration const& _variable) { return _variable.hasReferenceOrMappingType(); }); } void SMTChecker::resetVariables(vector _variables) { for (auto const* decl: _variables) + resetVariable(*decl); +} + +void SMTChecker::resetVariables(function const& _filter) +{ + for_each(begin(m_variables), end(m_variables), [&](auto _variable) { - newValue(*decl); - setUnknownValue(*decl); - } + if (_filter(*_variable.first)) + this->resetVariable(*_variable.first); + }); } void SMTChecker::mergeVariables(vector const& _variables, smt::Expression const& _condition, VariableIndices const& _indicesEndTrue, VariableIndices const& _indicesEndFalse) diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index caa837647..a85933c83 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -147,8 +147,11 @@ private: void initializeLocalVariables(FunctionDefinition const& _function); void initializeFunctionCallParameters(FunctionDefinition const& _function, std::vector const& _callArgs); + void resetVariable(VariableDeclaration const& _variable); void resetStateVariables(); + void resetStorageReferences(); void resetVariables(std::vector _variables); + void resetVariables(std::function const& _filter); /// Given two different branches and the touched variables, /// merge the touched variables into after-branch ite variables /// using the branch condition as guard. diff --git a/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol b/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol index b42602240..0ceb3b46c 100644 --- a/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol +++ b/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol @@ -9,5 +9,4 @@ contract C { } } // ---- -// Warning: (99-107): Assertion checker does not yet implement this type of function call. // Warning: (141-144): Assertion checker does not support recursive function calls. diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol new file mode 100644 index 000000000..16482e7a7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; + +contract D +{ + function g(uint x) public; +} + +contract C +{ + uint x; + function f(uint y, D d) public { + require(x == y); + assert(x == y); + d.g(y); + // Storage knowledge is cleared after an external call. + assert(x == y); + } +} +// ---- +// Warning: (119-122): Assertion checker does not yet support the type of this variable. +// Warning: (240-254): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol new file mode 100644 index 000000000..1e704c9db --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; + +contract D +{ + function g(uint x) public; +} + +contract C +{ + mapping (uint => uint) map; + function f(uint y, D d) public { + require(map[0] == map[1]); + assert(map[0] == map[1]); + d.g(y); + // Storage knowledge is cleared after an external call. + assert(map[0] == map[1]); + } +} +// ---- +// Warning: (139-142): Assertion checker does not yet support the type of this variable. +// Warning: (280-304): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol new file mode 100644 index 000000000..dd36ec736 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol @@ -0,0 +1,22 @@ +pragma experimental SMTChecker; + +contract D +{ + function g(uint x) public; +} + +contract C +{ + mapping (uint => uint) storageMap; + function f(uint y, D d) public { + mapping (uint => uint) storage map = storageMap; + require(map[0] == map[1]); + assert(map[0] == map[1]); + d.g(y); + // Storage knowledge is cleared after an external call. + assert(map[0] == map[1]); + } +} +// ---- +// Warning: (146-149): Assertion checker does not yet support the type of this variable. +// Warning: (338-362): Assertion violation happens here