Merge pull request #11040 from ethereum/smt_fix_virtual_one_more_time

[SMTChecker] Fix bug in virtual functions called by constructor

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init_chain_alternate.sol

@@ -25,4 +25,4 @@ contract D is C {
 	}
 }
 // ----
-// Warning 6328: (319-333): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\na = 0\n\nTransaction trace:\nD.constructor(0)
+// Warning 6328: (319-333): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\na = 1\n\nTransaction trace:\nD.constructor(1)

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol

@@ -29,4 +29,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (299-313): CHC: Assertion violation happens here.\nCounterexample:\nowner = 0, y = 0, s = 0\n\nTransaction trace:\nC.constructor()\nState: owner = 0, y = 0, s = 0\nC.f()\n    s.f() -- untrusted external call
+// Warning 6328: (299-313): CHC: Assertion violation happens here.\nCounterexample:\nowner = 0, y = 0, s = 0\n\nTransaction trace:\nC.constructor()\nState: owner = 0, y = 0, s = 0\nC.f()\n    s.f() -- untrusted external call, synthesized as:\n        C.f() -- reentrant call\n            s.f() -- untrusted external call

test/libsolidity/smtCheckerTests/functions/constructor_state_value.sol

@@ -13,4 +13,4 @@ contract C {
 	}
 }
 // ----
-// Warning 6328: (145-159): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 9\n\nTransaction trace:\nC.constructor()\nState: x = 10\nC.f(9)
+// Warning 6328: (145-159): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\ny = 11\n\nTransaction trace:\nC.constructor()\nState: x = 10\nC.f(11)

test/libsolidity/smtCheckerTests/functions/virtual_function_called_by_constructor.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+contract A {
+    uint public x;
+    function v() internal virtual {
+        x = 2;
+    }
+    constructor() {
+        v();
+    }
+	function i() public view virtual {
+		assert(x == 2); // should hold
+		assert(x == 10); // should fail
+	}
+}
+
+contract C is A {
+    function v() internal override {
+        x = 10;
+    }
+	function i() public view override {
+		assert(x == 10); // should hold
+		assert(x == 2); // should fail
+	}
+}
+// ----
+// Warning 6328: (231-246): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nA.constructor()\nState: x = 2\nA.i()
+// Warning 6328: (419-433): CHC: Assertion violation happens here.\nCounterexample:\nx = 10\n\nTransaction trace:\nC.constructor()\nState: x = 10\nC.i()

test/libsolidity/smtCheckerTests/inheritance/constructor_state_variable_init_diamond_middle.sol

@@ -25,5 +25,5 @@ contract D is B, C {
 	}
 }
 // ----
-// Warning 6328: (167-181): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nD.constructor()
 // Warning 6328: (256-270): CHC: Assertion violation happens here.\nCounterexample:\nx = 3\n\nTransaction trace:\nD.constructor()
+// Warning 6328: (167-181): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nD.constructor()

test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol

@@ -12,5 +12,3 @@ contract C
 	}
 }
 // ----
-// Warning 4984: (139-144): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
-// Warning 2661: (139-144): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/loops/while_nested_break_fail.sol

@@ -30,4 +30,4 @@ contract C
 }
 // ----
 // Warning 6328: (329-344): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 10\nb = false\nc = true\n\nTransaction trace:\nC.constructor()\nC.f(0, 9, false, true)
-// Warning 6328: (380-395): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 15\ny = 0\nb = true\nc = false\n\nTransaction trace:\nC.constructor()\nC.f(9, 0, true, false)
+// Warning 6328: (380-395): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 15\ny = 20\nb = false\nc = false\n\nTransaction trace:\nC.constructor()\nC.f(0, 0, false, false)

test/libsolidity/smtCheckerTests/overflow/signed_div_overflow.sol

@@ -7,4 +7,4 @@ contract C  {
 }
 // ----
 // Warning 4281: (110-115): CHC: Division by zero happens here.\nCounterexample:\n\nx = 0\ny = 0\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0)
-// Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.
+// Warning 4984: (110-115): CHC: Overflow (resulting value larger than 0x80 * 2**248 - 1) happens here.\nCounterexample:\n\nx = (- 57896044618658097711785492504343953926634992332820282019728792003956564819968)\ny = (- 1)\n = 0\n\nTransaction trace:\nC.constructor()\nC.f((- 57896044618658097711785492504343953926634992332820282019728792003956564819968), (- 1))

test/libsolidity/smtCheckerTests/special/abi_decode_simple.sol

@@ -14,6 +14,6 @@ contract C {
 // Warning 2072: (184-188): Unused local variable.
 // Warning 8364: (155-156): Assertion checker does not yet implement type type(contract C)
 // Warning 8364: (225-226): Assertion checker does not yet implement type type(contract C)
-// Warning 6328: (252-268): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [13, 13, 13, 13, 13, 13, 13, 13, 10, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13]\n\nTransaction trace:\nC.constructor()\nC.f([13, 13, 13, 13, 13, 13, 13, 13, 10, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13, 13])
+// Warning 6328: (252-268): CHC: Assertion violation happens here.\nCounterexample:\n\ndata = [10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 13, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10]\n\nTransaction trace:\nC.constructor()\nC.f([10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 13, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10, 10])
 // Warning 8364: (155-156): Assertion checker does not yet implement type type(contract C)
 // Warning 8364: (225-226): Assertion checker does not yet implement type type(contract C)

test/libsolidity/smtCheckerTests/special/difficulty.sol

@@ -7,4 +7,4 @@ contract C
 	}
 }
 // ----
-// Warning 6328: (91-129): CHC: Assertion violation happens here.\nCounterexample:\n\ndifficulty = 38\n\nTransaction trace:\nC.constructor()\nC.f(38)
+// Warning 6328: (91-129): CHC: Assertion violation happens here.\nCounterexample:\n\ndifficulty = 39\n\nTransaction trace:\nC.constructor()\nC.f(39)

test/libsolidity/smtCheckerTests/special/msg_value_inheritance_2.sol

@@ -14,5 +14,5 @@ contract C is A {
 	}
 }
 // ----
-// Warning 6328: (93-107): CHC: Assertion violation happens here.\nCounterexample:\nv = 0, x = 1\n\nTransaction trace:\nC.constructor(){ value: 1 }
 // Warning 6328: (273-287): CHC: Assertion violation happens here.\nCounterexample:\nv = 1, x = 1\n\nTransaction trace:\nC.constructor(){ value: 1 }
+// Warning 6328: (93-107): CHC: Assertion violation happens here.\nCounterexample:\nv = 0, x = 1\n\nTransaction trace:\nC.constructor(){ value: 1 }

test/libsolidity/smtCheckerTests/types/contract_address_conversion.sol

@@ -7,4 +7,4 @@ contract C
 	}
 }
 // ----
-// Warning 6328: (90-113): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 0\na = 1\n\nTransaction trace:\nC.constructor()\nC.f(0, 1)
+// Warning 6328: (90-113): CHC: Assertion violation happens here.\nCounterexample:\n\nc = 1\na = 0\n\nTransaction trace:\nC.constructor()\nC.f(1, 0)

test/libsolidity/smtCheckerTests/types/mapping_as_parameter_1.sol

@@ -12,4 +12,4 @@ contract c {
 	}
 }
 // ----
-// Warning 6328: (289-306): CHC: Assertion violation happens here.\nCounterexample:\n\na = 38\nb = 21239\n\nTransaction trace:\nc.constructor()\nc.g(38, 21239)\n    c.f(map, 38, 21239) -- internal call
+// Warning 6328: (289-306): CHC: Assertion violation happens here.\nCounterexample:\n\na = 38\nb = 21238\n\nTransaction trace:\nc.constructor()\nc.g(38, 21238)\n    c.f(map, 38, 21238) -- internal call

test/libsolidity/smtCheckerTests/types/mapping_equal_keys_2.sol

@@ -9,4 +9,4 @@ contract C
 	}
 }
 // ----
-// Warning 6328: (119-133): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 1\n\nTransaction trace:\nC.constructor()\nC.f(0, 1)
+// Warning 6328: (119-133): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\ny = 0\n\nTransaction trace:\nC.constructor()\nC.f(1, 0)