From 8a06d53c0d1eca07019fd8cddcf9b89f8acc800a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 25 Jul 2025 19:57:27 +0000 Subject: [PATCH 1/3] Add unstable option assume-no-panic Compute verification results under the assumption that no panic occurs. --- kani-compiler/src/args.rs | 4 ++++ .../src/codegen_cprover_gotoc/codegen/assert.rs | 17 ++++++++++++----- kani-driver/src/args/mod.rs | 11 +++++++++++ kani-driver/src/call_single_file.rs | 4 ++++ tests/kani/Panic/assume_no_panic.rs | 12 ++++++++++++ 5 files changed, 43 insertions(+), 5 deletions(-) create mode 100644 tests/kani/Panic/assume_no_panic.rs diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index af9d025e22b0..dc8f4a408ddb 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -37,6 +37,10 @@ pub enum ReachabilityType { /// with. Usually stored in and accessible via [`crate::kani_queries::QueryDb`]. #[derive(Debug, Default, Clone, clap::Parser)] pub struct Arguments { + /// Compute verification results under the assumption that no panic occurs. + /// This feature is unstable, and it requires `-Z unstable-options` to be used + #[clap(long)] + pub assume_no_panic: bool, /// Option used to disable asserting function contracts. #[clap(long)] pub no_assert_contracts: bool, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index b82a0c108424..cb24f40eef38 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -133,11 +133,18 @@ impl GotocCtx<'_> { message: &str, loc: Location, ) -> Stmt { - let property_name = property_class.as_str(); - Stmt::block( - vec![Stmt::assert(cond.clone(), property_name, message, loc), Stmt::assume(cond, loc)], - loc, - ) + if property_class == PropertyClass::Assertion && self.queries.args().assume_no_panic { + Stmt::assume(cond, loc) + } else { + let property_name = property_class.as_str(); + Stmt::block( + vec![ + Stmt::assert(cond.clone(), property_name, message, loc), + Stmt::assume(cond, loc), + ], + loc, + ) + } } /// Generate code to cover the given condition at the current location diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index ef413e228939..5546aa30a52f 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -212,6 +212,11 @@ pub enum CargoKaniSubcommand { #[derive(Debug, clap::Args)] #[clap(next_help_heading = "Verification Options")] pub struct VerificationArgs { + /// Compute verification results under the assumption that no panic occurs. + /// This feature is unstable, and it requires `-Z unstable-options` to be used + #[arg(long, hide_short_help = true)] + pub assume_no_panic: bool, + /// Link external C files referenced by Rust code. /// This is an experimental feature and requires `-Z c-ffi` to be used #[arg(long, hide = true, num_args(1..))] @@ -634,6 +639,12 @@ impl ValidateArgs for VerificationArgs { // check_unstable() calls: for each unstable option, check that the requisite unstable feature is provided. let unstable = || -> Result<(), Error> { + self.common_args.check_unstable( + self.assume_no_panic, + "assume-no-panic", + UnstableFeature::UnstableOptions, + )?; + self.common_args.check_unstable( self.concrete_playback.is_some(), "concrete-playback", diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index bdd9fdf52314..8238345d75b2 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -116,6 +116,10 @@ impl KaniSession { pub fn kani_compiler_local_flags(&self) -> Vec { let mut flags: Vec = vec![]; + if self.args.assume_no_panic { + flags.push("--assume-no-panic".into()); + } + if self.args.common_args.debug { flags.push("--log-level=debug".into()); } else if self.args.common_args.verbose { diff --git a/tests/kani/Panic/assume_no_panic.rs b/tests/kani/Panic/assume_no_panic.rs new file mode 100644 index 000000000000..5c3cc607b258 --- /dev/null +++ b/tests/kani/Panic/assume_no_panic.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z unstable-options --assume-no-panic +//! Test that --assume-no-panic works + +#[kani::proof] +fn div0() -> i32 { + let x: i32 = kani::any(); + let y: i32 = kani::any(); + x / y +} From b296ca16499d7a00aad3ca364c55bbcf917413fa Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Jul 2025 07:52:14 +0000 Subject: [PATCH 2/3] Rename option to prove-safety-only --- kani-compiler/src/args.rs | 8 +++---- .../codegen_cprover_gotoc/codegen/assert.rs | 2 +- kani-driver/src/args/mod.rs | 22 +++++++++---------- kani-driver/src/call_single_file.rs | 8 +++---- ...ssume_no_panic.rs => prove_safety_only.rs} | 4 ++-- 5 files changed, 22 insertions(+), 22 deletions(-) rename tests/kani/Panic/{assume_no_panic.rs => prove_safety_only.rs} (66%) diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index dc8f4a408ddb..f20dd8318fe6 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -37,10 +37,6 @@ pub enum ReachabilityType { /// with. Usually stored in and accessible via [`crate::kani_queries::QueryDb`]. #[derive(Debug, Default, Clone, clap::Parser)] pub struct Arguments { - /// Compute verification results under the assumption that no panic occurs. - /// This feature is unstable, and it requires `-Z unstable-options` to be used - #[clap(long)] - pub assume_no_panic: bool, /// Option used to disable asserting function contracts. #[clap(long)] pub no_assert_contracts: bool, @@ -69,6 +65,10 @@ pub struct Arguments { /// Option used for suppressing global ASM error. #[clap(long)] pub ignore_global_asm: bool, + /// Compute verification results under the assumption that no panic occurs. + /// This feature is unstable, and it requires `-Z unstable-options` to be used + #[clap(long)] + pub prove_safety_only: bool, /// Option name used to select which reachability analysis to perform. #[clap(long = "reachability", default_value = "none")] pub reachability_analysis: ReachabilityType, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index 131387ff5dff..907edf954065 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -133,7 +133,7 @@ impl GotocCtx<'_> { message: &str, loc: Location, ) -> Stmt { - if property_class == PropertyClass::Assertion && self.queries.args().assume_no_panic { + if property_class == PropertyClass::Assertion && self.queries.args().prove_safety_only { Stmt::assume(cond, loc) } else { let property_name = property_class.as_str(); diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 5546aa30a52f..52f621c2f027 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -212,11 +212,6 @@ pub enum CargoKaniSubcommand { #[derive(Debug, clap::Args)] #[clap(next_help_heading = "Verification Options")] pub struct VerificationArgs { - /// Compute verification results under the assumption that no panic occurs. - /// This feature is unstable, and it requires `-Z unstable-options` to be used - #[arg(long, hide_short_help = true)] - pub assume_no_panic: bool, - /// Link external C files referenced by Rust code. /// This is an experimental feature and requires `-Z c-ffi` to be used #[arg(long, hide = true, num_args(1..))] @@ -335,6 +330,11 @@ pub struct VerificationArgs { #[arg(long, hide = true)] pub print_llbc: bool, + /// Compute verification results under the assumption that no panic occurs. + /// This feature is unstable, and it requires `-Z unstable-options` to be used + #[arg(long, hide_short_help = true)] + pub prove_safety_only: bool, + /// Randomize the layout of structures. This option can help catching code that relies on /// a specific layout chosen by the compiler that is not guaranteed to be stable in the future. /// If a value is given, it will be used as the seed for randomization @@ -639,12 +639,6 @@ impl ValidateArgs for VerificationArgs { // check_unstable() calls: for each unstable option, check that the requisite unstable feature is provided. let unstable = || -> Result<(), Error> { - self.common_args.check_unstable( - self.assume_no_panic, - "assume-no-panic", - UnstableFeature::UnstableOptions, - )?; - self.common_args.check_unstable( self.concrete_playback.is_some(), "concrete-playback", @@ -737,6 +731,12 @@ impl ValidateArgs for VerificationArgs { UnstableFeature::FunctionContracts, )?; + self.common_args.check_unstable( + self.prove_safety_only, + "prove-safety-only", + UnstableFeature::UnstableOptions, + )?; + Ok(()) }; diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 8238345d75b2..dc962b0b1063 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -116,10 +116,6 @@ impl KaniSession { pub fn kani_compiler_local_flags(&self) -> Vec { let mut flags: Vec = vec![]; - if self.args.assume_no_panic { - flags.push("--assume-no-panic".into()); - } - if self.args.common_args.debug { flags.push("--log-level=debug".into()); } else if self.args.common_args.verbose { @@ -179,6 +175,10 @@ impl KaniSession { flags.extend(args.into_iter().map(KaniArg::from)); } + if self.args.prove_safety_only { + flags.push("--prove-safety-only".into()); + } + flags.extend(self.args.common_args.unstable_features.as_arguments().map(KaniArg::from)); flags diff --git a/tests/kani/Panic/assume_no_panic.rs b/tests/kani/Panic/prove_safety_only.rs similarity index 66% rename from tests/kani/Panic/assume_no_panic.rs rename to tests/kani/Panic/prove_safety_only.rs index 5c3cc607b258..00bd5e40d94b 100644 --- a/tests/kani/Panic/assume_no_panic.rs +++ b/tests/kani/Panic/prove_safety_only.rs @@ -1,8 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: -Z unstable-options --assume-no-panic -//! Test that --assume-no-panic works +// kani-flags: -Z unstable-options --prove-safety-only +//! Test that --prove-safety-only works #[kani::proof] fn div0() -> i32 { From aee5da3278dbc43ab8a56aa6e0fbd12479898356 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Jul 2025 08:14:54 +0000 Subject: [PATCH 3/3] Additional test --- tests/kani/Panic/prove_safety_only.rs | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/tests/kani/Panic/prove_safety_only.rs b/tests/kani/Panic/prove_safety_only.rs index 00bd5e40d94b..76d9d6b31cca 100644 --- a/tests/kani/Panic/prove_safety_only.rs +++ b/tests/kani/Panic/prove_safety_only.rs @@ -10,3 +10,13 @@ fn div0() -> i32 { let y: i32 = kani::any(); x / y } + +#[kani::proof] +fn assert_hides_ub() { + let arr: [u8; 5] = kani::any(); + let mut bytes = kani::slice::any_slice_of_array(&arr); + let slice_offset = unsafe { bytes.as_ptr().offset_from(&arr as *const u8) }; + let offset: usize = kani::any(); + assert!(offset <= 4 && (slice_offset as usize) + offset <= 4); + let _ = unsafe { *bytes.as_ptr().add(offset) }; +}