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.

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

Proper error handling in JVM bytecode parser #924

Closed
brianhuffman opened this issue Nov 19, 2020 · 2 comments · Fixed by #1074
Closed

Proper error handling in JVM bytecode parser #924

brianhuffman opened this issue Nov 19, 2020 · 2 comments · Fixed by #1074
Assignees
Labels
subsystem: crucible-jvm Issues related to Java verification with crucible-jvm tech debt Issues that document or involve technical debt
Milestone

Comments

@brianhuffman
Copy link
Contributor

The JVM bytecode parser calls the haskell error function if it ever has any kind of parse error (see e.g. #920). This is not a nice way to handle problems in user-provided input files.

The jvm-parser needs to be redone with proper monadic error handling; reachable code should never call the haskell error function. I notice that it uses the Data.Binary.Get library, which provides two run functions: runGet (which calls error upon failure) and runGetIncremental (which returns a sum type). We should be using runGetIncremental.

@brianhuffman brianhuffman added subsystem: crucible-jvm Issues related to Java verification with crucible-jvm tech debt Issues that document or involve technical debt labels Nov 19, 2020
@brianhuffman
Copy link
Contributor Author

Besides the calls to error, the jvm-parser package also does a bunch of array lookups using the partial (!) operator from Data.Array. As the array indices are based on file input, there is no guarantee that they will be in bounds. Therefore we should avoid using this lookup operator.

@brianhuffman brianhuffman self-assigned this Dec 2, 2020
@atomb atomb added this to the 0.8 milestone Dec 11, 2020
@brianhuffman brianhuffman linked a pull request Feb 13, 2021 that will close this issue
@brianhuffman
Copy link
Contributor Author

The uses of error and runGet are addressed by GaloisInc/jvm-parser#9, which is included in saw-script with PR #1074. I think that's enough to close this ticket, although the partial array lookup operator (!) is still in use within jvm-parser, so there's still a bit of room for further improvement.

@mergify mergify bot closed this as completed in #1074 Feb 15, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: crucible-jvm Issues related to Java verification with crucible-jvm tech debt Issues that document or involve technical debt
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants