Skip to content

Commit

Permalink
improve calldata tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@daejunpark
daejunpark committed Sep 13, 2024
1 parent 0b3847d commit 69d3b7e
Show file tree
Hide file tree
Showing 2 changed files with 163 additions and 42 deletions.
88 changes: 80 additions & 8 deletions tests/expected/all.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1257,7 +1257,7 @@
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_1()",
"name": "check_createCalldata_Mock_1_fail()",
"exitcode": 1,
"num_models": 40,
"models": null,
Expand All @@ -1266,7 +1266,16 @@
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_2_excluding_view()",
"name": "check_createCalldata_Mock_1_pass()",
"exitcode": 0,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_2_excluding_view_fail()",
"exitcode": 1,
"num_models": 40,
"models": null,
Expand All @@ -1275,7 +1284,16 @@
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_2_including_view()",
"name": "check_createCalldata_Mock_2_excluding_view_pass()",
"exitcode": 0,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_2_including_view_fail()",
"exitcode": 1,
"num_models": 42,
"models": null,
Expand All @@ -1284,7 +1302,16 @@
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_3()",
"name": "check_createCalldata_Mock_2_including_view_pass()",
"exitcode": 0,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_3_fail()",
"exitcode": 1,
"num_models": 40,
"models": null,
Expand All @@ -1293,7 +1320,16 @@
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_4_excluding_view()",
"name": "check_createCalldata_Mock_3_pass()",
"exitcode": 0,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_4_excluding_view_fail()",
"exitcode": 1,
"num_models": 40,
"models": null,
Expand All @@ -1302,7 +1338,16 @@
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_4_including_view()",
"name": "check_createCalldata_Mock_4_excluding_view_pass()",
"exitcode": 0,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_4_including_view_fail()",
"exitcode": 1,
"num_models": 42,
"models": null,
Expand All @@ -1311,7 +1356,16 @@
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_interface_excluding_view()",
"name": "check_createCalldata_Mock_4_including_view_pass()",
"exitcode": 0,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_interface_excluding_view_fail()",
"exitcode": 1,
"num_models": 40,
"models": null,
Expand All @@ -1320,14 +1374,32 @@
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_interface_including_view()",
"name": "check_createCalldata_Mock_interface_excluding_view_pass()",
"exitcode": 0,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_interface_including_view_fail()",
"exitcode": 1,
"num_models": 42,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_interface_including_view_pass()",
"exitcode": 0,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createInt()",
"exitcode": 0,
Expand Down
117 changes: 83 additions & 34 deletions tests/regression/test/HalmosCheatCode.t.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -167,57 +167,92 @@ contract HalmosCheatCodeTest is SymTest, Test {
assertEq(ret, 42);
}

function check_createCalldata_Mock_1() public {
function check_createCalldata_Mock_1_pass() public {
bytes memory data = svm.createCalldata("Mock");
_check_createCalldata_Mock(data);
_check_createCalldata_Mock(data, true);
}
function check_createCalldata_Mock_1_fail() public {
bytes memory data = svm.createCalldata("Mock");
_check_createCalldata_Mock(data, false);
}

function check_createCalldata_Mock_2_excluding_view() public {
function check_createCalldata_Mock_2_excluding_view_pass() public {
bytes memory data = svm.createCalldata("Mock", false);
_check_createCalldata_Mock(data, true);
}
function check_createCalldata_Mock_2_excluding_view_fail() public {
bytes memory data = svm.createCalldata("Mock", false);
_check_createCalldata_Mock(data);
_check_createCalldata_Mock(data, false);
}

function check_createCalldata_Mock_2_including_view() public {
function check_createCalldata_Mock_2_including_view_pass() public {
bytes memory data = svm.createCalldata("Mock", true);
_check_createCalldata_Mock(data, true);
}
function check_createCalldata_Mock_2_including_view_fail() public {
bytes memory data = svm.createCalldata("Mock", true);
_check_createCalldata_Mock(data);
_check_createCalldata_Mock(data, false);
}

function check_createCalldata_Mock_3() public {
function check_createCalldata_Mock_3_pass() public {
bytes memory data = svm.createCalldata("HalmosCheatCode.t.sol", "Mock");
_check_createCalldata_Mock(data);
_check_createCalldata_Mock(data, true);
}
function check_createCalldata_Mock_3_fail() public {
bytes memory data = svm.createCalldata("HalmosCheatCode.t.sol", "Mock");
_check_createCalldata_Mock(data, false);
}

function check_createCalldata_Mock_4_excluding_view() public {
function check_createCalldata_Mock_4_excluding_view_pass() public {
bytes memory data = svm.createCalldata("HalmosCheatCode.t.sol", "Mock", false);
_check_createCalldata_Mock(data);
_check_createCalldata_Mock(data, true);
}
function check_createCalldata_Mock_4_excluding_view_fail() public {
bytes memory data = svm.createCalldata("HalmosCheatCode.t.sol", "Mock", false);
_check_createCalldata_Mock(data, false);
}

function check_createCalldata_Mock_4_including_view() public {
function check_createCalldata_Mock_4_including_view_pass() public {
bytes memory data = svm.createCalldata("HalmosCheatCode.t.sol", "Mock", true);
_check_createCalldata_Mock(data, true);
}
function check_createCalldata_Mock_4_including_view_fail() public {
bytes memory data = svm.createCalldata("HalmosCheatCode.t.sol", "Mock", true);
_check_createCalldata_Mock(data);
_check_createCalldata_Mock(data, false);
}

function check_createCalldata_Mock_interface_excluding_view() public {
function check_createCalldata_Mock_interface_excluding_view_pass() public {
bytes memory data = svm.createCalldata("IMock");
_check_createCalldata_Mock(data, true);
}
function check_createCalldata_Mock_interface_excluding_view_fail() public {
bytes memory data = svm.createCalldata("IMock");
_check_createCalldata_Mock(data);
_check_createCalldata_Mock(data, false);
}

function check_createCalldata_Mock_interface_including_view() public {
function check_createCalldata_Mock_interface_including_view_pass() public {
bytes memory data = svm.createCalldata("IMock", true);
_check_createCalldata_Mock(data);
_check_createCalldata_Mock(data, true);
}
function check_createCalldata_Mock_interface_including_view_fail() public {
bytes memory data = svm.createCalldata("IMock", true);
_check_createCalldata_Mock(data, false);
}

function _check_createCalldata_Mock(bytes memory data) public {
Mock mock = new Mock();
function _check_createCalldata_Mock(bytes memory data, bool pass) public {
Mock mock = new Mock(false); // use Mock(true) for debugging
(bool success, bytes memory retdata) = address(mock).call(data);
vm.assume(success);

bytes4 ret = abi.decode(retdata, (bytes4));
bytes4 expected = bytes4(bytes.concat(data[0], data[1], data[2], data[3]));

// the number of calldata generated == the # of counterexamples
if (ret == expected) {
assert(false);
if (pass) {
assertEq(ret, expected);
} else {
// NOTE: the purpose of fail mode is to count the number of calldata combinations,
// where the number of calldata combinations is equal to the # of counterexamples.
assertNotEq(ret, expected);
}
}

Expand Down Expand Up @@ -250,6 +285,12 @@ contract Fallback {
}

contract Mock {
bool log;

constructor (bool _log) {
log = _log;
}

function f_pure() public pure returns (bytes4) {
return this.f_pure.selector;
}
Expand All @@ -259,31 +300,39 @@ contract Mock {
}

function foo(uint[] memory x) public returns (bytes4) {
console.log("foo");
console.log(x.length); // 0, 1, 2
if (log) {
console.log("foo");
console.log(x.length); // 0, 1, 2
}
return this.foo.selector;
}

function bar(bytes memory x) public returns (bytes4) {
console.log("bar");
console.log(x.length); // 0, 32, 65, 1024
if (log) {
console.log("bar");
console.log(x.length); // 0, 32, 65, 1024
}
return this.bar.selector;
}

function zoo(uint[] memory x, bytes memory y) public returns (bytes4) {
console.log("zoo");
// 12 (= 3 * 4) combinations
console.log(x.length); // 0, 1, 2
console.log(y.length); // 0, 32, 65, 1024
if (log) {
console.log("zoo");
// 12 (= 3 * 4) combinations
console.log(x.length); // 0, 1, 2
console.log(y.length); // 0, 32, 65, 1024
}
return this.zoo.selector;
}

function foobar(bytes[] memory x) public returns (bytes4) {
console.log("foobar");
// 21 (= 16+4+1) combinations
console.log(x.length); // 0, 1, 2
for (uint i = 0; i < x.length; i++) {
console.log(x[i].length); // 0, 32, 65, 1024
if (log) {
console.log("foobar");
// 21 (= 16+4+1) combinations
console.log(x.length); // 0, 1, 2
for (uint i = 0; i < x.length; i++) {
console.log(x[i].length); // 0, 32, 65, 1024
}
}
return this.foobar.selector;
}
Expand Down

0 comments on commit 69d3b7e

Please sign in to comment.