new-mut-ref: more precise analysis for mut refs with loops

[tjhance]

At present, we can't handle the following when new-mut-ref is enabled:

fn test(a: &mut u64)
    ensures *fin(a) == 5,
{   
    loop {
        *a = 5;
        return;
    }   
}   

The problem is that a gets havoc'ed by the loop, so we need a loop invariant that mut_ref_future(a) == mut_ref_future(old(a)). This is a pretty big usability problem, as well as a major backwards compatibility issue.

The problem is fundamentally similar to something like this failing:

  fn test2(mut a: (u64, u64)) -> (ret: u64)
      ensures ret == a.1
  {   
      loop {
          a.0 = 5;
          return a.1;
      }   
  }   

The problem in both cases is that our analysis for havoc'ing vars across loops works on the coarse granularity of local variables and doesn't consider individual fields.

To fix this, I enhance our analysis to compute a "HavocSet", a finer grained set of subplaces, rather than a set of local variables. This system is currently special-cased to only handle the mut-ref issue (i.e. to fix test case test) but still doesn't track fields for structs or tuples in general (i.e., we don't address test2). However, I aimed to write the new code in a generic way that could be easily extended in the future.

_{By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.}