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

Jump to bottom

Typed exceptions #167

Closed
wants to merge 9 commits into from
Closed

Typed exceptions #167

wants to merge 9 commits into from

Conversation

ehildenb
Copy link
Member

This attaches metadata to the thrown exceptions so that it's easier to write bug-checking tools.

ehildenb
ehildenb commented Mar 21, 2018
View reviewed changes
driver.md
rule ETC:EthereumCommand ETS:EthereumSimulation => ETC ~> ETS
rule <k> .EthereumSimulation => . ... </k>
rule <k> ETC ETS:EthereumSimulation => ETC ~> ETS ... </k>
rule <k> ETC1:EthereumCommand ~> ETC2 ETS:EthereumSimulation => ETC1 ~> ETC2 ~> ETS ... </k>

Copy link
Member Author

Choose a reason for hiding this comment

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

@dwightguth I'm particularly interested in whether you have a better solution to this problem. I need __ to simplify out in the second position here as well.

@ehildenb
Copy link
Member Author

More changes coming, will let you know when ready to review.

dwightguth
dwightguth previously requested changes Mar 21, 2018
View reviewed changes
Copy link
Collaborator

@dwightguth dwightguth left a comment

Choose a reason for hiding this comment

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

I think it would be better if all exceptions had metadata instead of trying to duplicate every rule where we match on an exception, given that this information isn't /really/ part of the language. Also, I think you're missing some.

@ehildenb
Copy link
Member Author

@dwightguth I'll remove the non-metadata exceptions. I was thinking a similar thing.

@ehildenb
Copy link
Member Author

@daejunpark can you look at this PR and make a branch of the proofs repo which uses the typed exceptions instead?

@ehildenb
Copy link
Member Author

Jenkins: test this please

@ehildenb ehildenb mentioned this pull request Mar 23, 2018
Closed
@ehildenb
Copy link
Member Author

@daejunpark as mentioned in runtimeverification/verified-smart-contracts#10

Can you provide insight into why the Vyper proofs are passing? My impression was that Vyper does not generate INVALID opcode ever, based on discussion here: vyperlang/vyper#711

If it's not the case, please clarify. Also inspect the new proofs and approve this PR only if everything looks good on that repo.

@ehildenb ehildenb dismissed dwightguth’s stale review March 23, 2018 21:02

Have updated to remove non-typed exceptions.

@ehildenb
Copy link
Member Author

Jenkins: test this please

@ehildenb ehildenb force-pushed the typed-exceptions branch 2 times, most recently from 0fd630b to 4390f0f Compare March 26, 2018 22:21
@ehildenb
Copy link
Member Author

@pepyakin I've removed the EVM_OUT_OF_MEMORY exception, it's been supersceded by EVM_INVALID_MEMORY_ACCESS from ethereum/evmjit#173

@ehildenb
Copy link
Member Author

@dwightguth please re-review.

@ehildenb ehildenb mentioned this pull request Mar 28, 2018
Closed
dwightguth
dwightguth approved these changes Mar 28, 2018
View reviewed changes
Copy link
Collaborator

@dwightguth dwightguth left a comment

Choose a reason for hiding this comment

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

I only see one minor issue, please fix it before you merge, but it otherwise looks good so I'm going to approve.

evm.md Outdated
@@ -408,13 +412,13 @@ The `#next` operator executes a single step by:
</k>
```

- `#invalid?` checks if it's the designated invalid opcode.
- `#invalid?` checks if it's the designated invalid opcode, and throws `#exception ASSERT_FAILURE` if it is.
Copy link
Collaborator

Choose a reason for hiding this comment

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

seems to be an out of date comment

@ehildenb ehildenb mentioned this pull request Mar 29, 2018
Merged
@ehildenb
Copy link
Member Author

Closing until I have a chance to fix #177

@ehildenb ehildenb closed this Mar 29, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@dwightguth dwightguth dwightguth approved these changes

@daejunpark daejunpark Awaiting requested review from daejunpark

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@ehildenb @dwightguth