Bugs in HEVM Equivalence #203
Open
+350
−350
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
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.
This PR fixes two bugs in HEVM equivalence:
The arguments of constructor calls where being substituted in the update expressions. As a result, they where evaluated in the callee context that have wrong results (the new test tests/hevm/pass/multi6/multi6.act was not working properly before. Now the arguments are evaluated in the caller context and are being passed around in an environment.
The resulting storage graph of the constructor was not being checked for aliased contract references. Act disallows having the same contract address stored twice in the storage of a contract. This was already checked for behaviours, but was missing from constructors. This is now done with the
checkTreefunction.Few more tests were added. Some tests had to be moved from
passtofailbecause of the aliasing check (they were never supposed to succeed).Note that the various error messages in
HEVM.hsare quite messy and they should be fixed in a future PR.