crux-mir-comp: Panic when clobbering static of type closure [] (traverseMirAggregate: mismatched keys in aggregate) #2687
Description
The following (heavily minimized) program causes crux-mir-comp to panic:
// test.rs
extern crate crucible;
extern crate crucible_proc_macros;
use crucible::crucible_assert;
use crucible_proc_macros::crux_spec_for;
pub fn wat() -> u32 {
(|| 42u32)()
}
#[crux_spec_for(wat)]
pub fn wat_equiv() {
let expected = 42u32;
let actual = wat();
crucible_assert!(expected == actual);
}$ cabal -v0 run exe:crux-mir-comp -- test.rs
You have encountered a bug in saw-central's implementation.
*** Please create an issue at https://github.com/GaloisInc/saw-script/issues
%< ---------------------------------------------------
Revision: 8dbf5f331
Branch: T2596-mir_exact_adt
Location: traverseMirAggregate
Message: mismatched keys in aggregate
CallStack (from HasCallStack):
panic, called at saw-support/src/SAWSupport/PanicSupport.hs:133:3 in saw-1.4.0.99-inplace-saw-support:SAWSupport.PanicSupport
doPanic, called at saw-central/src/SAWCentral/Panic.hs:20:19 in saw-1.4.0.99-inplace-saw-central:SAWCentral.Panic
panic, called at saw-central/src/SAWCentral/Crucible/MIR/TypeShape.hs:590:12 in saw-1.4.0.99-inplace-saw-central:SAWCentral.Crucible.MIR.TypeShape
%< ---------------------------------------------------
test test/7e18d5ec::wat_equiv[0]:
My hunch is that this is a result of the crux_spec_for macro clobbering static items under the hood. Passing --print-mir to crux-mir-comp reveals the following static items:
$ cabal -v0 run exe:crux-mir-comp -- test.rs --print-mir
<snip>
STATICS
False crucible/4180b7fd::{{alloc}}[21] : [u8; 79] = ""not implemented: MethodSpecBuilder is not supported on this version of crux-mir""
False crucible/4180b7fd::{{alloc}}[22] : [&str; 1] = [ &crucible/4180b7fd::{{alloc}}[21] ]
False test/7e18d5ec::{{alloc}}[0] : [u8; 18] = ""expected == actual""
False test/7e18d5ec::{{alloc}}[1] : [u8; 7] = ""test.rs""
False test/7e18d5ec::{{alloc}}[2] : closure [] = closure[]
Of those, only test/7e18d5ec::{{alloc}}[2] : closure [] looks like something that would be cause traverseMirAggregate to be called, as I believe that Rust closures are represented the same way that tuples are in crucible-mir.