From dc6d0db607a7f232f46dbdd609061e89f62cb5fc Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Mon, 28 Aug 2023 13:59:06 +0200 Subject: [PATCH 1/4] This occurs fairly often --- src/EVM/Expr.hs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs index 4539e5792..03dc17522 100644 --- a/src/EVM/Expr.hs +++ b/src/EVM/Expr.hs @@ -663,6 +663,8 @@ simplify e = if (mapExpr go e == e) go (WriteWord a b c) = writeWord a b c go (WriteByte a b c) = writeByte a b c + go (CopySlice srcOff@(Lit 0) dstOff size@(Lit sz) (WriteWord (Lit 0) value (ConcreteBuf buf)) dst) = (CopySlice srcOff dstOff size (WriteWord (Lit 0) value (ConcreteBuf simplifiedBuf)) dst) + where simplifiedBuf = BS.take (unsafeInto sz) buf go (CopySlice a b c d f) = copySlice a b c d f go (IndexWord a b) = indexWord a b From 6306808c5d581b73af9f0f6c54a37d21cbe81610 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Mon, 28 Aug 2023 14:08:29 +0200 Subject: [PATCH 2/4] Adding changelog entry --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index a5280f098..ef61f9b7f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -40,6 +40,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - Contract balances can now be fully symbolic - Contract code can now be fully abstract. Calls into contracts with unknown code will fail with `UnexpectedSymbolicArg`. - Run expression simplification on branch conditions +- CopySlice+WriteWord+ConcreteBuf now truncates ConcreteBuf in special cases ## API Changes From 53dfe7d76e9318973572818f0d265cc724b97725 Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Thu, 31 Aug 2023 16:33:45 +0200 Subject: [PATCH 3/4] Making this CopySlice rewrite more generic --- src/EVM/Expr.hs | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs index 03dc17522..92bcf3d7b 100644 --- a/src/EVM/Expr.hs +++ b/src/EVM/Expr.hs @@ -663,8 +663,15 @@ simplify e = if (mapExpr go e == e) go (WriteWord a b c) = writeWord a b c go (WriteByte a b c) = writeByte a b c - go (CopySlice srcOff@(Lit 0) dstOff size@(Lit sz) (WriteWord (Lit 0) value (ConcreteBuf buf)) dst) = (CopySlice srcOff dstOff size (WriteWord (Lit 0) value (ConcreteBuf simplifiedBuf)) dst) - where simplifiedBuf = BS.take (unsafeInto sz) buf + go orig@(CopySlice srcOff@(Lit n) dstOff size@(Lit sz) + -- It doesn't matter what wOffs we write to, because only the first + -- n+sz of ConcreteBuf will be used by CopySlice + (WriteWord wOff value (ConcreteBuf buf)) dst) + -- Let's not deal with overflow + | n+sz >= n && n+sz >= sz = (CopySlice srcOff dstOff size + (WriteWord wOff value (ConcreteBuf simplifiedBuf)) dst) + | otherwise = orig + where simplifiedBuf = BS.take (unsafeInto (n+sz)) buf go (CopySlice a b c d f) = copySlice a b c d f go (IndexWord a b) = indexWord a b From a415b5f80cd2a1aaaf208d831b4f6ccc9243c90b Mon Sep 17 00:00:00 2001 From: dxo <6689924+d-xo@users.noreply.github.com> Date: Mon, 4 Sep 2023 13:31:08 +0200 Subject: [PATCH 4/4] Update src/EVM/Expr.hs --- src/EVM/Expr.hs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs index 92bcf3d7b..d9559007b 100644 --- a/src/EVM/Expr.hs +++ b/src/EVM/Expr.hs @@ -663,6 +663,8 @@ simplify e = if (mapExpr go e == e) go (WriteWord a b c) = writeWord a b c go (WriteByte a b c) = writeByte a b c + + -- truncate some concrete source buffers to the portion relevant for the CopySlice if we're copying a fully concrete region go orig@(CopySlice srcOff@(Lit n) dstOff size@(Lit sz) -- It doesn't matter what wOffs we write to, because only the first -- n+sz of ConcreteBuf will be used by CopySlice