1from opcodes import NOT, SUB
2from rule import Rule
3from z3 import BitVec, BitVecVal
4
5"""
6Rule:
7SUB(~0, X) -> NOT(X)
8Requirements:
9"""
10
11rule = Rule()
12
13n_bits = 256
14
15# Input vars
16X = BitVec('X', n_bits)
17
18# Constants
19ZERO = BitVecVal(0, n_bits)
20
21# Non optimized result
22nonopt = SUB(~ZERO, X)
23
24# Optimized result
25opt = NOT(X)
26
27rule.check(nonopt, opt)
28