From ba4173cd8ab51ed762583fd483b11ba1f7a4a0ac Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Wed, 10 Nov 2021 17:17:07 +0100 Subject: [PATCH] Add new tests with semantic this and indirect storage changes --- .../deployment/deploy_bmc_trusted.sol | 18 +++++ .../deployment/deploy_bmc_untrusted.sol | 17 +++++ .../deployment/deploy_trusted.sol | 16 +++++ .../deployment/deploy_trusted_addresses.sol | 19 ++++++ .../deployment/deploy_trusted_flow.sol | 24 +++++++ ...eploy_trusted_keep_storage_constraints.sol | 17 +++++ .../deployment/deploy_trusted_state_flow.sol | 23 +++++++ .../deploy_trusted_state_flow_2.sol | 20 ++++++ .../deploy_trusted_state_flow_3.sol | 23 +++++++ .../deploy_trusted_state_flow_4.sol | 20 ++++++ .../deployment/deploy_untrusted.sol | 17 +++++ .../deployment/deploy_untrusted_addresses.sol | 22 ++++++ ...oy_untrusted_erase_storage_constraints.sol | 17 +++++ .../deployment_trusted_with_value_1.sol | 20 ++++++ ...ternal_call_from_constructor_1_trusted.sol | 21 ++++++ ...ternal_call_from_constructor_2_trusted.sol | 17 +++++ ...ternal_call_from_constructor_3_trusted.sol | 25 +++++++ .../external_call_indirect_1.sol | 40 +++++++++++ .../external_call_indirect_2.sol | 46 +++++++++++++ .../external_call_indirect_3.sol | 44 ++++++++++++ .../external_call_indirect_4.sol | 48 +++++++++++++ .../external_call_indirect_5.sol | 50 ++++++++++++++ .../external_call_semantic_this_1.sol | 16 +++++ .../external_call_semantic_this_2.sol | 16 +++++ .../external_call_semantic_this_3.sol | 17 +++++ .../external_hash_known_code_pure_trusted.sol | 33 +++++++++ ..._known_code_state_reentrancy_2_trusted.sol | 47 +++++++++++++ ...code_state_reentrancy_indirect_trusted.sol | 56 +++++++++++++++ ...sh_known_code_state_reentrancy_trusted.sol | 38 +++++++++++ ...n_code_state_reentrancy_unsafe_trusted.sol | 43 ++++++++++++ ...external_hash_known_code_state_trusted.sol | 35 ++++++++++ ...l_hash_known_code_state_unsafe_trusted.sol | 40 +++++++++++ .../token_trusted_transfer_correct.sol | 64 +++++++++++++++++ .../token_trusted_transfer_wrong.sol | 68 +++++++++++++++++++ 34 files changed, 1037 insertions(+) create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_bmc_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_bmc_untrusted.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_trusted_addresses.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_trusted_keep_storage_constraints.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_2.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_3.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_4.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_untrusted.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_untrusted_addresses.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deploy_untrusted_erase_storage_constraints.sol create mode 100644 test/libsolidity/smtCheckerTests/deployment/deployment_trusted_with_value_1.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_2.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_4.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_5.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_2.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_3.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe_trusted.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/token_trusted_transfer_correct.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/token_trusted_transfer_wrong.sol diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_bmc_trusted.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_bmc_trusted.sol new file mode 100644 index 000000000..81ddc515e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_bmc_trusted.sol @@ -0,0 +1,18 @@ +contract D { + uint x; + function f() public view returns (uint) { return x; } +} + +contract C { + function g() public { + D d = new D(); + uint y = d.f(); + assert(y == 0); // should fail in BMC + } +} +// ==== +// SMTEngine: bmc +// SMTExtCalls: trusted +// ---- +// Warning 8729: (124-131): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. +// Warning 4661: (153-167): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_bmc_untrusted.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_bmc_untrusted.sol new file mode 100644 index 000000000..f69a8d6c7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_bmc_untrusted.sol @@ -0,0 +1,17 @@ +contract D { + uint x; + function f() public view returns (uint) { return x; } +} + +contract C { + function g() public { + D d = new D(); + uint y = d.f(); + assert(y == 0); // should fail in ext calls untrusted mode + } +} +// ==== +// SMTEngine: bmc +// ---- +// Warning 8729: (124-131): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. +// Warning 4661: (153-167): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted.sol new file mode 100644 index 000000000..388b0b0db --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted.sol @@ -0,0 +1,16 @@ +contract D { + uint x; + function f() public view returns (uint) { return x; } +} + +contract C { + function g() public { + D d = new D(); + uint y = d.f(); + assert(y == 0); // should hold in ext calls trusted mode + } +} +// ==== +// SMTEngine: all +// SMTExtCalls: trusted +// ---- diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_addresses.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_addresses.sol new file mode 100644 index 000000000..cf43dbda2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_addresses.sol @@ -0,0 +1,19 @@ +contract D { + uint x; +} + +contract C { + function f() public { + D d1 = new D(); + D d2 = new D(); + + assert(d1 != d2); // should hold in ext calls trusted mode + assert(address(this) != address(d1)); // should hold in ext calls trusted mode + assert(address(this) != address(d2)); // should hold in ext calls trusted mode + } +} +// ==== +// SMTEngine: all +// SMTExtCalls: trusted +// ---- +// Info 1180: Contract invariant(s) for :C:\n(:var 0).isActive[address(this)]\n diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol new file mode 100644 index 000000000..5a6720067 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol @@ -0,0 +1,24 @@ +contract D { + uint x; + function inc() public { ++x; } + function f() public view returns (uint) { return x; } +} + +contract C { + function f() public { + D d = new D(); + assert(d.f() == 0); // should hold + d.inc(); + assert(d.f() == 1); // should hold + d = new D(); + assert(d.f() == 0); // should hold + assert(d.f() == 1); // should fail + } +} +// ==== +// SMTEngine: all +// SMTExtCalls: trusted +// ---- +// Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. +// Warning 6328: (304-322): CHC: Assertion violation happens here. +// Warning 2661: (47-50): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_keep_storage_constraints.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_keep_storage_constraints.sol new file mode 100644 index 000000000..b2aa7ac98 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_keep_storage_constraints.sol @@ -0,0 +1,17 @@ +contract D { + uint x; +} + +contract C { + uint y; + function g() public { + D d = new D(); + assert(y == 0); // should hold + } +} +// ==== +// SMTEngine: all +// SMTExtCalls: trusted +// ---- +// Warning 2072: (72-75): Unused local variable. +// Info 1180: Contract invariant(s) for :C:\n(y <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow.sol new file mode 100644 index 000000000..94dff06f0 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow.sol @@ -0,0 +1,23 @@ +contract D { + uint x; + function inc() public { ++x; } + function f() public view returns (uint) { return x; } +} + +contract C { + D d; + constructor() { + d = new D(); + assert(d.f() == 0); // should hold + } + function g() public view { + assert(d.f() == 0); // should fail + } +} +// ==== +// SMTEngine: all +// SMTExtCalls: trusted +// ---- +// Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. +// Warning 6328: (233-251): CHC: Assertion violation happens here. +// Warning 2661: (47-50): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_2.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_2.sol new file mode 100644 index 000000000..66684df8c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_2.sol @@ -0,0 +1,20 @@ +contract D { + uint x; + function f() public view returns (uint) { return x; } +} + +contract C { + D d; + constructor() { + d = new D(); + assert(d.f() == 0); // should hold + } + function g() public view { + assert(d.f() == 0); // should hold + } +} +// ==== +// SMTEngine: all +// SMTExtCalls: trusted +// ---- +// Info 1180: Contract invariant(s) for :C:\n((:var 1).storage.storage_D_12[d].x_3_D_12 <= 0)\nReentrancy property(ies) for :D:\n((x' <= 0) || !(x <= 0))\n diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_3.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_3.sol new file mode 100644 index 000000000..504362145 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_3.sol @@ -0,0 +1,23 @@ +contract D { + uint x; + function s(uint _x) public { x = _x; } + function f() public view returns (uint) { return x; } +} + +contract C { + D d; + constructor() { + d = new D(); + } + function g() public view { + assert(d.f() == 0); // should fail + } +} +// ==== +// SMTContract: C +// SMTEngine: all +// SMTExtCalls: trusted +// ---- +// Warning 1218: (204-222): CHC: Error trying to invoke SMT solver. +// Warning 6328: (204-222): CHC: Assertion violation might happen here. +// Warning 4661: (204-222): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_4.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_4.sol new file mode 100644 index 000000000..e2036b32f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_trusted_state_flow_4.sol @@ -0,0 +1,20 @@ +contract D { + bool b; + function s() public { b = true; } + function f() public view returns (bool) { return b; } +} + +contract C { + D d; + constructor() { + d = new D(); + } + function g() public view { + assert(d.f()); // should fail + } +} +// ==== +// SMTEngine: all +// SMTExtCalls: trusted +// ---- +// Warning 6328: (199-212): CHC: Assertion violation happens here.\nCounterexample:\nd = 0\n\nTransaction trace:\nC.constructor()\nState: d = 0\nC.g()\n D.f() -- trusted external call diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_untrusted.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_untrusted.sol new file mode 100644 index 000000000..a28d46210 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_untrusted.sol @@ -0,0 +1,17 @@ +contract D { + uint x; + function f() public view returns (uint) { return x; } +} + +contract C { + function g() public { + D d = new D(); + uint y = d.f(); + assert(y == 0); // should fail in ext calls untrusted mode + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 8729: (124-131): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. +// Warning 6328: (153-167): CHC: Assertion violation happens here.\nCounterexample:\n\nd = 0\ny = 1\n\nTransaction trace:\nC.constructor()\nC.g()\n d.f() -- untrusted external call diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_untrusted_addresses.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_untrusted_addresses.sol new file mode 100644 index 000000000..c934e152b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_untrusted_addresses.sol @@ -0,0 +1,22 @@ +contract D { + uint x; +} + +contract C { + function f() public { + D d1 = new D(); + D d2 = new D(); + + assert(d1 != d2); // should fail in ext calls untrusted mode + assert(address(this) != address(d1)); // should fail in ext calls untrusted mode + assert(address(this) != address(d2)); // should fail in ext calls untrusted mode + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 8729: (70-77): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. +// Warning 8729: (88-95): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. +// Warning 6328: (100-116): CHC: Assertion violation happens here.\nCounterexample:\n\nd1 = 0\nd2 = 0\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (163-199): CHC: Assertion violation happens here.\nCounterexample:\n\nd1 = 21238\nd2 = 21238\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 6328: (246-282): CHC: Assertion violation happens here.\nCounterexample:\n\nd1 = 21238\nd2 = 21238\n\nTransaction trace:\nC.constructor()\nC.f() diff --git a/test/libsolidity/smtCheckerTests/deployment/deploy_untrusted_erase_storage_constraints.sol b/test/libsolidity/smtCheckerTests/deployment/deploy_untrusted_erase_storage_constraints.sol new file mode 100644 index 000000000..be18b33f6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deploy_untrusted_erase_storage_constraints.sol @@ -0,0 +1,17 @@ +contract D { + uint x; +} + +contract C { + uint y; + function g() public { + D d = new D(); + assert(y == 0); // should fail in ext calls untrusted mode + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 2072: (72-75): Unused local variable. +// Warning 8729: (78-85): Contract deployment is only supported in the trusted mode for external calls with the CHC engine. +// Warning 6328: (89-103): CHC: Assertion violation happens here.\nCounterexample:\ny = 1\nd = 0\n\nTransaction trace:\nC.constructor()\nState: y = 0\nC.g() diff --git a/test/libsolidity/smtCheckerTests/deployment/deployment_trusted_with_value_1.sol b/test/libsolidity/smtCheckerTests/deployment/deployment_trusted_with_value_1.sol new file mode 100644 index 000000000..92195221e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/deployment/deployment_trusted_with_value_1.sol @@ -0,0 +1,20 @@ +contract A { + constructor() payable {} +} + +contract B { + function f() public payable { + require(address(this).balance == 100); + A a = new A{value: 50}(); + assert(address(this).balance == 50); // should hold + assert(address(this).balance == 60); // should fail + assert(address(a).balance >= 50); // should hold + assert(address(a).balance == 50); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// ---- +// Warning 6328: (211-246): CHC: Assertion violation happens here. +// Warning 6328: (316-348): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1_trusted.sol new file mode 100644 index 000000000..ef3b53a90 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1_trusted.sol @@ -0,0 +1,21 @@ +contract State { + function f(uint _x) public pure returns (uint) { + assert(_x < 100); + return _x; + } +} +contract C { + State s; + uint z = s.f(2); + + function f() public view { + assert(z == 2); // should hold in trusted mode + } +} +// ==== +// SMTContract: C +// SMTEngine: all +// SMTExtCalls: trusted +// ---- +// Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100) +// Info 1180: Contract invariant(s) for :C:\n(!(z >= 3) && !(z <= 1))\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2_trusted.sol new file mode 100644 index 000000000..a81422729 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2_trusted.sol @@ -0,0 +1,17 @@ +contract C { + uint z = this.g(2); + + function g(uint _x) public pure returns (uint) { + assert(_x > 0); // should fail + return _x; + } + + function f() public view { + assert(z == 2); // should hold + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\nz = 2\n_x = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: z = 2\nC.g(0) +// Info 1180: Contract invariant(s) for :C:\n(!(z >= 3) && !(z <= 1))\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3_trusted.sol new file mode 100644 index 000000000..ce7b382b7 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3_trusted.sol @@ -0,0 +1,25 @@ +contract State { + function f(uint _x) public pure returns (uint) { + assert(_x < 100); + return _x; + } +} +contract C { + State s; + uint z; + + constructor() { + z = s.f(2); + } + + function f() public view { + assert(z == 2); // should hold in trusted mode + } +} +// ==== +// SMTContract: C +// SMTEngine: all +// SMTExtCalls: trusted +// ---- +// Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100) +// Info 1180: Contract invariant(s) for :C:\n(!(z >= 3) && !(z <= 1))\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol new file mode 100644 index 000000000..4fef1dc99 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_1.sol @@ -0,0 +1,40 @@ +contract A { + uint x; + function setX(uint _x) public { + x = _x; + } + function getX() public view returns (uint) { + return x; + } +} + +contract B { + A a; + constructor() { + a = new A(); + assert(a.getX() == 0); // should hold + } + function g() public view { + assert(a.getX() == 0); // should fail because A.setX() can be called without B + } + function getX() public view returns (uint) { + return a.getX(); + } +} + +contract C { + B b; + constructor() { + b = new B(); + assert(b.getX() == 0); // should hold + } + function f() public view { + assert(b.getX() == 0); // should fail because A.setX() can be called without A + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// ---- +// Warning 6328: (256-277): CHC: Assertion violation happens here. +// Warning 6328: (533-554): CHC: Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_2.sol new file mode 100644 index 000000000..ba9a72265 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_2.sol @@ -0,0 +1,46 @@ +contract A { + uint x; + address immutable owner; + constructor() { + owner = msg.sender; + } + function setX(uint _x) public { + require(msg.sender == owner); + x = _x; + } + function getX() public view returns (uint) { + return x; + } +} + +contract B { + A a; + constructor() { + a = new A(); + assert(a.getX() == 0); // should hold + } + function g() public view { + assert(a.getX() == 0); // should hold + } + function getX() public view returns (uint) { + return a.getX(); + } +} + +contract C { + B b; + constructor() { + b = new B(); + assert(b.getX() == 0); // should hold + } + function f() public view { + assert(b.getX() == 0); // should hold + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// ---- +// Warning 1218: (356-377): CHC: Error trying to invoke SMT solver. +// Warning 6328: (356-377): CHC: Assertion violation might happen here. +// Warning 6328: (592-613): CHC: Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol new file mode 100644 index 000000000..f9a596bc3 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_3.sol @@ -0,0 +1,44 @@ +contract A { + uint x; + address immutable owner; + constructor() { + owner = msg.sender; + } + function setX(uint _x) public { + require(msg.sender == owner); + x = _x; + } + function getX() public view returns (uint) { + return x; + } +} + +contract B { + A a; + constructor() { + a = new A(); + assert(a.getX() == 0); // should hold + } + function g() public { + a.setX(42); + } + function getX() public view returns (uint) { + return a.getX(); + } +} + +contract C { + B b; + constructor() { + b = new B(); + assert(b.getX() == 0); // should hold + } + function f() public view { + assert(b.getX() == 0); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// ---- +// Warning 6328: (561-582): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_4.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_4.sol new file mode 100644 index 000000000..336a5c2d1 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_4.sol @@ -0,0 +1,48 @@ +contract A { + uint x; + address immutable owner; + constructor() { + owner = msg.sender; + } + function setX(uint _x) public { + require(msg.sender == owner); + x = _x; + } + function getX() public view returns (uint) { + return x; + } +} + +contract B { + A a; + address immutable owner; + constructor() { + owner = msg.sender; + a = new A(); + assert(a.getX() == 0); // should hold + } + function g() public { + require(msg.sender == owner); + a.setX(42); + } + function getX() public view returns (uint) { + return a.getX(); + } +} + +contract C { + B b; + constructor() { + b = new B(); + assert(b.getX() == 0); // should hold + } + function f() public view { + assert(b.getX() == 0); // should hold + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// ---- +// Warning 1218: (641-662): CHC: Error trying to invoke SMT solver. +// Warning 6328: (641-662): CHC: Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_5.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_5.sol new file mode 100644 index 000000000..f5acee5aa --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_indirect_5.sol @@ -0,0 +1,50 @@ +contract A { + uint x; + address immutable owner; + constructor() { + owner = msg.sender; + } + function setX(uint _x) public { + require(msg.sender == owner); + x = _x; + } + function getX() public view returns (uint) { + return x; + } +} + +contract B { + A a; + address immutable owner; + constructor() { + owner = msg.sender; + a = new A(); + } + function g() public { + require(msg.sender == owner); + a.setX(42); + } + function getX() public view returns (uint) { + return a.getX(); + } +} + +contract C { + B b; + constructor() { + b = new B(); + assert(b.getX() == 0); // should hold + } + function f() public view { + assert(b.getX() == 0); // should fail + } + function h() public { + b.g(); + } +} +// ==== +// SMTContract: C +// SMTEngine: chc +// SMTExtCalls: trusted +// ---- +// Warning 6328: (601-622): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol new file mode 100644 index 000000000..5e1ad8b1b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_1.sol @@ -0,0 +1,16 @@ +contract C { + uint x; + function i() public { ++x; } + function f() public { + x = 0; + this.i(); + assert(x == 1); // should hold in trusted mode + assert(x != 1); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (147-161): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f()\n C.i() -- trusted external call diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_2.sol new file mode 100644 index 000000000..40e918862 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_2.sol @@ -0,0 +1,16 @@ +contract C { + uint x; + function i() public { ++x; } + function f() public { + x = 0; + ((this)).i(); + assert(x == 1); // should hold in trusted mode + assert(x != 1); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (151-165): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_3.sol new file mode 100644 index 000000000..1b95859af --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_semantic_this_3.sol @@ -0,0 +1,17 @@ +contract C { + uint x; + function i() public { ++x; } + function f() public { + x = 0; + C c = this; + c.i(); + assert(x == 1); // should hold in trusted mode + assert(x != 1); // should fail + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (158-172): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure_trusted.sol new file mode 100644 index 000000000..6c634d4ef --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure_trusted.sol @@ -0,0 +1,33 @@ +contract Crypto { + function hash(bytes32) external pure returns (bytes32) { + return bytes32(0); + } +} + +contract C { + address owner; + bytes32 sig_1; + bytes32 sig_2; + Crypto d; + + constructor() { + owner = msg.sender; + } + + function f1(bytes32 _msg) public { + address prevOwner = owner; + sig_1 = d.hash(_msg); + sig_2 = d.hash(_msg); + assert(prevOwner == owner); + } + + function inv() public view { + assert(sig_1 == sig_2); + } +} +// ==== +// SMTContract: C +// SMTEngine: all +// SMTExtCalls: trusted +// ---- +// Info 1180: Contract invariant(s) for :C:\n((sig_1 <= 0) && (sig_2 <= 0))\nReentrancy property(ies) for :Crypto:\n( = 0)\n = 0 -> no errors\n = 1 -> Assertion failed at assert(prevOwner == owner)\n = 3 -> Assertion failed at assert(sig_1 == sig_2)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2_trusted.sol new file mode 100644 index 000000000..62f53b64c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2_trusted.sol @@ -0,0 +1,47 @@ +contract State { + C c; + constructor(C _c) { + c = _c; + } + function f() public view returns (uint) { + return c.g(); + } +} + +contract C { + address owner; + uint y; + uint z; + State s; + bool insidef; + + constructor() { + owner = msg.sender; + s = new State(this); + } + + function zz() public { + require(insidef); + z = 3; + } + + function f() public { + require(!insidef); + address prevOwner = owner; + insidef = true; + s.f(); + assert(z == y); + assert(prevOwner == owner); + insidef = false; + } + + function g() public view returns (uint) { + return y; + } +} +// ==== +// SMTContract: C +// SMTEngine: chc +// SMTExtCalls: trusted +// ---- +// Info 1180: Contract invariant(s) for :C:\n((y <= 0) && (insidef || (z <= 0)))\nReentrancy property(ies) for :State:\n( = 0)\n = 0 -> no errors\n = 2 -> Assertion failed at assert(z == y)\n = 3 -> Assertion failed at assert(prevOwner == owner)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect_trusted.sol new file mode 100644 index 000000000..8000b3267 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect_trusted.sol @@ -0,0 +1,56 @@ +contract Other { + C c; + constructor(C _c) { + c = _c; + } + function h() public { + c.setOwner(address(0)); + } +} + +contract State { + uint x; + Other o; + C c; + constructor(C _c) { + c = _c; + o = new Other(_c); + } + function f() public returns (uint) { + o.h(); + return c.g(); + } +} + +contract C { + address owner; + uint y; + State s; + + constructor() { + owner = msg.sender; + s = new State(this); + } + + function setOwner(address _owner) public { + owner = _owner; + } + + function f() public { + address prevOwner = owner; + uint z = s.f(); + assert(z == y); // should hold + assert(prevOwner == owner); // should not hold because of reentrancy + } + + function g() public view returns (uint) { + return y; + } +} +// ==== +// SMTContract: C +// SMTEngine: chc +// SMTExtCalls: trusted +// ---- +// Warning 6328: (531-545): CHC: Assertion violation might happen here. +// Warning 6328: (564-590): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_trusted.sol new file mode 100644 index 000000000..ee373e293 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_trusted.sol @@ -0,0 +1,38 @@ +contract State { + C c; + constructor(C _c) { + c = _c; + } + function f() public view returns (uint) { + return c.g(); + } +} + +contract C { + address owner; + uint y; + State s; + + constructor() { + owner = msg.sender; + s = new State(this); + } + + function f() public view { + address prevOwner = owner; + uint z = s.f(); + assert(z == y); + assert(prevOwner == owner); + } + + function g() public view returns (uint) { + return y; + } +} +// ==== +// SMTContract: C +// SMTEngine: chc +// SMTExtCalls: trusted +// ---- +// Warning 6328: (314-328): CHC: Assertion violation might happen here. +// Info 1180: Reentrancy property(ies) for :State:\n( = 0)\n = 0 -> no errors\n = 1 -> Assertion failed at assert(z == y)\n = 2 -> Assertion failed at assert(prevOwner == owner)\n diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe_trusted.sol new file mode 100644 index 000000000..19f39b1d9 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe_trusted.sol @@ -0,0 +1,43 @@ +contract State { + C c; + constructor(C _c) { + c = _c; + } + function f() public returns (uint) { + c.setOwner(address(0)); + return c.g(); + } +} + +contract C { + address owner; + uint y; + State s; + + constructor() { + owner = msg.sender; + s = new State(this); + } + + function setOwner(address _owner) public { + owner = _owner; + } + + function f() public { + address prevOwner = owner; + uint z = s.f(); + assert(z == y); // should hold + assert(prevOwner == owner); // should not hold because of reentrancy + } + + function g() public view returns (uint) { + return y; + } +} +// ==== +// SMTContract: C +// SMTEngine: chc +// SMTExtCalls: trusted +// ---- +// Warning 6328: (396-410): CHC: Assertion violation might happen here. +// Warning 6328: (429-455): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol new file mode 100644 index 000000000..10d9dd709 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_trusted.sol @@ -0,0 +1,35 @@ +contract State { + uint x; + function f() public returns (uint) { + if (x == 0) x = 1; + else if (x == 1) x = 2; + else if (x == 2) x = 0; + return x; + } +} + +contract C { + address owner; + uint y; + uint z; + State s; + + constructor() { + s = new State(); + owner = msg.sender; + } + + function f() public { + address prevOwner = owner; + y = s.f(); + z = s.f(); + assert(prevOwner == owner); + assert(y != z); + } +} +// ==== +// SMTContract: C +// SMTEngine: chc +// SMTExtCalls: trusted +// ---- +// Warning 6328: (385-399): CHC: Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe_trusted.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe_trusted.sol new file mode 100644 index 000000000..7d217e145 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe_trusted.sol @@ -0,0 +1,40 @@ +contract State { + uint x; + function f() public returns (uint) { + if (x == 0) x = 1; + else if (x == 1) x = 2; + else if (x == 2) x = 0; + return x; + } +} + +contract C { + address owner; + uint y; + uint z; + State s; + + constructor() { + owner = msg.sender; + s = new State(); + } + + function setOwner(address _owner) public { + owner = _owner; + } + + function f() public { + address prevOwner = owner; + y = s.f(); + z = s.f(); + assert(prevOwner == owner); + assert(y != z); + } +} +// ==== +// SMTContract: C +// SMTEngine: chc +// SMTExtCalls: trusted +// ---- +// Warning 6328: (421-447): CHC: Assertion violation might happen here. +// Warning 6328: (451-465): CHC: Assertion violation might happen here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/token_trusted_transfer_correct.sol b/test/libsolidity/smtCheckerTests/external_calls/token_trusted_transfer_correct.sol new file mode 100644 index 000000000..438feae21 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/token_trusted_transfer_correct.sol @@ -0,0 +1,64 @@ +interface Token { + function balanceOf(address _a) external view returns (uint); + function transfer(address _to, uint _amt) external; +} + +contract TokenCorrect is Token { + mapping (address => uint) balance; + constructor(address _a, uint _b) { + balance[_a] = _b; + } + function balanceOf(address _a) public view override returns (uint) { + return balance[_a]; + } + function transfer(address _to, uint _amt) public override { + require(balance[msg.sender] >= _amt); + balance[msg.sender] -= _amt; + balance[_to] += _amt; + } +} + +contract Test { + function property_transfer(address _token, address _to, uint _amt) public { + require(_to != address(this)); + + TokenCorrect t = TokenCorrect(_token); + + uint xPre = t.balanceOf(address(this)); + require(xPre >= _amt); + uint yPre = t.balanceOf(_to); + + t.transfer(_to, _amt); + uint xPost = t.balanceOf(address(this)); + uint yPost = t.balanceOf(_to); + + assert(xPost == xPre - _amt); + assert(yPost == yPre + _amt); + } + + function test_concrete() public { + TokenCorrect t = new TokenCorrect(address(this), 1000); + + uint b = t.balanceOf(address(this)); + assert(b == 1000); + + address other = address(0x333); + require(address(this) != other); + + uint c = t.balanceOf(other); + assert(c == 0); + + t.transfer(other, 100); + + uint d = t.balanceOf(address(this)); + assert(d == 900); + + uint e = t.balanceOf(other); + assert(e == 100); + } +} +// ==== +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTContract: Test +// SMTTargets: assert diff --git a/test/libsolidity/smtCheckerTests/external_calls/token_trusted_transfer_wrong.sol b/test/libsolidity/smtCheckerTests/external_calls/token_trusted_transfer_wrong.sol new file mode 100644 index 000000000..6bb6074b2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/token_trusted_transfer_wrong.sol @@ -0,0 +1,68 @@ +interface Token { + function balanceOf(address _a) external view returns (uint); + function transfer(address _to, uint _amt) external; +} + +contract TokenWrong is Token { + mapping (address => uint) balance; + constructor(address _a, uint _b) { + balance[_a] = _b; + } + function balanceOf(address _a) public view override returns (uint) { + return balance[_a]; + } + function transfer(address _to, uint _amt) public override { + require(balance[msg.sender] >= _amt); + // Commented out to make this token implementation wrong. + //balance[msg.sender] -= _amt; + balance[_to] += _amt; + } +} + +contract Test { + function property_transfer(address _token, address _to, uint _amt) public { + require(_to != address(this)); + + TokenWrong t = TokenWrong(_token); + + uint xPre = t.balanceOf(address(this)); + require(xPre >= _amt); + uint yPre = t.balanceOf(_to); + + t.transfer(_to, _amt); + uint xPost = t.balanceOf(address(this)); + uint yPost = t.balanceOf(_to); + + assert(xPost == xPre - _amt); // should fail + assert(yPost == yPre + _amt); + } + + function test_concrete() public { + TokenWrong t = new TokenWrong(address(this), 1000); + + uint b = t.balanceOf(address(this)); + assert(b == 1000); + + address other = address(0x333); + require(address(this) != other); + + uint c = t.balanceOf(other); + assert(c == 0); + + t.transfer(other, 100); + + uint d = t.balanceOf(address(this)); + assert(d == 900); // should fail + + uint e = t.balanceOf(other); + assert(e == 100); + } +} +// ==== +// SMTContract: Test +// SMTEngine: chc +// SMTExtCalls: trusted +// SMTTargets: assert +// ---- +// Warning 6328: (950-978): CHC: Assertion violation happens here. +// Warning 6328: (1370-1386): CHC: Assertion violation happens here.