1from opcodes import SIGNEXTEND
2from rule import Rule
3from z3 import BitVec, BitVecVal, Extract, SignExt, UGT
4
5"""
6Checking the implementation of SIGNEXTEND using Z3's native SignExt and Extract
7"""
8
9rule = Rule()
10n_bits = 256
11
12x = BitVec('X', n_bits)
13
14def SIGNEXTEND_native(i, x):
15    return SignExt(256 - 8 * i - 8, Extract(8 * i + 7, 0, x))
16
17for i in range(0, 32):
18    rule.check(
19        SIGNEXTEND(BitVecVal(i, n_bits), x),
20        SIGNEXTEND_native(i, x)
21    )
22
23i = BitVec('I', n_bits)
24rule.require(UGT(i, BitVecVal(31, n_bits)))
25rule.check(SIGNEXTEND(i, x), x)
26