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