solidity/test/formal/replace_mul_by_shift.py
2021-03-18 08:42:49 +01:00

38 lines
559 B
Python

from rule import Rule
from opcodes import *
"""
Rule:
MUL(X, A) -> SHL(k, X)
MUL(A, X) -> SHL(k, X)
DIV(X, A) -> SHR(k, X)
Requirements:
A == 1 << K
"""
rule = Rule()
n_bits = 32
# Input vars
X = BitVec('X', n_bits)
A = BitVec('A', n_bits)
K = BitVec('K', n_bits)
# Requirements
rule.require(A == SHL(K, 1))
# Non optimized result
nonopt_1 = MUL(X, A)
nonopt_2 = MUL(A, X)
nonopt_3 = DIV(X, A)
# Optimized result
opt_1 = SHL(K, X)
opt_2 = SHL(K, X)
opt_3 = SHR(K, X)
rule.check(nonopt_1, opt_1)
rule.check(nonopt_2, opt_2)
rule.check(nonopt_3, opt_3)