Maps and Arrays cannot match + masking rewrite rule #756
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
msooseth
force-pushed
the
array-map-cannot-clash
branch
3 times, most recently
from
575ee3b to
c211e17
Compare
msooseth
changed the title
msooseth
force-pushed
the
array-map-cannot-clash
branch
from
c211e17 to
bde48c6
Compare
Update changelog
msooseth
force-pushed
the
array-map-cannot-clash
branch
from
bde48c6 to
33af861
Compare
msooseth
changed the title
blishko
reviewed
Jun 1, 2025
| @@ -3953,8 +3976,7 @@ tests = testGroup "hevm" | |||
| _ -> False | |||
| assertBoolM "Did not find expected storage cex" testCex | |||
| putStrLnM "expected counterexample found" | |||
| , | |||
| expectFail $ test "calling unique contracts (read from storage)" $ do | |||
| , test "calling-unique-contracts--read-from-storage" $ do | |||
There was a problem hiding this comment.
Can you explain what changed here?
What exactly is this test checking?
What was happening before and what is happening now?
| @@ -161,6 +161,7 @@ getMultiSol smt2@(SMT2 cmds cexvars _) multiSol r inst availableInstances fileCo | |||
| writeChan r Nothing | |||
| Right _ -> do | |||
| sat <- liftIO $ sendLine inst "(check-sat)" | |||
| when conf.dumpQueries $ liftIO $ writeSMT2File smt2 (show fileCounter <> "-origquery") | |||
There was a problem hiding this comment.
Should this be in a separate PR?
Comment on lines
+1091
to
+1094
| -- Masking as as per Solidity bit-packing of e.g. function parameters | ||
| go (And (Lit mask1) (Or (And (Lit mask2) _) x)) | (mask1 .&. mask2 == 0) | ||
| = And (Lit mask1) x | ||
|
|
There was a problem hiding this comment.
Nice!
Do we get this pattern also in optimized bytecode? Or only unoptimized?
Meaning, is this maybe some optimization that solc should be doing but is not?
Comment on lines
+661
to
+664
| (MappingSlot idA _, ArraySlotWithOffs idB (Lit offs)) | isMap' idA, isArray idB, offs < 1000 -> go slot prev | ||
| (Keccak idA, ArraySlotWithOffs idB (Lit offs)) | isMap idA, isArray idB, offs < 1000 -> go slot prev | ||
| (ArraySlotWithOffs idA (Lit offs), Keccak idB) | isArray idA, isMap idB, offs < 1000 -> go slot prev | ||
| (ArraySlotWithOffs idA (Lit offs), MappingSlot idB _) | isArray idA, isMap' idB, offs < 1000 -> go slot prev |
There was a problem hiding this comment.
Why is the magic number 1000?
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description
When either the Array offset is low or 0, Maps and Arrays cannot clash. Furthermore, I added one more rewrite rule that allows us to deal with Solidity argument packing.
I added a test for the masking rewrite rule. It also happens to fix an issue we had in one of our tests, so that has been enabled as well (should have had
ignoreTest, notexpectFail, now it's enabled)Checklist