dataflow: avoid propagating offset permissions upward from field acce…

…ss (#1031)

Pointers to structs with array fields being iterated over via `offset`
were erroneously being given `OFFSET` permissions. Those permissions
should be limited to the fields themselves. This PR introduces a new
dataflow constraint that will propagate permissions except for a
specified set. When a field projection is detected, offset permissions
are no longer propagated to the base pointer.

c2rust-analyze/src/context.rs

@@ -945,14 +945,39 @@ impl<'a, 'tcx> AnalysisCtxt<'a, 'tcx> {
         }
     }
 
+    /// Returns the [`LTy`] of an [`Rvalue`]
     pub fn type_of_rvalue(&self, rv: &Rvalue<'tcx>, loc: Location) -> LTy<'tcx> {
-        if let Some(&lty) = self.rvalue_tys.get(&loc) {
+        if let Some(lty) = self.rvalue_tys.get(&loc) {
             return lty;
         }
 
         self.derived_type_of_rvalue(rv)
     }
 
+    /// Returns a boolean indicating whether or
+    /// not the `Rvalue` is a reference or pointer containing a field projection.
+    /// For example, the following [`Rvalue`]s will satisfy that criteria:
+    /// - let r1 = std::ptr::addr_of!(x.field);
+    /// - let r2 = &x.field;
+    /// - let r3 = &(*p).field;
+    /// The following will NOT satisfy that critera:
+    /// - let r1 = x.field;
+    /// - let r2 = x.field + y;
+    pub fn has_field_projection(&self, rv: &Rvalue<'tcx>) -> bool {
+        if let Some(desc) = describe_rvalue(rv) {
+            match desc {
+                RvalueDesc::Project { proj, .. } | RvalueDesc::AddrOfLocal { proj, .. } => {
+                    for p in proj {
+                        if let PlaceElem::Field(..) = p {
+                            return true;
+                        }
+                    }
+                }
+            }
+        }
+        false
+    }
+
     /// In some cases, we can compute an `LTy` for an `Rvalue` that uses `PointerId`s derived from
     /// the `LTy`s of other value, rather than using the `PointerId`s assigned in `rvalue_tys`.
     /// For example, suppose we have this code:
@@ -1015,7 +1040,7 @@ impl<'a, 'tcx> AnalysisCtxt<'a, 'tcx> {
             }
         }
 
-        match *rv {
+        let ty = match *rv {
             Rvalue::Use(ref op) => self.type_of(op),
             Rvalue::CopyForDeref(pl) => self.type_of(pl),
             Rvalue::Repeat(ref op, _) => {
@@ -1041,7 +1066,9 @@ impl<'a, 'tcx> AnalysisCtxt<'a, 'tcx> {
             }
             Rvalue::Aggregate(ref _kind, ref _vals) => todo!("type_of Aggregate: rv = {rv:?}"),
             Rvalue::ShallowInitBox(ref _op, _ty) => todo!("type_of ShallowInitBox: rv = {rv:?}"),
-        }
+        };
+
+        ty
     }
 
     pub fn projection_lty(&self, lty: LTy<'tcx>, proj: &PlaceElem<'tcx>) -> LTy<'tcx> {

c2rust-analyze/src/dataflow/mod.rs

@@ -10,6 +10,9 @@ mod type_check;
 enum Constraint {
     /// Pointer `.0` must have a subset of the permissions of pointer `.1`.
     Subset(PointerId, PointerId),
+    /// Pointer `.0` must have a subset of permissions of pointer `.1`, except
+    /// for the provided permission set.
+    SubsetExcept(PointerId, PointerId, PermissionSet),
     /// Pointer `.0` must have all the permissions in `.1`.
     AllPerms(PointerId, PermissionSet),
     /// Pointer `.0` must not have any of the permissions in `.1`.
@@ -26,6 +29,11 @@ impl DataflowConstraints {
         self.constraints.push(Constraint::Subset(a, b));
     }
 
+    fn add_subset_except(&mut self, a: PointerId, b: PointerId, except: PermissionSet) {
+        self.constraints
+            .push(Constraint::SubsetExcept(a, b, except));
+    }
+
     fn add_all_perms(&mut self, ptr: PointerId, perms: PermissionSet) {
         self.constraints.push(Constraint::AllPerms(ptr, perms));
     }
@@ -50,11 +58,22 @@ impl DataflowConstraints {
         struct PropagatePerms;
         impl PropagateRules<PermissionSet> for PropagatePerms {
             fn subset(
+                &mut self,
+                a_ptr: PointerId,
+                a_val: &PermissionSet,
+                b_ptr: PointerId,
+                b_val: &PermissionSet,
+            ) -> (PermissionSet, PermissionSet) {
+                self.subset_except(a_ptr, a_val, b_ptr, b_val, PermissionSet::NONE)
+            }
+
+            fn subset_except(
                 &mut self,
                 _a_ptr: PointerId,
                 a_val: &PermissionSet,
                 _b_ptr: PointerId,
                 b_val: &PermissionSet,
+                except: PermissionSet,
             ) -> (PermissionSet, PermissionSet) {
                 let old_a = *a_val;
                 let old_b = *b_val;
@@ -76,8 +95,8 @@ impl DataflowConstraints {
                     | PermissionSet::FREE;
 
                 (
-                    old_a & !(!old_b & PROPAGATE_DOWN),
-                    old_b | (old_a & PROPAGATE_UP),
+                    old_a & !(!old_b & (PROPAGATE_DOWN & !except)),
+                    old_b | (old_a & (PROPAGATE_UP & !except)),
                 )
             }
 
@@ -141,6 +160,18 @@ impl DataflowConstraints {
                         xs.set(b, new_b);
                     }
 
+                    Constraint::SubsetExcept(a, b, except) => {
+                        if !xs.dirty(a) && !xs.dirty(b) {
+                            continue;
+                        }
+
+                        let old_a = xs.get(a);
+                        let old_b = xs.get(b);
+                        let (new_a, new_b) = rules.subset_except(a, old_a, b, old_b, except);
+                        xs.set(a, new_a);
+                        xs.set(b, new_b);
+                    }
+
                     Constraint::AllPerms(ptr, perms) => {
                         if !xs.dirty(ptr) {
                             continue;
@@ -216,6 +247,18 @@ impl DataflowConstraints {
                 (a_flags, b_flags)
             }
 
+            fn subset_except(
+                &mut self,
+                a_ptr: PointerId,
+                a_val: &FlagSet,
+                b_ptr: PointerId,
+                b_val: &FlagSet,
+                _except: PermissionSet,
+            ) -> (FlagSet, FlagSet) {
+                // Call original subset function
+                self.subset(a_ptr, a_val, b_ptr, b_val)
+            }
+
             fn all_perms(
                 &mut self,
                 _ptr: PointerId,
@@ -248,6 +291,9 @@ impl Constraint {
     pub fn remap_pointers(&mut self, map: PointerTable<PointerId>) {
         *self = match *self {
             Constraint::Subset(a, b) => Constraint::Subset(map[a], map[b]),
+            Constraint::SubsetExcept(a, b, perms) => {
+                Constraint::SubsetExcept(map[a], map[b], perms)
+            }
             Constraint::AllPerms(ptr, perms) => Constraint::AllPerms(map[ptr], perms),
             Constraint::NoPerms(ptr, perms) => Constraint::NoPerms(map[ptr], perms),
         };
@@ -316,6 +362,14 @@ impl<'a, T: PartialEq> TrackedPointerTable<'a, T> {
 
 trait PropagateRules<T> {
     fn subset(&mut self, a_ptr: PointerId, a_val: &T, b_ptr: PointerId, b_val: &T) -> (T, T);
+    fn subset_except(
+        &mut self,
+        a_ptr: PointerId,
+        a_val: &T,
+        b_ptr: PointerId,
+        b_val: &T,
+        except: PermissionSet,
+    ) -> (T, T);
     fn all_perms(&mut self, ptr: PointerId, perms: PermissionSet, val: &T) -> T;
     fn no_perms(&mut self, ptr: PointerId, perms: PermissionSet, val: &T) -> T;
 }

c2rust-analyze/src/dataflow/type_check.rs

@@ -52,6 +52,12 @@ impl<'tcx> TypeChecker<'tcx, '_> {
         self.constraints.add_subset(dest, src);
     }
 
+    fn add_edge_except(&mut self, src: PointerId, dest: PointerId, except: PermissionSet) {
+        // Copying `src` to `dest` can discard permissions, but can't add new ones,
+        // except for the specified exceptions.
+        self.constraints.add_subset_except(dest, src, except);
+    }
+
     fn add_equiv(&mut self, a: PointerId, b: PointerId) {
         self.equiv_constraints.push((a, b));
     }
@@ -303,6 +309,11 @@ impl<'tcx> TypeChecker<'tcx, '_> {
         self.do_equivalence_nested(pl_lty, rv_lty);
     }
 
+    fn do_assign_except(&mut self, pl_lty: LTy<'tcx>, rv_lty: LTy<'tcx>, except: PermissionSet) {
+        self.do_assign_pointer_ids_except(pl_lty.label, rv_lty.label, except);
+        self.do_equivalence_nested(pl_lty, rv_lty);
+    }
+
     /// Add a dataflow edge indicating that `rv_ptr` flows into `pl_ptr`.  If both `PointerId`s are
     /// `NONE`, this has no effect.
     fn do_assign_pointer_ids(&mut self, pl_ptr: PointerId, rv_ptr: PointerId) {
@@ -313,6 +324,19 @@ impl<'tcx> TypeChecker<'tcx, '_> {
         }
     }
 
+    fn do_assign_pointer_ids_except(
+        &mut self,
+        pl_ptr: PointerId,
+        rv_ptr: PointerId,
+        except: PermissionSet,
+    ) {
+        if pl_ptr != PointerId::NONE || rv_ptr != PointerId::NONE {
+            assert!(pl_ptr != PointerId::NONE);
+            assert!(rv_ptr != PointerId::NONE);
+            self.add_edge_except(rv_ptr, pl_ptr, except);
+        }
+    }
+
     /// Unify corresponding [`PointerId`]s in `lty1` and `lty2`.
     ///
     /// The two inputs must have identical underlying types.
@@ -361,7 +385,17 @@ impl<'tcx> TypeChecker<'tcx, '_> {
 
                 let rv_lty = self.acx.type_of_rvalue(rv, loc);
                 self.visit_rvalue(rv, rv_lty);
-                self.do_assign(pl_lty, rv_lty);
+
+                if self.acx.has_field_projection(rv) {
+                    // Fields don't get offset permissions propagated to their base pointer
+                    self.do_assign_except(
+                        pl_lty,
+                        rv_lty,
+                        PermissionSet::OFFSET_ADD | PermissionSet::OFFSET_SUB,
+                    )
+                } else {
+                    self.do_assign(pl_lty, rv_lty);
+                }
             }
             // TODO(spernsteiner): handle other `StatementKind`s
             _ => (),

c2rust-analyze/tests/filecheck/algo_md5.rs

@@ -90,7 +90,9 @@ pub unsafe extern "C" fn MD5_Init(mut context: *mut MD5_CTX) {
     (*context).state[3 as libc::c_int as usize] = 0x10325476 as libc::c_int as uint32_t;
 }
 #[no_mangle]
+// CHECK-LABEL: pub unsafe extern "C" fn MD5_Update<'h0,'h1>(
 pub unsafe extern "C" fn MD5_Update(
+    // CHECK: mut context: &'h0 mut (MD5_CTX),
     mut context: *mut MD5_CTX,
     mut _input: *const libc::c_void,
     mut inputLen: libc::c_uint,