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

Crucible/LLVM: Group argument equality assertions in override matching #522

Closed
langston-barrett opened this issue Aug 2, 2019 · 0 comments · Fixed by #525
Closed

Crucible/LLVM: Group argument equality assertions in override matching #522

langston-barrett opened this issue Aug 2, 2019 · 0 comments · Fixed by #525
Assignees
Labels
subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm topics: error-messages Issues involving the messages SAW produces on error type: enhancement Issues describing an improvement to an existing feature or capability

Comments

@langston-barrett
Copy link
Contributor

Crucible/LLVM currently matches arguments for overrides by collecting a bunch of assertions (from methodSpecHandler_prestate):

       xs <- liftIO (zipWithM aux expectedArgTypes (assignmentToList args))
       sequence_ [ matchArg opts sc cc cs PreState x y z | (x, y, z) <- xs]

The matchArg function is in an OverrideState state monad, and so doesn't return the assertions it makes. We're losing granularity here: when the call to matchArg is made, we know that the added assertions are related to an equality condition for the override's arguments, but after the call we have no understanding of where they came from.

If we keep track of which argument equality these assertions come from, we can later report that more meaningfully/at a higher level to the user.

@langston-barrett langston-barrett added topics: error-messages Issues involving the messages SAW produces on error subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm type: enhancement Issues describing an improvement to an existing feature or capability labels Aug 2, 2019
langston-barrett added a commit to langston-barrett/saw-script that referenced this issue Aug 7, 2019
langston-barrett added a commit to langston-barrett/saw-script that referenced this issue Aug 7, 2019
@langston-barrett langston-barrett self-assigned this Aug 7, 2019
langston-barrett added a commit that referenced this issue Aug 7, 2019
#525)

* More explicit handling of assertions in override matching

* Crucible/LLVM: Better errors for argument and return value equalities

Fixes #522

* Propagate changes to methodSpecHandler

* add space

* Simplify

* Add an assertion
Ptival pushed a commit that referenced this issue Oct 31, 2019
#525)

* More explicit handling of assertions in override matching

* Crucible/LLVM: Better errors for argument and return value equalities

Fixes #522

* Propagate changes to methodSpecHandler

* add space

* Simplify

* Add an assertion
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm topics: error-messages Issues involving the messages SAW produces on error type: enhancement Issues describing an improvement to an existing feature or capability
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant