From d9eaad91a75afe94cb0eeafb500cfd2662b39bd5 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 24 Sep 2024 16:26:26 -0700 Subject: [PATCH] chore: update halmos.toml example + add missing tests (#371) --- tests/expected/all.json | 11 +++ tests/lib/halmos-cheatcodes | 2 +- tests/regression/halmos.toml | 16 ++++- tests/regression/test/Concretization.t.sol | 79 ++++++++++++++++++++++ 4 files changed, 106 insertions(+), 2 deletions(-) create mode 100644 tests/regression/test/Concretization.t.sol diff --git a/tests/expected/all.json b/tests/expected/all.json index e624f9d2..3e9e2fde 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -336,6 +336,17 @@ "num_bounded_loops": null } ], + "test/Concretization.t.sol:ConcretizationTest": [ + { + "name": "check_custom_calldata_decoding()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], "test/Console.t.sol:ConsoleTest": [ { "name": "check_log_address()", diff --git a/tests/lib/halmos-cheatcodes b/tests/lib/halmos-cheatcodes index c75b36d4..a02072cd 160000 --- a/tests/lib/halmos-cheatcodes +++ b/tests/lib/halmos-cheatcodes @@ -1 +1 @@ -Subproject commit c75b36d4bbc3c7b5d1293350b486474f976cd2b4 +Subproject commit a02072cd5eb8560d00c3f4a73b27831ec6e3137e diff --git a/tests/regression/halmos.toml b/tests/regression/halmos.toml index 5254d685..d2841e90 100644 --- a/tests/regression/halmos.toml +++ b/tests/regression/halmos.toml @@ -1,3 +1,11 @@ +# ___ ___ ___ ___ ___ ___ +# /\__\ /\ \ /\__\ /\__\ /\ \ /\ \ +# /:/__/_ /::\ \ /:/ / /::L_L_ /::\ \ /::\ \ +# /::\/\__\ /::\:\__\ /:/__/ /:/L:\__\ /:/\:\__\ /\:\:\__\ +# \/\::/ / \/\::/ / \:\ \ \/_/:/ / \:\/:/ / \:\:\/__/ +# /:/ / /:/ / \:\__\ /:/ / \::/ / \::/ / +# \/__/ \/__/ \/__/ \/__/ \/__/ \/__/ + [global] # run tests in the given contract @@ -28,6 +36,9 @@ depth = 0 # set the length of dynamic-sized arrays including bytes and string (default: loop unrolling bound) # array-lengths = NAME1=LENGTH1,NAME2=LENGTH2,... +# set the default length candidates for bytes and string not specified in --array-lengths +default-bytes-lengths = "0,1024,65" + # Select one of the available storage layout models # The generic model should only be necessary for vyper, huff, or unconventional storage patterns in yul. storage-layout = "solidity" @@ -102,7 +113,7 @@ smt-exp-by-const = 2 solver-timeout-branching = 1 # set timeout (in milliseconds) for solving assertion violation conditions; 0 means no timeout -solver-timeout-assertion = 1000 +solver-timeout-assertion = 60000 # set memory limit (in megabytes) for the solver; 0 means no limit solver-max-memory = 0 @@ -113,6 +124,9 @@ solver-max-memory = 0 # set the number of threads for parallel solvers # solver-threads = N +# cache unsat queries using unsat cores +cache-solver = false + ################################################################################ # Experimental options # ################################################################################ diff --git a/tests/regression/test/Concretization.t.sol b/tests/regression/test/Concretization.t.sol new file mode 100644 index 00000000..751ae632 --- /dev/null +++ b/tests/regression/test/Concretization.t.sol @@ -0,0 +1,79 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity >=0.8.0 <0.9.0; + +import "forge-std/Test.sol"; +import {SymTest} from "halmos-cheatcodes/SymTest.sol"; + +contract C1 { + function foo(bytes calldata data) external { + uint offset; + uint size; + // This simulates custom calldata decoding: + // 1. Copy static portion of calldata into memory + // 2. Read offset and size from the copied memory + // 3. Copy the actual data using calldatacopy + assembly { + // Copy the first 68 bytes of calldata into memory + // This includes: + // - 4 bytes for function selector + // - 32 bytes for offset + // - 32 bytes for size + calldatacopy(0, 0, 68) + + // Read offset and size from copied memory + // Note: Proper concretization is crucial here. + // Without it, reading the size would fail due to a symbolic memory offset. + offset := mload(4) + size := mload(add(4, offset)) + + // Copy the actual data portion + calldatacopy(68, 68, size) + + // Return the decoded data + return(4, add(size, 64)) + } + } +} + +contract C2 { + function foo(bytes calldata data) external returns (bytes memory) { + uint offset; + uint size; + // This simulates standard calldata decoding: + // 1. Read offset and size directly from calldata using calldataload + // 2. Copy the entire calldata into memory + // 3. Copy the actual data portion + assembly { + // Read offset and size directly from calldata + offset := calldataload(4) + size := calldataload(add(4, offset)) + + // Copy the first 68 bytes of calldata into memory + calldatacopy(0, 0, 68) + + // Copy the actual data portion + calldatacopy(68, 68, size) + + // Return the decoded data + return(4, add(size, 64)) + } + } +} + +contract ConcretizationTest is SymTest, Test { + address c1; + address c2; + + function setUp() public { + c1 = address(new C1()); + c2 = address(new C2()); + } + + function check_custom_calldata_decoding() public { + bytes memory data = svm.createCalldata("Concretization.t.sol", "C1"); + (bool success1, bytes memory retdata1) = c1.call(data); + (bool success2, bytes memory retdata2) = c2.call(data); + assertEq(success1, success2); + assertEq(retdata1, retdata2); + } +}