fix is_byte performance

a16z · Dec 22, 2023 · 06f6433 · 06f6433
1 parent 7c5c364
commit 06f6433
Showing 1 changed file with 9 additions and 4 deletions.
diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py
@@ -246,10 +246,6 @@ def wstore_partial(
         raise ValueError(data)
 
 
-def is_byte(x: Any) -> bool:
-    return x in range(0, 256) or (is_bv(x) and eq(x.sort(), BitVecSort8))
-
-
 def wstore_bytes(
     mem: List[UnionType[int, BitVecRef]], loc: int, size: int, arr: List[Byte]
 ) -> None:
@@ -264,6 +260,15 @@ def wstore_bytes(
         mem[loc + i] = val
 
 
+def is_byte(x: Any) -> bool:
+    if is_bv(x):
+        return eq(x.sort(), BitVecSort8)
+    elif isinstance(x, int):
+        return 0 <= x < 256
+    else:
+        return False
+
+
 def normalize(expr: Any) -> Any:
     # Concat(Extract(255, 8, op(x, y)), op(Extract(7, 0, x), Extract(7, 0, y))) => op(x, y)
     def normalize_extract(arg0, arg1):