Merge pull request #8579 from ethereum/smt_symbolic_state

[SMTChecker] Symbolic state

libsolidity/CMakeLists.txt

@@ -106,6 +106,8 @@ set(sources
 	formal/Sorts.h
 	formal/SSAVariable.cpp
 	formal/SSAVariable.h
+	formal/SymbolicState.cpp
+	formal/SymbolicState.h
 	formal/SymbolicTypes.cpp
 	formal/SymbolicTypes.h
 	formal/SymbolicVariables.cpp

libsolidity/formal/BMC.cpp

@@ -18,6 +18,7 @@
 #include <libsolidity/formal/BMC.h>
 
 #include <libsolidity/formal/SMTPortfolio.h>
+#include <libsolidity/formal/SymbolicState.h>
 #include <libsolidity/formal/SymbolicTypes.h>
 
 #include <boost/algorithm/string/replace.hpp>
@@ -376,7 +377,7 @@ void BMC::endVisit(FunctionCall const& _funCall)
 		SMTEncoder::endVisit(_funCall);
 		auto value = _funCall.arguments().front();
 		solAssert(value, "");
-		smt::Expression thisBalance = m_context.balance();
+		smt::Expression thisBalance = m_context.state().balance();
 
 		addVerificationTarget(
 			VerificationTarget::Type::Balance,

libsolidity/formal/EncodingContext.cpp

@@ -25,13 +25,8 @@ using namespace solidity::util;
 using namespace solidity::frontend::smt;
 
 EncodingContext::EncodingContext():
-	m_thisAddress(make_unique<SymbolicAddressVariable>("this", *this))
+	m_state(*this)
 {
-	auto sort = make_shared<ArraySort>(
-		SortProvider::intSort,
-		SortProvider::intSort
-	);
-	m_balances = make_unique<SymbolicVariable>(sort, "balances", *this);
 }
 
 void EncodingContext::reset()
@@ -39,8 +34,7 @@ void EncodingContext::reset()
 	resetAllVariables();
 	m_expressions.clear();
 	m_globalContext.clear();
-	m_thisAddress->resetIndex();
-	m_balances->resetIndex();
+	m_state.reset();
 	m_assertions.clear();
 }
 
@@ -183,40 +177,6 @@ bool EncodingContext::knownGlobalSymbol(string const& _var) const
 	return m_globalContext.count(_var);
 }
 
-// Blockchain
-
-Expression EncodingContext::thisAddress()
-{
-	return m_thisAddress->currentValue();
-}
-
-Expression EncodingContext::balance()
-{
-	return balance(m_thisAddress->currentValue());
-}
-
-Expression EncodingContext::balance(Expression _address)
-{
-	return Expression::select(m_balances->currentValue(), move(_address));
-}
-
-void EncodingContext::transfer(Expression _from, Expression _to, Expression _value)
-{
-	unsigned indexBefore = m_balances->index();
-	addBalance(_from, 0 - _value);
-	addBalance(_to, move(_value));
-	unsigned indexAfter = m_balances->index();
-	solAssert(indexAfter > indexBefore, "");
-	m_balances->increaseIndex();
-	/// Do not apply the transfer operation if _from == _to.
-	auto newBalances = Expression::ite(
-		move(_from) == move(_to),
-		m_balances->valueAtIndex(indexBefore),
-		m_balances->valueAtIndex(indexAfter)
-	);
-	addAssertion(m_balances->currentValue() == newBalances);
-}
-
 /// Solver.
 
 Expression EncodingContext::assertions()
@@ -248,16 +208,3 @@ void EncodingContext::addAssertion(Expression const& _expr)
 	else
 		m_assertions.back() = _expr && move(m_assertions.back());
 }
-
-/// Private helpers.
-
-void EncodingContext::addBalance(Expression _address, Expression _value)
-{
-	auto newBalances = Expression::store(
-		m_balances->currentValue(),
-		_address,
-		balance(_address) + move(_value)
-	);
-	m_balances->increaseIndex();
-	addAssertion(newBalances == m_balances->currentValue());
-}

libsolidity/formal/EncodingContext.h

@@ -18,6 +18,7 @@
 #pragma once
 
 #include <libsolidity/formal/SolverInterface.h>
+#include <libsolidity/formal/SymbolicState.h>
 #include <libsolidity/formal/SymbolicVariables.h>
 
 #include <unordered_map>
@@ -121,18 +122,6 @@ public:
 	bool knownGlobalSymbol(std::string const& _var) const;
 	//@}
 
-	/// Blockchain.
-	//@{
-	/// Value of `this` address.
-	Expression thisAddress();
-	/// @returns the symbolic balance of address `this`.
-	Expression balance();
-	/// @returns the symbolic balance of an address.
-	Expression balance(Expression _address);
-	/// Transfer _value from _from to _to.
-	void transfer(Expression _from, Expression _to, Expression _value);
-	//@}
-
 	/// Solver.
 	//@{
 	/// @returns conjunction of all added assertions.
@@ -148,10 +137,9 @@ public:
 	}
 	//@}
 
-private:
-	/// Adds _value to _account's balance.
-	void addBalance(Expression _account, Expression _value);
+	SymbolicState& state() { return m_state; }
 
+private:
 	/// Symbolic expressions.
 	//{@
 	/// Symbolic variables.
@@ -164,11 +152,8 @@ private:
 	/// variables and functions.
 	std::unordered_map<std::string, std::shared_ptr<smt::SymbolicVariable>> m_globalContext;
 
-	/// Symbolic `this` address.
-	std::unique_ptr<SymbolicAddressVariable> m_thisAddress;
-
-	/// Symbolic balances.
-	std::unique_ptr<SymbolicVariable> m_balances;
+	/// Symbolic representation of the blockchain state.
+	SymbolicState m_state;
 	//@}
 
 	/// Solver related.

libsolidity/formal/SMTEncoder.cpp

@@ -19,6 +19,7 @@
 
 #include <libsolidity/ast/TypeProvider.h>
 #include <libsolidity/formal/SMTPortfolio.h>
+#include <libsolidity/formal/SymbolicState.h>
 #include <libsolidity/formal/SymbolicTypes.h>
 
 #include <boost/range/adaptors.hpp>
@@ -619,10 +620,10 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 		auto const& value = args.front();
 		solAssert(value, "");
 
-		smt::Expression thisBalance = m_context.balance();
+		smt::Expression thisBalance = m_context.state().balance();
 		setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), m_context);
 
-		m_context.transfer(m_context.thisAddress(), expr(address), expr(*value));
+		m_context.state().transfer(m_context.state().thisAddress(), expr(address), expr(*value));
 		break;
 	}
 	default:
@@ -711,7 +712,7 @@ void SMTEncoder::endVisit(Identifier const& _identifier)
 		defineGlobalVariable(_identifier.name(), _identifier);
 	else if (_identifier.name() == "this")
 	{
-		defineExpr(_identifier, m_context.thisAddress());
+		defineExpr(_identifier, m_context.state().thisAddress());
 		m_uninterpretedTerms.insert(&_identifier);
 	}
 	else
@@ -858,7 +859,7 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 		_memberAccess.expression().accept(*this);
 		if (_memberAccess.memberName() == "balance")
 		{
-			defineExpr(_memberAccess, m_context.balance(expr(_memberAccess.expression())));
+			defineExpr(_memberAccess, m_context.state().balance(expr(_memberAccess.expression())));
 			setSymbolicUnknownValue(*m_context.expression(_memberAccess), m_context);
 			m_uninterpretedTerms.insert(&_memberAccess);
 			return false;

libsolidity/formal/SymbolicState.cpp

@@ -0,0 +1,82 @@
+/*
+	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/SymbolicState.h>
+
+#include <libsolidity/formal/EncodingContext.h>
+
+using namespace std;
+using namespace solidity::frontend::smt;
+
+SymbolicState::SymbolicState(EncodingContext& _context):
+	m_context(_context)
+{
+}
+
+void SymbolicState::reset()
+{
+	m_thisAddress.resetIndex();
+	m_balances.resetIndex();
+}
+
+// Blockchain
+
+Expression SymbolicState::thisAddress()
+{
+	return m_thisAddress.currentValue();
+}
+
+Expression SymbolicState::balance()
+{
+	return balance(m_thisAddress.currentValue());
+}
+
+Expression SymbolicState::balance(Expression _address)
+{
+	return Expression::select(m_balances.currentValue(), move(_address));
+}
+
+void SymbolicState::transfer(Expression _from, Expression _to, Expression _value)
+{
+	unsigned indexBefore = m_balances.index();
+	addBalance(_from, 0 - _value);
+	addBalance(_to, move(_value));
+	unsigned indexAfter = m_balances.index();
+	solAssert(indexAfter > indexBefore, "");
+	m_balances.increaseIndex();
+	/// Do not apply the transfer operation if _from == _to.
+	auto newBalances = Expression::ite(
+		move(_from) == move(_to),
+		m_balances.valueAtIndex(indexBefore),
+		m_balances.valueAtIndex(indexAfter)
+	);
+	m_context.addAssertion(m_balances.currentValue() == newBalances);
+}
+
+/// Private helpers.
+
+void SymbolicState::addBalance(Expression _address, Expression _value)
+{
+	auto newBalances = Expression::store(
+		m_balances.currentValue(),
+		_address,
+		balance(_address) + move(_value)
+	);
+	m_balances.increaseIndex();
+	m_context.addAssertion(newBalances == m_balances.currentValue());
+}
+

libsolidity/formal/SymbolicState.h

@@ -0,0 +1,71 @@
+/*
+	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/Sorts.h>
+#include <libsolidity/formal/SolverInterface.h>
+#include <libsolidity/formal/SymbolicVariables.h>
+
+namespace solidity::frontend::smt
+{
+
+class EncodingContext;
+
+/**
+ * Symbolic representation of the blockchain state.
+ */
+class SymbolicState
+{
+public:
+	SymbolicState(EncodingContext& _context);
+
+	void reset();
+
+	/// Blockchain.
+	//@{
+	/// Value of `this` address.
+	Expression thisAddress();
+	/// @returns the symbolic balance of address `this`.
+	Expression balance();
+	/// @returns the symbolic balance of an address.
+	Expression balance(Expression _address);
+	/// Transfer _value from _from to _to.
+	void transfer(Expression _from, Expression _to, Expression _value);
+	//@}
+
+private:
+	/// Adds _value to _account's balance.
+	void addBalance(Expression _account, Expression _value);
+
+	EncodingContext& m_context;
+
+	/// Symbolic `this` address.
+	SymbolicAddressVariable m_thisAddress{
+		"this",
+		m_context
+	};
+
+	/// Symbolic balances.
+	SymbolicArrayVariable m_balances{
+		std::make_shared<ArraySort>(SortProvider::intSort, SortProvider::intSort),
+		"balances",
+		m_context
+	};
+};
+
+}