Skip to content

Commit

Permalink
feat: add symbol naming support (#113)
Browse files Browse the repository at this point in the history
  • Loading branch information
@daejunpark
daejunpark committed Jun 24, 2023
1 parent c1dc9ff commit dd6a92a
Show file tree
Hide file tree
Showing 3 changed files with 75 additions and 48 deletions.
24 changes: 12 additions & 12 deletions src/halmos/cheatcodes.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
63 changes: 41 additions & 22 deletions src/halmos/sevm.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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]
Expand Down Expand Up @@ -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)}'
Expand Down Expand Up @@ -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):
Expand Down Expand Up @@ -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:

Expand Down
36 changes: 22 additions & 14 deletions tests/test/HalmosCheatCode.t.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -30,43 +30,51 @@ 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);
assert(0 <= y && y <= type(uint8).max);
}

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;
}
}

0 comments on commit dd6a92a

Please sign in to comment.