From 29f90f0a206c7f5c63a7966101c816b4eb97e3d2 Mon Sep 17 00:00:00 2001 From: luksgrin Date: Fri, 18 Aug 2023 09:38:01 +0000 Subject: [PATCH 01/14] Added ffi cheatcode --- src/halmos/cheatcodes.py | 3 ++ src/halmos/sevm.py | 89 ++++++++++++++++++++++++++++++++-------- 2 files changed, 75 insertions(+), 17 deletions(-) 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/sevm.py b/src/halmos/sevm.py index 8dd65a10..9fa0ff4b 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 @@ -409,6 +411,52 @@ def extract_string_argument(calldata: BitVecRef, arg_idx: int): string_bytes = string_value.to_bytes(string_length, "big") 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] @@ -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,29 @@ 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: + 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 = stdout.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 From a3627441474746ba0678676715a75e6c4d0b8004 Mon Sep 17 00:00:00 2001 From: luksgrin Date: Sun, 20 Aug 2023 21:30:19 +0000 Subject: [PATCH 02/14] Disabled ffi by default and added an argument to enable it --- src/halmos/__main__.py | 1 + src/halmos/parser.py | 6 ++++++ src/halmos/sevm.py | 4 ++++ 3 files changed, 11 insertions(+) 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/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 9fa0ff4b..13442b61 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -1883,6 +1883,10 @@ def call_unknown() -> None: 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, From 20d1221b978c5cbcfda8d0026ad9af7bdd37cca7 Mon Sep 17 00:00:00 2001 From: luksgrin Date: Mon, 21 Aug 2023 09:36:50 +0000 Subject: [PATCH 03/14] Fixed bug on UTF-8 output of subprocess --- src/halmos/sevm.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 13442b61..5f145f7a 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -1903,7 +1903,7 @@ def call_unknown() -> None: out_bytes = stdout.decode("utf-8") if not out_bytes.startswith("0x"): - out_bytes = stdout.strip().encode("utf-8").hex() + out_bytes = out_bytes.strip().encode("utf-8").hex() else: out_bytes = out_bytes.strip().replace("0x", "") From 453f1609d92d9bd67854a169dc05b39057074d8e Mon Sep 17 00:00:00 2001 From: luksgrin Date: Mon, 21 Aug 2023 13:23:56 +0000 Subject: [PATCH 04/14] Added Ffi test --- tests/expected/all.json | 18 ++++++++++++ tests/test/Ffi.t.sol | 64 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 82 insertions(+) create mode 100644 tests/test/Ffi.t.sol diff --git a/tests/expected/all.json b/tests/expected/all.json index 294c5abb..e3104bb0 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -549,6 +549,24 @@ "num_bounded_loops": null } ], + "test/Ffi.t.sol:Create2Test": [ + { + "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)", diff --git a/tests/test/Ffi.t.sol b/tests/test/Ffi.t.sol new file mode 100644 index 00000000..a986ffb4 --- /dev/null +++ b/tests/test/Ffi.t.sol @@ -0,0 +1,64 @@ +// SPDX-License-Identifier: Unlicensed +pragma solidity >=0.8.0 <0.9.0; + +import "forge-std/Test.sol"; +import "forge-std/console2.sol"; + +/** + * @dev The interface of this cheat code is called `_CheatCodes`, + * so you can use the `CheatCodes` interface (see here: + * https://book.getfoundry.sh/cheatcodes/?highlight=CheatCodes#cheatcode-types) + * in other test files without errors. + */ +// solhint-disable-next-line contract-name-camelcase +interface _CheatCodes { + function ffi(string[] calldata) external returns (bytes memory); +} + + + +contract FfiTest is Test { + // address private constant HEVM_ADDRESS = address(uint160(uint256(keccak256("hevm cheat code")))); + /** + * @dev Initialises `cheatCodes` in order to use the foreign function interface (ffi) + */ + //_CheatCodes private cheatCodes = _CheatCodes(HEVM_ADDRESS); + _CheatCodes private cheatCodes = _CheatCodes(address(uint160(uint256(keccak256("hevm cheat code"))))); + + /** + * @dev ffi is a function that takes a list of strings and returns a bytes array. + */ + function ffi(string[] memory _cmds) internal returns (bytes memory) { + return cheatCodes.ffi(_cmds); + } + + function check_FfiHexOutput() 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 = 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[](3); + inputs[0] = "echo"; + inputs[1] = "-n"; + inputs[2] = str; + + bytes32 expected = keccak256(abi.encodePacked(str)); + bytes32 output = keccak256( + ffi(inputs) /* Perform ffi */ + ); + + assert(expected == output); + } +} \ No newline at end of file From 795c1a2ef763ddb0b2b6e3a7d67e463e20e785a3 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Mon, 21 Aug 2023 09:54:04 -0700 Subject: [PATCH 05/14] chore: formatting --- src/halmos/sevm.py | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 5f145f7a..cc837936 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -411,38 +411,38 @@ def extract_string_argument(calldata: BitVecRef, arg_idx: int): string_bytes = string_value.to_bytes(string_length, "big") 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)) + 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) + 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_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_enc = hex(string_bytes_len).replace("0x", "").rjust(64, "0") string_bytes_len_ceil = (string_bytes_len + 31) // 32 * 32 @@ -1888,9 +1888,7 @@ def call_unknown() -> None: out.append(ex) return process = Popen( - extract_string_array_argument(arg, 0), - stdout=PIPE, - stderr=PIPE + extract_string_array_argument(arg, 0), stdout=PIPE, stderr=PIPE ) (stdout, stderr) = process.communicate() From fe34e54b6da685e78220fd29d79cc8e3234b5787 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Mon, 21 Aug 2023 10:01:26 -0700 Subject: [PATCH 06/14] test: fix FfiTest --- tests/test/Ffi.t.sol | 37 +++++-------------------------------- 1 file changed, 5 insertions(+), 32 deletions(-) diff --git a/tests/test/Ffi.t.sol b/tests/test/Ffi.t.sol index a986ffb4..f6108420 100644 --- a/tests/test/Ffi.t.sol +++ b/tests/test/Ffi.t.sol @@ -2,44 +2,17 @@ pragma solidity >=0.8.0 <0.9.0; import "forge-std/Test.sol"; -import "forge-std/console2.sol"; - -/** - * @dev The interface of this cheat code is called `_CheatCodes`, - * so you can use the `CheatCodes` interface (see here: - * https://book.getfoundry.sh/cheatcodes/?highlight=CheatCodes#cheatcode-types) - * in other test files without errors. - */ -// solhint-disable-next-line contract-name-camelcase -interface _CheatCodes { - function ffi(string[] calldata) external returns (bytes memory); -} - - +/// @custom:halmos --ffi contract FfiTest is Test { - // address private constant HEVM_ADDRESS = address(uint160(uint256(keccak256("hevm cheat code")))); - /** - * @dev Initialises `cheatCodes` in order to use the foreign function interface (ffi) - */ - //_CheatCodes private cheatCodes = _CheatCodes(HEVM_ADDRESS); - _CheatCodes private cheatCodes = _CheatCodes(address(uint160(uint256(keccak256("hevm cheat code"))))); - - /** - * @dev ffi is a function that takes a list of strings and returns a bytes array. - */ - function ffi(string[] memory _cmds) internal returns (bytes memory) { - return cheatCodes.ffi(_cmds); - } - function check_FfiHexOutput() 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 = ffi(inputs); - + bytes memory res = vm.ffi(inputs); + bytes32 expected = keccak256(abi.encodePacked("arbitrary string")); bytes32 output = keccak256(abi.encodePacked(abi.decode(res, (string)))); @@ -56,9 +29,9 @@ contract FfiTest is Test { bytes32 expected = keccak256(abi.encodePacked(str)); bytes32 output = keccak256( - ffi(inputs) /* Perform ffi */ + vm.ffi(inputs) /* Perform ffi */ ); assert(expected == output); } -} \ No newline at end of file +} From 2e2906c3e3c352b0dd0cc28b36e02f386ed0fe81 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Mon, 21 Aug 2023 10:15:56 -0700 Subject: [PATCH 07/14] test: fix contract name in tests/expected/all.json --- tests/expected/all.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/expected/all.json b/tests/expected/all.json index e3104bb0..c30cb71f 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -549,7 +549,7 @@ "num_bounded_loops": null } ], - "test/Ffi.t.sol:Create2Test": [ + "test/Ffi.t.sol:FfiTest": [ { "name": "check_FfiHexOutput()", "exitcode": 0, From a98b15d1670dfb8f8f8f1df0e0b01a67e83fc30e Mon Sep 17 00:00:00 2001 From: karmacoma Date: Mon, 21 Aug 2023 10:32:39 -0700 Subject: [PATCH 08/14] test: see if plain "echo" cmd is happier on windows --- tests/test/Ffi.t.sol | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/tests/test/Ffi.t.sol b/tests/test/Ffi.t.sol index f6108420..429767a7 100644 --- a/tests/test/Ffi.t.sol +++ b/tests/test/Ffi.t.sol @@ -6,10 +6,9 @@ import "forge-std/Test.sol"; /// @custom:halmos --ffi contract FfiTest is Test { function check_FfiHexOutput() public { - string[] memory inputs = new string[](3); + string[] memory inputs = new string[](2); inputs[0] = "echo"; - inputs[1] = "-n"; - inputs[2] = /* "arbitrary string" abi.encoded hex representation */"0x0000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000001061726269747261727920737472696e6700000000000000000000000000000000"; + inputs[1] = /* "arbitrary string" abi.encoded hex representation */"0x0000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000001061726269747261727920737472696e6700000000000000000000000000000000"; bytes memory res = vm.ffi(inputs); @@ -22,10 +21,9 @@ contract FfiTest is Test { function check_FfiStringOutput() public { string memory str = "arbitrary string"; - string[] memory inputs = new string[](3); + string[] memory inputs = new string[](2); inputs[0] = "echo"; - inputs[1] = "-n"; - inputs[2] = str; + inputs[1] = str; bytes32 expected = keccak256(abi.encodePacked(str)); bytes32 output = keccak256( From 1d97a587be96960f8e9088cf154e49f90f80d1a5 Mon Sep 17 00:00:00 2001 From: luksgrin Date: Sun, 27 Aug 2023 12:13:05 +0000 Subject: [PATCH 09/14] Added a test that expects ffi failure --- tests/errorHelper.sh | 2 ++ tests/expected/all.json | 8 ++++++ tests/test/Ffi.t.sol | 58 ++++++++++++++++++++++++++++++++++------- 3 files changed, 59 insertions(+), 9 deletions(-) create mode 100644 tests/errorHelper.sh diff --git a/tests/errorHelper.sh b/tests/errorHelper.sh new file mode 100644 index 00000000..3e3ac30b --- /dev/null +++ b/tests/errorHelper.sh @@ -0,0 +1,2 @@ +echo "Error!" 1>&2; +exit 1; \ No newline at end of file diff --git a/tests/expected/all.json b/tests/expected/all.json index c30cb71f..e44ec452 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -565,6 +565,14 @@ "num_paths": null, "time": null, "num_bounded_loops": null + }, + { + "name": "check_FfiFailure()", + "exitcode": 1, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null } ], "test/Foundry.t.sol:FoundryTest": [ diff --git a/tests/test/Ffi.t.sol b/tests/test/Ffi.t.sol index 429767a7..a835353d 100644 --- a/tests/test/Ffi.t.sol +++ b/tests/test/Ffi.t.sol @@ -2,16 +2,44 @@ pragma solidity >=0.8.0 <0.9.0; import "forge-std/Test.sol"; +import "forge-std/console2.sol"; + +/** + * @dev The interface of this cheat code is called `_CheatCodes`, + * so you can use the `CheatCodes` interface (see here: + * https://book.getfoundry.sh/cheatcodes/?highlight=CheatCodes#cheatcode-types) + * in other test files without errors. + */ +// solhint-disable-next-line contract-name-camelcase +interface _CheatCodes { + function ffi(string[] calldata) external returns (bytes memory); +} + + -/// @custom:halmos --ffi contract FfiTest is Test { + // address private constant HEVM_ADDRESS = address(uint160(uint256(keccak256("hevm cheat code")))); + /** + * @dev Initialises `cheatCodes` in order to use the foreign function interface (ffi) + */ + //_CheatCodes private cheatCodes = _CheatCodes(HEVM_ADDRESS); + _CheatCodes private cheatCodes = _CheatCodes(address(uint160(uint256(keccak256("hevm cheat code"))))); + + /** + * @dev ffi is a function that takes a list of strings and returns a bytes array. + */ + function ffi(string[] memory _cmds) internal returns (bytes memory) { + return cheatCodes.ffi(_cmds); + } + function check_FfiHexOutput() public { - string[] memory inputs = new string[](2); + string[] memory inputs = new string[](3); inputs[0] = "echo"; - inputs[1] = /* "arbitrary string" abi.encoded hex representation */"0x0000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000001061726269747261727920737472696e6700000000000000000000000000000000"; - - bytes memory res = vm.ffi(inputs); + inputs[1] = "-n"; + inputs[2] = /* "arbitrary string" abi.encoded hex representation */"0x0000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000001061726269747261727920737472696e6700000000000000000000000000000000"; + bytes memory res = ffi(inputs); + bytes32 expected = keccak256(abi.encodePacked("arbitrary string")); bytes32 output = keccak256(abi.encodePacked(abi.decode(res, (string)))); @@ -21,15 +49,27 @@ contract FfiTest is Test { function check_FfiStringOutput() public { string memory str = "arbitrary string"; - string[] memory inputs = new string[](2); + string[] memory inputs = new string[](3); inputs[0] = "echo"; - inputs[1] = str; + inputs[1] = "-n"; + inputs[2] = str; bytes32 expected = keccak256(abi.encodePacked(str)); bytes32 output = keccak256( - vm.ffi(inputs) /* Perform ffi */ + ffi(inputs) /* Perform ffi */ ); assert(expected == output); } -} + + function check_FfiFailure() public { + + string[] memory inputs = new string[](2); + inputs[0] = "bash"; + inputs[1] = "errorHelper.sh"; + + bytes32 output = keccak256( + vm.ffi(inputs) /* Perform ffi that generates non empty stderr */ + ); + } +} \ No newline at end of file From 57241d869ae8b8603130a3ef9d00a3fb5bf42042 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 11 Sep 2023 16:45:44 -0700 Subject: [PATCH 10/14] change ffi behavior to not fail when stderr is present --- src/halmos/sevm.py | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index cc837936..a65e0c91 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -29,6 +29,7 @@ UNSUPPORTED_OPCODE, LIBRARY_PLACEHOLDER, UNINTERPRETED_UNKNOWN_CALLS, + INTERNAL_ERROR, ) Word = Any # z3 expression (including constants) @@ -1894,9 +1895,10 @@ def call_unknown() -> None: (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 + 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") From 9a7f039b808103c3f80f957c8887e43e62d7edc7 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 11 Sep 2023 16:47:25 -0700 Subject: [PATCH 11/14] separate ffi tests --- .github/workflows/test.yml | 2 +- tests/errorHelper.sh | 2 -- tests/expected/all.json | 26 ----------------------- tests/expected/ffi.json | 43 ++++++++++++++++++++++++++++++++++++++ tests/test/Ffi.t.sol | 32 ++++++++++++++++++++-------- tests/test_halmos.py | 5 +++++ 6 files changed, 72 insertions(+), 38 deletions(-) delete mode 100644 tests/errorHelper.sh create mode 100644 tests/expected/ffi.json 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/tests/errorHelper.sh b/tests/errorHelper.sh deleted file mode 100644 index 3e3ac30b..00000000 --- a/tests/errorHelper.sh +++ /dev/null @@ -1,2 +0,0 @@ -echo "Error!" 1>&2; -exit 1; \ No newline at end of file diff --git a/tests/expected/all.json b/tests/expected/all.json index e44ec452..294c5abb 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -549,32 +549,6 @@ "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 - }, - { - "name": "check_FfiFailure()", - "exitcode": 1, - "num_models": 0, - "num_paths": null, - "time": null, - "num_bounded_loops": null - } - ], "test/Foundry.t.sol:FoundryTest": [ { "name": "check_assume(uint256)", 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 index a835353d..86c45118 100644 --- a/tests/test/Ffi.t.sol +++ b/tests/test/Ffi.t.sol @@ -25,28 +25,28 @@ contract FfiTest is Test { //_CheatCodes private cheatCodes = _CheatCodes(HEVM_ADDRESS); _CheatCodes private cheatCodes = _CheatCodes(address(uint160(uint256(keccak256("hevm cheat code"))))); - /** + /** * @dev ffi is a function that takes a list of strings and returns a bytes array. */ function ffi(string[] memory _cmds) internal returns (bytes memory) { return cheatCodes.ffi(_cmds); } - function check_FfiHexOutput() public { + 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 = 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 { + function testFFI_StringOutput() public { string memory str = "arbitrary string"; string[] memory inputs = new string[](3); @@ -62,14 +62,28 @@ contract FfiTest is Test { assert(expected == output); } - function check_FfiFailure() public { + function testFFI_Stderr() public { + string[] memory inputs = new string[](3); + inputs[0] = "logger"; + inputs[1] = "-s"; + inputs[2] = "Error!"; - string[] memory inputs = new string[](2); - inputs[0] = "bash"; - inputs[1] = "errorHelper.sh"; + 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 generates non empty stderr */ ); } -} \ No newline at end of file +} 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", From 3a3c2d19818d338b87ccbbf972ba94ebf35fe21f Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 11 Sep 2023 16:48:04 -0700 Subject: [PATCH 12/14] add separate ci for ffi tests --- .github/workflows/test-ffi.yml | 41 ++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) create mode 100644 .github/workflows/test-ffi.yml 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" From 0ae8839169c9bd510f0958baf4f96f21a5f0400e Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 11 Sep 2023 17:05:48 -0700 Subject: [PATCH 13/14] update ffi tests --- tests/test/Ffi.t.sol | 35 ++++------------------------------- 1 file changed, 4 insertions(+), 31 deletions(-) diff --git a/tests/test/Ffi.t.sol b/tests/test/Ffi.t.sol index 86c45118..7667b47d 100644 --- a/tests/test/Ffi.t.sol +++ b/tests/test/Ffi.t.sol @@ -1,36 +1,9 @@ -// SPDX-License-Identifier: Unlicensed +// SPDX-License-Identifier: AGPL-3.0 pragma solidity >=0.8.0 <0.9.0; import "forge-std/Test.sol"; -import "forge-std/console2.sol"; - -/** - * @dev The interface of this cheat code is called `_CheatCodes`, - * so you can use the `CheatCodes` interface (see here: - * https://book.getfoundry.sh/cheatcodes/?highlight=CheatCodes#cheatcode-types) - * in other test files without errors. - */ -// solhint-disable-next-line contract-name-camelcase -interface _CheatCodes { - function ffi(string[] calldata) external returns (bytes memory); -} - - contract FfiTest is Test { - // address private constant HEVM_ADDRESS = address(uint160(uint256(keccak256("hevm cheat code")))); - /** - * @dev Initialises `cheatCodes` in order to use the foreign function interface (ffi) - */ - //_CheatCodes private cheatCodes = _CheatCodes(HEVM_ADDRESS); - _CheatCodes private cheatCodes = _CheatCodes(address(uint160(uint256(keccak256("hevm cheat code"))))); - - /** - * @dev ffi is a function that takes a list of strings and returns a bytes array. - */ - function ffi(string[] memory _cmds) internal returns (bytes memory) { - return cheatCodes.ffi(_cmds); - } function testFFI_HexOutput() public { string[] memory inputs = new string[](3); @@ -38,7 +11,7 @@ contract FfiTest is Test { inputs[1] = "-n"; inputs[2] = /* "arbitrary string" abi.encoded hex representation */"0x0000000000000000000000000000000000000000000000000000000000000020000000000000000000000000000000000000000000000000000000000000001061726269747261727920737472696e6700000000000000000000000000000000"; - bytes memory res = ffi(inputs); + bytes memory res = vm.ffi(inputs); bytes32 expected = keccak256(abi.encodePacked("arbitrary string")); bytes32 output = keccak256(abi.encodePacked(abi.decode(res, (string)))); @@ -56,7 +29,7 @@ contract FfiTest is Test { bytes32 expected = keccak256(abi.encodePacked(str)); bytes32 output = keccak256( - ffi(inputs) /* Perform ffi */ + vm.ffi(inputs) /* Perform ffi */ ); assert(expected == output); @@ -83,7 +56,7 @@ contract FfiTest is Test { inputs[0] = "must_fail"; bytes32 output = keccak256( - vm.ffi(inputs) /* Perform ffi that generates non empty stderr */ + vm.ffi(inputs) /* Perform ffi that must fail */ ); } } From 59d449da297c6cfdebadea1fb43c45cccace23cf Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Mon, 11 Sep 2023 17:35:36 -0700 Subject: [PATCH 14/14] update external test ci --- .github/workflows/test-external.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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"