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

[chathhorn-galois]

Don't require slice backing allocations to be the same size when checking slices for compatibility with compositional overrides in the MIR backend.

Fixes #2620

[RyanGlScott]

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]

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

[RyanGlScott]

What other issues are you encountering?

[chathhorn-galois]

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]

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]

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]

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

[chathhorn-galois]

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]

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.