Proof.

test/formal/redundant_store_unrelated.py

@@ -0,0 +1,55 @@
+from z3 import Solver, Int, IntVal, unsat
+import sys
+
+"""
+Tests that the conditions inside RedundantStoreEliminator::knownUnrelated
+properly account for overflow.
+
+"""
+
+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 - length2)
+
+# x is a potential point where the memory operations
+# overlap.
+# Note that we do not use wrapping arithmetics
+# 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)
+
+if solver.check() != unsat:
+  print("Expected unsat but got something else")
+  sys.exit(1)