Add support for symbolic values containing mutable borrows

[sonmarcho]

Content

This PR adds proper support for symbolic values containing mutable borrows. This is a first step towards generalising the way the symbolic execution handles borrows, for instance to support nested borrows. In particular, this PR adds support for types like [&'a mut T; 32], and enumerations containing borrows.

We currently don't properly support instantiating functions with type parameters containing (mutable) borrows: I leave this as future work. In the meantime, I hacked support for instantiating Box::new with types containing borrows because this is really necessary to support interesting examples - I believe this can be generalised without too much work to an interesting class of functions.

I still need to update the join operation to properly support those generalised symbolic values, but the good news is that as of today it is not necessary (because for instance when computing loops fixed points we rarely join two enumerations with different variants). In particular, I was able to (finally!) update the code of the hashmap so that the get and get_mut functions now return options, instead of panicking if the key could not be found.

Translation Examples

Consider the following mutable list type and its pop function:

enum MutList<'a, T> {
    Nil,
    Cons(&'a mut T, Box<MutList<'a, T>>),
}

impl<'a, T> MutList<'a, T> {
    pub fn pop(self) -> (&'a mut T, Self) {
        use MutList::*;
        match self {
            Nil => panic!(),
            Cons(hd, tl) => (hd, *tl),
        }
    }
}

The generated model is as follows:

inductive MutList (T : Type) :=
| Nil : MutList T
| Cons : T → MutList T → MutList T

def MutList.pop
  {T : Type} (self : MutList T) :
  Result ((T × (MutList T)) × ((T × (MutList T)) → MutList T))
  :=
  match self with
  | MutList.Nil => Result.fail .panic
  | MutList.Cons hd tl =>
    let back := fun ret => let (t, ml) := ret
                           MutList.Cons t ml
    Result.ok ((hd, tl), back)

The push function is more subtle:

impl<'a, T> MutList<'a, T> {
    pub fn push(self, x: &'a mut T) -> Self {
        MutList::Cons(x, Box::new(self))
    }
}

In the push function, the backward function needs to deconstruct the list to retrieve the head and the tail. In case the consumed value doesn't have the variant Cons (which should not happen if the backward function is properly used) we should fail, but I don't like the idea of having fallible backward functions, so rather we just use dummy values instead (in practice, I'm using the original values of the borrows):

def MutList.push
  {T : Type} (self : MutList T) (x : T) :
  Result ((MutList T) × (MutList T → ((MutList T) × T)))
  :=
  let back :=
    fun ret =>
      let (x1, ml) :=
        match ret with
        | MutList.Cons t ml1 => (t, ml1)
        | _ => (x, self) -- this shouldn't happen: we use dummy values
      (ml, x1)
  Result.ok (MutList.Cons x self, back)