Merge pull request #7152 from ethereum/smt_fix_pointer_cleanup

[SMTChecker] Erase pointer knowledge properly inside loops

Changelog.md

@@ -19,6 +19,7 @@ Compiler Features:
 
 Bugfixes:
  * SMTChecker: Fix internal error when inlining functions that contain tuple expressions.
+ * SMTChecker: Fix pointer knowledge erasing in loops.
  * View/Pure Checker: Properly detect state variable access through base class.
  * Yul analyzer: Check availability of data objects already in analysis phase.
  * Yul Optimizer: Fix an issue where memory-accessing code was removed even though ``msize`` was used in the program.

libsolidity/formal/SMTEncoder.cpp

@@ -1173,6 +1173,21 @@ void SMTEncoder::mergeVariables(set<VariableDeclaration const*> const& _variable
 		return var1->id() < var2->id();
 	};
 	set<VariableDeclaration const*, decltype(cmp)> sortedVars(begin(_variables), end(_variables), cmp);
+
+	/// Knowledge about references is erased if a reference is assigned,
+	/// so those also need their SSA's merged.
+	/// This does not cause scope harm since the symbolic variables
+	/// are kept alive.
+	for (auto const& var: _indicesEndTrue)
+	{
+		solAssert(_indicesEndFalse.count(var.first), "");
+		if (
+			_indicesEndFalse.at(var.first) != var.second &&
+			!sortedVars.count(var.first)
+		)
+			sortedVars.insert(var.first);
+	}
+
 	for (auto const* decl: sortedVars)
 	{
 		solAssert(_indicesEndTrue.count(decl) && _indicesEndFalse.count(decl), "");

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_memory.sol

@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+contract LoopFor2 {
+	function testUnboundedForLoop(uint n, uint[] memory b, uint[] memory c) public pure {
+		b[0] = 900;
+		uint[] memory a = b;
+		require(n > 0 && n < 100);
+		for (uint i = 0; i < n; i += 1) {
+			b[i] = i + 1;
+			c[i] = b[i];
+		}
+		assert(b[0] == c[0]);
+		assert(a[0] == 900);
+		assert(b[0] == 900);
+	}
+}
+// ----
+// Warning: (281-301): Assertion violation happens here
+// Warning: (305-324): Assertion violation happens here
+// Warning: (328-347): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_memory_storage.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract LoopFor2 {
+	uint[] a;
+
+	function testUnboundedForLoop(uint n, uint[] memory b, uint[] memory c) public {
+		b[0] = 900;
+		a = b;
+		require(n > 0 && n < 100);
+		for (uint i = 0; i < n; i += 1) {
+			b[i] = i + 1;
+			c[i] = b[i];
+		}
+		assert(b[0] == c[0]);
+		assert(a[0] == 900);
+		assert(b[0] == 900);
+	}
+}
+// ----
+// Warning: (274-294): Assertion violation happens here
+// Warning: (321-340): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract LoopFor2 {
+	uint[] b;
+	uint[] c;
+
+	function testUnboundedForLoop(uint n) public {
+		b[0] = 900;
+		uint[] memory a = b;
+		require(n > 0 && n < 100);
+		for (uint i = 0; i < n; i += 1) {
+			b[i] = i + 1;
+			c[i] = b[i];
+		}
+		assert(b[0] == c[0]);
+		assert(a[0] == 900);
+		assert(b[0] == 900);
+	}
+}
+// ----
+// Warning: (265-285): Assertion violation happens here
+// Warning: (312-331): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+
+contract LoopFor2 {
+	uint[] b;
+	uint[] c;
+
+	function testUnboundedForLoop(uint n) public {
+		b[0] = 900;
+		uint[] storage a = b;
+		require(n > 0 && n < 100);
+		for (uint i = 0; i < n; i += 1) {
+			b[i] = i + 1;
+			c[i] = b[i];
+		}
+		assert(b[0] == c[0]);
+		assert(a[0] == 900);
+		assert(b[0] == 900);
+	}
+}
+// ----
+// Warning: (266-286): Assertion violation happens here
+// Warning: (290-309): Assertion violation happens here
+// Warning: (313-332): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract LoopFor2 {
+	function testUnboundedForLoop(uint n, uint[] memory b, uint[] memory c) public pure {
+		b[0] = 900;
+		uint[] memory a = b;
+		require(n > 0 && n < 100);
+		uint i;
+		while (i < n) {
+			b[i] = i + 1;
+			c[i] = b[i];
+			++i;
+		}
+		assert(b[0] == c[0]);
+		assert(a[0] == 900);
+		assert(b[0] == 900);
+	}
+}
+// ----
+// Warning: (281-301): Assertion violation happens here
+// Warning: (305-324): Assertion violation happens here
+// Warning: (328-347): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+
+contract LoopFor2 {
+	uint[] a;
+
+	function testUnboundedForLoop(uint n, uint[] memory b, uint[] memory c) public {
+		b[0] = 900;
+		a = b;
+		require(n > 0 && n < 100);
+		uint i;
+		while (i < n) {
+			b[i] = i + 1;
+			c[i] = b[i];
+			++i;
+		}
+		assert(b[0] == c[0]);
+		assert(a[0] == 900);
+		assert(b[0] == 900);
+	}
+}
+// ----
+// Warning: (274-294): Assertion violation happens here
+// Warning: (321-340): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_memory.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+
+contract LoopFor2 {
+	uint[] b;
+	uint[] c;
+
+	function testUnboundedForLoop(uint n) public {
+		b[0] = 900;
+		uint[] memory a = b;
+		require(n > 0 && n < 100);
+		uint i;
+		while (i < n) {
+			b[i] = i + 1;
+			c[i] = b[i];
+			++i;
+		}
+		assert(b[0] == c[0]);
+		assert(a[0] == 900);
+		assert(b[0] == 900);
+	}
+}
+// ----
+// Warning: (265-285): Assertion violation happens here
+// Warning: (312-331): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol

@@ -0,0 +1,25 @@
+pragma experimental SMTChecker;
+
+contract LoopFor2 {
+	uint[] b;
+	uint[] c;
+
+	function testUnboundedForLoop(uint n) public {
+		b[0] = 900;
+		uint[] storage a = b;
+		require(n > 0 && n < 100);
+		uint i;
+		while (i < n) {
+			b[i] = i + 1;
+			c[i] = b[i];
+			++i;
+		}
+		assert(b[0] == c[0]);
+		assert(a[0] == 900);
+		assert(b[0] == 900);
+	}
+}
+// ----
+// Warning: (266-286): Assertion violation happens here
+// Warning: (290-309): Assertion violation happens here
+// Warning: (313-332): Assertion violation happens here