Merge pull request #6507 from ethereum/smt_address_members

[SMTChecker] Address members

Changelog.md

@@ -19,6 +19,7 @@ Compiler Features:
  * SMTChecker: Support mod.
  * SMTChecker: Support ``contract`` type.
  * SMTChecker: Support ``this`` as address.
+ * SMTChecker: Support address members.
  * 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/formal/EncodingContext.cpp

@@ -28,14 +28,58 @@ EncodingContext::EncodingContext(SolverInterface& _solver):
 	m_solver(_solver),
 	m_thisAddress(make_unique<SymbolicAddressVariable>("this", m_solver))
 {
+	auto sort = make_shared<smt::ArraySort>(
+		make_shared<smt::Sort>(smt::Kind::Int),
+		make_shared<smt::Sort>(smt::Kind::Int)
+	);
+	m_balances = make_unique<SymbolicVariable>(sort, "balances", m_solver);
 }
 
 void EncodingContext::reset()
 {
 	m_thisAddress->increaseIndex();
+	m_balances->increaseIndex();
 }
 
 smt::Expression EncodingContext::thisAddress()
 {
 	return m_thisAddress->currentValue();
 }
+
+smt::Expression EncodingContext::balance()
+{
+	return balance(m_thisAddress->currentValue());
+}
+
+smt::Expression EncodingContext::balance(smt::Expression _address)
+{
+	return smt::Expression::select(m_balances->currentValue(), move(_address));
+}
+
+void EncodingContext::transfer(smt::Expression _from, smt::Expression _to, smt::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 = smt::Expression::ite(
+		move(_from) == move(_to),
+		m_balances->valueAtIndex(indexBefore),
+		m_balances->valueAtIndex(indexAfter)
+	);
+	m_solver.addAssertion(m_balances->currentValue() == newBalances);
+}
+
+void EncodingContext::addBalance(smt::Expression _address, smt::Expression _value)
+{
+	auto newBalances = smt::Expression::store(
+		m_balances->currentValue(),
+		_address,
+		balance(_address) + move(_value)
+	);
+	m_balances->increaseIndex();
+	m_solver.addAssertion(newBalances == m_balances->currentValue());
+}

libsolidity/formal/EncodingContext.h

@@ -41,12 +41,24 @@ public:
 	/// Value of `this` address.
 	smt::Expression thisAddress();
 
+	/// @returns the symbolic balance of address `this`.
+	smt::Expression balance();
+	/// @returns the symbolic balance of an address.
+	smt::Expression balance(smt::Expression _address);
+	/// Transfer _value from _from to _to.
+	void transfer(smt::Expression _from, smt::Expression _to, smt::Expression _value);
+
 private:
+	/// Adds _value to _account's balance.
+	void addBalance(smt::Expression _account, smt::Expression _value);
+
 	SolverInterface& m_solver;
 
 	/// Symbolic `this` address.
 	std::unique_ptr<SymbolicAddressVariable> m_thisAddress;
 
+	/// Symbolic balances.
+	std::unique_ptr<SymbolicVariable> m_balances;
 };
 
 }

libsolidity/formal/SMTChecker.cpp

@@ -112,6 +112,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 	if (isRootFunction())
 	{
 		m_interface->reset();
+		m_context.reset();
 		m_pathConditions.clear();
 		m_callStack.clear();
 		m_expressions.clear();
@@ -609,6 +610,12 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
 		popCallStack();
 		break;
 	case FunctionType::Kind::External:
+	case FunctionType::Kind::DelegateCall:
+	case FunctionType::Kind::BareCall:
+	case FunctionType::Kind::BareCallCode:
+	case FunctionType::Kind::BareDelegateCall:
+	case FunctionType::Kind::BareStaticCall:
+	case FunctionType::Kind::Creation:
 		m_externalFunctionCallHappened = true;
 		resetStateVariables();
 		resetStorageReferences();
@@ -622,6 +629,22 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::MulMod:
 		abstractFunctionCall(_funCall);
 		break;
+	case FunctionType::Kind::Send:
+	case FunctionType::Kind::Transfer:
+	{
+		auto const& memberAccess = dynamic_cast<MemberAccess const&>(_funCall.expression());
+		auto const& address = memberAccess.expression();
+		auto const& value = args.at(0);
+		solAssert(value, "");
+
+		smt::Expression thisBalance = m_context.balance();
+		setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), *m_interface);
+		checkCondition(thisBalance < expr(*value), _funCall.location(), "Insufficient funds", "address(this).balance", &thisBalance);
+
+		m_context.transfer(m_context.thisAddress(), expr(address), expr(*value));
+		createExpr(_funCall);
+		break;
+	}
 	default:
 		m_errorReporter.warning(
 			_funCall.location(),
@@ -874,6 +897,17 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess)
 		}
 		return false;
 	}
+	else if (exprType->category() == Type::Category::Address)
+	{
+		_memberAccess.expression().accept(*this);
+		if (_memberAccess.memberName() == "balance")
+		{
+			defineExpr(_memberAccess, m_context.balance(expr(_memberAccess.expression())));
+			setSymbolicUnknownValue(*m_expressions[&_memberAccess], *m_interface);
+			m_uninterpretedTerms.insert(&_memberAccess);
+			return false;
+		}
+	}
 	else
 		m_errorReporter.warning(
 			_memberAccess.location(),

libsolidity/formal/SMTChecker.h

@@ -286,6 +286,7 @@ private:
 	std::unordered_map<Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions;
 	std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables;
 	std::unordered_map<std::string, std::shared_ptr<SymbolicVariable>> m_globalContext;
+
 	/// Stores the instances of an Uninterpreted Function applied to arguments.
 	/// These may be direct application of UFs or Array index access.
 	/// Used to retrieve models.

test/libsolidity/smtCheckerTests/types/address_balance.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(address a, address b) public view {
+		uint x = b.balance + 1000 ether;
+		assert(a.balance > b.balance);
+	}
+}
+// ----
+// Warning: (96-102): Unused local variable.
+// Warning: (131-160): Assertion violation happens here
+// Warning: (105-127): Overflow (resulting value larger than 2**256 - 1) happens here

test/libsolidity/smtCheckerTests/types/address_call.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint x;
+	mapping (uint => uint) map;
+	function f(address a, bytes memory data) public {
+		x = 0;
+		map[0] = 0;
+		mapping (uint => uint) storage localMap = map;
+		(bool success, bytes memory ret) = a.call(data);
+		assert(success);
+		assert(x == 0);
+		assert(map[0] == 0);
+		assert(localMap[0] == 0);
+	}
+}
+// ====
+// EVMVersion: >spuriousDragon
+// ----
+// Warning: (224-240): Unused local variable.
+// Warning: (209-256): Assertion checker does not yet support such variable declarations.
+// Warning: (260-275): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/address_delegatecall.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint x;
+	mapping (uint => uint) map;
+	function f(address a, bytes memory data) public {
+		x = 0;
+		map[0] = 0;
+		mapping (uint => uint) storage localMap = map;
+		(bool success, bytes memory ret) = a.delegatecall(data);
+		assert(success);
+		assert(x == 0);
+		assert(map[0] == 0);
+		assert(localMap[0] == 0);
+	}
+}
+// ====
+// EVMVersion: >spuriousDragon
+// ----
+// Warning: (224-240): Unused local variable.
+// Warning: (209-264): Assertion checker does not yet support such variable declarations.
+// Warning: (268-283): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/address_staticcall.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint x;
+	mapping (uint => uint) map;
+	function f(address a, bytes memory data) public {
+		x = 0;
+		map[0] = 0;
+		mapping (uint => uint) storage localMap = map;
+		(bool success, bytes memory ret) = a.staticcall(data);
+		assert(success);
+		assert(x == 0);
+		assert(map[0] == 0);
+		assert(localMap[0] == 0);
+	}
+}
+// ====
+// EVMVersion: >spuriousDragon
+// ----
+// Warning: (224-240): Unused local variable.
+// Warning: (209-262): Assertion checker does not yet support such variable declarations.
+// Warning: (266-281): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/address_transfer.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(address payable a) public {
+		uint x = 100;
+		require(x == a.balance);
+		a.transfer(600);
+		// This fails since a == this is possible.
+		assert(a.balance == 700);
+	}
+}
+// ----
+// Warning: (131-146): Insufficient funds happens here
+// Warning: (131-146): Assertion checker does not yet implement this type.
+// Warning: (195-219): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/address_transfer_2.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint x, address payable a, address payable b) public {
+		require(a != b);
+		require(x == 100);
+		require(x == a.balance);
+		require(a.balance == b.balance);
+		a.transfer(600);
+		b.transfer(100);
+		// Fails since a == this is possible.
+		assert(a.balance > b.balance);
+	}
+}
+// ----
+// Warning: (217-232): Insufficient funds happens here
+// Warning: (217-232): Assertion checker does not yet implement this type.
+// Warning: (236-251): Insufficient funds happens here
+// Warning: (236-251): Assertion checker does not yet implement this type.
+// Warning: (295-324): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(address payable a, address payable b) public {
+		require(a.balance == 0);
+		a.transfer(600);
+		b.transfer(1000);
+		// Fails since a == this is possible.
+		assert(a.balance == 600);
+	}
+}
+// ----
+// Warning: (134-149): Insufficient funds happens here
+// Warning: (134-149): Assertion checker does not yet implement this type.
+// Warning: (153-169): Insufficient funds happens here
+// Warning: (153-169): Assertion checker does not yet implement this type.
+// Warning: (213-237): Assertion violation happens here

test/libsolidity/smtCheckerTestsJSON/multi.json

@@ -3,9 +3,9 @@
 	{
 		"smtlib2responses":
 		{
-			"0x47826ec8b83cfec30171b34f944aed6c33ecd12f02b9ad522ca45317c9bd5f45": "sat\n((|EVALEXPR_0| 1))",
+			"0x47a038dd9021ecb218726ea6bf1f75c215a50b1981bae4341e89c9f2b7ac5db7": "sat\n((|EVALEXPR_0| 1))",
-			"0x734c058efe9d6ec224de3cf2bdfa6c936a1c9c159c040c128d631145b2fed195": "unsat\n",
+			"0xf057b272f2ceb99a2f714cb132960babdeedfb84ff8ffb96106a58bc0c2060cb": "sat\n((|EVALEXPR_0| 0))",
-			"0xa0c072acdbe5181dd56cbad8960cb5bb0b9e97fd598cfd895467bd73bbcca028": "sat\n((|EVALEXPR_0| 0))"
+			"0xf49b9d0eb7b6d2f2ac9e1604288e52ee1a08cda57058e26d7843ed109ca6d7c9": "unsat\n"
 		}
 	}
 }

test/libsolidity/smtCheckerTestsJSON/simple.json

@@ -3,7 +3,7 @@
 	{
 		"smtlib2responses":
 		{
-			"0xa0c072acdbe5181dd56cbad8960cb5bb0b9e97fd598cfd895467bd73bbcca028": "sat\n((|EVALEXPR_0| 0))\n"
+			"0xf057b272f2ceb99a2f714cb132960babdeedfb84ff8ffb96106a58bc0c2060cb": "sat\n((|EVALEXPR_0| 0))\n"
 		}
 	}
 }