Merge pull request #6550 from ethereum/smt_this

[SMTChecker] Support this as address

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.

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

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 <http://www.gnu.org/licenses/>.
+*/
+
+#include <libsolidity/formal/EncodingContext.h>
+
+#include <libsolidity/formal/SymbolicTypes.h>
+
+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<SymbolicAddressVariable>("this", m_solver))
+{
+}
+
+void EncodingContext::reset()
+{
+	m_thisAddress->increaseIndex();
+}
+
+smt::Expression EncodingContext::thisAddress()
+{
+	return m_thisAddress->currentValue();
+}

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 <http://www.gnu.org/licenses/>.
+*/
+
+#pragma once
+
+#include <libsolidity/formal/SolverInterface.h>
+#include <libsolidity/formal/SymbolicVariables.h>
+
+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<SymbolicAddressVariable> m_thisAddress;
+
+};
+
+}
+}
+}

libsolidity/formal/SMTChecker.cpp

@@ -36,7 +36,8 @@ using namespace dev::solidity;
 SMTChecker::SMTChecker(ErrorReporter& _errorReporter, map<h256, string> const& _smtlib2Responses):
 	m_interface(make_shared<smt::SMTPortfolio>(_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(

libsolidity/formal/SMTChecker.h

@@ -18,6 +18,7 @@
 #pragma once
 
 
+#include <libsolidity/formal/EncodingContext.h>
 #include <libsolidity/formal/SolverInterface.h>
 #include <libsolidity/formal/SymbolicVariables.h>
 #include <libsolidity/formal/VariableUsage.h>
@@ -316,6 +317,9 @@ private:
 	/// when placeholder is visited.
 	/// Needs to be a stack because of function calls.
 	std::vector<int> m_modifierDepthStack;
+
+	/// Stores the context of the encoding.
+	smt::EncodingContext m_context;
 };
 
 }

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.

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

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));
+	}
+}