Erase balances when delegatecall is seen

Author: Leo Alt

libsolidity/formal/BMC.cpp

@@ -591,6 +591,7 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
 	{
 		m_externalFunctionCallHappened = true;
 		resetStorageVariables();
+		resetBalances();
 	}
 }
 

libsolidity/formal/CHC.cpp

@@ -995,6 +995,7 @@ void CHC::resetContractAnalysis()
 void CHC::eraseKnowledge()
 {
 	resetStorageVariables();
+	resetBalances();
 }
 
 void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)

libsolidity/formal/SMTEncoder.cpp

@@ -2281,6 +2281,13 @@ void SMTEncoder::resetStorageVariables()
 	});
 }
 
+void SMTEncoder::resetBalances()
+{
+	// TODO this should be changed to `balances` only
+	// when `state` gets more members.
+	state().newState();
+}
+
 void SMTEncoder::resetReferences(VariableDeclaration const& _varDecl)
 {
 	m_context.resetVariables([&](VariableDeclaration const& _var) {

libsolidity/formal/SMTEncoder.h

@@ -303,6 +303,7 @@ class SMTEncoder: public ASTConstVisitor
 	void resetStateVariables();
 	void resetStorageVariables();
 	void resetMemoryVariables();
+	void resetBalances();
 	/// Resets all references/pointers that have the same type or have
 	/// a subexpression of the same type as _varDecl.
 	void resetReferences(VariableDeclaration const& _varDecl);

test/libsolidity/smtCheckerTests/blockchain_state/free_function_1.sol

@@ -0,0 +1,15 @@
+function l(address payable a) {}
+
+contract C {
+	uint x;
+	function f(address payable a) public payable {
+		require(msg.value > 1);
+		uint b1 = address(this).balance;
+		l(a);
+		uint b2 = address(this).balance;
+		assert(b1 == b2); // should hold
+		assert(x == 0); // should hold
+	}
+}
+// ====
+// SMTEngine: all

test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol

@@ -0,0 +1,24 @@
+function l(address payable a) {
+	a.transfer(1);
+}
+
+contract C {
+	uint x;
+	function f(address payable a) public payable {
+		require(msg.value > 1);
+		uint b1 = address(this).balance;
+		l(a);
+		uint b2 = address(this).balance;
+		assert(b1 == b2); // should fail
+		assert(b1 == b2 - 1); // should hold but we don't keep track of balances with msg.value yet
+		assert(x == 0); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 6328: (227-243): CHC: Assertion violation happens here.
+// Warning 3944: (275-281): CHC: Underflow (resulting value less than 0) happens here.
+// Warning 6328: (262-282): CHC: Assertion violation happens here.
+// Warning 1236: (33-46): BMC: Insufficient funds happens here.

test/libsolidity/smtCheckerTests/blockchain_state/library_internal_1.sol

@@ -0,0 +1,18 @@
+library L {
+	function l(address payable a) internal {}
+}
+
+contract C {
+	using L for address payable;
+	uint x;
+	function f(address payable a) public payable {
+		require(msg.value > 1);
+		uint b1 = address(this).balance;
+		a.l();
+		uint b2 = address(this).balance;
+		assert(b1 == b2); // should hold
+		assert(x == 0); // should hold
+	}
+}
+// ====
+// SMTEngine: all

test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol

@@ -0,0 +1,27 @@
+library L {
+	function l(address payable a) internal {
+		a.transfer(1);
+	}
+}
+
+contract C {
+	using L for address payable;
+	uint x;
+	function f(address payable a) public payable {
+		require(msg.value > 1);
+		uint b1 = address(this).balance;
+		a.l();
+		uint b2 = address(this).balance;
+		assert(b1 == b2); // should fail
+		assert(b1 == b2 - 1); // should hold but we don't keep track of balances with msg.value yet
+		assert(x == 0); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (284-300): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 21238\nb1 = 8856\nb2 = 8855\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(21238){ value: 11799 }\n    L.l(21238){ value: 11799 } -- internal call
+// Warning 3944: (332-338): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\nx = 0\na = 38\nb1 = 1\nb2 = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(38){ value: 21240 }\n    L.l(38){ value: 21240 } -- internal call
+// Warning 6328: (319-339): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 21238\nb1 = 40\nb2 = 39\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(21238){ value: 8857 }\n    L.l(21238){ value: 8857 } -- internal call
+// Warning 1236: (56-69): BMC: Insufficient funds happens here.
+// Warning 1236: (56-69): BMC: Insufficient funds happens here.

test/libsolidity/smtCheckerTests/blockchain_state/library_public_1.sol

@@ -0,0 +1,23 @@
+library L {
+	function l(address payable a) public {}
+}
+
+contract C {
+	using L for address payable;
+	uint x;
+	function f(address payable a) public payable {
+		require(msg.value > 1);
+		uint b1 = address(this).balance;
+		a.l();
+		uint b2 = address(this).balance;
+		assert(b1 == b2); // should fail because the called library can transfer with `this`s balance
+		assert(x == 0); // should fail because of `delegatecall`
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 4588: (219-224): Assertion checker does not yet implement this type of function call.
+// Warning 6328: (263-279): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\nb1 = 7720\nb2 = 7719\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0){ value: 5855 }
+// Warning 6328: (359-373): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\nb1 = 39\nb2 = 38\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0){ value: 21240 }
+// Warning 4588: (219-224): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/blockchain_state/library_public_2.sol

@@ -0,0 +1,27 @@
+library L {
+	function l(address payable a) public {
+		a.transfer(1);
+	}
+}
+
+contract C {
+	using L for address payable;
+	uint x;
+	function f(address payable a) public payable {
+		require(msg.value > 1);
+		uint b1 = address(this).balance;
+		a.l();
+		uint b2 = address(this).balance;
+		assert(b1 == b2); // should fail
+		assert(x == 0); // should fail because of `delegatecall`
+	}
+}
+// ====
+// SMTEngine: all
+// SMTIgnoreCex: yes
+// ----
+// Warning 4588: (238-243): Assertion checker does not yet implement this type of function call.
+// Warning 6328: (282-298): CHC: Assertion violation happens here.
+// Warning 6328: (317-331): CHC: Assertion violation happens here.
+// Warning 1236: (54-67): BMC: Insufficient funds happens here.
+// Warning 4588: (238-243): Assertion checker does not yet implement this type of function call.