Add annotation support for trait methods and verify that implementations satisfy them

[coeff-aij]

This feature allows users to annotate trait methods with predicates. The Thrust verifies that the concrete implementations of those methods and their associated predicates satisfy the annotations given in trait.

• Example
  The specification for A::double() is expressed through the annotations on Double::double().
  The method refers to the predicate Double::is_double(), whose concrete implementation is provided by A::is_double().

// A is represented as Tuple<Int> in SMT-LIB2 format.
struct A {
    x: i64,
}

trait Double {
    // Support annotations in trait definitions
    #[thrust::predicate]
    fn is_double(self, doubled: Self) -> bool;

    // This annotations are applied to all implementors of the `Double` trait.
    #[thrust::requires(true)]
    #[thrust::ensures(is_double(*self, ^self))]
    fn double(&mut self);
}

impl Double for A {
    // Write concrete definitions for predicates in `impl` blocks
    #[thrust::predicate]
    fn is_double(self, doubled: Self) -> bool {
        // (tuple_proj<Int>.0 self) is equivalent to self.x
        // self.x * 2 == doubled.x is written as following:
        "(=
            (* (tuple_proj<Int>.0 self) 2)
            (tuple_proj<Int>.0 doubled)
        )"; true
    }

    // Check if this method complies with annotations in
    // trait definition.
    fn double(&mut self) {
        self.x += self.x;
    }
}

[coeff-aij]

We can't create new instance of Analyzer for method definitions in trait because they don't appear in MIR. I have extended the self.extract_*_annot() so that they can analyze any definitions not only the one identified by self.local_def_id. This implementation works, but it could be refactored for a clearer architecture.

[coord-e]

I have extended the self.extract_*_annot() so that they can analyze any definitions not only the one identified by self.local_def_id. This implementation works, but it could be refactored for a clearer architecture.

Cool, could you move these extract_*_annot() functions that take DefId to analyze::Analyzer? I'm putting utilities that need tcx and aren't bound to crates, local defs, or basic blocks into analyze::Analyzer.

[coeff-aij]

We also need to verify that every predicate implementation defined in a trait is annotated with the #[thrust::predicate] attribute. (But I will postpone the implementation of this check for now.)

[coeff-aij]

I've addressed your review comments.

[coord-e]

thank you!