LLVM/MIR: Use the same pretty-printer consistently in structural mismatch errors

[RyanGlScott]

This should minimize some spurious differences in expected/actual when displaying structural mismatch errors arising from overrides. Still not perfect by any means, but an improvement nonetheless.

[RyanGlScott]

Alas, this isn't as easy as I thought it would be. Three test cases fail with panics of the form:

Matching 1 overrides of  test/ad8922ea::f[0] ...
You have encountered a bug in saw-central's implementation.
*** Please create an issue at https://github.com/GaloisInc/saw-script/issues

%< --------------------------------------------------- 
  Revision:  4db4794
  Branch:    (HEAD detached at pull/3261/merge)
  Location:  MIRSetup (in lookupAllocIndex)
  Message:   Unresolved prestate variable: AllocIndex 0
CallStack (from HasCallStack):
  panic, called at saw-support/src/SAWSupport/PanicSupport.hs:137:3 in saw-1.5.0.99-inplace-saw-support:SAWSupport.PanicSupport
  doPanic, called at saw-central/src/SAWCentral/Panic.hs:20:19 in saw-1.5.0.99-inplace-saw-central:SAWCentral.Panic
  panic, called at saw-central/src/SAWCentral/Crucible/MIR/ResolveSetupValue.hs:611:9 in saw-1.5.0.99-inplace-saw-central:SAWCentral.Crucible.MIR.ResolveSetupValue
%< --------------------------------------------------- 

I'll mark this as a draft for now, as I'm not sure what is causing this.

[sauclovian-g]

It looks at least plausible that it might be linked to mir_ref_of, but I haven't really looked for serious yet.

[brianhuffman]

Are the panics happening within the calls to resolveSetupValueLLVM and resolveSetupValueMIR that you added?

[RyanGlScott]

Yes, the calls to resolveSetupValue{LLVM,MIR} are almost certainly involved in some way. I haven't figured out exactly why they're relevant, however.

For what it's worth, nothing about mir_ref_of is essential to triggering the panic, as the following variant of test3096 also triggers the same panic:

// test.rs
pub fn f(_p: &i32, _q: &i32) {}

pub fn g() {
    let x: i32 = 1;
    let y: i32 = 2;
    f(&x, &y);
    let xs = [1, 2, 3];
    f(&xs[0], &xs[1]);
}

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

let f_spec = do {
    x <- mir_fresh_var "x" mir_i32;
    p <- mir_alloc mir_i32;
    mir_points_to p (mir_term x);
    y <- mir_fresh_var "y" mir_i32;
    q <- mir_alloc mir_i32;
    mir_points_to q (mir_term y);
    mir_execute_func [p, q];
};

let f_array_spec = do {
    xs <- mir_fresh_var "xs" (mir_array 3 mir_i32);
    p <- mir_alloc (mir_array 3 mir_i32);
    mir_points_to p (mir_term xs);
    mir_execute_func [mir_elem_ref p 0, mir_elem_ref p 1];
};

let g_spec = mir_execute_func [];

f_ov <- mir_verify m "test::f" [] false f_spec z3;
f_array_ov <- mir_verify m "test::f" [] false f_array_spec z3;
mir_verify m "test::g" [f_ov, f_array_ov] false g_spec z3;

[RyanGlScott]

Interestingly, if I translate this program into something equivalent-looking in C:

// test.c
#include <stdint.h>

void f(int32_t* p, int32_t* q) {}

void g(void) {
    int32_t x = 1;
    int32_t y = 2;
    f(&x, &y);
    int32_t xs[3] = {1, 2, 3};
    f(&xs[0], &xs[1]);
}

// test.saw
m <- llvm_load_module "test.bc";

let f_spec = do {
    x <- llvm_fresh_var "x" (llvm_int 32);
    p <- llvm_alloc (llvm_int 32);
    llvm_points_to p (llvm_term x);
    y <- llvm_fresh_var "y" (llvm_int 32);
    q <- llvm_alloc (llvm_int 32);
    llvm_points_to q (llvm_term y);
    llvm_execute_func [p, q];
};

let f_array_spec = do {
    xs <- llvm_fresh_var "xs" (llvm_array 3 (llvm_int 32));
    p <- llvm_alloc (llvm_array 3 (llvm_int 32));
    llvm_points_to p (llvm_term xs);
    llvm_execute_func [llvm_elem p 0, llvm_elem p 1];
};

let g_spec = llvm_execute_func [];

f_ov <- llvm_verify m "f" [] false f_spec z3;
f_array_ov <- llvm_verify m "f" [] false f_array_spec z3;
llvm_verify m "g" [f_ov, f_array_ov] false g_spec z3;

Then SAW does not panic. The plot thickens.

[RyanGlScott]

I think this comes down to the fact that SAW has more checks for mir_elem_ref than the corresponding checks for llvm_elem, and as a result, SAW can fail to apply an override involving mir_elem_ref before it ever has a chance to perform the bookkeeping needed for resolveSetupValueMIR to work.

To explain what I mean in a bit more detail, consider the override machinery that runs when you attempt to match an override that uses mir_elem_ref as an argument:

saw-script/saw-central/src/SAWCentral/Crucible/MIR/Override.hs

Lines 1338 to 1365 in adfe651

	-- match reference SetupElem by getting the reference to the
	-- containing aggregate
	(MirIndexIntoRef, []) ->
	case actual of
	MIRVal (RefShape elemRefTy elemTy elemMutbl _elemTpr) elemRef -> do
	arrRefTy <- typeOfSetupValue cc tyenv nameEnv z
	case tyToShape col arrRefTy of
	Some arrRefShp@(RefShape _
	(Mir.TyArray elemTy' _)
	arrMutbl
	Mir.MirAggregateRepr)
	| tyToPtrKind elemRefTy == tyToPtrKind arrRefTy
	, checkCompatibleTys elemTy elemTy'
	, elemMutbl == arrMutbl -> do
	let elemSize = tySize col elemTy
	-- get the reference to the containing aggregate and the
	-- index of the current reference within it
	Ctx.Empty Ctx.:> Crucible.RV arrRef
	Ctx.:> Crucible.RV i'_sym <-
	tryMirOperation $ Mir.mirRef_peelIndexMA bak iTypes elemRef elemSize
	-- the index should be concrete
	case fromInteger . BV.asUnsigned <$> W4.asBV i'_sym of
	Just i'
	-- make sure the expected and actual indices match
	| i == i' ->
	go inCast [] (MIRVal arrRefShp arrRef) z
	_ -> fail_
	_ -> fail_

The recursive call to go is what establishes that the reference which mir_elem_ref offsets into has a corresponding AllocIndex. The Unresolved prestate variable message in the panic above also mentions an AllocIndex, which it expects to find, but does not. This happens because something is calling resolveSetupValueMIR (which transitively invokes lookupAllocIndex) before the recursive call to go.

As it turns out, this is caused by the call to tryMirOperation . mirRef_peelIndexMA before go. mirRef_peelIndexMA is a fallible memory model operation, and if it does fail, then SAW will immediately prepare the error message that would be displayed should no other override match successfully. As part of preparing this error message, it calls resolveSetupValueMIR, but since the bookkeeping done by the recursive call to go hasn't yet happened, this results in the catastrophic panic seen above.

Contrast this with the LLVM-oriented override machinery for llvm_elem:

saw-script/saw-central/src/SAWCentral/Crucible/LLVM/Override.hs

Lines 1204 to 1210 in adfe651

	(Crucible.LLVMValInt blk off, _, SetupElem () v i) | Crucible.isPointerMemType expectedTy ->
	do let tyenv = MS.csAllocations cs
	nameEnv = MS.csTypeNames cs
	delta <- llvmExceptToFail sc $ resolveSetupElemOffset cc tyenv nameEnv v i
	off' <- liftIO $ W4.bvSub sym off
	=<< W4.bvLit sym (W4.bvWidth off) (Crucible.bytesToBV (W4.bvWidth off) delta)
	matchArg opts sc cc cs prepost md (Crucible.LLVMValInt blk off') expectedTy v

llvm_elem just translates to computing a numeric offset, which can't really fail in the same way that mirRef_peelIndexMA can. As such, the recursive call (to matchArg this time) always occurs, even if the offset pointer doesn't end up matching.

I don't yet have a bright idea for how to fix things on the MIR side, but I wanted to record this while it was fresh on my mind.