-
Notifications
You must be signed in to change notification settings - Fork 97
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Fix size and alignment computation for intrinsics
Implement overflow checks for `size_of_val`, and panic for foreign types.
- Loading branch information
Showing
8 changed files
with
228 additions
and
13 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
112 changes: 112 additions & 0 deletions
112
kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,112 @@ | ||
| // Copyright Kani Contributors | ||
| // SPDX-License-Identifier: Apache-2.0 OR MIT | ||
| // | ||
| //! Module responsible for implementing a few Rust compiler intrinsics. | ||
| //! | ||
| //! Note that some rustc intrinsics are lowered to MIR instructions. Those can also be handled | ||
| //! here. | ||
| use crate::intrinsics::Intrinsic; | ||
| use crate::kani_middle::kani_functions::{KaniFunction, KaniModel}; | ||
| use crate::kani_middle::transform::body::{MutMirVisitor, MutableBody}; | ||
| use crate::kani_middle::transform::{TransformPass, TransformationType}; | ||
| use crate::kani_queries::QueryDb; | ||
| use rustc_middle::ty::TyCtxt; | ||
| use stable_mir::mir::mono::Instance; | ||
| use stable_mir::mir::{Body, ConstOperand, LocalDecl, Operand, Terminator, TerminatorKind}; | ||
| use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind}; | ||
| use std::collections::HashMap; | ||
| use tracing::debug; | ||
|
|
||
| /// Generate the body for a few Kani intrinsics. | ||
| #[derive(Debug)] | ||
| pub struct RustcIntrinsicsPass { | ||
| /// Used to cache FnDef lookups for intrinsics models. | ||
| models: HashMap<KaniModel, FnDef>, | ||
| } | ||
|
|
||
| impl TransformPass for RustcIntrinsicsPass { | ||
| fn transformation_type() -> TransformationType | ||
| where | ||
| Self: Sized, | ||
| { | ||
| TransformationType::Stubbing | ||
| } | ||
|
|
||
| fn is_enabled(&self, _query_db: &QueryDb) -> bool | ||
| where | ||
| Self: Sized, | ||
| { | ||
| true | ||
| } | ||
|
|
||
| /// Transform the function body by inserting checks one-by-one. | ||
| /// For every unsafe dereference or a transmute operation, we check all values are valid. | ||
| fn transform(&mut self, _tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { | ||
| debug!(function=?instance.name(), "transform"); | ||
| let mut new_body = MutableBody::from(body); | ||
| let mut visitor = ReplaceIntrinsicVisitor::new(&self.models, new_body.locals().to_vec()); | ||
| visitor.visit_body(&mut new_body); | ||
| (visitor.changed, new_body.into()) | ||
| } | ||
| } | ||
|
|
||
| impl RustcIntrinsicsPass { | ||
| pub fn new(queries: &QueryDb) -> Self { | ||
| let models = queries | ||
| .kani_functions() | ||
| .iter() | ||
| .filter_map(|(func, def)| { | ||
| if let KaniFunction::Model(model) = func { Some((*model, *def)) } else { None } | ||
| }) | ||
| .collect(); | ||
| debug!(?models, "RustcIntrinsicsPass::new"); | ||
| RustcIntrinsicsPass { models } | ||
| } | ||
| } | ||
|
|
||
| struct ReplaceIntrinsicVisitor<'a> { | ||
| models: &'a HashMap<KaniModel, FnDef>, | ||
| locals: Vec<LocalDecl>, | ||
| changed: bool, | ||
| } | ||
|
|
||
| impl<'a> ReplaceIntrinsicVisitor<'a> { | ||
| fn new(models: &'a HashMap<KaniModel, FnDef>, locals: Vec<LocalDecl>) -> Self { | ||
| ReplaceIntrinsicVisitor { models, locals, changed: false } | ||
| } | ||
| } | ||
|
|
||
| impl MutMirVisitor for ReplaceIntrinsicVisitor<'_> { | ||
| /// Replace the terminator for some intrinsics. | ||
| /// | ||
| /// Note that intrinsics must always be called directly. | ||
| fn visit_terminator(&mut self, term: &mut Terminator) { | ||
| if let TerminatorKind::Call { func, .. } = &mut term.kind { | ||
| if let TyKind::RigidTy(RigidTy::FnDef(def, args)) = | ||
| func.ty(&self.locals).unwrap().kind() | ||
| { | ||
| if def.is_intrinsic() { | ||
| let instance = Instance::resolve(def, &args).unwrap(); | ||
| let intrinsic = Intrinsic::from_instance(&instance); | ||
| debug!(?intrinsic, "handle_terminator"); | ||
| let model = match intrinsic { | ||
| Intrinsic::SizeOfVal => self.models[&KaniModel::SizeOfVal], | ||
| Intrinsic::MinAlignOfVal => self.models[&KaniModel::AlignOfVal], | ||
| // The rest is handled in codegen. | ||
| _ => { | ||
| return self.super_terminator(term); | ||
| } | ||
| }; | ||
| let new_instance = Instance::resolve(model, &args).unwrap(); | ||
| let literal = MirConst::try_new_zero_sized(new_instance.ty()).unwrap(); | ||
| let span = term.span; | ||
| let new_func = ConstOperand { span, user_ty: None, const_: literal }; | ||
| *func = Operand::Constant(new_func); | ||
| self.changed = true; | ||
| } | ||
| } | ||
| } | ||
| self.super_terminator(term); | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,20 @@ | ||
| Checking harness check_size_of_overflows... | ||
|
|
||
| safety_check\ | ||
| Status: FAILURE\ | ||
| Description: "failed to compute `size_of_val`" | ||
|
|
||
| Status: SUCCESS\ | ||
| Description: "assertion failed: unsafe { size_of_val_raw(new_ptr) } == expected_size" | ||
|
|
||
| Failed Checks: failed to compute `size_of_val` | ||
| VERIFICATION:- FAILED | ||
|
|
||
| Checking harness check_size_of_adt_overflows... | ||
|
|
||
| 0 of 2 cover properties satisfied (2 unreachable) | ||
| Failed Checks: failed to compute `size_of_val` | ||
| VERIFICATION:- FAILED | ||
|
|
||
| Verification failed for - check_size_of_overflows | ||
| Verification failed for - check_size_of_adt_overflows |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,53 @@ | ||
| // Copyright Kani Contributors | ||
| // SPDX-License-Identifier: Apache-2.0 OR MIT | ||
|
|
||
| //! This test case checks the behavior of `size_of_val_raw` for dynamically sized types. | ||
| #![feature(layout_for_ptr)] | ||
| #![feature(ptr_metadata)] | ||
|
|
||
| use std::mem::size_of_val_raw; | ||
| use std::ptr; | ||
|
|
||
| #[derive(Clone, Copy, kani::Arbitrary)] | ||
| struct Wrapper<T: ?Sized> { | ||
| _size: usize, | ||
| _value: T, | ||
| } | ||
|
|
||
| #[kani::proof] | ||
| pub fn check_size_of_adt_overflows() { | ||
| let var: Wrapper<[u64; 4]> = kani::any(); | ||
| let fat_ptr: *const Wrapper<[u64]> = &var as *const _; | ||
| let (thin_ptr, size) = fat_ptr.to_raw_parts(); | ||
| let new_size: usize = kani::any(); | ||
| let new_ptr: *const Wrapper<[u64]> = ptr::from_raw_parts(thin_ptr, new_size); | ||
| if let Some(slice_size) = new_size.checked_mul(size_of::<u64>()) { | ||
| if let Some(expected_size) = slice_size.checked_add(size_of::<usize>()) { | ||
| assert_eq!(unsafe { size_of_val_raw(new_ptr) }, expected_size); | ||
| } else { | ||
| // Expect UB detection | ||
| let _should_ub = unsafe { size_of_val_raw(new_ptr) }; | ||
| kani::cover!(true, "Expected unreachable"); | ||
| } | ||
| } else { | ||
| // Expect UB detection | ||
| let _should_ub = unsafe { size_of_val_raw(new_ptr) }; | ||
| kani::cover!(true, "Expected unreachable"); | ||
| } | ||
| } | ||
|
|
||
| #[kani::proof] | ||
| pub fn check_size_of_overflows() { | ||
| let var: [u64; 4] = kani::any(); | ||
| let fat_ptr: *const [u64] = &var as *const _; | ||
| let (thin_ptr, size) = fat_ptr.to_raw_parts(); | ||
| let new_size: usize = kani::any(); | ||
| let new_ptr: *const [u64] = ptr::from_raw_parts(thin_ptr, new_size); | ||
| if let Some(expected_size) = new_size.checked_mul(size_of::<u64>()) { | ||
| assert_eq!(unsafe { size_of_val_raw(new_ptr) }, expected_size); | ||
| } else { | ||
| // Expect UB detection | ||
| let _should_ub = unsafe { size_of_val_raw(new_ptr) }; | ||
| } | ||
| } |
File renamed without changes.