diff --git a/Changelog.md b/Changelog.md index 93661c507..9e1ca0556 100644 --- a/Changelog.md +++ b/Changelog.md @@ -17,6 +17,7 @@ Compiler Features: * SMTChecker: Show unsupported warning for inline assembly blocks. * SMTChecker: Support mod. * SMTChecker: Support ``contract`` type. + * SMTChecker: Support ``this`` as address. * Optimizer: Add rule for shifts by constants larger than 255 for Constantinople. * Optimizer: Add rule to simplify certain ANDs and SHL combinations * Yul: Adds break and continue keywords to for-loop syntax. diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index 5b4c7e0d3..88c1a31b1 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -73,6 +73,8 @@ set(sources codegen/ir/IRGeneratorForStatements.h codegen/ir/IRGenerationContext.cpp codegen/ir/IRGenerationContext.h + formal/EncodingContext.cpp + formal/EncodingContext.h formal/SMTChecker.cpp formal/SMTChecker.h formal/SMTLib2Interface.cpp diff --git a/libsolidity/formal/EncodingContext.cpp b/libsolidity/formal/EncodingContext.cpp new file mode 100644 index 000000000..03f904d7f --- /dev/null +++ b/libsolidity/formal/EncodingContext.cpp @@ -0,0 +1,41 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ + +#include + +#include + +using namespace std; +using namespace dev; +using namespace dev::solidity; +using namespace dev::solidity::smt; + +EncodingContext::EncodingContext(SolverInterface& _solver): + m_solver(_solver), + m_thisAddress(make_unique("this", m_solver)) +{ +} + +void EncodingContext::reset() +{ + m_thisAddress->increaseIndex(); +} + +smt::Expression EncodingContext::thisAddress() +{ + return m_thisAddress->currentValue(); +} diff --git a/libsolidity/formal/EncodingContext.h b/libsolidity/formal/EncodingContext.h new file mode 100644 index 000000000..4170341cb --- /dev/null +++ b/libsolidity/formal/EncodingContext.h @@ -0,0 +1,54 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ + +#pragma once + +#include +#include + +namespace dev +{ +namespace solidity +{ +namespace smt +{ + +/** + * Stores the context of the SMT encoding. + */ +class EncodingContext +{ +public: + EncodingContext(SolverInterface& _solver); + + /// Resets the entire context. + void reset(); + + /// Value of `this` address. + smt::Expression thisAddress(); + +private: + SolverInterface& m_solver; + + /// Symbolic `this` address. + std::unique_ptr m_thisAddress; + +}; + +} +} +} diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index dfc8f7428..997b0df70 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -36,7 +36,8 @@ using namespace dev::solidity; SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map const& _smtlib2Responses): m_interface(make_shared(_smtlib2Responses)), m_errorReporterReference(_errorReporter), - m_errorReporter(m_smtErrors) + m_errorReporter(m_smtErrors), + m_context(*m_interface) { #if defined (HAVE_Z3) || defined (HAVE_CVC4) if (!_smtlib2Responses.empty()) @@ -734,6 +735,11 @@ void SMTChecker::endVisit(Identifier const& _identifier) defineExpr(_identifier, currentValue(*decl)); else if (_identifier.name() == "now") defineGlobalVariable(_identifier.name(), _identifier); + else if (_identifier.name() == "this") + { + defineExpr(_identifier, m_context.thisAddress()); + m_uninterpretedTerms.insert(&_identifier); + } else // TODO: handle MagicVariableDeclaration here m_errorReporter.warning( diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index ad840c771..c6fcc4982 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -18,6 +18,7 @@ #pragma once +#include #include #include #include @@ -316,6 +317,9 @@ private: /// when placeholder is visited. /// Needs to be a stack because of function calls. std::vector m_modifierDepthStack; + + /// Stores the context of the encoding. + smt::EncodingContext m_context; }; } 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 17443e427..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-103): Assertion checker does not yet support the type of this variable. // Warning: (141-144): Assertion checker does not support recursive function calls. diff --git a/test/libsolidity/smtCheckerTests/special/this.sol b/test/libsolidity/smtCheckerTests/special/this.sol new file mode 100644 index 000000000..06fc07404 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/this.sol @@ -0,0 +1,10 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(address a) public view { + assert(a == address(this)); + } +} +// ---- +// Warning: (85-111): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/special/this_state.sol b/test/libsolidity/smtCheckerTests/special/this_state.sol new file mode 100644 index 000000000..48e496d7a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/special/this_state.sol @@ -0,0 +1,11 @@ +pragma experimental SMTChecker; + +contract C +{ + address thisAddr; + function f(address a) public { + require(a == address(this)); + thisAddr = a; + assert(thisAddr == address(this)); + } +}