`mir_unsafe_assume_spec` #1959

RyanGlScott · 2023-10-13T16:03:22Z

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

This is a large patch, but most of it is cargo-culted from the LLVM backend and is therefore not that interesting to review. I've left comments in the most interesting parts of the patch.

RyanGlScott · 2023-11-09T16:45:22Z

doc/manual/manual.md

@@ -2416,6 +2414,295 @@ In this case, doing the verification compositionally doesn't save
 computational effort, since the functions are so simple, but it
 illustrates the approach.

+### Compositional Verification and Mutable Allocations


The documentation. Due to the way the SAW manual is set up, I describe compositional verification in both the LLVM and MIR backends here, although this patch doesn't change anything in the way that the LLVM backend works.

RyanGlScott · 2023-11-09T16:46:13Z

intTests/test_mir_unsafe_assume_spec/test.saw

@@ -0,0 +1,159 @@
+enable_experimental;


The first test case, which doesn't involve mutable statics.

RyanGlScott · 2023-11-09T16:47:05Z

intTests/test_mir_unsafe_assume_spec_statics/test.saw

@@ -0,0 +1,55 @@
+enable_experimental;


The second test case, which does involve mutable statics. I kept this separate to avoid having to clutter the pre-/post-conditions of many specifications with extra statements involving the value of A.

RyanGlScott · 2023-11-09T16:48:10Z

src/SAWScript/Crucible/MIR/Override.hs

+-- | When a specification is used as a composition override, this function
+-- checks that the postconditions of the specification fully specify (via
+-- @mir_points_to@ statements) the values of all local mutable allocations
+-- (which are declared in the preconditions via @mir_alloc_mut@) and all
+-- mutable static items. If not, this function will raise an appropriate error
+-- message. See @Note [MIR compositional verification and mutable allocations]@.
+checkMutableAllocPostconds ::
+  Options ->
+  SharedContext ->
+  MIRCrucibleContext ->
+  CrucibleMethodSpecIR ->
+  OverrideMatcher MIR md ()


A key function that checks if compositional MIR overrides are well-formed with respect to mutable allocations. This is the part of the implementation that is the most interesting, as it isn't simply cargo-culted from the LLVM backend.

RyanGlScott · 2023-11-09T16:48:47Z

src/SAWScript/Crucible/MIR/Override.hs

+(<<>>) = PC.joinOrderingF
+
+{-
+Note [MIR compositional verification and mutable allocations]


A Note which describes the checkMutableAllocPostconds function at a high level.

RyanGlScott · 2023-11-10T00:54:37Z

Sadly, this is still not quite right. Here is a very simple example that should work, but doesn't:

pub fn inner(_x: &mut u32) {}

pub fn outer(x: &mut u32) {
    inner(x)
}

enable_experimental;

impl_mir <- mir_load_module "test.linked-mir.json";

let inner_spec = do {
    x <- mir_fresh_var "x" mir_u32;
    r <- mir_alloc_mut mir_u32;
    mir_points_to r (mir_term x);

    mir_execute_func [r];

    mir_points_to r (mir_term x);
};

let outer_spec = do {
    x <- mir_fresh_var "y" mir_u32;
    r <- mir_alloc_mut mir_u32;
    mir_points_to r (mir_term x);

    mir_execute_func [r];

    mir_points_to r (mir_term x);
};

inner_ov <- mir_verify impl_mir "test::inner" []         false inner_spec z3;
outer_ov <- mir_verify impl_mir "test::outer" [inner_ov] false outer_spec z3;

Shockingly, this fails with:

$ saw test.saw



[00:54:13.728] Loading file "/home/ryanscott/Documents/Hacking/SAW/test.saw"
[00:54:13.731] Verifying test/5600d078::inner[0] ...
[00:54:13.740] Simulating test/5600d078::inner[0] ...
[00:54:13.740] Checking proof obligations test/5600d078::inner[0] ...
[00:54:13.740] Proof succeeded! test/5600d078::inner[0]
[00:54:13.741] Verifying test/5600d078::outer[0] ...
[00:54:13.749] Simulating test/5600d078::outer[0] ...
[00:54:13.749] Matching 1 overrides of  test/5600d078::inner[0] ...
[00:54:13.749] Branching on 1 override variants of test/5600d078::inner[0] ...
[00:54:13.749] Applied override! test/5600d078::inner[0]
[00:54:13.750] Checking proof obligations test/5600d078::outer[0] ...
[00:54:13.763] Subgoal failed: test/5600d078::outer[0] Literal equality postcondition

[00:54:13.763] SolverStats {solverStatsSolvers = fromList ["SBV->Z3"], solverStatsGoalSize = 170}
[00:54:13.763] ----------Counterexample----------
[00:54:13.763]   x: 4294965247
[00:54:13.763]   y: 2048
[00:54:13.763] Stack trace:
"mir_verify" (/home/ryanscott/Documents/Hacking/SAW/test.saw:26:13-26:23)
Proof failed.

Marking as a draft until I get to the bottom of this.

RyanGlScott · 2023-11-16T21:23:17Z

That bug has been fixed, so this is ready for a final review.

This will prove useful in a subsequent commit where we add support for overrides in MIR, which make use of this `ConditionMetadata`.

These will need to be accessible from `SAWScript.Crucible.MIR.ResolveSetupValue` in a subsequent patch.

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.

spernsteiner

Looks good to me, aside from the soundness question about interior mutability, which may be better left to a separate PR (we may need to improve mir-json so it exports some additional information).

doc/manual/manual.md

src/SAWScript/Crucible/MIR/Override.hs

intTests/test_mir_unsafe_assume_spec_statics/test.rs

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.

This was referenced Oct 13, 2023

Support ghost values in all language backends #1958

Merged

Add mir_alloc_static_mut and mir_initialize_static_mut commands #1960

Closed

Support Rust verification in SAW via crucible-mir #1859

Closed

RyanGlScott force-pushed the T1859-mir_unsafe_assume_spec-take-4 branch from b1a4a16 to 3a12af7 Compare October 16, 2023 19:07

RyanGlScott force-pushed the T1859-mir_unsafe_assume_spec-take-4 branch 2 times, most recently from 043b62d to a3635f4 Compare November 9, 2023 16:42

RyanGlScott changed the title ~~Draft: mir_unsafe_assume_spec~~ mir_unsafe_assume_spec Nov 9, 2023

RyanGlScott marked this pull request as ready for review November 9, 2023 16:43

RyanGlScott requested review from qsctr and spernsteiner November 9, 2023 16:44

RyanGlScott commented Nov 9, 2023

View reviewed changes

RyanGlScott marked this pull request as draft November 10, 2023 00:54

RyanGlScott mentioned this pull request Nov 13, 2023

MIR: Add mir_alloc_static command to better track mutable statics #1982

Open

RyanGlScott force-pushed the T1859-mir_unsafe_assume_spec-take-4 branch from a3635f4 to d65c4f2 Compare November 16, 2023 21:21

RyanGlScott marked this pull request as ready for review November 16, 2023 21:23

RyanGlScott force-pushed the T1859-mir_unsafe_assume_spec-take-4 branch 2 times, most recently from f4ff18c to ff7bf47 Compare November 20, 2023 20:53

RyanGlScott added 4 commits November 22, 2023 15:10

Add maConditionMetadata to MirAllocSpec

0a6be48

This will prove useful in a subsequent commit where we add support for overrides in MIR, which make use of this `ConditionMetadata`.

Refactor: Move checkCompatibleTys, readMaybeType, firstPointsToReferent

6234628

These will need to be accessible from `SAWScript.Crucible.MIR.ResolveSetupValue` in a subsequent patch.

Use ppMIRVal in mkStructuralMismatch

69f0dc5

RyanGlScott force-pushed the T1859-mir_unsafe_assume_spec-take-4 branch from ff7bf47 to 02db0d5 Compare November 22, 2023 20:11

spernsteiner approved these changes Nov 22, 2023

View reviewed changes

doc/manual/manual.md Outdated Show resolved Hide resolved

doc/manual/manual.md Outdated Show resolved Hide resolved

src/SAWScript/Crucible/MIR/Override.hs Outdated Show resolved Hide resolved

intTests/test_mir_unsafe_assume_spec_statics/test.rs Show resolved Hide resolved

RyanGlScott force-pushed the T1859-mir_unsafe_assume_spec-take-4 branch from 02db0d5 to ac46b5b Compare November 22, 2023 22:38

RyanGlScott added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label Nov 22, 2023

mergify bot merged commit b002a93 into master Nov 22, 2023
40 checks passed

mergify bot deleted the T1859-mir_unsafe_assume_spec-take-4 branch November 22, 2023 23:38

RyanGlScott mentioned this pull request Dec 6, 2023

Start a SAW Rust verification tutorial #1939

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

`mir_unsafe_assume_spec` #1959

`mir_unsafe_assume_spec` #1959

RyanGlScott commented Oct 13, 2023 •

edited

Loading

RyanGlScott left a comment

RyanGlScott Nov 9, 2023

RyanGlScott Nov 9, 2023

RyanGlScott Nov 9, 2023

RyanGlScott Nov 9, 2023

RyanGlScott Nov 9, 2023

RyanGlScott commented Nov 10, 2023

RyanGlScott commented Nov 16, 2023

spernsteiner left a comment

mir_unsafe_assume_spec #1959

mir_unsafe_assume_spec #1959

Conversation

RyanGlScott commented Oct 13, 2023 • edited Loading

RyanGlScott left a comment

Choose a reason for hiding this comment

RyanGlScott Nov 9, 2023

Choose a reason for hiding this comment

RyanGlScott Nov 9, 2023

Choose a reason for hiding this comment

RyanGlScott Nov 9, 2023

Choose a reason for hiding this comment

RyanGlScott Nov 9, 2023

Choose a reason for hiding this comment

RyanGlScott Nov 9, 2023

Choose a reason for hiding this comment

RyanGlScott commented Nov 10, 2023

RyanGlScott commented Nov 16, 2023

spernsteiner left a comment

Choose a reason for hiding this comment

`mir_unsafe_assume_spec` #1959

`mir_unsafe_assume_spec` #1959

RyanGlScott commented Oct 13, 2023 •

edited

Loading