Skip to content

Commit

Permalink
analyze: add option to skip borrowck (#1181)
Browse files Browse the repository at this point in the history
This adds a new command-line option `--skip-borrowck` that completely
disables the borrowck pass. All pointers are given the `UNIQUE`
permission, allowing them to be rewritten to `&mut T` instead of
`&Cell<T>`. This is useful when the code uses language features that
aren't supported by borrowck and it's known (or assumed) that it doesn't
require any `Cell` rewrites.
  • Loading branch information
spernsteiner authored Dec 9, 2024
2 parents c9f0c11 + 6c3455e commit bcc772e
Show file tree
Hide file tree
Showing 3 changed files with 38 additions and 10 deletions.
34 changes: 24 additions & 10 deletions c2rust-analyze/src/analyze.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -796,6 +798,7 @@ fn run(tcx: TyCtxt) {
&mut func_info,
&mut asn,
&mut updates_forbidden,
skip_borrowck_everywhere,
pdg_file_path,
);
}
Expand Down Expand Up @@ -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());
Expand All @@ -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());
Expand All @@ -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;
Expand Down Expand Up @@ -2230,6 +2243,7 @@ fn pdg_update_permissions<'tcx>(
func_info: &mut HashMap<LocalDefId, FuncInfo<'tcx>>,
asn: &mut Assignment,
updates_forbidden: &mut GlobalPointerTable<PermissionSet>,
skip_borrowck_everywhere: bool,
pdg_file_path: impl AsRef<Path>,
) {
let allow_unsound =
Expand Down Expand Up @@ -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);
}
}
Expand Down
10 changes: 10 additions & 0 deletions c2rust-analyze/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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(())
})?;

Expand Down
4 changes: 4 additions & 0 deletions c2rust-analyze/src/util.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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",
}
}
}
Expand Down

0 comments on commit bcc772e

Please sign in to comment.