analyze: allow overriding dataflow for specific permissions (#1088)

This adds a new internal feature for overriding dataflow analysis for
specific permissions of specific pointers. The `propagate` method of
`dataflow` now takes an additional `updates_forbidden` set, which has a
`PermissionSet` mask for every `PointerId`, and avoids adding or
removing a permission for a `ptr` if the corresponding bit is set in
`updates_forbidden[ptr]`. When `updates_forbidden` is used, the
resulting permissions after running `dataflow` might not actually
satisfy the dataflow constraints.

This is designed to support the PDG "`NON_NULL` override" feature, where
information about nullability from the PDG can override static analysis
results, though that feature is not part of the current PR.

Author: spernsteiner

c2rust-analyze/src/analyze.rs

@@ -554,6 +554,8 @@ struct FuncInfo<'tcx> {
     /// get a complete [`Assignment`] for this function, which maps every [`PointerId`] in this
     /// function to a [`PermissionSet`] and [`FlagSet`].
     lasn: MaybeUnset<LocalAssignment>,
+    /// Local part of the `updates_forbidden` mask.
+    l_updates_forbidden: MaybeUnset<LocalPointerTable<PermissionSet>>,
     /// Constraints on pointee types gathered from the body of this function.
     pointee_constraints: MaybeUnset<pointee_type::ConstraintSet<'tcx>>,
     /// Local part of pointee type sets.
@@ -872,6 +874,8 @@ fn run(tcx: TyCtxt) {
     const INITIAL_FLAGS: FlagSet = FlagSet::empty();
 
     let mut gasn = GlobalAssignment::new(gacx.num_pointers(), INITIAL_PERMS, INITIAL_FLAGS);
+    let mut g_updates_forbidden = GlobalPointerTable::new(gacx.num_pointers());
+
     for (ptr, &info) in gacx.ptr_info().iter() {
         if should_make_fixed(info) {
             gasn.flags[ptr].insert(FlagSet::FIXED);
@@ -897,6 +901,7 @@ fn run(tcx: TyCtxt) {
     for info in func_info.values_mut() {
         let num_pointers = info.acx_data.num_pointers();
         let mut lasn = LocalAssignment::new(num_pointers, INITIAL_PERMS, INITIAL_FLAGS);
+        let l_updates_forbidden = LocalPointerTable::new(num_pointers);
 
         for (ptr, &info) in info.acx_data.local_ptr_info().iter() {
             if should_make_fixed(info) {
@@ -905,6 +910,7 @@ fn run(tcx: TyCtxt) {
         }
 
         info.lasn.set(lasn);
+        info.l_updates_forbidden.set(l_updates_forbidden);
     }
 
     // Load permission info from PDG
@@ -1082,18 +1088,14 @@ fn run(tcx: TyCtxt) {
     // Run dataflow solver and borrowck analysis
     // ----------------------------------
 
-    // For testing, putting #[c2rust_analyze_test::fail_before_analysis] on a function marks it as
-    // failed at this point.
-    for &ldid in &all_fn_ldids {
-        if !util::has_test_attr(tcx, ldid, TestAttr::FailBeforeAnalysis) {
-            continue;
-        }
-        gacx.mark_fn_failed(
-            ldid.to_def_id(),
-            DontRewriteFnReason::FAKE_INVALID_FOR_TESTING,
-            PanicDetail::new("explicit fail_before_analysis for testing".to_owned()),
-        );
-    }
+    apply_test_attr_fail_before_analysis(&mut gacx, &all_fn_ldids);
+    apply_test_attr_force_non_null_args(
+        &mut gacx,
+        &all_fn_ldids,
+        &mut func_info,
+        &mut gasn,
+        &mut g_updates_forbidden,
+    );
 
     eprintln!("=== ADT Metadata ===");
     eprintln!("{:?}", gacx.adt_metadata);
@@ -1121,16 +1123,19 @@ fn run(tcx: TyCtxt) {
             let field_ltys = gacx.field_ltys.clone();
             let acx = gacx.function_context_with_data(&mir, info.acx_data.take());
             let mut asn = gasn.and(&mut info.lasn);
+            let updates_forbidden = g_updates_forbidden.and(&info.l_updates_forbidden);
 
             let r = panic_detail::catch_unwind(AssertUnwindSafe(|| {
                 // `dataflow.propagate` and `borrowck_mir` both run until the assignment converges
                 // on a fixpoint, so there's no need to do multiple iterations here.
-                info.dataflow.propagate(&mut asn.perms_mut());
+                info.dataflow
+                    .propagate(&mut asn.perms_mut(), &updates_forbidden);
 
                 borrowck::borrowck_mir(
                     &acx,
                     &info.dataflow,
                     &mut asn.perms_mut(),
+                    &updates_forbidden,
                     name.as_str(),
                     &mir,
                     field_ltys,
@@ -1818,6 +1823,57 @@ fn make_sig_fixed(gasn: &mut GlobalAssignment, lsig: &LFnSig) {
     }
 }
 
+/// For testing, putting #[c2rust_analyze_test::fail_before_analysis] on a function marks it as
+/// failed at this point.
+fn apply_test_attr_fail_before_analysis(
+    gacx: &mut GlobalAnalysisCtxt,
+    all_fn_ldids: &[LocalDefId],
+) {
+    let tcx = gacx.tcx;
+    for &ldid in all_fn_ldids {
+        if !util::has_test_attr(tcx, ldid, TestAttr::FailBeforeAnalysis) {
+            continue;
+        }
+        gacx.mark_fn_failed(
+            ldid.to_def_id(),
+            DontRewriteFnReason::FAKE_INVALID_FOR_TESTING,
+            PanicDetail::new("explicit fail_before_analysis for testing".to_owned()),
+        );
+    }
+}
+
+/// For testing, putting #[c2rust_analyze_test::force_non_null_args] on a function marks its
+/// arguments as `NON_NULL` and also adds `NON_NULL` to the `updates_forbidden` mask.
+fn apply_test_attr_force_non_null_args(
+    gacx: &mut GlobalAnalysisCtxt,
+    all_fn_ldids: &[LocalDefId],
+    func_info: &mut HashMap<LocalDefId, FuncInfo>,
+    gasn: &mut GlobalAssignment,
+    g_updates_forbidden: &mut GlobalPointerTable<PermissionSet>,
+) {
+    let tcx = gacx.tcx;
+    for &ldid in all_fn_ldids {
+        if !util::has_test_attr(tcx, ldid, TestAttr::ForceNonNullArgs) {
+            continue;
+        }
+
+        let info = func_info.get_mut(&ldid).unwrap();
+        let mut asn = gasn.and(&mut info.lasn);
+        let mut updates_forbidden = g_updates_forbidden.and_mut(&mut info.l_updates_forbidden);
+
+        let lsig = &gacx.fn_sigs[&ldid.to_def_id()];
+        for arg_lty in lsig.inputs.iter().copied() {
+            for lty in arg_lty.iter() {
+                let ptr = lty.label;
+                if !ptr.is_none() {
+                    asn.perms_mut()[ptr].insert(PermissionSet::NON_NULL);
+                    updates_forbidden[ptr].insert(PermissionSet::NON_NULL);
+                }
+            }
+        }
+    }
+}
+
 fn local_span(decl: &LocalDecl) -> Span {
     let mut span = decl.source_info.span;
     if let Some(ref info) = decl.local_info {

c2rust-analyze/src/borrowck/mod.rs

@@ -4,7 +4,7 @@ use crate::context::AdtMetadataTable;
 use crate::context::{AnalysisCtxt, PermissionSet};
 use crate::dataflow::DataflowConstraints;
 use crate::labeled_ty::{LabeledTy, LabeledTyCtxt};
-use crate::pointer_id::PointerTableMut;
+use crate::pointer_id::{PointerTable, PointerTableMut};
 use crate::util::{describe_rvalue, RvalueDesc};
 use indexmap::{IndexMap, IndexSet};
 use rustc_hir::def_id::DefId;
@@ -120,6 +120,7 @@ pub fn borrowck_mir<'tcx>(
     acx: &AnalysisCtxt<'_, 'tcx>,
     dataflow: &DataflowConstraints,
     hypothesis: &mut PointerTableMut<PermissionSet>,
+    updates_forbidden: &PointerTable<PermissionSet>,
     name: &str,
     mir: &Body<'tcx>,
     field_ltys: HashMap<DefId, context::LTy<'tcx>>,
@@ -181,7 +182,7 @@ pub fn borrowck_mir<'tcx>(
         }
 
         eprintln!("propagate");
-        changed |= dataflow.propagate(hypothesis);
+        changed |= dataflow.propagate(hypothesis, updates_forbidden);
         eprintln!("done propagating");
 
         if !changed {

c2rust-analyze/src/dataflow/mod.rs

@@ -45,7 +45,14 @@ impl DataflowConstraints {
     }
 
     /// Update the pointer permissions in `hypothesis` to satisfy these constraints.
-    pub fn propagate(&self, hypothesis: &mut PointerTableMut<PermissionSet>) -> bool {
+    ///
+    /// If `restrict_updates[ptr]` has some flags set, then those flags will be left unchanged in
+    /// `hypothesis[ptr]`.
+    pub fn propagate(
+        &self,
+        hypothesis: &mut PointerTableMut<PermissionSet>,
+        updates_forbidden: &PointerTable<PermissionSet>,
+    ) -> bool {
         eprintln!("=== propagating ===");
         eprintln!("constraints:");
         for c in &self.constraints {
@@ -118,27 +125,52 @@ impl DataflowConstraints {
             ) -> PermissionSet {
                 *val & !perms
             }
+
+            fn restrict_updates(
+                &mut self,
+                old: &PermissionSet,
+                new: &PermissionSet,
+                updates_forbidden: &PermissionSet,
+            ) -> PermissionSet {
+                let (old, new, updates_forbidden) = (*old, *new, *updates_forbidden);
+                (new & !updates_forbidden) | (old & updates_forbidden)
+            }
         }
 
-        match self.propagate_inner(hypothesis, &mut PropagatePerms) {
+        match self.propagate_inner(hypothesis, &mut PropagatePerms, Some(updates_forbidden)) {
             Ok(changed) => changed,
             Err(msg) => {
                 panic!("{}", msg);
             }
         }
     }
 
+    /// Update `xs` by propagating dataflow information of type `T` according to the constraints
+    /// recorded in `self`.
+    ///
+    /// If `updates_forbidden` is provided, then the parts of `xs` indicated by `updates_forbidden`
+    /// will not be modified.  (Specifically, all updates will be filtered through the method
+    /// `PropagateRules::restrict_updates`.)
     fn propagate_inner<T, R>(
         &self,
         xs: &mut PointerTableMut<T>,
         rules: &mut R,
+        updates_forbidden: Option<&PointerTable<T>>,
     ) -> Result<bool, String>
     where
         T: PartialEq,
         R: PropagateRules<T>,
     {
         let mut xs = TrackedPointerTable::new(xs.borrow_mut());
 
+        let restrict_updates = |rules: &mut R, ptr, old: &T, new: T| {
+            if let Some(updates_forbidden) = updates_forbidden {
+                rules.restrict_updates(old, &new, &updates_forbidden[ptr])
+            } else {
+                new
+            }
+        };
+
         let mut changed = false;
         let mut i = 0;
         loop {
@@ -157,6 +189,8 @@ impl DataflowConstraints {
                         let old_a = xs.get(a);
                         let old_b = xs.get(b);
                         let (new_a, new_b) = rules.subset(a, old_a, b, old_b);
+                        let new_a = restrict_updates(rules, a, old_a, new_a);
+                        let new_b = restrict_updates(rules, b, old_b, new_b);
                         xs.set(a, new_a);
                         xs.set(b, new_b);
                     }
@@ -169,6 +203,8 @@ impl DataflowConstraints {
                         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);
+                        let new_a = restrict_updates(rules, a, old_a, new_a);
+                        let new_b = restrict_updates(rules, b, old_b, new_b);
                         xs.set(a, new_a);
                         xs.set(b, new_b);
                     }
@@ -180,6 +216,7 @@ impl DataflowConstraints {
 
                         let old = xs.get(ptr);
                         let new = rules.all_perms(ptr, perms, old);
+                        let new = restrict_updates(rules, ptr, old, new);
                         xs.set(ptr, new);
                     }
 
@@ -190,6 +227,7 @@ impl DataflowConstraints {
 
                         let old = xs.get(ptr);
                         let new = rules.no_perms(ptr, perms, old);
+                        let new = restrict_updates(rules, ptr, old, new);
                         xs.set(ptr, new);
                     }
                 }
@@ -277,9 +315,19 @@ impl DataflowConstraints {
             ) -> FlagSet {
                 *val
             }
+
+            fn restrict_updates(
+                &mut self,
+                old: &FlagSet,
+                new: &FlagSet,
+                updates_forbidden: &FlagSet,
+            ) -> FlagSet {
+                let (old, new, updates_forbidden) = (*old, *new, *updates_forbidden);
+                (new & !updates_forbidden) | (old & updates_forbidden)
+            }
         }
 
-        match self.propagate_inner(&mut flags, &mut Rules { perms }) {
+        match self.propagate_inner(&mut flags, &mut Rules { perms }, None) {
             Ok(_changed) => {}
             Err(msg) => {
                 panic!("{}", msg);
@@ -373,6 +421,9 @@ trait PropagateRules<T> {
     ) -> (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;
+    /// Apply a filter to restrict updates.  The result is similar to `new`, but all flags marked
+    /// in `updates_forbidden` are adjusted to match their `old` values.
+    fn restrict_updates(&mut self, old: &T, new: &T, updates_forbidden: &T) -> T;
 }
 
 pub fn generate_constraints<'tcx>(

c2rust-analyze/src/util.rs

@@ -530,6 +530,9 @@ pub enum TestAttr {
     FailBeforeRewriting,
     /// `#[c2rust_analyze_test::skip_rewrite]`: Skip generating rewrites for the function.
     SkipRewrite,
+    /// `#[c2rust_analyze_test::force_non_null_args]`: Mark arguments as `NON_NULL` and don't allow
+    /// that flag to be changed during dataflow analysis.
+    ForceNonNullArgs,
 }
 
 impl TestAttr {
@@ -539,6 +542,7 @@ impl TestAttr {
             TestAttr::FailBeforeAnalysis => "fail_before_analysis",
             TestAttr::FailBeforeRewriting => "fail_before_rewriting",
             TestAttr::SkipRewrite => "skip_rewrite",
+            TestAttr::ForceNonNullArgs => "force_non_null_args",
         }
     }
 }

c2rust-analyze/tests/filecheck.rs

@@ -56,6 +56,7 @@ define_tests! {
     insertion_sort_rewrites,
     known_fn,
     non_null,
+    non_null_force,
     offset1,
     offset2,
     pointee,

c2rust-analyze/tests/filecheck/non_null_force.rs

@@ -0,0 +1,40 @@
+#![feature(register_tool)]
+#![register_tool(c2rust_analyze_test)]
+
+// TODO: All the pointers here are currently inferred to be non-`UNIQUE`, even though the access
+// patterns look fine.
+
+use std::ptr;
+
+// CHECK-LABEL: final labeling for "f"
+fn f(cond: bool) {
+    let x = 1_i32;
+    // CHECK: ([[@LINE+1]]: mut y): {{.*}}, type = (empty)#
+    let mut y = ptr::addr_of!(x);
+    if cond {
+        y = 0 as *const _;
+    }
+    // The expression `y` is considered nullable even though it's passed for argument `p` of `g`,
+    // which is forced to be `NON_NULL`.
+    // CHECK: ([[@LINE+1]]: y): {{.*}}, type = (empty)#
+    g(cond, y);
+}
+
+// CHECK-LABEL: final labeling for "g"
+// `p` should be non-null, as it's forced to be by the attribute.  This emulates the "unsound" PDG
+// case, where a variable is forced to stay `NON_NULL` even though a null possibly flows into it.
+// CHECK: ([[@LINE+2]]: p): {{.*}}, type = NON_NULL#
+#[c2rust_analyze_test::force_non_null_args]
+fn g(cond: bool, p: *const i32) {
+    // `q` is not forced to be `NON_NULL`, so it should be inferred nullable due to the null
+    // assignment below.
+    // CHECK: ([[@LINE+1]]: mut q): {{.*}}, type = (empty)#
+    let mut q = p;
+    if cond {
+        q = 0 as *const _;
+    }
+    // `r` is derived from `q` (and is not forced), so it should also be nullable.
+    // CHECK: ([[@LINE+1]]: r): {{.*}}, type = (empty)#
+    let r = q;
+}
+