Instrumentation for delayed UB stemming from uninitialized memory

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -87,6 +87,13 @@ impl GotocCodegenBackend {
         check_contract: Option<InternalDefId>,
         mut transformer: BodyTransformation,
     ) -> (GotocCtx<'tcx>, Vec<MonoItem>, Option<AssignsContract>) {
+        // This runs reachability analysis before global passes are applied. 
+        //
+        // Alternatively, we could run reachability only once after the global passes are applied
+        // and resolve the necessary dependencies inside the passes on the fly. This, however, has a
+        // disadvantage of not having a precomputed call graph for the global passes to use. The
+        // call graph could be used, for example, in resolving function pointer or vtable calls for
+        // global passes that need this.
         let (items, call_graph) = with_timer(
             || collect_reachable_items(tcx, &mut transformer, starting_items),
             "codegen reachability analysis",
@@ -115,6 +122,13 @@ impl GotocCodegenBackend {
             call_graph,
         );
 
+        // Re-collect reachable items after global transformations were applied. This is necessary
+        // since global pass could add extra calls to instrumentation.
+        let (items, _) = with_timer(
+            || collect_reachable_items(tcx, &mut transformer, starting_items),
+            "codegen reachability analysis (second pass)",
+        );
+
         // Follow rustc naming convention (cx is abbrev for context).
         // https://rustc-dev-guide.rust-lang.org/conventions.html#naming-conventions
         let mut gcx =
@@ -260,8 +274,8 @@ impl CodegenBackend for GotocCodegenBackend {
                     for unit in units.iter() {
                         // We reset the body cache for now because each codegen unit has different
                         // configurations that affect how we transform the instance body.
-                        let mut transformer = BodyTransformation::new(&queries, tcx, &unit);
                         for harness in &unit.harnesses {
+                            let transformer = BodyTransformation::new(&queries, tcx, &unit);
                             let model_path = units.harness_model_path(*harness).unwrap();
                             let contract_metadata =
                                 contract_metadata_for_harness(tcx, harness.def.def_id()).unwrap();
@@ -273,7 +287,7 @@ impl CodegenBackend for GotocCodegenBackend {
                                 contract_metadata,
                                 transformer,
                             );
-                            transformer = results.extend(gcx, items, None);
+                            results.extend(gcx, items, None);
                             if let Some(assigns_contract) = contract_info {
                                 modifies_instances.push((*harness, assigns_contract));
                             }

kani-compiler/src/kani_middle/transform/body.rs

@@ -469,6 +469,12 @@ impl SourceInstruction {
             SourceInstruction::Terminator { bb } => blocks[bb].terminator.span,
         }
     }
+
+    pub fn bb(&self) -> usize {
+        match self {
+            SourceInstruction::Statement { bb, .. } | SourceInstruction::Terminator { bb } => *bb,
+        }
+    }
 }
 
 fn find_instance(tcx: TyCtxt, diagnostic: &str) -> Option<Instance> {

kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs

@@ -0,0 +1,148 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! This module contains the visitor responsible for collecting initial analysis targets for delayed
+//! UB instrumentation.
+
+use stable_mir::{
+    mir::{
+        alloc::GlobalAlloc,
+        mono::{Instance, InstanceKind},
+        visit::Location,
+        Body, CastKind, LocalDecl, MirVisitor, Mutability, NonDivergingIntrinsic, Operand, Place,
+        Rvalue, Statement, StatementKind, Terminator, TerminatorKind,
+    },
+    ty::{ConstantKind, RigidTy, TyKind},
+    CrateDef, DefId,
+};
+
+use crate::kani_middle::transform::check_uninit::ty_layout::tys_layout_compatible;
+
+/// Pointer, write through which might trigger delayed UB.
+pub enum AnalysisTarget {
+    Place(Place),
+    Static(DefId),
+}
+
+/// 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 InitialTargetVisitor {
+    body: Body,
+    targets: Vec<AnalysisTarget>,
+}
+
+impl InitialTargetVisitor {
+    pub fn new(body: Body) -> Self {
+        Self { body, targets: vec![] }
+    }
+
+    pub fn into_targets(self) -> Vec<AnalysisTarget> {
+        self.targets
+    }
+
+    pub fn push_operand(&mut self, operand: &Operand) {
+        match operand {
+            Operand::Copy(place) | Operand::Move(place) => {
+                self.targets.push(AnalysisTarget::Place(place.clone()));
+            }
+            Operand::Constant(constant) => {
+                // Extract the static from the constant.
+                if let ConstantKind::Allocated(allocation) = constant.const_.kind() {
+                    for (_, prov) in &allocation.provenance.ptrs {
+                        if let GlobalAlloc::Static(static_def) = GlobalAlloc::from(prov.0) {
+                            self.targets.push(AnalysisTarget::Static(static_def.def_id()));
+                        };
+                    }
+                }
+            }
+        }
+    }
+}
+
+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();
+            match kind {
+                CastKind::Transmute | CastKind::PtrToPtr => {
+                    if let (
+                        RigidTy::RawPtr(from_ty, Mutability::Mut),
+                        RigidTy::RawPtr(to_ty, Mutability::Mut),
+                    ) = (operand_ty.kind().rigid().unwrap(), ty.kind().rigid().unwrap())
+                    {
+                        if !tys_layout_compatible(from_ty, to_ty) {
+                            self.push_operand(operand);
+                        }
+                    }
+                }
+                _ => {}
+            };
+        }
+        self.super_rvalue(rvalue, location);
+    }
+
+    fn visit_statement(&mut self, stmt: &Statement, location: Location) {
+        if let StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(copy)) =
+            &stmt.kind
+        {
+            self.push_operand(&copy.dst);
+        }
+        self.super_statement(stmt, location);
+    }
+
+    fn visit_terminator(&mut self, term: &Terminator, location: Location) {
+        if let TerminatorKind::Call { func, args, .. } = &term.kind {
+            let instance = match try_resolve_instance(self.body.locals(), func) {
+                Ok(instance) => instance,
+                Err(reason) => {
+                    panic!("{reason}");
+                }
+            };
+            if instance.kind == InstanceKind::Intrinsic {
+                match instance.intrinsic_name().unwrap().as_str() {
+                    "copy" => {
+                        assert_eq!(args.len(), 3, "Unexpected number of arguments for `copy`");
+                        assert!(matches!(
+                            args[0].ty(self.body.locals()).unwrap().kind(),
+                            TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not))
+                        ));
+                        assert!(matches!(
+                            args[1].ty(self.body.locals()).unwrap().kind(),
+                            TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut))
+                        ));
+                        // Here, `dst` is the second argument.
+                        self.push_operand(&args[1]);
+                    }
+                    "volatile_copy_memory" | "volatile_copy_nonoverlapping_memory" => {
+                        assert_eq!(
+                            args.len(),
+                            3,
+                            "Unexpected number of arguments for `volatile_copy`"
+                        );
+                        assert!(matches!(
+                            args[0].ty(self.body.locals()).unwrap().kind(),
+                            TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut))
+                        ));
+                        assert!(matches!(
+                            args[1].ty(self.body.locals()).unwrap().kind(),
+                            TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not))
+                        ));
+                        // Here, `dst` is the first argument.
+                        self.push_operand(&args[0]);
+                    }
+                    _ => {}
+                }
+            }
+        }
+        self.super_terminator(term, location);
+    }
+}
+
+/// Try retrieving instance for the given function operand.
+fn try_resolve_instance(locals: &[LocalDecl], func: &Operand) -> Result<Instance, String> {
+    let ty = func.ty(locals).unwrap();
+    match ty.kind() {
+        TyKind::RigidTy(RigidTy::FnDef(def, args)) => Ok(Instance::resolve(def, &args).unwrap()),
+        _ => Err(format!("Kani does not support reasoning about arguments to `{ty:?}`.")),
+    }
+}

kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/instrumentation_visitor.rs

@@ -0,0 +1,125 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Visitor that collects all instructions relevant to uninitialized memory access caused by delayed
+//! 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, Statement, Terminator};
+use std::collections::HashSet;
+
+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
+    /// later.
+    skip_next: bool,
+    /// The instruction being visited at a given point.
+    current: SourceInstruction,
+    /// The target instruction that should be verified.
+    pub target: Option<InitRelevantInstruction>,
+    /// 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, 'tcx> TargetFinder for InstrumentationVisitor<'a, 'tcx> {
+    fn find_next(
+        &mut self,
+        body: &MutableBody,
+        bb: BasicBlockIdx,
+        skip_first: bool,
+    ) -> Option<InitRelevantInstruction> {
+        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, '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,
+            after_instruction: vec![],
+            before_instruction: vec![],
+        });
+        target.push_operation(source_op);
+    }
+}
+
+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;
+        } else if self.target.is_none() {
+            // Check all inner places.
+            self.super_statement(stmt, location);
+            // Switch to the next statement.
+            let SourceInstruction::Statement { idx, bb } = self.current else { unreachable!() };
+            self.current = SourceInstruction::Statement { idx: idx + 1, bb };
+        }
+    }
+
+    fn visit_terminator(&mut self, term: &Terminator, location: Location) {
+        if !(self.skip_next || self.target.is_some()) {
+            self.current = SourceInstruction::Terminator { bb: self.current.bb() };
+            self.super_terminator(term, location);
+        }
+    }
+
+    fn visit_place(&mut self, place: &Place, ptx: PlaceContext, location: Location) {
+        // Match the place by whatever it is pointing to and find an intersection with the targets.
+        if self
+            .points_to
+            .follow_from_place(rustc_internal::internal(self.tcx, place), self.current_def_id)
+            .intersection(&self.analysis_targets)
+            .next()
+            .is_some()
+        {
+            // 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)
+    }
+}