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

mir_unsafe_assume_spec #1959

Merged
merged 5 commits into from
Nov 22, 2023
Merged

mir_unsafe_assume_spec #1959

merged 5 commits into from
Nov 22, 2023
+2,056 −275

Commits on Nov 22, 2023

  1. Add maConditionMetadata to MirAllocSpec 

    This will prove useful in a subsequent commit where we add support for
overrides in MIR, which make use of this `ConditionMetadata`.
    @RyanGlScott
    RyanGlScott committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    0a6be48 View commit details
    Browse the repository at this point in the history

  2. Refactor: Move checkCompatibleTys, readMaybeType, firstPointsToReferent 

    These will need to be accessible from
`SAWScript.Crucible.MIR.ResolveSetupValue` in a subsequent patch.
    @RyanGlScott
    RyanGlScott committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    6234628 View commit details
    Browse the repository at this point in the history

  3. Use ppMIRVal in mkStructuralMismatch

    @RyanGlScott
    RyanGlScott committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    69f0dc5 View commit details
    Browse the repository at this point in the history

  4. Refactor: Move some definitions to SAWScript.Crucible.Common.Override 

    These previously existed as internal definitions in the LLVM and JVM backends,
but nothing about these definitions are specific any particular backend. In a
subsequent patch, I will make use of these definitions in the MIR backend, so
it is nice to avoid having to duplicate them further.
    @RyanGlScott
    RyanGlScott committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    256251d View commit details
    Browse the repository at this point in the history

  5. mir_unsafe_assume_spec 

    This implements supports for compositional overrides in the SAW MIR backend,
largely inspired by the existing implementation in the LLVM backend. I've added
`test_mir_unsafe_assume_spec` and `test_mir_unsafe_assume_spec_statics`
integration tests to kick the tires and ensure the basics work as expected.

One place where the MIR backend meaningfully differs from the LLVM backend with
respect to compositional overrides is in the treatment of mutable allocations.
While the LLVM backend is content to simply invalidate the memory of
underspecified mutable allocations that appear in the postconditions of
overrides, the MIR backend is stricter and will outright reject any such
underspecified mutable allocations, regardless of whether they are used or not.
For further commentary on this, see the new sections of the SAW manual, as well
as the `Note [MIR compositional verification and mutable allocations]` that
describes the implementation.

Checks off one box in #1859.
    @RyanGlScott
    RyanGlScott committed Nov 22, 2023
    Configuration menu
    Copy the full SHA
    ac46b5b View commit details
    Browse the repository at this point in the history