1from opcodes import SIGNEXTEND, AND 2from rule import Rule 3from z3 import BitVec, BitVecVal, ULT 4 5""" 6Rule: 7AND(A, SIGNEXTEND(B, X)) -> AND(A, X) 8given 9 B < WordSize / 8 - 1 AND 10 A & (1 << ((B + 1) * 8) - 1) == A 11""" 12 13n_bits = 128 14 15# Input vars 16X = BitVec('X', n_bits) 17A = BitVec('A', n_bits) 18B = BitVec('B', n_bits) 19 20rule = Rule() 21# Requirements 22rule.require(ULT(B, BitVecVal(n_bits // 8 - 1, n_bits))) 23rule.require((A & ((BitVecVal(1, n_bits) << ((B + 1) * 8)) - 1)) == A) 24rule.check( 25 AND(A, SIGNEXTEND(B, X)), 26 AND(A, X) 27) 28