Closed sauclovian-g closed 1 week ago
The error message arises from here in crucible-mir
:
refRootEq _sym (Const_RefRoot _ _) (Const_RefRoot _ _) =
leafAbort $ Unsupported callStack $ "Cannot compare Const_RefRoots"
Next steps: figure out which Const_RefRoot
s are being compared and why.
Some printf debugging reveals the following:
refRootEq
originates from the use of equalRefsPred
here in enforceDisjointness
. enforceDisjointness
is used to assert that all memory allocations matched by an override's precondition are disjoint.Const_RefRoot
values both originate here in crucible-mir
. Specifically, the are born in the code that translates constant string slice values to Crucible."count"
and "last_incr"
. It's not yet clear to me how these values in particular end up in the allocations in the preconditions of the map_unpack_to_slice
override (do these originate from the Rust code or on the SAW side?), but that might be a good place to start in minimizing this example further.Those are the names of the fields in the custom struct type. They are getting stringized by the Rust macros that drive that stuff.
One possible next step is to write a smaller Rust program that uses string constants directly to call map_unpack_to_slice, but I think that probably isn't going to tell us anything new. I think we're going to need to figure out how to be able to tell if these are disjoint. From what I understand so far, that's something of a can of worms because we don't carry around the info we need for that. (Also, what happens if the field names are "ounce" and "pounce" and the rust compiler decides to do prefix compression on string constants, so that they aren't properly speaking disjoint?)
While I haven't yet produced a minimal program that produces the same error message as above, I have produced a minimal program (which should be accepted, but SAW currently rejects) that has the same root cause in enforceDisjointness
. See https://github.com/GaloisInc/saw-script/issues/2064. It would be worth looking more into this issue, as I expect that any insights we gain there would apply equally to this issue.
This is fixed, and the fix will be in the pending SAW release.
The spec for
map_unpack_to_slice
(which is required for custom_types) fails with:This is AIUI in the Crucible/SAW interface.
It's probably connected somehow to using an array of string slices (since that's what's different about this function) but not necessarily.