solidity/test/formal/shl_workaround_8.py
2021-10-13 16:20:10 +02:00

29 lines
535 B
Python

from opcodes import SHL
from rule import Rule
from z3 import BitVec, BV2Int, Int2BV, IntVal
"""
Shift left workaround that Solidity implements
due to a bug in Boost.
"""
rule = Rule()
n_bits = 8
bigint_bits = 16
# Input vars
X = BitVec('X', n_bits)
A = BitVec('A', n_bits)
B = BitVec('B', bigint_bits)
# Compute workaround
workaround = Int2BV(
BV2Int(
(Int2BV(BV2Int(X), bigint_bits) << Int2BV(BV2Int(A), bigint_bits)) &
Int2BV(BV2Int(Int2BV(IntVal(-1), n_bits)), bigint_bits)
), n_bits
)
rule.check(workaround, SHL(A, X))