diff --git a/cprover_bindings/src/env.rs b/cprover_bindings/src/env.rs index 42080e52119a..d31d213aa7d2 100644 --- a/cprover_bindings/src/env.rs +++ b/cprover_bindings/src/env.rs @@ -8,7 +8,7 @@ //! c.f. CBMC code [src/ansi-c/ansi_c_internal_additions.cpp]. //! One possible invocation of this insertion in CBMC can be found in \[ansi_c_languaget::parse\]. -use super::goto_program::{Expr, Location, Symbol, Type}; +use super::goto_program::{Expr, Location, Symbol, SymbolTable, Type}; use super::MachineModel; use num::bigint::BigInt; fn int_constant(name: &str, value: T) -> Symbol @@ -71,6 +71,8 @@ pub fn machine_model_symbols(mm: &MachineModel) -> Vec { ] } +const DEAD_OBJECT_IDENTIFIER: &str = "__CPROVER_dead_object"; + pub fn additional_env_symbols() -> Vec { vec![ Symbol::builtin_function("__CPROVER_initialize", vec![], Type::empty()), @@ -82,5 +84,16 @@ pub fn additional_env_symbols() -> Vec { Location::none(), ) .with_is_extern(true), + Symbol::static_variable( + DEAD_OBJECT_IDENTIFIER, + DEAD_OBJECT_IDENTIFIER, + Type::void_pointer(), + Location::none(), + ) + .with_is_extern(true), ] } + +pub fn global_dead_object(symbol_table: &SymbolTable) -> Expr { + symbol_table.lookup(DEAD_OBJECT_IDENTIFIER).unwrap().to_expr() +} diff --git a/cprover_bindings/src/irep/goto_binary_serde.rs b/cprover_bindings/src/irep/goto_binary_serde.rs index 324c5e764d1a..6f821768f996 100644 --- a/cprover_bindings/src/irep/goto_binary_serde.rs +++ b/cprover_bindings/src/irep/goto_binary_serde.rs @@ -11,7 +11,7 @@ use std::io::{self, BufReader}; use std::io::{BufWriter, Bytes, Error, ErrorKind, Read, Write}; use std::path::Path; -/// Writes a symbol table to a file in goto binary format in version 5. +/// Writes a symbol table to a file in goto binary format in version 6. /// /// In CBMC, the serialization rules are defined in : /// - src/goto-programs/write_goto_binary.h @@ -26,7 +26,7 @@ pub fn write_goto_binary_file(filename: &Path, source: &crate::goto_program::Sym serializer.write_file(irep_symbol_table); } -/// Reads a symbol table from a file expected to be in goto binary format in version 5. +/// Reads a symbol table from a file expected to be in goto binary format in version 6. // /// In CBMC, the deserialization rules are defined in : /// - src/goto-programs/read_goto_binary.h @@ -540,7 +540,7 @@ where assert!(written == 4); // Write goto binary version - self.write_usize_varenc(5); + self.write_usize_varenc(6); } /// Writes the symbol table using the GOTO binary file format to the byte stream. @@ -921,12 +921,12 @@ where // Read goto binary version let goto_binary_version = self.read_usize_varenc()?; - if goto_binary_version != 5 { + if goto_binary_version != 6 { return Err(Error::new( ErrorKind::Other, format!( "Unsupported GOTO binary version: {}. Supported version: {}", - goto_binary_version, 5 + goto_binary_version, 6 ), )); } diff --git a/cprover_bindings/src/irep/irep_id.rs b/cprover_bindings/src/irep/irep_id.rs index 9d52f4ef32fa..69962edf150e 100644 --- a/cprover_bindings/src/irep/irep_id.rs +++ b/cprover_bindings/src/irep/irep_id.rs @@ -366,7 +366,7 @@ pub enum IrepId { Div, Power, FactorialPower, - PrettyName, + CPrettyName, CClass, CField, CInterface, @@ -1242,7 +1242,7 @@ impl Display for IrepId { IrepId::Div => "/", IrepId::Power => "**", IrepId::FactorialPower => "factorial_power", - IrepId::PrettyName => "pretty_name", + IrepId::CPrettyName => "#pretty_name", IrepId::CClass => "#class", IrepId::CField => "#field", IrepId::CInterface => "#interface", diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 05774fdf8b43..bf0b8ce862dd 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -132,7 +132,7 @@ impl ToIrep for DatatypeComponent { match self { DatatypeComponent::Field { name, typ } => Irep::just_named_sub(linear_map![ (IrepId::Name, Irep::just_string_id(name.to_string())), - (IrepId::PrettyName, Irep::just_string_id(name.to_string())), + (IrepId::CPrettyName, Irep::just_string_id(name.to_string())), (IrepId::Type, typ.to_irep(mm)), ]), DatatypeComponent::Padding { name, bits } => Irep::just_named_sub(linear_map![ diff --git a/cprover_bindings/src/lib.rs b/cprover_bindings/src/lib.rs index e77b29a24ca2..a5901afbac2d 100644 --- a/cprover_bindings/src/lib.rs +++ b/cprover_bindings/src/lib.rs @@ -33,6 +33,7 @@ #![feature(f16)] mod env; +pub use env::global_dead_object; pub mod goto_program; pub mod irep; mod machine_model; diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index e4b7a4435b0f..3efc5c0f4f61 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -74,9 +74,6 @@ pub struct Arguments { /// Enable specific checks. #[clap(long)] pub ub_check: Vec, - /// Ignore storage markers. - #[clap(long)] - pub ignore_storage_markers: bool, } #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)] diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 697cacd3b191..b8db1a3d52b6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -75,18 +75,68 @@ impl<'tcx> GotocCtx<'tcx> { .goto_expr; self.codegen_set_discriminant(dest_ty, dest_expr, *variant_index, location) } + // StorageLive and StorageDead are modelled via CBMC's internal means of detecting + // accesses to dangling pointers, which uses demonic non-determinism. That is, CBMC + // non-deterministically chooses a single object's address to be tracked in a + // pointer-typed global instrumentation variable __CPROVER_dead_object. Any dereference + // entails a check that the pointer being dereferenced is not equal to the pointer held + // in __CPROVER_dead_object. We use this to bridge the difference between Rust and MIR + // semantics as follows: + // + // 1. (At the time of writing) MIR declares all function-local variables at function + // scope, irrespective of the scope/block that Rust code originally used. + // 2. In MIR, StorageLive and StorageDead markers are inserted at the beginning and end + // of the Rust block to record the Rust-level lifetime of the object. + // 3. We translate MIR declarations into GOTO declarations, implying that we will have + // a single object per function for a local variable, even when Rust had a variable + // declared in a sub-scope of the function where said scope was entered multiple + // times (e.g., a loop body). + // 4. To enable detection of use of dangling pointers, we now use + // __CPROVER_dead_object, unless the address of the local object is never taken + // (implying that there cannot be a use of a dangling pointer with respect to said + // object). We update __CPROVER_dead_object as follows: + // * StorageLive is set to NULL when __CPROVER_dead_object pointed to the object + // (re-)entering scope, or else is left unchanged. + // * StorageDead non-deterministically updates (or leaves unchanged) + // __CPROVER_dead_object to point to the object going out of scope. (This is the + // same update approach as used within CBMC.) + // + // This approach will also work when there are multiple occurrences of StorageLive (or + // StorageDead) on a path, or across control-flow branches, and even when StorageDead + // occurs without a preceding StorageLive. StatementKind::StorageLive(var_id) => { - if self.queries.args().ignore_storage_markers { + if !self.current_fn().is_address_taken_local(*var_id) { Stmt::skip(location) } else { - Stmt::decl(self.codegen_local(*var_id, location), None, location) + let global_dead_object = cbmc::global_dead_object(&self.symbol_table); + Stmt::assign( + global_dead_object.clone(), + global_dead_object + .clone() + .eq(self + .codegen_local(*var_id, location) + .address_of() + .cast_to(global_dead_object.typ().clone())) + .ternary(global_dead_object.typ().null(), global_dead_object), + location, + ) } } StatementKind::StorageDead(var_id) => { - if self.queries.args().ignore_storage_markers { + if !self.current_fn().is_address_taken_local(*var_id) { Stmt::skip(location) } else { - Stmt::dead(self.codegen_local(*var_id, location), location) + let global_dead_object = cbmc::global_dead_object(&self.symbol_table); + Stmt::assign( + global_dead_object.clone(), + Type::bool().nondet().ternary( + self.codegen_local(*var_id, location) + .address_of() + .cast_to(global_dead_object.typ().clone()), + global_dead_object, + ), + location, + ) } } StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping( @@ -424,6 +474,7 @@ impl<'tcx> GotocCtx<'tcx> { .branches() .map(|(c, bb)| { Expr::int_constant(c, switch_ty.clone()) + .with_location(loc) .switch_case(Stmt::goto(bb_label(bb), loc)) }) .collect(); diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs index 32c5d72f7007..ea3c9e909eb6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs @@ -7,9 +7,9 @@ use cbmc::InternedString; use rustc_middle::ty::Instance as InstanceInternal; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; -use stable_mir::mir::{Body, Local, LocalDecl}; +use stable_mir::mir::{visit::Location, visit::MirVisitor, Body, Local, LocalDecl, Rvalue}; use stable_mir::CrateDef; -use std::collections::HashMap; +use std::collections::{HashMap, HashSet}; /// This structure represents useful data about the function we are currently compiling. #[derive(Debug)] @@ -26,6 +26,8 @@ pub struct CurrentFnCtx<'tcx> { locals: Vec, /// A list of pretty names for locals that corrspond to user variables. local_names: HashMap, + /// Collection of variables that are used in a reference or address-of expression. + address_taken_locals: HashSet, /// The symbol name of the current function name: String, /// A human readable pretty name for the current function @@ -34,6 +36,24 @@ pub struct CurrentFnCtx<'tcx> { temp_var_counter: u64, } +struct AddressTakenLocalsCollector { + /// Locals that appear in `Rvalue::Ref` or `Rvalue::AddressOf` expressions. + address_taken_locals: HashSet, +} + +impl MirVisitor for AddressTakenLocalsCollector { + fn visit_rvalue(&mut self, rvalue: &Rvalue, _location: Location) { + match rvalue { + Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => { + if p.projection.is_empty() { + self.address_taken_locals.insert(p.local); + } + } + _ => (), + } + } +} + /// Constructor impl<'tcx> CurrentFnCtx<'tcx> { pub fn new(instance: Instance, gcx: &GotocCtx<'tcx>, body: &Body) -> Self { @@ -46,6 +66,8 @@ impl<'tcx> CurrentFnCtx<'tcx> { .iter() .filter_map(|info| info.local().map(|local| (local, (&info.name).into()))) .collect::>(); + let mut visitor = AddressTakenLocalsCollector { address_taken_locals: HashSet::new() }; + visitor.visit_body(body); Self { block: vec![], instance, @@ -53,6 +75,7 @@ impl<'tcx> CurrentFnCtx<'tcx> { krate: instance.def.krate().name, locals, local_names, + address_taken_locals: visitor.address_taken_locals, name, readable_name, temp_var_counter: 0, @@ -106,6 +129,10 @@ impl<'tcx> CurrentFnCtx<'tcx> { pub fn local_name(&self, local: Local) -> Option { self.local_names.get(&local).copied() } + + pub fn is_address_taken_local(&self, local: Local) -> bool { + self.address_taken_locals.contains(&local) + } } /// Utility functions diff --git a/kani-dependencies b/kani-dependencies index 844d83c23dc7..421188a08762 100644 --- a/kani-dependencies +++ b/kani-dependencies @@ -1,6 +1,6 @@ -CBMC_MAJOR="5" -CBMC_MINOR="95" -CBMC_VERSION="5.95.1" +CBMC_MAJOR="6" +CBMC_MINOR="1" +CBMC_VERSION="6.1.1" # If you update this version number, remember to bump it in `src/setup.rs` too CBMC_VIEWER_MAJOR="3" diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index d043035bcab2..158f1c001b5b 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -245,14 +245,6 @@ pub struct VerificationArgs { #[arg(long, hide_short_help = true, requires("enable_unstable"))] pub ignore_global_asm: bool, - /// Ignore lifetimes of local variables. This effectively extends their - /// lifetimes to the function scope, and hence may cause Kani to miss - /// undefined behavior resulting from using the variable after it dies. - /// This option may impact the soundness of the analysis and may cause false - /// proofs and/or counterexamples - #[arg(long, hide_short_help = true, requires("enable_unstable"))] - pub ignore_locals_lifetime: bool, - /// Write the GotoC symbol table to a file in JSON format instead of goto binary format. #[arg(long, hide_short_help = true)] pub write_json_symtab: bool, diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 81d50865cc13..387a9723fcdb 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -153,6 +153,11 @@ impl KaniSession { args.push(file.to_owned().into_os_string()); + // Make CBMC verbose by default to tell users about unwinding progress. This should be + // reviewed as CBMC's verbosity defaults evolve. + args.push("--verbosity".into()); + args.push("9".into()); + Ok(args) } @@ -160,18 +165,25 @@ impl KaniSession { pub fn cbmc_check_flags(&self) -> Vec { let mut args = Vec::new(); - if self.args.checks.memory_safety_on() { - args.push("--bounds-check".into()); - args.push("--pointer-check".into()); + // We assume that malloc cannot fail, see https://github.com/model-checking/kani/issues/891 + args.push("--no-malloc-may-fail".into()); + + // With PR #2630 we generate the appropriate checks directly rather than relying on CBMC's + // checks (which are for C semantics). + args.push("--no-undefined-shift-check".into()); + // With PR #647 we use Rust's `-C overflow-checks=on` instead of: + // --unsigned-overflow-check + // --signed-overflow-check + // So these options are deliberately skipped to avoid erroneously re-checking operations. + args.push("--no-signed-overflow-check".into()); + + if !self.args.checks.memory_safety_on() { + args.push("--no-bounds-check".into()); + args.push("--no-pointer-check".into()); } if self.args.checks.overflow_on() { - args.push("--div-by-zero-check".into()); args.push("--float-overflow-check".into()); args.push("--nan-check".into()); - // With PR #647 we use Rust's `-C overflow-checks=on` instead of: - // --unsigned-overflow-check - // --signed-overflow-check - // So these options are deliberately skipped to avoid erroneously re-checking operations. // TODO: Implement conversion checks as an optional check. // They are a well defined operation in rust, but they may yield unexpected results to @@ -179,11 +191,13 @@ impl KaniSession { // We might want to create a transformation pass instead of enabling CBMC since Kani // compiler sometimes rely on the bitwise conversion of signed <-> unsigned. // args.push("--conversion-check".into()); + } else { + args.push("--no-div-by-zero-check".into()); } - if self.args.checks.unwinding_on() { - // TODO: With CBMC v6 the below can be removed as those are defaults. - args.push("--unwinding-assertions".into()); + if !self.args.checks.unwinding_on() { + args.push("--no-unwinding-assertions".into()); + } else { args.push("--no-self-loops-to-assumptions".into()); } @@ -192,7 +206,8 @@ impl KaniSession { // still catch any invalid dereference with --pointer-check. Thus, only enable them // if the user explicitly request them. args.push("--pointer-overflow-check".into()); - args.push("--pointer-primitive-check".into()); + } else { + args.push("--no-pointer-primitive-check".into()); } args diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index 83744eddabfd..ae76be150871 100644 --- a/kani-driver/src/call_goto_instrument.rs +++ b/kani-driver/src/call_goto_instrument.rs @@ -93,6 +93,7 @@ impl KaniSession { fn add_library(&self, file: &Path) -> Result<()> { let args: Vec = vec![ "--add-library".into(), + "--no-malloc-may-fail".into(), file.to_owned().into_os_string(), // input file.to_owned().into_os_string(), // output ]; @@ -173,6 +174,7 @@ impl KaniSession { assigns.contracted_function_name.as_str().into(), "--nondet-static-exclude".into(), assigns.recursion_tracker.as_str().into(), + "--no-malloc-may-fail".into(), file.into(), file.into(), ]; diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 411dabb5270e..bbeb5bfa417d 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -146,10 +146,6 @@ impl KaniSession { flags.push("--ub-check=uninit".into()); } - if self.args.ignore_locals_lifetime { - flags.push("--ignore-storage-markers".into()) - } - flags.extend(self.args.common_args.unstable_features.as_arguments().map(str::to_string)); // This argument will select the Kani flavour of the compiler. It will be removed before diff --git a/kani-driver/src/cbmc_output_parser.rs b/kani-driver/src/cbmc_output_parser.rs index 127f98beab56..b3a78e8d03e2 100644 --- a/kani-driver/src/cbmc_output_parser.rs +++ b/kani-driver/src/cbmc_output_parser.rs @@ -329,6 +329,7 @@ pub enum CheckStatus { Satisfied, // for `cover` properties only Success, Undetermined, + Unknown, Unreachable, Uncovered, // for `code_coverage` properties only Unsatisfiable, // for `cover` properties only @@ -344,6 +345,9 @@ impl std::fmt::Display for CheckStatus { CheckStatus::Failure => style("FAILURE").red(), CheckStatus::Unreachable => style("UNREACHABLE").yellow(), CheckStatus::Undetermined => style("UNDETERMINED").yellow(), + // CBMC 6+ uses UNKNOWN when another property of undefined behavior failed, making it + // impossible to definitively conclude whether other properties hold or not. + CheckStatus::Unknown => style("UNDETERMINED").yellow(), CheckStatus::Unsatisfiable => style("UNSATISFIABLE").yellow(), }; write!(f, "{check_str}") diff --git a/tests/expected/dead-invalid-access-via-raw/main.expected b/tests/expected/dead-invalid-access-via-raw/main.expected index 1d464eb5f031..1cdbd0547226 100644 --- a/tests/expected/dead-invalid-access-via-raw/main.expected +++ b/tests/expected/dead-invalid-access-via-raw/main.expected @@ -1,7 +1,5 @@ SUCCESS\ address must be a multiple of its type's alignment -FAILURE\ -unsafe { *raw_ptr } == 10 SUCCESS\ pointer NULL SUCCESS\ @@ -10,7 +8,3 @@ SUCCESS\ deallocated dynamic object FAILURE\ dead object -SUCCESS\ -pointer outside object bounds -SUCCESS\ -invalid integer address diff --git a/tests/expected/dead-invalid-access-via-raw/value.expected b/tests/expected/dead-invalid-access-via-raw/value.expected index 858d44d54ea4..525e5e40a3b2 100644 --- a/tests/expected/dead-invalid-access-via-raw/value.expected +++ b/tests/expected/dead-invalid-access-via-raw/value.expected @@ -1,2 +1 @@ -Failed Checks: assertion failed: *p_subscoped == 7 Failed Checks: dereference failure: dead object diff --git a/tests/expected/shadow/unsupported_num_objects/test.rs b/tests/expected/shadow/unsupported_num_objects/test.rs index f60d0020e989..88b1171ef09d 100644 --- a/tests/expected/shadow/unsupported_num_objects/test.rs +++ b/tests/expected/shadow/unsupported_num_objects/test.rs @@ -15,14 +15,14 @@ fn check_max_objects() { // - the NULL pointer whose object ID is 0, and // - the object ID for `i` while i < N { - let x = i; - assert_eq!(kani::mem::pointer_object(&x as *const usize), i + 2); + let x: Box = Box::new(i); + assert_eq!(kani::mem::pointer_object(&*x as *const usize), 2 * i + 2); i += 1; } // create a new object whose ID is `N` + 2 let x = 42; - assert_eq!(kani::mem::pointer_object(&x as *const i32), N + 2); + assert_eq!(kani::mem::pointer_object(&x as *const i32), 2 * N + 2); // the following call to `set` would fail if the object ID for `x` exceeds // the maximum allowed by Kani's shadow memory model unsafe { @@ -32,10 +32,10 @@ fn check_max_objects() { #[kani::proof] fn check_max_objects_pass() { - check_max_objects::<1021>(); + check_max_objects::<510>(); } #[kani::proof] fn check_max_objects_fail() { - check_max_objects::<1022>(); + check_max_objects::<511>(); } diff --git a/tests/kani/FloatingPoint/main.rs b/tests/kani/FloatingPoint/main.rs index 93a29f169f27..f8ebccdac02a 100644 --- a/tests/kani/FloatingPoint/main.rs +++ b/tests/kani/FloatingPoint/main.rs @@ -26,7 +26,6 @@ macro_rules! test_floats { } #[kani::proof] -#[kani::solver(minisat)] fn main() { assert!(1.1 == 1.1 * 1.0); assert!(1.1 != 1.11 / 1.0); diff --git a/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs b/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs index 642d984a7e2b..09c630aa94a7 100644 --- a/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs @@ -45,7 +45,6 @@ fn test_conc_sci() { } #[kani::proof] -#[kani::solver(minisat)] fn test_towards_inf() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); @@ -54,7 +53,6 @@ fn test_towards_inf() { } #[kani::proof] -#[kani::solver(minisat)] fn test_diff_one() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); diff --git a/tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs b/tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs index 54ad74c33430..0560a2c55064 100644 --- a/tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs @@ -45,7 +45,6 @@ fn test_conc_sci() { } #[kani::proof] -#[kani::solver(minisat)] fn test_towards_neg_inf() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); @@ -54,7 +53,6 @@ fn test_towards_neg_inf() { } #[kani::proof] -#[kani::solver(minisat)] fn test_diff_one() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); diff --git a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs index 7ffdb5f28747..25e02f45a943 100644 --- a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs +++ b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs @@ -50,7 +50,6 @@ fn test_conc_sci() { } #[kani::proof] -#[kani::solver(minisat)] fn test_towards_nearest() { let x: f32 = kani::any(); kani::assume(!x.is_nan()); @@ -89,7 +88,6 @@ fn test_towards_nearest() { } #[kani::proof] -#[kani::solver(minisat)] fn test_diff_half_one() { let x: f32 = kani::any(); kani::assume(!x.is_nan()); diff --git a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs index bf656512562e..589a44a4d1ac 100644 --- a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs @@ -50,7 +50,6 @@ fn test_conc_sci() { } #[kani::proof] -#[kani::solver(minisat)] fn test_towards_nearest() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); @@ -89,7 +88,6 @@ fn test_towards_nearest() { } #[kani::proof] -#[kani::solver(minisat)] fn test_diff_half_one() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); diff --git a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs index 53d9d7d5fc73..79a0a4f9be2c 100644 --- a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs +++ b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs @@ -55,7 +55,6 @@ fn test_conc_sci() { } #[kani::proof] -#[kani::solver(minisat)] fn test_towards_nearest() { let x: f32 = kani::any(); kani::assume(!x.is_nan()); @@ -94,7 +93,6 @@ fn test_towards_nearest() { } #[kani::proof] -#[kani::solver(minisat)] fn test_diff_half_one() { let x: f32 = kani::any(); kani::assume(!x.is_nan()); diff --git a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs index de608e7cdb9f..8c8ea583a2d5 100644 --- a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs @@ -55,7 +55,6 @@ fn test_conc_sci() { } #[kani::proof] -#[kani::solver(minisat)] fn test_towards_nearest() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); @@ -94,7 +93,6 @@ fn test_towards_nearest() { } #[kani::proof] -#[kani::solver(minisat)] fn test_diff_half_one() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); diff --git a/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs b/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs index 04893727dcfa..8a8780878925 100644 --- a/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs +++ b/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs @@ -39,7 +39,6 @@ fn test_conc_sci() { } #[kani::proof] -#[kani::solver(minisat)] fn test_towards_closer() { let x: f32 = kani::any(); kani::assume(!x.is_nan()); @@ -62,7 +61,6 @@ fn test_towards_closer() { } #[kani::proof] -#[kani::solver(minisat)] fn test_diff_half_one() { let x: f32 = kani::any(); kani::assume(!x.is_nan()); diff --git a/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs b/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs index cd61e9607646..ddafc45a2e9e 100644 --- a/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs @@ -39,7 +39,6 @@ fn test_conc_sci() { } #[kani::proof] -#[kani::solver(minisat)] fn test_towards_closer() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); @@ -62,7 +61,6 @@ fn test_towards_closer() { } #[kani::proof] -#[kani::solver(minisat)] fn test_diff_half_one() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); diff --git a/tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs b/tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs index a8a80672e36b..5fcc8c80606d 100644 --- a/tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs @@ -38,7 +38,6 @@ fn test_conc_sci() { } #[kani::proof] -#[kani::solver(minisat)] fn test_towards_zero() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); @@ -51,7 +50,6 @@ fn test_towards_zero() { } #[kani::proof] -#[kani::solver(minisat)] fn test_diff_one() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); diff --git a/tests/kani/Spurious/storage_fixme.rs b/tests/kani/StorageMarkers/main.rs similarity index 99% rename from tests/kani/Spurious/storage_fixme.rs rename to tests/kani/StorageMarkers/main.rs index 51d13f31bcef..770995605ded 100644 --- a/tests/kani/Spurious/storage_fixme.rs +++ b/tests/kani/StorageMarkers/main.rs @@ -3,7 +3,7 @@ // Modifications Copyright Kani Contributors // See GitHub history for details. -// Our handling of storage markers causes spurious failures in this test. +// Our handling of storage markers used to cause spurious failures in this test. // https://github.com/model-checking/kani/issues/3099 // The code is extracted from the implementation of `BTreeMap` which is where we // originally saw the spurious failures while trying to enable storage markers diff --git a/tests/perf/btreeset/insert_any/Cargo.toml b/tests/perf/btreeset/insert_any/Cargo.toml index 66d8ecdddeb1..41fa0a2db3ba 100644 --- a/tests/perf/btreeset/insert_any/Cargo.toml +++ b/tests/perf/btreeset/insert_any/Cargo.toml @@ -9,8 +9,3 @@ edition = "2021" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] - -# Temporarily ignore the handling of storage markers till -# https://github.com/model-checking/kani/issues/3099 is fixed -[package.metadata.kani] -flags = { ignore-locals-lifetime = true, enable-unstable = true } diff --git a/tests/perf/btreeset/insert_multi/Cargo.toml b/tests/perf/btreeset/insert_multi/Cargo.toml index 44028f8c842d..bdd2f4e3528a 100644 --- a/tests/perf/btreeset/insert_multi/Cargo.toml +++ b/tests/perf/btreeset/insert_multi/Cargo.toml @@ -9,8 +9,3 @@ edition = "2021" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] - -# Temporarily ignore the handling of storage markers till -# https://github.com/model-checking/kani/issues/3099 is fixed -[package.metadata.kani] -flags = { ignore-locals-lifetime = true, enable-unstable = true } diff --git a/tests/perf/btreeset/insert_same/Cargo.toml b/tests/perf/btreeset/insert_same/Cargo.toml index 465119c74fbe..0a4e0f7ee037 100644 --- a/tests/perf/btreeset/insert_same/Cargo.toml +++ b/tests/perf/btreeset/insert_same/Cargo.toml @@ -9,8 +9,3 @@ edition = "2021" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] - -# Temporarily ignore the handling of storage markers till -# https://github.com/model-checking/kani/issues/3099 is fixed -[package.metadata.kani] -flags = { ignore-locals-lifetime = true, enable-unstable = true } diff --git a/tests/perf/hashset/Cargo.toml b/tests/perf/hashset/Cargo.toml index 464fba412e6d..d0757e11154b 100644 --- a/tests/perf/hashset/Cargo.toml +++ b/tests/perf/hashset/Cargo.toml @@ -12,8 +12,3 @@ description = "Verify HashSet basic behavior" [package.metadata.kani.unstable] stubbing = true - -# Temporarily ignore the handling of storage markers till -# https://github.com/model-checking/kani/issues/3099 is fixed -[package.metadata.kani] -flags = { ignore-locals-lifetime = true, enable-unstable = true } diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index cc4e6d023f8e..71f8d9f5aafb 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit cc4e6d023f8edf92fea294dcaea2fd5a1132cb47 +Subproject commit 71f8d9f5aafbf59f31ad85eeb7b4b67a7564a685 diff --git a/tests/kani/Strings/copy_empty_string_by_intrinsic.rs b/tests/slow/kani/Strings/copy_empty_string_by_intrinsic.rs similarity index 100% rename from tests/kani/Strings/copy_empty_string_by_intrinsic.rs rename to tests/slow/kani/Strings/copy_empty_string_by_intrinsic.rs diff --git a/tests/kani/Vectors/any/push_slow.rs b/tests/slow/kani/Vectors/any/push_slow.rs similarity index 100% rename from tests/kani/Vectors/any/push_slow.rs rename to tests/slow/kani/Vectors/any/push_slow.rs diff --git a/tests/ui/cbmc_checks/signed-overflow/check_message.rs b/tests/ui/cbmc_checks/signed-overflow/check_message.rs index 0a1527e9a8fc..af496192ee60 100644 --- a/tests/ui/cbmc_checks/signed-overflow/check_message.rs +++ b/tests/ui/cbmc_checks/signed-overflow/check_message.rs @@ -2,7 +2,6 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // // Check we don't print temporary variables as part of CBMC messages. -// cbmc-flags: --signed-overflow-check extern crate kani; use kani::any; diff --git a/tests/ui/cbmc_checks/signed-overflow/expected b/tests/ui/cbmc_checks/signed-overflow/expected index 70669b325e9e..80d3eef3cd25 100644 --- a/tests/ui/cbmc_checks/signed-overflow/expected +++ b/tests/ui/cbmc_checks/signed-overflow/expected @@ -7,4 +7,3 @@ Failed Checks: attempt to calculate the remainder with a divisor of zero Failed Checks: attempt to calculate the remainder with overflow Failed Checks: attempt to shift left with overflow Failed Checks: attempt to shift right with overflow -Failed Checks: arithmetic overflow on signed shl diff --git a/tools/benchcomp/configs/perf-regression.yaml b/tools/benchcomp/configs/perf-regression.yaml index c938b3dd861f..d1e65b24ca2c 100644 --- a/tools/benchcomp/configs/perf-regression.yaml +++ b/tools/benchcomp/configs/perf-regression.yaml @@ -10,13 +10,13 @@ variants: kani_new: config: directory: new - command_line: scripts/kani-perf.sh + command_line: "scripts/setup/ubuntu/install_deps.sh && scripts/kani-perf.sh" env: RUST_TEST_THREADS: "1" kani_old: config: directory: old - command_line: scripts/kani-perf.sh + command_line: "scripts/setup/ubuntu/install_deps.sh && scripts/kani-perf.sh" env: RUST_TEST_THREADS: "1"