Merge pull request #15256 from ethereum/smt-more-test-simplification

SMTChecker: Further test simplifications

Author: blishko

test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol

@@ -1,6 +1,6 @@
 contract D {
 	uint x;
-	function inc() public { ++x; }
+	function inc() public { require(x < 5); ++x; }
 	function f() public view returns (uint) { return x; }
 }
 
@@ -18,9 +18,7 @@ contract C {
 // ====
 // SMTEngine: all
 // SMTExtCalls: trusted
+// SMTTargets: assert
 // ----
-// Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
-// Warning 6328: (304-322): CHC: Assertion violation might happen here.
+// Warning 6328: (320-338): CHC: Assertion violation happens here.
 // Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
-// Warning 2661: (47-50): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 4661: (304-322): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect_trusted.sol

@@ -1,23 +1,17 @@
 contract Other {
-	C c;
-	constructor(C _c) {
-		c = _c;
-	}
-	function h() public {
+	function h(C c) public {
 		c.setOwner(address(0));
 	}
 }
 
 contract State {
 	uint x;
 	Other o;
-	C c;
-	constructor(C _c) {
-		c = _c;
-		o = new Other(_c);
+	constructor() {
+		o = new Other();
 	}
-	function f() public returns (uint) {
-		o.h();
+	function f(C c) public returns (uint) {
+		o.h(c);
 		return c.g();
 	}
 }
@@ -29,7 +23,7 @@ contract C {
 
 	constructor() {
 		owner = msg.sender;
-		s = new State(this);
+		s = new State();
 	}
 
 	function setOwner(address _owner) public {
@@ -38,7 +32,7 @@ contract C {
 
 	function f() public {
 		address prevOwner = owner;
-		uint z = s.f();
+		uint z = s.f(this);
 		assert(z == y); // should hold
 		assert(prevOwner == owner); // should not hold because of reentrancy
 	}
@@ -52,5 +46,5 @@ contract C {
 // SMTEngine: chc
 // SMTExtCalls: trusted
 // ----
-// Warning 6328: (531-545): CHC: Assertion violation might happen here.
-// Warning 6328: (564-590): CHC: Assertion violation happens here.
+// Warning 6328: (509-535): CHC: Assertion violation happens here.
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/external_calls/external_inc.sol

@@ -7,18 +7,18 @@ contract C {
 	D d;
 
 	function inc() public {
+		require(x < 10);
 		++x;
 	}
 
 	function f() public {
 		d.d();
-		assert(x < 10);
+		assert(x < 5);
 	}
 }
 // ====
 // SMTEngine: all
 // SMTIgnoreCex: yes
 // ----
-// Warning 4984: (113-116): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
-// Warning 6328: (156-170): CHC: Assertion violation happens here.
-// Warning 2661: (113-116): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 6328: (175-188): CHC: Assertion violation happens here.\nCounterexample:\nx = 5, d = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.inc()\nState: x = 1, d = 0\nC.inc()\nState: x = 2, d = 0\nC.inc()\nState: x = 3, d = 0\nC.inc()\nState: x = 4, d = 0\nC.f()\n    d.d() -- untrusted external call, synthesized as:\n        C.inc() -- reentrant call
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/external_calls/external_safe.sol

@@ -6,16 +6,15 @@ contract C {
 	uint x;
 	D d;
 	function f() public {
-		if (x < 10)
+		if (x < 5)
 			++x;
 	}
 	function g() public {
 		d.d();
-		assert(x < 11);
+		assert(x < 6);
 	}
 }
 // ====
 // SMTEngine: all
-// SMTIgnoreOS: macos
 // ----
 // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/types/array_branches_3d.sol

@@ -15,12 +15,6 @@ contract C
 }
 // ====
 // SMTEngine: all
-// SMTIgnoreOS: macos
+// SMTTargets: assert
 // ----
-// Warning 6368: (124-131): CHC: Out of bounds access might happen here.
-// Warning 6368: (124-134): CHC: Out of bounds access might happen here.
-// Warning 6368: (152-159): CHC: Out of bounds access might happen here.
-// Warning 6368: (152-162): CHC: Out of bounds access might happen here.
-// Warning 6368: (177-184): CHC: Out of bounds access might happen here.
-// Warning 6368: (177-187): CHC: Out of bounds access might happen here.
-// Info 1391: CHC: 7 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/types/array_branches_3d_show_unproved.sol

@@ -5,7 +5,6 @@ contract C
 	mapping (uint => uint8)[2] severalMaps8;
 	mapping (uint => uint)[2][2] severalMaps3d;
 	function f(mapping (uint => uint) storage map) internal {
-		// Accesses are safe but oob is reported because of aliasing.
 		severalMaps[0][0] = 42;
 		severalMaps8[0][0] = 42;
 		severalMaps3d[0][0][0] = 42;
@@ -15,8 +14,7 @@ contract C
 		// 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.
-		// Removed because current Spacer seg faults in cex generation.
-		//assert(severalMaps3d[0][0][0] == 42);
+		assert(severalMaps3d[0][0][0] == 42);
 	}
 	function g(uint x) public {
 		require(x < severalMaps.length);
@@ -26,6 +24,8 @@ contract C
 // ====
 // SMTEngine: all
 // SMTIgnoreCex: yes
+// SMTTargets: assert
 // ----
-// Warning 6328: (456-487): CHC: Assertion violation happens here.
-// Info 1391: CHC: 8 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Warning 6328: (392-423): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n    C.f(map) -- counterexample incomplete; parameter name used instead of value -- internal call
+// Warning 6328: (606-642): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n    C.f(map) -- counterexample incomplete; parameter name used instead of value -- internal call
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol

@@ -5,7 +5,6 @@ contract C
 	mapping (uint => uint8)[2] severalMaps8;
 	mapping (uint => uint)[2][2] severalMaps3d;
 	function f(mapping (uint => uint) storage map) internal {
-		// Accesses are safe but reported as unsafe due to aliasing.
 		map[0] = 42;
 		severalMaps[0][0] = 42;
 		severalMaps8[0][0] = 42;
@@ -16,8 +15,7 @@ contract C
 		// 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.
-		// Removed because of Spacer nondeterminism.
-		//assert(severalMaps3d[0][0][0] == 42);
+		assert(severalMaps3d[0][0][0] == 42);
 		// Should fail since singleMap == map is possible.
 		assert(map[0] == 42);
 	}
@@ -29,9 +27,7 @@ contract C
 // ====
 // SMTEngine: all
 // SMTIgnoreCex: yes
+// SMTTargets: assert
 // ----
-// Warning 6368: (340-355): CHC: Out of bounds access might happen here.
-// Warning 6368: (612-627): CHC: Out of bounds access might happen here.
-// Warning 6328: (860-880): CHC: Assertion violation happens here.
-// Warning 6368: (936-952): CHC: Out of bounds access might happen here.
-// Info 1391: CHC: 7 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Warning 6328: (748-768): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n    C.f(map) -- counterexample incomplete; parameter name used instead of value -- internal call
+// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.