From c248af11a05817560947ae9fb3eab69634bea274 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Mon, 29 Apr 2024 13:39:47 -0700 Subject: [PATCH 1/4] analyze: dataflow: internal implementation of updates_forbidden --- c2rust-analyze/src/dataflow/mod.rs | 48 ++++++++++++++++++++++++++++-- 1 file changed, 46 insertions(+), 2 deletions(-) diff --git a/c2rust-analyze/src/dataflow/mod.rs b/c2rust-analyze/src/dataflow/mod.rs index 39c1a5f7b..2e3ab2658 100644 --- a/c2rust-analyze/src/dataflow/mod.rs +++ b/c2rust-analyze/src/dataflow/mod.rs @@ -118,9 +118,19 @@ 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, None) { Ok(changed) => changed, Err(msg) => { panic!("{}", msg); @@ -128,10 +138,17 @@ impl DataflowConstraints { } } + /// 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( &self, xs: &mut PointerTableMut, rules: &mut R, + updates_forbidden: Option<&PointerTable>, ) -> Result where T: PartialEq, @@ -139,6 +156,14 @@ impl DataflowConstraints { { 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 +182,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 +196,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 +209,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 +220,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 +308,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 +414,9 @@ trait PropagateRules { ) -> (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>( From da4276f28f49c4b7dcb563fd7da55aaf97d31ffd Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Mon, 29 Apr 2024 16:40:14 -0700 Subject: [PATCH 2/4] analyze: create updates_forbidden set and pass it to dataflow --- c2rust-analyze/src/analyze.rs | 11 ++++++++++- c2rust-analyze/src/borrowck/mod.rs | 5 +++-- c2rust-analyze/src/dataflow/mod.rs | 11 +++++++++-- 3 files changed, 22 insertions(+), 5 deletions(-) diff --git a/c2rust-analyze/src/analyze.rs b/c2rust-analyze/src/analyze.rs index b8058d9ca..7a2efce28 100644 --- a/c2rust-analyze/src/analyze.rs +++ b/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, + /// Local part of the `updates_forbidden` mask. + l_updates_forbidden: MaybeUnset>, /// Constraints on pointee types gathered from the body of this function. pointee_constraints: MaybeUnset>, /// 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 @@ -1121,16 +1127,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, diff --git a/c2rust-analyze/src/borrowck/mod.rs b/c2rust-analyze/src/borrowck/mod.rs index ad2a95004..19fa1b621 100644 --- a/c2rust-analyze/src/borrowck/mod.rs +++ b/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, + updates_forbidden: &PointerTable, name: &str, mir: &Body<'tcx>, field_ltys: HashMap>, @@ -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 { diff --git a/c2rust-analyze/src/dataflow/mod.rs b/c2rust-analyze/src/dataflow/mod.rs index 2e3ab2658..5a74ab2ce 100644 --- a/c2rust-analyze/src/dataflow/mod.rs +++ b/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) -> 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, + updates_forbidden: &PointerTable, + ) -> bool { eprintln!("=== propagating ==="); eprintln!("constraints:"); for c in &self.constraints { @@ -130,7 +137,7 @@ impl DataflowConstraints { } } - match self.propagate_inner(hypothesis, &mut PropagatePerms, None) { + match self.propagate_inner(hypothesis, &mut PropagatePerms, Some(updates_forbidden)) { Ok(changed) => changed, Err(msg) => { panic!("{}", msg); From ac5e674525988fb06c9eba5a746575723b10621d Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Mon, 29 Apr 2024 16:43:17 -0700 Subject: [PATCH 3/4] analyze: add test case exercising updates_forbidden --- c2rust-analyze/src/analyze.rs | 23 +++++++++++ c2rust-analyze/src/util.rs | 4 ++ c2rust-analyze/tests/filecheck.rs | 1 + .../tests/filecheck/non_null_force.rs | 40 +++++++++++++++++++ 4 files changed, 68 insertions(+) create mode 100644 c2rust-analyze/tests/filecheck/non_null_force.rs diff --git a/c2rust-analyze/src/analyze.rs b/c2rust-analyze/src/analyze.rs index 7a2efce28..4aa584a1b 100644 --- a/c2rust-analyze/src/analyze.rs +++ b/c2rust-analyze/src/analyze.rs @@ -1101,6 +1101,29 @@ fn run(tcx: TyCtxt) { ); } + // 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. + 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); + } + } + } + } + eprintln!("=== ADT Metadata ==="); eprintln!("{:?}", gacx.adt_metadata); diff --git a/c2rust-analyze/src/util.rs b/c2rust-analyze/src/util.rs index 7f34dcf5e..9c6902ecf 100644 --- a/c2rust-analyze/src/util.rs +++ b/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", } } } diff --git a/c2rust-analyze/tests/filecheck.rs b/c2rust-analyze/tests/filecheck.rs index d228c8c0f..c33f1f322 100644 --- a/c2rust-analyze/tests/filecheck.rs +++ b/c2rust-analyze/tests/filecheck.rs @@ -56,6 +56,7 @@ define_tests! { insertion_sort_rewrites, known_fn, non_null, + non_null_force, offset1, offset2, pointee, diff --git a/c2rust-analyze/tests/filecheck/non_null_force.rs b/c2rust-analyze/tests/filecheck/non_null_force.rs new file mode 100644 index 000000000..a6757f581 --- /dev/null +++ b/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; +} + From 9f3129d4328a9f86514e1e89bbb4c81523b9b043 Mon Sep 17 00:00:00 2001 From: Stuart Pernsteiner Date: Thu, 2 May 2024 09:46:18 -0700 Subject: [PATCH 4/4] analyze: refactor: move some TestAttr handling into helper fns --- c2rust-analyze/src/analyze.rs | 94 ++++++++++++++++++++++------------- 1 file changed, 59 insertions(+), 35 deletions(-) diff --git a/c2rust-analyze/src/analyze.rs b/c2rust-analyze/src/analyze.rs index 4aa584a1b..f0e627b19 100644 --- a/c2rust-analyze/src/analyze.rs +++ b/c2rust-analyze/src/analyze.rs @@ -1088,41 +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()), - ); - } - - // 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. - 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); - } - } - } - } + 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); @@ -1850,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, + gasn: &mut GlobalAssignment, + g_updates_forbidden: &mut GlobalPointerTable, +) { + 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 {