add ffi cheatcode

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
@@ -410,6 +412,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 +1755,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 +1881,31 @@ 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:
+                        ex.error = f"An exception has occurred during the usage of the ffi cheatcode:\n{stderr.decode('utf-8')}"
+                        out.append(ex)
+                        return
+
+                    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/all.json

@@ -549,6 +549,24 @@
                 "num_bounded_loops": null
             }
         ],
+        "test/Ffi.t.sol:FfiTest": [
+            {
+                "name": "check_FfiHexOutput()",
+                "exitcode": 0,
+                "num_models": 0,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_FfiStringOutput()",
+                "exitcode": 0,
+                "num_models": 0,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            }
+        ],
         "test/Foundry.t.sol:FoundryTest": [
             {
                 "name": "check_assume(uint256)",

tests/test/Ffi.t.sol

@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: Unlicensed
+pragma solidity >=0.8.0 <0.9.0;
+
+import "forge-std/Test.sol";
+
+/// @custom:halmos --ffi
+contract FfiTest is Test {
+    function check_FfiHexOutput() public {
+        string[] memory inputs = new string[](2);
+        inputs[0] = "echo";
+        inputs[1] = /* "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 check_FfiStringOutput() public {
+        string memory str = "arbitrary string";
+
+        string[] memory inputs = new string[](2);
+        inputs[0] = "echo";
+        inputs[1] = str;
+
+        bytes32 expected = keccak256(abi.encodePacked(str));
+        bytes32 output = keccak256(
+            vm.ffi(inputs) /* Perform ffi */
+        );
+
+        assert(expected == output);
+    }
+}