From 69d3b7e35c29fff54c8565aa1bb10eff4ca29b46 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Fri, 13 Sep 2024 10:40:58 -0700 Subject: [PATCH] improve calldata tests --- tests/expected/all.json | 88 +++++++++++++-- tests/regression/test/HalmosCheatCode.t.sol | 117 ++++++++++++++------ 2 files changed, 163 insertions(+), 42 deletions(-) diff --git a/tests/expected/all.json b/tests/expected/all.json index 7beb7f73..ad129a39 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -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, @@ -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, @@ -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, @@ -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, @@ -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, @@ -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, @@ -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, @@ -1320,7 +1374,16 @@ "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, @@ -1328,6 +1391,15 @@ "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, diff --git a/tests/regression/test/HalmosCheatCode.t.sol b/tests/regression/test/HalmosCheatCode.t.sol index 7d1a4d52..53f01c70 100644 --- a/tests/regression/test/HalmosCheatCode.t.sol +++ b/tests/regression/test/HalmosCheatCode.t.sol @@ -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); } } @@ -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; } @@ -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; }