From 62c1aa84511dc6b321ac9b5a1ceb7b36b02a6d2b Mon Sep 17 00:00:00 2001 From: zoep Date: Wed, 1 May 2024 20:00:11 +0300 Subject: [PATCH] Decompile: new rewriting rule from work with Lexi and sideconditions --- src/Act/Decompile.hs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/Act/Decompile.hs b/src/Act/Decompile.hs index f74fe2c9..ae519ca3 100644 --- a/src/Act/Decompile.hs +++ b/src/Act/Decompile.hs @@ -63,7 +63,6 @@ import Act.Error import Act.Traversals - -- Top Level --------------------------------------------------------------------------------------- @@ -387,6 +386,12 @@ fromWord layout w = go w pure . evmbool $ InRange nowhere (AbiUIntType 256) (Mul nowhere a' b') + -- SLT (max(a, length txdata) - 4) b == 0 if a - 4 = b + -- sideconditions: a - 4 < (2 ^ 256)/2 and b < (2 ^ 256)/2 so that both numbers are positive in two's complement. Otherwise SLT might not have the intended semantics. + -- For example SLT 42 2^255 == 0, because in two's complement 2^255 represents - 2 ^ 255 + -- Note that we already have (length txdata) <= 2 ^ 64. These restrictions could be relaxed further, but it is not needed for our intended use + go (EVM.SLT (EVM.Mod (EVM.Add (EVM.Lit 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffc) (EVM.Max (EVM.Lit a) (EVM.BufLength (EVM.AbstractBuf "txdata")))) (EVM.Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff)) (EVM.Lit b)) | (a - 4 == b) && (a - 4) < 2^(255 :: Integer) && b < 2^(255 :: Integer)= pure (LitInt nowhere 0) + -- booleans go (EVM.LT a b) = do