chore: update halmos.toml example + add missing tests (a16z#371)

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()",

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                             #
 ################################################################################

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);
+    }
+}