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