diff --git a/.github/workflows/test-external.yml b/.github/workflows/test-external.yml index 92d27d64..6fc9022f 100644 --- a/.github/workflows/test-external.yml +++ b/.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" diff --git a/.github/workflows/test-ffi.yml b/.github/workflows/test-ffi.yml new file mode 100644 index 00000000..262d4df2 --- /dev/null +++ b/.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" diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index e5a890c2..6fe8e17c 100644 --- a/.github/workflows/test.yml +++ b/.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" diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index 0d282cbd..4813b9c8 100644 --- a/src/halmos/__main__.py +++ b/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: diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index c4ed16ee..b2f2aa41 100644 --- a/src/halmos/cheatcodes.py +++ b/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); diff --git a/src/halmos/parser.py b/src/halmos/parser.py index 32685b61..7d7a5b39 100644 --- a/src/halmos/parser.py +++ b/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" ) diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 8dd65a10..a65e0c91 100644 --- a/src/halmos/sevm.py +++ b/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 diff --git a/tests/expected/ffi.json b/tests/expected/ffi.json new file mode 100644 index 00000000..302adc00 --- /dev/null +++ b/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 + } + ] + } +} \ No newline at end of file diff --git a/tests/test/Ffi.t.sol b/tests/test/Ffi.t.sol new file mode 100644 index 00000000..7667b47d --- /dev/null +++ b/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 */ + ); + } +} diff --git a/tests/test_halmos.py b/tests/test_halmos.py index 2bce77e2..64880c26 100644 --- a/tests/test_halmos.py +++ b/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",