diff --git a/test/libsolidity/smtCheckerTests/control_flow/try_catch_1.sol b/test/libsolidity/smtCheckerTests/control_flow/try_catch_1.sol index 921aeea7b..9f15677dc 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/try_catch_1.sol +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/control_flow/try_catch_2.sol b/test/libsolidity/smtCheckerTests/control_flow/try_catch_2.sol index ed1971b4a..b0b9706fd 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/try_catch_2.sol +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_1.sol b/test/libsolidity/smtCheckerTests/try_catch/try_1.sol new file mode 100644 index 000000000..4f2755f80 --- /dev/null +++ b/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() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_2.sol b/test/libsolidity/smtCheckerTests/try_catch/try_2.sol new file mode 100644 index 000000000..8f80601e4 --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_3.sol b/test/libsolidity/smtCheckerTests/try_catch/try_3.sol new file mode 100644 index 000000000..b3e7c7e1e --- /dev/null +++ b/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() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_4.sol b/test/libsolidity/smtCheckerTests/try_catch/try_4.sol new file mode 100644 index 000000000..c10624db4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/try_catch/try_4.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 { + 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 + } + } +} +// ---- +// Warning 6328: (211-225): CHC: Assertion violation happens here.\nCounterexample:\nx = (- 1), d = 0\n\n\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f() +// Warning 6328: (351-365): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, d = 0\n\n\n\nTransaction trace:\nC.constructor()\nState: x = 0, d = 0\nC.f() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_5.sol b/test/libsolidity/smtCheckerTests/try_catch/try_5.sol new file mode 100644 index 000000000..2c7a68674 --- /dev/null +++ b/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() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_inside_if.sol b/test/libsolidity/smtCheckerTests/try_catch/try_inside_if.sol new file mode 100644 index 000000000..ec9ed22f1 --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses.sol b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses.sol new file mode 100644 index 000000000..654396afd --- /dev/null +++ b/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() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values.sol b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values.sol new file mode 100644 index 000000000..aeb76a4bc --- /dev/null +++ b/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() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_new.sol b/test/libsolidity/smtCheckerTests/try_catch/try_new.sol new file mode 100644 index 000000000..563e2fdfe --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_public_var.sol b/test/libsolidity/smtCheckerTests/try_catch/try_public_var.sol new file mode 100644 index 000000000..5d044f5b7 --- /dev/null +++ b/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() diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol b/test/libsolidity/smtCheckerTests/try_catch/try_public_var_mapping.sol new file mode 100644 index 000000000..908af50ce --- /dev/null +++ b/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()