From 74068648333448ad98271a8c54bee84c5bdaefa0 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Fri, 21 Feb 2025 14:56:05 -0800 Subject: [PATCH] more fixes --- src/halmos/__main__.py | 18 ++++--- src/halmos/bitvec.py | 107 +++++++++++++++++++++++++---------------- src/halmos/sevm.py | 41 +++++++--------- src/halmos/utils.py | 7 ++- 4 files changed, 99 insertions(+), 74 deletions(-) diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index 4bfab81f..3913f25f 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -834,17 +834,18 @@ def run_contract(ctx: ContractContext) -> list[TestResult]: def contract_regex(args): - if args.contract: - return f"^{args.contract}$" + if contract := args.contract: + return f"^{contract}$" else: return args.match_contract def test_regex(args): - if args.match_test.startswith("^"): - return args.match_test + match_test = args.match_test + if match_test.startswith("^"): + return match_test else: - return f"^{args.function}.*{args.match_test}" + return f"^{args.function}.*{match_test}" @dataclass(frozen=True) @@ -957,8 +958,11 @@ def on_signal(signum, frame): # run # + _contract_regex = contract_regex(args) + _test_regex = test_regex(args) + for build_out_map, filename, contract_name in build_output_iterator(build_out): - if not re.search(contract_regex(args), contract_name): + if not re.search(_contract_regex, contract_name): continue (contract_json, contract_type, natspec) = build_out_map[filename][contract_name] @@ -966,7 +970,7 @@ def on_signal(signum, frame): continue methodIdentifiers = contract_json["methodIdentifiers"] - funsigs = [f for f in methodIdentifiers if re.search(test_regex(args), f)] + funsigs = [f for f in methodIdentifiers if re.search(_test_regex, f)] num_found = len(funsigs) if num_found == 0: diff --git a/src/halmos/bitvec.py b/src/halmos/bitvec.py index 146c1e82..e6bacd15 100644 --- a/src/halmos/bitvec.py +++ b/src/halmos/bitvec.py @@ -1,6 +1,7 @@ from typing import TypeAlias from z3 import ( + ULT, And, BitVecRef, BitVecVal, @@ -33,6 +34,14 @@ def is_power_of_two(x: int) -> bool: return x > 0 and not (x & (x - 1)) +def to_signed(x: int, bit_size: int) -> int: + """ + Interpret x (masked to bit_size bits) as a signed integer in two's complement. + """ + sign_bit = 1 << (bit_size - 1) + return x - (1 << bit_size) if (x & sign_bit) else x + + def as_int(value: AnyValue) -> tuple[BVValue, MaybeSize]: if isinstance(value, int): return value, None @@ -52,6 +61,7 @@ def as_int(value: AnyValue) -> tuple[BVValue, MaybeSize]: raise TypeError(f"Cannot convert {type(value)} to int") +# TODO: HalmosBool.TRUE, HalmosBool.FALSE class HalmosBool: """ Immutable wrapper for concrete or symbolic boolean values. @@ -129,6 +139,14 @@ def is_concrete(self) -> bool: def value(self) -> AnyBool: return self._value + @property + def is_true(self) -> bool: + return self.is_concrete and self._value + + @property + def is_false(self) -> bool: + return self.is_concrete and not self._value + def is_zero(self) -> "HalmosBool": return self @@ -142,33 +160,24 @@ def neg(self) -> "HalmosBool": else HalmosBool(not self._value) ) - def __and__(self, other: AnyValue) -> "HalmosBool": - return ( - HalmosBool(And(self._value, other)) - if self._symbolic - else HalmosBool(self._value and other) - ) + def eq(self, other: "HalmosBool") -> "HalmosBool": + return HalmosBool(self._value == other._value) - def __rand__(self, other: AnyValue) -> "HalmosBool": - return ( - HalmosBool(And(other, self._value)) - if self._symbolic - else HalmosBool(other and self._value) - ) + def __and__(self, other: "HalmosBool") -> "HalmosBool": + if self.is_true and other.is_true: + return HalmosBool(True) + elif self.is_false or other.is_false: + return HalmosBool(False) + else: + return HalmosBool(And(self.wrapped(), other.wrapped())) def __or__(self, other: AnyValue) -> "HalmosBool": - return ( - HalmosBool(Or(self._value, other)) - if self._symbolic - else HalmosBool(self._value or other) - ) - - def __ror__(self, other: AnyValue) -> "HalmosBool": - return ( - HalmosBool(Or(other, self._value)) - if self._symbolic - else HalmosBool(other or self._value) - ) + if self.is_true or other.is_true: + return HalmosBool(True) + elif self.is_false and other.is_false: + return HalmosBool(False) + else: + return HalmosBool(Or(self.wrapped(), other.wrapped())) def as_bv(self, size: int = 1) -> BV: if self._symbolic: @@ -293,7 +302,11 @@ def __int__(self) -> int: return self._value def __repr__(self) -> str: - return f"HalmosBitVec({self._value}, {self._size})" + return ( + f"HalmosBitVec({self._value}, {self._size})" + if self._size != 256 + else f"{self._value}" + ) def __str__(self) -> str: return str(self._value) @@ -508,9 +521,7 @@ def __rmod__(self, other: AnyValue) -> "HalmosBitVec": # Shifts def __lshift__(self, shift: AnyValue) -> "HalmosBitVec": """ - Logical left shift by shift bits. - Python's << does this for ints, - for symbolic you might do self._value << shift. + Logical left shift """ size = self._size @@ -564,18 +575,6 @@ def __invert__(self) -> BV: # TODO: handle concrete case return HalmosBitVec(~self.wrapped(), size=self.size) - def __lt__(self, other: BV) -> HalmosBool: - return self.ult(other) - - def __gt__(self, other: BV) -> HalmosBool: - return self.ugt(other) - - def __le__(self, other: BV) -> HalmosBool: - return self.ule(other) - - def __ge__(self, other: BV) -> HalmosBool: - return self.uge(other) - def __eq__(self, other: BV) -> bool: if self.is_symbolic and other.is_symbolic: return self.size == other.size and eq(self.value, other.value) @@ -587,7 +586,21 @@ def __eq__(self, other: BV) -> bool: def ult(self, other: BV) -> HalmosBool: assert self._size == other._size - return HalmosBool(self._value < other._value) + + if self.is_concrete and other.is_concrete: + return HalmosBool(self.value < other.value) + + return HalmosBool(ULT(self.wrapped(), other.wrapped())) + + def slt(self, other: BV) -> HalmosBool: + assert self._size == other._size + + if self.is_concrete and other.is_concrete: + left = to_signed(self._value, self._size) + right = to_signed(other._value, other._size) + return HalmosBool(left < right) + + return HalmosBool(self.wrapped() < other.wrapped()) def ugt(self, other: BV) -> HalmosBool: assert self._size == other._size @@ -604,3 +617,15 @@ def uge(self, other: BV) -> HalmosBool: def eq(self, other: BV) -> HalmosBool: assert self._size == other._size return HalmosBool(self._value == other._value) + + def __and__(self, other: BV) -> BV: + assert self._size == other._size + return HalmosBitVec(self._value & other._value, size=self._size) + + def __or__(self, other: BV) -> BV: + assert self._size == other._size + return HalmosBitVec(self._value | other._value, size=self._size) + + def __xor__(self, other: BV) -> BV: + assert self._size == other._size + return HalmosBitVec(self._value ^ other._value, size=self._size) diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 54beb682..d294154b 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -22,7 +22,6 @@ from rich.status import Status from z3 import ( UGE, - UGT, ULE, ULT, And, @@ -38,13 +37,11 @@ Extract, Function, If, - Or, Select, SignExt, Solver, SRem, Store, - Xor, ZeroExt, eq, is_eq, @@ -504,7 +501,7 @@ def pop(self) -> Word: raise StackUnderflowError() return self.stack.pop() - def popi(self) -> Word: + def popi(self) -> BV: """The stack can contain BitVecs or Bools -- this function converts Bools to BitVecs""" return BV(self.pop()) @@ -1735,16 +1732,14 @@ def add_all(cls, args: list) -> BitVecRef: def bitwise(op, x: Word, y: Word) -> Word: - if is_bool(x) and is_bool(y): - if op == EVM.AND: - return And(x, y) - elif op == EVM.OR: - return Or(x, y) - elif op == EVM.XOR: - return Xor(x, y) - else: - raise ValueError(op, x, y) - elif is_bv(x) and is_bv(y): + # only convert to BV if one of the operands is a bool + if isinstance(x, Bool) and isinstance(y, BV): + return bitwise(op, BV(x), y) + + elif isinstance(x, BV) and isinstance(y, Bool): + return bitwise(op, x, BV(y)) + + else: if op == EVM.AND: return x & y elif op == EVM.OR: @@ -1753,8 +1748,6 @@ def bitwise(op, x: Word, y: Word) -> Word: return x ^ y # bvxor else: raise ValueError(op, x, y) - else: - return bitwise(op, b2i(x), b2i(y)) def b2i(w: BitVecRef | BoolRef) -> BV: @@ -1904,7 +1897,7 @@ def arith(self, ex: Exec, op: int, w1: Word, w2: Word) -> Word: # if is_power_of_two(i2): # return LShR(w1, i2.bit_length() - 1) - + raise NotImplementedError("TODO: move to bitvec.py") return self.mk_div(ex, w1, w2) if op == EVM.MOD: @@ -2867,22 +2860,22 @@ def finalize(ex: Exec): elif opcode == EVM.LT: w1 = ex.st.popi() w2 = ex.st.popi() - ex.st.push(w1 < w2) # bvult + ex.st.push(w1.ult(w2)) # bvult elif opcode == EVM.GT: w1 = ex.st.popi() w2 = ex.st.popi() - ex.st.push(UGT(w1, w2)) # bvugt + ex.st.push(w1.ugt(w2)) # bvugt elif opcode == EVM.SLT: w1 = ex.st.popi() w2 = ex.st.popi() - ex.st.push(w1 < w2) # bvslt + ex.st.push(w1.slt(w2)) # bvslt elif opcode == EVM.SGT: w1 = ex.st.popi() w2 = ex.st.popi() - ex.st.push(w1 > w2) # bvsgt + ex.st.push(w1.sgt(w2)) # bvsgt elif opcode == EVM.EQ: w1 = ex.st.pop() @@ -2890,11 +2883,11 @@ def finalize(ex: Exec): match (w1, w2): case (Bool(), Bool()): - ex.st.push(w1 == w2) + ex.st.push(w1.eq(w2)) case (BV(), BV()): - ex.st.push(w1 == w2) + ex.st.push(w1.eq(w2)) case (_, _): - ex.st.push(BV(w1) == BV(w2)) + ex.st.push(BV(w1).eq(BV(w2))) elif opcode == EVM.ISZERO: ex.st.push(is_zero(ex.st.pop())) diff --git a/src/halmos/utils.py b/src/halmos/utils.py index 6c71ae0d..3445415e 100644 --- a/src/halmos/utils.py +++ b/src/halmos/utils.py @@ -249,7 +249,7 @@ def test(x: Word, b: bool) -> Word: def is_non_zero(x: Word) -> Bool: if isinstance(x, Bool): - return x.neg() + return x if isinstance(x, BV): return x.is_non_zero() @@ -261,7 +261,7 @@ def is_non_zero(x: Word) -> Bool: def is_zero(x: Word) -> Bool: if isinstance(x, Bool): - return x + return x.neg() if isinstance(x, BV): return x.is_zero() @@ -410,6 +410,9 @@ def int_of(x: Any, err: str = None, subst: dict = None) -> int: Converts int-like objects to int or raises NotConcreteError """ + if hasattr(x, "unwrap"): + x = x.unwrap() + # attempt to replace symbolic (sub-)terms with their concrete values if subst and is_bv(x) and not is_bv_value(x): x = simplify(substitute(x, *subst.items()))