Ensure fixes are not lost when they lead to errors #302
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.
If a bug is found in bi-abduction that happens during the same command a fix is generated, the state before the command was executed is used to generate the spec, which means the fix gets lost.
This PR modifies
BiState
to always include an up to date copy of the state along with every memory error. When encountering failures,Abductor
then checks if any of the errors is a memory error, in which case it uses the attached state rather instead.Example
For a state model stack
Freeable(Exclusive)
:Generated specs diff (before/after):
Notes
A couple hacky things I did, that I don't like but don't know how to avoid (I'm happy to edit the PR with suggestions):
BiState.mli
to include information onm_err_t
.S.t
, which at that point isn't defined yet, so I need to define it explicitly, which requires me to define aBiState._t
type (which leaks no information but must exist).t
, because otherwise I need to define thetype t
in theMake
functor asnonrec
, andnonrec
types don't support PPX 🫠include State.S with type ...
without defining it, let me know as it would avoid this mess (ie. if there's a way of havingm_err_t = t * BaseState.m_err_t
)SState
doesn't enforcem_err_t
to derrive yojson/show, so I can't automatically derive yojson/show onerr_t
either.show
it's ok because I can unlift the error and useSState.show
yojson
however, I need to hand parse it which isn't super pretty -- I can't unlift it because then I lost the information on the state, which means I can't recreate the error inerr_t_of_yojson
. I would have otherwise just put an empty state, but that requiresinit_data
which I have no way of extracting+parsing.