Merge #1063

1063: Use field type from projection in encoding r=Aurel300 a=zgrannan

In `mir_encoder/mod.rs` the type from a field of a closure was taken from `upvar_tys()`. However, it appears that the field does not necessarily correspond to an upvar. In particular the included test raised an internal error because obtaining the type from `upvar_tys()` returns the type of argument to `go` (i.e. `String`), rather than the type of a value returned by the closure (a variant of `ChainRequest`.

It looks like the MIR already includes the field type in the `Field` projection, so this PR uses that instead.

Co-authored-by: Zack Grannan <[email protected]>
Co-authored-by: Aurel <[email protected]>

prusti-tests/tests/verify/fail/unsupported/closure_ref_in_return.rs

@@ -0,0 +1,27 @@
+pub enum TrackingId {
+    Static(&'static str),
+}
+
+pub struct TrackedMsgs {
+    pub msgs: u32,
+    pub tracking_id: TrackingId
+}
+
+pub enum ChainRequest {
+    SendMessagesAndWaitCheckTx {
+        tracked_msgs: TrackedMsgs
+    },
+
+    AddKey {
+        key_name: String
+    },
+}
+
+
+fn go(key_name: String) -> () {
+    || ChainRequest::AddKey { //~ ERROR access to reference-typed fields is not supported
+        key_name
+    };
+}
+
+fn main() {}

prusti-viper/src/encoder/mir_encoder/mod.rs

@@ -105,7 +105,7 @@ pub trait PlaceEncoder<'v, 'tcx: 'v> {
 
         let elem = projection.last().unwrap();
         Ok(match elem {
-            mir::ProjectionElem::Field(ref field, _) => {
+            mir::ProjectionElem::Field(ref field, proj_field_ty) => {
                 match base_ty.kind() {
                     ty::TyKind::Tuple(elems) => {
                         let field_name = format!("tuple_{}", field.index());
@@ -144,7 +144,7 @@ pub trait PlaceEncoder<'v, 'tcx: 'v> {
                             encoded_base
                         };
                         let field = &variant_def.fields[field.index()];
-                        let field_ty = field.ty(tcx, subst);
+                        let field_ty = *proj_field_ty;
                         if utils::is_reference(field_ty) {
                             return Err(EncodingError::unsupported(
                                 "access to reference-typed fields is not supported",
@@ -160,47 +160,19 @@ pub trait PlaceEncoder<'v, 'tcx: 'v> {
                         (encoded_projection, field_ty, None)
                     }
 
-                    ty::TyKind::Closure(def_id, ref closure_subst) => {
-                        debug!("def_id={:?} closure_subst {:?}", def_id, closure_subst);
-
+                    ty::TyKind::Closure(def_id, closure_subst) => {
                         let closure_subst = closure_subst.as_closure();
-                        debug!("Closure subst: {:?}", closure_subst);
-
-                        // let tcx = self.encoder().env().tcx();
-                        // let node_id = tcx.hir.as_local_node_id(def_id).unwrap();
-                        // let field_ty = closure_subst
-                        //     .upvar_tys(def_id, tcx)
-                        //     .nth(field.index())
-                        //     .unwrap();
-                        let field_ty = closure_subst.upvar_tys().nth(field.index())
-                            .ok_or_else(|| EncodingError::internal(format!(
-                                "failed to obtain the type of the captured path #{} of closure {:?}",
-                                field.index(),
-                                base_ty,
-                            )))?;
+                        debug!("def_id={:?} closure_subst {:?}", def_id, closure_subst);
 
+                        let field_ty = *proj_field_ty;
                         let field_name = format!("closure_{}", field.index());
                         let encoded_field = self.encoder()
                             .encode_raw_ref_field(field_name, field_ty)?;
                         let encoded_projection = encoded_base.field(encoded_field);
-
-                        // let encoded_projection: vir::Expr = tcx.with_freevars(node_id, |freevars| {
-                        //     let freevar = &freevars[field.index()];
-                        //     let field_name = format!("closure_{}", field.index());
-                        //     let encoded_field = self.encoder()
-                        //          .encode_raw_ref_field(field_name, field_ty)?;
-                        //     let res = encoded_base.field(encoded_field);
-                        //     let var_name = tcx.hir.name(freevar.var_id()).to_string();
-                        //     trace!("Field {:?} of closure corresponds to variable '{}', encoded as {}", field, var_name, res);
-                        //     res
-                        // });
-
-                        let encoded_field_type = self.encoder().encode_type(field_ty)?;
-                        // debug!("Rust closure projection {:?}", place_projection);
                         debug!("encoded_projection: {:?}", encoded_projection);
 
+                        let encoded_field_type = self.encoder().encode_type(field_ty)?;
                         assert_eq!(encoded_projection.get_type(), &encoded_field_type);
-
                         (encoded_projection, field_ty, None)
                     }