Merge pull request #10721 from blishko/smt-try-catch

[SMTChecker] Support try-catch statements

test/libsolidity/smtCheckerTests/bmc_coverage/try_multiple_catch_clauses_2.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+contract C {
+
+	function g() public pure {}
+
+	function f() public view {
+		uint x = 0;
+		bool success = false;
+		try this.g() {
+			success = true;
+			x = 1;
+		} catch Error (string memory /*reason*/) {
+			x = 2;
+		} catch (bytes memory /*reason*/) {
+			x = 3;
+		}
+		assert(x > 0 && x < 4); // should hold
+		assert(x == 0); // should fail
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (338-352): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/bmc_coverage/try_multiple_returned_values_with_tuple.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+contract C {
+
+	struct S {
+		uint x;
+		int y;
+	}
+
+	function g() public pure returns (bool b, S memory s) {
+		b = true;
+		s.x = 42;
+		s.y = -1;
+	}
+
+	function f() public view {
+		bool success = false;
+		try this.g() returns (bool b, S memory s) {
+			success = true;
+			assert(b && s.x == 42 && s.y == -1); // should hold
+		} catch {
+		}
+		assert(success); // fails, not guaranteed that there will be no error
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (368-383): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/try_catch_1.sol

@@ -9,7 +9,3 @@ contract C {
 // EVMVersion: >=byzantium
 // ----
 // Warning 6321: (75-79): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
-// Warning 7645: (98-121): Assertion checker does not support try/catch clauses.
-// Warning 7645: (124-159): Assertion checker does not support try/catch clauses.
-// Warning 7645: (98-121): Assertion checker does not support try/catch clauses.
-// Warning 7645: (124-159): Assertion checker does not support try/catch clauses.

test/libsolidity/smtCheckerTests/control_flow/try_catch_2.sol

@@ -10,7 +10,3 @@ contract C {
 // ====
 // EVMVersion: >=byzantium
 // ----
-// Warning 7645: (83-85): Assertion checker does not support try/catch clauses.
-// Warning 7645: (88-122): Assertion checker does not support try/catch clauses.
-// Warning 7645: (83-85): Assertion checker does not support try/catch clauses.
-// Warning 7645: (88-122): Assertion checker does not support try/catch clauses.

test/libsolidity/smtCheckerTests/try_catch/try_1.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+contract C {
+	int x;
+
+	function g() public  {
+		x = 42;
+	}
+
+	function f() public {
+		x = 0;
+		bool success = false;
+		try this.g() {
+			success = true;
+		} catch (bytes memory s) {
+			assert(x == 0); // should hold
+		}
+		assert(success); // fails for now, since external call is over-approximated (both success and fail are considered possible) for now even for known code
+	}
+}
+// ----
+// Warning 5667: (195-209): Unused try/catch parameter. Remove or comment out the variable name to silence this warning.
+// Warning 6328: (253-268): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()

test/libsolidity/smtCheckerTests/try_catch/try_2.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+contract C {
+	int x;
+
+	function g() public  {
+		x = 42;
+	}
+
+	function f() public {
+		x = 0;
+		try this.g() {
+			assert(x == 42); // should hold
+		} catch (bytes memory s) {
+			assert(x == 0); // should hold
+		}
+	}
+}
+// ----
+// Warning 5667: (187-201): Unused try/catch parameter. Remove or comment out the variable name to silence this warning.

test/libsolidity/smtCheckerTests/try_catch/try_3.sol

@@ -0,0 +1,25 @@
+pragma experimental SMTChecker;
+contract C {
+	int x;
+
+	function g(int y) public pure returns (int) {
+		return y;
+	}
+
+	function postinc() internal returns (int) {
+		x += 1;
+		return x;
+	}
+
+	function f() public {
+		x = 0;
+		try this.g(postinc()) {
+			assert(x == 1); // should hold
+		} catch (bytes memory s) {
+			assert(x == 0); // should fail - state is reverted to the state after postinc(), but before the call to this.g()
+		}
+	}
+}
+// ----
+// Warning 5667: (291-305): Unused try/catch parameter. Remove or comment out the variable name to silence this warning.
+// Warning 6328: (312-326): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\n\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()

test/libsolidity/smtCheckerTests/try_catch/try_4.sol

@@ -0,0 +1,30 @@
+pragma experimental SMTChecker;
+
+abstract contract D {
+	function d() external virtual;
+}
+
+contract C {
+
+	int x;
+	D d;
+
+	function set(int n) public {
+		x = n;
+	}
+
+	function f() public {
+		x = 0;
+		try d.d() {
+			assert(x == 0); // should fail, x can be anything here
+		} catch {
+			assert(x == 0); // should hold, all changes to x has been reverted
+			assert(x == 1); // should fail
+		}
+	}
+}
+// ====
+// SMTIgnoreCex: yes
+// ----
+// Warning 6328: (211-225): CHC: Assertion violation happens here.
+// Warning 6328: (351-365): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/try_catch/try_5.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+abstract contract D {
+	function d() external virtual;
+}
+
+contract C {
+
+	int x;
+	D d;
+
+	function set(int n) public {
+		require(n < 100);
+		x = n;
+	}
+
+	function f() public {
+		x = 0;
+		try d.d() {
+			assert(x < 100); // should hold
+		} catch {
+			assert(x == 0); // should hold, all changes to x has been reverted
+			assert(x == 1); // should fail
+		}
+	}
+}
+// ----
+// Warning 6328: (348-362): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\n\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()

test/libsolidity/smtCheckerTests/try_catch/try_inside_if.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C {
+  function g(bool b) public {}
+  function f(bool b) public returns (bytes memory txt) {
+    if (0==1)
+      try this.g(b) {}
+      catch (bytes memory s) {
+        txt = s;
+      }
+  }
+}
+
+// ----
+// Warning 6838: (141-145): BMC: Condition is always false.

test/libsolidity/smtCheckerTests/try_catch/try_inside_while.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+contract C {
+	function f() public returns (uint) {
+		while(1==1)
+			try this.f() returns (uint b) {
+				b = 2;
+			} catch {
+			}
+	}
+}
+// ----
+// Warning 6321: (75-79): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
+// Warning 6838: (91-95): BMC: Condition is always true.

test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses.sol

@@ -0,0 +1,25 @@
+pragma experimental SMTChecker;
+contract C {
+	int x;
+
+	function g() public  {
+		x = 42;
+	}
+
+	function f() public {
+		x = 1;
+		bool success = false;
+		try this.g() {
+			success = true;
+			assert(x == 42); // should hold
+		} catch Error (string memory /*reason*/) {
+			assert(x == 1); // should hold
+		} catch (bytes memory /*reason*/) {
+			assert(x == 1); // should hold
+		}
+		assert((success && x == 42) || (!success && x == 1)); // should hold
+		assert(success); // can fail
+	}
+}
+// ----
+// Warning 6328: (447-462): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\n\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()

test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+contract C {
+
+	function g() public pure {}
+
+	function f() public view {
+		uint x = 0;
+		bool success = false;
+		try this.g() {
+			success = true;
+			x = 1;
+		} catch Error (string memory /*reason*/) {
+			x = 2;
+		} catch (bytes memory /*reason*/) {
+			x = 3;
+		}
+		assert(x > 0 && x < 4); // should hold
+		assert(x == 0); // should fail
+	}
+}
+// ----
+// Warning 6328: (338-352): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nC.constructor()\nC.f()

test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+abstract contract D {
+	function d() external virtual returns (uint x, bool b);
+}
+
+contract C {
+
+	int x;
+	D d;
+
+	function f() public {
+		x = 0;
+		try d.d() returns (uint x, bool c) {
+			assert(x == 0); // should fail, x is the local variable shadowing the state variable
+			assert(!c); // should fail, c can be anything
+		} catch {
+			assert(x == 0); // should hold, x is the state variable
+			assert(x == 1); // should fail
+		}
+	}
+}
+// ----
+// Warning 2519: (197-203): This declaration shadows an existing declaration.
+// Warning 6328: (218-232): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\n\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()
+// Warning 6328: (306-316): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\n\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()
+// Warning 6328: (426-440): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\n\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f()

test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values_with_tuple.sol

@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+contract C {
+
+	struct S {
+		uint x;
+		int y;
+	}
+
+	function g() public pure returns (bool b, S memory s) {
+		b = true;
+		s.x = 42;
+		s.y = -1;
+	}
+
+	function f() public view {
+		bool success = false;
+		try this.g() returns (bool b, S memory s) {
+			success = true;
+			assert(b && s.x == 42 && s.y == -1);
+		} catch {
+		}
+		assert(success); // fails, not guaranteed that there will be no error
+	}
+}
+// ----
+// Warning 6328: (353-368): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nC.constructor()\nC.f()

test/libsolidity/smtCheckerTests/try_catch/try_new.sol

@@ -0,0 +1,34 @@
+pragma experimental SMTChecker;
+
+contract Reverts {
+    constructor(uint) { revert("test message."); }
+}
+contract Succeeds {
+    constructor(uint) { }
+}
+
+contract C {
+    function f() public returns (Reverts x, string memory txt) {
+        uint i = 3;
+        try new Reverts(i) returns (Reverts r) {
+            x = r;
+            txt = "success";
+        } catch Error(string memory s) {
+            txt = s;
+        }
+    }
+    function g() public returns (Succeeds x, string memory txt) {
+        uint i = 8;
+        try new Succeeds(i) returns (Succeeds r) {
+            x = r;
+            txt = "success";
+        } catch Error(string memory s) {
+            txt = s;
+        }
+    }
+}
+// ----
+// Warning 4588: (264-278): Assertion checker does not yet implement this type of function call.
+// Warning 4588: (525-540): Assertion checker does not yet implement this type of function call.
+// Warning 4588: (264-278): Assertion checker does not yet implement this type of function call.
+// Warning 4588: (525-540): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/try_catch/try_public_var.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C {
+	int public x;
+
+	function f() public view {
+		try this.x() returns (int v) {
+			assert(x == v); // should hold
+		} catch {
+			assert(false); // this fails, because we over-approximate every external call in the way that it can both succeed and fail
+		}
+	}
+}
+// ----
+// Warning 6328: (171-184): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()

test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol

@@ -0,0 +1,23 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (uint => uint[]) public m;
+
+	constructor() {
+		m[0].push();
+		m[0].push();
+		m[0][1] = 42;
+	}
+
+	function f() public view {
+		try this.m(0,1) returns (uint y) {
+			assert(y == m[0][1]); // should hold
+		}
+		catch {
+			assert(m[0][1] == 42); // should hold
+			assert(m[0][1] == 1); // should fail
+		}
+	}
+}
+// ----
+// Warning 6328: (313-333): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nC.constructor()\nC.f()

test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_bytes_array.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+contract C {
+
+	function g() public pure returns (bytes memory) {
+		return hex"ffff";
+	}
+
+	function f() public view {
+		try this.g() returns (bytes memory b) {
+			assert(b[0] == bytes1(uint8(255)) && b[1] == bytes1(uint8(255))); // should hold
+			assert(b[0] == bytes1(uint8(0)) || b[1] == bytes1(uint8(0))); // should fail
+		} catch {
+		}
+	}
+}
+// ----
+// Warning 6328: (278-338): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nC.constructor()\nC.f()

test/libsolidity/smtCheckerTests/try_catch/try_string_literal_to_fixed_bytes.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+contract C {
+
+	function g() public pure returns (bytes2) {
+		return hex"ffff";
+	}
+
+	function f() public view {
+		try this.g() returns (bytes2 b) {
+			assert(uint8(b[0]) == 255 && uint8(b[1]) == 255); // should hold
+			assert(uint8(b[0]) == 0 || uint8(b[1]) == 0); // should fail
+		} catch {
+		}
+	}
+}
+// ----
+// Warning 6328: (250-294): CHC: Assertion violation happens here.