Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

A fairly regular CopySlice simplification #366

Merged
merged 5 commits into from
Sep 7, 2023
Merged

A fairly regular CopySlice simplification #366

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
dc6d0db
This occurs fairly often
msooseth Aug 28, 2023
6306808
Adding changelog entry
msooseth Aug 28, 2023
53dfe7d
Making this CopySlice rewrite more generic
msooseth Aug 31, 2023
a415b5f
Update src/EVM/Expr.hs
d-xo Sep 4, 2023
7a6b43e
Merge branch 'main' into simplified-copyslice
msooseth Sep 7, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,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
- Better simplification of Eq IR elements

## API Changes
Expand Down
11 changes: 11 additions & 0 deletions src/EVM/Expr.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -663,6 +663,17 @@ 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)
d-xo marked this conversation as resolved.
Show resolved Hide resolved
-- 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)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

fine to merge as is, but wondering if we can have some recursive rewrites that work for buffers other than a single writeword over concretebuf?

| 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
Expand Down
Loading