diff --git a/c2rust-analyze/src/analyze.rs b/c2rust-analyze/src/analyze.rs index f38c1d4e4..710784bb6 100644 --- a/c2rust-analyze/src/analyze.rs +++ b/c2rust-analyze/src/analyze.rs @@ -785,6 +785,8 @@ fn run(tcx: TyCtxt) { } } + let skip_borrowck_everywhere = env::var("C2RUST_ANALYZE_SKIP_BORROWCK").as_deref() == Ok("1"); + // Load permission info from PDG let pdg_compare = env::var("C2RUST_ANALYZE_COMPARE_PDG").as_deref() == Ok("1"); // In compare mode, we load the PDG for comparison after analysis, not before. @@ -796,6 +798,7 @@ fn run(tcx: TyCtxt) { &mut func_info, &mut asn, &mut updates_forbidden, + skip_borrowck_everywhere, pdg_file_path, ); } @@ -891,6 +894,9 @@ fn run(tcx: TyCtxt) { continue; } + let skip_borrowck = + skip_borrowck_everywhere || util::has_test_attr(tcx, ldid, TestAttr::SkipBorrowck); + let info = func_info.get_mut(&ldid).unwrap(); let ldid_const = WithOptConstParam::unknown(ldid); let name = tcx.item_name(ldid.to_def_id()); @@ -905,15 +911,17 @@ fn run(tcx: TyCtxt) { // on a fixpoint, so there's no need to do multiple iterations here. info.dataflow.propagate(&mut asn.perms, &updates_forbidden); - borrowck::borrowck_mir( - &acx, - &info.dataflow, - &mut asn.perms_mut(), - &updates_forbidden, - name.as_str(), - &mir, - field_ltys, - ); + if !skip_borrowck { + borrowck::borrowck_mir( + &acx, + &info.dataflow, + &mut asn.perms_mut(), + &updates_forbidden, + name.as_str(), + &mir, + field_ltys, + ); + } })); info.acx_data.set(acx.into_data()); @@ -934,6 +942,11 @@ fn run(tcx: TyCtxt) { let mut num_changed = 0; for (i, &old) in old_gasn.iter().enumerate() { let ptr = PointerId::global(i as u32); + + if skip_borrowck_everywhere { + asn.perms[ptr].insert(PermissionSet::UNIQUE); + } + let new = asn.perms[ptr]; if old != new { let added = new & !old; @@ -2230,6 +2243,7 @@ fn pdg_update_permissions<'tcx>( func_info: &mut HashMap>, asn: &mut Assignment, updates_forbidden: &mut GlobalPointerTable, + skip_borrowck_everywhere: bool, pdg_file_path: impl AsRef, ) { let allow_unsound = @@ -2268,7 +2282,7 @@ fn pdg_update_permissions<'tcx>( if node_info.flows_to.neg_offset.is_some() { perms.insert(PermissionSet::OFFSET_SUB); } - if !node_info.unique { + if !node_info.unique && !skip_borrowck_everywhere { perms.remove(PermissionSet::UNIQUE); } } diff --git a/c2rust-analyze/src/main.rs b/c2rust-analyze/src/main.rs index ce392588e..f77e602e0 100644 --- a/c2rust-analyze/src/main.rs +++ b/c2rust-analyze/src/main.rs @@ -104,6 +104,11 @@ struct Args { #[clap(long)] annotate_def_spans: bool, + /// Completely disable the `borrowck` pass. All pointers will be given the `UNIQUE` + /// permission; none will be wrapped in `Cell`. + #[clap(long)] + skip_borrowck: bool, + /// Read a list of defs that should be marked non-rewritable (`FIXED`) from this file path. /// Run `c2rust-analyze` without this option and check the debug output for a full list of defs /// in the crate being analyzed; the file passed to this option should list a subset of those @@ -408,6 +413,7 @@ fn cargo_wrapper(rustc_wrapper: &Path) -> anyhow::Result<()> { rewrite_in_place, use_manual_shims, annotate_def_spans, + skip_borrowck, fixed_defs_list, force_rewrite_defs_list, skip_pointee_defs_list, @@ -489,6 +495,10 @@ fn cargo_wrapper(rustc_wrapper: &Path) -> anyhow::Result<()> { cmd.env("C2RUST_ANALYZE_ANNOTATE_DEF_SPANS", "1"); } + if skip_borrowck { + cmd.env("C2RUST_ANALYZE_SKIP_BORROWCK", "1"); + } + Ok(()) })?; diff --git a/c2rust-analyze/src/util.rs b/c2rust-analyze/src/util.rs index 1239cae6f..042026e4e 100644 --- a/c2rust-analyze/src/util.rs +++ b/c2rust-analyze/src/util.rs @@ -552,6 +552,9 @@ pub enum TestAttr { /// `#[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, + /// `#[c2rust_analyze_test::skip_borrowck]`: Don't run borrowck for this function. The + /// `UNIQUE` permission won't be removed from pointers. + SkipBorrowck, } impl TestAttr { @@ -562,6 +565,7 @@ impl TestAttr { TestAttr::FailBeforeRewriting => "fail_before_rewriting", TestAttr::SkipRewrite => "skip_rewrite", TestAttr::ForceNonNullArgs => "force_non_null_args", + TestAttr::SkipBorrowck => "skip_borrowck", } } }