From b92172d66a4d3da4343ff7251abece12ecc55fc5 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 19 Sep 2023 16:10:49 -0700 Subject: [PATCH 1/3] fix xor semantics --- src/halmos/sevm.py | 41 ++++++++++++++++++----------------------- 1 file changed, 18 insertions(+), 23 deletions(-) diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 6ffa3bfd..eb62b703 100644 --- 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())) From 773000aede08f2683817f7181ca6af6c4fcc7dc3 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 19 Sep 2023 18:42:09 -0700 Subject: [PATCH 2/3] fix not semantics --- src/halmos/sevm.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index eb62b703..067de24d 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -2489,7 +2489,7 @@ def run(self, ex0: Exec) -> Tuple[List[Exec], Steps]: 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 + ex.st.push(~b2i(ex.st.pop())) # bvnot elif opcode == EVM.SHL: w = ex.st.pop() ex.st.push(b2i(ex.st.pop()) << b2i(w)) # bvshl From 77c8076b489e5ed85e266ef994dbc7e53cc83821 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 19 Sep 2023 18:42:25 -0700 Subject: [PATCH 3/3] cleanup --- src/halmos/sevm.py | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 067de24d..875de16b 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -1227,7 +1227,7 @@ def is_zero(x: Word) -> Word: return test(x, False) -def lop(op, x: Word, y: Word) -> Word: +def bitwise(op, x: Word, y: Word) -> Word: if is_bool(x) and is_bool(y): if op == EVM.AND: return And(x, y) @@ -1243,13 +1243,13 @@ def lop(op, x: Word, y: Word) -> Word: elif op == EVM.OR: return x | y elif op == EVM.XOR: - return x ^ y + return x ^ y # bvxor else: raise ValueError(op, x, y) elif is_bool(x) and is_bv(y): - return lop(op, If(x, con(1), con(0)), y) + return bitwise(op, If(x, con(1), con(0)), y) elif is_bv(x) and is_bool(y): - return lop(op, x, If(y, con(1), con(0))) + return bitwise(op, x, If(y, con(1), con(0))) else: raise ValueError(op, x, y) @@ -2487,7 +2487,7 @@ def run(self, ex0: Exec) -> Tuple[List[Exec], Steps]: ex.st.push(is_zero(ex.st.pop())) elif opcode in [EVM.AND, EVM.OR, EVM.XOR]: - ex.st.push(lop(opcode, ex.st.pop(), ex.st.pop())) + ex.st.push(bitwise(opcode, ex.st.pop(), ex.st.pop())) elif opcode == EVM.NOT: ex.st.push(~b2i(ex.st.pop())) # bvnot elif opcode == EVM.SHL: