Full marker trait support for improved contract flexibility

[f4z3r]

This PR introduces (near) full support for marker trait invariants:

#[invariant="self.d1 == self.d2"]
trait Foo {}

The above defines a trait invariant signaling the type implementing the trait should have two
comparable fields d1 and d2, and those should be equal.

This is fully type checked:

struct Dummy<T> {
    d1: T,
    d2: T,
}

impl<T> Foo for Dummy<T> { }

// ==>
// error[E0369]: binary operation `==` cannot be applied to type `T`
//  --> prusti/tests/verify/pass/marker-traits/generic-advanced.rs:5:14
//   |
// 5 | #[invariant="self.d1 == self.d2"]
//   |              ^^^^^^^^^^^^^^^^^^
//   |
//   = note: `T` might need a bound for `std::cmp::PartialEq`

Moreover, any unrecognised marker attribute on traits is reported (only checked if trait is
used/implemented):

#[requires="self.d1 == self.d2"]
trait Foo {}

// ==>
// error: only invariant allowed for traits
//  --> prusti/tests/verify/pass/marker-traits/generic-advanced.rs:6:7
//   |
// 6 | trait Foo {}
//   |       ^^^
// 

Finally, support for generics is granted:

#[invariant="self.d1 == self.d2"]
trait Foo {}

struct Dummy<T> {
    d1: T,
    d2: T,
}

impl Foo for Dummy<i32> { }

fn test_dummy(d: &Dummy<i32>) {
    assert!(d.d1 == d.d2);
}
// ==>
// verifies

Issues

There is still an issue in the encoding of types for generics:

#[invariant="self.d1 == self.d2"]
trait Foo {}

struct Dummy<T> {
    d1: T,
    d2: T,
}

impl<T> Foo for Dummy<T> where T: PartialEq { }

fn test_dummy(d: &Dummy<i32>) {
    assert!(d.d1 == d.d2);
}

The snippet above creates valid Rust code on the first parser pass and properly creates the
invariant only for the required type. However, this panics at runtime during the encoding of the
type bounds:

...
 INFO 2020-06-05T21:43:06Z: prusti_viper::verifier: Received 2 items to be verified:
 INFO 2020-06-05T21:43:06Z: prusti_viper::verifier:  - generic::test_dummy from prusti/tests/verify/pass/marker-traits/generic.rs:13:1: 15:2 (generic::test_dummy[0])
 INFO 2020-06-05T21:43:06Z: prusti_viper::verifier:  - generic::main from prusti/tests/verify/pass/marker-traits/generic.rs:17:1: 17:14 (generic::main[0])
 INFO 2020-06-05T21:43:06Z: prusti_viper::encoder::encoder: Encoding: generic::test_dummy from prusti/tests/verify/pass/marker-traits/generic.rs:13:1: 15:2 (generic::test_dummy[0])
thread 'main' panicked at 'internal error: entered unreachable code', prusti-viper/src/encoder/foldunfold/branch_ctxt.rs:839:41
note: Run with `RUST_BACKTRACE=1` for a backtrace.

error: internal compiler error: unexpected panic

note: the compiler or Prusti unexpectedly panicked.

note: possible reasons include the usage of Rust features that are not supported by Prusti.

note: we would appreciate a bug report for Prusti: <https://github.com/viperproject/prusti-dev/issues>

note: Prusti hash d47b8909e40c1b57eb3 built on 2020-06-05 21:31:56

note: rustc <unknown> running on x86_64-unknown-linux-gnu

[fpoli]

The "internal error: entered unreachable code" panic that you observed might be caused by some other component. Do you have an intuition of what the bug is? I would be fine with merging this PR and opening a separate issue to debug that panic.

Before merging, could you just add one or two negative test cases in the fail/ folder?

[f4z3r]

The "internal error: entered unreachable code" panic that you observed might be caused by some other component. Do you have an intuition of what the bug is? I would be fine with merging this PR and opening a separate issue to debug that panic.

Before merging, could you just add one or two negative test cases in the fail/ folder?

Yes the error is caused by the viper type encoding. I had a look into the problem for a couple of hours last Friday but did not find the issue. It is related with generic encoding for sure, as similar examples that do not use generics as extensively run fine.

I will add the examples in a second.