fix xor semantics

a16z · Sep 19, 2023 · b92172d · b92172d
1 parent c13095d
commit b92172d
Showing 1 changed file with 18 additions and 23 deletions.
diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py
@@ -1227,31 +1227,31 @@ def is_zero(x: Word) -> Word:
     return test(x, False)
 
 
-def and_or(x: Word, y: Word, is_and: bool) -> Word:
+def lop(op, x: Word, y: Word) -> Word:
     if is_bool(x) and is_bool(y):
-        if is_and:
+        if op == EVM.AND:
             return And(x, y)
-        else:
+        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):
-        if is_and:
+        if op == EVM.AND:
             return x & y
-        else:
+        elif op == EVM.OR:
             return x | y
+        elif op == EVM.XOR:
+            return x ^ y
+        else:
+            raise ValueError(op, x, y)
     elif is_bool(x) and is_bv(y):
-        return and_or(If(x, con(1), con(0)), y, is_and)
+        return lop(op, If(x, con(1), con(0)), y)
     elif is_bv(x) and is_bool(y):
-        return and_or(x, If(y, con(1), con(0)), is_and)
+        return lop(op, x, If(y, con(1), con(0)))
     else:
-        raise ValueError(x, y, is_and)
-
-
-def and_of(x: Word, y: Word) -> Word:
-    return and_or(x, y, True)
-
-
-def or_of(x: Word, y: Word) -> Word:
-    return and_or(x, y, False)
+        raise ValueError(op, x, y)
 
 
 def b2i(w: Word) -> Word:
@@ -2486,10 +2486,8 @@ def run(self, ex0: Exec) -> Tuple[List[Exec], Steps]:
                 elif opcode == EVM.ISZERO:
                     ex.st.push(is_zero(ex.st.pop()))
 
-                elif opcode == EVM.AND:
-                    ex.st.push(and_of(ex.st.pop(), ex.st.pop()))
-                elif opcode == EVM.OR:
-                    ex.st.push(or_of(ex.st.pop(), ex.st.pop()))
+                elif opcode in [EVM.AND, EVM.OR, EVM.XOR]:
+                    ex.st.push(lop(opcode, ex.st.pop(), ex.st.pop()))
                 elif opcode == EVM.NOT:
                     ex.st.push(~ex.st.pop())  # bvnot
                 elif opcode == EVM.SHL:
@@ -2508,9 +2506,6 @@ def run(self, ex0: Exec) -> Tuple[List[Exec], Steps]:
                         bl = (w + 1) * 8
                         ex.st.push(SignExt(256 - bl, Extract(bl - 1, 0, ex.st.pop())))
 
-                elif opcode == EVM.XOR:
-                    ex.st.push(ex.st.pop() ^ ex.st.pop())  # bvxor
-
                 elif opcode == EVM.CALLDATALOAD:
                     if ex.calldata is None:
                         ex.st.push(f_calldataload(ex.st.pop()))