Implement Enums

[tillarnold]

• Add support for enums to new prusti
  • Pure (snapshots)
  • Impure (predicates)
  • I refactored mk_structlike to extract the different parts into functions that I then reuse for mk_enum
• Implement mir::TerminatorKind::FalseEdge by treating it like a goto
• Implement promoted constants
• Change the triggers for the tuple/struct read axioms from s_Tuple_read_1(s_Tuple_cons(f0, f1)) to s_Tuple_cons(f0, f1). We discussed this change on the 20st of October in chat and you determined that this is the correct trigger. This used to be Change the triggers for the tuple and struct read axioms #20 but because I refactored that code here I include this change here as it is needed for enums to work anyways.
• Implement Terminator repacks. These were needed for this to work.
• I introduced some mk_* functions in the context.rs but I did not rewrite any other code to use these yet to make merging easier

(Replaces #17)

[tillarnold]

@JonasAlaif this is getting close to ready but i have some unresolved questions:

1. TypeData::Int now has a bitwidth. What should i use there for the enum discriminant functions?
2. I introduces a new PureKind::Constant in the pure encoder for promoted constants. it that ok or should i reuse an existing kind?
3. here I stop the reification for the unevaluated constant. Is that the correct thing to do?
4. I filled out the fields for TypeEncoderOutputRefSubEnum and as a result i'm not sure what the values for the never type should be here (Not sure if that just an issue for me but since this links to the typ.rs file and that is collapsed in the github diff view i need to manually expand that first for to see the line of code im referring too)
5. I changed this to handle signed integers too but i suspect this was limited to unsigned for a reason?

[JonasAlaif]

1. Use: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/adt/struct.AdtDef.html#method.discriminants (or if you look at the sorce of that, as you should, then maybe you can take the code from here and here to get .repr().discr_type().to_ty(tcx))
2. Looks good, but put the mir::Primoted inside this variant (instead of the Option it's currently in
3. What do you mean you stop reification? At that point you shouldn't be creating a Lazy thing at all imo, just do expr.reify(...) there with empty args no?
4. It should work the same as an empty enum, I'll take a look at this when I review the PR
5. Are you sure that you get the correct results for signed integers... the input is just a 128 bit sequence, I doubt it's correct to simply interpret that as a u128 integer for signed (e.g. you can never get negative values)

[JonasAlaif]

@Aurel300 this is a different PR from when you reviewed it last, you probably want to take a look again. The biggest difference is that Rust types with generics are encoded as Viper domains with generics (but predicates and non-domain functions are still monomorphised and duplicated)

[Aurel300]

@JonasAlaif Mostly looks good, see comments. Tomorrow I would also like to discuss the overall architecture of the type encoder and what is going on with the type parameters.

[JonasAlaif]

Ready to be merged after the discussion tomorrow