Skip to content

SMTChecker: Further test simplifications #15256

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
blishko merged 1 commit into from
Jul 15, 2024
Merged

SMTChecker: Further test simplifications #15256

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 3 additions & 5 deletions test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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; }
}

Expand All @@ -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.
24 changes: 9 additions & 15 deletions ...heckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect_trusted.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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();
}
}
Expand All @@ -29,7 +23,7 @@ contract C {

constructor() {
owner = msg.sender;
s = new State(this);
s = new State();
}

function setOwner(address _owner) public {
Expand All @@ -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
}
Expand All @@ -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.
8 changes: 4 additions & 4 deletions test/libsolidity/smtCheckerTests/external_calls/external_inc.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
5 changes: 2 additions & 3 deletions test/libsolidity/smtCheckerTests/external_calls/external_safe.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
10 changes: 2 additions & 8 deletions test/libsolidity/smtCheckerTests/types/array_branches_3d.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,12 +15,6 @@ contract C
}
// ====
// SMTEngine: all
// SMTIgnoreOS: macos
// SMTTargets: assert
Copy link
Collaborator Author

@blishko blishko Jul 11, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The out of bounds checks seem to be difficult for Z3, but there is no point to test them, they are safe.
The point of this test is to test the assertion.

// ----
// 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.
27 changes: 0 additions & 27 deletions test/libsolidity/smtCheckerTests/types/array_branches_3d_show_unproved.sol
View file
Open in desktop
Copy link
Collaborator Author

@blishko blishko Jul 11, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The only difference between this file and array_branches_3d.sol was that this has an option SMTShowUnproved: yes, but that is actually the default for that option, so this test was identical to the other one.
We can delete it without losing anything.

This file was deleted.

10 changes: 5 additions & 5 deletions test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_1.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Copy link
Collaborator Author

@blishko blishko Jul 10, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems the problem with aliasing of maps had been fixed somewhere along the way, because no oob was reported here anymore.

severalMaps[0][0] = 42;
severalMaps8[0][0] = 42;
severalMaps3d[0][0][0] = 42;
Expand All @@ -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);
Expand All @@ -26,6 +24,8 @@ contract C
// ====
// SMTEngine: all
// SMTIgnoreCex: yes
// SMTTargets: assert
Copy link
Collaborator Author

@blishko blishko Jul 10, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In this test, we want to focus on assertions, not the accesses.

// ----
// 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.
12 changes: 4 additions & 8 deletions test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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);
}
Expand All @@ -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.