From dd6a92aa7cd8c29801ac17efc68e9f516228ed42 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Fri, 23 Jun 2023 22:17:22 -0700 Subject: [PATCH] feat: add symbol naming support (#113) --- src/halmos/cheatcodes.py | 24 ++++++------ src/halmos/sevm.py | 63 +++++++++++++++++++++----------- tests/test/HalmosCheatCode.t.sol | 36 +++++++++++------- 3 files changed, 75 insertions(+), 48 deletions(-) diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index 0e45197b..1497dbcb 100644 --- a/src/halmos/cheatcodes.py +++ b/src/halmos/cheatcodes.py @@ -59,23 +59,23 @@ class halmos_cheat_code: # address(bytes20(uint160(uint256(keccak256('svm cheat code'))))); address: BitVecRef = con_addr(0xf3993a62377bcd56ae39d773740a5390411e8bc9) - # bytes4(keccak256("createUint(uint256)")) - create_symbolic_uint: int = 0xd90c7c38 + # bytes4(keccak256("createUint(uint256,string)")) + create_uint: int = 0x66830dfa - # bytes4(keccak256("createBytes(uint256)")) - create_symbolic_bytes: int = 0x57f9200b + # bytes4(keccak256("createBytes(uint256,string)")) + create_bytes: int = 0xeef5311d - # bytes4(keccak256("createUint256()")) - create_symbolic_uint256: int = 0xbabe11c4 + # bytes4(keccak256("createUint256(string)")) + create_uint256: int = 0xbc7beefc - # bytes4(keccak256("createBytes32()")) - create_symbolic_bytes32: int = 0x27c045e3 + # bytes4(keccak256("createBytes32(string)")) + create_bytes32: int = 0xbf72fa66 - # bytes4(keccak256("createAddress()")) - create_symbolic_address: int = 0xc7f40b64 + # bytes4(keccak256("createAddress(string)")) + create_address: int = 0x3b0fa01b - # bytes4(keccak256("createBool()")) - create_symbolic_bool: int = 0x57b40092 + # bytes4(keccak256("createBool(string)")) + create_bool: int = 0x6e0bb659 class hevm_cheat_code: # https://github.com/dapphub/ds-test/blob/cd98eff28324bfac652e63a239a60632a761790b/src/test.sol diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 7e89cc73..4f01404f 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -47,6 +47,9 @@ def id_str(x: Any) -> str: return hexify(x).replace(' ', '') +def name_of(x: str) -> str: + return re.sub(r'\s+', '_', x) + class Instruction: pc: int opcode: int @@ -278,6 +281,16 @@ def extract_funsig(calldata: BitVecRef): 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') + + class State: stack: List[Word] memory: List[Byte] @@ -1156,37 +1169,43 @@ def call_unknown() -> None: funsig: int = int_of(extract_funsig(arg), 'symbolic halmos cheatcode function selector') - # createSymbolicUint(uint256) returns (uint256) - if funsig == halmos_cheat_code.create_symbolic_uint: - bit_size = int_of(simplify(extract_bytes(arg, 4, 32)), 'symbolic bit size for halmos.createSymbolicUint()') + # 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()') + label = name_of(extract_string_argument(arg, 1)) if bit_size <= 256: - ret = uint256(BitVec(f'halmos_symbolic_uint{bit_size}_{ex.new_symbol_id():>02}', bit_size)) + ret = uint256(BitVec(f'halmos_{label}_uint{bit_size}_{ex.new_symbol_id():>02}', bit_size)) else: ex.error = f'bitsize larger than 256: {bit_size}' out.append(ex) return - # createSymbolicBytes(uint256) returns (bytes) - elif funsig == halmos_cheat_code.create_symbolic_bytes: - byte_size = int_of(simplify(extract_bytes(arg, 4, 32)), 'symbolic byte size for halmos.createSymbolicBytes()') - symbolic_bytes = BitVec(f'halmos_symbolic_bytes_{ex.new_symbol_id():>02}', byte_size * 8) + # 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()') + label = name_of(extract_string_argument(arg, 1)) + symbolic_bytes = BitVec(f'halmos_{label}_bytes_{ex.new_symbol_id():>02}', byte_size * 8) ret = Concat(BitVecVal(32, 256), BitVecVal(byte_size, 256), symbolic_bytes) - # createSymbolicUint256() returns (uint256) - elif funsig == halmos_cheat_code.create_symbolic_uint256: - ret = BitVec(f'halmos_symbolic_uint256_{ex.new_symbol_id():>02}', 256) + # createUint256(string) returns (uint256) + elif funsig == halmos_cheat_code.create_uint256: + label = name_of(extract_string_argument(arg, 0)) + ret = BitVec(f'halmos_{label}_uint256_{ex.new_symbol_id():>02}', 256) - # createSymbolicBytes32() returns (bytes32) - elif funsig == halmos_cheat_code.create_symbolic_bytes32: - ret = BitVec(f'halmos_symbolic_bytes32_{ex.new_symbol_id():>02}', 256) + # createBytes32(string) returns (bytes32) + elif funsig == halmos_cheat_code.create_bytes32: + label = name_of(extract_string_argument(arg, 0)) + ret = BitVec(f'halmos_{label}_bytes32_{ex.new_symbol_id():>02}', 256) - # createSymbolicAddress() returns (address) - elif funsig == halmos_cheat_code.create_symbolic_address: - ret = uint256(BitVec(f'halmos_symbolic_address_{ex.new_symbol_id():>02}', 160)) + # createAddress(string) returns (address) + elif funsig == halmos_cheat_code.create_address: + label = name_of(extract_string_argument(arg, 0)) + ret = uint256(BitVec(f'halmos_{label}_address_{ex.new_symbol_id():>02}', 160)) - # createSymbolicBool() returns (bool) - elif funsig == halmos_cheat_code.create_symbolic_bool: - ret = uint256(BitVec(f'halmos_symbolic_bool_{ex.new_symbol_id():>02}', 1)) + # createBool(string) returns (bool) + elif funsig == halmos_cheat_code.create_bool: + label = name_of(extract_string_argument(arg, 0)) + ret = uint256(BitVec(f'halmos_{label}_bool_{ex.new_symbol_id():>02}', 1)) else: ex.error = f'Unknown halmos cheat code: function selector = 0x{funsig:0>8x}, calldata = {hexify(arg)}' @@ -1300,7 +1319,7 @@ def call_unknown() -> None: ex.block.timestamp = simplify(Extract(255, 0, arg)) # vm.etch(address,bytes) elif extract_funsig(arg) == hevm_cheat_code.etch_sig: - who = simplify(extract_bytes(arg, 4 + 12, 20)) + who = extract_bytes(arg, 4 + 12, 20) # who must be concrete if not is_bv_value(who): @@ -1334,7 +1353,7 @@ def call_unknown() -> None: funsig: int = int_of(extract_funsig(arg), 'symbolic console function selector') if funsig == console.log_uint: - print(simplify(extract_bytes(arg, 4, 32))) + print(extract_bytes(arg, 4, 32)) # elif funsig == console.log_string: diff --git a/tests/test/HalmosCheatCode.t.sol b/tests/test/HalmosCheatCode.t.sol index 36e2ef5b..41993945 100644 --- a/tests/test/HalmosCheatCode.t.sol +++ b/tests/test/HalmosCheatCode.t.sol @@ -3,22 +3,22 @@ pragma solidity >=0.8.0 <0.9.0; interface SVM { // Create a new symbolic uint value ranging over [0, 2**bitSize - 1] (inclusive) - function createUint(uint256 bitSize) external returns (uint256 value); + function createUint(uint256 bitSize, string memory name) external returns (uint256 value); // Create a new symbolic byte array with the given byte size - function createBytes(uint256 byteSize) external returns (bytes memory value); + function createBytes(uint256 byteSize, string memory name) external returns (bytes memory value); // Create a new symbolic uint256 value - function createUint256() external returns (uint256 value); + function createUint256(string memory name) external returns (uint256 value); // Create a new symbolic bytes32 value - function createBytes32() external returns (bytes32 value); + function createBytes32(string memory name) external returns (bytes32 value); // Create a new symbolic address value - function createAddress() external returns (address value); + function createAddress(string memory name) external returns (address value); // Create a new symbolic boolean value - function createBool() external returns (bool value); + function createBool(string memory name) external returns (bool value); } abstract contract SymTest { @@ -30,16 +30,16 @@ abstract contract SymTest { contract HalmosCheatCodeTest is SymTest { function testSymbolicUint() public { - uint x = svm.createUint(256); - uint y = svm.createUint(160); - uint z = svm.createUint(8); + uint x = svm.createUint(256, 'x'); + uint y = svm.createUint(160, 'y'); + uint z = svm.createUint(8, 'z'); assert(0 <= x && x <= type(uint256).max); assert(0 <= y && y <= type(uint160).max); assert(0 <= z && z <= type(uint8).max); } function testSymbolicBytes() public { - bytes memory data = svm.createBytes(2); + bytes memory data = svm.createBytes(2, 'data'); uint x = uint(uint8(data[0])); uint y = uint(uint8(data[1])); assert(0 <= x && x <= type(uint8).max); @@ -47,26 +47,34 @@ contract HalmosCheatCodeTest is SymTest { } function testSymbolicUint256() public { - uint x = svm.createUint256(); + uint x = svm.createUint256('x'); assert(0 <= x && x <= type(uint256).max); } function testSymbolicBytes32() public { - bytes32 x = svm.createBytes32(); + bytes32 x = svm.createBytes32('x'); assert(0 <= uint(x) && uint(x) <= type(uint256).max); uint y; assembly { y := x } assert(0 <= y && y <= type(uint256).max); } function testSymbolicAddress() public { - address x = svm.createAddress(); + address x = svm.createAddress('x'); uint y; assembly { y := x } assert(0 <= y && y <= type(uint160).max); } function testSymbolicBool() public { - bool x = svm.createBool(); + bool x = svm.createBool('x'); uint y; assembly { y := x } assert(y == 0 || y == 1); } + + function testSymbolLabel() public returns (uint256) { + uint x = svm.createUint256(''); + uint y = svm.createUint256(' '); + uint z = svm.createUint256(' a '); + uint w = svm.createUint256(' a b '); + return x + y + z + w; + } }