Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
add calldata tests for nested arrays
Browse files Browse the repository at this point in the history
daejunpark committed Sep 13, 2024
1 parent 37c7423 commit 36bbc3f
Showing 2 changed files with 178 additions and 68 deletions.
128 changes: 74 additions & 54 deletions tests/expected/all.json
Original file line number Diff line number Diff line change
@@ -1203,16 +1203,16 @@
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Beep_1_excluding_pure()",
"exitcode": 4,
"name": "check_createInt()",
"exitcode": 0,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Beep_1_including_pure()",
"name": "check_createInt256()",
"exitcode": 0,
"num_models": 0,
"models": null,
@@ -1221,16 +1221,16 @@
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Beep_2_excluding_pure()",
"exitcode": 4,
"name": "check_createString()",
"exitcode": 0,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Beep_2_including_pure()",
"name": "check_createUint()",
"exitcode": 0,
"num_models": 0,
"models": null,
@@ -1239,52 +1239,54 @@
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Dummy_fail()",
"exitcode": 3,
"name": "check_createUint256()",
"exitcode": 0,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Fallback()",
"exitcode": 0,
"num_models": 0,
"name": "check_enableSymbolicStorage_fail()",
"exitcode": 1,
"num_models": 1,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_1_fail()",
"exitcode": 1,
"num_models": 40,
"name": "check_enableSymbolicStorage_nonexistent()",
"exitcode": 3,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_1_pass()",
"name": "check_enableSymbolicStorage_pass(uint256)",
"exitcode": 0,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
}
],
"test/HalmosCheatCode.t.sol:HalmosCreateCalldataTest": [
{
"name": "check_createCalldata_Mock_2_excluding_view_fail()",
"exitcode": 1,
"num_models": 40,
"name": "check_createCalldata_Beep_1_excluding_pure()",
"exitcode": 4,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_2_excluding_view_pass()",
"name": "check_createCalldata_Beep_1_including_pure()",
"exitcode": 0,
"num_models": 0,
"models": null,
@@ -1293,16 +1295,16 @@
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_2_including_view_fail()",
"exitcode": 1,
"num_models": 42,
"name": "check_createCalldata_Beep_2_excluding_pure()",
"exitcode": 4,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_2_including_view_pass()",
"name": "check_createCalldata_Beep_2_including_pure()",
"exitcode": 0,
"num_models": 0,
"models": null,
@@ -1311,16 +1313,16 @@
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_3_fail()",
"exitcode": 1,
"num_models": 40,
"name": "check_createCalldata_Dummy_fail()",
"exitcode": 3,
"num_models": 0,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_3_pass()",
"name": "check_createCalldata_Fallback()",
"exitcode": 0,
"num_models": 0,
"models": null,
@@ -1329,16 +1331,16 @@
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_4_excluding_view_fail()",
"name": "check_createCalldata_Mock_1_fail()",
"exitcode": 1,
"num_models": 40,
"num_models": 18,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_4_excluding_view_pass()",
"name": "check_createCalldata_Mock_1_pass()",
"exitcode": 0,
"num_models": 0,
"models": null,
@@ -1347,16 +1349,16 @@
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_4_including_view_fail()",
"name": "check_createCalldata_Mock_2_excluding_view_fail()",
"exitcode": 1,
"num_models": 42,
"num_models": 18,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_4_including_view_pass()",
"name": "check_createCalldata_Mock_2_excluding_view_pass()",
"exitcode": 0,
"num_models": 0,
"models": null,
@@ -1365,16 +1367,16 @@
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_interface_excluding_view_fail()",
"name": "check_createCalldata_Mock_2_including_view_fail()",
"exitcode": 1,
"num_models": 40,
"num_models": 20,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_interface_excluding_view_pass()",
"name": "check_createCalldata_Mock_2_including_view_pass()",
"exitcode": 0,
"num_models": 0,
"models": null,
@@ -1383,16 +1385,16 @@
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_interface_including_view_fail()",
"name": "check_createCalldata_Mock_3_fail()",
"exitcode": 1,
"num_models": 42,
"num_models": 18,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_interface_including_view_pass()",
"name": "check_createCalldata_Mock_3_pass()",
"exitcode": 0,
"num_models": 0,
"models": null,
@@ -1401,16 +1403,16 @@
"num_bounded_loops": null
},
{
"name": "check_createInt()",
"exitcode": 0,
"num_models": 0,
"name": "check_createCalldata_Mock_4_excluding_view_fail()",
"exitcode": 1,
"num_models": 18,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createInt256()",
"name": "check_createCalldata_Mock_4_excluding_view_pass()",
"exitcode": 0,
"num_models": 0,
"models": null,
@@ -1419,16 +1421,16 @@
"num_bounded_loops": null
},
{
"name": "check_createString()",
"exitcode": 0,
"num_models": 0,
"name": "check_createCalldata_Mock_4_including_view_fail()",
"exitcode": 1,
"num_models": 20,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createUint()",
"name": "check_createCalldata_Mock_4_including_view_pass()",
"exitcode": 0,
"num_models": 0,
"models": null,
@@ -1437,7 +1439,16 @@
"num_bounded_loops": null
},
{
"name": "check_createUint256()",
"name": "check_createCalldata_Mock_interface_excluding_view_fail()",
"exitcode": 1,
"num_models": 18,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_Mock_interface_excluding_view_pass()",
"exitcode": 0,
"num_models": 0,
"models": null,
@@ -1446,25 +1457,34 @@
"num_bounded_loops": null
},
{
"name": "check_enableSymbolicStorage_fail()",
"name": "check_createCalldata_Mock_interface_including_view_fail()",
"exitcode": 1,
"num_models": 1,
"num_models": 20,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_enableSymbolicStorage_nonexistent()",
"exitcode": 3,
"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_enableSymbolicStorage_pass(uint256)",
"name": "check_createCalldata_NestedArrays_1_fail()",
"exitcode": 1,
"num_models": 541,
"models": null,
"num_paths": null,
"time": null,
"num_bounded_loops": null
},
{
"name": "check_createCalldata_NestedArrays_1_pass()",
"exitcode": 0,
"num_models": 0,
"models": null,
118 changes: 104 additions & 14 deletions tests/regression/test/HalmosCheatCode.t.sol
Original file line number Diff line number Diff line change
@@ -138,7 +138,10 @@ contract HalmosCheatCodeTest is SymTest, Test {
// symbolic storage is not allowed for a nonexistent account
svm.enableSymbolicStorage(address(0xdeadbeef)); // HalmosException
}
}

/// @custom:halmos --default-bytes-lengths 0,65
contract HalmosCreateCalldataTest is SymTest, Test {
function check_createCalldata_Beep_1_excluding_pure() public {
bytes memory data = svm.createCalldata("HalmosCheatCode.t.sol", "Beep");
_check_createCalldata_Beep(data); // fail because the only function in Beep is pure, which is excluded in createCalldata()
@@ -240,8 +243,12 @@ contract HalmosCheatCodeTest is SymTest, Test {
}

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);
Mock target = new Mock(false); // use Mock(true) for debugging
_check_createCalldata_generic(address(target), data, pass);
}

function _check_createCalldata_generic(address target, bytes memory data, bool pass) public {
(bool success, bytes memory retdata) = target.call(data);
vm.assume(success);

bytes4 ret = abi.decode(retdata, (bytes4));
@@ -256,6 +263,21 @@ contract HalmosCheatCodeTest is SymTest, Test {
}
}

function check_createCalldata_NestedArrays_1_pass() public {
bytes memory data = svm.createCalldata("NestedArrays");
_check_createCalldata_NestedArrays(data, true);
}

function check_createCalldata_NestedArrays_1_fail() public {
bytes memory data = svm.createCalldata("NestedArrays");
_check_createCalldata_NestedArrays(data, false);
}

function _check_createCalldata_NestedArrays(bytes memory data, bool pass) public {
NestedArrays target = new NestedArrays(false); // use NestedArrays(true) for debugging
_check_createCalldata_generic(address(target), data, pass);
}

function check_createCalldata_Dummy_fail() public {
// fail due to ambiguity of Dummy
bytes memory data = svm.createCalldata("Dummy");
@@ -301,45 +323,113 @@ contract Mock {

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

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

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

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

contract NestedArrays {
bool log;

constructor (bool _log) {
log = _log;
}

struct BytesBytes {
bytes b1;
bytes b2;
}

struct UintBytesBytesArray {
uint256 u1;
BytesBytes[] u2;
}

struct UintBytesArray {
uint256 u1;
bytes[] u2;
}

// TODO: test nested arrays, e.g.:
// "bulkAddKeysForMigration((uint256,(bytes,bytes)[])[])": "708e9c70",
// "bulkResetKeysForMigration((uint256,bytes[])[])": "46b3f429",
function f_bytes_bytes_array(BytesBytes[] memory x) public returns (bytes4) {
if (log) {
console.log("f((bytes,bytes)[])");
console.log(x.length); // 0, 1, 2
// 21 (= 1 + 4 + 4*4) combinations
for (uint i = 0; i < x.length; i++) {
// 4 (= 2*2) combinations
console.log(x[i].b1.length); // 0, 65
console.log(x[i].b2.length); // 0, 65
}
}
return this.f_bytes_bytes_array.selector;
}

function f_bytes_bytes_array_array(UintBytesBytesArray[] memory x) public returns (bytes4) {
if (log) {
console.log("f((uint256,(bytes,bytes)[])[])");
console.log(x.length); // 0, 1, 2
// 463 (= 1 + 21 + 21*21) combinations
for (uint i = 0; i < x.length; i++) {
// 21 (= 1 + 4 + 4*4) combinations
console.log(x[i].u2.length); // 0, 1, 2
for (uint j = 0; j < x[i].u2.length; j++) {
// 4 (= 2*2) combinations
console.log(x[i].u2[j].b1.length); // 0, 65
console.log(x[i].u2[j].b2.length); // 0, 65
}
}
}
return this.f_bytes_bytes_array_array.selector;
}

function f_bytes_array_array(UintBytesArray[] memory x) public returns (bytes4) {
if (log) {
console.log("f((uint256,bytes[])[])");
console.log(x.length); // 0, 1, 2
// 57 (= 1 + 7 + 7*7) combinations
for (uint i = 0; i < x.length; i++) {
// 7 (= 1 + 2 + 2*2) combinations
console.log(x[i].u2.length); // 0, 1, 2
for (uint j = 0; j < x[i].u2.length; j++) {
// 2 combinations
console.log(x[i].u2[j].length); // 0, 65
}
}
}
return this.f_bytes_array_array.selector;
}
}

interface IMock {

0 comments on commit 36bbc3f

Please sign in to comment.