cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

An equivalence check for SIGNEXTEND opcode

Browse Source 
Checking the implementation of SIGNEXTEND using Z3's native SignExt and Extract
This commit is contained in:
hrkrshnn 2021-08-10 12:55:34 +02:00 committed by chriseth
parent 5906d25a39
commit 59db0f1537
1 changed files with 24 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
test/formal/signextend_equivalence.py Normal file
View File

@ -0,0 +1,24 @@
from rule import Rule
from opcodes import *
"""
Checking the implementation of SIGNEXTEND using Z3's native SignExt and Extract
"""
rule = Rule()
n_bits = 256
x = BitVec('X', n_bits)
def SIGNEXTEND_native(i, x):
return SignExt(256 - 8 * i - 8, Extract(8 * i + 7, 0, x))
for i in range(0, 32):
rule.check(
SIGNEXTEND(BitVecVal(i, n_bits), x),
SIGNEXTEND_native(i, x)
)
i = BitVec('I', n_bits)
rule.require(UGT(i, BitVecVal(31, n_bits)))
rule.check(SIGNEXTEND(i, x), x)