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.

Sign up for GitHub

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

Jump to bottom

Goal metadata #1679

Merged
merged 12 commits into from
Jun 2, 2022
Merged

Goal metadata #1679

merged 12 commits into from
Jun 2, 2022

Commits on Jun 2, 2022

  1. Introduce a notion of "condition metadata", which 

    currently tracks the location a condition was asserted
(in the proof script), and user-specified "tags"
that can be associated. The condition metadata is
threaded through symbolic exeuction and attached to
the resulting verification goals.  Then, tactics
can query the tags associated to goals in order
to filter them and take different actions.

Currently, only the LLVM verification method threads
through metadata information; the JVM and X86 verification
modules need to be modified in a similar way.
    @robdockins
    robdockins committed Jun 2, 2022
    Configuration menu
    Copy the full SHA
    fa6958e View commit details
    Browse the repository at this point in the history

  2. Implement a special case when we have exactly one override that could 

    apply after structural matching. In this (common) special case,
we can have a more natural handling of function preconditions
which allows us to retain better metadata about them.
    @robdockins
    robdockins committed Jun 2, 2022
    Configuration menu
    Copy the full SHA
    1adda9d View commit details
    Browse the repository at this point in the history

  3. Fix warnings

    @robdockins
    robdockins committed Jun 2, 2022
    Configuration menu
    Copy the full SHA
    55611fa View commit details
    Browse the repository at this point in the history

  4. Fix crux-mir-comp build

    @robdockins
    robdockins committed Jun 2, 2022
    Configuration menu
    Copy the full SHA
    d0ac7e2 View commit details
    Browse the repository at this point in the history

  5. Implement partial condition metadata tracking for JVM. 

    Override preconditions are still not currently handled.
    @robdockins
    robdockins committed Jun 2, 2022
    Configuration menu
    Copy the full SHA
    20ed0b0 View commit details
    Browse the repository at this point in the history

  6. Gate the new special-case handling of single overrides 

    with an option.

Changing the number/order of goals generated seems like it was
disrupting some preexisting proofs.
    @robdockins
    robdockins committed Jun 2, 2022
    Configuration menu
    Copy the full SHA
    b99840c View commit details
    Browse the repository at this point in the history

  7. Pipe condition metadata through the X86 verification modes.

    @robdockins
    robdockins committed Jun 2, 2022
    Configuration menu
    Copy the full SHA
    ecef4a7 View commit details
    Browse the repository at this point in the history

  8. Add a simple test for the goal tagging primitives.

    @robdockins
    robdockins committed Jun 2, 2022
    Configuration menu
    Copy the full SHA
    58289a4 View commit details
    Browse the repository at this point in the history

  9. Update changelog

    @robdockins
    robdockins committed Jun 2, 2022
    Configuration menu
    Copy the full SHA
    cc2ba1b View commit details
    Browse the repository at this point in the history

  10. Stray comments/typos

    @robdockins
    robdockins committed Jun 2, 2022
    Configuration menu
    Copy the full SHA
    79e7ea9 View commit details
    Browse the repository at this point in the history

  11. Update JVM and X86 metadata propagation to match LLVM.

    @robdockins
    robdockins committed Jun 2, 2022
    Configuration menu
    Copy the full SHA
    67fe177 View commit details
    Browse the repository at this point in the history

  12. Add the jvm_setup_with_tag primitive, similar to the LLVM one 

    with a similar name.
    @robdockins
    robdockins committed Jun 2, 2022
    Configuration menu
    Copy the full SHA
    84b00b7 View commit details
    Browse the repository at this point in the history