mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
64 lines
1.5 KiB
Python
64 lines
1.5 KiB
Python
import sys
|
|
from z3 import Solver, Int, unsat
|
|
|
|
"""
|
|
Tests that the conditions inside RedundantStoreEliminator::knownUnrelated
|
|
only return "unrelated" incorrectly if one of the operation reverts
|
|
due to large memory access.
|
|
"""
|
|
|
|
n_bits = 256
|
|
|
|
solver = Solver()
|
|
solver.set("timeout", 60000)
|
|
|
|
def restrict(x):
|
|
solver.add(x >= 0)
|
|
solver.add(x < 2**n_bits)
|
|
|
|
def restrictedInt(x):
|
|
var = Int(x)
|
|
restrict(var)
|
|
return var
|
|
|
|
start1 = restrictedInt('start1')
|
|
length1 = restrictedInt('length1')
|
|
start2 = restrictedInt('start2')
|
|
length2 = restrictedInt('length2')
|
|
|
|
k = Int('k')
|
|
diff = Int('diff')
|
|
solver.add(diff == start2 - start1 + k * 2**n_bits)
|
|
restrict(diff)
|
|
# diff is the result of sub(start2, start1) in EVM
|
|
|
|
# These are the conditions in the code.
|
|
solver.add(diff >= length1)
|
|
solver.add(diff <= 2**(n_bits-1))
|
|
|
|
# We check that the two conditions are conflicting:
|
|
# - overlap
|
|
# - start1 is small
|
|
|
|
# Overlap:
|
|
# x is a potential point where the memory operations
|
|
# overlap.
|
|
# Note that we do not use wrapping arithmetic
|
|
# here, because it is not done in the EVM either.
|
|
# For example calldatacopy(2**256 - 2, 0, 10)
|
|
# (copy 10 bytes from calldata position zero to memory
|
|
# position 2**256 - 2) would not write to memory position
|
|
# zero either.
|
|
x = Int('x')
|
|
solver.add(start1 <= x)
|
|
solver.add(x < start1 + length1)
|
|
solver.add(start2 <= x)
|
|
solver.add(x < start2 + length2)
|
|
|
|
# start1 is "small":
|
|
solver.add(start1 < 2**(n_bits-1))
|
|
|
|
if solver.check() != unsat:
|
|
print("Expected unsat but got something else")
|
|
sys.exit(1)
|