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