diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 9fb35033d2d1..72ef4e2de889 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -104,10 +104,14 @@ jobs: apt-get install -y software-properties-common apt-utils add-apt-repository ppa:git-core/ppa add-apt-repository ppa:deadsnakes/ppa + add-apt-repository ppa:ubuntu-toolchain-r/test apt-get update apt-get install -y \ - build-essential bash-completion curl lsb-release sudo g++ gcc flex \ + build-essential bash-completion curl lsb-release sudo g++-9 gcc-9 flex \ bison make patch git python3.7 python3.7-dev python3.7-distutils + update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-9 110 \ + --slave /usr/bin/g++ g++ /usr/bin/g++-9 + ln -sf cpp-9 /usr/bin/cpp update-alternatives --install /usr/bin/python3 python3 /usr/bin/python3.7 1 curl -s https://bootstrap.pypa.io/pip/3.7/get-pip.py -o get-pip.py python3 get-pip.py --force-reinstall diff --git a/.github/workflows/verify-std-check.yml b/.github/workflows/verify-std-check.yml new file mode 100644 index 000000000000..667be6b340c5 --- /dev/null +++ b/.github/workflows/verify-std-check.yml @@ -0,0 +1,86 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +# +# This workflow will try to build and run the `verify-rust-std` repository. +# +# This check should be optional, but it has been added to help provide +# visibility to when a PR may break the `verify-rust-std` repository. +# +# We expect toolchain updates to potentially break this workflow in cases where +# the version tracked in the `verify-rust-std` is not compatible with newer +# versions of the Rust toolchain. +# +# Changes unrelated to the toolchain should match the current status of main. + +name: Check Std Verification +on: + pull_request: + workflow_call: + +env: + RUST_BACKTRACE: 1 + +jobs: + verify-std: + runs-on: ${{ matrix.os }} + strategy: + matrix: + # Kani does not support windows. + os: [ ubuntu-22.04, macos-14 ] + steps: + - name: Checkout Library + uses: actions/checkout@v4 + with: + repository: model-checking/verify-rust-std + path: verify-rust-std + submodules: true + + - name: Checkout `Kani` + uses: actions/checkout@v4 + with: + path: kani + + - name: Setup Kani Dependencies + uses: ./kani/.github/actions/setup + with: + os: ${{ matrix.os }} + kani_dir: kani + + - name: Build Kani + working-directory: kani + run: | + cargo build-dev + echo "$(pwd)/scripts" >> $GITHUB_PATH + + - name: Run verification with HEAD + id: check-head + working-directory: verify-rust-std + continue-on-error: true + run: | + kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \ + -Z mem-predicates -Z ptr-to-ref-cast-checks + + # If the head failed, check if it's a new failure. + - name: Checkout base + working-directory: kani + if: steps.check-head.outcome != 'success' && github.event_name == 'pull_request' + run: | + BASE_REF=${{ github.event.pull_request.base.sha }} + git checkout ${BASE_REF} + cargo build-dev + + - name: Run verification with BASE + id: check-base + if: steps.check-head.outcome != 'success' && github.event_name == 'pull_request' + working-directory: verify-rust-std + continue-on-error: true + run: | + kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \ + -Z mem-predicates -Z ptr-to-ref-cast-checks + + - name: Compare PR results + if: steps.check-head.outcome != 'success' && steps.check-head.output != github.check-base.output + run: | + echo "New failure introduced by this change" + exit 1 + diff --git a/.github/workflows/verify-std-update.yml b/.github/workflows/verify-std-update.yml new file mode 100644 index 000000000000..518f80ecd1b8 --- /dev/null +++ b/.github/workflows/verify-std-update.yml @@ -0,0 +1,35 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +# +# This workflow will try to update the verify std branch. + +name: Update "features/verify-rust-std" +on: + schedule: + - cron: "30 3 * * *" # Run this every day at 03:30 UTC + workflow_dispatch: # Allow manual dispatching. + +env: + RUST_BACKTRACE: 1 + +jobs: + # First ensure the HEAD is compatible with the `verify-rust-std` repository. + verify-std: + name: Verify Std + permissions: { } + uses: ./.github/workflows/verify-std-check.yml + + # Push changes to the features branch. + update-branch: + needs: verify-std + permissions: + contents: write + runs-on: ubuntu-latest + steps: + - name: Checkout Kani + uses: actions/checkout@v4 + + - name: Update feature branch + run: | + git push origin HEAD:features/verify-rust-std + diff --git a/Cargo.lock b/Cargo.lock index fe420de27a88..0fd31f73278b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -169,7 +169,7 @@ dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.71", + "syn 2.0.72", ] [[package]] @@ -482,7 +482,7 @@ dependencies = [ "proc-macro-error", "proc-macro2", "quote", - "syn 2.0.71", + "syn 2.0.72", ] [[package]] @@ -801,9 +801,9 @@ dependencies = [ [[package]] name = "redox_syscall" -version = "0.5.2" +version = "0.5.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c82cf8cff14456045f55ec4241383baeff27af886adb72ffb2162f99911de0fd" +checksum = "2a908a6e00f1fdd0dfd9c0eb08ce85126f6d8bbda50017e74bc4a4b7d4a926a4" dependencies = [ "bitflags", ] @@ -924,7 +924,7 @@ checksum = "e0cd7e117be63d3c3678776753929474f3b04a43a080c744d6b0ae2a8c28e222" dependencies = [ "proc-macro2", "quote", - "syn 2.0.71", + "syn 2.0.72", ] [[package]] @@ -1030,7 +1030,7 @@ dependencies = [ "proc-macro2", "quote", "rustversion", - "syn 2.0.71", + "syn 2.0.72", ] [[package]] @@ -1045,9 +1045,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.71" +version = "2.0.72" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b146dcf730474b4bcd16c311627b31ede9ab149045db4d6088b3becaea046462" +checksum = "dc4b9b9bf2add8093d3f2c0204471e951b2285580335de42f9d2534f3ae7a8af" dependencies = [ "proc-macro2", "quote", @@ -1068,22 +1068,22 @@ dependencies = [ [[package]] name = "thiserror" -version = "1.0.62" +version = "1.0.63" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f2675633b1499176c2dff06b0856a27976a8f9d436737b4cf4f312d4d91d8bbb" +checksum = "c0342370b38b6a11b6cc11d6a805569958d54cfa061a29969c3b5ce2ea405724" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "1.0.62" +version = "1.0.63" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d20468752b09f49e909e55a5d338caa8bedf615594e9d80bc4c565d30faf798c" +checksum = "a4558b58466b9ad7ca0f102865eccc95938dca1a74a856f2b57b6629050da261" dependencies = [ "proc-macro2", "quote", - "syn 2.0.71", + "syn 2.0.72", ] [[package]] @@ -1098,9 +1098,9 @@ dependencies = [ [[package]] name = "toml" -version = "0.8.14" +version = "0.8.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6f49eb2ab21d2f26bd6db7bf383edc527a7ebaee412d17af4d40fdccd442f335" +checksum = "ac2caab0bf757388c6c0ae23b3293fdb463fee59434529014f85e3263b995c28" dependencies = [ "serde", "serde_spanned", @@ -1119,9 +1119,9 @@ dependencies = [ [[package]] name = "toml_edit" -version = "0.22.15" +version = "0.22.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d59a3a72298453f564e2b111fa896f8d07fabb36f51f06d7e875fc5e0b5a3ef1" +checksum = "278f3d518e152219c994ce877758516bca5e118eaed6996192a774fb9fbf0788" dependencies = [ "indexmap", "serde", @@ -1149,7 +1149,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" dependencies = [ "proc-macro2", "quote", - "syn 2.0.71", + "syn 2.0.72", ] [[package]] @@ -1384,9 +1384,9 @@ checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" [[package]] name = "winnow" -version = "0.6.13" +version = "0.6.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "59b5e5f6c299a3c7890b876a2a587f3115162487e704907d9b6cd29473052ba1" +checksum = "374ec40a2d767a3c1b4972d9475ecd557356637be906f2cb3f7fe17a6eb5e22f" dependencies = [ "memchr", ] @@ -1414,5 +1414,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.71", + "syn 2.0.72", ] diff --git a/cprover_bindings/src/goto_program/location.rs b/cprover_bindings/src/goto_program/location.rs index 4097d075276d..9a2a046f6387 100644 --- a/cprover_bindings/src/goto_program/location.rs +++ b/cprover_bindings/src/goto_program/location.rs @@ -19,6 +19,7 @@ pub enum Location { start_col: Option, end_line: u64, end_col: Option, + pragmas: &'static [&'static str], // CBMC `#pragma check` statements per location. }, /// Location for Statements that use Property Class and Description - Assert, Assume, Cover etc. Property { @@ -28,6 +29,7 @@ pub enum Location { col: Option, comment: InternedString, property_class: InternedString, + pragmas: &'static [&'static str], // CBMC `#pragma check` statements per location. }, /// Covers cases where Location Details are unknown or set as None but Property Class is needed. PropertyUnknownLocation { comment: InternedString, property_class: InternedString }, @@ -99,6 +101,7 @@ impl Location { start_col: Option, end_line: T, end_col: Option, + pragmas: &'static [&'static str], ) -> Location where T: TryInto, @@ -117,6 +120,7 @@ impl Location { start_col: start_col_into, end_line: end_line_into, end_col: end_col_into, + pragmas, } } @@ -128,6 +132,7 @@ impl Location { col: Option, comment: U, property_name: U, + pragmas: &'static [&'static str], ) -> Location where T: TryInto, @@ -140,7 +145,7 @@ impl Location { let function = function.intern(); let property_class = property_name.into(); let comment = comment.into(); - Location::Property { file, function, line, col, comment, property_class } + Location::Property { file, function, line, col, comment, property_class, pragmas } } /// Create a Property type Location from an already existing Location type @@ -157,17 +162,25 @@ impl Location { None, comment.into(), property_name.into(), + &[], + ), + Location::Loc { + file, + function, + start_line, + start_col, + end_line: _, + end_col: _, + pragmas, + } => Location::property_location( + file.into(), + function.intern(), + start_line, + start_col, + comment.into(), + property_name.into(), + pragmas, ), - Location::Loc { file, function, start_line, start_col, end_line: _, end_col: _ } => { - Location::property_location( - file.into(), - function.intern(), - start_line, - start_col, - comment.into(), - property_name.into(), - ) - } Location::Property { .. } => location, Location::PropertyUnknownLocation { .. } => location, // This converts None type Locations to PropertyUnknownLocation type which inserts Property Class and Description diff --git a/cprover_bindings/src/goto_program/symbol.rs b/cprover_bindings/src/goto_program/symbol.rs index ad71b0f84346..457be1163a3a 100644 --- a/cprover_bindings/src/goto_program/symbol.rs +++ b/cprover_bindings/src/goto_program/symbol.rs @@ -8,6 +8,8 @@ use std::fmt::Display; /// Based off the CBMC symbol implementation here: /// +/// +/// TODO: We should consider using BitFlags for all the boolean flags. #[derive(Clone, Debug)] pub struct Symbol { /// Unique identifier. Mangled name from compiler `foo12_bar17_x@1` @@ -46,6 +48,14 @@ pub struct Symbol { pub is_thread_local: bool, pub is_volatile: bool, pub is_weak: bool, + + /// This flag marks a variable as constant (IrepId: `ID_C_constant`). + /// + /// In CBMC, this is a property of the type or expression. However, we keep it here to avoid + /// having to propagate the attribute to all variants of `Type` and `Expr`. + /// + /// During contract verification, CBMC will not havoc static variables marked as constant. + pub is_static_const: bool, } /// The equivalent of a "mathematical function" in CBMC. Semantically this is an @@ -157,6 +167,7 @@ impl Symbol { is_lvalue: false, is_parameter: false, is_static_lifetime: false, + is_static_const: false, is_thread_local: false, is_volatile: false, is_weak: false, @@ -363,6 +374,11 @@ impl Symbol { self } + pub fn set_is_static_const(&mut self, v: bool) -> &mut Symbol { + self.is_static_const = v; + self + } + pub fn with_is_state_var(mut self, v: bool) -> Symbol { self.is_state_var = v; self @@ -383,11 +399,21 @@ impl Symbol { self } + pub fn set_pretty_name>(&mut self, pretty_name: T) -> &mut Symbol { + self.pretty_name = Some(pretty_name.into()); + self + } + pub fn with_is_hidden(mut self, hidden: bool) -> Symbol { self.is_auxiliary = hidden; self } + pub fn set_is_hidden(&mut self, hidden: bool) -> &mut Symbol { + self.is_auxiliary = hidden; + self + } + /// Set `is_property`. pub fn with_is_property(mut self, v: bool) -> Self { self.is_property = v; diff --git a/cprover_bindings/src/goto_program/symbol_table.rs b/cprover_bindings/src/goto_program/symbol_table.rs index 8125c8df3cd9..cd5bd8a6d967 100644 --- a/cprover_bindings/src/goto_program/symbol_table.rs +++ b/cprover_bindings/src/goto_program/symbol_table.rs @@ -107,6 +107,11 @@ impl SymbolTable { self.symbol_table.get(&name) } + pub fn lookup_mut>(&mut self, name: T) -> Option<&mut Symbol> { + let name = name.into(); + self.symbol_table.get_mut(&name) + } + pub fn machine_model(&self) -> &MachineModel { &self.machine_model } diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 4b5c86350172..05774fdf8b43 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -389,15 +389,32 @@ impl ToIrep for Location { (IrepId::Function, Irep::just_string_id(function_name.to_string())), ]) .with_named_sub_option(IrepId::Line, line.map(Irep::just_int_id)), - Location::Loc { file, function, start_line, start_col, end_line: _, end_col: _ } => { - Irep::just_named_sub(linear_map![ - (IrepId::File, Irep::just_string_id(file.to_string())), - (IrepId::Line, Irep::just_int_id(*start_line)), - ]) - .with_named_sub_option(IrepId::Column, start_col.map(Irep::just_int_id)) - .with_named_sub_option(IrepId::Function, function.map(Irep::just_string_id)) - } - Location::Property { file, function, line, col, property_class, comment } => { + Location::Loc { + file, + function, + start_line, + start_col, + end_line: _, + end_col: _, + pragmas, + } => Irep::just_named_sub(linear_map![ + (IrepId::File, Irep::just_string_id(file.to_string())), + (IrepId::Line, Irep::just_int_id(*start_line)), + ]) + .with_named_sub_option(IrepId::Column, start_col.map(Irep::just_int_id)) + .with_named_sub_option(IrepId::Function, function.map(Irep::just_string_id)) + .with_named_sub_option( + IrepId::Pragma, + Some(Irep::just_named_sub( + pragmas + .iter() + .map(|pragma| { + (IrepId::from_string(*pragma), Irep::just_id(IrepId::EmptyString)) + }) + .collect(), + )), + ), + Location::Property { file, function, line, col, property_class, comment, pragmas } => { Irep::just_named_sub(linear_map![ (IrepId::File, Irep::just_string_id(file.to_string())), (IrepId::Line, Irep::just_int_id(*line)), @@ -409,6 +426,17 @@ impl ToIrep for Location { IrepId::PropertyClass, Irep::just_string_id(property_class.to_string()), ) + .with_named_sub_option( + IrepId::Pragma, + Some(Irep::just_named_sub( + pragmas + .iter() + .map(|pragma| { + (IrepId::from_string(*pragma), Irep::just_id(IrepId::EmptyString)) + }) + .collect(), + )), + ) } Location::PropertyUnknownLocation { property_class, comment } => { Irep::just_named_sub(linear_map![ @@ -570,6 +598,10 @@ impl goto_program::Symbol { Irep::just_sub(contract.assigns.iter().map(|req| req.to_irep(mm)).collect()), ); } + if self.is_static_const { + // Add a `const` to the type. + typ = typ.with_named_sub(IrepId::CConstant, Irep::just_id(IrepId::from_int(1))) + } super::Symbol { typ, value: match &self.value { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 5549edcced25..85bb8292ec67 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -3,13 +3,13 @@ use crate::codegen_cprover_gotoc::utils::slice_fat_ptr; use crate::codegen_cprover_gotoc::GotocCtx; use crate::unwrap_or_return_codegen_unimplemented; -use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Stmt, Symbol, Type}; +use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Symbol, Type}; use rustc_middle::ty::Const as ConstInternal; use rustc_smir::rustc_internal; use rustc_span::Span as SpanInternal; use stable_mir::mir::alloc::{AllocId, GlobalAlloc}; use stable_mir::mir::mono::{Instance, StaticDef}; -use stable_mir::mir::Operand; +use stable_mir::mir::{Mutability, Operand}; use stable_mir::ty::{ Allocation, ConstantKind, FloatTy, FnDef, GenericArgs, IntTy, MirConst, RigidTy, Size, Ty, TyConst, TyConstKind, TyKind, UintTy, @@ -470,11 +470,17 @@ impl<'tcx> GotocCtx<'tcx> { name: Option, loc: Location, ) -> Expr { - debug!(?name, "codegen_const_allocation"); + debug!(?name, ?alloc, "codegen_const_allocation"); let alloc_name = match self.alloc_map.get(alloc) { None => { let alloc_name = if let Some(name) = name { name } else { self.next_global_name() }; - self.codegen_alloc_in_memory(alloc.clone(), alloc_name.clone(), loc); + let has_interior_mutabity = false; // Constants cannot be mutated. + self.codegen_alloc_in_memory( + alloc.clone(), + alloc_name.clone(), + loc, + has_interior_mutabity, + ); alloc_name } Some(name) => name.clone(), @@ -484,13 +490,18 @@ impl<'tcx> GotocCtx<'tcx> { mem_place.address_of() } - /// Insert an allocation into the goto symbol table, and generate a goto function that will - /// initialize it. + /// Insert an allocation into the goto symbol table, and generate an init value. /// - /// This function is ultimately responsible for creating new statically initialized global variables - /// in our goto binaries. - pub fn codegen_alloc_in_memory(&mut self, alloc: Allocation, name: String, loc: Location) { - debug!(?alloc, ?name, "codegen_alloc_in_memory"); + /// This function is ultimately responsible for creating new statically initialized global + /// variables. + pub fn codegen_alloc_in_memory( + &mut self, + alloc: Allocation, + name: String, + loc: Location, + has_interior_mutabity: bool, + ) { + debug!(?name, ?alloc, "codegen_alloc_in_memory"); let struct_name = &format!("{name}::struct"); // The declaration of a static variable may have one type and the constant initializer for @@ -513,50 +524,40 @@ impl<'tcx> GotocCtx<'tcx> { .collect() }); + // Create the allocation from a byte array. + let init_fn = |gcx: &mut GotocCtx, var: Symbol| { + let val = Expr::struct_expr_from_values( + alloc_typ_ref.clone(), + alloc_data + .iter() + .map(|d| match d { + AllocData::Bytes(bytes) => Expr::array_expr( + Type::unsigned_int(8).array_of(bytes.len()), + bytes + .iter() + // We should consider adding a poison / undet where we have none + // This mimics the behaviour before StableMIR though. + .map(|b| Expr::int_constant(b.unwrap_or(0), Type::unsigned_int(8))) + .collect(), + ), + AllocData::Expr(e) => e.clone(), + }) + .collect(), + &gcx.symbol_table, + ); + if val.typ() == &var.typ { val } else { val.transmute_to(var.typ, &gcx.symbol_table) } + }; + // The global static variable may not be in the symbol table if we are dealing - // with a literal that can be statically allocated. - // We need to make a constructor whether it was in the table or not, so we can't use the - // closure argument to ensure_global_var to do that here. - let var = self.ensure_global_var( + // with a promoted constant. + let _var = self.ensure_global_var_init( &name, false, //TODO is this correct? + alloc.mutability == Mutability::Not && !has_interior_mutabity, alloc_typ_ref.clone(), loc, - |_, _| None, - ); - let var_typ = var.typ().clone(); - - // Assign the initial value `val` to `var` via an intermediate `temp_var` to allow for - // transmuting the allocation type to the global static variable type. - let val = Expr::struct_expr_from_values( - alloc_typ_ref.clone(), - alloc_data - .iter() - .map(|d| match d { - AllocData::Bytes(bytes) => Expr::array_expr( - Type::unsigned_int(8).array_of(bytes.len()), - bytes - .iter() - // We should consider adding a poison / undet where we have none - // This mimics the behaviour before StableMIR though. - .map(|b| Expr::int_constant(b.unwrap_or(0), Type::unsigned_int(8))) - .collect(), - ), - AllocData::Expr(e) => e.clone(), - }) - .collect(), - &self.symbol_table, - ); - let fn_name = Self::initializer_fn_name(&name); - let temp_var = self.gen_function_local_variable(0, &fn_name, alloc_typ_ref, loc).to_expr(); - let body = Stmt::block( - vec![ - Stmt::decl(temp_var.clone(), Some(val), loc), - var.assign(temp_var.transmute_to(var_typ, &self.symbol_table), loc), - ], - loc, + init_fn, ); - self.register_initializer(&name, body); self.alloc_map.insert(alloc, name); } @@ -663,12 +664,6 @@ impl<'tcx> GotocCtx<'tcx> { let fn_item_struct_ty = self.codegen_fndef_type_stable(instance); // This zero-sized object that a function name refers to in Rust is globally unique, so we create such a global object. let fn_singleton_name = format!("{mangled_name}::FnDefSingleton"); - self.ensure_global_var( - &fn_singleton_name, - false, - fn_item_struct_ty, - loc, - |_, _| None, // zero-sized, so no initialization necessary - ) + self.ensure_global_var(&fn_singleton_name, false, fn_item_struct_ty, loc).to_expr() } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index e01ffbe462ba..4883c608f482 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -703,8 +703,10 @@ impl<'tcx> GotocCtx<'tcx> { if meta.typ().sizeof(&self.symbol_table) == 0 { data_cast } else { - let vtable_expr = - meta.member("_vtable_ptr", &self.symbol_table).cast_to( + let vtable_expr = meta + .member("_vtable_ptr", &self.symbol_table) + .member("pointer", &self.symbol_table) + .cast_to( typ.lookup_field_type("vtable", &self.symbol_table).unwrap(), ); dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table) @@ -835,13 +837,29 @@ impl<'tcx> GotocCtx<'tcx> { dst_goto_typ.lookup_components(&self.symbol_table).unwrap(); assert_eq!(dst_components.len(), 2); assert_eq!(dst_components[0].name(), "_vtable_ptr"); - assert!(dst_components[0].typ().is_pointer()); + assert!(dst_components[0].typ().is_struct_like()); assert_eq!(dst_components[1].name(), "_phantom"); self.assert_is_rust_phantom_data_like(&dst_components[1].typ()); + // accessing pointer type of _vtable_ptr, which is wrapped in NonNull + let vtable_ptr_typ = dst_goto_typ + .lookup_field_type("_vtable_ptr", &self.symbol_table) + .unwrap() + .lookup_components(&self.symbol_table) + .unwrap()[0] + .typ(); Expr::struct_expr( - dst_goto_typ, + dst_goto_typ.clone(), btree_string_map![ - ("_vtable_ptr", vtable_expr.cast_to(dst_components[0].typ())), + ( + "_vtable_ptr", + Expr::struct_expr_from_values( + dst_goto_typ + .lookup_field_type("_vtable_ptr", &self.symbol_table) + .unwrap(), + vec![vtable_expr.clone().cast_to(vtable_ptr_typ)], + &self.symbol_table + ) + ), ( "_phantom", Expr::struct_expr( @@ -1426,9 +1444,10 @@ impl<'tcx> GotocCtx<'tcx> { let vtable_name = self.vtable_name_stable(trait_type).intern(); let vtable_impl_name = format!("{vtable_name}_impl_for_{src_name}"); - self.ensure_global_var( + self.ensure_global_var_init( vtable_impl_name, true, + true, Type::struct_tag(vtable_name), loc, |ctx, var| { @@ -1469,11 +1488,10 @@ impl<'tcx> GotocCtx<'tcx> { vtable_fields, &ctx.symbol_table, ); - let body = var.assign(vtable, loc); - let block = Stmt::block(vec![size_assert, body], loc); - Some(block) + Expr::statement_expression(vec![size_assert, vtable.as_stmt(loc)], var.typ, loc) }, ) + .to_expr() } /// Cast a pointer to a fat pointer. diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs index aadb4fbebed9..41a3da11324b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs @@ -5,9 +5,31 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::Location; +use lazy_static::lazy_static; +use rustc_ast::Attribute; use rustc_smir::rustc_internal; use rustc_span::Span; use stable_mir::ty::Span as SpanStable; +use std::collections::HashMap; + +lazy_static! { + /// Pragmas key-value store to prevent CBMC from generating automatic checks. + /// This list is taken from https://github.com/diffblue/cbmc/blob/develop/regression/cbmc/pragma_cprover_enable_all/main.c. + static ref PRAGMAS: HashMap<&'static str, &'static str> = + [("bounds", "disable:bounds-check"), + ("pointer", "disable:pointer-check"), + ("div-by-zero", "disable:div-by-zero-check"), + ("float-div-by-zero", "disable:float-div-by-zero-check"), + ("enum-range", "disable:enum-range-check"), + ("signed-overflow", "disable:signed-overflow-check"), + ("unsigned-overflow", "disable:unsigned-overflow-check"), + ("pointer-overflow", "disable:pointer-overflow-check"), + ("float-overflow", "disable:float-overflow-check"), + ("conversion", "disable:conversion-check"), + ("undefined-shift", "disable:undefined-shift-check"), + ("nan", "disable:nan-check"), + ("pointer-primitive", "disable:pointer-primitive-check")].iter().copied().collect(); +} impl<'tcx> GotocCtx<'tcx> { pub fn codegen_span(&self, sp: &Span) -> Location { @@ -15,6 +37,36 @@ impl<'tcx> GotocCtx<'tcx> { } pub fn codegen_span_stable(&self, sp: SpanStable) -> Location { + // Attribute to mark functions as where automatic pointer checks should not be generated. + let should_skip_ptr_checks_attr = vec![ + rustc_span::symbol::Symbol::intern("kanitool"), + rustc_span::symbol::Symbol::intern("disable_checks"), + ]; + let pragmas: &'static [&str] = { + let disabled_checks: Vec<_> = self + .current_fn + .as_ref() + .map(|current_fn| { + let instance = current_fn.instance(); + self.tcx + .get_attrs_by_path(instance.def.def_id(), &should_skip_ptr_checks_attr) + .collect() + }) + .unwrap_or_default(); + disabled_checks + .iter() + .map(|attr| { + let arg = parse_word(attr).expect( + "incorrect value passed to `disable_checks`, expected a single identifier", + ); + *PRAGMAS.get(arg.as_str()).expect(format!( + "attempting to disable an unexisting check, the possible options are {:?}", + PRAGMAS.keys() + ).as_str()) + }) + .collect::>() + .leak() // This is to preserve `Location` being Copy, but could blow up the memory utilization of compiler. + }; let loc = sp.get_lines(); Location::new( sp.get_filename().to_string(), @@ -23,6 +75,7 @@ impl<'tcx> GotocCtx<'tcx> { Some(loc.start_col), loc.end_line, Some(loc.end_col), + pragmas, ) } @@ -39,3 +92,18 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_span(&topmost) } } + +/// Extracts the single argument from the attribute provided as a string. +/// For example, `disable_checks(foo)` return `Some("foo")` +fn parse_word(attr: &Attribute) -> Option { + // Vector of meta items , that contain the arguments given the attribute + let attr_args = attr.meta_item_list()?; + // Only extracts one string ident as a string + if attr_args.len() == 1 { + attr_args[0].ident().map(|ident| ident.to_string()) + } + // Return none if there are no attributes or if there's too many attributes + else { + None + } +} diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index c606ae13d095..697cacd3b191 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -317,9 +317,8 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_ret_unit(&mut self, loc: Location) -> Stmt { let is_file_local = false; let ty = self.codegen_ty_unit(); - let var = - self.ensure_global_var(FN_RETURN_VOID_VAR_NAME, is_file_local, ty, loc, |_, _| None); - Stmt::ret(Some(var), loc) + let var = self.ensure_global_var(FN_RETURN_VOID_VAR_NAME, is_file_local, ty, loc); + Stmt::ret(Some(var.to_expr()), loc) } /// Generates Goto-C for MIR [TerminatorKind::Drop] calls. We only handle code _after_ Rust's "drop elaboration" diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs index e05da3f7f622..537fbcb63fbb 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs @@ -4,7 +4,7 @@ //! This file contains functions related to codegenning MIR static variables into gotoc use crate::codegen_cprover_gotoc::GotocCtx; -use cbmc::goto_program::Symbol; +use crate::kani_middle::is_interior_mut; use stable_mir::mir::mono::{Instance, StaticDef}; use stable_mir::CrateDef; use tracing::debug; @@ -19,7 +19,12 @@ impl<'tcx> GotocCtx<'tcx> { debug!("codegen_static"); let alloc = def.eval_initializer().unwrap(); let symbol_name = Instance::from(def).mangled_name(); - self.codegen_alloc_in_memory(alloc, symbol_name, self.codegen_span_stable(def.span())); + self.codegen_alloc_in_memory( + alloc, + symbol_name, + self.codegen_span_stable(def.span()), + is_interior_mut(self.tcx, def.ty()), + ); } /// Mutates the Goto-C symbol table to add a forward-declaration of the static variable. @@ -37,9 +42,8 @@ impl<'tcx> GotocCtx<'tcx> { // havoc static variables. Kani uses the location and pretty name to identify // the correct variables. If the wrong name is used, CBMC may fail silently. // More details at https://github.com/diffblue/cbmc/issues/8225. - let symbol = Symbol::static_variable(symbol_name.clone(), symbol_name, typ, location) - .with_is_hidden(false) // Static items are always user defined. - .with_pretty_name(pretty_name); - self.symbol_table.insert(symbol); + self.ensure_global_var(symbol_name, false, typ, location) + .set_is_hidden(false) // Static items are always user defined. + .set_pretty_name(pretty_name); } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index abb69a655472..986cd00e32a5 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -7,14 +7,14 @@ use crate::args::ReachabilityType; use crate::codegen_cprover_gotoc::GotocCtx; use crate::kani_middle::analysis; use crate::kani_middle::attributes::{is_test_harness_description, KaniAttributes}; +use crate::kani_middle::check_reachable_items; use crate::kani_middle::codegen_units::{CodegenUnit, CodegenUnits}; use crate::kani_middle::metadata::gen_test_metadata; use crate::kani_middle::provide; use crate::kani_middle::reachability::{ collect_reachable_items, filter_const_crate_items, filter_crate_items, }; -use crate::kani_middle::transform::BodyTransformation; -use crate::kani_middle::{check_reachable_items, dump_mir_items}; +use crate::kani_middle::transform::{BodyTransformation, GlobalPasses}; use crate::kani_queries::QueryDb; use cbmc::goto_program::Location; use cbmc::irep::goto_binary_serde::write_goto_binary_file; @@ -24,9 +24,7 @@ use kani_metadata::artifact::convert_type; use kani_metadata::UnsupportedFeature; use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata}; use kani_metadata::{AssignsContract, CompilerArtifactStub}; -use rustc_codegen_ssa::back::archive::{ - get_native_object_symbols, ArArchiveBuilder, ArchiveBuilder, -}; +use rustc_codegen_ssa::back::archive::{ArArchiveBuilder, ArchiveBuilder, DEFAULT_OBJECT_READER}; use rustc_codegen_ssa::back::metadata::create_wrapper_file; use rustc_codegen_ssa::traits::CodegenBackend; use rustc_codegen_ssa::{CodegenResults, CrateInfo}; @@ -89,11 +87,33 @@ impl GotocCodegenBackend { check_contract: Option, mut transformer: BodyTransformation, ) -> (GotocCtx<'tcx>, Vec, Option) { - let items = with_timer( + let (items, call_graph) = with_timer( || collect_reachable_items(tcx, &mut transformer, starting_items), "codegen reachability analysis", ); - dump_mir_items(tcx, &mut transformer, &items, &symtab_goto.with_extension("kani.mir")); + + // Retrieve all instances from the currently codegened items. + let instances = items + .iter() + .filter_map(|item| match item { + MonoItem::Fn(instance) => Some(*instance), + MonoItem::Static(static_def) => { + let instance: Instance = (*static_def).into(); + instance.has_body().then_some(instance) + } + MonoItem::GlobalAsm(_) => None, + }) + .collect(); + + // Apply all transformation passes, including global passes. + let mut global_passes = GlobalPasses::new(&self.queries.lock().unwrap(), tcx); + global_passes.run_global_passes( + &mut transformer, + tcx, + starting_items, + instances, + call_graph, + ); // Follow rustc naming convention (cx is abbrev for context). // https://rustc-dev-guide.rust-lang.org/conventions.html#naming-conventions @@ -402,7 +422,7 @@ impl CodegenBackend for GotocCodegenBackend { debug!(?crate_type, ?out_path, "link"); if *crate_type == CrateType::Rlib { // Emit the `rlib` that contains just one file: `.rmeta` - let mut builder = Box::new(ArArchiveBuilder::new(sess, get_native_object_symbols)); + let mut builder = Box::new(ArArchiveBuilder::new(sess, &DEFAULT_OBJECT_READER)); let tmp_dir = TempFileBuilder::new().prefix("kani").tempdir().unwrap(); let path = MaybeTempDir::new(tmp_dir, sess.opts.cg.save_temps); let (metadata, _metadata_position) = create_wrapper_file( diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 7d51cff037c6..e360cd491edd 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -21,7 +21,9 @@ use crate::codegen_cprover_gotoc::utils::full_crate_name; use crate::codegen_cprover_gotoc::UnsupportedConstructs; use crate::kani_middle::transform::BodyTransformation; use crate::kani_queries::QueryDb; -use cbmc::goto_program::{DatatypeComponent, Expr, Location, Stmt, Symbol, SymbolTable, Type}; +use cbmc::goto_program::{ + DatatypeComponent, Expr, Location, Stmt, Symbol, SymbolTable, SymbolValues, Type, +}; use cbmc::utils::aggr_tag; use cbmc::{InternedString, MachineModel}; use rustc_data_structures::fx::FxHashMap; @@ -38,6 +40,7 @@ use rustc_target::abi::{HasDataLayout, TargetDataLayout}; use stable_mir::mir::mono::Instance; use stable_mir::mir::Body; use stable_mir::ty::Allocation; +use std::fmt::Debug; pub struct GotocCtx<'tcx> { /// the typing context @@ -200,34 +203,58 @@ impl<'tcx> GotocCtx<'tcx> { self.symbol_table.lookup(name).unwrap() } + /// Ensures that a global variable `name` appears in the Symbol table and is initialized. + /// + /// This will add the symbol to the Symbol Table if not inserted yet. + /// This will register the initialization function if not initialized yet. + /// - This case can happen for static variables, since they are declared first. + pub fn ensure_global_var_init( + &mut self, + name: T, + is_file_local: bool, + is_const: bool, + t: Type, + loc: Location, + init: F, + ) -> &mut Symbol + where + T: Into + Clone + Debug, + F: Fn(&mut GotocCtx, Symbol) -> Expr, + { + let sym = self.ensure_global_var(name.clone(), is_file_local, t, loc); + sym.set_is_static_const(is_const); + if matches!(sym.value, SymbolValues::None) { + // Clone sym so we can use `&mut self`. + let sym = sym.clone(); + let init_expr = SymbolValues::Expr(init(self, sym)); + // Need to lookup again since symbol table might've changed. + let sym = self.symbol_table.lookup_mut(name).unwrap(); + sym.value = init_expr; + sym + } else { + self.symbol_table.lookup_mut(name).unwrap() + } + } + /// Ensures that a global variable `name` appears in the Symbol table. - /// If it doesn't, inserts it. - /// If `init_fn` returns `Some(body)`, creates an initializer for the variable using `body`. - /// Otherwise, leaves the variable uninitialized . - pub fn ensure_global_var< - F: FnOnce(&mut GotocCtx<'tcx>, Expr) -> Option, - T: Into, - >( + /// + /// This will add the symbol to the Symbol Table if not inserted yet. + pub fn ensure_global_var + Clone>( &mut self, name: T, is_file_local: bool, t: Type, loc: Location, - init_fn: F, - ) -> Expr { - let name = name.into(); - if !self.symbol_table.contains(name) { - tracing::debug!(?name, "Ensure global variable"); - let sym = Symbol::static_variable(name, name, t, loc) + ) -> &mut Symbol { + let sym_name = name.clone().into(); + if !self.symbol_table.contains(sym_name) { + tracing::debug!(?sym_name, "ensure_global_var insert"); + let sym = Symbol::static_variable(sym_name, sym_name, t, loc) .with_is_file_local(is_file_local) .with_is_hidden(false); - let var = sym.to_expr(); - self.symbol_table.insert(sym); - if let Some(body) = init_fn(self, var) { - self.register_initializer(&name.to_string(), body); - } + self.symbol_table.insert(sym.clone()); } - self.symbol_table.lookup(name).unwrap().to_expr() + self.symbol_table.lookup_mut(sym_name).unwrap() } /// Ensures that a struct with name `struct_name` appears in the symbol table. @@ -284,23 +311,6 @@ impl<'tcx> GotocCtx<'tcx> { } Type::union_tag(union_name) } - - /// Makes a `__attribute__((constructor)) fnname() {body}` initalizer function - pub fn register_initializer(&mut self, var_name: &str, body: Stmt) -> &Symbol { - let fn_name = Self::initializer_fn_name(var_name); - let pretty_name = format!("{var_name}::init"); - let loc = *body.location(); - self.ensure(&fn_name, |_tcx, _| { - Symbol::function( - &fn_name, - Type::code(vec![], Type::constructor()), - Some(Stmt::block(vec![body], loc)), //TODO is this block needed? - &pretty_name, - loc, - ) - .with_is_file_local(true) - }) - } } /// Mutators diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 84ec8d627c59..9eb6d3d6ee4e 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -74,6 +74,9 @@ enum KaniAttributeKind { /// We use this attribute to properly instantiate `kani::any_modifies` in /// cases when recursion is present given our contracts instrumentation. Recursion, + /// Used to mark functions where generating automatic pointer checks should be disabled. This is + /// used later to automatically attach pragma statements to locations. + DisableChecks, } impl KaniAttributeKind { @@ -93,7 +96,8 @@ impl KaniAttributeKind { | KaniAttributeKind::CheckedWith | KaniAttributeKind::Modifies | KaniAttributeKind::InnerCheck - | KaniAttributeKind::IsContractGenerated => false, + | KaniAttributeKind::IsContractGenerated + | KaniAttributeKind::DisableChecks => false, } } @@ -382,6 +386,10 @@ impl<'tcx> KaniAttributes<'tcx> { KaniAttributeKind::InnerCheck => { self.inner_check(); } + KaniAttributeKind::DisableChecks => { + // Ignored here, because it should be an internal attribute. Actual validation + // happens when pragmas are generated. + } } } } @@ -490,6 +498,10 @@ impl<'tcx> KaniAttributes<'tcx> { | KaniAttributeKind::InnerCheck | KaniAttributeKind::ReplacedWith => { self.tcx.dcx().span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref())); + }, + KaniAttributeKind::DisableChecks => { + // Internal attribute which shouldn't exist here. + unreachable!() } }; harness diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 17b08b687e30..a7a512c86de3 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -4,9 +4,7 @@ //! and transformations. use std::collections::HashSet; -use std::path::Path; -use crate::kani_middle::transform::BodyTransformation; use crate::kani_queries::QueryDb; use rustc_hir::{def::DefKind, def_id::LOCAL_CRATE}; use rustc_middle::span_bug; @@ -15,18 +13,16 @@ use rustc_middle::ty::layout::{ LayoutOfHelpers, TyAndLayout, }; use rustc_middle::ty::{self, Instance as InstanceInternal, Ty as TyInternal, TyCtxt}; -use rustc_session::config::OutputType; use rustc_smir::rustc_internal; use rustc_span::source_map::respan; use rustc_span::Span; use rustc_target::abi::call::FnAbi; use rustc_target::abi::{HasDataLayout, TargetDataLayout}; -use stable_mir::mir::mono::{Instance, MonoItem}; -use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, TyKind}; +use stable_mir::mir::mono::MonoItem; +use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, Ty, TyKind}; +use stable_mir::visitor::{Visitable, Visitor as TyVisitor}; use stable_mir::CrateDef; -use std::fs::File; -use std::io::BufWriter; -use std::io::Write; +use std::ops::ControlFlow; use self::attributes::KaniAttributes; @@ -68,6 +64,36 @@ pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) { tcx.dcx().abort_if_errors(); } +/// Traverse the type definition to see if the type contains interior mutability. +/// +/// See for more details. +pub fn is_interior_mut(tcx: TyCtxt, ty: Ty) -> bool { + let mut visitor = FindUnsafeCell { tcx }; + visitor.visit_ty(&ty) == ControlFlow::Break(()) +} + +struct FindUnsafeCell<'tcx> { + tcx: TyCtxt<'tcx>, +} + +impl<'tcx> TyVisitor for FindUnsafeCell<'tcx> { + type Break = (); + fn visit_ty(&mut self, ty: &Ty) -> ControlFlow { + match ty.kind() { + TyKind::RigidTy(RigidTy::Adt(def, _)) + if rustc_internal::internal(self.tcx, def).is_unsafe_cell() => + { + ControlFlow::Break(()) + } + TyKind::RigidTy(RigidTy::Ref(..) | RigidTy::RawPtr(..)) => { + // We only care about the current memory space. + ControlFlow::Continue(()) + } + _ => ty.super_visit(self), + } + } +} + /// Check that all given items are supported and there's no misconfiguration. /// This method will exhaustively print any error / warning and it will abort at the end if any /// error was found. @@ -92,41 +118,6 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) tcx.dcx().abort_if_errors(); } -/// Print MIR for the reachable items if the `--emit mir` option was provided to rustc. -pub fn dump_mir_items( - tcx: TyCtxt, - transformer: &mut BodyTransformation, - items: &[MonoItem], - output: &Path, -) { - /// Convert MonoItem into a DefId. - /// Skip stuff that we cannot generate the MIR items. - fn get_instance(item: &MonoItem) -> Option { - match item { - // Exclude FnShims and others that cannot be dumped. - MonoItem::Fn(instance) => Some(*instance), - MonoItem::Static(def) => { - let instance: Instance = (*def).into(); - instance.has_body().then_some(instance) - } - MonoItem::GlobalAsm(_) => None, - } - } - - if tcx.sess.opts.output_types.contains_key(&OutputType::Mir) { - // Create output buffer. - let out_file = File::create(output).unwrap(); - let mut writer = BufWriter::new(out_file); - - // For each def_id, dump their MIR - for instance in items.iter().filter_map(get_instance) { - writeln!(writer, "// Item: {} ({})", instance.name(), instance.mangled_name()).unwrap(); - let body = transformer.body(tcx, instance); - let _ = body.dump(&mut writer, &instance.name()); - } - } -} - /// Structure that represents the source location of a definition. /// TODO: Use `InternedString` once we move it out of the cprover_bindings. /// diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 279dcf8cc107..d2c9d50515c4 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -22,6 +22,7 @@ use rustc_data_structures::fingerprint::Fingerprint; use rustc_data_structures::fx::FxHashSet; use rustc_data_structures::stable_hasher::{HashStable, StableHasher}; use rustc_middle::ty::{TyCtxt, VtblEntry}; +use rustc_session::config::OutputType; use rustc_smir::rustc_internal; use stable_mir::mir::alloc::{AllocId, GlobalAlloc}; use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem, StaticDef}; @@ -32,6 +33,12 @@ use stable_mir::mir::{ use stable_mir::ty::{Allocation, ClosureKind, ConstantKind, RigidTy, Ty, TyKind}; use stable_mir::CrateItem; use stable_mir::{CrateDef, ItemKind}; +use std::fmt::{Display, Formatter}; +use std::{ + collections::{HashMap, HashSet}, + fs::File, + io::{BufWriter, Write}, +}; use crate::kani_middle::coercion; use crate::kani_middle::coercion::CoercionBase; @@ -42,7 +49,7 @@ pub fn collect_reachable_items( tcx: TyCtxt, transformer: &mut BodyTransformation, starting_points: &[MonoItem], -) -> Vec { +) -> (Vec, CallGraph) { // For each harness, collect items using the same collector. // I.e.: This will return any item that is reachable from one or more of the starting points. let mut collector = MonoItemsCollector::new(tcx, transformer); @@ -62,7 +69,7 @@ pub fn collect_reachable_items( // order of the errors and warnings is stable. let mut sorted_items: Vec<_> = collector.collected.into_iter().collect(); sorted_items.sort_by_cached_key(|item| to_fingerprint(tcx, item)); - sorted_items + (sorted_items, collector.call_graph) } /// Collect all (top-level) items in the crate that matches the given predicate. @@ -118,7 +125,24 @@ where } } } - roots + roots.into_iter().map(|root| root.item).collect() +} + +/// Reason for introducing an edge in the call graph. +#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)] +enum CollectionReason { + DirectCall, + IndirectCall, + VTableMethod, + Static, + StaticDrop, +} + +/// A destination of the edge in the call graph. +#[derive(Clone, Debug, Eq, PartialEq, Hash)] +struct CollectedItem { + item: MonoItem, + reason: CollectionReason, } struct MonoItemsCollector<'tcx, 'a> { @@ -130,8 +154,8 @@ struct MonoItemsCollector<'tcx, 'a> { collected: FxHashSet, /// Items enqueued for visiting. queue: Vec, - #[cfg(debug_assertions)] - call_graph: debug::CallGraph, + /// Call graph used for dataflow analysis. + call_graph: CallGraph, } impl<'tcx, 'a> MonoItemsCollector<'tcx, 'a> { @@ -140,8 +164,7 @@ impl<'tcx, 'a> MonoItemsCollector<'tcx, 'a> { tcx, collected: FxHashSet::default(), queue: vec![], - #[cfg(debug_assertions)] - call_graph: debug::CallGraph::default(), + call_graph: CallGraph::default(), transformer, } } @@ -167,17 +190,17 @@ impl<'tcx, 'a> MonoItemsCollector<'tcx, 'a> { vec![] } }; - #[cfg(debug_assertions)] self.call_graph.add_edges(to_visit, &next_items); - self.queue - .extend(next_items.into_iter().filter(|item| !self.collected.contains(item))); + self.queue.extend(next_items.into_iter().filter_map( + |CollectedItem { item, .. }| (!self.collected.contains(&item)).then_some(item), + )); } } } /// Visit a function and collect all mono-items reachable from its instructions. - fn visit_fn(&mut self, instance: Instance) -> Vec { + fn visit_fn(&mut self, instance: Instance) -> Vec { let _guard = debug_span!("visit_fn", function=?instance).entered(); let body = self.transformer.body(self.tcx, instance); let mut collector = @@ -187,19 +210,24 @@ impl<'tcx, 'a> MonoItemsCollector<'tcx, 'a> { } /// Visit a static object and collect drop / initialization functions. - fn visit_static(&mut self, def: StaticDef) -> Vec { + fn visit_static(&mut self, def: StaticDef) -> Vec { let _guard = debug_span!("visit_static", ?def).entered(); let mut next_items = vec![]; // Collect drop function. let static_ty = def.ty(); let instance = Instance::resolve_drop_in_place(static_ty); - next_items.push(instance.into()); + next_items + .push(CollectedItem { item: instance.into(), reason: CollectionReason::StaticDrop }); // Collect initialization. let alloc = def.eval_initializer().unwrap(); for (_, prov) in alloc.provenance.ptrs { - next_items.extend(collect_alloc_items(prov.0).into_iter()); + next_items.extend( + collect_alloc_items(prov.0) + .into_iter() + .map(|item| CollectedItem { item, reason: CollectionReason::Static }), + ); } next_items @@ -213,7 +241,7 @@ impl<'tcx, 'a> MonoItemsCollector<'tcx, 'a> { struct MonoItemsFnCollector<'a, 'tcx> { tcx: TyCtxt<'tcx>, - collected: FxHashSet, + collected: FxHashSet, body: &'a Body, } @@ -251,7 +279,9 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { } }); trace!(methods=?methods.clone().collect::>(), "collect_vtable_methods"); - self.collected.extend(methods); + self.collected.extend( + methods.map(|item| CollectedItem { item, reason: CollectionReason::VTableMethod }), + ); } // Add the destructor for the concrete type. @@ -282,7 +312,12 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { }; if should_collect && should_codegen_locally(&instance) { trace!(?instance, "collect_instance"); - self.collected.insert(instance.into()); + let reason = if is_direct_call { + CollectionReason::DirectCall + } else { + CollectionReason::IndirectCall + }; + self.collected.insert(CollectedItem { item: instance.into(), reason }); } } @@ -290,7 +325,11 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { fn collect_allocation(&mut self, alloc: &Allocation) { debug!(?alloc, "collect_allocation"); for (_, id) in &alloc.provenance.ptrs { - self.collected.extend(collect_alloc_items(id.0).into_iter()) + self.collected.extend( + collect_alloc_items(id.0) + .into_iter() + .map(|item| CollectedItem { item, reason: CollectionReason::Static }), + ) } } } @@ -366,7 +405,8 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> { } Rvalue::ThreadLocalRef(item) => { trace!(?item, "visit_rvalue thread_local"); - self.collected.insert(MonoItem::Static(StaticDef::try_from(item).unwrap())); + let item = MonoItem::Static(StaticDef::try_from(item).unwrap()); + self.collected.insert(CollectedItem { item, reason: CollectionReason::Static }); } _ => { /* not interesting */ } } @@ -485,128 +525,150 @@ fn collect_alloc_items(alloc_id: AllocId) -> Vec { items } -#[cfg(debug_assertions)] -#[allow(dead_code)] -mod debug { - - use std::fmt::{Display, Formatter}; - use std::{ - collections::{HashMap, HashSet}, - fs::File, - io::{BufWriter, Write}, - }; - - use rustc_session::config::OutputType; - - use super::*; +/// Call graph with edges annotated with the reason why they were added to the graph. +#[derive(Debug, Default)] +pub struct CallGraph { + /// Nodes of the graph. + nodes: HashSet, + /// Edges of the graph. + edges: HashMap>, + /// Since the graph is directed, we also store back edges. + back_edges: HashMap>, +} - #[derive(Debug, Default)] - pub struct CallGraph { - // Nodes of the graph. - nodes: HashSet, - edges: HashMap>, - back_edges: HashMap>, +/// Newtype around MonoItem. +#[derive(Clone, Debug, Eq, PartialEq, Hash)] +struct Node(pub MonoItem); + +/// Newtype around CollectedItem. +#[derive(Clone, Debug, Eq, PartialEq, Hash)] +struct CollectedNode(pub CollectedItem); + +impl CallGraph { + /// Add a new node into a graph. + fn add_node(&mut self, item: MonoItem) { + let node = Node(item); + self.nodes.insert(node.clone()); + self.edges.entry(node.clone()).or_default(); + self.back_edges.entry(node).or_default(); } - #[derive(Clone, Debug, Eq, PartialEq, Hash)] - struct Node(pub MonoItem); - - impl CallGraph { - pub fn add_node(&mut self, item: MonoItem) { - let node = Node(item); - self.nodes.insert(node.clone()); - self.edges.entry(node.clone()).or_default(); - self.back_edges.entry(node).or_default(); - } + /// Add a new edge "from" -> "to". + fn add_edge(&mut self, from: MonoItem, to: MonoItem, collection_reason: CollectionReason) { + let from_node = Node(from.clone()); + let to_node = Node(to.clone()); + self.add_node(from.clone()); + self.add_node(to.clone()); + self.edges + .get_mut(&from_node) + .unwrap() + .push(CollectedNode(CollectedItem { item: to, reason: collection_reason })); + self.back_edges + .get_mut(&to_node) + .unwrap() + .push(CollectedNode(CollectedItem { item: from, reason: collection_reason })); + } - /// Add a new edge "from" -> "to". - pub fn add_edge(&mut self, from: MonoItem, to: MonoItem) { - let from_node = Node(from.clone()); - let to_node = Node(to.clone()); - self.add_node(from); - self.add_node(to); - self.edges.get_mut(&from_node).unwrap().push(to_node.clone()); - self.back_edges.get_mut(&to_node).unwrap().push(from_node); + /// Add multiple new edges for the "from" node. + fn add_edges(&mut self, from: MonoItem, to: &[CollectedItem]) { + self.add_node(from.clone()); + for CollectedItem { item, reason } in to { + self.add_edge(from.clone(), item.clone(), *reason); } + } - /// Add multiple new edges for the "from" node. - pub fn add_edges(&mut self, from: MonoItem, to: &[MonoItem]) { - self.add_node(from.clone()); - for item in to { - self.add_edge(from.clone(), item.clone()); + /// Print the graph in DOT format to a file. + /// See for more information. + fn dump_dot(&self, tcx: TyCtxt) -> std::io::Result<()> { + if let Ok(target) = std::env::var("KANI_REACH_DEBUG") { + debug!(?target, "dump_dot"); + let outputs = tcx.output_filenames(()); + let base_path = outputs.path(OutputType::Metadata); + let path = base_path.as_path().with_extension("dot"); + let out_file = File::create(path)?; + let mut writer = BufWriter::new(out_file); + writeln!(writer, "digraph ReachabilityGraph {{")?; + if target.is_empty() { + self.dump_all(&mut writer)?; + } else { + // Only dump nodes that led the reachability analysis to the target node. + self.dump_reason(&mut writer, &target)?; } + writeln!(writer, "}}")?; } - /// Print the graph in DOT format to a file. - /// See for more information. - pub fn dump_dot(&self, tcx: TyCtxt) -> std::io::Result<()> { - if let Ok(target) = std::env::var("KANI_REACH_DEBUG") { - debug!(?target, "dump_dot"); - let outputs = tcx.output_filenames(()); - let base_path = outputs.path(OutputType::Metadata); - let path = base_path.as_path().with_extension("dot"); - let out_file = File::create(path)?; - let mut writer = BufWriter::new(out_file); - writeln!(writer, "digraph ReachabilityGraph {{")?; - if target.is_empty() { - self.dump_all(&mut writer)?; - } else { - // Only dump nodes that led the reachability analysis to the target node. - self.dump_reason(&mut writer, &target)?; - } - writeln!(writer, "}}")?; - } + Ok(()) + } - Ok(()) + /// Write all notes to the given writer. + fn dump_all(&self, writer: &mut W) -> std::io::Result<()> { + tracing::info!(nodes=?self.nodes.len(), edges=?self.edges.len(), "dump_all"); + for node in &self.nodes { + writeln!(writer, r#""{node}""#)?; + for succ in self.edges.get(node).unwrap() { + let reason = succ.0.reason; + writeln!(writer, r#""{node}" -> "{succ}" [label={reason:?}] "#)?; + } } + Ok(()) + } - /// Write all notes to the given writer. - fn dump_all(&self, writer: &mut W) -> std::io::Result<()> { - tracing::info!(nodes=?self.nodes.len(), edges=?self.edges.len(), "dump_all"); - for node in &self.nodes { - writeln!(writer, r#""{node}""#)?; - for succ in self.edges.get(node).unwrap() { - writeln!(writer, r#""{node}" -> "{succ}" "#)?; - } + /// Write all notes that may have led to the discovery of the given target. + fn dump_reason(&self, writer: &mut W, target: &str) -> std::io::Result<()> { + let mut queue: Vec = + self.nodes.iter().filter(|item| item.to_string().contains(target)).cloned().collect(); + let mut visited: HashSet = HashSet::default(); + tracing::info!(target=?queue, nodes=?self.nodes.len(), edges=?self.edges.len(), "dump_reason"); + while let Some(to_visit) = queue.pop() { + if !visited.contains(&to_visit) { + visited.insert(to_visit.clone()); + queue.extend( + self.back_edges + .get(&to_visit) + .unwrap() + .iter() + .map(|item| Node::from(item.clone())), + ); } - Ok(()) } - /// Write all notes that may have led to the discovery of the given target. - fn dump_reason(&self, writer: &mut W, target: &str) -> std::io::Result<()> { - let mut queue = self - .nodes - .iter() - .filter(|item| item.to_string().contains(target)) - .collect::>(); - let mut visited: HashSet<&Node> = HashSet::default(); - tracing::info!(target=?queue, nodes=?self.nodes.len(), edges=?self.edges.len(), "dump_reason"); - while let Some(to_visit) = queue.pop() { - if !visited.contains(to_visit) { - visited.insert(to_visit); - queue.extend(self.back_edges.get(to_visit).unwrap()); - } + for node in &visited { + writeln!(writer, r#""{node}""#)?; + let edges = self.edges.get(node).unwrap(); + for succ in edges.iter().filter(|item| { + let node = Node::from((*item).clone()); + visited.contains(&node) + }) { + let reason = succ.0.reason; + writeln!(writer, r#""{node}" -> "{succ}" [label={reason:?}] "#)?; } + } + Ok(()) + } +} - for node in &visited { - writeln!(writer, r#""{node}""#)?; - for succ in - self.edges.get(node).unwrap().iter().filter(|item| visited.contains(item)) - { - writeln!(writer, r#""{node}" -> "{succ}" "#)?; - } - } - Ok(()) +impl Display for Node { + fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { + match &self.0 { + MonoItem::Fn(instance) => write!(f, "{}", instance.name()), + MonoItem::Static(def) => write!(f, "{}", def.name()), + MonoItem::GlobalAsm(asm) => write!(f, "{asm:?}"), } } +} - impl Display for Node { - fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { - match &self.0 { - MonoItem::Fn(instance) => write!(f, "{}", instance.name()), - MonoItem::Static(def) => write!(f, "{}", def.name()), - MonoItem::GlobalAsm(asm) => write!(f, "{asm:?}"), - } +impl Display for CollectedNode { + fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { + match &self.0.item { + MonoItem::Fn(instance) => write!(f, "{}", instance.name()), + MonoItem::Static(def) => write!(f, "{}", def.name()), + MonoItem::GlobalAsm(asm) => write!(f, "{asm:?}"), } } } + +impl From for Node { + fn from(value: CollectedNode) -> Self { + Node(value.0.item) + } +} diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index d82dda80cc05..d3f2afc15d31 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -88,16 +88,20 @@ impl MutableBody { pub fn new_str_operand(&mut self, msg: &str, span: Span) -> Operand { let literal = MirConst::from_str(msg); - Operand::Constant(ConstOperand { span, user_ty: None, const_: literal }) + self.new_const_operand(literal, span) } - pub fn new_const_operand(&mut self, val: u128, uint_ty: UintTy, span: Span) -> Operand { + pub fn new_uint_operand(&mut self, val: u128, uint_ty: UintTy, span: Span) -> Operand { let literal = MirConst::try_from_uint(val, uint_ty).unwrap(); + self.new_const_operand(literal, span) + } + + fn new_const_operand(&mut self, literal: MirConst, span: Span) -> Operand { Operand::Constant(ConstOperand { span, user_ty: None, const_: literal }) } /// Create a raw pointer of `*mut type` and return a new local where that value is stored. - pub fn new_cast_ptr( + pub fn insert_ptr_cast( &mut self, from: Operand, pointee_ty: Ty, @@ -108,13 +112,13 @@ impl MutableBody { assert!(from.ty(self.locals()).unwrap().kind().is_raw_ptr()); let target_ty = Ty::new_ptr(pointee_ty, mutability); let rvalue = Rvalue::Cast(CastKind::PtrToPtr, from, target_ty); - self.new_assignment(rvalue, source, position) + self.insert_assignment(rvalue, source, position) } /// Add a new assignment for the given binary operation. /// /// Return the local where the result is saved. - pub fn new_binary_op( + pub fn insert_binary_op( &mut self, bin_op: BinOp, lhs: Operand, @@ -123,13 +127,13 @@ impl MutableBody { position: InsertPosition, ) -> Local { let rvalue = Rvalue::BinaryOp(bin_op, lhs, rhs); - self.new_assignment(rvalue, source, position) + self.insert_assignment(rvalue, source, position) } /// Add a new assignment. /// - /// Return local where the result is saved. - pub fn new_assignment( + /// Return the local where the result is saved. + pub fn insert_assignment( &mut self, rvalue: Rvalue, source: &mut SourceInstruction, @@ -146,9 +150,10 @@ impl MutableBody { /// Add a new assert to the basic block indicated by the given index. /// /// The new assertion will have the same span as the source instruction, and the basic block - /// will be split. The source instruction will be adjusted to point to the first instruction in - /// the new basic block. - pub fn add_check( + /// will be split. If `InsertPosition` is `InsertPosition::Before`, `source` will point to the + /// same instruction as before. If `InsertPosition` is `InsertPosition::After`, `source` will + /// point to the new terminator. + pub fn insert_check( &mut self, tcx: TyCtxt, check_type: &CheckType, @@ -183,7 +188,7 @@ impl MutableBody { unwind: UnwindAction::Terminate, }; let terminator = Terminator { kind, span }; - self.split_bb(source, position, terminator); + self.insert_terminator(source, position, terminator); } CheckType::Panic | CheckType::NoCore => { tcx.sess @@ -199,10 +204,11 @@ impl MutableBody { /// Add a new call to the basic block indicated by the given index. /// - /// The new call will have the same span as the source instruction, and the basic block - /// will be split. The source instruction will be adjusted to point to the first instruction in - /// the new basic block. - pub fn add_call( + /// The new call will have the same span as the source instruction, and the basic block will be + /// split. If `InsertPosition` is `InsertPosition::Before`, `source` will point to the same + /// instruction as before. If `InsertPosition` is `InsertPosition::After`, `source` will point + /// to the new terminator. + pub fn insert_call( &mut self, callee: &Instance, source: &mut SourceInstruction, @@ -222,13 +228,14 @@ impl MutableBody { unwind: UnwindAction::Terminate, }; let terminator = Terminator { kind, span }; - self.split_bb(source, position, terminator); + self.insert_terminator(source, position, terminator); } - /// Split a basic block and use the new terminator in the basic block that was split. - /// - /// The source is updated to point to the same instruction which is now in the new basic block. - pub fn split_bb( + /// Split a basic block and use the new terminator in the basic block that was split. If + /// `InsertPosition` is `InsertPosition::Before`, `source` will point to the same instruction as + /// before. If `InsertPosition` is `InsertPosition::After`, `source` will point to the new + /// terminator. + fn split_bb( &mut self, source: &mut SourceInstruction, position: InsertPosition, @@ -245,6 +252,7 @@ impl MutableBody { } /// Split a basic block right before the source location. + /// `source` will point to the same instruction as before after the function is done. fn split_bb_before(&mut self, source: &mut SourceInstruction, new_term: Terminator) { let new_bb_idx = self.blocks.len(); let (idx, bb) = match source { @@ -268,6 +276,7 @@ impl MutableBody { } /// Split a basic block right after the source location. + /// `source` will point to the new terminator after the function is done. fn split_bb_after(&mut self, source: &mut SourceInstruction, mut new_term: Terminator) { let new_bb_idx = self.blocks.len(); match source { @@ -275,39 +284,69 @@ impl MutableBody { // and move the remaining statements into the new one. SourceInstruction::Statement { idx, bb } => { let (orig_idx, orig_bb) = (*idx, *bb); - *idx = 0; - *bb = new_bb_idx; let old_term = mem::replace(&mut self.blocks[orig_bb].terminator, new_term); let bb_stmts = &mut self.blocks[orig_bb].statements; let remaining = bb_stmts.split_off(orig_idx + 1); let new_bb = BasicBlock { statements: remaining, terminator: old_term }; self.blocks.push(new_bb); + // Update the source to point at the terminator. + *source = SourceInstruction::Terminator { bb: orig_bb }; } // Make the terminator at `source` point at the new block, // the terminator of which is a simple Goto instruction. SourceInstruction::Terminator { bb } => { - let current_terminator = &mut self.blocks.get_mut(*bb).unwrap().terminator; - // Kani can only instrument function calls like this. - match (&mut current_terminator.kind, &mut new_term.kind) { - ( - TerminatorKind::Call { target: Some(target_bb), .. }, - TerminatorKind::Call { target: Some(new_target_bb), .. }, - ) => { - // Set the new terminator to point where previous terminator pointed. - *new_target_bb = *target_bb; - // Point the current terminator to the new terminator's basic block. - *target_bb = new_bb_idx; - // Update the current poisition. - *bb = new_bb_idx; - self.blocks.push(BasicBlock { statements: vec![], terminator: new_term }); - } - _ => unimplemented!("Kani can only split blocks after calls."), - }; + let current_term = &mut self.blocks.get_mut(*bb).unwrap().terminator; + let target_bb = get_mut_target_ref(current_term); + let new_target_bb = get_mut_target_ref(&mut new_term); + // Set the new terminator to point where previous terminator pointed. + *new_target_bb = *target_bb; + // Point the current terminator to the new terminator's basic block. + *target_bb = new_bb_idx; + // Update the source to point at the terminator. + *bb = new_bb_idx; + self.blocks.push(BasicBlock { statements: vec![], terminator: new_term }); } }; } - /// Insert statement before or after the source instruction and update the source as needed. + /// Insert basic block before or after the source instruction and update `source` accordingly. If + /// `InsertPosition` is `InsertPosition::Before`, `source` will point to the same instruction as + /// before. If `InsertPosition` is `InsertPosition::After`, `source` will point to the + /// terminator of the newly inserted basic block. + pub fn insert_bb( + &mut self, + mut bb: BasicBlock, + source: &mut SourceInstruction, + position: InsertPosition, + ) { + // Splitting adds 1 block, so the added block index is len + 1; + let split_bb_idx = self.blocks().len(); + let inserted_bb_idx = self.blocks().len() + 1; + // Update the terminator of the basic block to point at the remaining part of the split + // basic block. + let target = get_mut_target_ref(&mut bb.terminator); + *target = split_bb_idx; + let new_term = Terminator { + kind: TerminatorKind::Goto { target: inserted_bb_idx }, + span: source.span(&self.blocks), + }; + self.split_bb(source, position, new_term); + self.blocks.push(bb); + } + + pub fn insert_terminator( + &mut self, + source: &mut SourceInstruction, + position: InsertPosition, + terminator: Terminator, + ) { + self.split_bb(source, position, terminator); + } + + /// Insert statement before or after the source instruction and update the source as needed. If + /// `InsertPosition` is `InsertPosition::Before`, `source` will point to the same instruction as + /// before. If `InsertPosition` is `InsertPosition::After`, `source` will point to the + /// newly inserted statement. pub fn insert_stmt( &mut self, new_stmt: Statement, @@ -338,22 +377,18 @@ impl MutableBody { SourceInstruction::Terminator { bb } => { // Create a new basic block, as we need to append a statement after the terminator. let current_terminator = &mut self.blocks.get_mut(*bb).unwrap().terminator; - // Kani can only instrument function calls in this way. - match &mut current_terminator.kind { - TerminatorKind::Call { target: Some(target_bb), .. } => { - *source = SourceInstruction::Statement { idx: 0, bb: new_bb_idx }; - let new_bb = BasicBlock { - statements: vec![new_stmt], - terminator: Terminator { - kind: TerminatorKind::Goto { target: *target_bb }, - span, - }, - }; - *target_bb = new_bb_idx; - self.blocks.push(new_bb); - } - _ => unimplemented!("Kani can only insert statements after calls."), + // Update target of the terminator. + let target_bb = get_mut_target_ref(current_terminator); + *source = SourceInstruction::Statement { idx: 0, bb: new_bb_idx }; + let new_bb = BasicBlock { + statements: vec![new_stmt], + terminator: Terminator { + kind: TerminatorKind::Goto { target: *target_bb }, + span, + }, }; + *target_bb = new_bb_idx; + self.blocks.push(new_bb); } } } @@ -574,3 +609,15 @@ pub trait MutMirVisitor { } } } + +fn get_mut_target_ref(terminator: &mut Terminator) -> &mut BasicBlockIdx { + match &mut terminator.kind { + TerminatorKind::Assert { target, .. } + | TerminatorKind::Drop { target, .. } + | TerminatorKind::Goto { target } + | TerminatorKind::Call { target: Some(target), .. } => target, + _ => unimplemented!( + "Kani can only insert instructions after terminators that have a `target` field." + ), + } +} 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 56840bb988d7..f1ae463e66c3 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -233,7 +233,7 @@ impl UninitPass { *pointee_info.ty(), ); collect_skipped(&operation, body, skip_first); - body.add_call( + body.insert_call( &is_ptr_initialized_instance, source, operation.position(), @@ -260,7 +260,7 @@ impl UninitPass { let layout_operand = mk_layout_operand(body, source, operation.position(), &element_layout); collect_skipped(&operation, body, skip_first); - body.add_call( + body.insert_call( &is_ptr_initialized_instance, source, operation.position(), @@ -279,7 +279,7 @@ impl UninitPass { // Make sure all non-padding bytes are initialized. collect_skipped(&operation, body, skip_first); let ptr_operand_ty = ptr_operand.ty(body.locals()).unwrap(); - body.add_check( + body.insert_check( tcx, &self.check_type, source, @@ -348,7 +348,7 @@ impl UninitPass { *pointee_info.ty(), ); collect_skipped(&operation, body, skip_first); - body.add_call( + body.insert_call( &set_ptr_initialized_instance, source, operation.position(), @@ -375,7 +375,7 @@ impl UninitPass { let layout_operand = mk_layout_operand(body, source, operation.position(), &element_layout); collect_skipped(&operation, body, skip_first); - body.add_call( + body.insert_call( &set_ptr_initialized_instance, source, operation.position(), @@ -443,8 +443,8 @@ impl UninitPass { span, user_ty: None, })); - let result = body.new_assignment(rvalue, source, position); - body.add_check(tcx, &self.check_type, source, position, result, reason); + let result = body.insert_assignment(rvalue, source, position); + body.insert_check(tcx, &self.check_type, source, position, result, reason); } } @@ -467,7 +467,7 @@ pub fn mk_layout_operand( layout_byte_mask: &[bool], ) -> Operand { Operand::Move(Place { - local: body.new_assignment( + local: body.insert_assignment( Rvalue::Aggregate( AggregateKind::Array(Ty::bool_ty()), layout_byte_mask @@ -566,7 +566,7 @@ fn inject_memory_init_setup( ) .unwrap(); - new_body.add_call( + new_body.insert_call( &memory_initialization_init, &mut source, InsertPosition::Before, diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs index 96790f594a82..787b55172bfd 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs @@ -59,7 +59,7 @@ impl MemoryInitOp { Operand::Copy(place) | Operand::Move(place) => place, Operand::Constant(_) => unreachable!(), }; - body.new_assignment( + body.insert_assignment( Rvalue::AddressOf(Mutability::Not, place.clone()), source, self.position(), diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index a7d0f14d270f..a81f76d25393 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -85,13 +85,13 @@ impl ValidValuePass { for operation in instruction.operations { match operation { SourceOp::BytesValidity { ranges, target_ty, rvalue } => { - let value = body.new_assignment(rvalue, &mut source, InsertPosition::Before); + let value = body.insert_assignment(rvalue, &mut source, InsertPosition::Before); let rvalue_ptr = Rvalue::AddressOf(Mutability::Not, Place::from(value)); for range in ranges { let result = build_limits(body, &range, rvalue_ptr.clone(), &mut source); let msg = format!("Undefined Behavior: Invalid value of type `{target_ty}`",); - body.add_check( + body.insert_check( tcx, &self.check_type, &mut source, @@ -106,7 +106,7 @@ impl ValidValuePass { let result = build_limits(body, &range, rvalue.clone(), &mut source); let msg = format!("Undefined Behavior: Invalid value of type `{pointee_ty}`",); - body.add_check( + body.insert_check( tcx, &self.check_type, &mut source, @@ -139,8 +139,8 @@ impl ValidValuePass { span, user_ty: None, })); - let result = body.new_assignment(rvalue, source, InsertPosition::Before); - body.add_check(tcx, &self.check_type, source, InsertPosition::Before, result, reason); + let result = body.insert_assignment(rvalue, source, InsertPosition::Before); + body.insert_check(tcx, &self.check_type, source, InsertPosition::Before, result, reason); } } @@ -771,24 +771,25 @@ pub fn build_limits( let span = source.span(body.blocks()); debug!(?req, ?rvalue_ptr, ?span, "build_limits"); let primitive_ty = uint_ty(req.size.bytes()); - let start_const = body.new_const_operand(req.valid_range.start, primitive_ty, span); - let end_const = body.new_const_operand(req.valid_range.end, primitive_ty, span); + let start_const = body.new_uint_operand(req.valid_range.start, primitive_ty, span); + let end_const = body.new_uint_operand(req.valid_range.end, primitive_ty, span); let orig_ptr = if req.offset != 0 { - let start_ptr = move_local(body.new_assignment(rvalue_ptr, source, InsertPosition::Before)); - let byte_ptr = move_local(body.new_cast_ptr( + let start_ptr = + move_local(body.insert_assignment(rvalue_ptr, source, InsertPosition::Before)); + let byte_ptr = move_local(body.insert_ptr_cast( start_ptr, Ty::unsigned_ty(UintTy::U8), Mutability::Not, source, InsertPosition::Before, )); - let offset_const = body.new_const_operand(req.offset as _, UintTy::Usize, span); - let offset = move_local(body.new_assignment( + let offset_const = body.new_uint_operand(req.offset as _, UintTy::Usize, span); + let offset = move_local(body.insert_assignment( Rvalue::Use(offset_const), source, InsertPosition::Before, )); - move_local(body.new_binary_op( + move_local(body.insert_binary_op( BinOp::Offset, byte_ptr, offset, @@ -796,9 +797,9 @@ pub fn build_limits( InsertPosition::Before, )) } else { - move_local(body.new_assignment(rvalue_ptr, source, InsertPosition::Before)) + move_local(body.insert_assignment(rvalue_ptr, source, InsertPosition::Before)) }; - let value_ptr = body.new_cast_ptr( + let value_ptr = body.insert_ptr_cast( orig_ptr, Ty::unsigned_ty(primitive_ty), Mutability::Not, @@ -806,13 +807,18 @@ pub fn build_limits( InsertPosition::Before, ); let value = Operand::Copy(Place { local: value_ptr, projection: vec![ProjectionElem::Deref] }); - let start_result = - body.new_binary_op(BinOp::Ge, value.clone(), start_const, source, InsertPosition::Before); + let start_result = body.insert_binary_op( + BinOp::Ge, + value.clone(), + start_const, + source, + InsertPosition::Before, + ); let end_result = - body.new_binary_op(BinOp::Le, value, end_const, source, InsertPosition::Before); + body.insert_binary_op(BinOp::Le, value, end_const, source, InsertPosition::Before); if req.valid_range.wraps_around() { // valid >= start || valid <= end - body.new_binary_op( + body.insert_binary_op( BinOp::BitOr, move_local(start_result), move_local(end_result), @@ -821,7 +827,7 @@ pub fn build_limits( ) } else { // valid >= start && valid <= end - body.new_binary_op( + body.insert_binary_op( BinOp::BitAnd, move_local(start_result), move_local(end_result), diff --git a/kani-compiler/src/kani_middle/transform/dump_mir_pass.rs b/kani-compiler/src/kani_middle/transform/dump_mir_pass.rs new file mode 100644 index 000000000000..9393ec0d88c9 --- /dev/null +++ b/kani-compiler/src/kani_middle/transform/dump_mir_pass.rs @@ -0,0 +1,69 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Global transformation pass, which does not modify bodies but dumps MIR whenever the appropriate debug flag is passed. + +use crate::kani_middle::reachability::CallGraph; +use crate::kani_middle::transform::GlobalPass; +use crate::kani_queries::QueryDb; +use kani_metadata::ArtifactType; +use rustc_middle::ty::TyCtxt; +use rustc_session::config::OutputType; +use stable_mir::mir::mono::{Instance, MonoItem}; +use std::fs::File; +use std::io::BufWriter; +use std::io::Write; + +use super::BodyTransformation; + +/// Dump all MIR bodies. +#[derive(Debug)] +pub struct DumpMirPass { + enabled: bool, +} + +impl DumpMirPass { + pub fn new(tcx: TyCtxt) -> Self { + Self { enabled: tcx.sess.opts.output_types.contains_key(&OutputType::Mir) } + } +} + +impl GlobalPass for DumpMirPass { + fn is_enabled(&self, _query_db: &QueryDb) -> bool { + self.enabled + } + + fn transform( + &mut self, + tcx: TyCtxt, + _call_graph: &CallGraph, + starting_items: &[MonoItem], + instances: Vec, + transformer: &mut BodyTransformation, + ) { + // Create output buffer. + let file_path = { + let base_path = tcx.output_filenames(()).path(OutputType::Object); + let base_name = base_path.as_path(); + let entry_point = (starting_items.len() == 1).then_some(starting_items[0].clone()); + // If there is a single entry point, use it as a file name. + if let Some(MonoItem::Fn(starting_instance)) = entry_point { + let mangled_name = starting_instance.mangled_name(); + let file_stem = + format!("{}_{mangled_name}", base_name.file_stem().unwrap().to_str().unwrap()); + base_name.with_file_name(file_stem).with_extension(ArtifactType::SymTabGoto) + } else { + // Otherwise, use the object output path from the compiler. + base_name.with_extension(ArtifactType::SymTabGoto) + } + }; + let out_file = File::create(file_path.with_extension("kani.mir")).unwrap(); + let mut writer = BufWriter::new(out_file); + + // For each def_id, dump their MIR. + for instance in instances.iter() { + writeln!(writer, "// Item: {} ({})", instance.name(), instance.mangled_name()).unwrap(); + let _ = transformer.body(tcx, *instance).dump(&mut writer, &instance.name()); + } + } +} diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index c4534bf11b4d..d6475465d1b1 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -136,11 +136,11 @@ impl IntrinsicGeneratorPass { user_ty: None, })); let result = - new_body.new_assignment(rvalue, &mut terminator, InsertPosition::Before); + 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.add_check( + new_body.insert_check( tcx, &self.check_type, &mut terminator, @@ -212,7 +212,7 @@ impl IntrinsicGeneratorPass { InsertPosition::Before, &layout, ); - new_body.add_call( + new_body.insert_call( &is_ptr_initialized_instance, &mut terminator, InsertPosition::Before, @@ -242,7 +242,7 @@ impl IntrinsicGeneratorPass { InsertPosition::Before, &element_layout, ); - new_body.add_call( + new_body.insert_call( &is_ptr_initialized_instance, &mut terminator, InsertPosition::Before, @@ -256,14 +256,14 @@ impl IntrinsicGeneratorPass { span, user_ty: None, })); - let result = new_body.new_assignment( + let result = new_body.insert_assignment( rvalue, &mut terminator, InsertPosition::Before, ); let reason: &str = "Kani does not support reasoning about memory initialization of pointers to trait objects."; - new_body.add_check( + new_body.insert_check( tcx, &self.check_type, &mut terminator, @@ -282,11 +282,11 @@ impl IntrinsicGeneratorPass { user_ty: None, })); let result = - new_body.new_assignment(rvalue, &mut terminator, InsertPosition::Before); + new_body.insert_assignment(rvalue, &mut terminator, InsertPosition::Before); let reason = format!( "Kani currently doesn't support checking memory initialization of `{target_ty}`. {msg}" ); - new_body.add_check( + new_body.insert_check( tcx, &self.check_type, &mut terminator, diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index 26a95978fcaf..5b497b09619d 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -17,6 +17,7 @@ //! For all instrumentation passes, always use exhaustive matches to ensure soundness in case a new //! case is added. use crate::kani_middle::codegen_units::CodegenUnit; +use crate::kani_middle::reachability::CallGraph; use crate::kani_middle::transform::body::CheckType; use crate::kani_middle::transform::check_uninit::UninitPass; use crate::kani_middle::transform::check_values::ValidValuePass; @@ -24,8 +25,9 @@ use crate::kani_middle::transform::contracts::AnyModifiesPass; use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass; use crate::kani_middle::transform::stubs::{ExternFnStubPass, FnStubPass}; use crate::kani_queries::QueryDb; +use dump_mir_pass::DumpMirPass; use rustc_middle::ty::TyCtxt; -use stable_mir::mir::mono::Instance; +use stable_mir::mir::mono::{Instance, MonoItem}; use stable_mir::mir::Body; use std::collections::HashMap; use std::fmt::Debug; @@ -34,6 +36,7 @@ pub(crate) mod body; mod check_uninit; mod check_values; mod contracts; +mod dump_mir_pass; mod kani_intrinsics; mod stubs; @@ -90,7 +93,8 @@ impl BodyTransformation { transformer } - /// Retrieve the body of an instance. + /// Retrieve the body of an instance. This does not apply global passes, but will retrieve the + /// body after global passes running if they were previously applied. /// /// Note that this assumes that the instance does have a body since existing consumers already /// assume that. Use `instance.has_body()` to check if an instance has a body. @@ -152,6 +156,23 @@ pub(crate) trait TransformPass: Debug { fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body); } +/// A trait to represent transformation passes that operate on the whole codegen unit. +pub(crate) trait GlobalPass: Debug { + fn is_enabled(&self, query_db: &QueryDb) -> bool + where + Self: Sized; + + /// Run a transformation pass on the whole codegen unit. + fn transform( + &mut self, + tcx: TyCtxt, + call_graph: &CallGraph, + starting_items: &[MonoItem], + instances: Vec, + transformer: &mut BodyTransformation, + ); +} + /// The transformation result. /// We currently only cache the body of functions that were instrumented. #[derive(Clone, Debug)] @@ -159,3 +180,37 @@ enum TransformationResult { Modified(Body), NotModified, } + +pub struct GlobalPasses { + /// The passes that operate on the whole codegen unit, they run after all previous passes are + /// done. + global_passes: Vec>, +} + +impl GlobalPasses { + pub fn new(queries: &QueryDb, tcx: TyCtxt) -> Self { + let mut global_passes = GlobalPasses { global_passes: vec![] }; + global_passes.add_global_pass(queries, DumpMirPass::new(tcx)); + global_passes + } + + fn add_global_pass(&mut self, query_db: &QueryDb, pass: P) { + if pass.is_enabled(&query_db) { + self.global_passes.push(Box::new(pass)) + } + } + + /// Run all global passes and store the results in a cache that can later be queried by `body`. + pub fn run_global_passes( + &mut self, + transformer: &mut BodyTransformation, + tcx: TyCtxt, + starting_items: &[MonoItem], + instances: Vec, + call_graph: CallGraph, + ) { + for global_pass in self.global_passes.iter_mut() { + global_pass.transform(tcx, &call_graph, starting_items, instances.clone(), transformer); + } + } +} diff --git a/kani-dependencies b/kani-dependencies index 200755839284..844d83c23dc7 100644 --- a/kani-dependencies +++ b/kani-dependencies @@ -4,7 +4,7 @@ CBMC_VERSION="5.95.1" # If you update this version number, remember to bump it in `src/setup.rs` too CBMC_VIEWER_MAJOR="3" -CBMC_VIEWER_MINOR="8" -CBMC_VIEWER_VERSION="3.8" +CBMC_VIEWER_MINOR="9" +CBMC_VIEWER_VERSION="3.9" KISSAT_VERSION="3.1.1" diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs index 424ca2485d57..ef6e2ef23dd4 100644 --- a/library/kani/src/arbitrary.rs +++ b/library/kani/src/arbitrary.rs @@ -16,12 +16,7 @@ where Self: Sized, { fn any() -> Self; - fn any_array() -> [Self; MAX_ARRAY_LENGTH] - // the requirement defined in the where clause must appear on the `impl`'s method `any_array` - // but also on the corresponding trait's method - where - [(); std::mem::size_of::<[Self; MAX_ARRAY_LENGTH]>()]:, - { + fn any_array() -> [Self; MAX_ARRAY_LENGTH] { [(); MAX_ARRAY_LENGTH].map(|_| Self::any()) } } @@ -33,20 +28,10 @@ macro_rules! trivial_arbitrary { #[inline(always)] fn any() -> Self { // This size_of call does not use generic_const_exprs feature. It's inside a macro, and Self isn't generic. - unsafe { crate::any_raw_internal::() }>() } + unsafe { crate::any_raw_internal::() } } - fn any_array() -> [Self; MAX_ARRAY_LENGTH] - where - // `generic_const_exprs` requires all potential errors to be reflected in the signature/header. - // We must repeat the expression in the header, to make sure that if the body can fail the header will also fail. - [(); { std::mem::size_of::<[$type; MAX_ARRAY_LENGTH]>() }]:, - { - unsafe { - crate::any_raw_internal::< - [Self; MAX_ARRAY_LENGTH], - { std::mem::size_of::<[Self; MAX_ARRAY_LENGTH]>() }, - >() - } + fn any_array() -> [Self; MAX_ARRAY_LENGTH] { + unsafe { crate::any_raw_internal::<[Self; MAX_ARRAY_LENGTH]>() } } } }; @@ -128,7 +113,6 @@ nonzero_arbitrary!(NonZeroIsize, isize); impl Arbitrary for [T; N] where T: Arbitrary, - [(); std::mem::size_of::<[T; N]>()]:, { fn any() -> Self { T::any_array() diff --git a/library/kani/src/concrete_playback.rs b/library/kani/src/concrete_playback.rs index 711b9b005624..aa6cd7e4018d 100644 --- a/library/kani/src/concrete_playback.rs +++ b/library/kani/src/concrete_playback.rs @@ -47,19 +47,17 @@ pub fn concrete_playback_run(mut local_concrete_vals: Vec>, pro /// # Safety /// /// The semantics of this function require that SIZE_T equals the size of type T. -pub(crate) unsafe fn any_raw_internal() -> T { +pub(crate) unsafe fn any_raw_internal() -> T { + let sz = size_of::(); let mut next_concrete_val: Vec = Vec::new(); CONCRETE_VALS.with(|glob_concrete_vals| { let mut_ref_glob_concrete_vals = &mut *glob_concrete_vals.borrow_mut(); - next_concrete_val = if SIZE_T > 0 { + next_concrete_val = if sz > 0 { mut_ref_glob_concrete_vals.pop().expect("Not enough det vals found") } else { vec![] }; }); - let next_concrete_val_len = next_concrete_val.len(); - let bytes_t: [u8; SIZE_T] = next_concrete_val.try_into().expect(&format!( - "Expected {SIZE_T} bytes instead of {next_concrete_val_len} bytes in the following det vals vec" - )); - std::mem::transmute_copy::<[u8; SIZE_T], T>(&bytes_t) + assert_eq!(next_concrete_val.len(), sz, "Expected {sz} bytes in the following det vals vec"); + unsafe { *(next_concrete_val.as_ptr() as *mut T) } } diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 7487cc26b186..3cf46bd7af07 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -7,11 +7,10 @@ // Used for rustc_diagnostic_item. // Note: We could use a kanitool attribute instead. #![feature(rustc_attrs)] -// This is required for the optimized version of `any_array()` -#![feature(generic_const_exprs)] -#![allow(incomplete_features)] // Used to model simd. #![feature(repr_simd)] +#![feature(generic_const_exprs)] +#![allow(incomplete_features)] // Features used for tests only. #![cfg_attr(test, feature(core_intrinsics, portable_simd))] // Required for `rustc_diagnostic_item` and `core_intrinsics` @@ -21,6 +20,9 @@ #![feature(f16)] #![feature(f128)] +// Allow us to use `kani::` to access crate features. +extern crate self as kani; + pub mod arbitrary; #[cfg(feature = "concrete_playback")] mod concrete_playback; @@ -48,6 +50,7 @@ pub use invariant::Invariant; pub fn concrete_playback_run(_: Vec>, _: F) { unreachable!("Concrete playback does not work during verification") } + pub use futures::{block_on, block_on_with_spawn, spawn, yield_now, RoundRobin}; /// Creates an assumption that will be valid after this statement run. Note that the assumption @@ -246,21 +249,21 @@ pub fn any_where bool>(f: F) -> T { /// Note that SIZE_T must be equal the size of type T in bytes. #[inline(never)] #[cfg(not(feature = "concrete_playback"))] -pub(crate) unsafe fn any_raw_internal() -> T { +pub(crate) unsafe fn any_raw_internal() -> T { any_raw_inner::() } #[inline(never)] #[cfg(feature = "concrete_playback")] -pub(crate) unsafe fn any_raw_internal() -> T { - concrete_playback::any_raw_internal::() +pub(crate) unsafe fn any_raw_internal() -> T { + concrete_playback::any_raw_internal::() } /// This low-level function returns nondet bytes of size T. #[rustc_diagnostic_item = "KaniAnyRaw"] #[inline(never)] #[allow(dead_code)] -fn any_raw_inner() -> T { +fn any_raw_inner() -> T { kani_intrinsic() } diff --git a/library/kani/src/mem_init.rs b/library/kani/src/mem_init.rs index 08550fd67200..3755fc59a510 100644 --- a/library/kani/src/mem_init.rs +++ b/library/kani/src/mem_init.rs @@ -50,6 +50,7 @@ impl MemoryInitializationState { /// /// Such definition is necessary since both tracked object and tracked offset are chosen /// non-deterministically. + #[kanitool::disable_checks(pointer)] pub fn get( &mut self, ptr: *const u8, @@ -61,7 +62,7 @@ impl MemoryInitializationState { && self.tracked_offset >= offset && self.tracked_offset < offset + LAYOUT_SIZE { - !layout[(self.tracked_offset - offset) % LAYOUT_SIZE] || self.value + !layout[self.tracked_offset - offset] || self.value } else { true } @@ -73,6 +74,7 @@ impl MemoryInitializationState { /// /// Such definition is necessary since both tracked object and tracked offset are chosen /// non-deterministically. + #[kanitool::disable_checks(pointer)] pub fn set( &mut self, ptr: *const u8, @@ -85,7 +87,7 @@ impl MemoryInitializationState { && self.tracked_offset >= offset && self.tracked_offset < offset + LAYOUT_SIZE { - self.value = layout[(self.tracked_offset - offset) % LAYOUT_SIZE] && value; + self.value = layout[self.tracked_offset - offset] && value; } } @@ -122,6 +124,7 @@ impl MemoryInitializationState { /// /// Such definition is necessary since both tracked object and tracked offset are chosen /// non-deterministically. + #[kanitool::disable_checks(pointer)] pub fn get_slice( &mut self, ptr: *const u8, @@ -146,6 +149,7 @@ impl MemoryInitializationState { /// /// Such definition is necessary since both tracked object and tracked offset are chosen /// non-deterministically. + #[kanitool::disable_checks(pointer)] pub fn set_slice( &mut self, ptr: *const u8, @@ -169,6 +173,7 @@ impl MemoryInitializationState { static mut MEM_INIT_STATE: MemoryInitializationState = MemoryInitializationState::new(); /// Set tracked object and tracked offset to a non-deterministic value. +#[kanitool::disable_checks(pointer)] #[rustc_diagnostic_item = "KaniInitializeMemoryInitializationState"] fn initialize_memory_initialization_state() { unsafe { @@ -179,6 +184,7 @@ fn initialize_memory_initialization_state() { } /// Get initialization state of `num_elts` items laid out according to the `layout` starting at address `ptr`. +#[kanitool::disable_checks(pointer)] #[rustc_diagnostic_item = "KaniIsPtrInitialized"] fn is_ptr_initialized( ptr: *const T, @@ -192,6 +198,7 @@ fn is_ptr_initialized( } /// Set initialization state to `value` for `num_elts` items laid out according to the `layout` starting at address `ptr`. +#[kanitool::disable_checks(pointer)] #[rustc_diagnostic_item = "KaniSetPtrInitialized"] fn set_ptr_initialized( ptr: *const T, @@ -208,6 +215,7 @@ fn set_ptr_initialized( } /// Get initialization state of `num_elts` items laid out according to the `layout` starting at address `ptr`. +#[kanitool::disable_checks(pointer)] #[rustc_diagnostic_item = "KaniIsSliceChunkPtrInitialized"] fn is_slice_chunk_ptr_initialized( ptr: *const T, @@ -222,6 +230,7 @@ fn is_slice_chunk_ptr_initialized( } /// Set initialization state to `value` for `num_elts` items laid out according to the `layout` starting at address `ptr`. +#[kanitool::disable_checks(pointer)] #[rustc_diagnostic_item = "KaniSetSliceChunkPtrInitialized"] fn set_slice_chunk_ptr_initialized( ptr: *const T, @@ -239,6 +248,7 @@ fn set_slice_chunk_ptr_initialized( } /// Get initialization state of the slice, items of which are laid out according to the `layout` starting at address `ptr`. +#[kanitool::disable_checks(pointer)] #[rustc_diagnostic_item = "KaniIsSlicePtrInitialized"] fn is_slice_ptr_initialized( ptr: *const [T], @@ -252,6 +262,7 @@ fn is_slice_ptr_initialized( } /// Set initialization state of the slice, items of which are laid out according to the `layout` starting at address `ptr` to `value`. +#[kanitool::disable_checks(pointer)] #[rustc_diagnostic_item = "KaniSetSlicePtrInitialized"] fn set_slice_ptr_initialized( ptr: *const [T], @@ -268,6 +279,7 @@ fn set_slice_ptr_initialized( } /// Get initialization state of the string slice, items of which are laid out according to the `layout` starting at address `ptr`. +#[kanitool::disable_checks(pointer)] #[rustc_diagnostic_item = "KaniIsStrPtrInitialized"] fn is_str_ptr_initialized( ptr: *const str, @@ -281,6 +293,7 @@ fn is_str_ptr_initialized( } /// Set initialization state of the string slice, items of which are laid out according to the `layout` starting at address `ptr` to `value`. +#[kanitool::disable_checks(pointer)] #[rustc_diagnostic_item = "KaniSetStrPtrInitialized"] fn set_str_ptr_initialized( ptr: *const str, diff --git a/library/kani/src/vec.rs b/library/kani/src/vec.rs index 626d152f02d4..a3ec05a9c953 100644 --- a/library/kani/src/vec.rs +++ b/library/kani/src/vec.rs @@ -6,7 +6,6 @@ use crate::{any, any_where, Arbitrary}; pub fn any_vec() -> Vec where T: Arbitrary, - [(); std::mem::size_of::<[T; MAX_LENGTH]>()]:, { let real_length: usize = any_where(|sz| *sz <= MAX_LENGTH); match real_length { @@ -26,7 +25,6 @@ where pub fn exact_vec() -> Vec where T: Arbitrary, - [(); std::mem::size_of::<[T; EXACT_LENGTH]>()]:, { let boxed_array: Box<[T; EXACT_LENGTH]> = Box::new(any()); <[T]>::into_vec(boxed_array) diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs index a8271ad758cf..7cfb649b11a0 100644 --- a/library/kani_core/src/arbitrary.rs +++ b/library/kani_core/src/arbitrary.rs @@ -8,6 +8,7 @@ //! //! TODO: Use this inside kani library so that we dont have to maintain two copies of the same proc macro for arbitrary. #[macro_export] +#[allow(clippy::crate_in_macro_def)] macro_rules! generate_arbitrary { ($core:path) => { use core_path::marker::{PhantomData, PhantomPinned}; @@ -18,13 +19,7 @@ macro_rules! generate_arbitrary { Self: Sized, { fn any() -> Self; - #[cfg(kani_sysroot)] - fn any_array() -> [Self; MAX_ARRAY_LENGTH] - // the requirement defined in the where clause must appear on the `impl`'s method `any_array` - // but also on the corresponding trait's method - where - [(); core_path::mem::size_of::<[Self; MAX_ARRAY_LENGTH]>()]:, - { + fn any_array() -> [Self; MAX_ARRAY_LENGTH] { [(); MAX_ARRAY_LENGTH].map(|_| Self::any()) } } @@ -36,22 +31,10 @@ macro_rules! generate_arbitrary { #[inline(always)] fn any() -> Self { // This size_of call does not use generic_const_exprs feature. It's inside a macro, and Self isn't generic. - unsafe { any_raw_internal::() }>() } + unsafe { crate::kani::any_raw_internal::() } } - // Disable this for standard library since we cannot enable generic constant expr. - #[cfg(kani_sysroot)] - fn any_array() -> [Self; MAX_ARRAY_LENGTH] - where - // `generic_const_exprs` requires all potential errors to be reflected in the signature/header. - // We must repeat the expression in the header, to make sure that if the body can fail the header will also fail. - [(); { core_path::mem::size_of::<[$type; MAX_ARRAY_LENGTH]>() }]:, - { - unsafe { - any_raw_internal::< - [Self; MAX_ARRAY_LENGTH], - { core_path::mem::size_of::<[Self; MAX_ARRAY_LENGTH]>() }, - >() - } + fn any_array() -> [Self; MAX_ARRAY_LENGTH] { + unsafe { crate::kani::any_raw_internal::<[Self; MAX_ARRAY_LENGTH]>() } } } }; @@ -134,6 +117,15 @@ macro_rules! generate_arbitrary { } } + impl Arbitrary for [T; N] + where + T: Arbitrary, + { + fn any() -> Self { + T::any_array::() + } + } + impl Arbitrary for Option where T: Arbitrary, @@ -165,15 +157,33 @@ macro_rules! generate_arbitrary { } } - #[cfg(kani_sysroot)] - impl Arbitrary for [T; N] - where - T: Arbitrary, - [(); core_path::mem::size_of::<[T; N]>()]:, - { + arbitrary_tuple!(A); + arbitrary_tuple!(A, B); + arbitrary_tuple!(A, B, C); + arbitrary_tuple!(A, B, C, D); + arbitrary_tuple!(A, B, C, D, E); + arbitrary_tuple!(A, B, C, D, E, F); + arbitrary_tuple!(A, B, C, D, E, F, G); + arbitrary_tuple!(A, B, C, D, E, F, G, H); + arbitrary_tuple!(A, B, C, D, E, F, G, H, I); + arbitrary_tuple!(A, B, C, D, E, F, G, H, I, J); + arbitrary_tuple!(A, B, C, D, E, F, G, H, I, J, K); + arbitrary_tuple!(A, B, C, D, E, F, G, H, I, J, K, L); + }; +} + +/// This macro implements `kani::Arbitrary` on a tuple whose elements +/// already implement `kani::Arbitrary` by running `kani::any()` on +/// each index of the tuple. +#[allow(clippy::crate_in_macro_def)] +#[macro_export] +macro_rules! arbitrary_tuple { + ($($type:ident),*) => { + impl<$($type : Arbitrary),*> Arbitrary for ($($type,)*) { + #[inline(always)] fn any() -> Self { - T::any_array() + ($(crate::kani::any::<$type>(),)*) } } - }; + } } diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 68a8e79658f1..016c805e8f8e 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -60,6 +60,7 @@ macro_rules! kani_lib { /// such as core in rust's std library itself. /// /// TODO: Use this inside kani library so that we dont have to maintain two copies of the same intrinsics. +#[allow(clippy::crate_in_macro_def)] #[macro_export] macro_rules! kani_intrinsics { ($core:tt) => { @@ -180,7 +181,7 @@ macro_rules! kani_intrinsics { /// under all possible `NonZeroU8` input values, i.e., all possible `u8` values except zero. /// /// ```rust - /// let inputA = kani::any::(); + /// let inputA = kani::any::(); /// fn_under_verification(inputA); /// ``` /// @@ -247,21 +248,21 @@ macro_rules! kani_intrinsics { /// Note that SIZE_T must be equal the size of type T in bytes. #[inline(never)] #[cfg(not(feature = "concrete_playback"))] - pub(crate) unsafe fn any_raw_internal() -> T { + pub(crate) unsafe fn any_raw_internal() -> T { any_raw_inner::() } #[inline(never)] #[cfg(feature = "concrete_playback")] - pub(crate) unsafe fn any_raw_internal() -> T { - concrete_playback::any_raw_internal::() + pub(crate) unsafe fn any_raw_internal() -> T { + concrete_playback::any_raw_internal::() } /// This low-level function returns nondet bytes of size T. #[rustc_diagnostic_item = "KaniAnyRaw"] #[inline(never)] #[allow(dead_code)] - pub fn any_raw_inner() -> T { + pub fn any_raw_inner() -> T { kani_intrinsic() } @@ -269,7 +270,7 @@ macro_rules! kani_intrinsics { /// supported by Kani display. /// /// During verification this will get replaced by `assert(false)`. For concrete executions, we just - /// invoke the regular `std::panic!()` function. This function is used by our standard library + /// invoke the regular `core::panic!()` function. This function is used by our standard library /// overrides, but not the other way around. #[inline(never)] #[rustc_diagnostic_item = "KaniPanic"] @@ -294,6 +295,8 @@ macro_rules! kani_intrinsics { } pub mod internal { + use crate::kani::Arbitrary; + use core::ptr; /// Helper trait for code generation for `modifies` contracts. /// @@ -301,7 +304,7 @@ macro_rules! kani_intrinsics { #[doc(hidden)] pub trait Pointer<'a> { /// Type of the pointed-to data - type Inner; + type Inner: ?Sized; /// Used for checking assigns contracts where we pass immutable references to the function. /// @@ -309,56 +312,52 @@ macro_rules! kani_intrinsics { /// argument, for instance one of type `&mut _`, in the `modifies` clause which would move it. unsafe fn decouple_lifetime(&self) -> &'a Self::Inner; - /// used for havocking on replecement of a `modifies` clause. - unsafe fn assignable(self) -> &'a mut Self::Inner; + unsafe fn assignable(self) -> *mut Self::Inner; } - impl<'a, 'b, T> Pointer<'a> for &'b T { + impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b T { type Inner = T; unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - $core::mem::transmute(*self) + core::mem::transmute(*self) } - #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn assignable(self) -> &'a mut Self::Inner { - $core::mem::transmute(self as *const T) + unsafe fn assignable(self) -> *mut Self::Inner { + core::mem::transmute(self as *const T) } } - impl<'a, 'b, T> Pointer<'a> for &'b mut T { + impl<'a, 'b, T: ?Sized> Pointer<'a> for &'b mut T { type Inner = T; #[allow(clippy::transmute_ptr_to_ref)] unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { - $core::mem::transmute::<_, &&'a T>(self) + core::mem::transmute::<_, &&'a T>(self) } - unsafe fn assignable(self) -> &'a mut Self::Inner { - $core::mem::transmute(self) + unsafe fn assignable(self) -> *mut Self::Inner { + self as *mut T } } - impl<'a, T> Pointer<'a> for *const T { + impl<'a, T: ?Sized> Pointer<'a> for *const T { type Inner = T; unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { &**self as &'a T } - #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn assignable(self) -> &'a mut Self::Inner { - $core::mem::transmute(self) + unsafe fn assignable(self) -> *mut Self::Inner { + core::mem::transmute(self) } } - impl<'a, T> Pointer<'a> for *mut T { + impl<'a, T: ?Sized> Pointer<'a> for *mut T { type Inner = T; unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { &**self as &'a T } - #[allow(clippy::transmute_ptr_to_ref)] - unsafe fn assignable(self) -> &'a mut Self::Inner { - $core::mem::transmute(self) + unsafe fn assignable(self) -> *mut Self::Inner { + self } } @@ -384,6 +383,55 @@ macro_rules! kani_intrinsics { #[doc(hidden)] #[rustc_diagnostic_item = "KaniInitContracts"] pub fn init_contracts() {} + + /// This should only be used within contracts. The intent is to + /// perform type inference on a closure's argument + #[doc(hidden)] + pub fn apply_closure bool>(f: U, x: &T) -> bool { + f(x) + } + + /// Recieves a reference to a pointer-like object and assigns kani::any_modifies to that object. + /// Only for use within function contracts and will not be replaced if the recursive or function stub + /// replace contracts are not used. + #[rustc_diagnostic_item = "KaniWriteAny"] + #[inline(never)] + #[doc(hidden)] + pub unsafe fn write_any(_pointer: *mut T) { + // This function should not be reacheable. + // Users must include `#[kani::recursion]` in any function contracts for recursive functions; + // otherwise, this might not be properly instantiate. We mark this as unreachable to make + // sure Kani doesn't report any false positives. + unreachable!() + } + + /// Fill in a slice with kani::any. + /// Intended as a post compilation replacement for write_any + #[rustc_diagnostic_item = "KaniWriteAnySlice"] + #[inline(always)] + pub unsafe fn write_any_slice(slice: *mut [T]) { + (*slice).fill_with(T::any) + } + + /// Fill in a pointer with kani::any. + /// Intended as a post compilation replacement for write_any + #[rustc_diagnostic_item = "KaniWriteAnySlim"] + #[inline(always)] + pub unsafe fn write_any_slim(pointer: *mut T) { + ptr::write(pointer, T::any()) + } + + /// Fill in a str with kani::any. + /// Intended as a post compilation replacement for write_any. + /// Not yet implemented + #[rustc_diagnostic_item = "KaniWriteAnyStr"] + #[inline(always)] + pub unsafe fn write_any_str(_s: *mut str) { + //TODO: strings introduce new UB + //(*s).as_bytes_mut().fill_with(u8::any) + //TODO: String validation + unimplemented!("Kani does not support creating arbitrary `str`") + } } }; } diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index 4e99590fc6a3..a7aaa8ae334e 100644 --- a/library/kani_macros/src/derive.rs +++ b/library/kani_macros/src/derive.rs @@ -28,11 +28,30 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok let (impl_generics, ty_generics, where_clause) = generics.split_for_impl(); let body = fn_any_body(&item_name, &derive_item.data); - let expanded = quote! { - // The generated implementation. - impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause { - fn any() -> Self { - #body + + // Get the safety constraints (if any) to produce type-safe values + let safety_conds_opt = safety_conds(&item_name, &derive_item.data); + + let expanded = if let Some(safety_cond) = safety_conds_opt { + let field_refs = field_refs(&item_name, &derive_item.data); + quote! { + // The generated implementation. + impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause { + fn any() -> Self { + let obj = #body; + #field_refs + kani::assume(#safety_cond); + obj + } + } + } + } else { + quote! { + // The generated implementation. + impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause { + fn any() -> Self { + #body + } } } }; @@ -75,6 +94,103 @@ fn fn_any_body(ident: &Ident, data: &Data) -> TokenStream { } } +/// Parse the condition expressions in `#[safety_constraint()]` attached to struct +/// fields and, it at least one was found, generate a conjunction to be assumed. +/// +/// For example, if we're deriving implementations for the struct +/// ``` +/// #[derive(Arbitrary)] +/// #[derive(Invariant)] +/// struct PositivePoint { +/// #[safety_constraint(*x >= 0)] +/// x: i32, +/// #[safety_constraint(*y >= 0)] +/// y: i32, +/// } +/// ``` +/// this function will generate the `TokenStream` +/// ``` +/// *x >= 0 && *y >= 0 +/// ``` +/// which can be passed to `kani::assume` to constrain the values generated +/// through the `Arbitrary` impl so that they are type-safe by construction. +fn safety_conds(ident: &Ident, data: &Data) -> Option { + match data { + Data::Struct(struct_data) => safety_conds_inner(ident, &struct_data.fields), + Data::Enum(_) => None, + Data::Union(_) => None, + } +} + +/// Generates an expression resulting from the conjunction of conditions +/// specified as safety constraints for each field. See `safety_conds` for more details. +fn safety_conds_inner(ident: &Ident, fields: &Fields) -> Option { + match fields { + Fields::Named(ref fields) => { + let conds: Vec = + fields.named.iter().filter_map(|field| parse_safety_expr(ident, field)).collect(); + if !conds.is_empty() { Some(quote! { #(#conds)&&* }) } else { None } + } + Fields::Unnamed(_) => None, + Fields::Unit => None, + } +} + +/// Generates the sequence of expressions to initialize the variables used as +/// references to the struct fields. +/// +/// For example, if we're deriving implementations for the struct +/// ``` +/// #[derive(Arbitrary)] +/// #[derive(Invariant)] +/// struct PositivePoint { +/// #[safety_constraint(*x >= 0)] +/// x: i32, +/// #[safety_constraint(*y >= 0)] +/// y: i32, +/// } +/// ``` +/// this function will generate the `TokenStream` +/// ``` +/// let x = &obj.x; +/// let y = &obj.y; +/// ``` +/// which allows us to refer to the struct fields without using `self`. +/// Note that the actual stream is generated in the `field_refs_inner` function. +fn field_refs(ident: &Ident, data: &Data) -> TokenStream { + match data { + Data::Struct(struct_data) => field_refs_inner(ident, &struct_data.fields), + Data::Enum(_) => unreachable!(), + Data::Union(_) => unreachable!(), + } +} + +/// Generates the sequence of expressions to initialize the variables used as +/// references to the struct fields. See `field_refs` for more details. +fn field_refs_inner(_ident: &Ident, fields: &Fields) -> TokenStream { + match fields { + Fields::Named(ref fields) => { + let field_refs: Vec = fields + .named + .iter() + .map(|field| { + let name = &field.ident; + quote_spanned! {field.span()=> + let #name = &obj.#name; + } + }) + .collect(); + if !field_refs.is_empty() { + quote! { #( #field_refs )* } + } else { + quote! {} + } + } + Fields::Unnamed(_) => quote! {}, + Fields::Unit => quote! {}, + } +} + /// Generate an item initialization where an item can be a struct or a variant. /// For named fields, this will generate: `Item { field1: kani::any(), field2: kani::any(), .. }` /// For unnamed fields, this will generate: `Item (kani::any(), kani::any(), ..)` @@ -115,6 +231,42 @@ fn init_symbolic_item(ident: &Ident, fields: &Fields) -> TokenStream { } } +/// Extract, parse and return the expression `cond` (i.e., `Some(cond)`) in the +/// `#[safety_constraint()]` attribute helper associated with a given field. +/// Return `None` if the attribute isn't specified. +fn parse_safety_expr(ident: &Ident, field: &syn::Field) -> Option { + let name = &field.ident; + let mut safety_helper_attr = None; + + // Keep the helper attribute if we find it + for attr in &field.attrs { + if attr.path().is_ident("safety_constraint") { + safety_helper_attr = Some(attr); + } + } + + // Parse the arguments in the `#[safety_constraint(...)]` attribute + if let Some(attr) = safety_helper_attr { + let expr_args: Result = attr.parse_args(); + + // Check if there was an error parsing the arguments + if let Err(err) = expr_args { + abort!(Span::call_site(), "Cannot derive impl for `{}`", ident; + note = attr.span() => + "safety constraint in field `{}` could not be parsed: {}", name.as_ref().unwrap().to_string(), err + ) + } + + // Return the expression associated to the safety constraint + let safety_expr = expr_args.unwrap(); + Some(quote_spanned! {field.span()=> + #safety_expr + }) + } else { + None + } +} + /// Generate the body of the function `any()` for enums. The cases are: /// 1. For zero-variants enumerations, this will encode a `panic!()` statement. /// 2. For one or more variants, the code will be something like: @@ -176,10 +328,14 @@ pub fn expand_derive_invariant(item: proc_macro::TokenStream) -> proc_macro::Tok let (impl_generics, ty_generics, where_clause) = generics.split_for_impl(); let body = is_safe_body(&item_name, &derive_item.data); + let field_refs = field_refs(&item_name, &derive_item.data); + let expanded = quote! { // The generated implementation. impl #impl_generics kani::Invariant for #item_name #ty_generics #where_clause { fn is_safe(&self) -> bool { + let obj = self; + #field_refs #body } } @@ -199,7 +355,7 @@ fn add_trait_bound_invariant(mut generics: Generics) -> Generics { fn is_safe_body(ident: &Ident, data: &Data) -> TokenStream { match data { - Data::Struct(struct_data) => struct_safe_conjunction(ident, &struct_data.fields), + Data::Struct(struct_data) => struct_invariant_conjunction(ident, &struct_data.fields), Data::Enum(_) => { abort!(Span::call_site(), "Cannot derive `Invariant` for `{}` enum", ident; note = ident.span() => @@ -215,21 +371,35 @@ fn is_safe_body(ident: &Ident, data: &Data) -> TokenStream { } } -/// Generates an expression that is the conjunction of `is_safe` calls for each field in the struct. -fn struct_safe_conjunction(_ident: &Ident, fields: &Fields) -> TokenStream { +/// Generates an expression that is the conjunction of safety constraints for each field in the struct. +fn struct_invariant_conjunction(ident: &Ident, fields: &Fields) -> TokenStream { match fields { // Expands to the expression + // `true && && && ..` + // where `safety_condN` is + // - `self.fieldN.is_safe() && ` if a condition `` was + // specified through the `#[safety_constraint()]` helper attribute, or + // - `self.fieldN.is_safe()` otherwise + // + // Therefore, if `#[safety_constraint()]` isn't specified for any field, this expands to // `true && self.field1.is_safe() && self.field2.is_safe() && ..` Fields::Named(ref fields) => { - let safe_calls = fields.named.iter().map(|field| { - let name = &field.ident; - quote_spanned! {field.span()=> - self.#name.is_safe() - } - }); + let safety_conds: Vec = fields + .named + .iter() + .map(|field| { + let name = &field.ident; + let default_expr = quote_spanned! {field.span()=> + #name.is_safe() + }; + parse_safety_expr(ident, field) + .map(|expr| quote! { #expr && #default_expr}) + .unwrap_or(default_expr) + }) + .collect(); // An initial value is required for empty structs - safe_calls.fold(quote! { true }, |acc, call| { - quote! { #acc && #call } + safety_conds.iter().fold(quote! { true }, |acc, cond| { + quote! { #acc && #cond } }) } Fields::Unnamed(ref fields) => { diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index b10b8a74cdc5..4e3a8d6f9f5b 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -100,16 +100,120 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::unstable(attr, item) } -/// Allow users to auto generate Arbitrary implementations by using `#[derive(Arbitrary)]` macro. +/// Allow users to auto generate `Arbitrary` implementations by using +/// `#[derive(Arbitrary)]` macro. +/// +/// When using `#[derive(Arbitrary)]` on a struct, the `#[safety_constraint()]` +/// attribute can be added to its fields to indicate a type safety invariant +/// condition ``. Since `kani::any()` is always expected to produce +/// type-safe values, **adding `#[safety_constraint(...)]` to any fields will further +/// constrain the objects generated with `kani::any()`**. +/// +/// For example, the `check_positive` harness in this code is expected to +/// pass: +/// +/// ```rs +/// #[derive(kani::Arbitrary)] +/// struct AlwaysPositive { +/// #[safety_constraint(*inner >= 0)] +/// inner: i32, +/// } +/// +/// #[kani::proof] +/// fn check_positive() { +/// let val: AlwaysPositive = kani::any(); +/// assert!(val.inner >= 0); +/// } +/// ``` +/// +/// Therefore, using the `#[safety_constraint(...)]` attribute can lead to vacuous +/// results when the values are over-constrained. For example, in this code +/// the `check_positive` harness will pass too: +/// +/// ```rs +/// #[derive(kani::Arbitrary)] +/// struct AlwaysPositive { +/// #[safety_constraint(*inner >= 0 && *inner < i32::MIN)] +/// inner: i32, +/// } +/// +/// #[kani::proof] +/// fn check_positive() { +/// let val: AlwaysPositive = kani::any(); +/// assert!(val.inner >= 0); +/// } +/// ``` +/// +/// Unfortunately, we made a mistake when specifying the condition because +/// `*inner >= 0 && *inner < i32::MIN` is equivalent to `false`. This results +/// in the relevant assertion being unreachable: +/// +/// ``` +/// Check 1: check_positive.assertion.1 +/// - Status: UNREACHABLE +/// - Description: "assertion failed: val.inner >= 0" +/// - Location: src/main.rs:22:5 in function check_positive +/// ``` +/// +/// As usual, we recommend users to defend against these behaviors by using +/// `kani::cover!(...)` checks and watching out for unreachable assertions in +/// their project's code. #[proc_macro_error] -#[proc_macro_derive(Arbitrary)] +#[proc_macro_derive(Arbitrary, attributes(safety_constraint))] pub fn derive_arbitrary(item: TokenStream) -> TokenStream { derive::expand_derive_arbitrary(item) } -/// Allow users to auto generate Invariant implementations by using `#[derive(Invariant)]` macro. +/// Allow users to auto generate `Invariant` implementations by using +/// `#[derive(Invariant)]` macro. +/// +/// When using `#[derive(Invariant)]` on a struct, the `#[safety_constraint()]` +/// attribute can be added to its fields to indicate a type safety invariant +/// condition ``. This will ensure that the gets additionally checked when +/// using the `is_safe()` method generated by the `#[derive(Invariant)]` macro. +/// +/// For example, the `check_positive` harness in this code is expected to +/// fail: +/// +/// ```rs +/// #[derive(kani::Invariant)] +/// struct AlwaysPositive { +/// #[safety_constraint(*inner >= 0)] +/// inner: i32, +/// } +/// +/// #[kani::proof] +/// fn check_positive() { +/// let val = AlwaysPositive { inner: -1 }; +/// assert!(val.is_safe()); +/// } +/// ``` +/// +/// This is not too surprising since the type safety invariant that we indicated +/// is not being taken into account when we create the `AlwaysPositive` object. +/// +/// As mentioned, the `is_safe()` methods generated by the +/// `#[derive(Invariant)]` macro check the corresponding `is_safe()` method for +/// each field in addition to any type safety invariants specified through the +/// `#[safety_constraint(...)]` attribute. +/// +/// For example, for the `AlwaysPositive` struct from above, we will generate +/// the following implementation: +/// +/// ```rs +/// impl kani::Invariant for AlwaysPositive { +/// fn is_safe(&self) -> bool { +/// let obj = self; +/// let inner = &obj.inner; +/// true && *inner >= 0 && inner.is_safe() +/// } +/// } +/// ``` +/// +/// Note: the assignments to `obj` and `inner` are made so that we can treat the +/// fields as if they were references. #[proc_macro_error] -#[proc_macro_derive(Invariant)] +#[proc_macro_derive(Invariant, attributes(safety_constraint))] pub fn derive_invariant(item: TokenStream) -> TokenStream { derive::expand_derive_invariant(item) } diff --git a/rust-toolchain.toml b/rust-toolchain.toml index bd69934d573c..27c29bb820e2 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-07-17" +channel = "nightly-2024-07-21" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/scripts/setup/macos/install_deps.sh b/scripts/setup/macos/install_deps.sh index 429eb200541a..179bf8c1237f 100755 --- a/scripts/setup/macos/install_deps.sh +++ b/scripts/setup/macos/install_deps.sh @@ -4,10 +4,10 @@ set -eux -# Github promises weekly build image updates, so we can skip the update step and +# Github promises weekly build image updates, so we could skip the update step and # worst case we should only be 1-2 weeks behind upstream brew. # https://docs.github.com/en/actions/using-github-hosted-runners/about-github-hosted-runners#supported-software -#brew update +brew update # Install Python separately to workround recurring homebrew CI issue. # See https://github.com/actions/runner-images/issues/9471 for more details. diff --git a/scripts/setup/ubuntu/install_cbmc.sh b/scripts/setup/ubuntu/install_cbmc.sh index f37aafcd6327..31015ab9de7a 100755 --- a/scripts/setup/ubuntu/install_cbmc.sh +++ b/scripts/setup/ubuntu/install_cbmc.sh @@ -42,7 +42,8 @@ pushd "${WORK_DIR}" mkdir build git submodule update --init -cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" +cmake -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" \ + -DBUILD_SHARED_LIBS=OFF -DCMAKE_EXE_LINKER_FLAGS=-static make -C build -j$(nproc) cpack -G DEB --config build/CPackConfig.cmake sudo dpkg -i ./cbmc-*.deb diff --git a/src/setup.rs b/src/setup.rs index 730679f06c10..58387f7031b7 100644 --- a/src/setup.rs +++ b/src/setup.rs @@ -189,7 +189,7 @@ fn setup_python_deps(kani_dir: &Path) -> Result<()> { let pyroot = kani_dir.join("pyroot"); // TODO: this is a repetition of versions from kani/kani-dependencies - let pkg_versions = &["cbmc-viewer==3.8"]; + let pkg_versions = &["cbmc-viewer==3.9"]; Command::new("python3") .args(["-m", "pip", "install", "--target"]) diff --git a/tests/expected/derive-arbitrary/safety_constraint_helper/expected b/tests/expected/derive-arbitrary/safety_constraint_helper/expected new file mode 100644 index 000000000000..f35f18084911 --- /dev/null +++ b/tests/expected/derive-arbitrary/safety_constraint_helper/expected @@ -0,0 +1,17 @@ +Check 1: check_invariant_helper_ok.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.x >= 0" + +Check 2: check_invariant_helper_ok.assertion.2\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.y >= 0" + +Check 1: check_invariant_helper_fail.assertion.1\ + - Status: FAILURE\ + - Description: "assertion failed: pos_point.x >= 0" + +Check 2: check_invariant_helper_fail.assertion.2\ + - Status: FAILURE\ + - Description: "assertion failed: pos_point.y >= 0" + +Complete - 2 successfully verified harnesses, 0 failures, 2 total. diff --git a/tests/expected/derive-arbitrary/safety_constraint_helper/safety_constraint_helper.rs b/tests/expected/derive-arbitrary/safety_constraint_helper/safety_constraint_helper.rs new file mode 100644 index 000000000000..5b608aa2a3c0 --- /dev/null +++ b/tests/expected/derive-arbitrary/safety_constraint_helper/safety_constraint_helper.rs @@ -0,0 +1,31 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that the `#[safety_constraint(...)]` attribute helper adds the conditions provided to +//! the attribute to the derived `Arbitrary` implementation. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +struct PositivePoint { + #[safety_constraint(*x >= 0)] + x: i32, + #[safety_constraint(*y >= 0)] + y: i32, +} + +#[kani::proof] +fn check_invariant_helper_ok() { + let pos_point: PositivePoint = kani::any(); + assert!(pos_point.x >= 0); + assert!(pos_point.y >= 0); +} + +#[kani::proof] +#[kani::should_panic] +fn check_invariant_helper_fail() { + let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() }; + assert!(pos_point.x >= 0); + assert!(pos_point.y >= 0); +} diff --git a/tests/expected/derive-invariant/attrs_cfg_guard/attrs_cfg_guard.rs b/tests/expected/derive-invariant/attrs_cfg_guard/attrs_cfg_guard.rs new file mode 100644 index 000000000000..546695bf3731 --- /dev/null +++ b/tests/expected/derive-invariant/attrs_cfg_guard/attrs_cfg_guard.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that the `#[safety_constraint(...)]` attribute helper is picked up +//! when it's used with `cfg_attr(kani, ...)]`. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct PositivePoint { + #[cfg_attr(kani, safety_constraint(*x >= 0))] + x: i32, + #[cfg_attr(kani, safety_constraint(*y >= 0))] + y: i32, +} + +#[kani::proof] +fn check_safety_constraint_cfg() { + let pos_point: PositivePoint = kani::any(); + assert!(pos_point.x >= 0); + assert!(pos_point.y >= 0); +} diff --git a/tests/expected/derive-invariant/attrs_cfg_guard/expected b/tests/expected/derive-invariant/attrs_cfg_guard/expected new file mode 100644 index 000000000000..edb3e256975d --- /dev/null +++ b/tests/expected/derive-invariant/attrs_cfg_guard/expected @@ -0,0 +1,9 @@ +Check 1: check_safety_constraint_cfg.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.x >= 0" + +Check 2: check_safety_constraint_cfg.assertion.2\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.y >= 0" + +Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/expected/derive-invariant/attrs_mixed/attrs_mixed.rs b/tests/expected/derive-invariant/attrs_mixed/attrs_mixed.rs new file mode 100644 index 000000000000..ff58ff846c67 --- /dev/null +++ b/tests/expected/derive-invariant/attrs_mixed/attrs_mixed.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that in the `#[safety_constraint(...)]` attribute helper it is +//! possible to refer to other struct fields, not just the one associated with +//! the attribute. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct PositivePoint { + #[safety_constraint(*x >= 0 && *y >= 0)] + x: i32, + y: i32, +} + +#[kani::proof] +fn check_safety_constraint_cfg() { + let pos_point: PositivePoint = kani::any(); + assert!(pos_point.x >= 0); + assert!(pos_point.y >= 0); +} diff --git a/tests/expected/derive-invariant/attrs_mixed/expected b/tests/expected/derive-invariant/attrs_mixed/expected new file mode 100644 index 000000000000..edb3e256975d --- /dev/null +++ b/tests/expected/derive-invariant/attrs_mixed/expected @@ -0,0 +1,9 @@ +Check 1: check_safety_constraint_cfg.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.x >= 0" + +Check 2: check_safety_constraint_cfg.assertion.2\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.y >= 0" + +Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/expected/derive-invariant/safety_constraint_helper/expected b/tests/expected/derive-invariant/safety_constraint_helper/expected new file mode 100644 index 000000000000..31b6de54c647 --- /dev/null +++ b/tests/expected/derive-invariant/safety_constraint_helper/expected @@ -0,0 +1,13 @@ +Check 1: check_invariant_helper_ok.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.is_safe()" + +Check 1: check_invariant_helper_ok_manual.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.is_safe()" + +Check 1: check_invariant_helper_fail.assertion.1\ + - Status: FAILURE\ + - Description: "assertion failed: pos_point.is_safe()" + +Complete - 3 successfully verified harnesses, 0 failures, 3 total. diff --git a/tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs b/tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs new file mode 100644 index 000000000000..44a218f8fa63 --- /dev/null +++ b/tests/expected/derive-invariant/safety_constraint_helper/safety_constraint_helper.rs @@ -0,0 +1,43 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that the `#[safety_constraint(...)]` attribute helper adds the conditions provided to +//! the attribute to the derived `Invariant` implementation. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct PositivePoint { + #[safety_constraint(*x >= 0)] + x: i32, + #[safety_constraint(*y >= 0)] + y: i32, +} + +#[kani::proof] +fn check_invariant_helper_ok() { + let pos_point: PositivePoint = kani::any(); + assert!(pos_point.is_safe()); +} + +#[kani::proof] +#[kani::should_panic] +fn check_invariant_helper_fail() { + // In this case, we build the struct from unconstrained arbitrary values + // that do not respect `PositivePoint`'s safety constraints. + let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() }; + assert!(pos_point.is_safe()); +} + +#[kani::proof] +fn check_invariant_helper_ok_manual() { + // In this case, we build the struct from unconstrained arbitrary values + // that do not respect `PositivePoint`'s safety constraints. However, we + // manually constrain them later. + let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() }; + kani::assume(pos_point.x >= 0); + kani::assume(pos_point.y >= 0); + assert!(pos_point.is_safe()); +} diff --git a/tests/expected/derive-invariant/safety_constraint_helper_funs/expected b/tests/expected/derive-invariant/safety_constraint_helper_funs/expected new file mode 100644 index 000000000000..31b6de54c647 --- /dev/null +++ b/tests/expected/derive-invariant/safety_constraint_helper_funs/expected @@ -0,0 +1,13 @@ +Check 1: check_invariant_helper_ok.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.is_safe()" + +Check 1: check_invariant_helper_ok_manual.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.is_safe()" + +Check 1: check_invariant_helper_fail.assertion.1\ + - Status: FAILURE\ + - Description: "assertion failed: pos_point.is_safe()" + +Complete - 3 successfully verified harnesses, 0 failures, 3 total. diff --git a/tests/expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs b/tests/expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs new file mode 100644 index 000000000000..a2c4600eb208 --- /dev/null +++ b/tests/expected/derive-invariant/safety_constraint_helper_funs/safety_constraint_helper_funs.rs @@ -0,0 +1,48 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that functions can be called in the `#[safety_constraint(...)]` attribute helpers. +//! This is like the `invariant_helper` test but using a function instead +//! of passing in a predicate. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct PositivePoint { + #[safety_constraint(is_coordinate_safe(x))] + x: i32, + #[safety_constraint(is_coordinate_safe(y))] + y: i32, +} + +fn is_coordinate_safe(val: &i32) -> bool { + *val >= 0 +} + +#[kani::proof] +fn check_invariant_helper_ok() { + let pos_point: PositivePoint = kani::any(); + assert!(pos_point.is_safe()); +} + +#[kani::proof] +#[kani::should_panic] +fn check_invariant_helper_fail() { + // In this case, we build the struct from unconstrained arbitrary values + // that do not respect `PositivePoint`'s safety constraints. + let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() }; + assert!(pos_point.is_safe()); +} + +#[kani::proof] +fn check_invariant_helper_ok_manual() { + // In this case, we build the struct from unconstrained arbitrary values + // that do not respect `PositivePoint`'s safety constraints. However, we + // manually constrain them later. + let pos_point: PositivePoint = PositivePoint { x: kani::any(), y: kani::any() }; + kani::assume(pos_point.x >= 0); + kani::assume(pos_point.y >= 0); + assert!(pos_point.is_safe()); +} diff --git a/tests/expected/derive-invariant/invariant_fail/expected b/tests/expected/derive-invariant/safety_invariant_fail/expected similarity index 100% rename from tests/expected/derive-invariant/invariant_fail/expected rename to tests/expected/derive-invariant/safety_invariant_fail/expected diff --git a/tests/expected/derive-invariant/invariant_fail/invariant_fail.rs b/tests/expected/derive-invariant/safety_invariant_fail/safety_invariant_fail.rs similarity index 100% rename from tests/expected/derive-invariant/invariant_fail/invariant_fail.rs rename to tests/expected/derive-invariant/safety_invariant_fail/safety_invariant_fail.rs diff --git a/tests/expected/derive-invariant/safety_invariant_fail_mut/expected b/tests/expected/derive-invariant/safety_invariant_fail_mut/expected new file mode 100644 index 000000000000..0853a68fa79e --- /dev/null +++ b/tests/expected/derive-invariant/safety_invariant_fail_mut/expected @@ -0,0 +1,11 @@ +Check 1: check_invariant_fail_mut.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: pos_point.is_safe()" + +Check 2: check_invariant_fail_mut.assertion.2\ + - Status: FAILURE\ + - Description: "assertion failed: pos_point.is_safe()" + +VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected) + +Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/expected/derive-invariant/safety_invariant_fail_mut/safety_invariant_fail_mut.rs b/tests/expected/derive-invariant/safety_invariant_fail_mut/safety_invariant_fail_mut.rs new file mode 100644 index 000000000000..dc659ec66dd6 --- /dev/null +++ b/tests/expected/derive-invariant/safety_invariant_fail_mut/safety_invariant_fail_mut.rs @@ -0,0 +1,28 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that a verification failure is triggered if we check the invariant +//! after mutating an object to violate it. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct PositivePoint { + #[safety_constraint(*x >= 0)] + x: i32, + #[safety_constraint(*y >= 0)] + y: i32, +} + +#[kani::proof] +#[kani::should_panic] +fn check_invariant_fail_mut() { + let mut pos_point: PositivePoint = kani::any(); + assert!(pos_point.is_safe()); + // Set the `x` field to an unsafe value + pos_point.x = -1; + // The object's invariant isn't preserved anymore so the next check fails + assert!(pos_point.is_safe()); +} diff --git a/tests/expected/uninit/access-static-padding.expected b/tests/expected/uninit/access-static-padding.expected new file mode 100644 index 000000000000..5577aa3684c5 --- /dev/null +++ b/tests/expected/uninit/access-static-padding.expected @@ -0,0 +1,12 @@ +Checking harness check_read_assoc_const_padding_fails... +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const [u8; 32]` + +Checking harness check_read_static_padding_fails... +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const [u8; 8]` + +Checking harness check_read_const_padding_fails... +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const [u8; 4]` + +Verification failed for - check_read_assoc_const_padding_fails +Verification failed for - check_read_static_padding_fails +Verification failed for - check_read_const_padding_fails diff --git a/tests/expected/uninit/access-static-padding.rs b/tests/expected/uninit/access-static-padding.rs new file mode 100644 index 000000000000..5e9edb5ff9fc --- /dev/null +++ b/tests/expected/uninit/access-static-padding.rs @@ -0,0 +1,34 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks +//! Add a check to ensure that we correctly detect reading the padding values of a static and +//! also of a constant. + +#![feature(generic_const_exprs)] + +/// Check if all the values in the buffer is equals to zero. +unsafe fn is_zeroed(orig: *const T) -> bool +where + [(); size_of::()]:, +{ + let buf = orig as *const [u8; size_of::()]; + unsafe { &*buf }.iter().all(|val| *val == 0) +} + +const CONST_PADDING: (u8, u16) = (0, 0); +static STATIC_PADDING: (u8, char) = (0, '\0'); + +#[kani::proof] +fn check_read_const_padding_fails() { + assert!(unsafe { is_zeroed(&CONST_PADDING) }); +} + +#[kani::proof] +fn check_read_static_padding_fails() { + assert!(unsafe { is_zeroed(&STATIC_PADDING) }); +} + +#[kani::proof] +fn check_read_assoc_const_padding_fails() { + assert!(unsafe { is_zeroed(&(0u128, 0u16)) }); +} diff --git a/tests/kani/Closure/boxed_closure.rs b/tests/kani/Closure/boxed_closure.rs new file mode 100644 index 000000000000..4071978d28b1 --- /dev/null +++ b/tests/kani/Closure/boxed_closure.rs @@ -0,0 +1,22 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// compile-flags: -Zmir-opt-level=2 + +// The main function of this test moves an integer into a closure, +// boxes the value, then passes the closure to a function that calls it. +// This test covers the issue +// https://github.com/model-checking/kani/issues/2874 . + +fn call_boxed_closure(f: Box ()>) -> () { + f() +} + +// #[kani::proof] +fn main() { + let x = 1; + let closure = move || { + let _ = x; + () + }; + call_boxed_closure(Box::new(closure)); +} diff --git a/tests/kani/CodegenStatic/main.rs b/tests/kani/CodegenStatic/main.rs index 9731ca4fe080..7d2791268c7d 100644 --- a/tests/kani/CodegenStatic/main.rs +++ b/tests/kani/CodegenStatic/main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT static STATIC: [&str; 1] = ["FOO"]; #[kani::proof] -fn main() { +fn check_static() { let x = STATIC[0]; let bytes = x.as_bytes(); assert!(bytes.len() == 3); diff --git a/tests/kani/CodegenStatic/struct.rs b/tests/kani/CodegenStatic/struct.rs index 441e118175b1..1801de3c7613 100644 --- a/tests/kani/CodegenStatic/struct.rs +++ b/tests/kani/CodegenStatic/struct.rs @@ -8,6 +8,24 @@ pub struct Foo { const x: Foo<3> = Foo { bytes: [1, 2, 3] }; #[kani::proof] -fn main() { +fn simple_struct() { assert!(x.bytes[0] == 1); } + +pub struct Outer { + data: char, + inner: Inner, +} + +pub struct Inner { + a: char, + b: char, + c: char, +} + +static OUTER: Outer = Outer { data: 'a', inner: Inner { a: 'a', b: 'b', c: 'c' } }; + +#[kani::proof] +fn nested_struct() { + assert!(OUTER.inner.c == 'c'); +} diff --git a/tests/kani/FloatingPoint/main.rs b/tests/kani/FloatingPoint/main.rs index f8ebccdac02a..93a29f169f27 100644 --- a/tests/kani/FloatingPoint/main.rs +++ b/tests/kani/FloatingPoint/main.rs @@ -26,6 +26,7 @@ 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/FunctionContracts/fixme_static_interior_mut.rs b/tests/kani/FunctionContracts/fixme_static_interior_mut.rs new file mode 100644 index 000000000000..1b18472b5590 --- /dev/null +++ b/tests/kani/FunctionContracts/fixme_static_interior_mut.rs @@ -0,0 +1,35 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +//! This file is a duplicate of `static_interior_mut.rs` that captures the current over-approx +//! we perform for static variables with `UnsafeCell`. +//! When you fix this, please delete this file and enable the `regular_field` harness in the +//! original file. + +extern crate kani; + +use std::cell::UnsafeCell; + +pub struct WithMut { + regular_field: u8, + mut_field: UnsafeCell, +} + +/// Just for test purpose. +unsafe impl Sync for WithMut {} + +/// A static definition of `WithMut` +static ZERO_VAL: WithMut = WithMut { regular_field: 0, mut_field: UnsafeCell::new(0) }; + +/// The regular field should be 0. +#[kani::ensures(|result| *result == 0)] +pub fn regular_field() -> u8 { + ZERO_VAL.regular_field +} + +/// This harness is a copy from `static_interior_mut.rs`. +/// Once this gets fixed, please delete this file and enable the original one. +#[kani::proof_for_contract(regular_field)] +fn check_regular_field_is_const() { + assert_eq!(regular_field(), 0); // ** This should succeed since this field is constant. +} diff --git a/tests/kani/FunctionContracts/fixme_static_mut.rs b/tests/kani/FunctionContracts/fixme_static_mut.rs new file mode 100644 index 000000000000..0ee88a3e5ad5 --- /dev/null +++ b/tests/kani/FunctionContracts/fixme_static_mut.rs @@ -0,0 +1,46 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +//! This test checks that contracts correctly handles mutable static. + +static mut WRAP_COUNTER: Option = None; + +/// This function is safe and should never crash. Counter starts at 0. +#[kani::modifies(std::ptr::addr_of!(WRAP_COUNTER))] +#[kani::ensures(|_| true)] +pub fn next() -> u32 { + // Safe in single-threaded. + unsafe { + match &WRAP_COUNTER { + Some(val) => { + WRAP_COUNTER = Some(val.wrapping_add(1)); + *val + } + None => { + WRAP_COUNTER = Some(0); + 0 + } + } + } +} + +/// This harness should succeed. +/// +/// Today, CBMC havocs WRAP_COUNTER, which includes invalid discriminants triggering UB. +#[kani::proof_for_contract(next)] +fn check_next() { + let _ret = next(); +} + +/// Without contracts, we can safely verify `next`. +#[kani::proof] +fn check_next_directly() { + // First check that initial iteration returns 0 (base case). + let first = next(); + assert_eq!(first, 0); + + // Havoc WRAP_COUNTER and invoke next. + unsafe { WRAP_COUNTER = kani::any() }; + let ret = next(); + kani::cover!(ret == 0); +} diff --git a/tests/kani/FunctionContracts/promoted_constants.rs b/tests/kani/FunctionContracts/promoted_constants.rs new file mode 100644 index 000000000000..75202f1bfedd --- /dev/null +++ b/tests/kani/FunctionContracts/promoted_constants.rs @@ -0,0 +1,54 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +//! This test checks that contracts does not havoc +//! [promoted constants](https://github.com/rust-lang/const-eval/blob/master/promotion.md). +//! Related issue: + +extern crate kani; + +#[derive(PartialEq, Eq, kani::Arbitrary)] +pub struct Foo(u8); + +/// A named constant static should work the same way as a promoted constant. +static FOO: Foo = Foo(1); + +/// A mutable static that should be havocked before contract validation. +static mut FOO_MUT: Foo = Foo(1); + +/// Add a contract using a temporary variable that is lifted to a const static. +#[kani::requires(foo == Foo(1))] +pub fn foo_promoted(foo: Foo) -> Foo { + assert!(foo.0 == 1); + foo +} + +/// Add a contract using a const static. +#[kani::requires(foo == FOO)] +pub fn foo_static(foo: Foo) -> Foo { + assert!(foo.0 == 1); + foo +} + +/// Add a contract using a mutable static. +#[kani::requires(&foo == unsafe { &FOO_MUT })] +pub fn foo_mut_static(foo: Foo) -> Foo { + assert!(foo.0 == 1); + foo +} + +#[kani::proof_for_contract(foo_promoted)] +fn check_promoted() { + foo_promoted(kani::any()); +} + +#[kani::proof_for_contract(foo_static)] +fn check_static() { + foo_static(kani::any()); +} + +#[kani::proof_for_contract(foo_mut_static)] +#[kani::should_panic] +fn check_mut_static() { + foo_mut_static(kani::any()); +} diff --git a/tests/kani/FunctionContracts/promoted_constants_enum.rs b/tests/kani/FunctionContracts/promoted_constants_enum.rs new file mode 100644 index 000000000000..12878eee8044 --- /dev/null +++ b/tests/kani/FunctionContracts/promoted_constants_enum.rs @@ -0,0 +1,32 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +//! This test checks that contracts does not havoc +//! [promoted constants](https://github.com/rust-lang/const-eval/blob/master/promotion.md) +//! that represents an enum variant. +//! +//! Related issue: + +extern crate kani; +#[derive(PartialEq, Eq, kani::Arbitrary)] +pub enum Foo { + A, + B, +} + +#[kani::ensures(|result: &Foo| *result == Foo::A)] +pub fn foo_a() -> Foo { + Foo::A +} + +#[kani::proof_for_contract(foo_a)] +fn check() { + let _ = foo_a(); +} + +#[kani::proof] +#[kani::stub_verified(foo_a)] +fn check_stub() { + let val = foo_a(); + assert!(val == Foo::A) +} diff --git a/tests/kani/FunctionContracts/static_interior_mut.rs b/tests/kani/FunctionContracts/static_interior_mut.rs new file mode 100644 index 000000000000..deb20e739fb3 --- /dev/null +++ b/tests/kani/FunctionContracts/static_interior_mut.rs @@ -0,0 +1,47 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts +//! This test checks that contracts havoc static variables with interior mutability. +//! For now, we over-approximate and havoc the entire static. + +extern crate kani; + +use std::cell::UnsafeCell; + +pub struct WithMut { + regular_field: u8, + mut_field: UnsafeCell, +} + +/// Just for test purpose. +unsafe impl Sync for WithMut {} + +/// A static definition of `WithMut` +static ZERO_VAL: WithMut = WithMut { regular_field: 0, mut_field: UnsafeCell::new(0) }; + +/// The regular field should be 0. +#[kani::ensures(|result| *result == 0)] +pub fn regular_field() -> u8 { + ZERO_VAL.regular_field +} + +/// The mutable field can be anything. +#[kani::ensures(|result| *result == old(unsafe { *ZERO_VAL.mut_field.get() }))] +pub unsafe fn mut_field() -> u8 { + unsafe { *ZERO_VAL.mut_field.get() } +} + +/// This harness is duplicated in `fixme_static_interior_mut.rs`. +/// Issue <> +#[cfg(fixme)] +#[kani::proof_for_contract(regular_field)] +fn check_regular_field_is_const() { + assert_eq!(regular_field(), 0); // ** This should succeed since this field is constant. +} + +// Ensure that Kani havoc the mutable field. +#[kani::should_panic] +#[kani::proof_for_contract(mut_field)] +fn check_regular_field_is_const() { + assert_eq!(unsafe { mut_field() }, 0); // ** This must fail since Kani havoc the mutable field. +} diff --git a/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs b/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs index 09c630aa94a7..642d984a7e2b 100644 --- a/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/Ceil/ceilf64.rs @@ -45,6 +45,7 @@ fn test_conc_sci() { } #[kani::proof] +#[kani::solver(minisat)] fn test_towards_inf() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); @@ -53,6 +54,7 @@ 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 0560a2c55064..54ad74c33430 100644 --- a/tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/Floor/floorf64.rs @@ -45,6 +45,7 @@ fn test_conc_sci() { } #[kani::proof] +#[kani::solver(minisat)] fn test_towards_neg_inf() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); @@ -53,6 +54,7 @@ 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 25e02f45a943..7ffdb5f28747 100644 --- a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs +++ b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf32.rs @@ -50,6 +50,7 @@ fn test_conc_sci() { } #[kani::proof] +#[kani::solver(minisat)] fn test_towards_nearest() { let x: f32 = kani::any(); kani::assume(!x.is_nan()); @@ -88,6 +89,7 @@ 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 589a44a4d1ac..bf656512562e 100644 --- a/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/NearbyInt/nearbyintf64.rs @@ -50,6 +50,7 @@ fn test_conc_sci() { } #[kani::proof] +#[kani::solver(minisat)] fn test_towards_nearest() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); @@ -88,6 +89,7 @@ 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 79a0a4f9be2c..53d9d7d5fc73 100644 --- a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs +++ b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf32.rs @@ -55,6 +55,7 @@ fn test_conc_sci() { } #[kani::proof] +#[kani::solver(minisat)] fn test_towards_nearest() { let x: f32 = kani::any(); kani::assume(!x.is_nan()); @@ -93,6 +94,7 @@ 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 8c8ea583a2d5..de608e7cdb9f 100644 --- a/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/RInt/rintf64.rs @@ -55,6 +55,7 @@ fn test_conc_sci() { } #[kani::proof] +#[kani::solver(minisat)] fn test_towards_nearest() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); @@ -93,6 +94,7 @@ 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 8a8780878925..04893727dcfa 100644 --- a/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs +++ b/tests/kani/Intrinsics/Math/Rounding/Round/roundf32.rs @@ -39,6 +39,7 @@ fn test_conc_sci() { } #[kani::proof] +#[kani::solver(minisat)] fn test_towards_closer() { let x: f32 = kani::any(); kani::assume(!x.is_nan()); @@ -61,6 +62,7 @@ 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 ddafc45a2e9e..cd61e9607646 100644 --- a/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/Round/roundf64.rs @@ -39,6 +39,7 @@ fn test_conc_sci() { } #[kani::proof] +#[kani::solver(minisat)] fn test_towards_closer() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); @@ -61,6 +62,7 @@ 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 5fcc8c80606d..a8a80672e36b 100644 --- a/tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs +++ b/tests/kani/Intrinsics/Math/Rounding/Trunc/truncf64.rs @@ -38,6 +38,7 @@ fn test_conc_sci() { } #[kani::proof] +#[kani::solver(minisat)] fn test_towards_zero() { let x: f64 = kani::any(); kani::assume(!x.is_nan()); @@ -50,6 +51,7 @@ 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/perf/s2n-quic b/tests/perf/s2n-quic index 71f8d9f5aafb..75afd77dfa88 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit 71f8d9f5aafbf59f31ad85eeb7b4b67a7564a685 +Subproject commit 75afd77dfa88d696900f12ee747409ddb208a745 diff --git a/tests/script-based-pre/mem-init-reinstrumentation/alloc-zeroed.rs b/tests/script-based-pre/mem-init-reinstrumentation/alloc-zeroed.rs new file mode 100644 index 000000000000..891a97fd8c22 --- /dev/null +++ b/tests/script-based-pre/mem-init-reinstrumentation/alloc-zeroed.rs @@ -0,0 +1,22 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +use std::alloc::{alloc_zeroed, Layout}; +use std::slice::from_raw_parts; + +#[kani::proof] +fn alloc_zeroed_to_slice() { + let layout = Layout::from_size_align(32, 8).unwrap(); + unsafe { + // This returns initialized memory, so any further accesses are valid. + let ptr = alloc_zeroed(layout); + *ptr = 0x41; + *ptr.add(1) = 0x42; + *ptr.add(2) = 0x43; + *ptr.add(3) = 0x44; + *ptr.add(16) = 0x00; + let _slice1 = from_raw_parts(ptr, 16); + let _slice2 = from_raw_parts(ptr.add(16), 16); + } +} diff --git a/tests/script-based-pre/mem-init-reinstrumentation/config.yml b/tests/script-based-pre/mem-init-reinstrumentation/config.yml new file mode 100644 index 000000000000..ef61a9171954 --- /dev/null +++ b/tests/script-based-pre/mem-init-reinstrumentation/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: mem-init-reinstrumentation.sh +expected: mem-init-reinstrumentation.expected diff --git a/tests/script-based-pre/mem-init-reinstrumentation/mem-init-reinstrumentation.expected b/tests/script-based-pre/mem-init-reinstrumentation/mem-init-reinstrumentation.expected new file mode 100644 index 000000000000..59b64322ad50 --- /dev/null +++ b/tests/script-based-pre/mem-init-reinstrumentation/mem-init-reinstrumentation.expected @@ -0,0 +1 @@ +success: no pointer checks are detected in initialized memory instrumentaiton diff --git a/tests/script-based-pre/mem-init-reinstrumentation/mem-init-reinstrumentation.sh b/tests/script-based-pre/mem-init-reinstrumentation/mem-init-reinstrumentation.sh new file mode 100755 index 000000000000..f859864d1c9a --- /dev/null +++ b/tests/script-based-pre/mem-init-reinstrumentation/mem-init-reinstrumentation.sh @@ -0,0 +1,20 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set -u + +KANI_OUTPUT=`kani -Z uninit-checks alloc-zeroed.rs` +echo "$KANI_OUTPUT" | egrep -q "kani::mem_init::.*pointer_dereference" +INSTRUMENTATION_DETECTED=$? + +if [[ $INSTRUMENTATION_DETECTED == 0 ]]; then + echo "failed: pointer checks are detected in initialized memory instrumentaiton" + exit 1 +elif [[ $INSTRUMENTATION_DETECTED == 1 ]]; then + echo "success: no pointer checks are detected in initialized memory instrumentaiton" + exit 0 +else + echo "failed: error occured when runnning egrep" + exit 0 +fi diff --git a/tests/script-based-pre/verify_std_cmd/verify_core.rs b/tests/script-based-pre/verify_std_cmd/verify_core.rs new file mode 100644 index 000000000000..28cf113a9210 --- /dev/null +++ b/tests/script-based-pre/verify_std_cmd/verify_core.rs @@ -0,0 +1,75 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +/// Dummy code that gets injected into `core` for basic tests for `verify-std` subcommand. +#[cfg(kani)] +kani_core::kani_lib!(core); + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +pub mod verify { + use crate::kani; + use core::num::NonZeroU8; + + #[kani::proof] + pub fn harness() { + kani::assert(true, "yay"); + } + + #[kani::proof_for_contract(fake_function)] + fn dummy_proof() { + fake_function(true); + } + + /// Add a `rustc_diagnostic_item` to ensure this works. + /// See for more details. + #[kani::requires(x == true)] + #[rustc_diagnostic_item = "fake_function"] + fn fake_function(x: bool) -> bool { + x + } + + #[kani::proof_for_contract(dummy_read)] + fn check_dummy_read() { + let val: char = kani::any(); + assert_eq!(unsafe { dummy_read(&val) }, val); + } + + /// Ensure we can verify constant functions. + #[kani::requires(kani::mem::can_dereference(ptr))] + #[rustc_diagnostic_item = "dummy_read"] + const unsafe fn dummy_read(ptr: *const T) -> T { + *ptr + } + + #[kani::proof_for_contract(swap_tuple)] + fn check_swap_tuple() { + let initial: (char, NonZeroU8) = kani::any(); + let _swapped = swap_tuple(initial); + } + + #[kani::ensures(| result | result.0 == second && result.1 == first)] + fn swap_tuple((first, second): (char, NonZeroU8)) -> (NonZeroU8, char) { + (second, first) + } + + #[kani::proof_for_contract(add_one)] + fn check_add_one() { + let mut initial: [u32; 4] = kani::any(); + unsafe { add_one(&mut initial) }; + } + + /// Function with a more elaborated contract that uses `old` and `modifies`. + #[kani::modifies(inout)] + #[kani::requires(kani::mem::can_dereference(inout) + && unsafe { inout.as_ref_unchecked().iter().all(| i | * i < u32::MAX) })] + #[kani::requires(kani::mem::can_write(inout))] + #[kani::ensures(| result | { + let (orig, i) = old({ + let i = kani::any_where(| i: & usize | * i < unsafe { inout.len() }); + (unsafe { inout.as_ref_unchecked()[i] }, i)}); + unsafe { inout.as_ref_unchecked()[i] > orig } + })] + unsafe fn add_one(inout: *mut [u32]) { + inout.as_mut_unchecked().iter_mut().for_each(|e| *e += 1) + } +} diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.expected b/tests/script-based-pre/verify_std_cmd/verify_std.expected index aa30da375dd3..22e8fb2e6375 100644 --- a/tests/script-based-pre/verify_std_cmd/verify_std.expected +++ b/tests/script-based-pre/verify_std_cmd/verify_std.expected @@ -9,7 +9,13 @@ VERIFICATION:- SUCCESSFUL Checking harness verify::check_dummy_read... VERIFICATION:- SUCCESSFUL +Checking harness verify::check_add_one... +VERIFICATION:- SUCCESSFUL + +Checking harness verify::check_swap_tuple... +VERIFICATION:- SUCCESSFUL + Checking harness num::verify::check_non_zero... VERIFICATION:- SUCCESSFUL -Complete - 4 successfully verified harnesses, 0 failures, 4 total. +Complete - 6 successfully verified harnesses, 0 failures, 6 total. diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.sh b/tests/script-based-pre/verify_std_cmd/verify_std.sh index 3253ad29756e..91454c4b65e7 100755 --- a/tests/script-based-pre/verify_std_cmd/verify_std.sh +++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh @@ -21,47 +21,7 @@ STD_PATH="${SYSROOT}/lib/rustlib/src/rust/library" cp -r "${STD_PATH}" "${TMP_DIR}" # Insert a small harness in one of the standard library modules. -CORE_CODE=' -#[cfg(kani)] -kani_core::kani_lib!(core); - -#[cfg(kani)] -#[unstable(feature = "kani", issue = "none")] -pub mod verify { - use crate::kani; - - #[kani::proof] - pub fn harness() { - kani::assert(true, "yay"); - } - - #[kani::proof_for_contract(fake_function)] - fn dummy_proof() { - fake_function(true); - } - - /// Add a `rustc_diagnostic_item` to ensure this works. - /// See for more details. - #[kani::requires(x == true)] - #[rustc_diagnostic_item = "fake_function"] - fn fake_function(x: bool) -> bool { - x - } - - #[kani::proof_for_contract(dummy_read)] - fn check_dummy_read() { - let val: char = kani::any(); - assert_eq!(unsafe { dummy_read(&val) }, val); - } - - /// Ensure we can verify constant functions. - #[kani::requires(kani::mem::can_dereference(ptr))] - #[rustc_diagnostic_item = "dummy_read"] - const unsafe fn dummy_read(ptr: *const T) -> T { - *ptr - } -} -' +CORE_CODE=$(cat verify_core.rs) STD_CODE=' #[cfg(kani)] diff --git a/tests/ui/derive-invariant/helper-empty/expected b/tests/ui/derive-invariant/helper-empty/expected new file mode 100644 index 000000000000..d8590a9d22b8 --- /dev/null +++ b/tests/ui/derive-invariant/helper-empty/expected @@ -0,0 +1,6 @@ +error: Cannot derive impl for `PositivePoint` + | +| #[derive(kani::Invariant)] + | ^^^^^^^^^^^^^^^ + | +note: safety constraint in field `x` could not be parsed: expected attribute arguments in parentheses: #[safety_constraint(...)] diff --git a/tests/ui/derive-invariant/helper-empty/helper-empty.rs b/tests/ui/derive-invariant/helper-empty/helper-empty.rs new file mode 100644 index 000000000000..3086603cf5db --- /dev/null +++ b/tests/ui/derive-invariant/helper-empty/helper-empty.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check the compilation error for the `#[safety_constraint(...)]` attribute helper when an +//! argument isn't provided. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct PositivePoint { + #[safety_constraint] + x: i32, + #[safety_constraint(*y >= 0)] + y: i32, +} diff --git a/tests/ui/derive-invariant/helper-no-expr/expected b/tests/ui/derive-invariant/helper-no-expr/expected new file mode 100644 index 000000000000..e9ac7e3e1124 --- /dev/null +++ b/tests/ui/derive-invariant/helper-no-expr/expected @@ -0,0 +1,6 @@ +error: Cannot derive impl for `PositivePoint` + | +| #[derive(kani::Invariant)] + | ^^^^^^^^^^^^^^^ + | +note: safety constraint in field `x` could not be parsed: unexpected end of input, expected an expression diff --git a/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs b/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs new file mode 100644 index 000000000000..080c94371257 --- /dev/null +++ b/tests/ui/derive-invariant/helper-no-expr/helper-no-expr.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check the compilation error for the `#[safety_constraint(...)]` attribute helper when the +//! argument is not a proper expression. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct PositivePoint { + #[safety_constraint()] + x: i32, + #[safety_constraint(*y >= 0)] + y: i32, +} diff --git a/tests/ui/derive-invariant/helper-side-effect/expected b/tests/ui/derive-invariant/helper-side-effect/expected new file mode 100644 index 000000000000..20b3d17efd38 --- /dev/null +++ b/tests/ui/derive-invariant/helper-side-effect/expected @@ -0,0 +1,9 @@ +error[E0596]: cannot borrow `*x` as mutable, as it is behind a `&` reference + | +| #[safety_constraint({*(x.as_mut()) = 0; true})] + | ^ `x` is a `&` reference, so the data it refers to cannot be borrowed as mutable + | +help: consider specifying this binding's type + | +| x: &mut std::boxed::Box: Box, + | +++++++++++++++++++++++++++ diff --git a/tests/ui/derive-invariant/helper-side-effect/helper-side-effect.rs b/tests/ui/derive-invariant/helper-side-effect/helper-side-effect.rs new file mode 100644 index 000000000000..e80f2ff25796 --- /dev/null +++ b/tests/ui/derive-invariant/helper-side-effect/helper-side-effect.rs @@ -0,0 +1,22 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that side effect expressions in the `#[safety_constraint(...)]` +//! attribute helpers are not allowed. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct PositivePoint { + #[safety_constraint({*(x.as_mut()) = 0; true})] + x: Box, + y: i32, +} + +#[kani::proof] +fn check_invariant_helper_ok() { + let pos_point: PositivePoint = kani::any(); + assert!(pos_point.is_safe()); +} diff --git a/tests/ui/derive-invariant/helper-wrong-expr/expected b/tests/ui/derive-invariant/helper-wrong-expr/expected new file mode 100644 index 000000000000..3f661bce9cbb --- /dev/null +++ b/tests/ui/derive-invariant/helper-wrong-expr/expected @@ -0,0 +1,9 @@ +error[E0308]: mismatched types + | +| #[safety_constraint(x >= 0)] + | ^ expected `&i32`, found integer + | +help: consider dereferencing the borrow + | +| #[safety_constraint(*x >= 0)] + | diff --git a/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs b/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs new file mode 100644 index 000000000000..66b42e02fd68 --- /dev/null +++ b/tests/ui/derive-invariant/helper-wrong-expr/helper-wrong-expr.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check the compilation error for the `#[safety_constraint(...)]` attribute helper when the +//! argument cannot be evaluated in the struct's context. + +extern crate kani; +use kani::Invariant; + +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +struct PositivePoint { + // Note: `x` is a reference in this context, we should refer to `*x` + #[safety_constraint(x >= 0)] + x: i32, + #[safety_constraint(*y >= 0)] + y: i32, +} diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index 7925ed83e6e5..50f1e3035ac8 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -272,14 +272,14 @@ impl<'test> TestCx<'test> { .arg("kani") .arg("--target-dir") .arg(self.output_base_dir().join("target")) - .current_dir(parent_dir) - .args(&self.config.extra_args); + .current_dir(parent_dir); if test { cargo.arg("--tests"); } if "expected" != self.testpaths.file.file_name().unwrap() { cargo.args(["--harness", function_name]); } + cargo.args(&self.config.extra_args); let proc_res = self.compose_and_run(cargo); self.verify_output(&proc_res, &self.testpaths.file);