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):
bispec test () : [[ emp ]]
proc test() {
gvar0 := [load]();
ret := 0i;
return
};
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):
Needed to extended the signature of BiState.mli to include information on m_err_t.
To do that I needed to refer to S.t, which at that point isn't defined yet, so I need to define it explicitly, which requires me to define a BiState._t type (which leaks no information but must exist).
I also couldn't call it simply t, because otherwise I need to define the type t in the Make functor as nonrec, and nonrec types don't support PPX 🫠
If there is a way to refer to a type in include State.S with type ... without defining it, let me know as it would avoid this mess (ie. if there's a way of having m_err_t = t * BaseState.m_err_t)
SState doesn't enforce m_err_t to derrive yojson/show, so I can't automatically derive yojson/show on err_t either.
For show it's ok because I can unlift the error and use SState.show
For 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 in err_t_of_yojson. I would have otherwise just put an empty state, but that requires init_data which I have no way of extracting+parsing.
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
BiStateto always include an up to date copy of the state along with every memory error. When encountering failures,Abductorthen 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.mlito 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._ttype (which leaks no information but must exist).t, because otherwise I need to define thetype tin theMakefunctor asnonrec, andnonrectypes 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)SStatedoesn't enforcem_err_tto derrive yojson/show, so I can't automatically derive yojson/show onerr_teither.showit's ok because I can unlift the error and useSState.showyojsonhowever, 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_datawhich I have no way of extracting+parsing.