Skip to content

MIR: relax requirement that slice backing allocations must be the same size when applying overrides #3070

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

Draft
chathhorn-galois wants to merge 7 commits into
base: master
Choose a base branch
from
Draft

MIR: relax requirement that slice backing allocations must be the same size when applying overrides #3070

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
e528298
intTests: add some missing .gitignores.
chathhorn-galois Feb 25, 2026
3ac148a
MIR: don't require slice backing allocs to be equal size when matchin…
chathhorn-galois Feb 25, 2026
b17c110
intTests: add missing Makefiles.
chathhorn-galois Feb 26, 2026
62c9b76
Mir override matching: fix issue with slices.
chathhorn-galois Mar 19, 2026
1d06288
Mir override matching: another slices test.
chathhorn-galois Mar 19, 2026
7272e25
Mir override matching: fix issue with offsets.
chathhorn-galois Mar 23, 2026
585b0ec
Mir override matching: fix MirSetupSliceRange case
chathhorn-galois Mar 23, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions intTests/test2242_2243/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
all: ;
clean:
sh ./test.sh clean

.PHONY: all clean
3 changes: 3 additions & 0 deletions intTests/test2301/.gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
*.rawlog
*.log
*.diff
Comment thread
RyanGlScott marked this conversation as resolved.
5 changes: 5 additions & 0 deletions intTests/test2301/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
all: ;
clean:
sh ./test.sh clean

.PHONY: all clean
2 changes: 2 additions & 0 deletions intTests/test2620/.gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
libtest.rlib
libtest.mir
2 changes: 2 additions & 0 deletions intTests/test2620/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
MIR_SRCS=test
include ../support/mir-blobs.mk
1 change: 1 addition & 0 deletions intTests/test2620/test.linked-mir.json
View file
Open in desktop

Large diffs are not rendered by default.

9 changes: 9 additions & 0 deletions intTests/test2620/test.linked-mir.json.FROM
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
versions
rustc 1.91.0-nightly (02c7b1a7a 2025-09-13)
mir-json 0.1.0 (JSON schema version 9)
Rust toolchain nightly-2025-09-14
mir-json mtime: Mar 18 15:26:04 2026
mir-json version from cargo: mir-json v0.1.0
probable mir-json commit: 71700ee8a69e1b7d84f4eed7cbd43373b29d4373 from Tue Mar 17 13:41:39 2026 and/or Tue Mar 17 13:41:39 2026
versions-notes
Generated by update-from.sh version 1
19 changes: 19 additions & 0 deletions intTests/test2620/test.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
fn f(_: &[u8]) {}

pub fn g(a: [u8; 2]) {
f(&a)
}

pub fn h(a: [u8; 5]) {
f(&a[0..2])
}

pub fn i(a: [u8; 5]) {
f(&a[3..5])
}

fn f_u32(_: &[u32]) {}

pub fn h_u32(a: [u32; 5]) {
f_u32(&a[0..2])
}
52 changes: 52 additions & 0 deletions intTests/test2620/test.saw
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,52 @@
enable_experimental;

let f_spec = do {
a_array <- mir_fresh_var "a_array" (mir_array 2 mir_u8);
a_ref <- mir_ref_of (mir_term a_array);
mir_execute_func [mir_slice_value a_ref];
};

let f_spec_len3 = do {
a_array <- mir_fresh_var "a_array" (mir_array 3 mir_u8);
a_ref <- mir_ref_of (mir_term a_array);
mir_execute_func [mir_slice_value a_ref];
};

let g_spec = do {
a_array <- mir_fresh_var "a_array" (mir_array 2 mir_u8);
mir_execute_func [mir_term a_array];
};

let h_spec = do {
a_array <- mir_fresh_var "a_array" (mir_array 5 mir_u8);
mir_execute_func [mir_term a_array];
};

let i_spec = do {
a_array <- mir_fresh_var "a_array" (mir_array 5 mir_u8);
mir_execute_func [mir_term a_array];
};

let f_u32_spec = do {
a_array <- mir_fresh_var "a_array" (mir_array 2 mir_u32);
a_ref <- mir_ref_of (mir_term a_array);
mir_execute_func [mir_slice_value a_ref];
};

let h_u32_spec = do {
a_array <- mir_fresh_var "a_array" (mir_array 5 mir_u32);
mir_execute_func [mir_term a_array];
};

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

f_ov <- mir_verify m "test::f" [] false f_spec z3;
mir_verify m "test::g" [f_ov] false g_spec z3;
mir_verify m "test::h" [f_ov] false h_spec z3;
mir_verify m "test::i" [f_ov] false i_spec z3;

f_u32_ov <- mir_verify m "test::f_u32" [] false f_u32_spec z3;
mir_verify m "test::h_u32" [f_u32_ov] false h_u32_spec z3;

f_ov_len3 <- mir_verify m "test::f" [] false f_spec_len3 z3;
fails (mir_verify m "test::h" [f_ov_len3] false h_spec z3);
3 changes: 3 additions & 0 deletions intTests/test2620/test.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
#!/bin/sh
SAW=${SAW:-saw}
${SAW} test.saw
3 changes: 3 additions & 0 deletions intTests/test2780/.gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
*.rawlog
*.log
*.diff
5 changes: 5 additions & 0 deletions intTests/test2780/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
all: ;
clean:
sh ./test.sh clean

.PHONY: all clean
5 changes: 5 additions & 0 deletions intTests/test2843/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
all: ;
clean:
sh ./test.sh clean

.PHONY: all clean
5 changes: 5 additions & 0 deletions intTests/test2939/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
all: ;
clean:
sh ./test.sh clean

.PHONY: all clean
3 changes: 3 additions & 0 deletions intTests/test_beta_reduce_term/.gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
*.rawlog
*.log
*.diff
3 changes: 3 additions & 0 deletions intTests/test_sawcore_type_errors/.gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
*.rawlog
*.log
*.diff
2 changes: 2 additions & 0 deletions intTests/test_yosys_cells/.gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
test.ys
test.log
5 changes: 3 additions & 2 deletions saw-central/src/SAWCentral/Crucible/MIR/Override.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2148,8 +2148,9 @@ valueToSC sym fail_ tval (MIRVal shp val) =
-- TypeShape might differ from the actual length of the RegValue, so we
-- need to check both.
| toInteger len == n
, length (Mir.mirAggregate_entries sym val) == fromIntegral len
-> do terms <- accessMirAggregateArray sym elemSz elemShp len val $
, length (Mir.mirAggregate_entries sym val) >= fromIntegral len
-> do let agg = Mir.resizeMirAggregate val $ fromIntegral len * elemSz

@RyanGlScott RyanGlScott Mar 18, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I like the way this new implementation (which only reads from the slice's backing array without overwriting its original contents) much better.

That being said, I think there is at least one case that this won't cover. Consider this example:

// test.rs

// PRECONDITION: `a` must have at least two elements.
fn f(a: &[u8]) -> (u8, u8) {
    (a[0], a[1])
}

pub fn g1(a: [u8; 5]) -> (u8, u8) {
    f(&a[0..2])
}

pub fn g2(a: [u8; 5]) -> (u8, u8) {
    f(&a)
}

g1 and g2 are very nearly the same function, except that while g1 only passes a subrange of the slice &a (the length of which is 2), g2 passes the entirety of the slice (the length of which is 5). It shouldn't really matter either way, as in either case, the length of the slice is long enough to support accessing elements at indexes 0 and 1. Despite this, SAW only half supports this example: it can use f as a compositional override when proving g1, but not when proving g2:

// test.saw

enable_experimental;

let f_spec = do {
    a_array <- mir_fresh_var "a_array" (mir_array 2 mir_u8);
    a_ref <- mir_ref_of (mir_term a_array);
    mir_execute_func [mir_slice_value a_ref];
    mir_return (mir_term {{ (a_array @ 0, a_array @ 1) }});
};

let g_spec = do {
    a_array <- mir_fresh_var "a_array" (mir_array 5 mir_u8);
    mir_execute_func [mir_term a_array];
    mir_return (mir_term {{ (a_array @ 0, a_array @ 1) }});
};

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

f_ov <- mir_verify m "test::f" [] false f_spec z3;
mir_verify m "test::g1" [f_ov] false g_spec z3;
mir_verify m "test::g2" [f_ov] false g_spec z3;

$ ./bin/saw test.saw
Loading file "test.saw"
Verifying test/2bbe2722::f[0] ...
Simulating test/2bbe2722::f[0] ...
Checking proof obligations test/2bbe2722::f[0] ...
Proof succeeded! test/2bbe2722::f[0]
Verifying test/2bbe2722::g1[0] ...
Simulating test/2bbe2722::g1[0] ...
Matching 1 overrides of  test/2bbe2722::f[0] ...
Branching on 1 override variants of test/2bbe2722::f[0] ...
Applied override! test/2bbe2722::f[0]
Checking proof obligations test/2bbe2722::g1[0] ...
Proof succeeded! test/2bbe2722::g1[0]
Verifying test/2bbe2722::g2[0] ...
Simulating test/2bbe2722::g2[0] ...
Matching 1 overrides of  test/2bbe2722::f[0] ...
Stack trace:
   (builtin) in mir_verify
   test.saw:22:1-22:47 (at top level)
Symbolic execution failed.
Abort due to assertion failure:
  test.rs:13:5: 13:10: error: in test/2bbe2722::g2[0]
  All overrides failed during structural matching:
  *  Name: test/2bbe2722::f[0]
     Location: test.saw:20:1
     Argument types:
     - &[u8]
     Return type: (u8, u8)
     Arguments:
     - <slice>
     at test.saw:20:1:
     Could not match specified value with actual value:
       actual (simulator) value: <slice>
       specified value:          @AllocIndex 0[..]
       type of actual value:     &[u8]
       type of specified value: &[u8]

I suspect that we will need to relax some of the checks around slice lengths in matchArg in order to make the g2 example work.

@chathhorn-galois chathhorn-galois Mar 19, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think I fixed this, but there are still other issues...

@RyanGlScott RyanGlScott Mar 19, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What other issues are you encountering?

@chathhorn-galois chathhorn-galois Mar 19, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I just pushed two more (failing) tests -- do they make sense to you or am I misunderstanding something about how this is supposed to work?

@RyanGlScott RyanGlScott Mar 19, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, thank you for providing an example. To shrink the example a bit, we have:

// test.rs

// PRECONDITION: `a` must have at least two elements.
fn tup(a: &[u8]) -> (u8, u8) {
    (a[0], a[1])
}

pub fn g3(a: [u8; 5]) -> (u8, u8) {
    tup(&a[1..3])
}

We would expect to be able to use tup as a compositional override in g3.

// test.saw

enable_experimental;

let tup_spec = do {
    a_array <- mir_fresh_var "a_array" (mir_array 2 mir_u8);
    a_ref <- mir_ref_of (mir_term a_array);
    mir_execute_func [mir_slice_value a_ref];
    mir_return (mir_term {{ (a_array @ 0, a_array @ 1) }});
};

let g3_spec = do {
    a_array <- mir_fresh_var "a_array" (mir_array 5 mir_u8);
    mir_execute_func [mir_term a_array];
    mir_return (mir_term {{ (a_array @ 1, a_array @ 2) }});
};

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

tup_ov <- mir_verify m "test::tup" [] false tup_spec z3;
mir_verify m "test::g3" [tup_ov] false g3_spec z3;

And yet, SAW fails to verify g3 this way:

$ ./bin/saw test.saw
Loading file "test.saw"
Verifying test/938f56ff::tup[0] ...
Simulating test/938f56ff::tup[0] ...
Checking proof obligations test/938f56ff::tup[0] ...
Proof succeeded! test/938f56ff::tup[0]
Verifying test/938f56ff::g3[0] ...
Simulating test/938f56ff::g3[0] ...
Matching 1 overrides of  test/938f56ff::tup[0] ...
Branching on 1 override variants of test/938f56ff::tup[0] ...
Applied override! test/938f56ff::tup[0]
Checking proof obligations test/938f56ff::g3[0] ...
Subgoal failed: test/938f56ff::g3[0] Literal equality postcondition
Expected term:
let { x`1 = seq (TCNum 8) Bool;
      x`2 = TCNum 5;
    }
 in ( ecAt x`2 x`1 Integer PIntegralInteger a_array`5947
        (ecNumber (TCNum 1) Integer PLiteralInteger)
    , ecAt x`2 x`1 Integer PIntegralInteger a_array`5947
        (ecNumber (TCNum 2) Integer PLiteralInteger) )
Actual term:
let { x`1 = seq (TCNum 8) Bool;
      x`2 = TCNum 2;
      x`3 = [at 5 x`1 a_array`5947 0, at 5 x`1 a_array`5947 1];
      x`4 = ( ecAt x`2 x`1 Integer PIntegralInteger x`3
                (ecNumber (TCNum 0) Integer PLiteralInteger)
      , ecAt x`2 x`1 Integer PIntegralInteger x`3
          (ecNumber (TCNum 1) Integer PLiteralInteger) );
    }
 in (x`4.0, x`4.1)

SolverStats {solverStatsSolvers = fromList ["SBV->Z3"], solverStatsGoalSize = 117}
----------Counterexample----------
  a_array: [8, 247, 8, 0, 0]
Stack trace:
   (builtin) in z3
   test.saw:21:48-21:50 in (callback)
   (builtin) in mir_verify
   test.saw:21:1-21:50 (at top level)
Proof failed.

I think what is happening here is that when matching the tup override against the call to tup(&a[1..3]) in g3, SAW is mistakenly using a's backing array starting at offset 0, not offset 1. That is, it is retrieving the first and second elements from a's backing array, whereas we actually want it to retrieve the second and third element. This is why you can unsoundly verify g3 using this erroneous spec:

let g_spec = do {
    a_array <- mir_fresh_var "a_array" (mir_array 5 mir_u8);
    mir_execute_func [mir_term a_array];
    mir_return (mir_term {{ (a_array @ 0, a_array @ 1) }});
};

// Unsound!
mir_verify m "test::g3" [tup_ov] false g_spec z3;

To make this work, I think we will need to modify the MirSetupSliceRange case in matchArg. Specifically, I think we need to add an offset to the slice's pointer field equal to the starting offset in the range. (This is similar to how the LLVM backend's llvm_field and llvm_elem command work, which also apply an offset to a pointer before matching on it.)

@RyanGlScott RyanGlScott Mar 19, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Er, slight clarification: the MirSetupSliceRange case is probably not involved, given that none of the specs make use of mir_slice_range_value. Still, I strongly suspect that a pointer offset is not getting applied somewhere it should be—we should narrow down where that is.

@chathhorn-galois chathhorn-galois Mar 19, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah, the MirSetupSliceRange is definitely another case that needs to be tested, though.

@chathhorn-galois chathhorn-galois Mar 23, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here's another approach that seems to work: create a new reference to a properly-sized backing allocation at the correct offset via mirAggregate_split.

edit: blegh, nevermind!

@RyanGlScott RyanGlScott Mar 24, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm less convinced that this is a good idea. The problem is that mkSlicedRef will now always create a fresh memory allocation that is disjoint from the original slice's backing allocation. This can cause SAW to incorrectly conclude that pointers are unequal when they should actually be equal. (The test failure in test2064 may be a symptom of this.)

Instead of resizing the MirAggregate of the slice's backing array, how about we take the slice's pointer and apply the corresponding offset (what you call actualStartBV in this PR) using mirRef_offsetMA? This should preserve the original allocation, and it would probably be less work overall.

terms <- accessMirAggregateArray sym elemSz elemShp len agg $
\_off val' -> valueToSC sym fail_ cryty (MIRVal elemShp val')
t <- shapeToTerm sc elemShp
liftIO (scVectorReduced sc t terms)
Expand Down
Loading