Support mutably borrowing fields.

stainless_extraction/src/expr/field.rs

@@ -9,7 +9,12 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> {
     rhs: &'a Expr<'a, 'tcx>,
   ) -> st::Expr<'l> {
     let f = self.factory();
-    let value = self.extract_expr(rhs);
+
+    // Assigning creates an alias of the rhs, therefore the rhs needs to be
+    // potentially fresh copied. Fresh copies are not inserted for MutCells i.e.
+    // mutable references. For other types it's safe to fresh copy because rustc
+    // ensures that we own the value we assign.
+    let value = self.extract_aliasable_expr(rhs);
     let lhs = self.strip_scopes(lhs);
     match &lhs.kind {
       ExprKind::VarRef { id } => f.Assignment(self.fetch_var(*id), value).into(),
@@ -44,7 +49,12 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> {
     }
   }
 
-  pub(super) fn extract_field(&mut self, lhs: &'a Expr<'a, 'tcx>, field: Field) -> st::Expr<'l> {
+  pub(super) fn extract_field(
+    &mut self,
+    lhs: &'a Expr<'a, 'tcx>,
+    field: Field,
+    mutable_borrow: bool,
+  ) -> st::Expr<'l> {
     let f = self.factory();
     match lhs.ty.kind() {
       TyKind::Tuple(_) => {
@@ -55,9 +65,12 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> {
       TyKind::Adt(adt_def, _) => {
         let selector = self.extract_field_selector(adt_def.did, field);
         let lhs = self.extract_expr(lhs);
-        self
-          .synth()
-          .mut_cell_value(f.ADTSelector(lhs, selector).into())
+        let field = f.ADTSelector(lhs, selector).into();
+        if mutable_borrow {
+          field
+        } else {
+          self.synth().mut_cell_value(field)
+        }
       }
 
       ref kind => unexpected(

stainless_extraction/src/expr/mod.rs

@@ -35,7 +35,7 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> {
       ExprKind::LogicalOp { op, lhs, rhs } => self.extract_logical_op(*op, lhs, rhs),
 
       ExprKind::Tuple { fields } => self.extract_tuple(fields, expr.span),
-      ExprKind::Field { lhs, name } => self.extract_field(lhs, *name),
+      ExprKind::Field { lhs, name } => self.extract_field(lhs, *name, false),
       ExprKind::VarRef { id } => self.extract_var_ref(*id),
 
       ExprKind::Call { ty, ref args, .. } => match ty.kind() {

stainless_extraction/src/expr/refs.rs

@@ -30,6 +30,8 @@ impl<'a, 'l, 'tcx> BodyExtractor<'a, 'l, 'tcx> {
           // Re-borrows a dereferenced mutable borrow, we take the original ref
           ExprKind::Deref { arg: inner } if is_mut_ref(inner.ty) => self.extract_expr(inner),
 
+          ExprKind::Field { lhs, name } => self.extract_field(lhs, name, true),
+
           ExprKind::VarRef { id } => self.fetch_var(id).into(),
           _ => self.extract_expr(arg),
         }