Skip to content

Commit

Permalink
analyze: emit permission annotations inline during rewriting
Browse files Browse the repository at this point in the history
  • Loading branch information
spernsteiner committed Mar 16, 2024
1 parent 6fab8ad commit 35d8394
Show file tree
Hide file tree
Showing 2 changed files with 93 additions and 20 deletions.
105 changes: 89 additions & 16 deletions c2rust-analyze/src/analyze.rs
Original file line number Diff line number Diff line change
@@ -1,16 +1,9 @@
use crate::annotate::AnnotationBuffer;
use crate::borrowck;
use crate::context::AnalysisCtxt;
use crate::context::AnalysisCtxtData;
use crate::context::FlagSet;
use crate::context::GlobalAnalysisCtxt;
use crate::context::GlobalAssignment;
use crate::context::LFnSig;
use crate::context::LTy;
use crate::context::LTyCtxt;
use crate::context::LocalAssignment;
use crate::context::PermissionSet;
use crate::context::PointerId;
use crate::context::PointerInfo;
use crate::context::{
self, AnalysisCtxt, AnalysisCtxtData, FlagSet, GlobalAnalysisCtxt, GlobalAssignment, LFnSig,
LTy, LTyCtxt, LocalAssignment, PermissionSet, PointerId, PointerInfo,
};
use crate::dataflow;
use crate::dataflow::DataflowConstraints;
use crate::equiv::GlobalEquivSet;
Expand Down Expand Up @@ -57,8 +50,7 @@ use rustc_middle::ty::Ty;
use rustc_middle::ty::TyCtxt;
use rustc_middle::ty::TyKind;
use rustc_middle::ty::WithOptConstParam;
use rustc_span::Span;
use rustc_span::Symbol;
use rustc_span::{Span, Symbol, DUMMY_SP};
use std::collections::HashMap;
use std::collections::HashSet;
use std::env;
Expand Down Expand Up @@ -115,6 +107,10 @@ impl<T> MaybeUnset<T> {
pub fn take(&mut self) -> T {
self.0.take().expect("value is not set")
}

pub fn is_set(&self) -> bool {
self.0.is_some()
}
}

impl<T> Deref for MaybeUnset<T> {
Expand Down Expand Up @@ -1235,6 +1231,9 @@ fn run(tcx: TyCtxt) {
// for a single function makes FileCheck tests easier to write.
let mut func_reports = HashMap::<LocalDefId, String>::new();

// Buffer for annotations, which are inserted inline as comments when rewriting.
let mut ann = AnnotationBuffer::new(tcx);

// Generate rewrites for all functions.
let mut all_rewrites = Vec::new();

Expand Down Expand Up @@ -1463,6 +1462,52 @@ fn run(tcx: TyCtxt) {
info.acx_data.set(acx.into_data());
}

// Generate annotations for all functions.
for ldid in tcx.hir().body_owners() {
// Skip any body owners that aren't present in `func_info`, and also get the info itself.
let info = match func_info.get_mut(&ldid) {
Some(x) => x,
None => continue,
};

if !info.acx_data.is_set() {
continue;
}

let ldid_const = WithOptConstParam::unknown(ldid);
let mir = tcx.mir_built(ldid_const);
let mir = mir.borrow();
let acx = gacx.function_context_with_data(&mir, info.acx_data.take());
let asn = gasn.and(&mut info.lasn);

// Generate inline annotations for pointer-typed locals
for (local, decl) in mir.local_decls.iter_enumerated() {
let span = local_span(decl);
let mut ptrs = Vec::new();
let ty_str = context::print_ty_with_pointer_labels(acx.local_tys[local], |ptr| {
if ptr.is_none() {
return String::new();
}
ptrs.push(ptr);
format!("{{{}}}", ptr)
});
if ptrs.len() == 0 {
continue;
}
// TODO: emit addr_of when it's nontrivial
// TODO: emit pointee_types when nontrivial
ann.emit(span, format_args!("typeof({:?}) = {}", local, ty_str));
for ptr in ptrs {
ann.emit(
span,
format_args!(" {} = {:?}, {:?}", ptr, asn.perms()[ptr], asn.flags()[ptr]),
);
}
}

info.acx_data.set(acx.into_data());
}

// Print results for `static` items.
eprintln!("\nfinal labeling for static items:");
let lcx1 = crate::labeled_ty::LabeledTyCtxt::new(tcx);
Expand Down Expand Up @@ -1497,6 +1542,27 @@ fn run(tcx: TyCtxt) {
let ty_flags = gasn.flags[pid];
eprintln!("{name:}: ({pid}) perms = {ty_perms:?}, flags = {ty_flags:?}");
}

// Emit annotations for fields
let span = tcx.def_ident_span(did).unwrap_or(DUMMY_SP);
let mut ptrs = Vec::new();
let ty_str = context::print_ty_with_pointer_labels(field_lty, |ptr| {
if ptr.is_none() {
return String::new();
}
ptrs.push(ptr);
format!("{{{}}}", ptr)
});
if ptrs.len() == 0 {
continue;
}
ann.emit(span, format_args!("typeof({}) = {}", name, ty_str));
for ptr in ptrs {
ann.emit(
span,
format_args!(" {} = {:?}, {:?}", ptr, gasn.perms[ptr], gasn.flags[ptr]),
);
}
}

let mut adt_dids = gacx.adt_metadata.table.keys().cloned().collect::<Vec<_>>();
Expand All @@ -1511,14 +1577,16 @@ fn run(tcx: TyCtxt) {
// Apply rewrites
// ----------------------------------

let annotations = ann.finish();

// Apply rewrite to all functions at once.
let mut update_files = rewrite::UpdateFiles::No;
if let Ok(val) = env::var("C2RUST_ANALYZE_REWRITE_IN_PLACE") {
if val == "1" {
update_files = rewrite::UpdateFiles::Yes;
}
}
rewrite::apply_rewrites(tcx, all_rewrites, HashMap::new(), update_files);
rewrite::apply_rewrites(tcx, all_rewrites, annotations, update_files);

// ----------------------------------
// Report caught panics
Expand Down Expand Up @@ -1617,7 +1685,7 @@ fn make_sig_fixed(gasn: &mut GlobalAssignment, lsig: &LFnSig) {
}
}

fn describe_local(tcx: TyCtxt, decl: &LocalDecl) -> String {
fn local_span(decl: &LocalDecl) -> Span {
let mut span = decl.source_info.span;
if let Some(ref info) = decl.local_info {
if let LocalInfo::User(ref binding_form) = **info {
Expand All @@ -1627,6 +1695,11 @@ fn describe_local(tcx: TyCtxt, decl: &LocalDecl) -> String {
}
}
}
span
}

fn describe_local(tcx: TyCtxt, decl: &LocalDecl) -> String {
let span = local_span(decl);
describe_span(tcx, span)
}

Expand Down
8 changes: 4 additions & 4 deletions c2rust-analyze/tests/filecheck/insertion_sort_driver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,8 @@ pub unsafe extern "C" fn insertion_sort(n: libc::c_int, p: *mut libc::c_int) {
// CHECK: let tmp: {{.*}} = *&(&(&*(p))[((i as isize) as usize) ..])[0];
let tmp: libc::c_int = *p.offset(i as isize);
let mut j: libc::c_int = i;
// CHECK-NOT: p.offset
// `p.offset` should not appear, except in inline annotation comments.
// CHECK-NOT: {{^[^/]*}}p.offset
while j > 0 as libc::c_int &&
*p.offset((j - 1 as libc::c_int) as isize) > tmp {
*p.offset(j as isize) =
Expand All @@ -28,10 +29,9 @@ pub unsafe extern "C" fn insertion_sort(n: libc::c_int, p: *mut libc::c_int) {

// CHECK-LABEL: pub unsafe extern "C" fn check_eq
// CHECK-SAME: p: &'h0 [(libc::c_int)]
// CHECK-NEXT: q: &'h1 [(libc::c_int)]
// CHECK-SAME: q: &'h1 [(libc::c_int)]
#[no_mangle]
pub unsafe extern "C" fn check_eq(n: libc::c_int, p: *mut libc::c_int,
q: *mut libc::c_int) {
pub unsafe extern "C" fn check_eq(n: libc::c_int, p: *mut libc::c_int, q: *mut libc::c_int) {
let mut i: libc::c_int = 0 as libc::c_int;
while i < n {
//assert!(*p.offset(i as isize) == *q.offset(i as isize));
Expand Down

0 comments on commit 35d8394

Please sign in to comment.