From 556cf7189cc5fc6749bb16a88025afaebe29fae5 Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Mon, 11 Mar 2024 11:58:02 -0700 Subject: [PATCH 1/5] cargo update and fix macos CI (#3067) Fix recurring [macos CI issue](https://github.com/actions/runner-images/issues/9471) (see https://github.com/model-checking/kani/actions/runs/8234799856/job/22521976090?pr=3065#step:3:202 for an example of a failing run) and do a `cargo update`. This subsumes https://github.com/model-checking/kani/pull/3065 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- Cargo.lock | 50 ++++++++++++++--------------- scripts/setup/macos/install_deps.sh | 12 +++---- 2 files changed, 30 insertions(+), 32 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 3af5e6232a76..4db35ee6ab77 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -145,7 +145,7 @@ version = "0.47.0" dependencies = [ "anyhow", "cargo_metadata", - "clap 4.5.1", + "clap 4.5.2", "which", ] @@ -204,9 +204,9 @@ dependencies = [ [[package]] name = "clap" -version = "4.5.1" +version = "4.5.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c918d541ef2913577a0f9566e9ce27cb35b6df072075769e0b26cb5a554520da" +checksum = "b230ab84b0ffdf890d5a10abdbc8b83ae1c4918275daea1ab8801f71536b2651" dependencies = [ "clap_builder", "clap_derive", @@ -214,9 +214,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.5.1" +version = "4.5.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9f3e7391dad68afb0c2ede1bf619f579a3dc9c2ec67f089baa397123a2f3d1eb" +checksum = "ae129e2e766ae0ec03484e609954119f123cc1fe650337e155d03b022f24f7b4" dependencies = [ "anstream", "anstyle", @@ -481,7 +481,7 @@ dependencies = [ name = "kani-compiler" version = "0.47.0" dependencies = [ - "clap 4.5.1", + "clap 4.5.2", "cprover_bindings", "home", "itertools", @@ -492,8 +492,8 @@ dependencies = [ "serde", "serde_json", "shell-words", - "strum 0.26.1", - "strum_macros 0.26.1", + "strum 0.26.2", + "strum_macros 0.26.2", "tracing", "tracing-subscriber", ] @@ -504,7 +504,7 @@ version = "0.47.0" dependencies = [ "anyhow", "cargo_metadata", - "clap 4.5.1", + "clap 4.5.2", "comfy-table", "console", "glob", @@ -517,8 +517,8 @@ dependencies = [ "rustc-demangle", "serde", "serde_json", - "strum 0.26.1", - "strum_macros 0.26.1", + "strum 0.26.2", + "strum_macros 0.26.2", "tempfile", "toml", "tracing", @@ -550,11 +550,11 @@ dependencies = [ name = "kani_metadata" version = "0.47.0" dependencies = [ - "clap 4.5.1", + "clap 4.5.2", "cprover_bindings", "serde", - "strum 0.26.1", - "strum_macros 0.26.1", + "strum 0.26.2", + "strum_macros 0.26.2", ] [[package]] @@ -896,7 +896,7 @@ checksum = "b62dbe01f0b06f9d8dc7d49e05a0785f153b00b2c227856282f671e0318c9b15" dependencies = [ "aho-corasick", "memchr", - "regex-automata 0.4.5", + "regex-automata 0.4.6", "regex-syntax 0.8.2", ] @@ -911,9 +911,9 @@ dependencies = [ [[package]] name = "regex-automata" -version = "0.4.5" +version = "0.4.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5bb987efffd3c6d0d8f5f89510bb458559eab11e4f869acb20bf845e016259cd" +checksum = "86b83b8b9847f9bf95ef68afb0b8e6cdb80f498442f5179a29fad448fcc1eaea" dependencies = [ "aho-corasick", "memchr", @@ -1115,9 +1115,9 @@ checksum = "290d54ea6f91c969195bdbcd7442c8c2a2ba87da8bf60a7ee86a235d4bc1e125" [[package]] name = "strum" -version = "0.26.1" +version = "0.26.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "723b93e8addf9aa965ebe2d11da6d7540fa2283fcea14b3371ff055f7ba13f5f" +checksum = "5d8cec3501a5194c432b2b7976db6b7d10ec95c253208b45f83f7136aa985e29" [[package]] name = "strum_macros" @@ -1134,9 +1134,9 @@ dependencies = [ [[package]] name = "strum_macros" -version = "0.26.1" +version = "0.26.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7a3417fc93d76740d974a01654a09777cb500428cc874ca9f45edfe0c4d4cd18" +checksum = "c6cf59daf282c0a494ba14fd21610a0325f9f90ec9d1231dea26bcb1d696c946" dependencies = [ "heck", "proc-macro2", @@ -1219,9 +1219,9 @@ dependencies = [ [[package]] name = "toml" -version = "0.8.10" +version = "0.8.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9a9aad4a3066010876e8dcf5a8a06e70a558751117a145c6ce2b82c2e2054290" +checksum = "af06656561d28735e9c1cd63dfd57132c8155426aa6af24f36a00a351f88c48e" dependencies = [ "serde", "serde_spanned", @@ -1240,9 +1240,9 @@ dependencies = [ [[package]] name = "toml_edit" -version = "0.22.6" +version = "0.22.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2c1b5fd4128cc8d3e0cb74d4ed9a9cc7c7284becd4df68f5f940e1ad123606f6" +checksum = "18769cd1cec395d70860ceb4d932812a0b4d06b1a4bb336745a4d21b9496e992" dependencies = [ "indexmap", "serde", diff --git a/scripts/setup/macos/install_deps.sh b/scripts/setup/macos/install_deps.sh index c544846b403f..429eb200541a 100755 --- a/scripts/setup/macos/install_deps.sh +++ b/scripts/setup/macos/install_deps.sh @@ -9,16 +9,14 @@ set -eux # https://docs.github.com/en/actions/using-github-hosted-runners/about-github-hosted-runners#supported-software #brew update +# Install Python separately to workround recurring homebrew CI issue. +# See https://github.com/actions/runner-images/issues/9471 for more details. +brew install python@3 || true +brew link --overwrite python@3 + # Install dependencies via `brew` brew install universal-ctags wget jq -# Add Python package dependencies -PYTHON_DEPS=( - autopep8 -) - -python3 -m pip install "${PYTHON_DEPS[@]}" - # Get the directory containing this script SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" From a8db1207996b793ce0db975ab9f1b1805fa74d84 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 11 Mar 2024 14:13:58 -0700 Subject: [PATCH 2/5] Bump tests/perf/s2n-quic from `d103836` to `1a7faa8` (#3066) Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `d103836` to `1a7faa8`.
Commits

Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting `@dependabot rebase`. [//]: # (dependabot-automerge-start) [//]: # (dependabot-automerge-end) ---
Dependabot commands and options
You can trigger Dependabot actions by commenting on this PR: - `@dependabot rebase` will rebase this PR - `@dependabot recreate` will recreate this PR, overwriting any edits that have been made to it - `@dependabot merge` will merge this PR after your CI passes on it - `@dependabot squash and merge` will squash and merge this PR after your CI passes on it - `@dependabot cancel merge` will cancel a previously requested merge and block automerging - `@dependabot reopen` will reopen this PR if it is closed - `@dependabot close` will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually - `@dependabot show ignore conditions` will show all of the ignore conditions of the specified dependency - `@dependabot ignore this major version` will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this minor version` will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this dependency` will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)
Signed-off-by: dependabot[bot] Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- tests/perf/s2n-quic | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index d103836ce086..1a7faa87ebcf 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit d103836ce086534e63c75a0b497079ed74e58c18 +Subproject commit 1a7faa87ebcf2b84a068f21af3306a6f42eb8c74 From e7a4d835fa5b0e81356ec96399270fbdcce7af01 Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Tue, 12 Mar 2024 11:06:45 -0700 Subject: [PATCH 3/5] Upgrade toolchain to 2024-03-11 (#3071) Relevant upstream changes: https://github.com/rust-lang/rust/pull/120675: An intrinsic `Symbol` is now wrapped in a `IntrinsicDef` struct, so the relevant part of the code needed to be updated. https://github.com/rust-lang/rust/pull/121464: The second argument of the `create_wrapper_file` function changed from a vector to a string. https://github.com/rust-lang/rust/pull/121662: `NullOp::DebugAssertions` was renamed to `NullOp::UbCheck` and it now has data (currently unused by Kani) https://github.com/rust-lang/rust/pull/121728: Introduces `F16` and `F128`, so needed to add stubs for them https://github.com/rust-lang/rust/pull/121969: `parse_sess` was renamed to `psess`, so updated the relevant code. https://github.com/rust-lang/rust/pull/122059: The `is_val_statically_known` intrinsic is now used in some `core::fmt` code, so had to handle it in (codegen'ed to false). https://github.com/rust-lang/rust/pull/122233: This added a new `retag_box_to_raw` intrinsic. This is an operation that is primarily relevant for stacked borrows. For Kani, we just return the pointer. Resolves #3057 --- .../codegen/intrinsic.rs | 19 +++++++++++++++++++ .../codegen_cprover_gotoc/codegen/rvalue.rs | 2 +- .../src/codegen_cprover_gotoc/codegen/typ.rs | 6 ++++++ .../compiler_interface.rs | 2 +- kani-compiler/src/kani_middle/attributes.rs | 7 +++---- kani-compiler/src/kani_middle/intrinsics.rs | 8 ++++---- kani-compiler/src/kani_middle/reachability.rs | 2 +- kani-driver/src/assess/mod.rs | 2 +- rust-toolchain.toml | 2 +- tests/coverage/unreachable/variant/expected | 2 +- tools/bookrunner/librustdoc/html/markdown.rs | 2 +- 11 files changed, 39 insertions(+), 15 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 20e3f34f48bf..2cabc4cfd273 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -474,6 +474,11 @@ impl<'tcx> GotocCtx<'tcx> { let binop_stmt = codegen_intrinsic_binop!(sub); self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span) } + "is_val_statically_known" => { + // Returning false is sound according do this intrinsic's documentation: + // https://doc.rust-lang.org/nightly/std/intrinsics/fn.is_val_statically_known.html + self.codegen_expr_to_place_stable(place, Expr::c_false()) + } "likely" => self.codegen_expr_to_place_stable(place, fargs.remove(0)), "log10f32" => unstable_codegen!(codegen_simple_intrinsic!(Log10f)), "log10f64" => unstable_codegen!(codegen_simple_intrinsic!(Log10)), @@ -506,6 +511,7 @@ impl<'tcx> GotocCtx<'tcx> { "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, place, loc), "ptr_offset_from_unsigned" => self.codegen_ptr_offset_from_unsigned(fargs, place, loc), "raw_eq" => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc), + "retag_box_to_raw" => self.codegen_retag_box_to_raw(fargs, place, loc), "rintf32" => codegen_simple_intrinsic!(Rintf), "rintf64" => codegen_simple_intrinsic!(Rint), "rotate_left" => codegen_intrinsic_binop!(rol), @@ -1259,6 +1265,19 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_expr_to_place_stable(p, e) } + // This is an operation that is primarily relevant for stacked borrow + // checks. For Kani, we simply return the pointer. + fn codegen_retag_box_to_raw( + &mut self, + mut fargs: Vec, + p: &Place, + _loc: Location, + ) -> Stmt { + assert_eq!(fargs.len(), 1, "raw_box_to_box expected one argument"); + let arg = fargs.remove(0); + self.codegen_expr_to_place_stable(p, arg) + } + fn vtable_info( &mut self, info: VTableInfo, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 3df6d807aaea..5867448d9973 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -725,7 +725,7 @@ impl<'tcx> GotocCtx<'tcx> { .bytes(), Type::size_t(), ), - NullOp::DebugAssertions => Expr::c_false(), + NullOp::UbCheck(_) => Expr::c_false(), } } Rvalue::ShallowInitBox(ref operand, content_ty) => { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 57af958abf41..089d871d22b4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -542,6 +542,9 @@ impl<'tcx> GotocCtx<'tcx> { ty::Float(k) => match k { FloatTy::F32 => Type::float(), FloatTy::F64 => Type::double(), + // `F16` and `F128` are not yet handled. + // Tracked here: + FloatTy::F16 | FloatTy::F128 => unimplemented!(), }, ty::Adt(def, _) if def.repr().simd() => self.codegen_vector(ty), ty::Adt(def, subst) => { @@ -1346,6 +1349,9 @@ impl<'tcx> GotocCtx<'tcx> { Primitive::F32 => self.tcx.types.f32, Primitive::F64 => self.tcx.types.f64, + // `F16` and `F128` are not yet handled. + // Tracked here: + Primitive::F16 | Primitive::F128 => unimplemented!(), Primitive::Pointer(_) => Ty::new_ptr( self.tcx, ty::TypeAndMut { ty: self.tcx.types.u8, mutbl: Mutability::Not }, diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 91e6c2538195..cad8bcbfb9ce 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -397,7 +397,7 @@ impl CodegenBackend for GotocCodegenBackend { let path = MaybeTempDir::new(tmp_dir, sess.opts.cg.save_temps); let (metadata, _metadata_position) = create_wrapper_file( sess, - b".rmeta".to_vec(), + ".rmeta".to_string(), codegen_results.metadata.raw_data(), ); let metadata = emit_wrapper_file(sess, &metadata, &path, METADATA_FILENAME); diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 621107acd13e..df494d7daa3c 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -611,9 +611,8 @@ fn parse_modify_values<'a>( let mut iter = t.trees(); std::iter::from_fn(move || { let tree = iter.next()?; - let wrong_token_err = || { - tcx.sess.parse_sess.dcx.span_err(tree.span(), "Unexpected token. Expected identifier.") - }; + let wrong_token_err = + || tcx.sess.psess.dcx.span_err(tree.span(), "Unexpected token. Expected identifier."); let result = match tree { TokenTree::Token(token, _) => { if let TokenKind::Ident(id, _) = &token.kind { @@ -640,7 +639,7 @@ fn parse_modify_values<'a>( match iter.next() { None | Some(comma_tok!()) => (), Some(not_comma) => { - tcx.sess.parse_sess.dcx.span_err( + tcx.sess.psess.dcx.span_err( not_comma.span(), "Unexpected token, expected end of attribute or comma", ); diff --git a/kani-compiler/src/kani_middle/intrinsics.rs b/kani-compiler/src/kani_middle/intrinsics.rs index 404cb0f277c3..51e6140b7e1a 100644 --- a/kani-compiler/src/kani_middle/intrinsics.rs +++ b/kani-compiler/src/kani_middle/intrinsics.rs @@ -6,7 +6,7 @@ use rustc_index::IndexVec; use rustc_middle::mir::{Body, Const as mirConst, ConstValue, Operand, TerminatorKind}; use rustc_middle::mir::{Local, LocalDecl}; use rustc_middle::ty::{self, Ty, TyCtxt}; -use rustc_middle::ty::{Const, GenericArgsRef}; +use rustc_middle::ty::{Const, GenericArgsRef, IntrinsicDef}; use rustc_span::source_map::Spanned; use rustc_span::symbol::{sym, Symbol}; use tracing::{debug, trace}; @@ -33,8 +33,8 @@ impl<'tcx> ModelIntrinsics<'tcx> { let terminator = block.terminator_mut(); if let TerminatorKind::Call { func, args, .. } = &mut terminator.kind { let func_ty = func.ty(&self.local_decls, self.tcx); - if let Some((intrinsic_name, generics)) = resolve_rust_intrinsic(self.tcx, func_ty) - { + if let Some((intrinsic, generics)) = resolve_rust_intrinsic(self.tcx, func_ty) { + let intrinsic_name = intrinsic.name; trace!(?func, ?intrinsic_name, "run_pass"); if intrinsic_name == sym::simd_bitmask { self.replace_simd_bitmask(func, args, generics) @@ -99,7 +99,7 @@ fn simd_len_and_type<'tcx>(tcx: TyCtxt<'tcx>, simd_ty: Ty<'tcx>) -> (Const<'tcx> fn resolve_rust_intrinsic<'tcx>( tcx: TyCtxt<'tcx>, func_ty: Ty<'tcx>, -) -> Option<(Symbol, GenericArgsRef<'tcx>)> { +) -> Option<(IntrinsicDef, GenericArgsRef<'tcx>)> { if let ty::FnDef(def_id, args) = *func_ty.kind() { if let Some(symbol) = tcx.intrinsic(def_id) { return Some((symbol, args)); diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 11ba57cb1cff..2fa1bf057c1c 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -515,8 +515,8 @@ fn collect_alloc_items(alloc_id: AllocId) -> Vec { } #[cfg(debug_assertions)] +#[allow(dead_code)] mod debug { - #![allow(dead_code)] use std::fmt::{Display, Formatter}; use std::{ diff --git a/kani-driver/src/assess/mod.rs b/kani-driver/src/assess/mod.rs index d183e880d8b2..2df4d993d2d7 100644 --- a/kani-driver/src/assess/mod.rs +++ b/kani-driver/src/assess/mod.rs @@ -170,7 +170,7 @@ fn reconstruct_metadata_structure( } if !package_artifacts.is_empty() { let mut merged = crate::metadata::merge_kani_metadata(package_artifacts); - merged.crate_name = package.name.clone(); + merged.crate_name.clone_from(&package.name); package_metas.push(merged); } } diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 747a9f2f5295..b6f6e8a63534 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-03-01" +channel = "nightly-2024-03-11" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/coverage/unreachable/variant/expected b/tests/coverage/unreachable/variant/expected index 08a2f824da83..8fa3ec8b870f 100644 --- a/tests/coverage/unreachable/variant/expected +++ b/tests/coverage/unreachable/variant/expected @@ -1,4 +1,4 @@ -coverage/unreachable/variant/main.rs, 15, PARTIAL +coverage/unreachable/variant/main.rs, 15, FULL coverage/unreachable/variant/main.rs, 16, NONE coverage/unreachable/variant/main.rs, 17, NONE coverage/unreachable/variant/main.rs, 18, FULL diff --git a/tools/bookrunner/librustdoc/html/markdown.rs b/tools/bookrunner/librustdoc/html/markdown.rs index 3f827b77ff2b..857b42bcd76a 100644 --- a/tools/bookrunner/librustdoc/html/markdown.rs +++ b/tools/bookrunner/librustdoc/html/markdown.rs @@ -225,7 +225,7 @@ impl LangString { let mut data = LangString::default(); let mut ignores = vec![]; - data.original = string.to_owned(); + string.clone_into(&mut data.original); for token in Self::tokens(string) { match token { From 0cc4b24638288166c5dcd73da55e37e8cd9399e9 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Wed, 13 Mar 2024 21:24:32 +0000 Subject: [PATCH 4/5] Emit `dead` goto-instructions on MIR StatementDead (#3063) This commit adds a new `Dead` goto-instruction that gets codegened whenever Kani sees a MIR `StatementDead` statement. This new goto instruction corresponds to the CBMC [code_deadt]( https://diffblue.github.io/cbmc/classcode__deadt.html) statement that marks the point where a local variable goes out of scope. This new instruction is needed to detect invalid accesses of dead local variables. The commit also codegens a CBMC `Decl` instruction upon seeing a MIR StatementLive. This ensures that variables that go out of scope at the end of a loop are not falsely marked as having a dead dereference when they are accessed on the next loop iteration. Resolves #3061. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- cprover_bindings/src/goto_program/stmt.rs | 7 +++++++ cprover_bindings/src/irep/to_irep.rs | 1 + .../src/codegen_cprover_gotoc/codegen/place.rs | 2 +- .../codegen_cprover_gotoc/codegen/statement.rs | 6 ++++-- kani-driver/src/call_single_file.rs | 2 ++ tests/coverage/reachable/assert-false/expected | 6 +++--- .../reachable/assert/reachable_pass/expected | 2 +- .../reachable/bounds/reachable_fail/expected | 2 +- .../reachable/div-zero/reachable_fail/expected | 2 +- .../reachable/overflow/reachable_fail/expected | 2 +- .../reachable/rem-zero/reachable_fail/expected | 2 +- tests/coverage/unreachable/assert/expected | 4 ++-- tests/coverage/unreachable/assert_eq/expected | 2 +- tests/coverage/unreachable/assert_ne/expected | 2 +- tests/coverage/unreachable/check_id/expected | 4 ++-- .../coverage/unreachable/if-statement/expected | 2 +- .../unreachable/tutorial_unreachable/expected | 2 +- .../unreachable/while-loop-break/expected | 2 +- .../dead-invalid-access-via-raw/expected | 16 ++++++++++++++++ .../dead-invalid-access-via-raw/main.rs | 17 +++++++++++++++++ 20 files changed, 65 insertions(+), 20 deletions(-) create mode 100644 tests/expected/dead-invalid-access-via-raw/expected create mode 100644 tests/expected/dead-invalid-access-via-raw/main.rs diff --git a/cprover_bindings/src/goto_program/stmt.rs b/cprover_bindings/src/goto_program/stmt.rs index 58755a0bffae..951e58f9a954 100644 --- a/cprover_bindings/src/goto_program/stmt.rs +++ b/cprover_bindings/src/goto_program/stmt.rs @@ -57,6 +57,8 @@ pub enum StmtBody { Break, /// `continue;` Continue, + /// End-of-life of a local variable + Dead(Expr), /// `lhs.typ lhs = value;` or `lhs.typ lhs;` Decl { lhs: Expr, // SymbolExpr @@ -232,6 +234,11 @@ impl Stmt { BuiltinFn::CProverCover.call(vec![cond], loc).as_stmt(loc) } + /// Local variable goes out of scope + pub fn dead(symbol: Expr, loc: Location) -> Self { + stmt!(Dead(symbol), loc) + } + /// `lhs.typ lhs = value;` or `lhs.typ lhs;` pub fn decl(lhs: Expr, value: Option, loc: Location) -> Self { assert!(lhs.is_symbol()); diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 16b8b69c8fe7..5c17ecf87b5d 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -433,6 +433,7 @@ impl ToIrep for StmtBody { } StmtBody::Break => code_irep(IrepId::Break, vec![]), StmtBody::Continue => code_irep(IrepId::Continue, vec![]), + StmtBody::Dead(symbol) => code_irep(IrepId::Dead, vec![symbol.to_irep(mm)]), StmtBody::Decl { lhs, value } => { if value.is_some() { code_irep( diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 9296b713c862..6b764fb63365 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -381,7 +381,7 @@ impl<'tcx> GotocCtx<'tcx> { } /// Codegen for a local - fn codegen_local(&mut self, l: Local) -> Expr { + pub fn codegen_local(&mut self, l: Local) -> Expr { let local_ty = self.local_ty_stable(l); // Check if the local is a function definition (see comment above) if let Some(fn_def) = self.codegen_local_fndef(local_ty) { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 05b153f9583f..6379a023423f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -75,8 +75,10 @@ impl<'tcx> GotocCtx<'tcx> { .goto_expr; self.codegen_set_discriminant(dest_ty, dest_expr, *variant_index, location) } - StatementKind::StorageLive(_) => Stmt::skip(location), // TODO: fix me - StatementKind::StorageDead(_) => Stmt::skip(location), // TODO: fix me + StatementKind::StorageLive(var_id) => { + Stmt::decl(self.codegen_local(*var_id), None, location) + } + StatementKind::StorageDead(var_id) => Stmt::dead(self.codegen_local(*var_id), location), StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping( CopyNonOverlapping { src, dst, count }, )) => { diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 9b6e0598daa5..fc41bac69d9c 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -122,6 +122,8 @@ impl KaniSession { "symbol-mangling-version=v0", "-Z", "panic_abort_tests=yes", + "-Z", + "sanitizer=address", ] .map(OsString::from), ); diff --git a/tests/coverage/reachable/assert-false/expected b/tests/coverage/reachable/assert-false/expected index 7a9fef1ca77c..97ffbe1d96e4 100644 --- a/tests/coverage/reachable/assert-false/expected +++ b/tests/coverage/reachable/assert-false/expected @@ -1,8 +1,8 @@ coverage/reachable/assert-false/main.rs, 6, FULL coverage/reachable/assert-false/main.rs, 7, FULL -coverage/reachable/assert-false/main.rs, 11, FULL -coverage/reachable/assert-false/main.rs, 12, FULL -coverage/reachable/assert-false/main.rs, 15, FULL +coverage/reachable/assert-false/main.rs, 11, PARTIAL +coverage/reachable/assert-false/main.rs, 12, PARTIAL +coverage/reachable/assert-false/main.rs, 15, PARTIAL coverage/reachable/assert-false/main.rs, 16, FULL coverage/reachable/assert-false/main.rs, 17, PARTIAL coverage/reachable/assert-false/main.rs, 19, FULL diff --git a/tests/coverage/reachable/assert/reachable_pass/expected b/tests/coverage/reachable/assert/reachable_pass/expected index 67ae085a3e83..9d21185b3a83 100644 --- a/tests/coverage/reachable/assert/reachable_pass/expected +++ b/tests/coverage/reachable/assert/reachable_pass/expected @@ -1,4 +1,4 @@ coverage/reachable/assert/reachable_pass/test.rs, 6, FULL -coverage/reachable/assert/reachable_pass/test.rs, 7, FULL +coverage/reachable/assert/reachable_pass/test.rs, 7, PARTIAL coverage/reachable/assert/reachable_pass/test.rs, 8, FULL coverage/reachable/assert/reachable_pass/test.rs, 10, FULL diff --git a/tests/coverage/reachable/bounds/reachable_fail/expected b/tests/coverage/reachable/bounds/reachable_fail/expected index af2f30e51fe2..fedfec8b2a1e 100644 --- a/tests/coverage/reachable/bounds/reachable_fail/expected +++ b/tests/coverage/reachable/bounds/reachable_fail/expected @@ -1,4 +1,4 @@ coverage/reachable/bounds/reachable_fail/test.rs, 5, PARTIAL coverage/reachable/bounds/reachable_fail/test.rs, 6, NONE -coverage/reachable/bounds/reachable_fail/test.rs, 10, FULL +coverage/reachable/bounds/reachable_fail/test.rs, 10, PARTIAL coverage/reachable/bounds/reachable_fail/test.rs, 11, NONE diff --git a/tests/coverage/reachable/div-zero/reachable_fail/expected b/tests/coverage/reachable/div-zero/reachable_fail/expected index 1ec1abefffd8..c1ac77404680 100644 --- a/tests/coverage/reachable/div-zero/reachable_fail/expected +++ b/tests/coverage/reachable/div-zero/reachable_fail/expected @@ -1,4 +1,4 @@ coverage/reachable/div-zero/reachable_fail/test.rs, 5, PARTIAL coverage/reachable/div-zero/reachable_fail/test.rs, 6, NONE -coverage/reachable/div-zero/reachable_fail/test.rs, 10, FULL +coverage/reachable/div-zero/reachable_fail/test.rs, 10, PARTIAL coverage/reachable/div-zero/reachable_fail/test.rs, 11, NONE diff --git a/tests/coverage/reachable/overflow/reachable_fail/expected b/tests/coverage/reachable/overflow/reachable_fail/expected index f20826fb1a8e..d45edcc37a63 100644 --- a/tests/coverage/reachable/overflow/reachable_fail/expected +++ b/tests/coverage/reachable/overflow/reachable_fail/expected @@ -1,5 +1,5 @@ coverage/reachable/overflow/reachable_fail/test.rs, 8, PARTIAL coverage/reachable/overflow/reachable_fail/test.rs, 9, FULL coverage/reachable/overflow/reachable_fail/test.rs, 13, FULL -coverage/reachable/overflow/reachable_fail/test.rs, 14, FULL +coverage/reachable/overflow/reachable_fail/test.rs, 14, PARTIAL coverage/reachable/overflow/reachable_fail/test.rs, 15, NONE diff --git a/tests/coverage/reachable/rem-zero/reachable_fail/expected b/tests/coverage/reachable/rem-zero/reachable_fail/expected index f7fa6ed7efeb..7852461e4f57 100644 --- a/tests/coverage/reachable/rem-zero/reachable_fail/expected +++ b/tests/coverage/reachable/rem-zero/reachable_fail/expected @@ -1,4 +1,4 @@ coverage/reachable/rem-zero/reachable_fail/test.rs, 5, PARTIAL coverage/reachable/rem-zero/reachable_fail/test.rs, 6, NONE -coverage/reachable/rem-zero/reachable_fail/test.rs, 10, FULL +coverage/reachable/rem-zero/reachable_fail/test.rs, 10, PARTIAL coverage/reachable/rem-zero/reachable_fail/test.rs, 11, NONE diff --git a/tests/coverage/unreachable/assert/expected b/tests/coverage/unreachable/assert/expected index f5b5f8044769..9bc6d8faa4f9 100644 --- a/tests/coverage/unreachable/assert/expected +++ b/tests/coverage/unreachable/assert/expected @@ -1,6 +1,6 @@ coverage/unreachable/assert/test.rs, 6, FULL -coverage/unreachable/assert/test.rs, 7, FULL -coverage/unreachable/assert/test.rs, 9, FULL +coverage/unreachable/assert/test.rs, 7, PARTIAL +coverage/unreachable/assert/test.rs, 9, PARTIAL coverage/unreachable/assert/test.rs, 10, NONE coverage/unreachable/assert/test.rs, 12, NONE coverage/unreachable/assert/test.rs, 16, FULL diff --git a/tests/coverage/unreachable/assert_eq/expected b/tests/coverage/unreachable/assert_eq/expected index f4e7608b2c13..9b13c3c96ded 100644 --- a/tests/coverage/unreachable/assert_eq/expected +++ b/tests/coverage/unreachable/assert_eq/expected @@ -1,5 +1,5 @@ coverage/unreachable/assert_eq/test.rs, 6, FULL coverage/unreachable/assert_eq/test.rs, 7, FULL -coverage/unreachable/assert_eq/test.rs, 8, FULL +coverage/unreachable/assert_eq/test.rs, 8, PARTIAL coverage/unreachable/assert_eq/test.rs, 9, NONE coverage/unreachable/assert_eq/test.rs, 11, FULL diff --git a/tests/coverage/unreachable/assert_ne/expected b/tests/coverage/unreachable/assert_ne/expected index 3b57defb4c36..f027f432e280 100644 --- a/tests/coverage/unreachable/assert_ne/expected +++ b/tests/coverage/unreachable/assert_ne/expected @@ -1,6 +1,6 @@ coverage/unreachable/assert_ne/test.rs, 6, FULL coverage/unreachable/assert_ne/test.rs, 7, FULL coverage/unreachable/assert_ne/test.rs, 8, FULL -coverage/unreachable/assert_ne/test.rs, 10, FULL +coverage/unreachable/assert_ne/test.rs, 10, PARTIAL coverage/unreachable/assert_ne/test.rs, 11, NONE coverage/unreachable/assert_ne/test.rs, 14, FULL diff --git a/tests/coverage/unreachable/check_id/expected b/tests/coverage/unreachable/check_id/expected index 214cbfa827bd..a2d296f0f9a3 100644 --- a/tests/coverage/unreachable/check_id/expected +++ b/tests/coverage/unreachable/check_id/expected @@ -1,5 +1,5 @@ coverage/unreachable/check_id/main.rs, 5, FULL -coverage/unreachable/check_id/main.rs, 6, FULL +coverage/unreachable/check_id/main.rs, 6, PARTIAL coverage/unreachable/check_id/main.rs, 8, NONE coverage/unreachable/check_id/main.rs, 10, FULL coverage/unreachable/check_id/main.rs, 14, FULL @@ -12,5 +12,5 @@ coverage/unreachable/check_id/main.rs, 20, FULL coverage/unreachable/check_id/main.rs, 21, FULL coverage/unreachable/check_id/main.rs, 22, FULL coverage/unreachable/check_id/main.rs, 23, FULL -coverage/unreachable/check_id/main.rs, 24, FULL +coverage/unreachable/check_id/main.rs, 24, PARTIAL coverage/unreachable/check_id/main.rs, 25, NONE diff --git a/tests/coverage/unreachable/if-statement/expected b/tests/coverage/unreachable/if-statement/expected index 4460f23a80de..8b481863a163 100644 --- a/tests/coverage/unreachable/if-statement/expected +++ b/tests/coverage/unreachable/if-statement/expected @@ -1,4 +1,4 @@ -coverage/unreachable/if-statement/main.rs, 5, FULL +coverage/unreachable/if-statement/main.rs, 5, PARTIAL coverage/unreachable/if-statement/main.rs, 7, PARTIAL coverage/unreachable/if-statement/main.rs, 8, NONE coverage/unreachable/if-statement/main.rs, 9, NONE diff --git a/tests/coverage/unreachable/tutorial_unreachable/expected b/tests/coverage/unreachable/tutorial_unreachable/expected index cf45a502d295..624aa520edc9 100644 --- a/tests/coverage/unreachable/tutorial_unreachable/expected +++ b/tests/coverage/unreachable/tutorial_unreachable/expected @@ -1,5 +1,5 @@ coverage/unreachable/tutorial_unreachable/main.rs, 6, FULL coverage/unreachable/tutorial_unreachable/main.rs, 7, FULL -coverage/unreachable/tutorial_unreachable/main.rs, 8, FULL +coverage/unreachable/tutorial_unreachable/main.rs, 8, PARTIAL coverage/unreachable/tutorial_unreachable/main.rs, 9, NONE coverage/unreachable/tutorial_unreachable/main.rs, 11, FULL diff --git a/tests/coverage/unreachable/while-loop-break/expected b/tests/coverage/unreachable/while-loop-break/expected index a0e43c183846..dc66d3e823d3 100644 --- a/tests/coverage/unreachable/while-loop-break/expected +++ b/tests/coverage/unreachable/while-loop-break/expected @@ -1,5 +1,5 @@ coverage/unreachable/while-loop-break/main.rs, 8, FULL -coverage/unreachable/while-loop-break/main.rs, 9, FULL +coverage/unreachable/while-loop-break/main.rs, 9, PARTIAL coverage/unreachable/while-loop-break/main.rs, 10, FULL coverage/unreachable/while-loop-break/main.rs, 11, FULL coverage/unreachable/while-loop-break/main.rs, 13, FULL diff --git a/tests/expected/dead-invalid-access-via-raw/expected b/tests/expected/dead-invalid-access-via-raw/expected new file mode 100644 index 000000000000..1d464eb5f031 --- /dev/null +++ b/tests/expected/dead-invalid-access-via-raw/expected @@ -0,0 +1,16 @@ +SUCCESS\ +address must be a multiple of its type's alignment +FAILURE\ +unsafe { *raw_ptr } == 10 +SUCCESS\ +pointer NULL +SUCCESS\ +pointer invalid +SUCCESS\ +deallocated dynamic object +FAILURE\ +dead object +SUCCESS\ +pointer outside object bounds +SUCCESS\ +invalid integer address diff --git a/tests/expected/dead-invalid-access-via-raw/main.rs b/tests/expected/dead-invalid-access-via-raw/main.rs new file mode 100644 index 000000000000..ed3ea655839e --- /dev/null +++ b/tests/expected/dead-invalid-access-via-raw/main.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// This test checks an issue reported in github.com/model-checking/kani#3063. +// The access of the raw pointer should fail because the value being dereferenced has gone out of +// scope at the time of access. + +#[kani::proof] +pub fn check_invalid_ptr() { + let raw_ptr = { + let var = 10; + &var as *const _ + }; + + // This should fail since it is de-referencing a dead object. + assert_eq!(unsafe { *raw_ptr }, 10); +} From e004eccab617546526ab696511c99f7f957f6074 Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Wed, 13 Mar 2024 15:54:31 -0700 Subject: [PATCH 5/5] Bump Kani version to 0.48.0 (#3075) These are the original release notes for the reference: ## What's Changed * Automatic cargo update to 2024-02-26 by @github-actions in https://github.com/model-checking/kani/pull/3043 * Upgrade rust toolchain to 2024-02-17 by @celinval in https://github.com/model-checking/kani/pull/3040 * Upgrade `windows-targets` crate to version 0.52.4 by @adpaco-aws in https://github.com/model-checking/kani/pull/3049 * Fix `codegen_atomic_binop` for `atomic_ptr` by @qinheping in https://github.com/model-checking/kani/pull/3047 * Upgrade Rust toolchain to `nightly-2024-02-25` by @adpaco-aws in https://github.com/model-checking/kani/pull/3048 * Update s2n-quic submodule by @zhassan-aws in https://github.com/model-checking/kani/pull/3050 * Update s2n-quic submodule weekly through dependabot by @zhassan-aws in https://github.com/model-checking/kani/pull/3053 * Retrieve info for recursion tracker reliably by @feliperodri in https://github.com/model-checking/kani/pull/3045 * Automatic cargo update to 2024-03-04 by @github-actions in https://github.com/model-checking/kani/pull/3055 * Upgrade Rust toolchain to `nightly-2024-03-01` by @adpaco-aws in https://github.com/model-checking/kani/pull/3052 * Add `--use-local-toolchain` to Kani setup by @jaisnan in https://github.com/model-checking/kani/pull/3056 * Replace internal reverse_postorder by a stable one by @celinval in https://github.com/model-checking/kani/pull/3064 * Add option to override `--crate-name` from `kani` by @adpaco-aws in https://github.com/model-checking/kani/pull/3054 * cargo update and fix macos CI by @zhassan-aws in https://github.com/model-checking/kani/pull/3067 * Bump tests/perf/s2n-quic from `d103836` to `1a7faa8` by @dependabot in https://github.com/model-checking/kani/pull/3066 * Upgrade toolchain to 2024-03-11 by @zhassan-aws in https://github.com/model-checking/kani/pull/3071 * Emit `dead` goto-instructions on MIR StatementDead by @karkhaz in https://github.com/model-checking/kani/pull/3063 **Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.47.0...kani-0.48.0 --- CHANGELOG.md | 15 +++++++++++++++ Cargo.lock | 18 +++++++++--------- Cargo.toml | 2 +- cprover_bindings/Cargo.toml | 2 +- kani-compiler/Cargo.toml | 2 +- kani-driver/Cargo.toml | 2 +- kani_metadata/Cargo.toml | 2 +- library/kani/Cargo.toml | 2 +- library/kani_macros/Cargo.toml | 2 +- library/std/Cargo.toml | 2 +- tools/build-kani/Cargo.toml | 2 +- 11 files changed, 33 insertions(+), 18 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 968906b6f4b5..08f687d8e31c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,21 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.) This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards. +## [0.48.0] + +### Major Changes +* We fixed a soundness bug that in some cases may cause Kani to not detect a use-after-free issue in https://github.com/model-checking/kani/pull/3063 + +### What's Changed +* Fix `codegen_atomic_binop` for `atomic_ptr` by @qinheping in https://github.com/model-checking/kani/pull/3047 +* Retrieve info for recursion tracker reliably by @feliperodri in https://github.com/model-checking/kani/pull/3045 +* Add `--use-local-toolchain` to Kani setup by @jaisnan in https://github.com/model-checking/kani/pull/3056 +* Replace internal reverse_postorder by a stable one by @celinval in https://github.com/model-checking/kani/pull/3064 +* Add option to override `--crate-name` from `kani` by @adpaco-aws in https://github.com/model-checking/kani/pull/3054 +* Rust toolchain upgraded to 2024-03-11 by @adpaco-ws @celinval @zyadh + +**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.47.0...kani-0.48.0 + ## [0.47.0] ### What's Changed diff --git a/Cargo.lock b/Cargo.lock index 4db35ee6ab77..7009622b1733 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -141,7 +141,7 @@ dependencies = [ [[package]] name = "build-kani" -version = "0.47.0" +version = "0.48.0" dependencies = [ "anyhow", "cargo_metadata", @@ -292,7 +292,7 @@ dependencies = [ [[package]] name = "cprover_bindings" -version = "0.47.0" +version = "0.48.0" dependencies = [ "lazy_static", "linear-map", @@ -472,14 +472,14 @@ checksum = "b1a46d1a171d865aa5f83f92695765caa047a9b4cbae2cbf37dbd613a793fd4c" [[package]] name = "kani" -version = "0.47.0" +version = "0.48.0" dependencies = [ "kani_macros", ] [[package]] name = "kani-compiler" -version = "0.47.0" +version = "0.48.0" dependencies = [ "clap 4.5.2", "cprover_bindings", @@ -500,7 +500,7 @@ dependencies = [ [[package]] name = "kani-driver" -version = "0.47.0" +version = "0.48.0" dependencies = [ "anyhow", "cargo_metadata", @@ -528,7 +528,7 @@ dependencies = [ [[package]] name = "kani-verifier" -version = "0.47.0" +version = "0.48.0" dependencies = [ "anyhow", "clap 2.34.0", @@ -538,7 +538,7 @@ dependencies = [ [[package]] name = "kani_macros" -version = "0.47.0" +version = "0.48.0" dependencies = [ "proc-macro-error", "proc-macro2", @@ -548,7 +548,7 @@ dependencies = [ [[package]] name = "kani_metadata" -version = "0.47.0" +version = "0.48.0" dependencies = [ "clap 4.5.2", "cprover_bindings", @@ -1079,7 +1079,7 @@ checksum = "e6ecd384b10a64542d77071bd64bd7b231f4ed5940fba55e98c3de13824cf3d7" [[package]] name = "std" -version = "0.47.0" +version = "0.48.0" dependencies = [ "kani", ] diff --git a/Cargo.toml b/Cargo.toml index 845751118363..c863ffdc1945 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-verifier" -version = "0.47.0" +version = "0.48.0" edition = "2021" description = "A bit-precise model checker for Rust." readme = "README.md" diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml index 3882e5ad300c..b9d0259b3577 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "cprover_bindings" -version = "0.47.0" +version = "0.48.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index c5ac44d0be1e..a5b7fd006180 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-compiler" -version = "0.47.0" +version = "0.48.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index a009f444840b..36a979a1366d 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-driver" -version = "0.47.0" +version = "0.48.0" edition = "2021" description = "Build a project with Kani and run all proof harnesses" license = "MIT OR Apache-2.0" diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml index 92cba41e27f8..6b6db72f4a6d 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_metadata" -version = "0.47.0" +version = "0.48.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index 27fc6fc9ad6d..4da7f91a9ed7 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani" -version = "0.47.0" +version = "0.48.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index 46b6cf3daadd..b2254b5c8954 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_macros" -version = "0.47.0" +version = "0.48.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index bdd10673f640..29467fddf70b 100644 --- a/library/std/Cargo.toml +++ b/library/std/Cargo.toml @@ -5,7 +5,7 @@ # Note: this package is intentionally named std to make sure the names of # standard library symbols are preserved name = "std" -version = "0.47.0" +version = "0.48.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml index 8c80063d7ff5..b75c373655bd 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "build-kani" -version = "0.47.0" +version = "0.48.0" edition = "2021" description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0"