From 2d99fface54027743323c43ba5267c0555f3314d Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 24 Jul 2024 15:21:05 -0700 Subject: [PATCH] Add support for closures, fix function call handling --- .../transform/check_uninit/delayed_ub/mod.rs | 1 + .../delayed_ub/points_to_analysis.rs | 71 +++++++++++++------ .../expected/uninit/delayed-ub/delayed-ub.rs | 32 +++++++-- tests/expected/uninit/delayed-ub/expected | 9 ++- 4 files changed, 86 insertions(+), 27 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs index 46881cb0c89c..a1da69b3bfba 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs @@ -112,6 +112,7 @@ impl GlobalPass for DelayedUbPass { call_graph, &instances, transformer, + &PointsToGraph::empty(), ); // Since analysis targets are *pointers*, need to get its followers for instrumentation. for target in targets.iter() { diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/points_to_analysis.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/points_to_analysis.rs index 9cc1d591debc..2fae0b4f51df 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/points_to_analysis.rs @@ -37,6 +37,7 @@ pub struct PointsToAnalysis<'a, 'tcx> { call_graph: &'a CallGraph, instances: &'a Vec, transformer: &'a mut BodyTransformation, + initial_graph: &'a PointsToGraph<'tcx>, } impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> { @@ -49,8 +50,17 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> { call_graph: &'a CallGraph, instances: &'a Vec, transformer: &'a mut BodyTransformation, + initial_graph: &'a PointsToGraph<'tcx>, ) -> PointsToGraph<'tcx> { - let analysis = Self { body: body.clone(), tcx, def_id, call_graph, instances, transformer }; + let analysis = Self { + body: body.clone(), + tcx, + def_id, + call_graph, + instances, + transformer, + initial_graph, + }; let mut cursor = analysis.into_engine(tcx, &body).iterate_to_fixpoint().into_results_cursor(&body); let mut results = PointsToGraph::from_body(&body, def_id); @@ -70,17 +80,18 @@ impl<'a, 'tcx> AnalysisDomain<'tcx> for PointsToAnalysis<'a, 'tcx> { const NAME: &'static str = "PointsToAnalysis"; /// Dataflow state instantiated at the beginning of each basic block. - fn bottom_value(&self, body: &Body<'tcx>) -> Self::Domain { - PointsToGraph::from_body(body, self.def_id) + fn bottom_value(&self, _body: &Body<'tcx>) -> Self::Domain { + PointsToGraph::empty() } - /// Dataflow state instantiated at the entry into the body, for us this coincides with the - /// bottom value, so we don't need to do anything. + /// Dataflow state instantiated at the entry into the body, this should be the current dataflow + /// graph. fn initialize_start_block( &self, _body: &rustc_middle::mir::Body<'tcx>, - _state: &mut Self::Domain, + state: &mut Self::Domain, ) { + state.join(&self.initial_graph); } } @@ -506,6 +517,36 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> { stable_body.internal_mir(self.tcx) }; + // One missing link is the connections between the arguments in the + // caller and parameters in the callee, add it to the graph. + match new_body.spread_arg { + Some(spread_arg) => { + let spread_arg_operand = args[spread_arg.as_usize()].node.clone(); + for i in 0..new_body.arg_count { + let lvalue_set = HashSet::from([LocalMemLoc::Place(Place { + local: (i + 1).into(), // Since arguments in the callee are starting with 1, account for that. + projection: List::empty(), + }) + .with_def_id(instance.def_id())]); + // This conservatively assumes all arguments alias to all parameters. This can be + // improved by supporting scalar places. + let rvalue_set = self.follow_rvalue(state, spread_arg_operand.clone()); + state.extend(&lvalue_set, &rvalue_set); + } + } + None => { + for (i, arg) in args.iter().enumerate() { + let lvalue_set = HashSet::from([LocalMemLoc::Place(Place { + local: (i + 1).into(), // Since arguments in the callee are starting with 1, account for that. + projection: List::empty(), + }) + .with_def_id(instance.def_id())]); + let rvalue_set = self.follow_rvalue(state, arg.node.clone()); + state.extend(&lvalue_set, &rvalue_set); + } + } + } + // Recursively run the analysis and join the results into the current state. let new_result = PointsToAnalysis::run( new_body, @@ -514,25 +555,11 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> { self.call_graph, self.instances, self.transformer, + state, ); state.join(&new_result); - // One missing link is the connections between the arguments in the - // caller and parameters in the callee, add it to the graph. - // - // TODO: this is probably wrong if the arguments are passed via spread, - // as in with closures, so we would need to fix that. - for (i, arg) in args.iter().enumerate() { - let lvalue_set = HashSet::from([LocalMemLoc::Place(Place { - local: (i + 1).into(), // Since arguments in the callee are starting with 1, account for that. - projection: List::empty(), - }) - .with_def_id(instance.def_id())]); - let rvalue_set = self.follow_rvalue(state, arg.node.clone()); - state.extend(&lvalue_set, &rvalue_set); - } - // Similarly, need to connect the return value to the return - // destination. + // Now, need to connect the return value to the return destination. let lvalue_set = state.follow_from_place(*destination, self.def_id); let rvalue_set = HashSet::from([LocalMemLoc::Place(Place { local: 0usize.into(), diff --git a/tests/expected/uninit/delayed-ub/delayed-ub.rs b/tests/expected/uninit/delayed-ub/delayed-ub.rs index 2e956856a334..b27a3c484eab 100644 --- a/tests/expected/uninit/delayed-ub/delayed-ub.rs +++ b/tests/expected/uninit/delayed-ub/delayed-ub.rs @@ -43,14 +43,14 @@ fn delayed_ub_static() { } /// Helper to launder the pointer while keeping the address. -unsafe fn launder(ptr: *mut (u8, u32, u64)) -> *mut (u8, u32, u64) { +unsafe fn launder(ptr: *mut u128) -> *mut u128 { let a = ptr; let b = a as *const u128; let c: *mut i128 = std::mem::transmute(b); let d = c as usize; let e = d + 1; let f = e - 1; - return f as *mut (u8, u32, u64); + return f as *mut u128; } /// Delayed UB via mutable pointer write with additional laundering. @@ -58,14 +58,38 @@ unsafe fn launder(ptr: *mut (u8, u32, u64)) -> *mut (u8, u32, u64) { fn delayed_ub_laundered() { unsafe { let mut value: u128 = 0; - let ptr = &mut value as *mut _ as *mut (u8, u32, u64); + let ptr = &mut value as *mut u128; // Pass pointer around in an attempt to remove the association. - let ptr = launder(ptr); + let ptr = launder(ptr) as *mut (u8, u32, u64); *ptr = (4, 4, 4); assert!(value > 0); // UB: This reads a padding value! } } +/// Delayed UB via mutable pointer write with additional laundering but via closure. +#[kani::proof] +fn delayed_ub_closure_laundered() { + unsafe { + let mut value: u128 = 0; + let ptr = &mut value as *mut u128; + // Add extra args to test spread_arg. + let launder = |arg1: bool, arg2: bool, arg3: bool, ptr: *mut u128| -> *mut u128 { + let a = ptr; + let b = a as *const u128; + let c: *mut i128 = std::mem::transmute(b); + let d = c as usize; + let e = d + 1; + let f = e - 1; + return f as *mut u128; + }; + // Pass pointer around in an attempt to remove the association. + let ptr = launder(false, true, false, ptr) as *mut (u8, u32, u64); + *ptr = (4, 4, 4); + assert!(value > 0); // UB: This reads a padding value! + } +} + + /// Delayed UB via mutable pointer write using `copy_nonoverlapping` under the hood. #[kani::proof] fn delayed_ub_copy() { diff --git a/tests/expected/uninit/delayed-ub/expected b/tests/expected/uninit/delayed-ub/expected index c493a56e228c..ae55f9cbc793 100644 --- a/tests/expected/uninit/delayed-ub/expected +++ b/tests/expected/uninit/delayed-ub/expected @@ -4,6 +4,12 @@ Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type VERIFICATION:- FAILED +Checking harness delayed_ub_closure_laundered... + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `u128` + +VERIFICATION:- FAILED + Checking harness delayed_ub_laundered... Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `u128` @@ -30,8 +36,9 @@ VERIFICATION:- FAILED Summary: Verification failed for - delayed_ub_copy +Verification failed for - delayed_ub_closure_laundered Verification failed for - delayed_ub_laundered Verification failed for - delayed_ub_static Verification failed for - delayed_ub_transmute Verification failed for - delayed_ub -Complete - 0 successfully verified harnesses, 5 failures, 5 total. +Complete - 0 successfully verified harnesses, 6 failures, 6 total.