Open Torrencem opened 1 month ago
RyanGlScott
commented
1 month ago Interestingly, I am not able to reproduce this locally on my x86_64-unknown-linux-gnu machine, which leads me to wonder if this issue is platform-specific. (I note that you're using aarch64-apple-darwin.) Would you be able to upload your hello.linked-mir.json file somewhere?
Torrencem
commented
1 month ago Here's the mir json (fair warning, it's 11mb): https://gist.github.com/Torrencem/2da86154e1a6ae7304bd6bc90ad92e53
RyanGlScott
commented
1 month ago @mccleeary-galois (who also uses aarch64-apple-darwin) is also able to reproduce this issue.
Torrencem
commented
1 month ago It's funny, as we were discussing this issue, the first thing we said was "this better not be an aarch64-apple-darwin issue again"
RyanGlScott
commented
1 month ago Thank you for uploading your MIR JSON file! This was invaluable in figuring out what is going on.
First, a general disclaimer: I doubt that SAW will be able to verify code that contains calls to println!, even if we fixed this bug. As such, I'd recommend removing calls to println! in any Rust code that you want to verify (at least, for the time being).
That being said, you're not actually verifying the main() function here—you're just loading it into SAW. Loading Rust code into SAW should never crash, so we should strive to make at least this much work. Here are some takeaways:
Thankfully, nothing's wrong on your end. This is a bug in how SAW ingests MIR JSON files.
The fact that this bug seemingly only arose on aarch64-apple-darwin is a bit of a red herring. That's simply because there's some code in the std crate which happens to use different implementations depending on what operating system is used, and it just so happens that the macOS implementation triggers this bug, but the Linux implementation doesn't.
Thankfully, it proves relatively straightforward to extract the code which triggers the bug into a minimal form that crashes on all operating systems:
// test.rs
pub fn foo(f: &dyn Fn(i32)) {
f(42)
}
pub fn bar() {
foo(&|_| ())
}// test.saw
enable_experimental;
m <- mir_load_module "test.linked-mir.json";$ saw-rustc test.rs && ~/Software/saw-1.1/bin/saw test.saw
test build - extract output path - ["rustc", "test.rs", "--test", "--target", "x86_64-unknown-linux-gnu", "--cfg", "crux"]
test build - ["rustc", "test.rs", "--target", "x86_64-unknown-linux-gnu", "--cfg", "crux", "--cfg", "crux_top_level", "--crate-type", "rlib"]
note: Emitting MIR for test/801036f2::bar
note: Emitting MIR for test/801036f2::bar::{{promoted}}[0]
note: Emitting MIR for test/801036f2::foo
note: Emitting trait def for Some(dyn std::ops::Fn(i32))
note: Emitting MIR for test/801036f2::bar::{closure#0}::_insta56a8199f5bc040a[0]
note: Emitting MIR for core/73237d41::ops::function::FnOnce::call_once::_callonce194a5c55a7e36159[0]
linking 1 mir files into test.linked-mir.json
inputs: libtest.mir
generated test script test
[13:10:27.920] Loading file "/home/ryanscott/Documents/Hacking/Haskell/sandbox/saw-script/test.saw"
[13:10:27.922] vtable signature mismatch for vtable core/73237d41::ops[0]::function[0]::Fn[0]::_vtbl87c30a95762061ee[0] of trait core/73237d41::ops[0]::function[0]::Fn[0]::_traitb9ec75e8d3618d41[0] : StructRepr [FunctionHandleRepr [AnyRepr, StructRepr [MaybeRepr (BVRepr 32)]] UnitRepr, FunctionHandleRepr [AnyRepr, BVRepr 32] UnitRepr, FunctionHandleRepr [AnyRepr, BVRepr 32] UnitRepr] != StructRepr [FunctionHandleRepr [AnyRepr, StructRepr [MaybeRepr (BVRepr 32)]] UnitRepr, FunctionHandleRepr [AnyRepr, StructRepr [MaybeRepr (BVRepr 32)]] UnitRepr, FunctionHandleRepr [AnyRepr, StructRepr [MaybeRepr (BVRepr 32)]] UnitRepr]
CallStack (from HasCallStack):
error, called at src/Mir/Trans.hs:980:20 in crucible-mir-0.2-inplace:Mir.Trans
mkTraitObject, called at src/Mir/Trans.hs:823:11 in crucible-mir-0.2-inplace:Mir.Trans
evalCast', called at src/Mir/Trans.hs:954:5 in crucible-mir-0.2-inplace:Mir.Trans
evalCast, called at src/Mir/Trans.hs:1011:30 in crucible-mir-0.2-inplace:Mir.Trans
evalRval, called at src/Mir/Trans.hs:1246:11 in crucible-mir-0.2-inplace:Mir.Trans
transStatement, called at src/Mir/Trans.hs:1712:68 in crucible-mir-0.2-inplace:Mir.Trans
translateBlockBody, called at src/Mir/Trans.hs:1721:28 in crucible-mir-0.2-inplace:Mir.Trans
registerBlock, called at src/Mir/Trans.hs:1761:10 in crucible-mir-0.2-inplace:Mir.Trans
genFn, called at src/Mir/Trans.hs:1807:24 in crucible-mir-0.2-inplace:Mir.Trans
transDefine, called at src/Mir/Trans.hs:2264:30 in crucible-mir-0.2-inplace:Mir.Trans
transCollection, called at src/Mir/ParseTranslate.hs:76:26 in crucible-mir-0.2-inplace:Mir.ParseTranslate
translateMIR, called at src/SAWScript/Crucible/MIR/Builtins.hs:528:11 in saw-script-1.1-inplace:SAWScript.Crucible.MIR.BuiltinsI haven't made it as far as identifying the actual cause of the underlying bug, but it appears that crucible-mir is improperly constructing the types of vtable shims. Note that you can also reproduce this bug using crux-mir (after annotating bar as a crux-mir test entrypoint):
// test.rs
pub fn foo(f: &dyn Fn(i32)) {
f(42)
}
#[crux::test]
pub fn bar() {
foo(&|_| ())
}$ crux-mir test.rs
vtable signature mismatch for vtable core/092bc89a::ops[0]::function[0]::Fn[0]::_vtbl437dbfe18b7afdbd[0] of trait core/092bc89a::ops[0]::function[0]::Fn[0]::_trait82b5b5831af5fcf4[0] : StructRepr [FunctionHandleRepr [AnyRepr, StructRepr [MaybeRepr (BVRepr 32)]] UnitRepr, FunctionHandleRepr [AnyRepr, BVRepr 32] UnitRepr, FunctionHandleRepr [AnyRepr, BVRepr 32] UnitRepr] != StructRepr [FunctionHandleRepr [AnyRepr, StructRepr [MaybeRepr (BVRepr 32)]] UnitRepr, FunctionHandleRepr [AnyRepr, StructRepr [MaybeRepr (BVRepr 32)]] UnitRepr, FunctionHandleRepr [AnyRepr, StructRepr [MaybeRepr (BVRepr 32)]] UnitRepr]
CallStack (from HasCallStack):
error, called at src/Mir/Trans.hs:980:20 in crucible-mir-0.2-inplace:Mir.Trans
mkTraitObject, called at src/Mir/Trans.hs:823:11 in crucible-mir-0.2-inplace:Mir.Trans
evalCast', called at src/Mir/Trans.hs:954:5 in crucible-mir-0.2-inplace:Mir.Trans
evalCast, called at src/Mir/Trans.hs:1011:30 in crucible-mir-0.2-inplace:Mir.Trans
evalRval, called at src/Mir/Trans.hs:1246:11 in crucible-mir-0.2-inplace:Mir.Trans
transStatement, called at src/Mir/Trans.hs:1712:68 in crucible-mir-0.2-inplace:Mir.Trans
translateBlockBody, called at src/Mir/Trans.hs:1721:28 in crucible-mir-0.2-inplace:Mir.Trans
registerBlock, called at src/Mir/Trans.hs:1761:10 in crucible-mir-0.2-inplace:Mir.Trans
genFn, called at src/Mir/Trans.hs:1807:24 in crucible-mir-0.2-inplace:Mir.Trans
transDefine, called at src/Mir/Trans.hs:2264:30 in crucible-mir-0.2-inplace:Mir.Trans
transCollection, called at src/Mir/ParseTranslate.hs:76:26 in crucible-mir-0.2-inplace:Mir.ParseTranslate
translateMIR, called at src/Mir/Language.hs:256:16 in crux-mir-0.8.0.99-inplace:Mir.LanguageAs such, this is really more of a crucible-mir issue than a SAW one. I'll move this issue over to the Crucible repo and retitle it accordingly.
RyanGlScott
commented
1 month ago @spernsteiner reminded me that the culprit is the spread_arg hack:
More specifically, suppose we have this program:
// test.rs
pub fn foo(f: &mut dyn FnMut(i16, i32)) {
f(27, 42)
}
#[crux::test]
pub fn bar() {
foo(&mut |_, _| ())
}If I dump out the internal representation of the FnMut instantiation in the program above (using mir-json), I get:
"traits": [
{
"items": [
{
"item_id": "core/092bc89a::ops::function::FnOnce::call_once",
"kind": "Method",
"signature": {
"abi": {
"kind": "RustCall"
},
"inputs": [
"ty::Dynamic::985de022e3d83671",
"ty::Tuple::05f82569127efd62"
],
"output": "ty::Tuple::e93222e871854c41"
}
},
{
"item_id": "core/092bc89a::ops::function::FnMut::call_mut",
"kind": "Method",
"signature": {
"abi": {
"kind": "RustCall"
},
"inputs": [
"ty::Ref::0751798588f5ec27",
"ty::Tuple::05f82569127efd62"
],
"output": "ty::Tuple::e93222e871854c41"
}
}
],
"name": "core/092bc89a::ops::function::FnMut::_traite54ca09db4b501ca[0]"
}
]Here, we see that both call_once and call_mut expect a Tuple argument, which corresponds to the pair (i16, i32). So far, so good.
If I look up the vtable used in this program, I see this:
"vtables": [
{
"items": [
{
"def_id": "core/092bc89a::ops::function::FnOnce::call_once::_callonce95ae10fa377a8068[0]",
"item_id": "core/092bc89a::ops::function::FnOnce::call_once"
},
{
"def_id": "test/7578cddf::bar::{closure#0}::_inst4da6783bb0bc5290[0]",
"item_id": "test/7578cddf::bar::{closure#0}"
}
],
"name": "core/092bc89a::ops::function::FnMut::_vtbl421e8f554162ba11[0]",
"trait_id": "core/092bc89a::ops::function::FnMut::_traite54ca09db4b501ca[0]"
}
]What is peculiar is the type of test/7578cddf::bar::{closure#0}::_inst4da6783bb0bc5290[0] used as the second item in the vtable:
{
...,
"args": [
{
"is_zst": false,
"mut": {
"kind": "Mut"
},
"name": "_1",
"ty": "ty::Ref::fcca228e69df3496"
},
{
"is_zst": false,
"mut": {
"kind": "Mut"
},
"name": "_2",
"ty": "ty::i16"
},
{
"is_zst": false,
"mut": {
"kind": "Mut"
},
"name": "_3",
"ty": "ty::i32"
}
],
...,
"name": "test/7578cddf::bar::{closure#0}::_inst4da6783bb0bc5290[0]",
"return_ty": "ty::Tuple::e93222e871854c41",
"spread_arg": null
}Unlike call_mut above, this doesn't take a Tuple as an argument. Instead it "unpacks" the tuple, having separate i16 and i32 arguments. This is the root cause of the vtable signature mismatch error reported earlier.
The unpacking (or lack thereof) is related to crucible-mir's hacky treatment of spread_arg in MIR. As the comment above indicates, the current hack works for direct calls to Fn-like things, but not function pointers. In order to make this work, we will likely need to remove the hack and do the right thing.
I've installed saw and
mir-jsonon my system, and I think I have the right version of everything set up.(kind of weird version is panicking but you can see the rustc version is correct in there)
When I try to compile the following:
it works fine, I'm able to handle it with the following saw script:
then I run
saw-rustc, which succeedswhen I run saw on this, it succeeds, telling me my installation is at least somewhat working:
however, if I then try a more complicated function that uses IO, like the following:
I can compile this with
saw-rustc:(and I can provide this mir file if it might be useful). When I run
saw hello.saw(same saw file) again for this example I getAny troubleshooting tips / suggestions? is my installation borked or is something else wrong with the way I'm doing things