Skip to content

Commit

Permalink
Add minimal statics support, clean up atomics
Browse files Browse the repository at this point in the history
  • Loading branch information
@artemagvanian
artemagvanian committed Jul 24, 2024
1 parent 9d3783e commit 40c8047
Show file tree
Hide file tree
Showing 8 changed files with 268 additions and 365 deletions.
34 changes: 14 additions & 20 deletions ...k_uninit/delayed_ub/delayed_ub_visitor.rs → ...init/delayed_ub/initial_target_visitor.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,22 +18,22 @@ use crate::kani_middle::transform::check_uninit::ty_layout::tys_layout_compatibl

/// Visitor that finds initial analysis targets for delayed UB instrumentation. For our purposes,
/// analysis targets are *pointers* to places reading and writing from which should be tracked.
pub struct DelayedUbVisitor {
pub struct InitialTargetVisitor {
body: Body,
delayed_ub_targets: Vec<Place>,
targets: Vec<Place>,
}

impl DelayedUbVisitor {
impl InitialTargetVisitor {
pub fn new(body: Body) -> Self {
Self { body, delayed_ub_targets: vec![] }
Self { body, targets: vec![] }
}

pub fn into_targets(self) -> Vec<Place> {
self.delayed_ub_targets
self.targets
}
}

impl MirVisitor for DelayedUbVisitor {
impl MirVisitor for InitialTargetVisitor {
fn visit_rvalue(&mut self, rvalue: &Rvalue, location: Location) {
if let Rvalue::Cast(kind, operand, ty) = rvalue {
let operand_ty = operand.ty(self.body.locals()).unwrap();
Expand All @@ -47,13 +47,11 @@ impl MirVisitor for DelayedUbVisitor {
match operand {
Operand::Copy(place) | Operand::Move(place) => {
if !tys_layout_compatible(from_ty, to_ty) {
self.delayed_ub_targets.push(place.clone());
self.targets.push(place.clone());
}
}
Operand::Constant(_) => {
unimplemented!(
"Delayed UB in presence of constants is not yet supported."
)
unreachable!("cannot be a constant")
}
}
}
Expand All @@ -70,10 +68,10 @@ impl MirVisitor for DelayedUbVisitor {
{
match &copy.dst {
Operand::Copy(place) | Operand::Move(place) => {
self.delayed_ub_targets.push(place.clone());
self.targets.push(place.clone());
}
Operand::Constant(_) => {
unimplemented!("Delayed UB in presence of constants is not yet supported.")
unreachable!("cannot be a constant")
}
}
}
Expand Down Expand Up @@ -103,11 +101,9 @@ impl MirVisitor for DelayedUbVisitor {
// Here, `dst` is the second argument.
match &args[1] {
Operand::Copy(place) | Operand::Move(place) => {
self.delayed_ub_targets.push(place.clone());
self.targets.push(place.clone());
}
Operand::Constant(_) => unimplemented!(
"Delayed UB in presence of constants is not yet supported."
),
Operand::Constant(_) => unreachable!("cannot be a constant"),
}
}
"volatile_copy_memory" | "volatile_copy_nonoverlapping_memory" => {
Expand All @@ -127,11 +123,9 @@ impl MirVisitor for DelayedUbVisitor {
// Here, `dst` is the first argument.
match &args[0] {
Operand::Copy(place) | Operand::Move(place) => {
self.delayed_ub_targets.push(place.clone());
self.targets.push(place.clone());
}
Operand::Constant(_) => unimplemented!(
"Delayed UB in presence of constants is not yet supported."
),
Operand::Constant(_) => unreachable!("cannot be a constant"),
}
}
_ => {}
Expand Down
96 changes: 56 additions & 40 deletions kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,15 +5,21 @@
//! UB. In practice, that means collecting all instructions where the place is featured.

use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction};
use crate::kani_middle::transform::check_uninit::delayed_ub::points_to_graph::{
GlobalMemLoc, PointsToGraph,
};
use crate::kani_middle::transform::check_uninit::relevant_instruction::{
InitRelevantInstruction, MemoryInitOp,
};
use crate::kani_middle::transform::check_uninit::TargetFinder;

use rustc_hir::def_id::DefId as InternalDefId;
use rustc_middle::ty::TyCtxt;
use rustc_smir::rustc_internal;
use stable_mir::mir::visit::{Location, PlaceContext};
use stable_mir::mir::{BasicBlockIdx, MirVisitor, Operand, Place, ProjectionElem, Statement};
use stable_mir::mir::{BasicBlockIdx, MirVisitor, Operand, Place, Statement};
use std::collections::HashSet;

pub struct DelayedUbTargetVisitor<'a> {
pub struct InstrumentationVisitor<'a, 'tcx> {
/// Whether we should skip the next instruction, since it might've been instrumented already.
/// When we instrument an instruction, we partition the basic block, and the instruction that
/// may trigger UB becomes the first instruction of the basic block, which we need to skip
Expand All @@ -23,29 +29,46 @@ pub struct DelayedUbTargetVisitor<'a> {
current: SourceInstruction,
/// The target instruction that should be verified.
pub target: Option<InitRelevantInstruction>,
/// The list of places we should be looking for, ignoring others.
place_filter: &'a [Place],
/// Aliasing analysis data.
points_to: &'a PointsToGraph<'tcx>,
/// The list of places we should be looking for, ignoring others
analysis_targets: &'a HashSet<GlobalMemLoc<'tcx>>,
current_def_id: InternalDefId,
tcx: TyCtxt<'tcx>,
}

impl<'a> TargetFinder for DelayedUbTargetVisitor<'a> {
impl<'a, 'tcx> TargetFinder for InstrumentationVisitor<'a, 'tcx> {
fn find_next(
&mut self,
body: &MutableBody,
bb: BasicBlockIdx,
skip_first: bool,
place_filter: &[Place],
) -> Option<InitRelevantInstruction> {
let mut visitor = DelayedUbTargetVisitor {
skip_next: skip_first,
current: SourceInstruction::Statement { idx: 0, bb },
target: None,
place_filter,
};
visitor.visit_basic_block(&body.blocks()[bb]);
visitor.target
self.skip_next = skip_first;
self.current = SourceInstruction::Statement { idx: 0, bb };
self.target = None;
self.visit_basic_block(&body.blocks()[bb]);
self.target.clone()
}
}

impl<'a> DelayedUbTargetVisitor<'a> {
impl<'a, 'tcx> InstrumentationVisitor<'a, 'tcx> {
pub fn new(
points_to: &'a PointsToGraph<'tcx>,
analysis_targets: &'a HashSet<GlobalMemLoc<'tcx>>,
current_def_id: InternalDefId,
tcx: TyCtxt<'tcx>,
) -> Self {
Self {
skip_next: false,
current: SourceInstruction::Statement { idx: 0, bb: 0 },
target: None,
points_to,
analysis_targets,
current_def_id,
tcx,
}
}
fn push_target(&mut self, source_op: MemoryInitOp) {
let target = self.target.get_or_insert_with(|| InitRelevantInstruction {
source: self.current,
Expand All @@ -56,7 +79,7 @@ impl<'a> DelayedUbTargetVisitor<'a> {
}
}

impl<'a> MirVisitor for DelayedUbTargetVisitor<'a> {
impl<'a, 'tcx> MirVisitor for InstrumentationVisitor<'a, 'tcx> {
fn visit_statement(&mut self, stmt: &Statement, location: Location) {
if self.skip_next {
self.skip_next = false;
Expand All @@ -70,31 +93,24 @@ impl<'a> MirVisitor for DelayedUbTargetVisitor<'a> {
}

fn visit_place(&mut self, place: &Place, ptx: PlaceContext, location: Location) {
// Match the place by its local.
// Match the place by whatever it is pointing to and find an intersection with the targets.
if self
.place_filter
.iter()
.any(|instrumented_place| instrumented_place.local == place.local)
.points_to
.follow_from_place(rustc_internal::internal(self.tcx, place), self.current_def_id)
.intersection(&self.analysis_targets)
.count()
!= 0
{
let deref_projection_detected = place
.projection
.iter()
.any(|projection_elem| matches!(projection_elem, ProjectionElem::Deref));
// We should only track the place itself, not whatever it gets dereferenced to.
if !deref_projection_detected {
// If we are mutating the place, initialize it.
if ptx.is_mutating() {
self.push_target(MemoryInitOp::SetRef {
operand: Operand::Copy(place.clone()),
value: true,
position: InsertPosition::After,
});
} else {
// Otherwise, check its initialization.
self.push_target(MemoryInitOp::CheckRef {
operand: Operand::Copy(place.clone()),
});
}
// If we are mutating the place, initialize it.
if ptx.is_mutating() {
self.push_target(MemoryInitOp::SetRef {
operand: Operand::Copy(place.clone()),
value: true,
position: InsertPosition::After,
});
} else {
// Otherwise, check its initialization.
self.push_target(MemoryInitOp::CheckRef { operand: Operand::Copy(place.clone()) });
}
}
self.super_place(place, ptx, location)
Expand Down
49 changes: 22 additions & 27 deletions kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,19 +16,20 @@ use crate::kani_middle::transform::BodyTransformation;
use crate::kani_middle::transform::GlobalPass;
use crate::kani_middle::transform::TransformationResult;
use crate::kani_queries::QueryDb;
use delayed_ub_visitor::DelayedUbVisitor;
use instrumentation_visitor::DelayedUbTargetVisitor;
use initial_target_visitor::InitialTargetVisitor;
use instrumentation_visitor::InstrumentationVisitor;
use points_to_analysis::PointsToAnalysis;
use points_to_graph::PlaceOrAlloc;
use points_to_graph::LocalMemLoc;
use points_to_graph::PointsToGraph;
use rustc_middle::ty::TyCtxt;
use rustc_mir_dataflow::JoinSemiLattice;
use rustc_smir::rustc_internal;
use stable_mir::mir::mono::{Instance, MonoItem};
use stable_mir::mir::MirVisitor;
use stable_mir::mir::Place;
use stable_mir::ty::FnDef;
use stable_mir::CrateDef;

mod delayed_ub_visitor;
mod initial_target_visitor;
mod instrumentation_visitor;
mod points_to_analysis;
mod points_to_graph;
Expand Down Expand Up @@ -66,18 +67,19 @@ impl GlobalPass for DelayedUbPass {
.flat_map(|instance| {
let def_id = rustc_internal::internal(tcx, instance.def.def_id());
let body = instance.body().unwrap();
let mut visitor = DelayedUbVisitor::new(body.clone());
let mut visitor = InitialTargetVisitor::new(body.clone());
visitor.visit_body(&body);
// Convert all places into the format of aliasing graph for later comparison.
visitor.into_targets().into_iter().map(move |place| {
PlaceOrAlloc::Place(rustc_internal::internal(tcx, place)).with_def_id(def_id)
LocalMemLoc::Place(rustc_internal::internal(tcx, place)).with_def_id(def_id)
})
})
.collect();

// Only perform this analysis if there is something to analyze.
if !targets.is_empty() {
let mut places_need_instrumentation = HashSet::new();
let mut analysis_targets = HashSet::new();
let mut global_points_to_graph = PointsToGraph::empty();
// Analyze aliasing for every harness.
for entry_item in starting_items {
// Convert each entry function into instance, if possible.
Expand Down Expand Up @@ -105,8 +107,9 @@ impl GlobalPass for DelayedUbPass {
);
// Since analysis targets are *pointers*, need to get its followers for instrumentation.
for target in targets.iter() {
places_need_instrumentation.extend(results.pointees_of(target));
analysis_targets.extend(results.pointees_of(target));
}
global_points_to_graph.join(&results);
}
}

Expand All @@ -118,24 +121,16 @@ impl GlobalPass for DelayedUbPass {
mem_init_fn_cache: &mut self.mem_init_fn_cache,
};
// Retrieve the body with all local instrumentation passes applied.
let new_body = MutableBody::from(transformer.body(tcx, instance));
// Retrieve all places we need to instrument in the appropriate format.
let place_filter: Vec<Place> = places_need_instrumentation
.iter()
.filter(|place| {
// Make sure only places from the current instance are included.
place.has_def_id(internal_def_id)
})
.filter_map(|global_place_or_alloc| {
match global_place_or_alloc.without_def_id() {
PlaceOrAlloc::Alloc(_) => None, // Allocations cannot be read directly, so we need not worry about them.
PlaceOrAlloc::Place(place) => Some(rustc_internal::stable(place)), // Convert back to StableMIR.
}
})
.collect();
// Finally, instrument.
let (instrumentation_added, body) = instrumenter
.instrument::<DelayedUbTargetVisitor>(tcx, new_body, instance, &place_filter);
let body = MutableBody::from(transformer.body(tcx, instance));
// Instrument for delayed UB.
let target_finder = InstrumentationVisitor::new(
&global_points_to_graph,
&analysis_targets,
internal_def_id,
tcx,
);
let (instrumentation_added, body) =
instrumenter.instrument(tcx, body, instance, target_finder);
// If some instrumentation has been performed, update the cached body in the local transformer.
if instrumentation_added {
transformer.cache.entry(instance).and_modify(|transformation_result| {
Expand Down
Loading

0 comments on commit 40c8047

Please sign in to comment.