viperproject
Limitations on structs with reference-typed fields
Hi! I have the following program and I have a question on what is and what is not supported atm:
use prusti_contracts::*;
pub struct Foo<T> {
foo: T,
}
pub struct Bar<'a> {
bar: &'a (),
}
pub struct Baz;
impl Baz {
#[trusted]
pub fn foobar(&self) -> Foo<Bar<'_>> {
unimplemented!()
}
pub fn baz(&self) {
let foobar = self.foobar();
drop(foobar); // comment this line and the error goes away
}
}
Results in an error from Prusti:
error: [Prusti: unsupported feature] access to reference-typed fields is not supported
--> src/lib.rs:17:5
|
17 | / pub fn baz(&self) {
18 | | let foobar = self.foobar();
19 | | drop(foobar); // comment this line and the error goes away
20 | | }
| |_____^
If I comment out the explicit call to drop(foobar) then Prusti compiles okay. The difference in the MIR for the program with and without the drop is just the basic block bb1 and its corresponding variables (i.e. without the drop, bb1, _4 and _5 are gone):
fn <impl at src/lib.rs:10:1: 10:9>::baz(_1: &Baz) -> () {
debug self => _1; // in scope 0 at src/lib.rs:15:16: 15:21
let mut _0: (); // return place in scope 0 at src/lib.rs:15:23: 15:23
let _2: Foo<Bar<'_>>; // in scope 0 at src/lib.rs:16:13: 16:19
let mut _3: &Baz; // in scope 0 at src/lib.rs:16:22: 16:35
let _4: (); // in scope 0 at src/lib.rs:17:9: 17:21
let mut _5: Foo<Bar<'_>>; // in scope 0 at src/lib.rs:17:14: 17:20
scope 1 {
debug foobar => _2; // in scope 1 at src/lib.rs:16:13: 16:19
}
bb0: {
_3 = _1; // scope 0 at src/lib.rs:16:22: 16:35
_2 = Baz::foobar(move _3) -> bb1; // scope 0 at src/lib.rs:16:22: 16:35
// mir::Constant
// + span: src/lib.rs:16:27: 16:33
// + literal: Const { ty: for<'a> fn(&'a Baz) -> Foo<Bar<'a>> {Baz::foobar}, val: Value(<ZST>) }
}
bb1: {
_5 = move _2; // scope 1 at src/lib.rs:17:14: 17:20
_4 = std::mem::drop::<Foo<Bar<'_>>>(move _5) -> bb2; // scope 1 at src/lib.rs:17:9: 17:21
// mir::Constant
// + span: src/lib.rs:17:9: 17:13
// + literal: Const { ty: fn(Foo<Bar<'_>>) {std::mem::drop::<Foo<Bar<'_>>>}, val: Value(<ZST>) }
}
bb2: {
return; // scope 0 at src/lib.rs:18:6: 18:6
}
}
The error message mentions access to reference-typed fields, which is technically not happening in this program due to none of the fields being reference in the Rust code nor at the MIR level. Should it be possible in Prusti to explicitly drop structs with reference typed fields? Or is the use of a struct with reference-typed fields already problematic and unsupported (for now) in this case?
Thanks!
p.s. a slight variation of the program and MIR is:
use prusti_contracts::*;
pub struct Foo<'a> {
foo: &'a (),
}
impl<'a> Drop for Foo<'a> {
fn drop(&mut self) {}
}
pub struct Bar;
impl Bar {
#[trusted]
pub fn foo(&self) -> Foo<'_> {
unimplemented!()
}
pub fn bar(&self) {
let foo = self.foo();
// drop(foo); // uncomment and we see the same error again
}
}
Although this time the MIR does show a drop call even when the explicit drop() is commented out, but without Prusti complaining about it:
fn <impl at src/lib.rs:11:1: 11:9>::baz(_1: &Bar) -> () {
debug self => _1; // in scope 0 at src/lib.rs:15:16: 15:21
let mut _0: (); // return place in scope 0 at src/lib.rs:15:23: 15:23
let _2: Foo<'_>; // in scope 0 at src/lib.rs:16:13: 16:16
let mut _3: &Bar; // in scope 0 at src/lib.rs:16:19: 16:29
scope 1 {
debug foo => _2; // in scope 1 at src/lib.rs:16:13: 16:16
}
bb0: {
_3 = _1; // scope 0 at src/lib.rs:16:19: 16:29
_2 = Bar::foo(move _3) -> bb1; // scope 0 at src/lib.rs:16:19: 16:29
// mir::Constant
// + span: src/lib.rs:16:24: 16:27
// + literal: Const { ty: for<'a> fn(&'a Bar) -> Foo<'a> {Bar::foo}, val: Value(<ZST>) }
}
bb1: {
drop(_2) -> bb2; // scope 0 at src/lib.rs:18:5: 18:6
}
bb2: {
return; // scope 0 at src/lib.rs:18:6: 18:6
}
}
Should it be possible in Prusti to explicitly drop structs with reference typed fields?
Yes. I guess the problem is with the information that Prusti gets from the borrow checker: when you use an explicit drop, it probably contains a problematic pattern that is not supported by Prusti.
