From 9bfff2e55641f74bca68e4009ca4c5ef8ba75497 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Fri, 13 Oct 2023 16:58:06 -0700 Subject: [PATCH 1/9] add type-sensitive rendering for model values --- src/halmos/__main__.py | 5 ++- src/halmos/exceptions.py | 8 ++++ src/halmos/sevm.py | 59 +++++--------------------- src/halmos/utils.py | 89 ++++++++++++++++++++++++++++++++++++++-- 4 files changed, 106 insertions(+), 55 deletions(-) diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index cc9ce3a5..4809f004 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -18,6 +18,7 @@ from .utils import ( create_solver, hexify, + stringify, indent_text, NamedTimer, yellow, @@ -1066,14 +1067,14 @@ def select(var): return name.startswith("p_") or name.startswith("halmos_") select_model = filter(select, model) if not print_full_model else model - return {str(decl): hexify(model[decl]) for decl in select_model} + return {str(decl): stringify(str(decl), model[decl]) for decl in select_model} def render_model(model: UnionType[str, StrModel]) -> str: if isinstance(model, str): return model - formatted = [f"\n {decl} = {hexify(val)}" for decl, val in model.items()] + formatted = [f"\n {decl} = {val}" for decl, val in model.items()] return "".join(sorted(formatted)) if formatted else "∅" diff --git a/src/halmos/exceptions.py b/src/halmos/exceptions.py index 4110ebe1..a8982f6e 100644 --- a/src/halmos/exceptions.py +++ b/src/halmos/exceptions.py @@ -8,6 +8,14 @@ """ +class HalmosException(Exception): + pass + + +class NotConcreteError(HalmosException): + pass + + class EvmException(Exception): """ Base class for all EVM exceptions. diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index d50c3fe6..a93ea56d 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -26,23 +26,24 @@ from .cheatcodes import halmos_cheat_code, hevm_cheat_code, console, Prank from .exceptions import * from .utils import ( - create_solver, - EVM, - sha3_inv, - restore_precomputed_hashes, - str_opcode, assert_address, assert_uint256, - con_addr, bv_value_to_bytes, - hexify, + byte_length, color_info, + con_addr, + create_solver, + EVM, + hexify, + int_of, + restore_precomputed_hashes, + sha3_inv, + str_opcode, + unbox_int, ) from .warnings import ( warn, - UNSUPPORTED_OPCODE, LIBRARY_PLACEHOLDER, - UNINTERPRETED_UNKNOWN_CALLS, INTERNAL_ERROR, ) @@ -165,14 +166,6 @@ def __len__(self) -> int: return instruction_length(self.opcode) -class HalmosException(Exception): - pass - - -class NotConcreteError(HalmosException): - pass - - def id_str(x: Any) -> str: return hexify(x).replace(" ", "") @@ -192,26 +185,6 @@ def padded_slice(lst: List, start: int, size: int, default=0) -> List: return [lst[i] if i < n else default for i in range(start, end)] -def unbox_int(x: Any) -> Any: - """Convert int-like objects to int""" - if isinstance(x, bytes): - return int.from_bytes(x, "big") - - if is_bv_value(x): - return x.as_long() - - return x - - -def int_of(x: Any, err: str = "expected concrete value but got") -> int: - res = unbox_int(x) - - if isinstance(res, int): - return res - - raise NotConcreteError(f"{err}: {x}") - - def iter_bytes(x: Any, _byte_length: int = -1): """Return an iterable over the bytes of x (concrete or symbolic)""" @@ -283,18 +256,6 @@ def con(n: int, size_bits=256) -> Word: return BitVecVal(n, BitVecSorts[size_bits]) -def byte_length(x: Any) -> int: - if is_bv(x): - if x.size() % 8 != 0: - raise ValueError(x) - return x.size() >> 3 - - if isinstance(x, bytes): - return len(x) - - raise ValueError(x) - - def instruction_length(opcode: Any) -> int: opcode = int_of(opcode) return (opcode - EVM.PUSH0 + 1) if EVM.PUSH1 <= opcode <= EVM.PUSH32 else 1 diff --git a/src/halmos/utils.py b/src/halmos/utils.py index 92102af5..7de305e0 100644 --- a/src/halmos/utils.py +++ b/src/halmos/utils.py @@ -3,10 +3,12 @@ import re from timeit import default_timer as timer -from typing import Dict, Tuple +from typing import Dict, Tuple, Any from z3 import * +from .exceptions import NotConcreteError + def create_solver(logic="QF_AUFBV", ctx=None, timeout=0, max_memory=0): # QF_AUFBV: quantifier-free bitvector + array theory: https://smtlib.cs.uiowa.edu/logics.shtml @@ -28,6 +30,43 @@ def bv_value_to_bytes(x: BitVecNumRef) -> bytes: return x.as_long().to_bytes(x.size() // 8, "big") +def unbox_int(x: Any) -> Any: + """ + Attempts to convert int-like objects to int + """ + if isinstance(x, bytes): + return int.from_bytes(x, "big") + + if is_bv_value(x): + return x.as_long() + + return x + + +def int_of(x: Any, err: str = "expected concrete value but got") -> int: + """ + Converts int-like objects to int or raises NotConcreteError + """ + res = unbox_int(x) + + if isinstance(res, int): + return res + + raise NotConcreteError(f"{err}: {x}") + + +def byte_length(x: Any) -> int: + if is_bv(x): + if x.size() % 8 != 0: + raise ValueError(x) + return x.size() >> 3 + + if isinstance(x, bytes): + return len(x) + + raise ValueError(x) + + def hexify(x): if isinstance(x, str): return re.sub(r"\b(\d+)\b", lambda match: hex(int(match.group(1))), x) @@ -36,13 +75,55 @@ def hexify(x): elif isinstance(x, bytes): return "0x" + x.hex() elif is_bv_value(x): - # preserving bitsize could be confusing due to some bv values given as strings; need refactoring to fix properly - # return hexify(x.as_long().to_bytes((x.size() + 7) // 8, 'big')) # bitsize may not be a multiple of 8 - return hex(x.as_long()) + # maintain the byte size of x + num_bytes = byte_length(x) + return f"0x{x.as_long():0{num_bytes * 2}x}" else: return hexify(str(x)) +def stringify(symbol_name: str, val: Any): + """ + Formats a value based on the inferred type of the variable. + + Expects symbol_name to be of the form 'p__', e.g. 'p_x_uint256' + """ + if not is_bv_value(val): + warn(f"{val} is not a bitvector value") + return str(val) + + tokens = symbol_name.split("_") + if len(tokens) < 3: + warn(f"Failed to infer type for symbol '{symbol_name}'") + + if len(tokens) >= 4 and tokens[-1].isdigit(): + # we may have something like p_val_bytes_01 + # the last token being a symbol number, discard it + tokens.pop() + + type_name = tokens[-1] + + if type_name.startswith("uint"): + v = val.as_long() + return v if v < 2**64 else hex(v) + elif type_name.startswith("int"): + v = val.as_signed_long() + if -(2**63) <= v < 2**63: + return v + return f"0x{val.as_long():0{byte_length(val) * 2}x}" + elif type_name == "bool": + return str(val.as_long() != 0).lower() + elif type_name == "string": + str_val = bytes.fromhex(hexify(val)[2:]).decode("utf-8") + return f'"{str_val}"' + elif type_name == "bytes": + return f'hex"{hex(val.as_long())[2:]}"' + elif type_name == "address": + return f"0x{val.as_long():040x}" + else: # address, bytes32, bytes4, structs, etc. + return hexify(val) + + def assert_address(x: BitVecRef) -> None: if x.size() != 160: raise ValueError(x) From 544a05cb33cae459e2961c5944d78d22c67684b8 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Fri, 13 Oct 2023 17:45:14 -0700 Subject: [PATCH 2/9] Add signatures for new cheatcodes --- src/halmos/cheatcodes.py | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index a81e20f4..fc9a6aee 100644 --- a/src/halmos/cheatcodes.py +++ b/src/halmos/cheatcodes.py @@ -71,11 +71,23 @@ class halmos_cheat_code: # bytes4(keccak256("createUint(uint256,string)")) create_uint: int = 0x66830DFA + # bytes4(keccak256("createUint256(string)")) + create_uint256: int = 0xBC7BEEFC + + # bytes4(keccak256("createInt(uint256,string)")) + create_int: int = 0x49B9C7D4 + + # bytes4(keccak256("createInt256(string)")) + create_int256: int = 0xC2CE6AED + # bytes4(keccak256("createBytes(uint256,string)")) create_bytes: int = 0xEEF5311D - # bytes4(keccak256("createUint256(string)")) - create_uint256: int = 0xBC7BEEFC + # bytes4(keccak256("createString(uint256,string)")) + create_string: int = 0xCE68656C + + # bytes4(keccak256("createBytes4(string)")) + create_bytes4: int = 0xDE143925 # bytes4(keccak256("createBytes32(string)")) create_bytes32: int = 0xBF72FA66 From 7fb60ffd8aa72b149697ea337601e6640faed4c2 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Mon, 16 Oct 2023 15:30:11 -0700 Subject: [PATCH 3/9] introduce Exec.set_code to fix vm.etch --- src/halmos/cheatcodes.py | 319 ++++++++++++++++++++++++- src/halmos/sevm.py | 491 ++------------------------------------- src/halmos/utils.py | 131 ++++++++++- 3 files changed, 458 insertions(+), 483 deletions(-) diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index fc9a6aee..d6004077 100644 --- a/src/halmos/cheatcodes.py +++ b/src/halmos/cheatcodes.py @@ -1,10 +1,89 @@ # SPDX-License-Identifier: AGPL-3.0 +import json +import re + +from subprocess import Popen, PIPE from typing import List, Dict, Set, Tuple, Any from z3 import * -from .utils import assert_address, con_addr +from .exceptions import FailCheatcode, HalmosException +from .utils import * +from .warnings import ( + INTERNAL_ERROR, + warn, +) + + +def name_of(x: str) -> str: + return re.sub(r"\s+", "_", x) + + +def extract_string_argument(calldata: BitVecRef, arg_idx: int): + """Extracts idx-th argument of string from calldata""" + string_offset = int_of( + extract_bytes(calldata, 4 + arg_idx * 32, 32), + "symbolic offset for string argument", + ) + string_length = int_of( + extract_bytes(calldata, 4 + string_offset, 32), + "symbolic size for string argument", + ) + if string_length == 0: + return "" + string_value = int_of( + extract_bytes(calldata, 4 + string_offset + 32, string_length), + "symbolic string argument", + ) + 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 Prank: @@ -20,9 +99,9 @@ def __init__(self, addr: Any = None, keep: bool = False) -> None: def __str__(self) -> str: if self.addr: if self.keep: - return f"startPrank({str(addr)})" + return f"startPrank({str(self.addr)})" else: - return f"prank({str(addr)})" + return f"prank({str(self.addr)})" else: return "None" @@ -98,6 +177,64 @@ class halmos_cheat_code: # bytes4(keccak256("createBool(string)")) create_bool: int = 0x6E0BB659 + @staticmethod + def handle(ex, arg: BitVec) -> BitVec: + funsig: int = int_of(extract_funsig(arg), "symbolic halmos cheatcode") + + # createUint(uint256,string) returns (uint256) + if funsig == halmos_cheat_code.create_uint: + bit_size = int_of( + extract_bytes(arg, 4, 32), + "symbolic bit size for halmos.createUint()", + ) + name = name_of(extract_string_argument(arg, 1)) + if bit_size <= 256: + label = f"halmos_{name}_uint{bit_size}_{ex.new_symbol_id():>02}" + ret = uint256(BitVec(label, BitVecSorts[bit_size])) + else: + raise HalmosException(f"bitsize larger than 256: {bit_size}") + + # createBytes(uint256,string) returns (bytes) + elif funsig == halmos_cheat_code.create_bytes: + byte_size = int_of( + extract_bytes(arg, 4, 32), + "symbolic byte size for halmos.createBytes()", + ) + name = name_of(extract_string_argument(arg, 1)) + label = f"halmos_{name}_bytes_{ex.new_symbol_id():>02}" + symbolic_bytes = BitVec(label, BitVecSorts[byte_size * 8]) + ret = Concat(con(32), con(byte_size), symbolic_bytes) + + # createUint256(string) returns (uint256) + elif funsig == halmos_cheat_code.create_uint256: + name = name_of(extract_string_argument(arg, 0)) + label = f"halmos_{name}_uint256_{ex.new_symbol_id():>02}" + ret = BitVec(label, BitVecSort256) + + # createBytes32(string) returns (bytes32) + elif funsig == halmos_cheat_code.create_bytes32: + name = name_of(extract_string_argument(arg, 0)) + label = f"halmos_{name}_bytes32_{ex.new_symbol_id():>02}" + ret = BitVec(label, BitVecSort256) + + # createAddress(string) returns (address) + elif funsig == halmos_cheat_code.create_address: + name = name_of(extract_string_argument(arg, 0)) + label = f"halmos_{name}_address_{ex.new_symbol_id():>02}" + ret = uint256(BitVec(label, BitVecSort160)) + + # createBool(string) returns (bool) + elif funsig == halmos_cheat_code.create_bool: + name = name_of(extract_string_argument(arg, 0)) + label = f"halmos_{name}_bool_{ex.new_symbol_id():>02}" + ret = uint256(BitVec(label, BitVecSort1)) + + else: + error_msg = f"Unknown halmos cheat code: function selector = 0x{funsig:0>8x}, calldata = {hexify(arg)}" + raise HalmosException(error_msg) + + return ret + class hevm_cheat_code: # https://github.com/dapphub/ds-test/blob/cd98eff28324bfac652e63a239a60632a761790b/src/test.sol @@ -166,11 +303,185 @@ class hevm_cheat_code: # bytes4(keccak256("ffi(string[])")) ffi_sig: int = 0x89160467 + @staticmethod + def handle(sevm, ex, arg: BitVec) -> BitVec: + funsig: int = int_of(extract_funsig(arg), "symbolic hevm cheatcode") + + # vm.fail() + # BitVecVal(hevm_cheat_code.fail_payload, 800) + if arg == hevm_cheat_code.fail_payload: + raise FailCheatcode() + + # vm.assume(bool) + elif ( + eq(arg.sort(), BitVecSorts[(4 + 32) * 8]) + and funsig == hevm_cheat_code.assume_sig + ): + assume_cond = simplify(is_non_zero(Extract(255, 0, arg))) + ex.solver.add(assume_cond) + ex.path.append(str(assume_cond)) + + # vm.getCode(string) + elif funsig == hevm_cheat_code.get_code_sig: + calldata = bytes.fromhex(hex(arg.as_long())[2:]) + path_len = int.from_bytes(calldata[36:68], "big") + path = calldata[68 : 68 + path_len].decode("utf-8") + + if ":" in path: + [filename, contract_name] = path.split(":") + path = "out/" + filename + "/" + contract_name + ".json" + + target = sevm.options["target"].rstrip("/") + path = target + "/" + path + + with open(path) as f: + artifact = json.loads(f.read()) + + if artifact["bytecode"]["object"]: + bytecode = artifact["bytecode"]["object"].replace("0x", "") + else: + bytecode = artifact["bytecode"].replace("0x", "") + + return stringified_bytes_to_bytes(bytecode) + + # vm.prank(address) + elif funsig == hevm_cheat_code.prank_sig: + result = ex.prank.prank(uint160(Extract(255, 0, arg))) + if not result: + raise HalmosException("You have an active prank already.") + + # vm.startPrank(address) + elif funsig == hevm_cheat_code.start_prank_sig: + result = ex.prank.startPrank(uint160(Extract(255, 0, arg))) + if not result: + raise HalmosException("You have an active prank already.") + + # vm.stopPrank() + elif funsig == hevm_cheat_code.stop_prank_sig: + ex.prank.stopPrank() + + # vm.deal(address,uint256) + elif funsig == hevm_cheat_code.deal_sig: + who = uint160(Extract(511, 256, arg)) + amount = simplify(Extract(255, 0, arg)) + ex.balance_update(who, amount) + + # vm.store(address,bytes32,bytes32) + elif funsig == hevm_cheat_code.store_sig: + store_account = uint160(Extract(767, 512, arg)) + store_slot = simplify(Extract(511, 256, arg)) + store_value = simplify(Extract(255, 0, arg)) + store_account_addr = sevm.resolve_address_alias(ex, store_account) + if store_account_addr is not None: + sevm.sstore(ex, store_account_addr, store_slot, store_value) + else: + raise HalmosException(f"uninitialized account: {store_account}") + + # vm.load(address,bytes32) + elif funsig == hevm_cheat_code.load_sig: + load_account = uint160(Extract(511, 256, arg)) + load_slot = simplify(Extract(255, 0, arg)) + load_account_addr = sevm.resolve_address_alias(ex, load_account) + if load_account_addr is not None: + return sevm.sload(ex, load_account_addr, load_slot) + else: + raise HalmosException(f"uninitialized account: {store_account}") + + # vm.fee(uint256) + elif funsig == hevm_cheat_code.fee_sig: + ex.block.basefee = simplify(Extract(255, 0, arg)) + + # vm.chainId(uint256) + elif funsig == hevm_cheat_code.chainid_sig: + ex.block.chainid = simplify(Extract(255, 0, arg)) + + # vm.coinbase(address) + elif funsig == hevm_cheat_code.coinbase_sig: + ex.block.coinbase = uint160(Extract(255, 0, arg)) + + # vm.difficulty(uint256) + elif funsig == hevm_cheat_code.difficulty_sig: + ex.block.difficulty = simplify(Extract(255, 0, arg)) + + # vm.roll(uint256) + elif funsig == hevm_cheat_code.roll_sig: + ex.block.number = simplify(Extract(255, 0, arg)) + + # vm.warp(uint256) + elif funsig == hevm_cheat_code.warp_sig: + ex.block.timestamp = simplify(Extract(255, 0, arg)) + + # vm.etch(address,bytes) + elif funsig == hevm_cheat_code.etch_sig: + who = extract_bytes(arg, 4 + 12, 20) + + # who must be concrete + if not is_bv_value(who): + error_msg = f"vm.etch(address who, bytes code) must have concrete argument `who` but received {who}" + raise HalmosException(error_msg) + + # code must be concrete + try: + code_offset = int_of(extract_bytes(arg, 4 + 32, 32)) + code_length = int_of(extract_bytes(arg, 4 + code_offset, 32)) + code_int = int_of(extract_bytes(arg, 4 + code_offset + 32, code_length)) + code_bytes = code_int.to_bytes(code_length, "big") + ex.set_code(who, code_bytes) + except Exception as e: + error_msg = f"vm.etch(address who, bytes code) must have concrete argument `code` but received calldata {arg}" + raise HalmosException(error_msg) from e + + # ffi(string[]) returns (bytes) + elif funsig == hevm_cheat_code.ffi_sig: + if not sevm.options.get("ffi"): + error_msg = "ffi cheatcode is disabled. Run again with `--ffi` if you want to enable it" + raise HalmosException(error_msg) + cmd = extract_string_array_argument(arg, 0) + process = Popen(cmd, 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", "") + + return stringified_bytes_to_bytes(out_bytes) + + else: + # TODO: support other cheat codes + msg = f"Unsupported cheat code: calldata = {hexify(arg)}" + raise HalmosException(msg) + class console: # address constant CONSOLE_ADDRESS = address(0x000000000000000000636F6e736F6c652e6c6f67); address: BitVecRef = con_addr(0x000000000000000000636F6E736F6C652E6C6F67) log_uint256: int = 0xF82C50F1 # bytes4(keccak256("log(uint256)")) - + log_uint: int = 0xF5B1BBA9 # bytes4(keccak256("log(uint256)")) log_string: int = 0x41304FAC # bytes4(keccak256("log(string)")) + + @staticmethod + def handle(ex, arg: BitVec) -> None: + funsig: int = int_of(extract_funsig(arg), "symbolic console function selector") + + if funsig == console.log_uint256 or funsig == console.log_uint: + print(extract_bytes(arg, 4, 32)) + + # elif funsig == console.log_string: + + else: + # TODO: support other console functions + info( + f"Unsupported console function: selector = 0x{funsig:0>8x}, " + f"calldata = {hexify(arg)}" + ) diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index a93ea56d..ee87f115 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -8,7 +8,6 @@ from collections import defaultdict from dataclasses import dataclass, field from functools import reduce -from subprocess import Popen, PIPE from typing import ( Any, Dict, @@ -25,32 +24,13 @@ from .cheatcodes import halmos_cheat_code, hevm_cheat_code, console, Prank from .exceptions import * -from .utils import ( - assert_address, - assert_uint256, - bv_value_to_bytes, - byte_length, - color_info, - con_addr, - create_solver, - EVM, - hexify, - int_of, - restore_precomputed_hashes, - sha3_inv, - str_opcode, - unbox_int, -) +from .utils import * from .warnings import ( warn, LIBRARY_PLACEHOLDER, INTERNAL_ERROR, ) -Word = Any # z3 expression (including constants) -Byte = Any # z3 expression (including constants) -Bytes = Any # z3 expression (including constants) -Address = BitVecRef # 160-bitvector Steps = Dict[int, Dict[str, Any]] # execution tree @@ -58,44 +38,6 @@ MAX_CALL_DEPTH = 1024 -# dynamic BitVecSort sizes -class BitVecSortCache: - def __init__(self): - self.cache = {} - for size in ( - 1, - 8, - 16, - 32, - 64, - 128, - 160, - 256, - 264, - 288, - 512, - 544, - 800, - 1024, - 1056, - ): - self.cache[size] = BitVecSort(size) - - def __getitem__(self, size: int) -> BitVecSort: - hit = self.cache.get(size) - return hit if hit is not None else BitVecSort(size) - - -BitVecSorts = BitVecSortCache() - -# known, fixed BitVecSort sizes -BitVecSort1 = BitVecSorts[1] -BitVecSort8 = BitVecSorts[8] -BitVecSort160 = BitVecSorts[160] -BitVecSort256 = BitVecSorts[256] -BitVecSort264 = BitVecSorts[264] -BitVecSort512 = BitVecSorts[512] - # symbolic states # calldataload(index) f_calldataload = Function("calldataload", BitVecSort256, BitVecSort256) @@ -170,10 +112,6 @@ def id_str(x: Any) -> str: return hexify(x).replace(" ", "") -def name_of(x: str) -> str: - return re.sub(r"\s+", "_", x) - - def padded_slice(lst: List, start: int, size: int, default=0) -> List: """ Return a slice of lst, starting at start and with size elements. If the slice @@ -224,38 +162,6 @@ def mnemonic(opcode) -> str: return str(opcode) -def concat(args): - if len(args) > 1: - return Concat(args) - else: - return args[0] - - -def uint256(x: BitVecRef) -> BitVecRef: - bitsize = x.size() - if bitsize > 256: - raise ValueError(x) - if bitsize == 256: - return x - return simplify(ZeroExt(256 - bitsize, x)) - - -def uint160(x: BitVecRef) -> BitVecRef: - bitsize = x.size() - if bitsize > 256: - raise ValueError(x) - if bitsize == 160: - return x - if bitsize > 160: - return simplify(Extract(159, 0, x)) - else: - return simplify(ZeroExt(160 - bitsize, x)) - - -def con(n: int, size_bits=256) -> Word: - return BitVecVal(n, BitVecSorts[size_bits]) - - def instruction_length(opcode: Any) -> int: opcode = int_of(opcode) return (opcode - EVM.PUSH0 + 1) if EVM.PUSH1 <= opcode <= EVM.PUSH32 else 1 @@ -350,99 +256,6 @@ def wstore_bytes( mem[loc + i] = arr[i] -def extract_bytes(data: BitVecRef, byte_offset: int, size_bytes: int) -> BitVecRef: - """Extract bytes from calldata. Zero-pad if out of bounds.""" - n = data.size() - if n % 8 != 0: - raise ValueError(n) - - # will extract hi - lo + 1 bits - hi = n - 1 - byte_offset * 8 - lo = n - byte_offset * 8 - size_bytes * 8 - lo = 0 if lo < 0 else lo - - val = simplify(Extract(hi, lo, data)) - - zero_padding = size_bytes * 8 - val.size() - if zero_padding < 0: - raise ValueError(val) - if zero_padding > 0: - val = simplify(Concat(val, con(0, zero_padding))) - - return val - - -def extract_funsig(calldata: BitVecRef): - """Extracts the function signature (first 4 bytes) from calldata""" - return extract_bytes(calldata, 0, 4) - - -def extract_string_argument(calldata: BitVecRef, arg_idx: int): - """Extracts idx-th argument of string from calldata""" - string_offset = int_of( - extract_bytes(calldata, 4 + arg_idx * 32, 32), - "symbolic offset for string argument", - ) - string_length = int_of( - extract_bytes(calldata, 4 + string_offset, 32), - "symbolic size for string argument", - ) - if string_length == 0: - return "" - string_value = int_of( - extract_bytes(calldata, 4 + string_offset + 32, string_length), - "symbolic string argument", - ) - 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) - - @dataclass(frozen=True) class EventLog: """ @@ -875,6 +688,15 @@ def current_opcode(self) -> UnionType[int, BitVecRef]: def current_instruction(self) -> Instruction: return self.pgm.decode_instruction(self.pc) + def set_code( + self, who: Address, code: UnionType[bytes, BitVecRef, Contract] + ) -> None: + """ + Sets the code at a given address. + """ + assert_address(who) + self.code[who] = code if isinstance(code, Contract) else Contract(code) + def str_cnts(self) -> str: return "".join( [ @@ -1317,31 +1139,6 @@ def add_all(cls, args: List) -> BitVecRef: SomeStorage = TypeVar("SomeStorage", bound=Storage) -# x == b if sort(x) = bool -# int_to_bool(x) == b if sort(x) = int -def test(x: Word, b: bool) -> Word: - if is_bool(x): - if b: - return x - else: - return Not(x) - elif is_bv(x): - if b: - return x != con(0) - else: - return x == con(0) - else: - raise ValueError(x) - - -def is_non_zero(x: Word) -> Word: - return test(x, True) - - -def is_zero(x: Word) -> Word: - return test(x, False) - - def bitwise(op, x: Word, y: Word) -> Word: if is_bool(x) and is_bool(y): if op == EVM.AND: @@ -1844,282 +1641,20 @@ def call_unknown() -> None: ex.solver.add(exit_code_var != con(0)) ret = arg - # TODO: factor out cheatcode semantics # halmos cheat code if eq(to, halmos_cheat_code.address): ex.solver.add(exit_code_var != con(0)) - - funsig: int = int_of( - extract_funsig(arg), "symbolic halmos cheatcode function selector" - ) - - if self.options.get("debug"): - print(f"Executing halmos cheat code: {hex(funsig)}") - - # createUint(uint256,string) returns (uint256) - if funsig == halmos_cheat_code.create_uint: - bit_size = int_of( - extract_bytes(arg, 4, 32), - "symbolic bit size for halmos.createUint()", - ) - name = name_of(extract_string_argument(arg, 1)) - if bit_size <= 256: - label = f"halmos_{name}_uint{bit_size}_{ex.new_symbol_id():>02}" - ret = uint256(BitVec(label, BitVecSorts[bit_size])) - else: - raise HalmosException(f"bitsize larger than 256: {bit_size}") - - # createBytes(uint256,string) returns (bytes) - elif funsig == halmos_cheat_code.create_bytes: - byte_size = int_of( - extract_bytes(arg, 4, 32), - "symbolic byte size for halmos.createBytes()", - ) - name = name_of(extract_string_argument(arg, 1)) - label = f"halmos_{name}_bytes_{ex.new_symbol_id():>02}" - symbolic_bytes = BitVec(label, BitVecSorts[byte_size * 8]) - ret = Concat(con(32), con(byte_size), symbolic_bytes) - - # createUint256(string) returns (uint256) - elif funsig == halmos_cheat_code.create_uint256: - name = name_of(extract_string_argument(arg, 0)) - label = f"halmos_{name}_uint256_{ex.new_symbol_id():>02}" - ret = BitVec(label, BitVecSort256) - - # createBytes32(string) returns (bytes32) - elif funsig == halmos_cheat_code.create_bytes32: - name = name_of(extract_string_argument(arg, 0)) - label = f"halmos_{name}_bytes32_{ex.new_symbol_id():>02}" - ret = BitVec(label, BitVecSort256) - - # createAddress(string) returns (address) - elif funsig == halmos_cheat_code.create_address: - name = name_of(extract_string_argument(arg, 0)) - label = f"halmos_{name}_address_{ex.new_symbol_id():>02}" - ret = uint256(BitVec(label, BitVecSort160)) - - # createBool(string) returns (bool) - elif funsig == halmos_cheat_code.create_bool: - name = name_of(extract_string_argument(arg, 0)) - label = f"halmos_{name}_bool_{ex.new_symbol_id():>02}" - ret = uint256(BitVec(label, BitVecSort1)) - - else: - error_msg = f"Unknown halmos cheat code: function selector = 0x{funsig:0>8x}, calldata = {hexify(arg)}" - raise HalmosException(error_msg) + ret = halmos_cheat_code.handle(ex, arg) # vm cheat code if eq(to, hevm_cheat_code.address): ex.solver.add(exit_code_var != con(0)) - # vm.fail() - # BitVecVal(hevm_cheat_code.fail_payload, 800) - if arg == hevm_cheat_code.fail_payload: - raise FailCheatcode() - - # vm.assume(bool) - elif ( - eq(arg.sort(), BitVecSorts[(4 + 32) * 8]) - and simplify(Extract(287, 256, arg)) == hevm_cheat_code.assume_sig - ): - assume_cond = simplify(is_non_zero(Extract(255, 0, arg))) - ex.solver.add(assume_cond) - ex.path.append(str(assume_cond)) - - # vm.getCode(string) - elif ( - simplify(Extract(arg_size * 8 - 1, arg_size * 8 - 32, arg)) - == hevm_cheat_code.get_code_sig - ): - calldata = bytes.fromhex(hex(arg.as_long())[2:]) - path_len = int.from_bytes(calldata[36:68], "big") - path = calldata[68 : 68 + path_len].decode("utf-8") - - if ":" in path: - [filename, contract_name] = path.split(":") - path = "out/" + filename + "/" + contract_name + ".json" - - target = self.options["target"].rstrip("/") - path = target + "/" + path - - with open(path) as f: - artifact = json.loads(f.read()) - - if artifact["bytecode"]["object"]: - bytecode = artifact["bytecode"]["object"].replace("0x", "") - else: - bytecode = artifact["bytecode"].replace("0x", "") - - ret = stringified_bytes_to_bytes(bytecode) - # vm.prank(address) - elif ( - eq(arg.sort(), BitVecSorts[(4 + 32) * 8]) - and simplify(Extract(287, 256, arg)) == hevm_cheat_code.prank_sig - ): - result = ex.prank.prank(uint160(Extract(255, 0, arg))) - if not result: - raise HalmosException("You have an active prank already.") - - # vm.startPrank(address) - elif ( - eq(arg.sort(), BitVecSorts[(4 + 32) * 8]) - and simplify(Extract(287, 256, arg)) - == hevm_cheat_code.start_prank_sig - ): - result = ex.prank.startPrank(uint160(Extract(255, 0, arg))) - if not result: - raise HalmosException("You have an active prank already.") - - # vm.stopPrank() - elif ( - eq(arg.sort(), BitVecSorts[4 * 8]) - and simplify(Extract(31, 0, arg)) == hevm_cheat_code.stop_prank_sig - ): - ex.prank.stopPrank() - # vm.deal(address,uint256) - elif ( - eq(arg.sort(), BitVecSorts[(4 + 32 * 2) * 8]) - and simplify(Extract(543, 512, arg)) == hevm_cheat_code.deal_sig - ): - who = uint160(Extract(511, 256, arg)) - amount = simplify(Extract(255, 0, arg)) - ex.balance_update(who, amount) - # vm.store(address,bytes32,bytes32) - elif ( - eq(arg.sort(), BitVecSorts[(4 + 32 * 3) * 8]) - and simplify(Extract(799, 768, arg)) == hevm_cheat_code.store_sig - ): - store_account = uint160(Extract(767, 512, arg)) - store_slot = simplify(Extract(511, 256, arg)) - store_value = simplify(Extract(255, 0, arg)) - store_account_addr = self.resolve_address_alias(ex, store_account) - if store_account_addr is not None: - self.sstore(ex, store_account_addr, store_slot, store_value) - else: - raise HalmosException(f"uninitialized account: {store_account}") - - # vm.load(address,bytes32) - elif ( - eq(arg.sort(), BitVecSorts[(4 + 32 * 2) * 8]) - and simplify(Extract(543, 512, arg)) == hevm_cheat_code.load_sig - ): - load_account = uint160(Extract(511, 256, arg)) - load_slot = simplify(Extract(255, 0, arg)) - load_account_addr = self.resolve_address_alias(ex, load_account) - if load_account_addr is not None: - ret = self.sload(ex, load_account_addr, load_slot) - else: - raise HalmosException(f"uninitialized account: {store_account}") - - # vm.fee(uint256) - elif ( - eq(arg.sort(), BitVecSorts[(4 + 32) * 8]) - and simplify(Extract(287, 256, arg)) == hevm_cheat_code.fee_sig - ): - ex.block.basefee = simplify(Extract(255, 0, arg)) - # vm.chainId(uint256) - elif ( - eq(arg.sort(), BitVecSorts[(4 + 32) * 8]) - and simplify(Extract(287, 256, arg)) == hevm_cheat_code.chainid_sig - ): - ex.block.chainid = simplify(Extract(255, 0, arg)) - # vm.coinbase(address) - elif ( - eq(arg.sort(), BitVecSorts[(4 + 32) * 8]) - and simplify(Extract(287, 256, arg)) == hevm_cheat_code.coinbase_sig - ): - ex.block.coinbase = uint160(Extract(255, 0, arg)) - # vm.difficulty(uint256) - elif ( - eq(arg.sort(), BitVecSorts[(4 + 32) * 8]) - and simplify(Extract(287, 256, arg)) - == hevm_cheat_code.difficulty_sig - ): - ex.block.difficulty = simplify(Extract(255, 0, arg)) - # vm.roll(uint256) - elif ( - eq(arg.sort(), BitVecSorts[(4 + 32) * 8]) - and simplify(Extract(287, 256, arg)) == hevm_cheat_code.roll_sig - ): - ex.block.number = simplify(Extract(255, 0, arg)) - # vm.warp(uint256) - elif ( - eq(arg.sort(), BitVecSorts[(4 + 32) * 8]) - and simplify(Extract(287, 256, arg)) == hevm_cheat_code.warp_sig - ): - ex.block.timestamp = simplify(Extract(255, 0, arg)) - # vm.etch(address,bytes) - elif extract_funsig(arg) == hevm_cheat_code.etch_sig: - who = extract_bytes(arg, 4 + 12, 20) - - # who must be concrete - if not is_bv_value(who): - error_msg = f"vm.etch(address who, bytes code) must have concrete argument `who` but received {who}" - raise HalmosException(error_msg) - - # code must be concrete - try: - code_offset = int_of(extract_bytes(arg, 4 + 32, 32)) - code_length = int_of(extract_bytes(arg, 4 + code_offset, 32)) - code_int = int_of( - extract_bytes(arg, 4 + code_offset + 32, code_length) - ) - code_bytes = code_int.to_bytes(code_length, "big") - - ex.code[who] = Contract(code_bytes) - except Exception as e: - error_msg = f"vm.etch(address who, bytes code) must have concrete argument `code` but received calldata {arg}" - raise HalmosException(error_msg) from e - # ffi(string[]) returns (bytes) - elif extract_funsig(arg) == hevm_cheat_code.ffi_sig: - if not self.options.get("ffi"): - error_msg = "ffi cheatcode is disabled. Run again with `--ffi` if you want to enable it" - raise HalmosException(error_msg) - cmd = extract_string_array_argument(arg, 0) - process = Popen(cmd, 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 - msg = f"Unsupported cheat code: calldata = {hexify(arg)}" - raise HalmosException(msg) + ret = hevm_cheat_code.handle(self, ex, arg) # console if eq(to, console.address): ex.solver.add(exit_code_var != con(0)) - - funsig: int = int_of( - extract_funsig(arg), "symbolic console function selector" - ) - - if funsig == console.log_uint256: - print(extract_bytes(arg, 4, 32)) - - # elif funsig == console.log_string: - - else: - # TODO: support other console functions - print( - color_info( - f"Unsupported console function: selector = 0x{funsig:0>8x}, " - f"calldata = {hexify(arg)}" - ) - ) + console.handle(ex, arg) # store return value if ret_size > 0: diff --git a/src/halmos/utils.py b/src/halmos/utils.py index 7de305e0..675427f8 100644 --- a/src/halmos/utils.py +++ b/src/halmos/utils.py @@ -10,6 +10,108 @@ from .exceptions import NotConcreteError +Word = Any # z3 expression (including constants) +Byte = Any # z3 expression (including constants) +Bytes = Any # z3 expression (including constants) +Address = BitVecRef # 160-bitvector + + +# dynamic BitVecSort sizes +class BitVecSortCache: + def __init__(self): + self.cache = {} + for size in ( + 1, + 8, + 16, + 32, + 64, + 128, + 160, + 256, + 264, + 288, + 512, + 544, + 800, + 1024, + 1056, + ): + self.cache[size] = BitVecSort(size) + + def __getitem__(self, size: int) -> BitVecSort: + hit = self.cache.get(size) + return hit if hit is not None else BitVecSort(size) + + +BitVecSorts = BitVecSortCache() + +# known, fixed BitVecSort sizes +BitVecSort1 = BitVecSorts[1] +BitVecSort8 = BitVecSorts[8] +BitVecSort160 = BitVecSorts[160] +BitVecSort256 = BitVecSorts[256] +BitVecSort264 = BitVecSorts[264] +BitVecSort512 = BitVecSorts[512] + + +def concat(args): + if len(args) > 1: + return Concat(args) + else: + return args[0] + + +def uint256(x: BitVecRef) -> BitVecRef: + bitsize = x.size() + if bitsize > 256: + raise ValueError(x) + if bitsize == 256: + return x + return simplify(ZeroExt(256 - bitsize, x)) + + +def uint160(x: BitVecRef) -> BitVecRef: + bitsize = x.size() + if bitsize > 256: + raise ValueError(x) + if bitsize == 160: + return x + if bitsize > 160: + return simplify(Extract(159, 0, x)) + else: + return simplify(ZeroExt(160 - bitsize, x)) + + +def con(n: int, size_bits=256) -> Word: + return BitVecVal(n, BitVecSorts[size_bits]) + + +# x == b if sort(x) = bool +# int_to_bool(x) == b if sort(x) = int +def test(x: Word, b: bool) -> Word: + if is_bool(x): + if b: + return x + else: + return Not(x) + elif is_bv(x): + if b: + return x != con(0) + else: + return x == con(0) + else: + raise ValueError(x) + + +def is_non_zero(x: Word) -> Word: + return test(x, True) + + +def is_zero(x: Word) -> Word: + return test(x, False) + + def create_solver(logic="QF_AUFBV", ctx=None, timeout=0, max_memory=0): # QF_AUFBV: quantifier-free bitvector + array theory: https://smtlib.cs.uiowa.edu/logics.shtml solver = SolverFor(logic, ctx=ctx) @@ -24,6 +126,33 @@ def create_solver(logic="QF_AUFBV", ctx=None, timeout=0, max_memory=0): return solver +def extract_bytes(data: BitVecRef, byte_offset: int, size_bytes: int) -> BitVecRef: + """Extract bytes from calldata. Zero-pad if out of bounds.""" + n = data.size() + if n % 8 != 0: + raise ValueError(n) + + # will extract hi - lo + 1 bits + hi = n - 1 - byte_offset * 8 + lo = n - byte_offset * 8 - size_bytes * 8 + lo = 0 if lo < 0 else lo + + val = simplify(Extract(hi, lo, data)) + + zero_padding = size_bytes * 8 - val.size() + if zero_padding < 0: + raise ValueError(val) + if zero_padding > 0: + val = simplify(Concat(val, con(0, zero_padding))) + + return val + + +def extract_funsig(calldata: BitVecRef): + """Extracts the function signature (first 4 bytes) from calldata""" + return extract_bytes(calldata, 0, 4) + + def bv_value_to_bytes(x: BitVecNumRef) -> bytes: if x.size() % 8 != 0: raise ValueError(x, x.size()) @@ -113,7 +242,7 @@ def stringify(symbol_name: str, val: Any): return f"0x{val.as_long():0{byte_length(val) * 2}x}" elif type_name == "bool": return str(val.as_long() != 0).lower() - elif type_name == "string": + elif type_name == "string" or "string" in symbol_name: # XXX TEMP HACK str_val = bytes.fromhex(hexify(val)[2:]).decode("utf-8") return f'"{str_val}"' elif type_name == "bytes": From d3b16a7e1b1f23052b3333697554d5fb4ccf30ae Mon Sep 17 00:00:00 2001 From: karmacoma Date: Mon, 16 Oct 2023 17:38:54 -0700 Subject: [PATCH 4/9] add more console.log functions with type based rendering --- src/halmos/cheatcodes.py | 126 +++++++++++++++++++++++----- src/halmos/utils.py | 57 +++++++++---- tests/regression/remappings.txt | 1 + tests/regression/test/Console.t.sol | 68 ++++++++++++++- 4 files changed, 212 insertions(+), 40 deletions(-) diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index d6004077..4ac43a28 100644 --- a/src/halmos/cheatcodes.py +++ b/src/halmos/cheatcodes.py @@ -20,24 +20,26 @@ def name_of(x: str) -> str: return re.sub(r"\s+", "_", x) -def extract_string_argument(calldata: BitVecRef, arg_idx: int): +def extract_bytes_argument(calldata: BitVecRef, arg_idx: int) -> bytes: """Extracts idx-th argument of string from calldata""" - string_offset = int_of( + offset = int_of( extract_bytes(calldata, 4 + arg_idx * 32, 32), - "symbolic offset for string argument", - ) - string_length = int_of( - extract_bytes(calldata, 4 + string_offset, 32), - "symbolic size for string argument", + "symbolic offset for bytes argument", ) - if string_length == 0: - return "" - string_value = int_of( - extract_bytes(calldata, 4 + string_offset + 32, string_length), - "symbolic string argument", + length = int_of( + extract_bytes(calldata, 4 + offset, 32), + "symbolic size for bytes argument", ) - string_bytes = string_value.to_bytes(string_length, "big") - return string_bytes.decode("utf-8") + if length == 0: + return b"" + + return bv_value_to_bytes(extract_bytes(calldata, 4 + offset + 32, length)) + + +def extract_string_argument(calldata: BitVecRef, arg_idx: int): + """Extracts idx-th argument of string from calldata""" + string_bytes = extract_bytes_argument(calldata, arg_idx) + return string_bytes.decode("utf-8") if string_bytes else "" def extract_string_array_argument(calldata: BitVecRef, arg_idx: int): @@ -463,25 +465,103 @@ def handle(sevm, ex, arg: BitVec) -> BitVec: class console: - # address constant CONSOLE_ADDRESS = address(0x000000000000000000636F6e736F6c652e6c6f67); + # see forge-std/console2.sol address: BitVecRef = con_addr(0x000000000000000000636F6E736F6C652E6C6F67) - log_uint256: int = 0xF82C50F1 # bytes4(keccak256("log(uint256)")) - log_uint: int = 0xF5B1BBA9 # bytes4(keccak256("log(uint256)")) - log_string: int = 0x41304FAC # bytes4(keccak256("log(string)")) + @staticmethod + def log_uint256(arg: BitVec) -> None: + b = extract_bytes(arg, 4, 32) + console.log(render_uint(b)) + + @staticmethod + def log_string(arg: BitVec) -> None: + str_val = extract_string_argument(arg, 0) + console.log(str_val) + + @staticmethod + def log_bytes(arg: BitVec) -> None: + b = extract_bytes_argument(arg, 0) + console.log(render_bytes(b)) + + @staticmethod + def log_string_address(arg: BitVec) -> None: + str_val = extract_string_argument(arg, 0) + addr = extract_bytes(arg, 36, 32) + console.log(f"{str_val} {render_address(addr)}") + + @staticmethod + def log_address(arg: BitVec) -> None: + addr = extract_bytes(arg, 4, 32) + console.log(render_address(addr)) + + @staticmethod + def log_string_bool(arg: BitVec) -> None: + str_val = extract_string_argument(arg, 0) + bool_val = extract_bytes(arg, 36, 32) + console.log(f"{str_val} {render_bool(bool_val)}") + + @staticmethod + def log_bool(arg: BitVec) -> None: + bool_val = extract_bytes(arg, 4, 32) + console.log(render_bool(bool_val)) + + @staticmethod + def log_string_string(arg: BitVec) -> None: + str1_val = extract_string_argument(arg, 0) + str2_val = extract_string_argument(arg, 1) + console.log(f"{str1_val} {str2_val}") + + @staticmethod + def log_bytes32(arg: BitVec) -> None: + b = extract_bytes(arg, 4, 32) + console.log(hexify(b)) + + @staticmethod + def log_string_int256(arg: BitVec) -> None: + str_val = extract_string_argument(arg, 0) + int_val = extract_bytes(arg, 36, 32) + console.log(f"{str_val} {render_int(int_val)}") + + @staticmethod + def log_int256(arg: BitVec) -> None: + int_val = extract_bytes(arg, 4, 32) + console.log(render_int(int_val)) + + @staticmethod + def log_string_uint256(arg: BitVec) -> None: + str_val = extract_string_argument(arg, 0) + uint_val = extract_bytes(arg, 36, 32) + console.log(f"{str_val} {render_uint(uint_val)}") + + @staticmethod + def log(what: str) -> None: + print(f"console.log: {magenta(what)}") @staticmethod def handle(ex, arg: BitVec) -> None: funsig: int = int_of(extract_funsig(arg), "symbolic console function selector") - if funsig == console.log_uint256 or funsig == console.log_uint: - print(extract_bytes(arg, 4, 32)) - - # elif funsig == console.log_string: + if funsig in console.handlers: + console.handlers[funsig](arg) else: - # TODO: support other console functions info( f"Unsupported console function: selector = 0x{funsig:0>8x}, " f"calldata = {hexify(arg)}" ) + + handlers = { + 0xF82C50F1: log_uint256, + 0xF5B1BBA9: log_uint256, # alias for 'log(uint)' + 0x41304FAC: log_string, + 0x0BE77F56: log_bytes, + 0x319AF333: log_string_address, + 0x2C2ECBC2: log_address, + 0xC3B55635: log_string_bool, + 0x32458EED: log_bool, + 0x4B5C4277: log_string_string, + 0x27B7CF85: log_bytes32, + 0x3CA6268E: log_string_int256, + 0x2D5B6CB9: log_int256, + 0xB60E72CC: log_string_uint256, + } diff --git a/src/halmos/utils.py b/src/halmos/utils.py index 675427f8..58b1101b 100644 --- a/src/halmos/utils.py +++ b/src/halmos/utils.py @@ -3,7 +3,7 @@ import re from timeit import default_timer as timer -from typing import Dict, Tuple, Any +from typing import Dict, Tuple, Any, Union as UnionType from z3 import * @@ -211,6 +211,36 @@ def hexify(x): return hexify(str(x)) +def render_uint(x: BitVecRef) -> str: + val = int_of(x) + return f"0x{val:0{byte_length(x) * 2}x} ({val})" + + +def render_int(x: BitVecRef) -> str: + val = x.as_signed_long() + return f"0x{x.as_long():0{byte_length(x) * 2}x} ({val})" + + +def render_bool(b: BitVecRef) -> str: + return str(b.as_long() != 0).lower() + + +def render_string(s: BitVecRef) -> str: + str_val = bytes.fromhex(hexify(s)[2:]).decode("utf-8") + return f'"{str_val}"' + + +def render_bytes(b: UnionType[BitVecRef, bytes]) -> str: + if is_bv(b): + return f'hex"{hex(b.as_long())[2:]}"' + else: + return f'hex"{b.hex()[2:]}"' + + +def render_address(a: BitVecRef) -> str: + return f"0x{a.as_long():040x}" + + def stringify(symbol_name: str, val: Any): """ Formats a value based on the inferred type of the variable. @@ -233,23 +263,18 @@ def stringify(symbol_name: str, val: Any): type_name = tokens[-1] if type_name.startswith("uint"): - v = val.as_long() - return v if v < 2**64 else hex(v) + return render_uint(val) elif type_name.startswith("int"): - v = val.as_signed_long() - if -(2**63) <= v < 2**63: - return v - return f"0x{val.as_long():0{byte_length(val) * 2}x}" + return render_int(val) elif type_name == "bool": - return str(val.as_long() != 0).lower() - elif type_name == "string" or "string" in symbol_name: # XXX TEMP HACK - str_val = bytes.fromhex(hexify(val)[2:]).decode("utf-8") - return f'"{str_val}"' + return render_bool(val) + elif type_name == "string": + return render_string(val) elif type_name == "bytes": - return f'hex"{hex(val.as_long())[2:]}"' + return render_bytes(val) elif type_name == "address": - return f"0x{val.as_long():040x}" - else: # address, bytes32, bytes4, structs, etc. + return render_address(val) + else: # bytes32, bytes4, structs, etc. return hexify(val) @@ -287,6 +312,10 @@ def cyan(text: str) -> str: return f"\033[36m{text}\033[0m" +def magenta(text: str) -> str: + return f"\033[35m{text}\033[0m" + + def color_good(text: str) -> str: return green(text) diff --git a/tests/regression/remappings.txt b/tests/regression/remappings.txt index 41f9d750..30f1086e 100644 --- a/tests/regression/remappings.txt +++ b/tests/regression/remappings.txt @@ -1,2 +1,3 @@ openzeppelin/=../lib/openzeppelin-contracts/contracts/ ds-test/=../lib/forge-std/lib/ds-test/src/ +forge-std/=../lib/forge-std/src/ diff --git a/tests/regression/test/Console.t.sol b/tests/regression/test/Console.t.sol index 117a3c95..6f00b515 100644 --- a/tests/regression/test/Console.t.sol +++ b/tests/regression/test/Console.t.sol @@ -2,10 +2,72 @@ pragma solidity >=0.8.0 <0.9.0; import "forge-std/Test.sol"; +import {console2} from "forge-std/console2.sol"; contract ConsoleTest is Test { - function check_log() public view { - console.log(0); - console.log(1); + function test_log_uint() public view { + console2.log("this is 0:", uint256(0)); + console2.log("this is 1:", uint256(1)); + + console2.log(uint256(0)); + console2.log(uint256(1)); + + console2.logUint(0); + console2.logUint(1); + } + + function test_log_int() public view { + console2.log("this is -1:", -1); + console2.log("this is 1:", int256(1)); + + console2.log(-1); + console2.log(int256(1)); + + console2.logInt(-1); + console2.logInt(int256(1)); + } + + function test_log_bytes() public view { + console2.log("this is hello (bytes):", "hello"); + console2.log("this is empty bytes:", ""); + + console2.logBytes("hello"); + console2.logBytes(""); + } + + function test_log_bytes32() public view { + console2.log("this is keccak256(hello):"); + console2.logBytes32(keccak256("hello")); + + console2.log("this is keccak256():"); + console2.logBytes32(keccak256("")); + } + + function test_log_address() public view { + console2.log("this is address(0):", address(0)); + console2.log("this is address(this):", address(this)); + + console2.log(address(0)); + console2.log(address(this)); + } + + function test_log_bool() public view { + console2.log("this is true:", true); + console2.log("this is false:", false); + + console2.log(true); + console2.log(false); + } + + function test_log_string() public view { + console2.log("this is hello (string):", "hello"); + console2.log("this is empty string:", ""); + + console2.log("hello"); + console2.log(""); + } + + function test_log_unsupported() public { + console2._sendLogPayload(abi.encodeWithSignature("doesNotExist()")); } } From b09fcd95799a9a962ff1869ba3c2b92305a295e6 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Tue, 17 Oct 2023 18:04:53 -0700 Subject: [PATCH 5/9] implement new halmos cheatcodes --- src/halmos/cheatcodes.py | 182 +++++++++++++++++++++------------------ 1 file changed, 97 insertions(+), 85 deletions(-) diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index 4ac43a28..452dca8f 100644 --- a/src/halmos/cheatcodes.py +++ b/src/halmos/cheatcodes.py @@ -149,93 +149,106 @@ class halmos_cheat_code: # address(bytes20(uint160(uint256(keccak256('svm cheat code'))))); address: BitVecRef = con_addr(0xF3993A62377BCD56AE39D773740A5390411E8BC9) - # bytes4(keccak256("createUint(uint256,string)")) - create_uint: int = 0x66830DFA + @staticmethod + def create_generic(ex, bits: int, var_name: str, type_name: str) -> BitVecRef: + label = f"halmos_{var_name}_{type_name}_{ex.new_symbol_id():>02}" + return BitVec(label, BitVecSorts[bits]) - # bytes4(keccak256("createUint256(string)")) - create_uint256: int = 0xBC7BEEFC + @staticmethod + def handle_create_uint(ex, arg): + bits = int_of( + extract_bytes(arg, 4, 32), "symbolic bit size for halmos.createUint()" + ) + if bits > 256: + raise HalmosException(f"bitsize larger than 256: {bits}") - # bytes4(keccak256("createInt(uint256,string)")) - create_int: int = 0x49B9C7D4 + name = name_of(extract_string_argument(arg, 1)) + return halmos_cheat_code.create_generic(ex, bits, name, f"uint{bits}") - # bytes4(keccak256("createInt256(string)")) - create_int256: int = 0xC2CE6AED + @staticmethod + def handle_create_uint256(ex, arg): + name = name_of(extract_string_argument(arg, 0)) + return halmos_cheat_code.create_generic(ex, 256, name, "uint256") - # bytes4(keccak256("createBytes(uint256,string)")) - create_bytes: int = 0xEEF5311D + @staticmethod + def handle_create_int(ex, arg): + bits = int_of( + extract_bytes(arg, 4, 32), "symbolic bit size for halmos.createUint()" + ) + if bits > 256: + raise HalmosException(f"bitsize larger than 256: {bits}") - # bytes4(keccak256("createString(uint256,string)")) - create_string: int = 0xCE68656C + name = name_of(extract_string_argument(arg, 1)) + return halmos_cheat_code.create_generic(ex, bits, name, f"int{bits}") - # bytes4(keccak256("createBytes4(string)")) - create_bytes4: int = 0xDE143925 + @staticmethod + def handle_create_int256(ex, arg): + name = name_of(extract_string_argument(arg, 0)) + return halmos_cheat_code.create_generic(ex, 256, name, "int256") - # bytes4(keccak256("createBytes32(string)")) - create_bytes32: int = 0xBF72FA66 + @staticmethod + def handle_create_bytes(ex, arg): + byte_size = int_of( + extract_bytes(arg, 4, 32), "symbolic byte size for halmos.createBytes()" + ) + name = name_of(extract_string_argument(arg, 1)) + symbolic_bytes = halmos_cheat_code.create_generic( + ex, byte_size * 8, name, "bytes" + ) + return Concat(con(32), con(byte_size), symbolic_bytes) - # bytes4(keccak256("createAddress(string)")) - create_address: int = 0x3B0FA01B + @staticmethod + def handle_create_string(ex, arg): + byte_size = int_of( + extract_bytes(arg, 4, 32), "symbolic byte size for halmos.createString()" + ) + name = name_of(extract_string_argument(arg, 1)) + symbolic_string = halmos_cheat_code.create_generic( + ex, byte_size * 8, name, "string" + ) + return Concat(con(32), con(byte_size), symbolic_string) - # bytes4(keccak256("createBool(string)")) - create_bool: int = 0x6E0BB659 + @staticmethod + def handle_create_bytes4(ex, arg): + name = name_of(extract_string_argument(arg, 0)) + return uint256(halmos_cheat_code.create_generic(ex, 32, name, "bytes4")) @staticmethod - def handle(ex, arg: BitVec) -> BitVec: - funsig: int = int_of(extract_funsig(arg), "symbolic halmos cheatcode") + def handle_create_bytes32(ex, arg): + name = name_of(extract_string_argument(arg, 0)) + return halmos_cheat_code.create_generic(ex, 256, name, "bytes32") - # createUint(uint256,string) returns (uint256) - if funsig == halmos_cheat_code.create_uint: - bit_size = int_of( - extract_bytes(arg, 4, 32), - "symbolic bit size for halmos.createUint()", - ) - name = name_of(extract_string_argument(arg, 1)) - if bit_size <= 256: - label = f"halmos_{name}_uint{bit_size}_{ex.new_symbol_id():>02}" - ret = uint256(BitVec(label, BitVecSorts[bit_size])) - else: - raise HalmosException(f"bitsize larger than 256: {bit_size}") + @staticmethod + def handle_create_address(ex, arg): + name = name_of(extract_string_argument(arg, 0)) + return uint256(halmos_cheat_code.create_generic(ex, 160, name, "address")) - # createBytes(uint256,string) returns (bytes) - elif funsig == halmos_cheat_code.create_bytes: - byte_size = int_of( - extract_bytes(arg, 4, 32), - "symbolic byte size for halmos.createBytes()", - ) - name = name_of(extract_string_argument(arg, 1)) - label = f"halmos_{name}_bytes_{ex.new_symbol_id():>02}" - symbolic_bytes = BitVec(label, BitVecSorts[byte_size * 8]) - ret = Concat(con(32), con(byte_size), symbolic_bytes) - - # createUint256(string) returns (uint256) - elif funsig == halmos_cheat_code.create_uint256: - name = name_of(extract_string_argument(arg, 0)) - label = f"halmos_{name}_uint256_{ex.new_symbol_id():>02}" - ret = BitVec(label, BitVecSort256) - - # createBytes32(string) returns (bytes32) - elif funsig == halmos_cheat_code.create_bytes32: - name = name_of(extract_string_argument(arg, 0)) - label = f"halmos_{name}_bytes32_{ex.new_symbol_id():>02}" - ret = BitVec(label, BitVecSort256) - - # createAddress(string) returns (address) - elif funsig == halmos_cheat_code.create_address: - name = name_of(extract_string_argument(arg, 0)) - label = f"halmos_{name}_address_{ex.new_symbol_id():>02}" - ret = uint256(BitVec(label, BitVecSort160)) - - # createBool(string) returns (bool) - elif funsig == halmos_cheat_code.create_bool: - name = name_of(extract_string_argument(arg, 0)) - label = f"halmos_{name}_bool_{ex.new_symbol_id():>02}" - ret = uint256(BitVec(label, BitVecSort1)) + @staticmethod + def handle_create_bool(ex, arg): + name = name_of(extract_string_argument(arg, 0)) + return uint256(halmos_cheat_code.create_generic(ex, 1, name, "bool")) - else: - error_msg = f"Unknown halmos cheat code: function selector = 0x{funsig:0>8x}, calldata = {hexify(arg)}" - raise HalmosException(error_msg) + handlers = { + 0x66830DFA: handle_create_uint, # createUint(uint256,string) + 0xBC7BEEFC: handle_create_uint256, # createUint256(string) + 0x49B9C7D4: handle_create_int, # createInt(uint256,string) + 0xC2CE6AED: handle_create_int256, # createInt256(string) + 0xEEF5311D: handle_create_bytes, # createBytes(uint256,string) + 0xCE68656C: handle_create_string, # createString(uint256,string) + 0xDE143925: handle_create_bytes4, # createBytes4(string) + 0xBF72FA66: handle_create_bytes32, # createBytes32(string) + 0x3B0FA01B: handle_create_address, # createAddress(string) + 0x6E0BB659: handle_create_bool, # createBool(string) + } + + @staticmethod + def handle(ex, arg: BitVec) -> BitVec: + funsig = int_of(extract_funsig(arg), "symbolic halmos cheatcode") + if handler := halmos_cheat_code.handlers.get(funsig): + return handler(ex, arg) - return ret + error_msg = f"Unknown halmos cheat code: function selector = 0x{funsig:0>8x}, calldata = {hexify(arg)}" + raise HalmosException(error_msg) class hevm_cheat_code: @@ -537,19 +550,6 @@ def log_string_uint256(arg: BitVec) -> None: def log(what: str) -> None: print(f"console.log: {magenta(what)}") - @staticmethod - def handle(ex, arg: BitVec) -> None: - funsig: int = int_of(extract_funsig(arg), "symbolic console function selector") - - if funsig in console.handlers: - console.handlers[funsig](arg) - - else: - info( - f"Unsupported console function: selector = 0x{funsig:0>8x}, " - f"calldata = {hexify(arg)}" - ) - handlers = { 0xF82C50F1: log_uint256, 0xF5B1BBA9: log_uint256, # alias for 'log(uint)' @@ -565,3 +565,15 @@ def handle(ex, arg: BitVec) -> None: 0x2D5B6CB9: log_int256, 0xB60E72CC: log_string_uint256, } + + @staticmethod + def handle(ex, arg: BitVec) -> None: + funsig: int = int_of(extract_funsig(arg), "symbolic console function selector") + + if handler := console.handlers.get(funsig): + return handler(arg) + + info( + f"Unsupported console function: selector = 0x{funsig:0>8x}, " + f"calldata = {hexify(arg)}" + ) From 084eaa47e216846fc1674938c601ef982a441c29 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Wed, 18 Oct 2023 15:20:55 -0700 Subject: [PATCH 6/9] rename tests in Console.t.sol and update expected json --- src/halmos/cheatcodes.py | 42 +++++++++---------- tests/expected/all.json | 65 ++++++++++++++++++++++++++++- tests/regression/test/Console.t.sol | 37 ++++++++-------- 3 files changed, 105 insertions(+), 39 deletions(-) diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index 452dca8f..528a378d 100644 --- a/src/halmos/cheatcodes.py +++ b/src/halmos/cheatcodes.py @@ -155,7 +155,7 @@ def create_generic(ex, bits: int, var_name: str, type_name: str) -> BitVecRef: return BitVec(label, BitVecSorts[bits]) @staticmethod - def handle_create_uint(ex, arg): + def create_uint(ex, arg): bits = int_of( extract_bytes(arg, 4, 32), "symbolic bit size for halmos.createUint()" ) @@ -163,15 +163,15 @@ def handle_create_uint(ex, arg): raise HalmosException(f"bitsize larger than 256: {bits}") name = name_of(extract_string_argument(arg, 1)) - return halmos_cheat_code.create_generic(ex, bits, name, f"uint{bits}") + return uint256(halmos_cheat_code.create_generic(ex, bits, name, f"uint{bits}")) @staticmethod - def handle_create_uint256(ex, arg): + def create_uint256(ex, arg): name = name_of(extract_string_argument(arg, 0)) return halmos_cheat_code.create_generic(ex, 256, name, "uint256") @staticmethod - def handle_create_int(ex, arg): + def create_int(ex, arg): bits = int_of( extract_bytes(arg, 4, 32), "symbolic bit size for halmos.createUint()" ) @@ -182,12 +182,12 @@ def handle_create_int(ex, arg): return halmos_cheat_code.create_generic(ex, bits, name, f"int{bits}") @staticmethod - def handle_create_int256(ex, arg): + def create_int256(ex, arg): name = name_of(extract_string_argument(arg, 0)) return halmos_cheat_code.create_generic(ex, 256, name, "int256") @staticmethod - def handle_create_bytes(ex, arg): + def create_bytes(ex, arg): byte_size = int_of( extract_bytes(arg, 4, 32), "symbolic byte size for halmos.createBytes()" ) @@ -198,7 +198,7 @@ def handle_create_bytes(ex, arg): return Concat(con(32), con(byte_size), symbolic_bytes) @staticmethod - def handle_create_string(ex, arg): + def create_string(ex, arg): byte_size = int_of( extract_bytes(arg, 4, 32), "symbolic byte size for halmos.createString()" ) @@ -209,36 +209,36 @@ def handle_create_string(ex, arg): return Concat(con(32), con(byte_size), symbolic_string) @staticmethod - def handle_create_bytes4(ex, arg): + def create_bytes4(ex, arg): name = name_of(extract_string_argument(arg, 0)) return uint256(halmos_cheat_code.create_generic(ex, 32, name, "bytes4")) @staticmethod - def handle_create_bytes32(ex, arg): + def create_bytes32(ex, arg): name = name_of(extract_string_argument(arg, 0)) return halmos_cheat_code.create_generic(ex, 256, name, "bytes32") @staticmethod - def handle_create_address(ex, arg): + def create_address(ex, arg): name = name_of(extract_string_argument(arg, 0)) return uint256(halmos_cheat_code.create_generic(ex, 160, name, "address")) @staticmethod - def handle_create_bool(ex, arg): + def create_bool(ex, arg): name = name_of(extract_string_argument(arg, 0)) return uint256(halmos_cheat_code.create_generic(ex, 1, name, "bool")) handlers = { - 0x66830DFA: handle_create_uint, # createUint(uint256,string) - 0xBC7BEEFC: handle_create_uint256, # createUint256(string) - 0x49B9C7D4: handle_create_int, # createInt(uint256,string) - 0xC2CE6AED: handle_create_int256, # createInt256(string) - 0xEEF5311D: handle_create_bytes, # createBytes(uint256,string) - 0xCE68656C: handle_create_string, # createString(uint256,string) - 0xDE143925: handle_create_bytes4, # createBytes4(string) - 0xBF72FA66: handle_create_bytes32, # createBytes32(string) - 0x3B0FA01B: handle_create_address, # createAddress(string) - 0x6E0BB659: handle_create_bool, # createBool(string) + 0x66830DFA: create_uint, # createUint(uint256,string) + 0xBC7BEEFC: create_uint256, # createUint256(string) + 0x49B9C7D4: create_int, # createInt(uint256,string) + 0xC2CE6AED: create_int256, # createInt256(string) + 0xEEF5311D: create_bytes, # createBytes(uint256,string) + 0xCE68656C: create_string, # createString(uint256,string) + 0xDE143925: create_bytes4, # createBytes4(string) + 0xBF72FA66: create_bytes32, # createBytes32(string) + 0x3B0FA01B: create_address, # createAddress(string) + 0x6E0BB659: create_bool, # createBool(string) } @staticmethod diff --git a/tests/expected/all.json b/tests/expected/all.json index 1f227576..2b8b95a8 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -273,7 +273,70 @@ ], "test/Console.t.sol:ConsoleTest": [ { - "name": "check_log()", + "name": "check_log_address()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_log_bool()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_log_bytes()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_log_bytes32()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_log_int()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_log_string()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_log_uint()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_log_unsupported()", "exitcode": 0, "num_models": 0, "models": null, diff --git a/tests/regression/test/Console.t.sol b/tests/regression/test/Console.t.sol index 6f00b515..96d6bd85 100644 --- a/tests/regression/test/Console.t.sol +++ b/tests/regression/test/Console.t.sol @@ -5,7 +5,7 @@ import "forge-std/Test.sol"; import {console2} from "forge-std/console2.sol"; contract ConsoleTest is Test { - function test_log_uint() public view { + function check_log_uint() public view { console2.log("this is 0:", uint256(0)); console2.log("this is 1:", uint256(1)); @@ -16,7 +16,7 @@ contract ConsoleTest is Test { console2.logUint(1); } - function test_log_int() public view { + function check_log_int() public view { console2.log("this is -1:", -1); console2.log("this is 1:", int256(1)); @@ -27,15 +27,16 @@ contract ConsoleTest is Test { console2.logInt(int256(1)); } - function test_log_bytes() public view { - console2.log("this is hello (bytes):", "hello"); - console2.log("this is empty bytes:", ""); - - console2.logBytes("hello"); - console2.logBytes(""); + function check_log_bytes() public view { + bytes memory hello = "hello"; + bytes memory empty = ""; + console2.log("this is hello (bytes):"); + console2.logBytes(hello); + console2.log("this is empty bytes:"); + console2.logBytes(empty); } - function test_log_bytes32() public view { + function check_log_bytes32() public view { console2.log("this is keccak256(hello):"); console2.logBytes32(keccak256("hello")); @@ -43,7 +44,7 @@ contract ConsoleTest is Test { console2.logBytes32(keccak256("")); } - function test_log_address() public view { + function check_log_address() public view { console2.log("this is address(0):", address(0)); console2.log("this is address(this):", address(this)); @@ -51,7 +52,7 @@ contract ConsoleTest is Test { console2.log(address(this)); } - function test_log_bool() public view { + function check_log_bool() public view { console2.log("this is true:", true); console2.log("this is false:", false); @@ -59,15 +60,17 @@ contract ConsoleTest is Test { console2.log(false); } - function test_log_string() public view { - console2.log("this is hello (string):", "hello"); - console2.log("this is empty string:", ""); + function check_log_string() public view { + string memory hello = "hello"; + string memory empty = ""; + console2.log("this is hello (string):", hello); + console2.log("this is empty string:", empty); - console2.log("hello"); - console2.log(""); + console2.log(hello); + console2.log(empty); } - function test_log_unsupported() public { + function check_log_unsupported() public { console2._sendLogPayload(abi.encodeWithSignature("doesNotExist()")); } } From f8025d6d629a730591c40c3f47775bd5fa15be95 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Wed, 18 Oct 2023 15:40:48 -0700 Subject: [PATCH 7/9] update halmos-cheatcodes + tests + fix createInt --- src/halmos/cheatcodes.py | 2 +- src/halmos/utils.py | 9 ++++++ tests/expected/all.json | 36 +++++++++++++++++++++ tests/lib/halmos-cheatcodes | 2 +- tests/regression/test/HalmosCheatCode.t.sol | 27 ++++++++++++++++ 5 files changed, 74 insertions(+), 2 deletions(-) diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index 528a378d..5cd5f024 100644 --- a/src/halmos/cheatcodes.py +++ b/src/halmos/cheatcodes.py @@ -179,7 +179,7 @@ def create_int(ex, arg): raise HalmosException(f"bitsize larger than 256: {bits}") name = name_of(extract_string_argument(arg, 1)) - return halmos_cheat_code.create_generic(ex, bits, name, f"int{bits}") + return int256(halmos_cheat_code.create_generic(ex, bits, name, f"int{bits}")) @staticmethod def create_int256(ex, arg): diff --git a/src/halmos/utils.py b/src/halmos/utils.py index 58b1101b..c6832010 100644 --- a/src/halmos/utils.py +++ b/src/halmos/utils.py @@ -71,6 +71,15 @@ def uint256(x: BitVecRef) -> BitVecRef: return simplify(ZeroExt(256 - bitsize, x)) +def int256(x: BitVecRef) -> BitVecRef: + bitsize = x.size() + if bitsize > 256: + raise ValueError(x) + if bitsize == 256: + return x + return simplify(SignExt(256 - bitsize, x)) + + def uint160(x: BitVecRef) -> BitVecRef: bitsize = x.size() if bitsize > 256: diff --git a/tests/expected/all.json b/tests/expected/all.json index 2b8b95a8..e1d99045 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -870,6 +870,42 @@ "time": null, "num_bounded_loops": null }, + { + "name": "check_createBytes4()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_createInt()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_createInt256()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_createString()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, { "name": "check_createUint()", "exitcode": 0, diff --git a/tests/lib/halmos-cheatcodes b/tests/lib/halmos-cheatcodes index c9e5f804..c0d86550 160000 --- a/tests/lib/halmos-cheatcodes +++ b/tests/lib/halmos-cheatcodes @@ -1 +1 @@ -Subproject commit c9e5f80441b9d8aeb2e724db07a1322e59aaeb82 +Subproject commit c0d865508c0fee0a11b97732c5e90f9cad6b65a5 diff --git a/tests/regression/test/HalmosCheatCode.t.sol b/tests/regression/test/HalmosCheatCode.t.sol index 1207ae48..ee928f81 100644 --- a/tests/regression/test/HalmosCheatCode.t.sol +++ b/tests/regression/test/HalmosCheatCode.t.sol @@ -13,6 +13,15 @@ contract HalmosCheatCodeTest is SymTest { assert(0 <= z && z <= type(uint8).max); } + function check_createInt() public { + int x = svm.createInt(256, 'x'); + int y = svm.createInt(160, 'y'); + int z = svm.createInt(8, 'z'); + assert(type(int256).min <= x && x <= type(int256).max); + assert(type(int160).min <= y && y <= type(int160).max); + assert(type(int8).min <= z && z <= type(int8).max); + } + function check_createBytes() public { bytes memory data = svm.createBytes(2, 'data'); uint x = uint(uint8(data[0])); @@ -21,11 +30,21 @@ contract HalmosCheatCodeTest is SymTest { assert(0 <= y && y <= type(uint8).max); } + function check_createString() public { + string memory data = svm.createString(5, 'str'); + assert(bytes(data).length == 5); + } + function check_createUint256() public { uint x = svm.createUint256('x'); assert(0 <= x && x <= type(uint256).max); } + function check_createInt256() public { + int x = svm.createInt256('x'); + assert(type(int256).min <= x && x <= type(int256).max); + } + function check_createBytes32() public { bytes32 x = svm.createBytes32('x'); assert(0 <= uint(x) && uint(x) <= type(uint256).max); @@ -33,6 +52,14 @@ contract HalmosCheatCodeTest is SymTest { assert(0 <= y && y <= type(uint256).max); } + function check_createBytes4() public { + bytes4 x = svm.createBytes4('x'); + uint256 x_uint = uint256(uint32(x)); + assert(0 <= x_uint && x_uint <= type(uint32).max); + uint y; assembly { y := x } + assert(0 <= y && y <= type(uint256).max); + } + function check_createAddress() public { address x = svm.createAddress('x'); uint y; assembly { y := x } From 5b3c56f452238c2bab03d8444e7e54e9b91b46bd Mon Sep 17 00:00:00 2001 From: karmacoma Date: Fri, 20 Oct 2023 15:08:20 -0700 Subject: [PATCH 8/9] staticmethod fix for python < 3.10 + factor our console.py out of cheatcodes.py + catch and log exceptions in stringify and console.log --- src/halmos/cheatcodes.py | 262 ++++++++++----------------------------- src/halmos/console.py | 111 +++++++++++++++++ src/halmos/sevm.py | 3 +- src/halmos/utils.py | 56 ++++++--- 4 files changed, 222 insertions(+), 210 deletions(-) create mode 100644 src/halmos/console.py diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index 5cd5f024..15bafa1e 100644 --- a/src/halmos/cheatcodes.py +++ b/src/halmos/cheatcodes.py @@ -20,28 +20,6 @@ def name_of(x: str) -> str: return re.sub(r"\s+", "_", x) -def extract_bytes_argument(calldata: BitVecRef, arg_idx: int) -> bytes: - """Extracts idx-th argument of string from calldata""" - offset = int_of( - extract_bytes(calldata, 4 + arg_idx * 32, 32), - "symbolic offset for bytes argument", - ) - length = int_of( - extract_bytes(calldata, 4 + offset, 32), - "symbolic size for bytes argument", - ) - if length == 0: - return b"" - - return bv_value_to_bytes(extract_bytes(calldata, 4 + offset + 32, length)) - - -def extract_string_argument(calldata: BitVecRef, arg_idx: int): - """Extracts idx-th argument of string from calldata""" - string_bytes = extract_bytes_argument(calldata, arg_idx) - return string_bytes.decode("utf-8") if string_bytes else "" - - def extract_string_array_argument(calldata: BitVecRef, arg_idx: int): """Extracts idx-th argument of string array from calldata""" @@ -144,89 +122,85 @@ def stopPrank(self) -> bool: return True -class halmos_cheat_code: - # address constant SVM_ADDRESS = - # address(bytes20(uint160(uint256(keccak256('svm cheat code'))))); - address: BitVecRef = con_addr(0xF3993A62377BCD56AE39D773740A5390411E8BC9) +def create_generic(ex, bits: int, var_name: str, type_name: str) -> BitVecRef: + label = f"halmos_{var_name}_{type_name}_{ex.new_symbol_id():>02}" + return BitVec(label, BitVecSorts[bits]) - @staticmethod - def create_generic(ex, bits: int, var_name: str, type_name: str) -> BitVecRef: - label = f"halmos_{var_name}_{type_name}_{ex.new_symbol_id():>02}" - return BitVec(label, BitVecSorts[bits]) - @staticmethod - def create_uint(ex, arg): - bits = int_of( - extract_bytes(arg, 4, 32), "symbolic bit size for halmos.createUint()" - ) - if bits > 256: - raise HalmosException(f"bitsize larger than 256: {bits}") +def create_uint(ex, arg): + bits = int_of( + extract_bytes(arg, 4, 32), "symbolic bit size for halmos.createUint()" + ) + if bits > 256: + raise HalmosException(f"bitsize larger than 256: {bits}") - name = name_of(extract_string_argument(arg, 1)) - return uint256(halmos_cheat_code.create_generic(ex, bits, name, f"uint{bits}")) + name = name_of(extract_string_argument(arg, 1)) + return uint256(create_generic(ex, bits, name, f"uint{bits}")) - @staticmethod - def create_uint256(ex, arg): - name = name_of(extract_string_argument(arg, 0)) - return halmos_cheat_code.create_generic(ex, 256, name, "uint256") - @staticmethod - def create_int(ex, arg): - bits = int_of( - extract_bytes(arg, 4, 32), "symbolic bit size for halmos.createUint()" - ) - if bits > 256: - raise HalmosException(f"bitsize larger than 256: {bits}") +def create_uint256(ex, arg): + name = name_of(extract_string_argument(arg, 0)) + return create_generic(ex, 256, name, "uint256") - name = name_of(extract_string_argument(arg, 1)) - return int256(halmos_cheat_code.create_generic(ex, bits, name, f"int{bits}")) - @staticmethod - def create_int256(ex, arg): - name = name_of(extract_string_argument(arg, 0)) - return halmos_cheat_code.create_generic(ex, 256, name, "int256") +def create_int(ex, arg): + bits = int_of( + extract_bytes(arg, 4, 32), "symbolic bit size for halmos.createUint()" + ) + if bits > 256: + raise HalmosException(f"bitsize larger than 256: {bits}") - @staticmethod - def create_bytes(ex, arg): - byte_size = int_of( - extract_bytes(arg, 4, 32), "symbolic byte size for halmos.createBytes()" - ) - name = name_of(extract_string_argument(arg, 1)) - symbolic_bytes = halmos_cheat_code.create_generic( - ex, byte_size * 8, name, "bytes" - ) - return Concat(con(32), con(byte_size), symbolic_bytes) + name = name_of(extract_string_argument(arg, 1)) + return int256(create_generic(ex, bits, name, f"int{bits}")) - @staticmethod - def create_string(ex, arg): - byte_size = int_of( - extract_bytes(arg, 4, 32), "symbolic byte size for halmos.createString()" - ) - name = name_of(extract_string_argument(arg, 1)) - symbolic_string = halmos_cheat_code.create_generic( - ex, byte_size * 8, name, "string" - ) - return Concat(con(32), con(byte_size), symbolic_string) - @staticmethod - def create_bytes4(ex, arg): - name = name_of(extract_string_argument(arg, 0)) - return uint256(halmos_cheat_code.create_generic(ex, 32, name, "bytes4")) +def create_int256(ex, arg): + name = name_of(extract_string_argument(arg, 0)) + return create_generic(ex, 256, name, "int256") - @staticmethod - def create_bytes32(ex, arg): - name = name_of(extract_string_argument(arg, 0)) - return halmos_cheat_code.create_generic(ex, 256, name, "bytes32") - @staticmethod - def create_address(ex, arg): - name = name_of(extract_string_argument(arg, 0)) - return uint256(halmos_cheat_code.create_generic(ex, 160, name, "address")) +def create_bytes(ex, arg): + byte_size = int_of( + extract_bytes(arg, 4, 32), "symbolic byte size for halmos.createBytes()" + ) + name = name_of(extract_string_argument(arg, 1)) + symbolic_bytes = create_generic(ex, byte_size * 8, name, "bytes") + return Concat(con(32), con(byte_size), symbolic_bytes) + + +def create_string(ex, arg): + byte_size = int_of( + extract_bytes(arg, 4, 32), "symbolic byte size for halmos.createString()" + ) + name = name_of(extract_string_argument(arg, 1)) + symbolic_string = create_generic(ex, byte_size * 8, name, "string") + return Concat(con(32), con(byte_size), symbolic_string) + + +def create_bytes4(ex, arg): + name = name_of(extract_string_argument(arg, 0)) + return uint256(create_generic(ex, 32, name, "bytes4")) + + +def create_bytes32(ex, arg): + name = name_of(extract_string_argument(arg, 0)) + return create_generic(ex, 256, name, "bytes32") + + +def create_address(ex, arg): + name = name_of(extract_string_argument(arg, 0)) + return uint256(create_generic(ex, 160, name, "address")) + + +def create_bool(ex, arg): + name = name_of(extract_string_argument(arg, 0)) + return uint256(create_generic(ex, 1, name, "bool")) - @staticmethod - def create_bool(ex, arg): - name = name_of(extract_string_argument(arg, 0)) - return uint256(halmos_cheat_code.create_generic(ex, 1, name, "bool")) + +class halmos_cheat_code: + # address constant SVM_ADDRESS = + # address(bytes20(uint160(uint256(keccak256('svm cheat code'))))); + address: BitVecRef = con_addr(0xF3993A62377BCD56AE39D773740A5390411E8BC9) handlers = { 0x66830DFA: create_uint, # createUint(uint256,string) @@ -242,7 +216,7 @@ def create_bool(ex, arg): } @staticmethod - def handle(ex, arg: BitVec) -> BitVec: + def handle(ex, arg: BitVecRef) -> BitVecRef: funsig = int_of(extract_funsig(arg), "symbolic halmos cheatcode") if handler := halmos_cheat_code.handlers.get(funsig): return handler(ex, arg) @@ -475,105 +449,3 @@ def handle(sevm, ex, arg: BitVec) -> BitVec: # TODO: support other cheat codes msg = f"Unsupported cheat code: calldata = {hexify(arg)}" raise HalmosException(msg) - - -class console: - # see forge-std/console2.sol - address: BitVecRef = con_addr(0x000000000000000000636F6E736F6C652E6C6F67) - - @staticmethod - def log_uint256(arg: BitVec) -> None: - b = extract_bytes(arg, 4, 32) - console.log(render_uint(b)) - - @staticmethod - def log_string(arg: BitVec) -> None: - str_val = extract_string_argument(arg, 0) - console.log(str_val) - - @staticmethod - def log_bytes(arg: BitVec) -> None: - b = extract_bytes_argument(arg, 0) - console.log(render_bytes(b)) - - @staticmethod - def log_string_address(arg: BitVec) -> None: - str_val = extract_string_argument(arg, 0) - addr = extract_bytes(arg, 36, 32) - console.log(f"{str_val} {render_address(addr)}") - - @staticmethod - def log_address(arg: BitVec) -> None: - addr = extract_bytes(arg, 4, 32) - console.log(render_address(addr)) - - @staticmethod - def log_string_bool(arg: BitVec) -> None: - str_val = extract_string_argument(arg, 0) - bool_val = extract_bytes(arg, 36, 32) - console.log(f"{str_val} {render_bool(bool_val)}") - - @staticmethod - def log_bool(arg: BitVec) -> None: - bool_val = extract_bytes(arg, 4, 32) - console.log(render_bool(bool_val)) - - @staticmethod - def log_string_string(arg: BitVec) -> None: - str1_val = extract_string_argument(arg, 0) - str2_val = extract_string_argument(arg, 1) - console.log(f"{str1_val} {str2_val}") - - @staticmethod - def log_bytes32(arg: BitVec) -> None: - b = extract_bytes(arg, 4, 32) - console.log(hexify(b)) - - @staticmethod - def log_string_int256(arg: BitVec) -> None: - str_val = extract_string_argument(arg, 0) - int_val = extract_bytes(arg, 36, 32) - console.log(f"{str_val} {render_int(int_val)}") - - @staticmethod - def log_int256(arg: BitVec) -> None: - int_val = extract_bytes(arg, 4, 32) - console.log(render_int(int_val)) - - @staticmethod - def log_string_uint256(arg: BitVec) -> None: - str_val = extract_string_argument(arg, 0) - uint_val = extract_bytes(arg, 36, 32) - console.log(f"{str_val} {render_uint(uint_val)}") - - @staticmethod - def log(what: str) -> None: - print(f"console.log: {magenta(what)}") - - handlers = { - 0xF82C50F1: log_uint256, - 0xF5B1BBA9: log_uint256, # alias for 'log(uint)' - 0x41304FAC: log_string, - 0x0BE77F56: log_bytes, - 0x319AF333: log_string_address, - 0x2C2ECBC2: log_address, - 0xC3B55635: log_string_bool, - 0x32458EED: log_bool, - 0x4B5C4277: log_string_string, - 0x27B7CF85: log_bytes32, - 0x3CA6268E: log_string_int256, - 0x2D5B6CB9: log_int256, - 0xB60E72CC: log_string_uint256, - } - - @staticmethod - def handle(ex, arg: BitVec) -> None: - funsig: int = int_of(extract_funsig(arg), "symbolic console function selector") - - if handler := console.handlers.get(funsig): - return handler(arg) - - info( - f"Unsupported console function: selector = 0x{funsig:0>8x}, " - f"calldata = {hexify(arg)}" - ) diff --git a/src/halmos/console.py b/src/halmos/console.py new file mode 100644 index 00000000..cf43bb3c --- /dev/null +++ b/src/halmos/console.py @@ -0,0 +1,111 @@ +from z3 import BitVecRef + +from .utils import * + + +def log_uint256(arg: BitVec) -> None: + b = extract_bytes(arg, 4, 32) + console.log(render_uint(b)) + + +def log_string(arg: BitVec) -> None: + str_val = extract_string_argument(arg, 0) + console.log(str_val) + + +def log_bytes(arg: BitVec) -> None: + b = extract_bytes_argument(arg, 0) + console.log(render_bytes(b)) + + +def log_string_address(arg: BitVec) -> None: + str_val = extract_string_argument(arg, 0) + addr = extract_bytes(arg, 36, 32) + console.log(f"{str_val} {render_address(addr)}") + + +def log_address(arg: BitVec) -> None: + addr = extract_bytes(arg, 4, 32) + console.log(render_address(addr)) + + +def log_string_bool(arg: BitVec) -> None: + str_val = extract_string_argument(arg, 0) + bool_val = extract_bytes(arg, 36, 32) + console.log(f"{str_val} {render_bool(bool_val)}") + + +def log_bool(arg: BitVec) -> None: + bool_val = extract_bytes(arg, 4, 32) + console.log(render_bool(bool_val)) + + +def log_string_string(arg: BitVec) -> None: + str1_val = extract_string_argument(arg, 0) + str2_val = extract_string_argument(arg, 1) + console.log(f"{str1_val} {str2_val}") + + +def log_bytes32(arg: BitVec) -> None: + b = extract_bytes(arg, 4, 32) + console.log(hexify(b)) + + +def log_string_int256(arg: BitVec) -> None: + str_val = extract_string_argument(arg, 0) + int_val = extract_bytes(arg, 36, 32) + console.log(f"{str_val} {render_int(int_val)}") + + +def log_int256(arg: BitVec) -> None: + int_val = extract_bytes(arg, 4, 32) + console.log(render_int(int_val)) + + +def log_string_uint256(arg: BitVec) -> None: + str_val = extract_string_argument(arg, 0) + uint_val = extract_bytes(arg, 36, 32) + console.log(f"{str_val} {render_uint(uint_val)}") + + +class console: + # see forge-std/console2.sol + address: BitVecRef = con_addr(0x000000000000000000636F6E736F6C652E6C6F67) + + handlers = { + 0xF82C50F1: log_uint256, + 0xF5B1BBA9: log_uint256, # alias for 'log(uint)' + 0x41304FAC: log_string, + 0x0BE77F56: log_bytes, + 0x319AF333: log_string_address, + 0x2C2ECBC2: log_address, + 0xC3B55635: log_string_bool, + 0x32458EED: log_bool, + 0x4B5C4277: log_string_string, + 0x27B7CF85: log_bytes32, + 0x3CA6268E: log_string_int256, + 0x2D5B6CB9: log_int256, + 0xB60E72CC: log_string_uint256, + } + + @staticmethod + def log(what: str) -> None: + print(f"[console.log] {magenta(what)}") + + @staticmethod + def handle(ex, arg: BitVec) -> None: + try: + funsig: int = int_of( + extract_funsig(arg), "symbolic console function selector" + ) + + if handler := console.handlers.get(funsig): + return handler(arg) + + info( + f"Unsupported console function: selector = 0x{funsig:0>8x}, " + f"calldata = {hexify(arg)}" + ) + except Exception as e: + # we don't want to fail execution because of an issue during console.log + warn(f"console.handle: {repr(e)}") diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index ee87f115..a00b76a8 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -22,7 +22,8 @@ ) from z3 import * -from .cheatcodes import halmos_cheat_code, hevm_cheat_code, console, Prank +from .cheatcodes import halmos_cheat_code, hevm_cheat_code, Prank +from .console import console from .exceptions import * from .utils import * from .warnings import ( diff --git a/src/halmos/utils.py b/src/halmos/utils.py index c6832010..f6e79cf5 100644 --- a/src/halmos/utils.py +++ b/src/halmos/utils.py @@ -135,6 +135,28 @@ def create_solver(logic="QF_AUFBV", ctx=None, timeout=0, max_memory=0): return solver +def extract_bytes_argument(calldata: BitVecRef, arg_idx: int) -> bytes: + """Extracts idx-th argument of string from calldata""" + offset = int_of( + extract_bytes(calldata, 4 + arg_idx * 32, 32), + "symbolic offset for bytes argument", + ) + length = int_of( + extract_bytes(calldata, 4 + offset, 32), + "symbolic size for bytes argument", + ) + if length == 0: + return b"" + + return bv_value_to_bytes(extract_bytes(calldata, 4 + offset + 32, length)) + + +def extract_string_argument(calldata: BitVecRef, arg_idx: int): + """Extracts idx-th argument of string from calldata""" + string_bytes = extract_bytes_argument(calldata, arg_idx) + return string_bytes.decode("utf-8") if string_bytes else "" + + def extract_bytes(data: BitVecRef, byte_offset: int, size_bytes: int) -> BitVecRef: """Extract bytes from calldata. Zero-pad if out of bounds.""" n = data.size() @@ -258,11 +280,12 @@ def stringify(symbol_name: str, val: Any): """ if not is_bv_value(val): warn(f"{val} is not a bitvector value") - return str(val) + return hexify(val) tokens = symbol_name.split("_") if len(tokens) < 3: warn(f"Failed to infer type for symbol '{symbol_name}'") + return hexify(val) if len(tokens) >= 4 and tokens[-1].isdigit(): # we may have something like p_val_bytes_01 @@ -271,19 +294,24 @@ def stringify(symbol_name: str, val: Any): type_name = tokens[-1] - if type_name.startswith("uint"): - return render_uint(val) - elif type_name.startswith("int"): - return render_int(val) - elif type_name == "bool": - return render_bool(val) - elif type_name == "string": - return render_string(val) - elif type_name == "bytes": - return render_bytes(val) - elif type_name == "address": - return render_address(val) - else: # bytes32, bytes4, structs, etc. + try: + if type_name.startswith("uint"): + return render_uint(val) + elif type_name.startswith("int"): + return render_int(val) + elif type_name == "bool": + return render_bool(val) + elif type_name == "string": + return render_string(val) + elif type_name == "bytes": + return render_bytes(val) + elif type_name == "address": + return render_address(val) + else: # bytes32, bytes4, structs, etc. + return hexify(val) + except Exception as e: + # log error and move on + warn(f"Failed to stringify {val} of type {type_name}: {repr(e)}") return hexify(val) From 8b5b151632ddc935a995d3e90126d11cc40b7a17 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Fri, 20 Oct 2023 15:44:04 -0700 Subject: [PATCH 9/9] add test for console.log with undecode string --- src/halmos/console.py | 2 +- tests/expected/all.json | 9 +++++++++ tests/regression/test/Console.t.sol | 6 ++++++ 3 files changed, 16 insertions(+), 1 deletion(-) diff --git a/src/halmos/console.py b/src/halmos/console.py index cf43bb3c..1fa0ed27 100644 --- a/src/halmos/console.py +++ b/src/halmos/console.py @@ -108,4 +108,4 @@ def handle(ex, arg: BitVec) -> None: ) except Exception as e: # we don't want to fail execution because of an issue during console.log - warn(f"console.handle: {repr(e)}") + warn(f"console.handle: {repr(e)} with arg={hexify(arg)}") diff --git a/tests/expected/all.json b/tests/expected/all.json index e1d99045..4e09cdef 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -335,6 +335,15 @@ "time": null, "num_bounded_loops": null }, + { + "name": "check_log_undecodable_string()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, { "name": "check_log_unsupported()", "exitcode": 0, diff --git a/tests/regression/test/Console.t.sol b/tests/regression/test/Console.t.sol index 96d6bd85..35002b78 100644 --- a/tests/regression/test/Console.t.sol +++ b/tests/regression/test/Console.t.sol @@ -70,6 +70,12 @@ contract ConsoleTest is Test { console2.log(empty); } + function check_log_undecodable_string() public view { + bytes memory badBytes = hex"ff"; + string memory bad = string(badBytes); + console2.log("this is a string that won't decode to utf-8:", bad); + } + function check_log_unsupported() public { console2._sendLogPayload(abi.encodeWithSignature("doesNotExist()")); }