diff --git a/Cargo.lock b/Cargo.lock index 3b776124d1bb..87286ca982bf 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -230,9 +230,9 @@ dependencies = [ [[package]] name = "cc" -version = "1.2.13" +version = "1.2.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c7777341816418c02e033934a09f20dc0ccaf65a5201ef8a450ae0105a573fda" +checksum = "0c3d1b2e905a3a7b00a6141adb0e4c0bb941d11caf55349d863942a1cc44e3c9" dependencies = [ "shlex", ] @@ -282,9 +282,9 @@ dependencies = [ [[package]] name = "clap" -version = "4.5.28" +version = "4.5.29" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3e77c3243bd94243c03672cb5154667347c457ca271254724f9f393aee1c05ff" +checksum = "8acebd8ad879283633b343856142139f2da2317c96b05b4dd6181c61e2480184" dependencies = [ "clap_builder", "clap_derive", @@ -292,9 +292,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.5.27" +version = "4.5.29" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1b26884eb4b57140e4d2d93652abfa49498b938b3c9179f9fc487b0acc3edad7" +checksum = "f6ba32cbda51c7e1dfd49acc1457ba1a7dec5b64fe360e828acb13ca8dc9c2f9" dependencies = [ "anstream", "anstyle", @@ -471,9 +471,9 @@ dependencies = [ [[package]] name = "csv-core" -version = "0.1.11" +version = "0.1.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5efa2b3d7902f4b634a20cae3c9c4e6209dc4779feb6863329607560143efa70" +checksum = "7d02f3b0da4c6504f86e9cd789d8dbafab48c2321be74e9987593de5a894d93d" dependencies = [ "memchr", ] @@ -600,9 +600,9 @@ dependencies = [ [[package]] name = "equivalent" -version = "1.0.1" +version = "1.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5" +checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f" [[package]] name = "errno" @@ -1004,9 +1004,9 @@ checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a" [[package]] name = "miniz_oxide" -version = "0.8.3" +version = "0.8.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b8402cab7aefae129c6977bb0ff1b8fd9a04eb5b51efc50a70bea51cda0c7924" +checksum = "b3b1c9bd4fe1f0f8b387f6eb9eb3b4a1aa26185e5750efb9140301703f62cd1b" dependencies = [ "adler2", ] @@ -1303,9 +1303,9 @@ dependencies = [ [[package]] name = "psm" -version = "0.1.24" +version = "0.1.25" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "200b9ff220857e53e184257720a14553b2f4aa02577d2ed9842d45d4b9654810" +checksum = "f58e5423e24c18cc840e1c98370b3993c6649cd1678b4d24318bcf0a083cbe88" dependencies = [ "cc", ] @@ -1613,15 +1613,15 @@ dependencies = [ [[package]] name = "smallvec" -version = "1.13.2" +version = "1.14.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67" +checksum = "7fcf8323ef1faaee30a44a340193b1ac6814fd9b7b4e88e9d4519a3e4abe1cfd" [[package]] name = "stacker" -version = "0.1.17" +version = "0.1.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "799c883d55abdb5e98af1a7b3f23b9b6de8ecada0ecac058672d7635eb48ca7b" +checksum = "1d08feb8f695b465baed819b03c128dc23f57a694510ab1f06c77f763975685e" dependencies = [ "cc", "cfg-if", @@ -1697,9 +1697,9 @@ checksum = "f764005d11ee5f36500a149ace24e00e3da98b0158b3e2d53a7495660d3f4d60" [[package]] name = "tempfile" -version = "3.16.0" +version = "3.17.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "38c246215d7d24f48ae091a2902398798e05d978b24315d6efbc00ede9a8bb91" +checksum = "a40f762a77d2afa88c2d919489e390a12bdd261ed568e60cfa7e48d4e20f0d33" dependencies = [ "cfg-if", "fastrand", @@ -1845,9 +1845,9 @@ dependencies = [ [[package]] name = "toml_edit" -version = "0.22.23" +version = "0.22.24" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "02a8b472d1a3d7c18e2d61a489aee3453fd9031c33e4f55bd533f4a7adca1bee" +checksum = "17b4795ff5edd201c7cd6dca065ae59972ce77d1b80fa0a84d94950ece7d1474" dependencies = [ "indexmap", "serde", @@ -2193,9 +2193,9 @@ checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" [[package]] name = "winnow" -version = "0.7.1" +version = "0.7.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "86e376c75f4f43f44db463cf729e0d3acbf954d13e22c51e26e4c264b4ab545f" +checksum = "59690dea168f2198d1a3b0cac23b8063efcd11012f10ae4698f284808c8ef603" dependencies = [ "memchr", ] diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 2d876899f235..813e07d06723 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -251,19 +251,37 @@ impl GotocCtx<'_> { if *expected { r } else { Expr::not(r) } }; - let msg = if let AssertMessage::BoundsCheck { .. } = msg { - // For bounds check the following panic message is generated at runtime: - // "index out of bounds: the length is {len} but the index is {index}", - // but CBMC only accepts static messages so we don't add values to the message. - "index out of bounds: the length is less than or equal to the given index" - } else if let AssertMessage::MisalignedPointerDereference { .. } = msg { - // Misaligned pointer dereference check messages is also a runtime messages. - // Generate a generic one here. - "misaligned pointer dereference: address must be a multiple of its type's \ - alignment" - } else { + let (msg, property_class) = match msg { + AssertMessage::BoundsCheck { .. } => { + // For bounds check the following panic message is generated at runtime: + // "index out of bounds: the length is {len} but the index is {index}", + // but CBMC only accepts static messages so we don't add values to the message. + ( + "index out of bounds: the length is less than or equal to the given index", + PropertyClass::Assertion, + ) + } + AssertMessage::MisalignedPointerDereference { .. } => { + // Misaligned pointer dereference check messages is also a runtime messages. + // Generate a generic one here. + ( + "misaligned pointer dereference: address must be a multiple of its type's \ + alignment", + PropertyClass::SafetyCheck, + ) + } // For all other assert kind we can get the static message. - msg.description().unwrap() + AssertMessage::NullPointerDereference => { + (msg.description().unwrap(), PropertyClass::SafetyCheck) + } + AssertMessage::Overflow { .. } + | AssertMessage::OverflowNeg { .. } + | AssertMessage::DivisionByZero { .. } + | AssertMessage::RemainderByZero { .. } + | AssertMessage::ResumedAfterReturn { .. } + | AssertMessage::ResumedAfterPanic { .. } => { + (msg.description().unwrap(), PropertyClass::Assertion) + } }; let (msg_str, reach_stmt) = @@ -274,7 +292,7 @@ impl GotocCtx<'_> { reach_stmt, self.codegen_assert_assume( cond.cast_to(Type::bool()), - PropertyClass::Assertion, + property_class, &msg_str, loc, ), diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 73c887b3eeaf..e54a1fc4dd9e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -151,6 +151,43 @@ impl GotocHook for UnsupportedCheck { unreachable!("{UNEXPECTED_CALL}") } + fn handle( + &self, + gcx: &mut GotocCtx, + _instance: Instance, + mut fargs: Vec, + _assign_to: &Place, + target: Option, + span: Span, + ) -> Stmt { + assert_eq!(fargs.len(), 1); + let msg = fargs.pop().unwrap(); + let msg = gcx.extract_const_message(&msg).unwrap(); + let caller_loc = gcx.codegen_caller_span_stable(span); + if let Some(target) = target { + Stmt::block( + vec![ + gcx.codegen_assert_assume_false( + PropertyClass::UnsupportedConstruct, + &msg, + caller_loc, + ), + Stmt::goto(bb_label(target), caller_loc), + ], + caller_loc, + ) + } else { + gcx.codegen_assert_assume_false(PropertyClass::UnsupportedConstruct, &msg, caller_loc) + } + } +} + +struct SafetyCheck; +impl GotocHook for SafetyCheck { + fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool { + unreachable!("{UNEXPECTED_CALL}") + } + fn handle( &self, gcx: &mut GotocCtx, @@ -168,12 +205,7 @@ impl GotocHook for UnsupportedCheck { let caller_loc = gcx.codegen_caller_span_stable(span); Stmt::block( vec![ - gcx.codegen_assert_assume( - cond, - PropertyClass::UnsupportedConstruct, - &msg, - caller_loc, - ), + gcx.codegen_assert_assume(cond, PropertyClass::SafetyCheck, &msg, caller_loc), Stmt::goto(bb_label(target), caller_loc), ], caller_loc, @@ -181,8 +213,8 @@ impl GotocHook for UnsupportedCheck { } } -struct SafetyCheck; -impl GotocHook for SafetyCheck { +struct SafetyCheckNoAssume; +impl GotocHook for SafetyCheckNoAssume { fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool { unreachable!("{UNEXPECTED_CALL}") } @@ -204,7 +236,7 @@ impl GotocHook for SafetyCheck { let caller_loc = gcx.codegen_caller_span_stable(span); Stmt::block( vec![ - gcx.codegen_assert_assume(cond, PropertyClass::SafetyCheck, &msg, caller_loc), + gcx.codegen_assert(cond, PropertyClass::SafetyCheck, &msg, caller_loc), Stmt::goto(bb_label(target), caller_loc), ], caller_loc, @@ -738,6 +770,7 @@ pub fn fn_hooks() -> GotocHooks { (KaniHook::Cover, Rc::new(Cover)), (KaniHook::AnyRaw, Rc::new(Nondet)), (KaniHook::SafetyCheck, Rc::new(SafetyCheck)), + (KaniHook::SafetyCheckNoAssume, Rc::new(SafetyCheckNoAssume)), (KaniHook::IsAllocated, Rc::new(IsAllocated)), (KaniHook::PointerObject, Rc::new(PointerObject)), (KaniHook::PointerOffset, Rc::new(PointerOffset)), diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 3182ced8fa61..01d237bf0773 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -148,6 +148,8 @@ pub enum KaniHook { PointerOffset, #[strum(serialize = "SafetyCheckHook")] SafetyCheck, + #[strum(serialize = "SafetyCheckNoAssumeHook")] + SafetyCheckNoAssume, #[strum(serialize = "UnsupportedCheckHook")] UnsupportedCheck, #[strum(serialize = "UntrackedDerefHook")] diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index f2072fb21fb1..6f7b59041d12 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -181,23 +181,31 @@ impl MutableBody { check_type: &CheckType, source: &mut SourceInstruction, position: InsertPosition, - value: Local, + value: Option, msg: &str, ) { - assert_eq!( - self.locals[value].ty, - Ty::bool_ty(), - "Expected boolean value as the assert input" - ); let new_bb = self.blocks.len(); let span = source.span(&self.blocks); - let CheckType::Assert(assert_fn) = check_type; + let msg_op = self.new_str_operand(msg, span); + let (assert_fn, args) = match check_type { + CheckType::SafetyCheck(assert_fn) | CheckType::SafetyCheckNoAssume(assert_fn) => { + assert_eq!( + self.locals[value.unwrap()].ty, + Ty::bool_ty(), + "Expected boolean value as the assert input" + ); + (assert_fn, vec![Operand::Move(Place::from(value.unwrap())), msg_op]) + } + CheckType::UnsupportedCheck(assert_fn) => { + assert!(value.is_none()); + (assert_fn, vec![msg_op]) + } + }; let assert_op = Operand::Copy(Place::from(self.new_local(assert_fn.ty(), span, Mutability::Not))); - let msg_op = self.new_str_operand(msg, span); let kind = TerminatorKind::Call { func: assert_op, - args: vec![Operand::Move(Place::from(value)), msg_op], + args, destination: Place { local: self.new_local(Ty::new_tuple(&[]), span, Mutability::Not), projection: vec![], @@ -441,30 +449,35 @@ impl MutableBody { } } -// TODO: Remove this enum, since we now only support kani's assert. #[derive(Clone, Debug)] pub enum CheckType { - /// This is used by default when the `kani` crate is available. - Assert(Instance), + SafetyCheck(Instance), + SafetyCheckNoAssume(Instance), + UnsupportedCheck(Instance), } impl CheckType { - /// This will create the type of check that is available in the current crate, attempting to - /// create a check that generates an assertion following by an assumption of the same assertion. - pub fn new_assert_assume(queries: &QueryDb) -> CheckType { - let fn_def = queries.kani_functions()[&KaniHook::Assert.into()]; - CheckType::Assert(Instance::resolve(fn_def, &GenericArgs(vec![])).unwrap()) - } - - /// This will create the type of check that is available in the current crate, attempting to - /// create a check that generates an assertion, without assuming the condition afterwards. - /// - /// If `kani` crate is available, this will return [CheckType::Assert], and the instance will - /// point to `kani::assert`. Otherwise, we will collect the `core::panic_str` method and return - /// [CheckType::Panic]. - pub fn new_assert(queries: &QueryDb) -> CheckType { - let fn_def = queries.kani_functions()[&KaniHook::Check.into()]; - CheckType::Assert(Instance::resolve(fn_def, &GenericArgs(vec![])).unwrap()) + /// This will create the type of safety check that is available in the current crate, attempting + /// to create a check that generates an assertion following by an assumption of the same + /// assertion. + pub fn new_safety_check_assert_assume(queries: &QueryDb) -> CheckType { + let fn_def = queries.kani_functions()[&KaniHook::SafetyCheck.into()]; + CheckType::SafetyCheck(Instance::resolve(fn_def, &GenericArgs(vec![])).unwrap()) + } + + /// This will create the type of safety check that is available in the current crate, attempting + /// to create a check that generates an assertion, but not following by an assumption. + pub fn new_safety_check_assert_no_assume(queries: &QueryDb) -> CheckType { + let fn_def = queries.kani_functions()[&KaniHook::SafetyCheckNoAssume.into()]; + CheckType::SafetyCheckNoAssume(Instance::resolve(fn_def, &GenericArgs(vec![])).unwrap()) + } + + /// This will create the type of operation-unsupported check that is available in the current + /// crate, attempting to create a check that generates an assertion following by an assumption + /// of the same assertion. + pub fn new_unsupported_check_assert_assume_false(queries: &QueryDb) -> CheckType { + let fn_def = queries.kani_functions()[&KaniHook::UnsupportedCheck.into()]; + CheckType::UnsupportedCheck(Instance::resolve(fn_def, &GenericArgs(vec![])).unwrap()) } } 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 19d625da6c53..15d5af1dced6 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 @@ -33,13 +33,22 @@ mod instrumentation_visitor; #[derive(Debug)] pub struct DelayedUbPass { - pub check_type: CheckType, + pub safety_check_type: CheckType, + pub unsupported_check_type: CheckType, pub mem_init_fn_cache: HashMap, } impl DelayedUbPass { - pub fn new(check_type: CheckType, queries: &QueryDb) -> Self { - Self { check_type, mem_init_fn_cache: queries.kani_functions().clone() } + pub fn new( + safety_check_type: CheckType, + unsupported_check_type: CheckType, + queries: &QueryDb, + ) -> Self { + Self { + safety_check_type, + unsupported_check_type, + mem_init_fn_cache: queries.kani_functions().clone(), + } } } @@ -122,7 +131,8 @@ impl GlobalPass for DelayedUbPass { let (instrumentation_added, body) = UninitInstrumenter::run( body, instance, - self.check_type.clone(), + self.safety_check_type.clone(), + self.unsupported_check_type.clone(), &mut self.mem_init_fn_cache, target_finder, ); diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs index 892c2086c65c..e7178e2a7eb0 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -70,7 +70,8 @@ const SKIPPED_ITEMS: &[KaniFunction] = &[ /// Instruments the code with checks for uninitialized memory, agnostic to the source of targets. pub struct UninitInstrumenter<'a> { - check_type: CheckType, + safety_check_type: CheckType, + unsupported_check_type: CheckType, /// Used to cache FnDef lookups of injected memory initialization functions. mem_init_fn_cache: &'a mut HashMap, } @@ -80,11 +81,13 @@ impl<'a> UninitInstrumenter<'a> { pub(crate) fn run( body: Body, instance: Instance, - check_type: CheckType, + safety_check_type: CheckType, + unsupported_check_type: CheckType, mem_init_fn_cache: &'a mut HashMap, target_finder: impl TargetFinder, ) -> (bool, Body) { - let mut instrumenter = Self { check_type, mem_init_fn_cache }; + let mut instrumenter = + Self { safety_check_type, unsupported_check_type, mem_init_fn_cache }; let body = MutableBody::from(body); let (changed, new_body) = instrumenter.instrument(body, instance, target_finder); (changed, new_body.into()) @@ -134,12 +137,11 @@ impl<'a> UninitInstrumenter<'a> { source: &mut SourceInstruction, operation: MemoryInitOp, ) { - if let MemoryInitOp::Unsupported { reason } | MemoryInitOp::TriviallyUnsafe { reason } = - &operation - { - // If the operation is unsupported or trivially accesses uninitialized memory, encode - // the check as `assert!(false)`. - self.inject_assert_false(body, source, operation.position(), reason); + if let MemoryInitOp::Unsupported { reason } = &operation { + self.inject_unsupported_check(body, source, operation.position(), reason); + return; + } else if let MemoryInitOp::TriviallyUnsafe { reason } = &operation { + self.inject_safety_check(body, source, operation.position(), reason); return; }; @@ -162,7 +164,7 @@ impl<'a> UninitInstrumenter<'a> { let reason = format!( "Kani currently doesn't support checking memory initialization for pointers to `{pointee_ty}. {reason}", ); - self.inject_assert_false(body, source, operation.position(), &reason); + self.inject_unsupported_check(body, source, operation.position(), &reason); return; } } @@ -284,7 +286,7 @@ impl<'a> UninitInstrumenter<'a> { } PointeeLayout::TraitObject => { let reason = "Kani does not support reasoning about memory initialization of pointers to trait objects."; - self.inject_assert_false(body, source, operation.position(), reason); + self.inject_unsupported_check(body, source, operation.position(), reason); return; } PointeeLayout::Union { .. } => { @@ -292,7 +294,7 @@ impl<'a> UninitInstrumenter<'a> { // TODO: we perhaps need to check that the union at least contains an intersection // of all layouts initialized. let reason = "Interaction between raw pointers and unions is not yet supported."; - self.inject_assert_false(body, source, operation.position(), reason); + self.inject_unsupported_check(body, source, operation.position(), reason); return; } }; @@ -309,10 +311,10 @@ impl<'a> UninitInstrumenter<'a> { _ => unreachable!(), }; body.insert_check( - &self.check_type, + &self.safety_check_type, source, operation.position(), - ret_place.local, + Some(ret_place.local), &format!( "Undefined Behavior: Reading from an uninitialized pointer of type `{operand_ty}`" ), @@ -452,7 +454,7 @@ impl<'a> UninitInstrumenter<'a> { None => { let reason = "Interaction between raw pointers and unions is not yet supported."; - self.inject_assert_false(body, source, operation.position(), reason); + self.inject_unsupported_check(body, source, operation.position(), reason); return; } }; @@ -617,7 +619,7 @@ impl<'a> UninitInstrumenter<'a> { body.insert_bb(BasicBlock { statements, terminator }, source, operation.position()); } - fn inject_assert_false( + fn inject_safety_check( &self, body: &mut MutableBody, source: &mut SourceInstruction, @@ -631,7 +633,17 @@ impl<'a> UninitInstrumenter<'a> { user_ty: None, })); let result = body.insert_assignment(rvalue, source, position); - body.insert_check(&self.check_type, source, position, result, reason); + body.insert_check(&self.safety_check_type, source, position, Some(result), reason); + } + + fn inject_unsupported_check( + &self, + body: &mut MutableBody, + source: &mut SourceInstruction, + position: InsertPosition, + reason: &str, + ) { + body.insert_check(&self.unsupported_check_type, source, position, None, reason); } } diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs index b8a8806ec48a..3cba12bf21ee 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs @@ -30,7 +30,8 @@ mod uninit_visitor; /// pointers. #[derive(Debug)] pub struct UninitPass { - pub check_type: CheckType, + pub safety_check_type: CheckType, + pub unsupported_check_type: CheckType, pub mem_init_fn_cache: HashMap, } @@ -66,7 +67,8 @@ impl TransformPass for UninitPass { let (instrumentation_added, body) = UninitInstrumenter::run( new_body.into(), instance, - self.check_type.clone(), + self.safety_check_type.clone(), + self.unsupported_check_type.clone(), &mut self.mem_init_fn_cache, CheckUninitVisitor::new(), ); diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index e2c8a153c9a1..8689bf6c59ac 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -27,12 +27,12 @@ use stable_mir::abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape, use stable_mir::mir::mono::Instance; use stable_mir::mir::visit::{Location, PlaceContext, PlaceRef}; use stable_mir::mir::{ - AggregateKind, BasicBlockIdx, BinOp, Body, CastKind, ConstOperand, FieldIdx, Local, LocalDecl, - MirVisitor, Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, RawPtrKind, - Rvalue, Statement, StatementKind, Terminator, TerminatorKind, + AggregateKind, BasicBlockIdx, BinOp, Body, CastKind, FieldIdx, Local, LocalDecl, MirVisitor, + Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, RawPtrKind, Rvalue, + Statement, StatementKind, Terminator, TerminatorKind, }; use stable_mir::target::{MachineInfo, MachineSize}; -use stable_mir::ty::{AdtKind, IndexedVal, MirConst, RigidTy, Span, Ty, TyKind, UintTy}; +use stable_mir::ty::{AdtKind, IndexedVal, RigidTy, Span, Ty, TyKind, UintTy}; use std::fmt::Debug; use strum_macros::AsRefStr; use tracing::{debug, trace}; @@ -40,7 +40,8 @@ use tracing::{debug, trace}; /// Instrument the code with checks for invalid values. #[derive(Debug)] pub struct ValidValuePass { - pub check_type: CheckType, + pub safety_check_type: CheckType, + pub unsupported_check_type: CheckType, } impl TransformPass for ValidValuePass { @@ -92,10 +93,10 @@ impl ValidValuePass { let msg = format!("Undefined Behavior: Invalid value of type `{target_ty}`",); body.insert_check( - &self.check_type, + &self.safety_check_type, &mut source, InsertPosition::Before, - result, + Some(result), &msg, ); } @@ -106,10 +107,10 @@ impl ValidValuePass { let msg = format!("Undefined Behavior: Invalid value of type `{pointee_ty}`",); body.insert_check( - &self.check_type, + &self.safety_check_type, &mut source, InsertPosition::Before, - result, + Some(result), &msg, ); } @@ -130,14 +131,13 @@ impl ValidValuePass { source: &mut SourceInstruction, reason: &str, ) { - let span = source.span(body.blocks()); - let rvalue = Rvalue::Use(Operand::Constant(ConstOperand { - const_: MirConst::from_bool(false), - span, - user_ty: None, - })); - let result = body.insert_assignment(rvalue, source, InsertPosition::Before); - body.insert_check(&self.check_type, source, InsertPosition::Before, result, reason); + body.insert_check( + &self.unsupported_check_type, + source, + InsertPosition::Before, + None, + reason, + ); } } diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index d18b4b059063..343fc2fe0c92 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -39,7 +39,7 @@ use tracing::{debug, trace}; /// Generate the body for a few Kani intrinsics. #[derive(Debug)] pub struct IntrinsicGeneratorPass { - check_type: CheckType, + unsupported_check_type: CheckType, /// Used to cache FnDef lookups for models and Kani intrinsics. kani_defs: HashMap, /// Whether the user enabled uninitialized memory checks when they invoked Kani. @@ -86,11 +86,11 @@ impl TransformPass for IntrinsicGeneratorPass { } impl IntrinsicGeneratorPass { - pub fn new(check_type: CheckType, queries: &QueryDb) -> Self { + pub fn new(unsupported_check_type: CheckType, queries: &QueryDb) -> Self { let enable_uninit = queries.args().ub_check.contains(&ExtraChecks::Uninit); let kani_defs = queries.kani_functions().clone(); debug!(?kani_defs, ?enable_uninit, "IntrinsicGeneratorPass::new"); - IntrinsicGeneratorPass { check_type, enable_uninit, kani_defs } + IntrinsicGeneratorPass { unsupported_check_type, enable_uninit, kani_defs } } /// Generate the body for valid value. Which should be something like: @@ -151,21 +151,14 @@ impl IntrinsicGeneratorPass { } Err(msg) => { // We failed to retrieve all the valid ranges. - let rvalue = Rvalue::Use(Operand::Constant(ConstOperand { - const_: MirConst::from_bool(false), - span, - user_ty: None, - })); - let result = - new_body.insert_assignment(rvalue, &mut terminator, InsertPosition::Before); let reason = format!( "Kani currently doesn't support checking validity of `{target_ty}`. {msg}" ); new_body.insert_check( - &self.check_type, + &self.unsupported_check_type, &mut terminator, InsertPosition::Before, - result, + None, &reason, ); } @@ -314,39 +307,25 @@ impl IntrinsicGeneratorPass { ); } PointeeLayout::TraitObject => { - let rvalue = Rvalue::Use(Operand::Constant(ConstOperand { - const_: MirConst::from_bool(false), - span: source.span(new_body.blocks()), - user_ty: None, - })); - let result = - new_body.insert_assignment(rvalue, &mut source, InsertPosition::Before); let reason: &str = "Kani does not support reasoning about memory initialization of pointers to trait objects."; new_body.insert_check( - &self.check_type, + &self.unsupported_check_type, &mut source, InsertPosition::Before, - result, + None, &reason, ); } PointeeLayout::Union { .. } => { - let rvalue = Rvalue::Use(Operand::Constant(ConstOperand { - const_: MirConst::from_bool(false), - span: source.span(new_body.blocks()), - user_ty: None, - })); - let result = - new_body.insert_assignment(rvalue, &mut source, InsertPosition::Before); let reason: &str = "Kani does not yet support using initialization predicates on unions."; new_body.insert_check( - &self.check_type, + &self.unsupported_check_type, &mut source, InsertPosition::Before, - result, + None, &reason, ); } @@ -354,21 +333,14 @@ impl IntrinsicGeneratorPass { } Err(reason) => { // We failed to retrieve the type layout. - let rvalue = Rvalue::Use(Operand::Constant(ConstOperand { - const_: MirConst::from_bool(false), - span: source.span(new_body.blocks()), - user_ty: None, - })); - let result = - new_body.insert_assignment(rvalue, &mut source, InsertPosition::Before); let reason = format!( "Kani currently doesn't support checking memory initialization for pointers to `{pointee_ty}. {reason}", ); new_body.insert_check( - &self.check_type, + &self.unsupported_check_type, &mut source, InsertPosition::Before, - result, + None, &reason, ); } diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index d1eac474b47a..fbe9bebf42f8 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -72,7 +72,8 @@ impl BodyTransformation { inst_passes: vec![], cache: Default::default(), }; - let check_type = CheckType::new_assert_assume(queries); + let safety_check_type = CheckType::new_safety_check_assert_assume(queries); + let unsupported_check_type = CheckType::new_unsupported_check_assert_assume_false(queries); // This has to come first, since creating harnesses affects later stubbing and contract passes. transformer.add_pass(queries, AutomaticHarnessPass::new(unit, queries)); transformer.add_pass(queries, FnStubPass::new(&unit.stubs)); @@ -81,7 +82,13 @@ impl BodyTransformation { // This has to come after the contract pass since we want this to only replace the closure // body that is relevant for this harness. transformer.add_pass(queries, AnyModifiesPass::new(tcx, queries, &unit)); - transformer.add_pass(queries, ValidValuePass { check_type: check_type.clone() }); + transformer.add_pass( + queries, + ValidValuePass { + safety_check_type: safety_check_type.clone(), + unsupported_check_type: unsupported_check_type.clone(), + }, + ); // Putting `UninitPass` after `ValidValuePass` makes sure that the code generated by // `UninitPass` does not get unnecessarily instrumented by valid value checks. However, it // would also make sense to check that the values are initialized before checking their @@ -91,11 +98,13 @@ impl BodyTransformation { queries, UninitPass { // Since this uses demonic non-determinism under the hood, should not assume the assertion. - check_type: CheckType::new_assert(queries), + safety_check_type: CheckType::new_safety_check_assert_no_assume(queries), + unsupported_check_type: unsupported_check_type.clone(), mem_init_fn_cache: queries.kani_functions().clone(), }, ); - transformer.add_pass(queries, IntrinsicGeneratorPass::new(check_type, &queries)); + transformer + .add_pass(queries, IntrinsicGeneratorPass::new(unsupported_check_type, &queries)); transformer.add_pass(queries, LoopContractPass::new(tcx, queries, &unit)); transformer.add_pass(queries, RustcIntrinsicsPass::new(&queries)); transformer @@ -198,8 +207,14 @@ pub struct GlobalPasses { impl GlobalPasses { pub fn new(queries: &QueryDb, tcx: TyCtxt) -> Self { let mut global_passes = GlobalPasses { global_passes: vec![] }; - global_passes - .add_global_pass(queries, DelayedUbPass::new(CheckType::new_assert(queries), queries)); + global_passes.add_global_pass( + queries, + DelayedUbPass::new( + CheckType::new_safety_check_assert_assume(queries), + CheckType::new_unsupported_check_assert_assume_false(queries), + queries, + ), + ); global_passes.add_global_pass(queries, DumpMirPass::new(tcx)); global_passes } diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index d3940160a91a..51b243c9ad33 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -358,6 +358,18 @@ macro_rules! kani_intrinsics { assert!(cond, "Safety check failed: {msg}"); } + #[doc(hidden)] + #[allow(dead_code)] + #[kanitool::fn_marker = "SafetyCheckNoAssumeHook"] + #[inline(never)] + pub(crate) fn safety_check_no_assume(cond: bool, msg: &'static str) { + #[cfg(not(feature = "concrete_playback"))] + return kani_intrinsic(); + + #[cfg(feature = "concrete_playback")] + assert!(cond, "Safety check failed: {msg}"); + } + /// This should indicate that Kani does not support a certain operation. #[doc(hidden)] #[allow(dead_code)] diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index baf90ed98158..1ab8a5ead993 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -178,10 +178,11 @@ macro_rules! kani_mem { // stubbed. // We first assert that the data_ptr let data_ptr = ptr as *const (); - super::assert( - unsafe { is_allocated(data_ptr, 0) }, - "Kani does not support reasoning about pointer to unallocated memory", - ); + if !unsafe { is_allocated(data_ptr, 0) } { + crate::kani::unsupported( + "Kani does not support reasoning about pointer to unallocated memory", + ); + } unsafe { is_allocated(data_ptr, sz) } } } @@ -248,11 +249,11 @@ macro_rules! kani_mem { pub fn same_allocation(addr1: *const (), addr2: *const ()) -> bool { let obj1 = crate::kani::mem::pointer_object(addr1); (obj1 == crate::kani::mem::pointer_object(addr2)) && { - // TODO(3571): This should be a unsupported check - crate::kani::assert( - unsafe { is_allocated(addr1, 0) || is_allocated(addr2, 0) }, - "Kani does not support reasoning about pointer to unallocated memory", - ); + if !unsafe { is_allocated(addr1, 0) || is_allocated(addr2, 0) } { + crate::kani::unsupported( + "Kani does not support reasoning about pointer to unallocated memory", + ); + } unsafe { is_allocated(addr1, 0) && is_allocated(addr2, 0) } } } diff --git a/tests/expected/MemPredicates/adt_with_metadata.expected b/tests/expected/MemPredicates/adt_with_metadata.expected new file mode 100644 index 000000000000..b3d971a40e61 --- /dev/null +++ b/tests/expected/MemPredicates/adt_with_metadata.expected @@ -0,0 +1,4 @@ +Failed Checks: Kani does not support reasoning about pointer to unallocated memory + +Verification failed for - invalid_access::check_invalid_dyn_ptr +Complete - 3 successfully verified harnesses, 1 failures, 4 total. diff --git a/tests/kani/MemPredicates/adt_with_metadata.rs b/tests/expected/MemPredicates/adt_with_metadata.rs similarity index 98% rename from tests/kani/MemPredicates/adt_with_metadata.rs rename to tests/expected/MemPredicates/adt_with_metadata.rs index aa536b26279f..9ec0a3787964 100644 --- a/tests/kani/MemPredicates/adt_with_metadata.rs +++ b/tests/expected/MemPredicates/adt_with_metadata.rs @@ -42,7 +42,6 @@ mod invalid_access { use super::*; use std::ptr; #[kani::proof] - #[kani::should_panic] pub fn check_invalid_dyn_ptr() { unsafe fn new_dead_ptr(val: T) -> *const T { let local = val; diff --git a/tests/expected/MemPredicates/fat_ptr_validity.expected b/tests/expected/MemPredicates/fat_ptr_validity.expected new file mode 100644 index 000000000000..b57ca4986e60 --- /dev/null +++ b/tests/expected/MemPredicates/fat_ptr_validity.expected @@ -0,0 +1,5 @@ +Failed Checks: Kani does not support reasoning about pointer to unallocated memory + +Verification failed for - invalid_access::check_invalid_slice_ptr +Verification failed for - invalid_access::check_invalid_dyn_ptr +Complete - 4 successfully verified harnesses, 2 failures, 6 total. diff --git a/tests/kani/MemPredicates/fat_ptr_validity.rs b/tests/expected/MemPredicates/fat_ptr_validity.rs similarity index 97% rename from tests/kani/MemPredicates/fat_ptr_validity.rs rename to tests/expected/MemPredicates/fat_ptr_validity.rs index c4f037f3a646..f39392b62c5c 100644 --- a/tests/kani/MemPredicates/fat_ptr_validity.rs +++ b/tests/expected/MemPredicates/fat_ptr_validity.rs @@ -38,14 +38,12 @@ mod valid_access { mod invalid_access { use super::*; #[kani::proof] - #[kani::should_panic] pub fn check_invalid_dyn_ptr() { let raw_ptr: *const dyn PartialEq = unsafe { new_dead_ptr::(0) }; assert!(can_dereference(raw_ptr)); } #[kani::proof] - #[kani::should_panic] pub fn check_invalid_slice_ptr() { let raw_ptr: *const [char] = unsafe { new_dead_ptr::<[char; 2]>(['a', 'b']) }; assert!(can_dereference(raw_ptr)); diff --git a/tests/expected/MemPredicates/thin_ptr_validity.expected b/tests/expected/MemPredicates/thin_ptr_validity.expected new file mode 100644 index 000000000000..54245a84a491 --- /dev/null +++ b/tests/expected/MemPredicates/thin_ptr_validity.expected @@ -0,0 +1,5 @@ +Failed Checks: Kani does not support reasoning about pointer to unallocated memory + +Verification failed for - invalid_access::check_invalid_array +Verification failed for - invalid_access::check_invalid_ptr +Complete - 3 successfully verified harnesses, 2 failures, 5 total. diff --git a/tests/kani/MemPredicates/thin_ptr_validity.rs b/tests/expected/MemPredicates/thin_ptr_validity.rs similarity index 96% rename from tests/kani/MemPredicates/thin_ptr_validity.rs rename to tests/expected/MemPredicates/thin_ptr_validity.rs index 553c5beab9f8..519a07297192 100644 --- a/tests/kani/MemPredicates/thin_ptr_validity.rs +++ b/tests/expected/MemPredicates/thin_ptr_validity.rs @@ -32,14 +32,12 @@ mod valid_access { mod invalid_access { use super::*; #[kani::proof] - #[kani::should_panic] pub fn check_invalid_ptr() { let raw_ptr = unsafe { new_dead_ptr::(0) }; assert!(!can_dereference(raw_ptr)); } #[kani::proof] - #[kani::should_panic] pub fn check_invalid_array() { let raw_ptr = unsafe { new_dead_ptr::<[char; 2]>(['a', 'b']) }; assert!(can_dereference(raw_ptr)); diff --git a/tests/expected/issue-3571/issue_3571.expected b/tests/expected/issue-3571/issue_3571.expected new file mode 100644 index 000000000000..bed39a66b7af --- /dev/null +++ b/tests/expected/issue-3571/issue_3571.expected @@ -0,0 +1,9 @@ +Failed Checks: misaligned pointer dereference: address must be a multiple of its type's alignment + +Failed Checks: null pointer dereference occurred + +VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected) + +Verification failed for - rust_ub_should_fail +Verification failed for - rust_ub_fails +Complete - 0 successfully verified harnesses, 2 failures, 2 total. diff --git a/tests/expected/issue-3571/issue_3571.rs b/tests/expected/issue-3571/issue_3571.rs new file mode 100644 index 000000000000..c4d55f39b4e4 --- /dev/null +++ b/tests/expected/issue-3571/issue_3571.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +#[kani::should_panic] +pub fn rust_ub_fails() { + let ptr = 0 as *const u32; + let _invalid_ref = unsafe { &*ptr }; +} + +#[kani::proof] +#[kani::should_panic] +pub fn rust_ub_should_fail() { + let ptr = 10 as *const u32; + let _invalid_read = unsafe { *ptr }; +} diff --git a/tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.expected b/tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.expected new file mode 100644 index 000000000000..89a3572de316 --- /dev/null +++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.expected @@ -0,0 +1,4 @@ +Failed Checks: Kani currently doesn't support checking memory initialization for pointers to `E1. Cannot determine layout for an Enum of type E1, as it has multiple variants that have different padding. + +Verification failed for - access_padding_unsupported +Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/kani/Uninit/access-padding-enum-diverging-variants.rs b/tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.rs similarity index 97% rename from tests/kani/Uninit/access-padding-enum-diverging-variants.rs rename to tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.rs index fae491c40622..6f41961acb13 100644 --- a/tests/kani/Uninit/access-padding-enum-diverging-variants.rs +++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-diverging-variants.rs @@ -21,7 +21,6 @@ enum E2 { } #[kani::proof] -#[kani::should_panic] fn access_padding_unsupported() { let s = E1::A(0, 0); let ptr: *const u8 = addr_of!(s) as *const u8; diff --git a/tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.expected b/tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.expected new file mode 100644 index 000000000000..29fa17a972f5 --- /dev/null +++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.expected @@ -0,0 +1,7 @@ +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` + +Verification failed for - access_padding_uninit_b +Verification failed for - access_padding_uninit_a +Complete - 2 successfully verified harnesses, 2 failures, 4 total. diff --git a/tests/kani/Uninit/access-padding-enum-multiple-variants.rs b/tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.rs similarity index 96% rename from tests/kani/Uninit/access-padding-enum-multiple-variants.rs rename to tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.rs index dd6942252cb2..11c70dd7cd92 100644 --- a/tests/kani/Uninit/access-padding-enum-multiple-variants.rs +++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-multiple-variants.rs @@ -33,7 +33,6 @@ fn access_padding_init_b() { } #[kani::proof] -#[kani::should_panic] fn access_padding_uninit_a() { let s = E::A(0, 0); let ptr: *const u8 = addr_of!(s) as *const u8; @@ -41,7 +40,6 @@ fn access_padding_uninit_a() { } #[kani::proof] -#[kani::should_panic] fn access_padding_uninit_b() { let s = E::A(0, 0); let ptr: *const u8 = addr_of!(s) as *const u8; diff --git a/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.expected b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.expected new file mode 100644 index 000000000000..caab803ad09a --- /dev/null +++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.expected @@ -0,0 +1,5 @@ +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` + +Verification failed for - access_padding_uninit +Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/kani/Uninit/access-padding-enum-single-field.rs b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.rs similarity index 97% rename from tests/kani/Uninit/access-padding-enum-single-field.rs rename to tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.rs index 63f7f6043905..da1f2a202364 100644 --- a/tests/kani/Uninit/access-padding-enum-single-field.rs +++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-field.rs @@ -25,7 +25,6 @@ fn access_padding_init() { } #[kani::proof] -#[kani::should_panic] fn access_padding_uninit() { let s = E::A(0); let ptr: *const u8 = addr_of!(s) as *const u8; diff --git a/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.expected b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.expected new file mode 100644 index 000000000000..fa661dfbe329 --- /dev/null +++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.expected @@ -0,0 +1,4 @@ +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` + +Verification failed for - access_padding_uninit +Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/kani/Uninit/access-padding-enum-single-variant.rs b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.rs similarity index 97% rename from tests/kani/Uninit/access-padding-enum-single-variant.rs rename to tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.rs index bb87d36d26c8..9946fc83cee9 100644 --- a/tests/kani/Uninit/access-padding-enum-single-variant.rs +++ b/tests/expected/uninit/access-padding-uninit/access-padding-enum-single-variant.rs @@ -24,7 +24,6 @@ fn access_padding_init() { } #[kani::proof] -#[kani::should_panic] fn access_padding_uninit() { let s = E::A(0, 0); let ptr: *const u8 = addr_of!(s) as *const u8; diff --git a/tests/expected/uninit/access-padding-uninit/expected b/tests/expected/uninit/access-padding-uninit/access-padding-uninit.expected similarity index 100% rename from tests/expected/uninit/access-padding-uninit/expected rename to tests/expected/uninit/access-padding-uninit/access-padding-uninit.expected diff --git a/tests/expected/uninit/copy/expose_padding_via_copy.expected b/tests/expected/uninit/copy/expose_padding_via_copy.expected index 83d8badc8bf5..28686a566df4 100644 --- a/tests/expected/uninit/copy/expose_padding_via_copy.expected +++ b/tests/expected/uninit/copy/expose_padding_via_copy.expected @@ -1,8 +1,8 @@ -std::ptr::read::.assertion.1\ +std::ptr::read::.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u64`"\ -std::ptr::read::.assertion.2\ +std::ptr::read::.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`"\ diff --git a/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.expected b/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.expected index cbe7ec97cb7b..b9cdd6137592 100644 --- a/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.expected +++ b/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.expected @@ -1,8 +1,8 @@ -std::ptr::read::.assertion.1\ +std::ptr::read::.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u64`"\ -std::ptr::read::.assertion.2\ +std::ptr::read::.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`"\ diff --git a/tests/expected/uninit/copy/expose_padding_via_non_byte_copy.expected b/tests/expected/uninit/copy/expose_padding_via_non_byte_copy.expected index 3fc86e45a46e..d3b1db9bd498 100644 --- a/tests/expected/uninit/copy/expose_padding_via_non_byte_copy.expected +++ b/tests/expected/uninit/copy/expose_padding_via_non_byte_copy.expected @@ -1,8 +1,8 @@ -std::ptr::read::.assertion.1\ +std::ptr::read::.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u64`"\ -std::ptr::read::.assertion.2\ +std::ptr::read::.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`"\ diff --git a/tests/expected/uninit/copy/read_after_copy.expected b/tests/expected/uninit/copy/read_after_copy.expected index 56a3460a1d7b..c5d133d787b9 100644 --- a/tests/expected/uninit/copy/read_after_copy.expected +++ b/tests/expected/uninit/copy/read_after_copy.expected @@ -1,8 +1,8 @@ -std::ptr::read::.assertion.1\ +std::ptr::read::.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u64`"\ -std::ptr::read::.assertion.2\ +std::ptr::read::.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`"\ diff --git a/tests/expected/uninit/delayed-ub/delayed-ub.expected b/tests/expected/uninit/delayed-ub/delayed-ub.expected index f062a30cf6b0..d998801c2ca7 100644 --- a/tests/expected/uninit/delayed-ub/delayed-ub.expected +++ b/tests/expected/uninit/delayed-ub/delayed-ub.expected @@ -1,40 +1,40 @@ -delayed_ub_trigger_copy.assertion.\ +delayed_ub_trigger_copy.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"\ -delayed_ub_structs.assertion.\ +delayed_ub_structs.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `U`" -delayed_ub_double_copy.assertion.\ +delayed_ub_double_copy.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"\ -delayed_ub_copy.assertion.\ +delayed_ub_copy.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub_closure_capture_laundered.assertion.\ +delayed_ub_closure_capture_laundered.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub_closure_laundered.assertion.\ +delayed_ub_closure_laundered.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub_laundered.assertion.\ +delayed_ub_laundered.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub_static.assertion.\ +delayed_ub_static.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub_transmute.assertion.\ +delayed_ub_transmute.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub.assertion.\ +delayed_ub.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" diff --git a/tests/expected/uninit/intrinsics/expected b/tests/expected/uninit/intrinsics/expected index b40fe6714ba8..d19d694df75e 100644 --- a/tests/expected/uninit/intrinsics/expected +++ b/tests/expected/uninit/intrinsics/expected @@ -1,36 +1,32 @@ -std::ptr::write::>.assertion.1\ +std::ptr::read::>.unsupported_construct.\ - Status: FAILURE\ - Description: "Interaction between raw pointers and unions is not yet supported." -std::ptr::write::>.assertion.1\ - - Status: FAILURE\ - - Description: "Interaction between raw pointers and unions is not yet supported."\ - -check_typed_swap_nonoverlapping.assertion.1\ +check_typed_swap_nonoverlapping.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8`" -check_typed_swap_nonoverlapping.assertion.2\ +check_typed_swap_nonoverlapping.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8`" -check_volatile_load.assertion.1\ +check_volatile_load.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`" -check_compare_bytes.assertion.1\ +check_compare_bytes.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`" -check_compare_bytes.assertion.2\ +check_compare_bytes.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`" -std::ptr::read::.assertion.1\ +std::ptr::read::.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`" -std::ptr::read::.assertion.2\ +std::ptr::read::.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u8`" diff --git a/tests/expected/uninit/multiple-instrumentations.expected b/tests/expected/uninit/multiple-instrumentations.expected index 0f503b624ca4..82f37b22ed0d 100644 --- a/tests/expected/uninit/multiple-instrumentations.expected +++ b/tests/expected/uninit/multiple-instrumentations.expected @@ -1,16 +1,16 @@ -multiple_instrumentations_different_vars.assertion\ +multiple_instrumentations_different_vars.safety_check\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -multiple_instrumentations_different_vars.assertion\ +multiple_instrumentations_different_vars.safety_check\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`" -multiple_instrumentations.assertion\ +multiple_instrumentations.safety_check\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -multiple_instrumentations.assertion\ +multiple_instrumentations.safety_check\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" diff --git a/tests/expected/uninit/unions.expected b/tests/expected/uninit/unions.expected index ca7f777c4065..cf40fbb608df 100644 --- a/tests/expected/uninit/unions.expected +++ b/tests/expected/uninit/unions.expected @@ -1,28 +1,28 @@ -union_update_should_fail.assertion.1\ +union_update_should_fail.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`" -union_complex_subfields_should_fail.assertion.1\ +union_complex_subfields_should_fail.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u16`" -basic_union_should_fail.assertion.1\ +basic_union_should_fail.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`" -cross_function_union_should_fail::helper.assertion.1\ +cross_function_union_should_fail::helper.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`" -cross_function_multi_union_should_fail::helper.assertion.1\ +cross_function_multi_union_should_fail::helper.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`" -multi_cross_function_union_should_fail::sub_helper.assertion.1\ +multi_cross_function_union_should_fail::sub_helper.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u32`" -basic_multifield_union_should_fail.assertion.7\ +basic_multifield_union_should_fail.safety_check.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" diff --git a/tests/expected/valid-value-checks/constants.expected b/tests/expected/valid-value-checks/constants.expected new file mode 100644 index 000000000000..639e193bc561 --- /dev/null +++ b/tests/expected/valid-value-checks/constants.expected @@ -0,0 +1,10 @@ +Failed Checks: Undefined Behavior: Invalid value of type `[char; 2]` + +Failed Checks: Undefined Behavior: Invalid value of type `char` + +Failed Checks: Undefined Behavior: Invalid value of type `bool` + +Verification failed for - cast_to_invalid_offset +Verification failed for - cast_to_invalid_char +Verification failed for - transmute_invalid_bool +Complete - 3 successfully verified harnesses, 3 failures, 6 total. diff --git a/tests/kani/ValidValues/constants.rs b/tests/expected/valid-value-checks/constants.rs similarity index 93% rename from tests/kani/ValidValues/constants.rs rename to tests/expected/valid-value-checks/constants.rs index 5230e6e5e6cb..aa7aba6fe079 100644 --- a/tests/kani/ValidValues/constants.rs +++ b/tests/expected/valid-value-checks/constants.rs @@ -21,19 +21,16 @@ fn cast_to_valid_offset() { } #[kani::proof] -#[kani::should_panic] fn transmute_invalid_bool() { let _b = unsafe { std::mem::transmute::(2) }; } #[kani::proof] -#[kani::should_panic] fn cast_to_invalid_char() { let _c = unsafe { *(&u32::MAX as *const u32 as *const char) }; } #[kani::proof] -#[kani::should_panic] fn cast_to_invalid_offset() { let val = [100u32, u32::MAX]; let _c = unsafe { *(&val as *const [u32; 2] as *const [char; 2]) }; diff --git a/tests/expected/valid-value-checks/custom_niche.expected b/tests/expected/valid-value-checks/custom_niche.expected new file mode 100644 index 000000000000..3d78563ef8b1 --- /dev/null +++ b/tests/expected/valid-value-checks/custom_niche.expected @@ -0,0 +1,28 @@ +Failed Checks: Undefined Behavior: Invalid value of type `Rating` + +Failed Checks: Kani currently doesn't support checking validity of `copy_nonoverlapping` for `*const Rating` + +Failed Checks: Kani currently doesn't support checking validity of `copy_nonoverlapping` for `*const Rating` + +Failed Checks: Undefined Behavior: Invalid value of type `Rating` + +Failed Checks: Undefined Behavior: Invalid value of type `Rating` + +Failed Checks: Undefined Behavior: Invalid value of type `Rating` + +Failed Checks: Undefined Behavior: Invalid value of type `Rating` + +Failed Checks: Undefined Behavior: Invalid value of type `Rating` + +Failed Checks: Undefined Behavior: Invalid value of type `Rating` + +Verification failed for - check_invalid_increment +Verification failed for - check_copy_nonoverlap_ub +Verification failed for - check_copy_nonoverlap +Verification failed for - check_invalid_transmute_copy +Verification failed for - check_invalid_transmute +Verification failed for - check_invalid_dereference +Verification failed for - check_new_with_ub_limits +Verification failed for - check_unchecked_new_ub +Verification failed for - check_new_with_ub +Complete - 2 successfully verified harnesses, 9 failures, 11 total. diff --git a/tests/kani/ValidValues/custom_niche.rs b/tests/expected/valid-value-checks/custom_niche.rs similarity index 94% rename from tests/kani/ValidValues/custom_niche.rs rename to tests/expected/valid-value-checks/custom_niche.rs index b282fec3c645..c27bc6fdc057 100644 --- a/tests/kani/ValidValues/custom_niche.rs +++ b/tests/expected/valid-value-checks/custom_niche.rs @@ -38,41 +38,35 @@ impl Rating { } #[kani::proof] -#[kani::should_panic] pub fn check_new_with_ub() { assert_eq!(Rating::new(10), None); } #[kani::proof] -#[kani::should_panic] pub fn check_unchecked_new_ub() { let val = kani::any(); assert_eq!(unsafe { Rating::new_unchecked(val).stars }, val); } #[kani::proof] -#[kani::should_panic] pub fn check_new_with_ub_limits() { let stars = kani::any_where(|s: &u8| *s == 0 || *s > 5); let _ = Rating::new(stars); } #[kani::proof] -#[kani::should_panic] pub fn check_invalid_dereference() { let any: u8 = kani::any(); let _rating: Rating = unsafe { *(&any as *const _ as *const _) }; } #[kani::proof] -#[kani::should_panic] pub fn check_invalid_transmute() { let any: u8 = kani::any(); let _rating: Rating = unsafe { mem::transmute(any) }; } #[kani::proof] -#[kani::should_panic] pub fn check_invalid_transmute_copy() { let any: u8 = kani::any(); let _rating: Rating = unsafe { mem::transmute_copy(&any) }; @@ -82,7 +76,6 @@ pub fn check_invalid_transmute_copy() { /// /// FIX-ME: This is not supported today, and we fail due to unsupported check. #[kani::proof] -#[kani::should_panic] pub fn check_copy_nonoverlap() { let stars = kani::any_where(|s: &u8| *s == 0 || *s > 5); let mut rating: Rating = kani::any(); @@ -90,7 +83,6 @@ pub fn check_copy_nonoverlap() { } #[kani::proof] -#[kani::should_panic] pub fn check_copy_nonoverlap_ub() { let any: u8 = kani::any(); let mut rating: Rating = kani::any(); @@ -98,7 +90,6 @@ pub fn check_copy_nonoverlap_ub() { } #[kani::proof] -#[kani::should_panic] pub fn check_invalid_increment() { let mut orig: Rating = kani::any(); unsafe { orig.stars += 1 }; diff --git a/tests/expected/valid-value-checks/maybe_uninit.expected b/tests/expected/valid-value-checks/maybe_uninit.expected new file mode 100644 index 000000000000..8264876dc4f7 --- /dev/null +++ b/tests/expected/valid-value-checks/maybe_uninit.expected @@ -0,0 +1,5 @@ + ** 1 of 14 failed (1 unreachable)\ +Failed Checks: Undefined Behavior: Invalid value of type `std::num::NonZero` + +Verification failed for - check_invalid_zeroed +Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/kani/ValidValues/maybe_uninit.rs b/tests/expected/valid-value-checks/maybe_uninit.rs similarity index 96% rename from tests/kani/ValidValues/maybe_uninit.rs rename to tests/expected/valid-value-checks/maybe_uninit.rs index 620ad8ef5ba3..926277a744dc 100644 --- a/tests/kani/ValidValues/maybe_uninit.rs +++ b/tests/expected/valid-value-checks/maybe_uninit.rs @@ -14,7 +14,6 @@ pub fn check_valid_zeroed() { } #[kani::proof] -#[kani::should_panic] pub fn check_invalid_zeroed() { let maybe = MaybeUninit::zeroed(); let _val: NonZeroI64 = unsafe { maybe.assume_init() }; diff --git a/tests/expected/valid-value-checks/non_null.expected b/tests/expected/valid-value-checks/non_null.expected new file mode 100644 index 000000000000..bc8572b879c6 --- /dev/null +++ b/tests/expected/valid-value-checks/non_null.expected @@ -0,0 +1,7 @@ +Failed Checks: Undefined Behavior: Invalid value of type `std::ptr::NonNull` + +Failed Checks: Undefined Behavior: Invalid value of type `std::ptr::NonNull` + +Verification failed for - check_invalid_value_cfg +Verification failed for - check_invalid_value +Complete - 1 successfully verified harnesses, 2 failures, 3 total. diff --git a/tests/kani/ValidValues/non_null.rs b/tests/expected/valid-value-checks/non_null.rs similarity index 94% rename from tests/kani/ValidValues/non_null.rs rename to tests/expected/valid-value-checks/non_null.rs index 4874b61bf2d0..85d1a3876785 100644 --- a/tests/kani/ValidValues/non_null.rs +++ b/tests/expected/valid-value-checks/non_null.rs @@ -7,13 +7,11 @@ use std::num::NonZeroU8; use std::ptr::{self, NonNull}; #[kani::proof] -#[kani::should_panic] pub fn check_invalid_value() { let _ = unsafe { NonNull::new_unchecked(ptr::null_mut::()) }; } #[kani::proof] -#[kani::should_panic] pub fn check_invalid_value_cfg() { let nn = unsafe { NonNull::new_unchecked(ptr::null_mut::()) }; // This should be unreachable. TODO: Make this expected test. diff --git a/tests/expected/valid-value-checks/write_bytes.expected b/tests/expected/valid-value-checks/write_bytes.expected new file mode 100644 index 000000000000..8c14a9046d8d --- /dev/null +++ b/tests/expected/valid-value-checks/write_bytes.expected @@ -0,0 +1,5 @@ + ** 1 of 11 failed (1 unreachable)\ +Failed Checks: Undefined Behavior: Invalid value of type `char` + +Verification failed for - check_invalid_write +Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/kani/ValidValues/write_bytes.rs b/tests/expected/valid-value-checks/write_bytes.rs similarity index 96% rename from tests/kani/ValidValues/write_bytes.rs rename to tests/expected/valid-value-checks/write_bytes.rs index e4f73b1f3479..0b0ae6f343db 100644 --- a/tests/kani/ValidValues/write_bytes.rs +++ b/tests/expected/valid-value-checks/write_bytes.rs @@ -5,7 +5,6 @@ #![feature(core_intrinsics)] #[kani::proof] -#[kani::should_panic] pub fn check_invalid_write() { let mut val = 'a'; let ptr = &mut val as *mut char; diff --git a/tests/expected/valid-value-checks/write_invalid.expected b/tests/expected/valid-value-checks/write_invalid.expected new file mode 100644 index 000000000000..ba6c5b2ba65c --- /dev/null +++ b/tests/expected/valid-value-checks/write_invalid.expected @@ -0,0 +1,13 @@ + ** 1 of 19 failed (2 unreachable)\ +Failed Checks: Kani currently doesn't support checking validity of `transmute` for `std::option::Option>` + + ** 1 of 43 failed (2 unreachable)\ +Failed Checks: Kani currently doesn't support checking validity of `transmute` for `std::option::Option>` + + ** 1 of 18 failed (1 unreachable)\ +Failed Checks: Kani currently doesn't support checking validity of `transmute` for `std::option::Option>` + +Verification failed for - read_invalid_is_ub +Verification failed for - write_valid_before_read +Verification failed for - write_invalid_bytes_no_ub_with_spurious_cex +Complete - 0 successfully verified harnesses, 3 failures, 3 total. diff --git a/tests/kani/ValidValues/write_invalid.rs b/tests/expected/valid-value-checks/write_invalid.rs similarity index 94% rename from tests/kani/ValidValues/write_invalid.rs rename to tests/expected/valid-value-checks/write_invalid.rs index 05d3705bd69a..677ffe4edf61 100644 --- a/tests/kani/ValidValues/write_invalid.rs +++ b/tests/expected/valid-value-checks/write_invalid.rs @@ -9,7 +9,6 @@ use std::num::NonZeroU8; #[kani::proof] -#[kani::should_panic] pub fn write_invalid_bytes_no_ub_with_spurious_cex() { let mut non_zero: NonZeroU8 = kani::any(); let dest = &mut non_zero as *mut _; @@ -17,7 +16,6 @@ pub fn write_invalid_bytes_no_ub_with_spurious_cex() { } #[kani::proof] -#[kani::should_panic] pub fn write_valid_before_read() { let mut non_zero: NonZeroU8 = kani::any(); let mut non_zero_2: NonZeroU8 = kani::any(); @@ -28,7 +26,6 @@ pub fn write_valid_before_read() { } #[kani::proof] -#[kani::should_panic] pub fn read_invalid_is_ub() { let mut non_zero: NonZeroU8 = kani::any(); let dest = &mut non_zero as *mut _; diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index a5d84229dae9..00e33714d74b 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit a5d84229dae984a40ece44add3f418b00342fa01 +Subproject commit 00e33714d74b0646bc18ab65c90a45504a185828 diff --git a/tests/script-based-pre/cargo_playback_array/playback_target.sh b/tests/script-based-pre/cargo_playback_array/playback_target.sh deleted file mode 100755 index 17eaa66a01c6..000000000000 --- a/tests/script-based-pre/cargo_playback_array/playback_target.sh +++ /dev/null @@ -1,27 +0,0 @@ -#!/usr/bin/env bash -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -set +e - -function check_playback { - local OUTPUT=output.log - cargo kani playback "${@}" >& $OUTPUT - # Sort output so we can rely on the order. - echo "$(grep "test verify::.* ok" $OUTPUT | sort)" - echo - echo "======= Raw Output =======" - cat $OUTPUT - echo "==========================" - echo - rm $OUTPUT -} - -pushd sample_crate > /dev/null -cargo clean - -cargo kani --concrete-playback inplace -Z concrete-playback -check_playback -Z concrete-playback - -cargo clean -popd > /dev/null diff --git a/tests/script-based-pre/cargo_playback_array/sample_crate/Cargo.toml b/tests/script-based-pre/cargo_playback_array/sample_crate/Cargo.toml deleted file mode 100644 index 202362506011..000000000000 --- a/tests/script-based-pre/cargo_playback_array/sample_crate/Cargo.toml +++ /dev/null @@ -1,10 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT -[package] -name = "sample_crate" -version = "0.1.0" -edition = "2021" -doctest = false - -[lints.rust] -unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_playback_array/sample_crate/src/lib.rs b/tests/script-based-pre/playback_array/array.rs similarity index 100% rename from tests/script-based-pre/cargo_playback_array/sample_crate/src/lib.rs rename to tests/script-based-pre/playback_array/array.rs diff --git a/tests/script-based-pre/cargo_playback_array/config.yml b/tests/script-based-pre/playback_array/config.yml similarity index 54% rename from tests/script-based-pre/cargo_playback_array/config.yml rename to tests/script-based-pre/playback_array/config.yml index 99bfe39f95a5..88b420e8a6f0 100644 --- a/tests/script-based-pre/cargo_playback_array/config.yml +++ b/tests/script-based-pre/playback_array/config.yml @@ -1,4 +1,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -script: playback_target.sh -expected: playback_target.expected +script: playback_array.sh +expected: playback_array.expected diff --git a/tests/script-based-pre/cargo_playback_array/playback_target.expected b/tests/script-based-pre/playback_array/playback_array.expected similarity index 100% rename from tests/script-based-pre/cargo_playback_array/playback_target.expected rename to tests/script-based-pre/playback_array/playback_array.expected diff --git a/tests/script-based-pre/playback_array/playback_array.sh b/tests/script-based-pre/playback_array/playback_array.sh new file mode 100755 index 000000000000..3cceb8da6297 --- /dev/null +++ b/tests/script-based-pre/playback_array/playback_array.sh @@ -0,0 +1,22 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -e +set -o pipefail +set -o nounset + +cleanup() +{ + rm ${RS_FILE} +} +trap cleanup EXIT + +RS_FILE="modified.rs" +cp array.rs ${RS_FILE} + +echo "[TEST] Generate test..." +kani ${RS_FILE} -Z concrete-playback --concrete-playback=inplace || true + +echo "[TEST] Run test..." +kani playback -Z concrete-playback ${RS_FILE} || true