-
Notifications
You must be signed in to change notification settings - Fork 63
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
Don't fail when What4 sends us a function-based array in a result. #2121
Conversation
-- it should be implemented in What4 so What4 never returns | ||
-- ArrayMapping. | ||
-- | ||
-- (See note in FiniteValue.hs where FirstOrderValue lives.) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
To make this more obvious:
-- (See note in FiniteValue.hs where FirstOrderValue lives.) | |
-- (See Note [FOVArray] in saw-core:Verifier.SAW.FiniteValue.) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fixed
-- | ||
-- FOVOpaqueArray is for arrays we get back from the solver only as a | ||
-- function call that one can use for lookups. We can't do anything | ||
-- with that (see notes below) so we just treat it as an opaque blob. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
-- with that (see notes below) so we just treat it as an opaque blob. | |
-- with that (see Note [FOVArray]) so we just treat it as an opaque blob. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Fixed
We can't store function-based arrays in FirstOrderValue for a number of reasons. But we also can't do anything much useful with them, so if we get one (unfortunately this does happen, which may or may not be amenable to improvement in What4) treat it as an opaque blob. Add an FOVOpaqueArray to FirstOrderValue for this. The footprint of having this undesirable object is not large, so it's the path of least resistance. We could in principle instead return something other than a FirstOrderValue out of groundToFOV for this case, if we had a use for the actual function, but since we can't do anything much with the function because we have no idea what keys to look up, there doesn't seem to be any point.
6be8c80
to
d489ee3
Compare
(force-pushed to squash) |
(see commit for description)
Fixes #2120.