Unsizing for trait objects

[rgwohlbold]

PR #149 implements trait objects as opaque types in Viper. However, to pass references to trait objects to functions, these are unsized before being borrowed, which is currently not supported:

trait MyTrait {}

struct S { x: i32 }

impl MyTrait for S {}

fn consume(_v: &dyn MyTrait) {}

#[ensures(result == 42)]
fn function() -> i32 {
    let s = S { x: 42 };
    consume(&s); // unsizing &S -> &dyn MyTrait happens here
    s.x
}

The handler in MirBuiltinEnc::handle_unsize currently only supports unsizing from arrays/slices to slices and panics on everything else. This PR enables unsizing of structs to trait objects and trait objects to themselves: Given a struct MyStruct that implements Trait MyTrait, this PR allows for unsizing &MyStruct -> &dyn MyTrait (as well as the &mut versions). It also allows for unsizing &dyn MyTrait -> &dyn MyTrait (as well as the mut versions) which happens in functions which take &dyn MyTrait and pass it into other functions.

Since trait objects are opaque, no postconditions about their content are encoded.

Supporting this unsizing has the effect of enabling significant standard library functionality, like #[derive(Debug)], making the following snippet not crash anymore:

use prusti_contracts::*;

#[derive(Debug)]
struct S {
    x: i32,
}

fn main() {
    let s = S { x: 42 };
}

TODO

I would like to add a test case with &mut dyn MyTrait. However, I get an error "verification error could not be backtranslated". However, this error also occurs outside of test cases that have to do with this PR, so it's maybe unrelated?

[Aurel300]

I would like to add a test case with &mut dyn MyTrait. However, I get an error "verification error could not be backtranslated". However, this error also occurs outside of test cases that have to do with this PR, so it's maybe unrelated?

This might still be an issue with your encoding (or something related to mutrefs in the testcase?) -- Prusti is simply saying that Viper returned an error, but we did not expect that error to happen (i.e., it is not an error that can be back-translated to the violation of a particular assertion or contract). Usually, I see these errors say there is a permission error in a precondition. What does Viper actually report? Does the generated vpr file make sense and is the error something that comes from your encoding?

[rgwohlbold]

So there are multiple problems here:

• First, the function signature fn consume(&mut dyn MyTrait) desugars to fn(&'a mut (dyn MyTrait + 'a)) which has two lifetime annotations. This makes PCG create self-edges a0↓'a -> a0↓'a (one per position, so two overall) as well as cross-edges a0↓0 -> a0↓1 and a0↓1 -> a0↓0. This results in the following wand being created:

  ensures (let wand_result ==
      (p_0_Tuple_snap(_0p)) in
      acc(p_Param(old(p_Ref_mutable_snap(_1p, s_Dyn_type())).s_Ref_mutable_0,
      s_Dyn_type()), write) --*
      acc(p_Param(old(p_Ref_mutable_snap(_1p, s_Dyn_type())).s_Ref_mutable_0,
      s_Dyn_type()), write))

This can be fixed by patching PCG to only create edges when input != output (not sure if this is fully right though)

• After patching PCG, Viper brings up an error on the undo_unsize call: There might be insufficient permission to access p_Ref_mutable(old[_before_0_11](_3p), s_Dyn_type()). This is since undo_unsize has

requires acc(p_Ref_mutable(dst, s_Dyn_type()), write)
requires acc(p_Param(p_Ref_mutable_snap(dst, s_Dyn_type()).s_Ref_mutable_0, s_Dyn_type()), write)

but m_consume only returns ensures acc(p_Param(old(p_Ref_mutable_snap(_1p, s_Dyn_type())).s_Ref_mutable_0, s_Dyn_type()), write). This could in principle be fixed by adding ensures acc(p_Ref_mutable(_1p, T), write) and a snap equality postcondition for each &mut T argument in the generated Viper method signature, but I'm a bit hesitant to change it since I don't fully understand it yet.

• Since the first argument to consume actually contains two lifetimes, PCG creates two edges when processing the unsize coercion, and undo_unsize is called twice. Even when patching the other two issues, the second call to undo_unsize doesn't have enough permissions. I guess we should deduplicate these edges somewhere in the code?

[rgwohlbold]

The second of these points is actually also the case when unsizing arrays to slices, and mutably borrowing them. Unlike tait objects, these only have one lifetime parameter. Example:

fn consume(v: &mut [i32]) {
}

fn main() {
    let mut arr = [1, 2, 3];
    consume(&mut arr);
}

The precondition of method mir_undo_unsize_$amp$$sq$$qm$6$sp$mut$sp$$lb$i32$sc$$sp$3_usize$rb$_to_$amp$$sq$$qm$5$sp$mut$sp$$lb$i32$rb$ might not hold. There might be insufficient permission to access p_Ref_mutable(old[_before_0_11](_3p), s_Slice_type(s_Int_i32_type()))

[rgwohlbold]

• The first point is fixed by the changes in fn_wand.rs, skipping wand creation when the wand would be an identity, like P --* P
• The second point is fixed by Insert a p_Ref_mutable assign before an undo_unsize for mutable references #162
• Edge deduplication is done by keeping track of the (src_place, dst_place) tuples in the ImpureEncVisitor and only emitting one undo_unsize

[rgwohlbold]

In principle, this PR is ready to review. It does depend on #162, so we should merge that one first.

[rgwohlbold]

Since #162 is now merged, this PR is ready for review