crucible-mir crashes due to improperly constructing vtable shim types
#1222
Comments
|
Interestingly, I am not able to reproduce this locally on my |
|
Here's the mir json (fair warning, it's 11mb): https://gist.github.com/Torrencem/2da86154e1a6ae7304bd6bc90ad92e53 |
|
@mccleeary-galois (who also uses |
|
It's funny, as we were discussing this issue, the first thing we said was "this better not be an |
|
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 That being said, you're not actually verifying the Your installation isn't borked.Thankfully, nothing's wrong on your end. This is a bug in how SAW ingests MIR JSON files. There's nothing inherently macOS-specific about this bug.The fact that this bug seemingly only arose on 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(&|_| ())
}What is actually going on here?I haven't made it as far as identifying the actual cause of the underlying bug, but it appears that // test.rs
pub fn foo(f: &dyn Fn(i32)) {
f(42)
}
#[crux::test]
pub fn bar() {
foo(&|_| ())
}As such, this is really more of a |
RyanGlScott
changed the title
crucible-mir crashes due to improperly constructing vtable shim types
|
@spernsteiner reminded me that the culprit is the crucible/crucible-mir/src/Mir/Mir.hs Lines 126 to 143 in 8cc5e17 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 "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 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 {
...,
"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 The unpacking (or lack thereof) is related to |
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
The text was updated successfully, but these errors were encountered: