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

Ensure fixes are not lost when they lead to errors #302

Merged
merged 3 commits into from
Jul 17, 2024

Conversation

N1ark
Copy link
Contributor

@N1ark N1ark commented Jul 13, 2024

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
};

Generated specs diff (before/after):

BUG SPECS:
  spec test ()
    ;
-   [[ emp ]]
-   [[ emp ]]
+   [[ <freed>(; ) ]]
+   [[ <freed>(; ) ]]
    bug

ERROR SPECS:
  

SUCCESSFUL SPECS:
  spec test ()
    [[ <points_to>(; #gen__0) ]]
    [[ (ret == 0i) * <points_to>(; 6i) ]]
    normal;

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):

  • 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.

In particular in `PState.m_err_t`, `CMemory.err_t`, `CState.m_err_t`, `State.m_err_t`
@giltho giltho merged commit 51cf7cf into GillianPlatform:master Jul 17, 2024
8 of 9 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants