Use the new update-field AIR support to simplify assignment though a path in AIR

[utaal]

This replaces code that takes a snapshot of the pre-state of the assignment, assumes the new value for the changed field and then assumes that all other fields (on each datatype of the path) are unchanged:

struct C {
    d: i64,
    e: u64,
}

struct B {
    c: C,
    e: u64,
}

struct A {
    b1: B,
    e: u64,
}

fn main (){
    let c1 = C{d: 3, e: 3};
    let b1 = B{c: c1, e: 3};
    let mut a = A{b1, e: 3};

    a.b1.c.d = 5;
}

  (snapshot snap%ASSIGN)
  (havoc a@)
  (assume
   (= (nestedstructs!C./C/d (%Poly%nestedstructs!C. (Poly%nestedstructs!C. (nestedstructs!B./B/c
        (%Poly%nestedstructs!B. (Poly%nestedstructs!B. (nestedstructs!A./A/b1 (%Poly%nestedstructs!A.
            (Poly%nestedstructs!A. a@)
     )))))))
    ) 5
  ))
  (assume
   (and
    (= (nestedstructs!C./C/e (nestedstructs!B./B/c (nestedstructs!A./A/b1 (old snap%ASSIGN
         a@
      )))
     ) (nestedstructs!C./C/e (nestedstructs!B./B/c (nestedstructs!A./A/b1 a@)))
    )
    (= (nestedstructs!B./B/e (nestedstructs!A./A/b1 (old snap%ASSIGN a@))) (nestedstructs!B./B/e
      (nestedstructs!A./A/b1 a@)
    ))
    (= (nestedstructs!A./A/e (old snap%ASSIGN a@)) (nestedstructs!A./A/e a@))
))

All this can be replaced with a single assignment using update-field:

(assign a@ ((_ update-field nestedstructs!A./A/?b1) (%Poly%nestedstructs!A. (Poly%nestedstructs!A. a@))
  ((_ update-field nestedstructs!B./B/?c) (%Poly%nestedstructs!B. (Poly%nestedstructs!B.
       (nestedstructs!A./A/b1 (%Poly%nestedstructs!A. (Poly%nestedstructs!A. a@)))
      )
     ) ((_ update-field nestedstructs!C./C/?d) (%Poly%nestedstructs!C. (Poly%nestedstructs!C.
        (nestedstructs!B./B/c (%Poly%nestedstructs!B. (Poly%nestedstructs!B. (nestedstructs!A./A/b1
            (%Poly%nestedstructs!A. (Poly%nestedstructs!A. a@))
       )))))
      ) 5
))))

This was primarily developed by @tim-rohde.

[Chris-Hawblitzel]

Overall, it looks good. I just have a few changes that I've requested.

[Chris-Hawblitzel]

maybe "datatype type" instead of "struct type"?

[Chris-Hawblitzel]

These look like copies of tests from other test files. If the tests are already in some other place, we don't have to have a second copy here. For refactoring an existing feature (like field update) for which tests already exist, we don't necessarily have to have a new test file.

[Chris-Hawblitzel]

If possible, I'd like to see boxing/unboxing coercions inserted by poly.rs rather than by sst_to_air.rs. The ongoing monomorphize branch, for example, would have to add special cases to sst_to_air.rs whenever sst_to_air.rs performs boxing/unboxing operations directly, whereas everything in poly.rs will automatically be skipped by monomorphize.