Merge pull request #7321 from ethereum/smt_const_array

[SMTChecker] Zero-initialize arrays

test/libsolidity/SMTChecker.cpp

@@ -212,7 +212,7 @@ BOOST_AUTO_TEST_CASE(compound_assignment_division)
 			uint[] array;
 			function f(uint x, uint p) public {
 				require(x == 2);
-				require(array[p] == 10);
+				array[p] = 10;
 				array[p] /= array[p] / x;
 				assert(array[p] == x);
 				assert(array[p] == 0);
@@ -225,7 +225,7 @@ BOOST_AUTO_TEST_CASE(compound_assignment_division)
 			mapping (uint => uint) map;
 			function f(uint x, uint p) public {
 				require(x == 2);
-				require(map[p] == 10);
+				map[p] = 10;
 				map[p] /= map[p] / x;
 				assert(map[p] == x);
 				assert(map[p] == 0);

test/libsolidity/smtCheckerTests/operators/compound_add_array_index.sol

@@ -5,11 +5,11 @@ contract C
 	uint[] array;
 	function f(uint x, uint p) public {
 		require(x < 100);
-		require(array[p] == 100);
+		array[p] = 100;
 		array[p] += array[p] + x;
 		assert(array[p] < 300);
 		assert(array[p] < 110);
 	}
 }
 // ----
-// Warning: (202-224): Assertion violation happens here
+// Warning: (192-214): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_add_mapping.sol

@@ -5,11 +5,11 @@ contract C
 	mapping (uint => uint) map;
 	function f(uint x, uint p) public {
 		require(x < 100);
-		require(map[p] == 100);
+		map[p] = 100;
 		map[p] += map[p] + x;
 		assert(map[p] < 300);
 		assert(map[p] < 110);
 	}
 }
 // ----
-// Warning: (208-228): Assertion violation happens here
+// Warning: (198-218): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_mul_array_index.sol

@@ -5,11 +5,11 @@ contract C
 	uint[] array;
 	function f(uint x, uint p) public {
 		require(x < 10);
-		require(array[p] == 10);
+		array[p] = 10;
 		array[p] *= array[p] + x;
 		assert(array[p] <= 190);
 		assert(array[p] < 50);
 	}
 }
 // ----
-// Warning: (201-222): Assertion violation happens here
+// Warning: (191-212): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_mul_mapping.sol

@@ -5,11 +5,11 @@ contract C
 	mapping (uint => uint) map;
 	function f(uint x, uint p) public {
 		require(x < 10);
-		require(map[p] == 10);
+		map[p] = 10;
 		map[p] *= map[p] + x;
 		assert(map[p] <= 190);
 		assert(map[p] < 50);
 	}
 }
 // ----
-// Warning: (207-226): Assertion violation happens here
+// Warning: (197-216): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_sub_array_index.sol

@@ -5,11 +5,11 @@ contract C
 	uint[] array;
 	function f(uint x, uint p) public {
 		require(x < 100);
-		require(array[p] == 200);
+		array[p] = 200;
 		array[p] -= array[p] - x;
 		assert(array[p] >= 0);
 		assert(array[p] < 90);
 	}
 }
 // ----
-// Warning: (201-222): Assertion violation happens here
+// Warning: (191-212): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/compound_sub_mapping.sol

@@ -5,11 +5,11 @@ contract C
 	mapping (uint => uint) map;
 	function f(uint x, uint p) public {
 		require(x < 100);
-		require(map[p] == 200);
+		map[p] = 200;
 		map[p] -= map[p] - x;
 		assert(map[p] >= 0);
 		assert(map[p] < 90);
 	}
 }
 // ----
-// Warning: (207-226): Assertion violation happens here
+// Warning: (197-216): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/delete_array.sol

@@ -10,12 +10,9 @@ contract C
 			delete a;
 		else
 			delete a[2];
-		// Assertion fails as false positive because
-		// setZeroValue for arrays needs \forall i . a[i] = 0
-		// which is still unimplemented.
 		assert(a[2] == 0);
+		assert(a[1] == 0);
 	}
 }
 // ----
 // Warning: (118-119): Condition is always true.
-// Warning: (297-314): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/delete_array_2d.sol

@@ -6,10 +6,6 @@ contract C
 	function f() public {
 		require(a[2][3] == 4);
 		delete a;
-		// Fails as false positive.
-		// setZeroValue needs forall for arrays.
 		assert(a[2][3] == 0);
 	}
 }
-// ----
-// Warning: (194-214): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol

@@ -9,11 +9,7 @@ contract C
 			delete a;
 		else
 			delete a[2];
-		// Fails as false positive since
-		// setZeroValue for arrays needs forall
-		// which is unimplemented.
 		assert(a[2][3] == 0);
+		assert(a[1][1] == 0);
 	}
 }
-// ----
-// Warning: (266-286): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/delete_function.sol

@@ -16,12 +16,9 @@ contract C
 			g();
 		else
 			h();
-		// Assertion fails as false positive because
-		// setZeroValue for arrays needs \forall i . a[i] = 0
-		// which is still unimplemented.
 		assert(a[2] == 0);
+		assert(a[1] == 0);
 	}
 }
 // ----
 // Warning: (201-202): Condition is always true.
-// Warning: (367-384): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_dynamic_2_fail.sol

@@ -4,10 +4,11 @@ contract C
 {
 	uint[][] array;
 	function f(uint x, uint y, uint z, uint t) public view {
-		require(array[x][y] == 200);
+		// TODO change to = 200 when 2d assignments are supported.
+		require(array[x][y] < 200);
 		require(x == z && y == t);
 		assert(array[z][t] > 300);
 	}
 }
 // ----
-// Warning: (183-208): Assertion violation happens here
+// Warning: (243-268): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_dynamic_3_fail.sol

@@ -4,10 +4,11 @@ contract C
 {
 	uint[][][] array;
 	function f(uint x, uint y, uint z, uint t, uint w, uint v) public view {
-		require(array[x][y][z] == 200);
+		// TODO change to = 200 when 3d assignments are supported.
+		require(array[x][y][z] < 200);
 		require(x == t && y == w && z == v);
 		assert(array[t][w][v] > 300);
 	}
 }
 // ----
-// Warning: (214-242): Assertion violation happens here
+// Warning: (274-302): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_static_2_fail.sol

@@ -4,10 +4,10 @@ contract C
 {
 	uint[10][20] array;
 	function f(uint x, uint y, uint z, uint t) public view {
-		require(array[x][y] == 200);
+		require(array[x][y] < 200);
 		require(x == z && y == t);
 		assert(array[z][t] > 300);
 	}
 }
 // ----
-// Warning: (187-212): Assertion violation happens here
+// Warning: (186-211): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/array_static_3_fail.sol

@@ -4,10 +4,11 @@ contract C
 {
 	uint[10][20][30] array;
 	function f(uint x, uint y, uint z, uint t, uint w, uint v) public view {
-		require(array[x][y][z] == 200);
+		// TODO change to = 200 when 3d assignments are supported.
+		require(array[x][y][z] < 200);
 		require(x == t && y == w && z == v);
 		assert(array[t][w][v] > 300);
 	}
 }
 // ----
-// Warning: (220-248): Assertion violation happens here
+// Warning: (280-308): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/mapping_4.sol

@@ -9,4 +9,3 @@ contract C
 	}
 }
 // ----
-// Warning: (125-144): Assertion violation happens here