more fixes

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,16 +958,19 @@ 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]
         if contract_type != "contract":
             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:

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)

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,34 +2860,34 @@ 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()
                     w2 = ex.st.pop()
 
                     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()))

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()))