Merge pull request #7154 from ethereum/smt_erase_only_required

Erase storage pointer knowledge only when necessary

Changelog.md

@@ -13,6 +13,7 @@ Compiler Features:
  * Metadata: Update the swarm hash, changes ``bzzr0`` to ``bzzr1`` and urls to use ``bzz-raw://``.
  * Standard JSON Interface: Compile only selected sources and contracts.
  * Standard JSON Interface: Provide secondary error locations (e.g. the source position of other conflicting declarations).
+ * SMTChecker: Do not erase knowledge about storage pointers if another storage pointer is assigned.
 
 
 

libsolidity/formal/SMTEncoder.cpp

@@ -759,6 +759,11 @@ void SMTEncoder::arrayIndexAssignment(Expression const& _expr, smt::Expression c
 			m_context.resetVariables([&](VariableDeclaration const& _var) {
 				if (_var == *varDecl)
 					return false;
+
+				// If both are state variables no need to clear knowledge.
+				if (_var.isStateVariable() && varDecl->isStateVariable())
+					return false;
+
 				TypePointer prefix = _var.type();
 				TypePointer originalType = typeWithoutPointer(varDecl->type());
 				while (

test/libsolidity/smtCheckerTests/types/array_aliasing_storage_5.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] b;
+	uint[] d;
+	function f(uint[] storage a, uint[] memory c) internal {
+		require(d[0] == 42);
+		require(c[0] == 42);
+		require(a[0] == 2);
+		b[0] = 1;
+		// Erasing knowledge about storage variables should not
+		// erase knowledge about memory references.
+		assert(c[0] == 42);
+		// Should not fail since b == d is not possible.
+		assert(d[0] == 42);
+		// Fails because b == a is possible.
+		assert(a[0] == 2);
+		assert(b[0] == 1);
+	}
+}
+// ----
+// Warning: (446-463): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_1.sol

@@ -13,7 +13,7 @@ contract C
 		map[0] = 2;
 		// Should fail since map == severalMaps[0] is possible.
 		assert(severalMaps[0][0] == 42);
-		// Should not fail since knowledge is erase only for mapping (uint => uint).
+		// Should not fail since knowledge is erased only for mapping (uint => uint).
 		assert(severalMaps8[0][0] == 42);
 		// Should fail since map == severalMaps3d[0][0] is possible.
 		assert(severalMaps3d[0][0][0] == 42);
@@ -21,4 +21,4 @@ contract C
 }
 // ----
 // Warning: (451-482): Assertion violation happens here
-// Warning: (664-700): Assertion violation happens here
+// Warning: (665-701): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol

@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => uint) singleMap;
+	mapping (uint => uint)[] severalMaps;
+	mapping (uint => uint8)[] severalMaps8;
+	mapping (uint => uint)[][] severalMaps3d;
+	function f(mapping (uint => uint) storage map) internal {
+		map[0] = 42;
+		require(severalMaps[0][0] == 42);
+		require(severalMaps8[0][0] == 42);
+		require(severalMaps3d[0][0][0] == 42);
+		singleMap[0] = 2;
+		// Should not fail since singleMap == severalMaps[0] is not possible.
+		assert(severalMaps[0][0] == 42);
+		// Should not fail since knowledge is erased only for mapping (uint => uint).
+		assert(severalMaps8[0][0] == 42);
+		// Should not fail since singleMap == severalMaps3d[0][0] is not possible.
+		assert(severalMaps3d[0][0][0] == 42);
+		// Should fail since singleMap == map is possible.
+		assert(map[0] == 42);
+	}
+}
+// ----
+// Warning: (807-827): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_static_aliasing_memory_5.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint[2] memory a, uint[2] memory b, uint[2] memory c) internal pure {
+		require(c[0] == 42);
+		require(a[0] == 2);
+		b[0] = 1;
+		// Should fail since b == c is possible.
+		assert(c[0] == 42);
+		// Should fail since b == a is possible.
+		assert(a[0] == 2);
+		assert(b[0] == 1);
+	}
+}
+// ----
+// Warning: (230-248): Assertion violation happens here
+// Warning: (295-312): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_static_aliasing_storage_5.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[2] b;
+	function f(uint[2] storage a, uint[2] memory c) internal {
+		require(c[0] == 42);
+		require(a[0] == 2);
+		b[0] = 1;
+		// Erasing knowledge about storage variables should not
+		// erase knowledge about memory references.
+		assert(c[0] == 42);
+		// Fails because b == a is possible.
+		assert(a[0] == 2);
+		assert(b[0] == 1);
+	}
+}
+// ----
+// Warning: (342-359): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => uint) singleMap;
+	mapping (uint => uint)[2] severalMaps;
+	mapping (uint => uint8)[2] severalMaps8;
+	mapping (uint => uint)[2][2] severalMaps3d;
+	function f(mapping (uint => uint) storage map) internal {
+		require(severalMaps[0][0] == 42);
+		require(severalMaps8[0][0] == 42);
+		require(severalMaps3d[0][0][0] == 42);
+		map[0] = 2;
+		// Should fail since map == severalMaps[0] is possible.
+		assert(severalMaps[0][0] == 42);
+		// Should not fail since knowledge is erased only for mapping (uint => uint).
+		assert(severalMaps8[0][0] == 42);
+		// Should fail since map == severalMaps3d[0][0] is possible.
+		assert(severalMaps3d[0][0][0] == 42);
+	}
+}
+// ----
+// Warning: (455-486): Assertion violation happens here
+// Warning: (669-705): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol

@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	mapping (uint => uint) singleMap;
+	mapping (uint => uint)[2] severalMaps;
+	mapping (uint => uint8)[2] severalMaps8;
+	mapping (uint => uint)[2][2] severalMaps3d;
+	function f(mapping (uint => uint) storage map) internal {
+		map[0] = 42;
+		require(severalMaps[0][0] == 42);
+		require(severalMaps8[0][0] == 42);
+		require(severalMaps3d[0][0][0] == 42);
+		singleMap[0] = 2;
+		// Should not fail since singleMap == severalMaps[0] is not possible.
+		assert(severalMaps[0][0] == 42);
+		// Should not fail since knowledge is erased only for mapping (uint => uint).
+		assert(severalMaps8[0][0] == 42);
+		// Should not fail since singleMap == severalMaps3d[0][0] is not possible.
+		assert(severalMaps3d[0][0][0] == 42);
+		// Should fail since singleMap == map is possible.
+		assert(map[0] == 42);
+	}
+}
+// ----
+// Warning: (811-831): Assertion violation happens here