add ffi cheatcode

.github/workflows/test-external.yml

@@ -28,8 +28,8 @@ jobs:
             branch: ""
           - repo: "farcasterxyz/contracts"
             dir: "farcaster-contracts"
-            cmd: "halmos --function check"
-            branch: "test/halmos"
+            cmd: "halmos"
+            branch: ""
           - repo: "zobront/halmos-solady"
             dir: "halmos-solady"
             cmd: "halmos --function testCheck"

.github/workflows/test-ffi.yml

@@ -0,0 +1,41 @@
+name: Test FFI
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+    branches: [main]
+
+jobs:
+  test:
+    runs-on: macos-latest
+
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+        - testname: "ffi:tests"
+
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+
+      - name: Set up Python
+        uses: actions/setup-python@v4
+        with:
+          python-version: "3.11"
+
+      - name: Install dependencies
+        run: |
+          python -m pip install --upgrade pip
+          pip install pytest
+
+      - name: Install Halmos
+        run: pip install -e .
+
+      - name: Run pytest
+        run: pytest -v tests/test_halmos.py -k ${{ matrix.testname }} --halmos-options="--ffi -v -st --error-unknown --test-parallel --solver-parallel --solver-timeout-assertion 0"

.github/workflows/test.yml

@@ -42,4 +42,4 @@ jobs:
         run: pip install -e .
 
       - name: Run pytest
-        run: pytest -v -k "not long" --halmos-options="-v -st --error-unknown ${{ matrix.parallel }} --solver-timeout-assertion 0"
+        run: pytest -v -k "not long and not ffi" --halmos-options="-v -st --error-unknown ${{ matrix.parallel }} --solver-timeout-assertion 0"

src/halmos/__main__.py

@@ -890,6 +890,7 @@ def mk_options(args: Namespace) -> Dict:
         "sym_jump": args.symbolic_jump,
         "print_steps": args.print_steps,
         "unknown_calls_return_size": args.return_size_of_unknown_calls,
+        "ffi": args.ffi,
     }
 
     if args.width is not None:

src/halmos/cheatcodes.py

@@ -151,6 +151,9 @@ class hevm_cheat_code:
     # bytes4(keccak256("etch(address,bytes)"))
     etch_sig: int = 0xB4D6C782
 
+    # bytes4(keccak256("ffi(string[])"))
+    ffi_sig: int = 0x89160467
+
 
 class console:
     # address constant CONSOLE_ADDRESS = address(0x000000000000000000636F6e736F6c652e6c6f67);

src/halmos/parser.py

@@ -75,6 +75,12 @@ def mk_arg_parser() -> argparse.ArgumentParser:
         help="do not run the constructor of test contracts",
     )
 
+    parser.add_argument(
+        "--ffi",
+        action="store_true",
+        help="allow the usage of FFI to call external functions",
+    )
+
     parser.add_argument(
         "--version", action="store_true", help="print the version number"
     )

src/halmos/sevm.py

@@ -4,6 +4,8 @@
 import math
 import re
 
+from subprocess import Popen, PIPE
+
 from copy import deepcopy
 from collections import defaultdict
 from typing import List, Set, Dict, Union as UnionType, Tuple, Any, Optional
@@ -27,6 +29,7 @@
     UNSUPPORTED_OPCODE,
     LIBRARY_PLACEHOLDER,
     UNINTERPRETED_UNKNOWN_CALLS,
+    INTERNAL_ERROR,
 )
 
 Word = Any  # z3 expression (including constants)
@@ -410,6 +413,52 @@ def extract_string_argument(calldata: BitVecRef, arg_idx: int):
     return string_bytes.decode("utf-8")
 
 
+def extract_string_array_argument(calldata: BitVecRef, arg_idx: int):
+    """Extracts idx-th argument of string array from calldata"""
+
+    array_slot = int_of(extract_bytes(calldata, 4 + 32 * arg_idx, 32))
+    num_strings = int_of(extract_bytes(calldata, 4 + array_slot, 32))
+
+    string_array = []
+
+    for i in range(num_strings):
+        string_offset = int_of(
+            extract_bytes(calldata, 4 + array_slot + 32 * (i + 1), 32)
+        )
+        string_length = int_of(
+            extract_bytes(calldata, 4 + array_slot + 32 + string_offset, 32)
+        )
+        string_value = int_of(
+            extract_bytes(
+                calldata, 4 + array_slot + 32 + string_offset + 32, string_length
+            )
+        )
+        string_bytes = string_value.to_bytes(string_length, "big")
+        string_array.append(string_bytes.decode("utf-8"))
+
+    return string_array
+
+
+def stringified_bytes_to_bytes(string_bytes: str):
+    """Converts a string of bytes to a bytes memory type"""
+
+    string_bytes_len = (len(string_bytes) + 1) // 2
+    string_bytes_len_enc = hex(string_bytes_len).replace("0x", "").rjust(64, "0")
+
+    string_bytes_len_ceil = (string_bytes_len + 31) // 32 * 32
+
+    ret_bytes = (
+        "00" * 31
+        + "20"
+        + string_bytes_len_enc
+        + string_bytes.ljust(string_bytes_len_ceil * 2, "0")
+    )
+    ret_len = len(ret_bytes) // 2
+    ret_bytes = bytes.fromhex(ret_bytes)
+
+    return BitVecVal(int.from_bytes(ret_bytes, "big"), ret_len * 8)
+
+
 class State:
     stack: List[Word]
     memory: List[Byte]
@@ -1707,23 +1756,7 @@ def call_unknown() -> None:
                     else:
                         bytecode = artifact["bytecode"].replace("0x", "")
 
-                    bytecode_len = (len(bytecode) + 1) // 2
-                    bytecode_len_enc = (
-                        hex(bytecode_len).replace("0x", "").rjust(64, "0")
-                    )
-
-                    bytecode_len_ceil = (bytecode_len + 31) // 32 * 32
-
-                    ret_bytes = (
-                        "00" * 31
-                        + "20"
-                        + bytecode_len_enc
-                        + bytecode.ljust(bytecode_len_ceil * 2, "0")
-                    )
-                    ret_len = len(ret_bytes) // 2
-                    ret_bytes = bytes.fromhex(ret_bytes)
-
-                    ret = con(int.from_bytes(ret_bytes, "big"), ret_len * 8)
+                    ret = stringified_bytes_to_bytes(bytecode)
                 # vm.prank(address)
                 elif (
                     eq(arg.sort(), BitVecSorts[(4 + 32) * 8])
@@ -1849,6 +1882,32 @@ def call_unknown() -> None:
                         ex.error = f"vm.etch(address who, bytes code) must have concrete argument `code` but received calldata {arg}"
                         out.append(ex)
                         return
+                # ffi(string[]) returns (bytes)
+                elif extract_funsig(arg) == hevm_cheat_code.ffi_sig:
+                    if not self.options.get("ffi"):
+                        ex.error = "ffi cheatcode is disabled. Run again with `--ffi` if you want to enable it"
+                        out.append(ex)
+                        return
+                    process = Popen(
+                        extract_string_array_argument(arg, 0), stdout=PIPE, stderr=PIPE
+                    )
+
+                    (stdout, stderr) = process.communicate()
+
+                    if stderr:
+                        warn(
+                            INTERNAL_ERROR,
+                            f"An exception has occurred during the usage of the ffi cheatcode:\n{stderr.decode('utf-8')}",
+                        )
+
+                    out_bytes = stdout.decode("utf-8")
+
+                    if not out_bytes.startswith("0x"):
+                        out_bytes = out_bytes.strip().encode("utf-8").hex()
+                    else:
+                        out_bytes = out_bytes.strip().replace("0x", "")
+
+                    ret = stringified_bytes_to_bytes(out_bytes)
 
                 else:
                     # TODO: support other cheat codes

tests/expected/ffi.json

@@ -0,0 +1,43 @@
+{
+    "exitcode": 1,
+    "test_results": {
+        "test/Ffi.t.sol:FfiTest": [
+            {
+                "name": "testFFI_Failure()",
+                "exitcode": 2,
+                "num_models": null,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "testFFI_HexOutput()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "testFFI_Stderr()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "testFFI_StringOutput()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            }
+        ]
+    }
+}

tests/test/Ffi.t.sol

@@ -0,0 +1,62 @@
+// SPDX-License-Identifier: AGPL-3.0
+pragma solidity >=0.8.0 <0.9.0;
+
+import "forge-std/Test.sol";
+
+contract FfiTest is Test {
+
+    function testFFI_HexOutput() public {
+        string[] memory inputs = new string[](3);
+        inputs[0] = "echo";
+        inputs[1] = "-n";
+        inputs[2] = /* "arbitrary string" abi.encoded hex representation */"0x0000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000001061726269747261727920737472696e6700000000000000000000000000000000";
+
+        bytes memory res = vm.ffi(inputs);
+
+        bytes32 expected = keccak256(abi.encodePacked("arbitrary string"));
+        bytes32 output = keccak256(abi.encodePacked(abi.decode(res, (string))));
+
+        assert(expected == output);
+    }
+
+    function testFFI_StringOutput() public {
+        string memory str = "arbitrary string";
+
+        string[] memory inputs = new string[](3);
+        inputs[0] = "echo";
+        inputs[1] = "-n";
+        inputs[2] = str;
+
+        bytes32 expected = keccak256(abi.encodePacked(str));
+        bytes32 output = keccak256(
+            vm.ffi(inputs) /* Perform ffi */
+        );
+
+        assert(expected == output);
+    }
+
+    function testFFI_Stderr() public {
+        string[] memory inputs = new string[](3);
+        inputs[0] = "logger";
+        inputs[1] = "-s";
+        inputs[2] = "Error!";
+
+        bytes32 output = keccak256(
+            vm.ffi(inputs) /* Perform ffi that generates non empty stderr */
+        );
+
+        /* TODO: fix bug in sha3 of empty bytes
+        bytes32 expected = keccak256(abi.encodePacked(""));
+        assert(expected == output);
+        */
+    }
+
+    function testFFI_Failure() public {
+        string[] memory inputs = new string[](1);
+        inputs[0] = "must_fail";
+
+        bytes32 output = keccak256(
+            vm.ffi(inputs) /* Perform ffi that must fail */
+        );
+    }
+}

tests/test_halmos.py

@@ -16,6 +16,10 @@
             ["--root", "tests"],
             "tests/expected/all.json",
         ),
+        (
+            ["--root", "tests", "--function", "testFFI_"],
+            "tests/expected/ffi.json",
+        ),
         (
             ["--root", "examples/toy", "--function", "test"],
             "tests/expected/toy.json",
@@ -31,6 +35,7 @@
     ],
     ids=(
         "tests",
+        "ffi:tests",
         "examples/toy",
         "long:examples/tokens/ERC20",
         "long:examples/tokens/ERC721",