From e906cde630dc4d9105fda37b636a39328c34641c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 10 Apr 2024 15:22:15 +0200 Subject: [PATCH 01/15] Remove is-a-parameter from gen_stack_variable (#3137) A function-local variable cannot at the same time be a parameter. Alas, all uses of gen_stack_variable passed in `false` for `is_param`, so this wasn't making a difference anyway. --- .../src/codegen_cprover_gotoc/context/goto_ctx.rs | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) 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 3a6501d544d8..095f907228a4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -137,7 +137,7 @@ impl<'tcx> GotocCtx<'tcx> { // Generate a Symbol Expression representing a function variable from the MIR pub fn gen_function_local_variable(&mut self, c: u64, fname: &str, t: Type) -> Symbol { - self.gen_stack_variable(c, fname, "var", t, Location::none(), false) + self.gen_stack_variable(c, fname, "var", t, Location::none()) } /// Given a counter `c` a function name `fname, and a prefix `prefix`, generates a new function local variable @@ -149,11 +149,10 @@ impl<'tcx> GotocCtx<'tcx> { prefix: &str, t: Type, loc: Location, - is_param: bool, ) -> Symbol { let base_name = format!("{prefix}_{c}"); let name = format!("{fname}::1::{base_name}"); - let symbol = Symbol::variable(name, base_name, t, loc).with_is_parameter(is_param); + let symbol = Symbol::variable(name, base_name, t, loc); self.symbol_table.insert(symbol.clone()); symbol } @@ -167,8 +166,7 @@ impl<'tcx> GotocCtx<'tcx> { loc: Location, ) -> (Expr, Stmt) { let c = self.current_fn_mut().get_and_incr_counter(); - let var = - self.gen_stack_variable(c, &self.current_fn().name(), "temp", t, loc, false).to_expr(); + let var = self.gen_stack_variable(c, &self.current_fn().name(), "temp", t, loc).to_expr(); let value = value.or_else(|| self.codegen_default_initializer(&var)); let decl = Stmt::decl(var.clone(), value, loc); (var, decl) From b9bd7a8a949105d42ef94591389883545cde88ef Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 16 Apr 2024 15:02:36 -0700 Subject: [PATCH 02/15] Upgrade toolchain to nightly-2024-04-15 (#3144) Related changes: - https://github.com/rust-lang/rust/pull/118310: Add `Ord::cmp` for primitives as a `BinOp` in MIR - https://github.com/rust-lang/rust/pull/120131: Add support to `Pat` pattern type - https://github.com/rust-lang/rust/pull/122935: Rename CastKind::PointerWithExposedProvenance - https://github.com/rust-lang/rust/pull/123097: Adapt to changes to local_def_path_hash_to_def_id Resolves #3130, #3142 --- cprover_bindings/src/goto_program/expr.rs | 1 + .../codegen_cprover_gotoc/codegen/place.rs | 5 + .../codegen_cprover_gotoc/codegen/rvalue.rs | 122 ++++++++++++------ .../src/codegen_cprover_gotoc/codegen/typ.rs | 8 ++ .../src/kani_middle/stubbing/annotations.rs | 2 +- .../src/kani_middle/stubbing/transform.rs | 2 +- .../src/kani_middle/transform/check_values.rs | 8 +- rust-toolchain.toml | 2 +- 8 files changed, 110 insertions(+), 40 deletions(-) diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 28f8afb4fae7..9f97e7a0a599 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -389,6 +389,7 @@ impl Expr { source.is_integer() || source.is_pointer() || source.is_bool() } else if target.is_integer() { source.is_c_bool() + || source.is_bool() || source.is_integer() || source.is_floating_point() || source.is_pointer() diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 6b764fb63365..d24e5448c595 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -292,6 +292,11 @@ impl<'tcx> GotocCtx<'tcx> { "element of {parent_ty:?} is not accessed via field projection" ) } + TyKind::RigidTy(RigidTy::Pat(..)) => { + // See https://github.com/rust-lang/types-team/issues/126 + // for what is currently supported. + unreachable!("projection inside a pattern is not supported, only transmute") + } } } // if we fall here, then we are handling an enum diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 74622d41ed50..cb78163fe99b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -20,6 +20,7 @@ use num::bigint::BigInt; use rustc_middle::ty::{TyCtxt, VtblEntry}; use rustc_smir::rustc_internal; use rustc_target::abi::{FieldsShape, TagEncoding, Variants}; +use stable_mir::abi::{Primitive, Scalar, ValueAbi}; use stable_mir::mir::mono::Instance; use stable_mir::mir::{ AggregateKind, BinOp, CastKind, NullOp, Operand, Place, PointerCoercion, Rvalue, UnOp, @@ -32,9 +33,11 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_comparison(&mut self, op: &BinOp, e1: &Operand, e2: &Operand) -> Expr { let left_op = self.codegen_operand_stable(e1); let right_op = self.codegen_operand_stable(e2); - let is_float = - matches!(self.operand_ty_stable(e1).kind(), TyKind::RigidTy(RigidTy::Float(..))); - comparison_expr(op, left_op, right_op, is_float) + let left_ty = self.operand_ty_stable(e1); + let right_ty = self.operand_ty_stable(e2); + let res_ty = op.ty(left_ty, right_ty); + let is_float = matches!(left_ty.kind(), TyKind::RigidTy(RigidTy::Float(..))); + self.comparison_expr(op, left_op, right_op, res_ty, is_float) } /// This function codegen comparison for fat pointers. @@ -72,16 +75,18 @@ impl<'tcx> GotocCtx<'tcx> { Expr::statement_expression(body, ret_type).with_location(loc) } else { // Compare data pointer. + let res_ty = op.ty(left_typ, right_typ); let left_ptr = self.codegen_operand_stable(left_op); let left_data = left_ptr.clone().member("data", &self.symbol_table); let right_ptr = self.codegen_operand_stable(right_op); let right_data = right_ptr.clone().member("data", &self.symbol_table); - let data_cmp = comparison_expr(op, left_data.clone(), right_data.clone(), false); + let data_cmp = + self.comparison_expr(op, left_data.clone(), right_data.clone(), res_ty, false); // Compare the slice metadata (this logic could be adapted to compare vtable if needed). let left_len = left_ptr.member("len", &self.symbol_table); let right_len = right_ptr.member("len", &self.symbol_table); - let metadata_cmp = comparison_expr(op, left_len, right_len, false); + let metadata_cmp = self.comparison_expr(op, left_len, right_len, res_ty, false); // Join the results. // https://github.com/rust-lang/rust/pull/29781 @@ -93,10 +98,20 @@ impl<'tcx> GotocCtx<'tcx> { // If data is different, only compare data. // If data is equal, apply operator to metadata. BinOp::Lt | BinOp::Le | BinOp::Ge | BinOp::Gt => { - let data_eq = - comparison_expr(&BinOp::Eq, left_data.clone(), right_data.clone(), false); - let data_strict_comp = - comparison_expr(&get_strict_operator(op), left_data, right_data, false); + let data_eq = self.comparison_expr( + &BinOp::Eq, + left_data.clone(), + right_data.clone(), + res_ty, + false, + ); + let data_strict_comp = self.comparison_expr( + &get_strict_operator(op), + left_data, + right_data, + res_ty, + false, + ); data_strict_comp.or(data_eq.and(metadata_cmp)) } _ => unreachable!("Unexpected operator {:?}", op), @@ -376,7 +391,7 @@ impl<'tcx> GotocCtx<'tcx> { BinOp::BitXor | BinOp::BitAnd | BinOp::BitOr => { self.codegen_unchecked_scalar_binop(op, e1, e2) } - BinOp::Eq | BinOp::Lt | BinOp::Le | BinOp::Ne | BinOp::Ge | BinOp::Gt => { + BinOp::Eq | BinOp::Lt | BinOp::Le | BinOp::Ne | BinOp::Ge | BinOp::Gt | BinOp::Cmp => { let op_ty = self.operand_ty_stable(e1); if self.is_fat_pointer_stable(op_ty) { self.codegen_comparison_fat_ptr(op, e1, e2, loc) @@ -681,7 +696,7 @@ impl<'tcx> GotocCtx<'tcx> { | CastKind::FnPtrToPtr | CastKind::PtrToPtr | CastKind::PointerExposeAddress - | CastKind::PointerFromExposedAddress, + | CastKind::PointerWithExposedProvenance, e, t, ) => self.codegen_misc_cast(e, *t), @@ -1260,7 +1275,7 @@ impl<'tcx> GotocCtx<'tcx> { fn check_vtable_size(&mut self, operand_type: Ty, vt_size: Expr) -> Stmt { // Check against the size we get from the layout from the what we // get constructing a value of that type - let ty: Type = self.codegen_ty_stable(operand_type); + let ty = self.codegen_ty_stable(operand_type); let codegen_size = ty.sizeof(&self.symbol_table); assert_eq!(vt_size.int_constant_value().unwrap(), BigInt::from(codegen_size)); @@ -1423,6 +1438,65 @@ impl<'tcx> GotocCtx<'tcx> { } } } + + fn comparison_expr( + &mut self, + op: &BinOp, + left: Expr, + right: Expr, + res_ty: Ty, + is_float: bool, + ) -> Expr { + match op { + BinOp::Eq => { + if is_float { + left.feq(right) + } else { + left.eq(right) + } + } + BinOp::Lt => left.lt(right), + BinOp::Le => left.le(right), + BinOp::Ne => { + if is_float { + left.fneq(right) + } else { + left.neq(right) + } + } + BinOp::Ge => left.ge(right), + BinOp::Gt => left.gt(right), + BinOp::Cmp => { + // Implement https://doc.rust-lang.org/core/cmp/trait.Ord.html as done in cranelift, + // i.e., (left > right) - (left < right) + // Return value is the Ordering enumeration: + // ``` + // #[repr(i8)] + // pub enum Ordering { + // Less = -1, + // Equal = 0, + // Greater = 1, + // } + // ``` + let res_typ = self.codegen_ty_stable(res_ty); + let ValueAbi::Scalar(Scalar::Initialized { value, valid_range }) = + res_ty.layout().unwrap().shape().abi + else { + unreachable!("Unexpected layout") + }; + assert_eq!(valid_range.start, -1i8 as u8 as u128); + assert_eq!(valid_range.end, 1); + let Primitive::Int { length, signed: true } = value else { unreachable!() }; + let scalar_typ = Type::signed_int(length.bits()); + left.clone() + .gt(right.clone()) + .cast_to(scalar_typ.clone()) + .sub(left.lt(right).cast_to(scalar_typ)) + .transmute_to(res_typ, &self.symbol_table) + } + _ => unreachable!(), + } + } } /// Perform a wrapping subtraction of an Expr with a constant "expr - constant" @@ -1445,30 +1519,6 @@ fn wrapping_sub(expr: &Expr, constant: u64) -> Expr { } } -fn comparison_expr(op: &BinOp, left: Expr, right: Expr, is_float: bool) -> Expr { - match op { - BinOp::Eq => { - if is_float { - left.feq(right) - } else { - left.eq(right) - } - } - BinOp::Lt => left.lt(right), - BinOp::Le => left.le(right), - BinOp::Ne => { - if is_float { - left.fneq(right) - } else { - left.neq(right) - } - } - BinOp::Ge => left.ge(right), - BinOp::Gt => left.gt(right), - _ => unreachable!(), - } -} - /// Remove the equality from an operator. Translates `<=` to `<` and `>=` to `>` fn get_strict_operator(op: &BinOp) -> BinOp { match op { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index b5ccf1a83716..64c36dd76cfb 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -595,6 +595,13 @@ impl<'tcx> GotocCtx<'tcx> { ) } } + // This object has the same layout as base. For now, translate this into `(base)`. + // The only difference is the niche. + ty::Pat(base_ty, ..) => { + self.ensure_struct(self.ty_mangled_name(ty), self.ty_pretty_name(ty), |tcx, _| { + tcx.codegen_ty_tuple_like(ty, vec![*base_ty]) + }) + } ty::Alias(..) => { unreachable!("Type should've been normalized already") } @@ -995,6 +1002,7 @@ impl<'tcx> GotocCtx<'tcx> { | ty::Int(_) | ty::RawPtr(_, _) | ty::Ref(..) + | ty::Pat(..) | ty::Tuple(_) | ty::Uint(_) => self.codegen_ty(pointee_type).to_pointer(), diff --git a/kani-compiler/src/kani_middle/stubbing/annotations.rs b/kani-compiler/src/kani_middle/stubbing/annotations.rs index 52b994ab97d2..26e508707207 100644 --- a/kani-compiler/src/kani_middle/stubbing/annotations.rs +++ b/kani-compiler/src/kani_middle/stubbing/annotations.rs @@ -56,7 +56,7 @@ pub fn update_stub_mapping( "duplicate stub mapping: {} mapped to {} and {}", tcx.def_path_str(orig_id), tcx.def_path_str(stub_id), - tcx.def_path_str(tcx.def_path_hash_to_def_id(other, &mut || panic!())) + tcx.def_path_str(tcx.def_path_hash_to_def_id(other, &())) ), ); } diff --git a/kani-compiler/src/kani_middle/stubbing/transform.rs b/kani-compiler/src/kani_middle/stubbing/transform.rs index 16c46990bc6f..f101a6009907 100644 --- a/kani-compiler/src/kani_middle/stubbing/transform.rs +++ b/kani-compiler/src/kani_middle/stubbing/transform.rs @@ -234,7 +234,7 @@ fn deserialize_mapping(tcx: TyCtxt, val: &str) -> HashMap { type Item = (u64, u64); let item_to_def_id = |item: Item| -> DefId { let hash = DefPathHash(Fingerprint::new(item.0, item.1)); - tcx.def_path_hash_to_def_id(hash, &mut || panic!()) + tcx.def_path_hash_to_def_id(hash, &()) }; let pairs: Vec<(Item, Item)> = serde_json::from_str(val).unwrap(); let mut m = HashMap::default(); diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index a620dfabb72e..d62b5807319e 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -631,7 +631,7 @@ impl<'a> MirVisitor for CheckValueVisitor<'a> { ty: (rvalue.ty(self.locals).unwrap()), }), CastKind::PointerExposeAddress - | CastKind::PointerFromExposedAddress + | CastKind::PointerWithExposedProvenance | CastKind::PointerCoercion(_) | CastKind::IntToInt | CastKind::FloatToInt @@ -898,6 +898,12 @@ fn ty_validity_per_offset( } } } + RigidTy::Pat(base_ty, ..) => { + // This is similar to a structure with one field and with niche defined. + let mut pat_validity = ty_req(); + pat_validity.append(&mut ty_validity_per_offset(machine_info, *base_ty, 0)?); + Ok(pat_validity) + } RigidTy::Tuple(tys) => { let mut tuple_validity = vec![]; for idx in layout.fields.fields_by_offset_order() { diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 1ee76e0f92f1..be42da187e10 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-04-02" +channel = "nightly-2024-04-15" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] From 7b08d7f9dc262a096c7264bd3d00052c64dbff44 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 17 Apr 2024 00:40:32 +0200 Subject: [PATCH 03/15] Fix syntax error in cbmc-update CI job (#3139) It's "env" and not "evn". --- .github/workflows/cbmc-update.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/cbmc-update.yml b/.github/workflows/cbmc-update.yml index 74d9caeb0fcf..6f9a6ae3a74b 100644 --- a/.github/workflows/cbmc-update.yml +++ b/.github/workflows/cbmc-update.yml @@ -79,7 +79,7 @@ jobs: token: ${{ github.token }} title: 'CBMC upgrade to ${{ env.CBMC_LATEST }} failed' body: > - Updating CBMC from ${{ evn.CBMC_VERSION }} to ${{ env.CBMC_LATEST }} failed. + Updating CBMC from ${{ env.CBMC_VERSION }} to ${{ env.CBMC_LATEST }} failed. The failed automated run [can be found here.](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) From ec34e01431d70cff72ab8b76f29c347bb086c4c6 Mon Sep 17 00:00:00 2001 From: Kareem Khazem Date: Wed, 17 Apr 2024 00:27:55 +0100 Subject: [PATCH 04/15] Handle errors thrown from benchcomp column exprs (#3145) Prior to this commit, errors thrown when evaluating the text of a benchcomp extra column would crash benchcomp. This could happen, for example, if a column tries to compare an old variant with a new one, but no data for the old variant exists, as seen in this run: https://github.com/model-checking/kani/actions/runs/8700040930/job/23859607740 Forcing the user to do error handling in the column text would make the text even more unwieldy than it already is, so this commit makes the column text evaluate to **** if an exception is raised during evaluation. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- tools/benchcomp/benchcomp/visualizers/__init__.py | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/tools/benchcomp/benchcomp/visualizers/__init__.py b/tools/benchcomp/benchcomp/visualizers/__init__.py index 8de4a9f130b6..1452488c76b1 100644 --- a/tools/benchcomp/benchcomp/visualizers/__init__.py +++ b/tools/benchcomp/benchcomp/visualizers/__init__.py @@ -358,7 +358,20 @@ def _add_extra_columns(self, metrics): for bench, variants in benches.items(): tmp_variants = dict(variants) for column in columns: - variants[column["column_name"]] = column["text"](tmp_variants) + if "column_name" not in column: + logging.error( + "A column specification for metric %s did not " + "contain a column_name field. Each column should " + "have a column name and column text", metric) + sys.exit(1) + try: + variants[column["column_name"]] = column["text"](tmp_variants) + except BaseException: + # This may be reached when evaluating the column text + # throws an exception. The column text is written in a + # YAML file and is typically a simple lambda so can't + # contain sophisticated error handling. + variants[column["column_name"]] = "**ERROR**" @staticmethod From 299b0b3cf94a96dbf09e8efb42858079c0dc1117 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 17 Apr 2024 14:01:05 -0700 Subject: [PATCH 05/15] Bump dependencies and Kani's version to 0.50.0 (#3148) Release notes are the following: ### Major Changes * Fix compilation issue with proc_macro2 (v1.0.80+) and Kani v0.49.0 (https://github.com/model-checking/kani/issues/3138). ### What's Changed * Implement valid value check for `write_bytes` by @celinval in https://github.com/model-checking/kani/pull/3108 * Rust toolchain upgraded to 2024-04-15 by @tautschnig @celinval **Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.49.0...kani-0.50.0 --- CHANGELOG.md | 14 ++++ Cargo.lock | 131 +++++++++++++++++---------------- 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, 92 insertions(+), 71 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index bd592b2f27a7..61e06601dfc3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,20 @@ 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.50.0] + +### Major Changes +* Fix compilation issue with proc_macro2 (v1.0.80+) and Kani v0.49.0 +(https://github.com/model-checking/kani/issues/3138). + +### What's Changed +* Implement valid value check for `write_bytes` by @celinval in +https://github.com/model-checking/kani/pull/3108 +* Rust toolchain upgraded to 2024-04-15 by @tautschnig @celinval + +**Full Changelog**: +https://github.com/model-checking/kani/compare/kani-0.49.0...kani-0.50.0 + ## [0.49.0] ### What's Changed diff --git a/Cargo.lock b/Cargo.lock index ae711d863430..821dbd9c346c 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -73,9 +73,9 @@ dependencies = [ [[package]] name = "anyhow" -version = "1.0.81" +version = "1.0.82" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0952808a6c2afd1aa8947271f3a60f1a6763c7b912d210184c5149b5cf147247" +checksum = "f538837af36e6f6a9be0faa67f9a314f8119e4e4b5867c6ab40ed60360142519" [[package]] name = "autocfg" @@ -97,7 +97,7 @@ checksum = "cf4b9d6a944f767f8e5e0db018570623c85f3d925ac718db4e06d0187adb21c1" [[package]] name = "build-kani" -version = "0.49.0" +version = "0.50.0" dependencies = [ "anyhow", "cargo_metadata", @@ -174,7 +174,7 @@ dependencies = [ "heck 0.5.0", "proc-macro2", "quote", - "syn 2.0.58", + "syn 2.0.59", ] [[package]] @@ -233,7 +233,7 @@ dependencies = [ [[package]] name = "cprover_bindings" -version = "0.49.0" +version = "0.50.0" dependencies = [ "lazy_static", "linear-map", @@ -295,9 +295,9 @@ dependencies = [ [[package]] name = "either" -version = "1.10.0" +version = "1.11.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "11157ac094ffbdde99aa67b23417ebdd801842852b500e395a45a9c0aac03e4a" +checksum = "a47c1c47d2f5964e29c61246e81db715514cd532db6b5116a25ea3c03d6780a2" [[package]] name = "encode_unicode" @@ -338,9 +338,9 @@ dependencies = [ [[package]] name = "getrandom" -version = "0.2.13" +version = "0.2.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a06fddc2749e0528d2813f95e050e87e52c8cbbae56223b9babf73b3e53b0cc6" +checksum = "94b22e06ecb0110981051723910cbf0b5f5e09a2062dd7663334ee79a9d1286c" dependencies = [ "cfg-if", "libc", @@ -410,14 +410,14 @@ checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b" [[package]] name = "kani" -version = "0.49.0" +version = "0.50.0" dependencies = [ "kani_macros", ] [[package]] name = "kani-compiler" -version = "0.49.0" +version = "0.50.0" dependencies = [ "clap", "cprover_bindings", @@ -438,7 +438,7 @@ dependencies = [ [[package]] name = "kani-driver" -version = "0.49.0" +version = "0.50.0" dependencies = [ "anyhow", "cargo_metadata", @@ -466,7 +466,7 @@ dependencies = [ [[package]] name = "kani-verifier" -version = "0.49.0" +version = "0.50.0" dependencies = [ "anyhow", "home", @@ -475,17 +475,17 @@ dependencies = [ [[package]] name = "kani_macros" -version = "0.49.0" +version = "0.50.0" dependencies = [ "proc-macro-error", "proc-macro2", "quote", - "syn 2.0.58", + "syn 2.0.59", ] [[package]] name = "kani_metadata" -version = "0.49.0" +version = "0.50.0" dependencies = [ "clap", "cprover_bindings", @@ -571,9 +571,9 @@ dependencies = [ [[package]] name = "num" -version = "0.4.1" +version = "0.4.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b05180d69e3da0e530ba2a1dae5110317e49e3b7f3d41be227dc5f92e49ee7af" +checksum = "3135b08af27d103b0a51f2ae0f8632117b7b185ccf931445affa8df530576a41" dependencies = [ "num-bigint", "num-complex", @@ -733,18 +733,18 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.79" +version = "1.0.81" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e835ff2298f5721608eb1a980ecaee1aef2c132bf95ecc026a11b7bf3c01c02e" +checksum = "3d1597b0c024618f09a9c3b8655b7e430397a36d23fdafec26d6965e9eec3eba" dependencies = [ "unicode-ident", ] [[package]] name = "quote" -version = "1.0.35" +version = "1.0.36" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "291ec9ab5efd934aaf503a6466c5d5251535d108ee747472c3977cc5acc868ef" +checksum = "0fa76aaf39101c457836aec0ce2316dbdc3ab723cdda1c6bd4e6ad4208acaca7" dependencies = [ "proc-macro2", ] @@ -909,29 +909,29 @@ dependencies = [ [[package]] name = "serde" -version = "1.0.197" +version = "1.0.198" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3fb1c873e1b9b056a4dc4c0c198b24c3ffa059243875552b2bd0933b1aee4ce2" +checksum = "9846a40c979031340571da2545a4e5b7c4163bdae79b301d5f86d03979451fcc" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.197" +version = "1.0.198" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7eb0b34b42edc17f6b7cac84a52a1c5f0e1bb2227e997ca9011ea3dd34e8610b" +checksum = "e88edab869b01783ba905e7d0153f9fc1a6505a96e4ad3018011eedb838566d9" dependencies = [ "proc-macro2", "quote", - "syn 2.0.58", + "syn 2.0.59", ] [[package]] name = "serde_json" -version = "1.0.115" +version = "1.0.116" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "12dc5c46daa8e9fdf4f5e71b6cf9a53f2487da0e86e55808e2d35539666497dd" +checksum = "3e17db7126d17feb94eb3fad46bf1a96b034e8aacbc2e775fe81505f8b0b2813" dependencies = [ "itoa", "ryu", @@ -992,7 +992,7 @@ checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67" [[package]] name = "std" -version = "0.49.0" +version = "0.50.0" dependencies = [ "kani", ] @@ -1030,7 +1030,7 @@ dependencies = [ "proc-macro2", "quote", "rustversion", - "syn 2.0.58", + "syn 2.0.59", ] [[package]] @@ -1045,9 +1045,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.58" +version = "2.0.59" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "44cfb93f38070beee36b3fef7d4f5a16f27751d94b187b666a5cc5e9b0d30687" +checksum = "4a6531ffc7b071655e4ce2e04bd464c4830bb585a61cabb96cf808f05172615a" dependencies = [ "proc-macro2", "quote", @@ -1083,7 +1083,7 @@ checksum = "c61f3ba182994efc43764a46c018c347bc492c79f024e705f46567b418f6d4f7" dependencies = [ "proc-macro2", "quote", - "syn 2.0.58", + "syn 2.0.59", ] [[package]] @@ -1149,7 +1149,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" dependencies = [ "proc-macro2", "quote", - "syn 2.0.58", + "syn 2.0.59", ] [[package]] @@ -1315,7 +1315,7 @@ version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d" dependencies = [ - "windows-targets 0.52.4", + "windows-targets 0.52.5", ] [[package]] @@ -1335,17 +1335,18 @@ dependencies = [ [[package]] name = "windows-targets" -version = "0.52.4" +version = "0.52.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7dd37b7e5ab9018759f893a1952c9420d060016fc19a472b4bb20d1bdd694d1b" +checksum = "6f0713a46559409d202e70e28227288446bf7841d3211583a4b53e3f6d96e7eb" dependencies = [ - "windows_aarch64_gnullvm 0.52.4", - "windows_aarch64_msvc 0.52.4", - "windows_i686_gnu 0.52.4", - "windows_i686_msvc 0.52.4", - "windows_x86_64_gnu 0.52.4", - "windows_x86_64_gnullvm 0.52.4", - "windows_x86_64_msvc 0.52.4", + "windows_aarch64_gnullvm 0.52.5", + "windows_aarch64_msvc 0.52.5", + "windows_i686_gnu 0.52.5", + "windows_i686_gnullvm", + "windows_i686_msvc 0.52.5", + "windows_x86_64_gnu 0.52.5", + "windows_x86_64_gnullvm 0.52.5", + "windows_x86_64_msvc 0.52.5", ] [[package]] @@ -1356,9 +1357,9 @@ checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8" [[package]] name = "windows_aarch64_gnullvm" -version = "0.52.4" +version = "0.52.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bcf46cf4c365c6f2d1cc93ce535f2c8b244591df96ceee75d8e83deb70a9cac9" +checksum = "7088eed71e8b8dda258ecc8bac5fb1153c5cffaf2578fc8ff5d61e23578d3263" [[package]] name = "windows_aarch64_msvc" @@ -1368,9 +1369,9 @@ checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc" [[package]] name = "windows_aarch64_msvc" -version = "0.52.4" +version = "0.52.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "da9f259dd3bcf6990b55bffd094c4f7235817ba4ceebde8e6d11cd0c5633b675" +checksum = "9985fd1504e250c615ca5f281c3f7a6da76213ebd5ccc9561496568a2752afb6" [[package]] name = "windows_i686_gnu" @@ -1380,9 +1381,15 @@ checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e" [[package]] name = "windows_i686_gnu" -version = "0.52.4" +version = "0.52.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b474d8268f99e0995f25b9f095bc7434632601028cf86590aea5c8a5cb7801d3" +checksum = "88ba073cf16d5372720ec942a8ccbf61626074c6d4dd2e745299726ce8b89670" + +[[package]] +name = "windows_i686_gnullvm" +version = "0.52.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "87f4261229030a858f36b459e748ae97545d6f1ec60e5e0d6a3d32e0dc232ee9" [[package]] name = "windows_i686_msvc" @@ -1392,9 +1399,9 @@ checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406" [[package]] name = "windows_i686_msvc" -version = "0.52.4" +version = "0.52.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1515e9a29e5bed743cb4415a9ecf5dfca648ce85ee42e15873c3cd8610ff8e02" +checksum = "db3c2bf3d13d5b658be73463284eaf12830ac9a26a90c717b7f771dfe97487bf" [[package]] name = "windows_x86_64_gnu" @@ -1404,9 +1411,9 @@ checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e" [[package]] name = "windows_x86_64_gnu" -version = "0.52.4" +version = "0.52.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5eee091590e89cc02ad514ffe3ead9eb6b660aedca2183455434b93546371a03" +checksum = "4e4246f76bdeff09eb48875a0fd3e2af6aada79d409d33011886d3e1581517d9" [[package]] name = "windows_x86_64_gnullvm" @@ -1416,9 +1423,9 @@ checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc" [[package]] name = "windows_x86_64_gnullvm" -version = "0.52.4" +version = "0.52.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "77ca79f2451b49fa9e2af39f0747fe999fcda4f5e241b2898624dca97a1f2177" +checksum = "852298e482cd67c356ddd9570386e2862b5673c85bd5f88df9ab6802b334c596" [[package]] name = "windows_x86_64_msvc" @@ -1428,15 +1435,15 @@ checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538" [[package]] name = "windows_x86_64_msvc" -version = "0.52.4" +version = "0.52.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "32b752e52a2da0ddfbdbcc6fceadfeede4c939ed16d13e648833a61dfb611ed8" +checksum = "bec47e5bfd1bff0eeaf6d8b485cc1074891a197ab4225d504cb7a1ab88b02bf0" [[package]] name = "winnow" -version = "0.6.5" +version = "0.6.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dffa400e67ed5a4dd237983829e66475f0a4a26938c4b04c21baede6262215b8" +checksum = "f0c976aaaa0e1f90dbb21e9587cdaf1d9679a1cde8875c0d6bd83ab96a208352" dependencies = [ "memchr", ] @@ -1464,5 +1471,5 @@ checksum = "9ce1b18ccd8e73a9321186f97e46f9f04b778851177567b1975109d26a08d2a6" dependencies = [ "proc-macro2", "quote", - "syn 2.0.58", + "syn 2.0.59", ] diff --git a/Cargo.toml b/Cargo.toml index e271a3650c03..93affb02856f 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-verifier" -version = "0.49.0" +version = "0.50.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 ed0e57847e71..d199558ff16a 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "cprover_bindings" -version = "0.49.0" +version = "0.50.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index ffc508e90866..244172715056 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-compiler" -version = "0.49.0" +version = "0.50.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 3a476922a838..ab83c2202bc9 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-driver" -version = "0.49.0" +version = "0.50.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 582c20c7bd9f..7936d943556b 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_metadata" -version = "0.49.0" +version = "0.50.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index b87536740fcd..97952dd7ab9e 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani" -version = "0.49.0" +version = "0.50.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 fe4279fc4366..a54fb44d8b6c 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_macros" -version = "0.49.0" +version = "0.50.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index 05f5b4de5635..6f9a380fc584 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.49.0" +version = "0.50.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 525c060232a7..eabb396e0923 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "build-kani" -version = "0.49.0" +version = "0.50.0" edition = "2021" description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0" From 12635fd10cdc5b81ceb880c19a9cfd9856d0014e Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 18 Apr 2024 16:11:21 -0700 Subject: [PATCH 06/15] Upgrade toolchain to 2024-04-18 and improve toolchain workflow (#3149) The toolchain upgrade itself didn't require any modification, but it looks like the rust toolchain script includes any untracked files to the PR, which is the root cause of the #3146 CI failure. Thus, I made the following changes (each one of them in its own commit): 1. Moved the upgrade step to its own script. 2. Added a bit of debugging and doc to the script. 3. Added a new step that cleans the workspace before the PR creation. 4. Actually update the toolchain. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .github/workflows/toolchain-upgrade.yml | 41 ++-------------- .gitignore | 4 ++ rust-toolchain.toml | 2 +- scripts/toolchain_update.sh | 65 +++++++++++++++++++++++++ 4 files changed, 75 insertions(+), 37 deletions(-) create mode 100755 scripts/toolchain_update.sh diff --git a/.github/workflows/toolchain-upgrade.yml b/.github/workflows/toolchain-upgrade.yml index 8252bfb826e6..a4b95ea195f0 100644 --- a/.github/workflows/toolchain-upgrade.yml +++ b/.github/workflows/toolchain-upgrade.yml @@ -30,42 +30,11 @@ jobs: env: GH_TOKEN: ${{ github.token }} run: | - current_toolchain_date=$(grep ^channel rust-toolchain.toml | sed 's/.*nightly-\(.*\)"/\1/') - echo "current_toolchain_date=$current_toolchain_date" >> $GITHUB_ENV - current_toolchain_epoch=$(date --date $current_toolchain_date +%s) - next_toolchain_date=$(date --date "@$(($current_toolchain_epoch + 86400))" +%Y-%m-%d) - echo "next_toolchain_date=$next_toolchain_date" >> $GITHUB_ENV - if gh issue list -S \ - "Toolchain upgrade to nightly-$next_toolchain_date failed" \ - --json number,title | grep title ; then - echo "next_step=none" >> $GITHUB_ENV - elif ! git ls-remote --exit-code origin toolchain-$next_toolchain_date ; then - echo "next_step=create_pr" >> $GITHUB_ENV - sed -i "/^channel/ s/$current_toolchain_date/$next_toolchain_date/" rust-toolchain.toml - git diff - git clone --filter=tree:0 https://github.com/rust-lang/rust rust.git - cd rust.git - current_toolchain_hash=$(curl https://static.rust-lang.org/dist/$current_toolchain_date/channel-rust-nightly-git-commit-hash.txt) - echo "current_toolchain_hash=$current_toolchain_hash" >> $GITHUB_ENV - next_toolchain_hash=$(curl https://static.rust-lang.org/dist/$next_toolchain_date/channel-rust-nightly-git-commit-hash.txt) - echo "next_toolchain_hash=$next_toolchain_hash" >> $GITHUB_ENV - EOF=$(dd if=/dev/urandom bs=15 count=1 status=none | base64) - echo "git_log<<$EOF" >> $GITHUB_ENV - git log --oneline $current_toolchain_hash..$next_toolchain_hash | \ - sed 's#^#https://github.com/rust-lang/rust/commit/#' >> $GITHUB_ENV - echo "$EOF" >> $GITHUB_ENV - cd .. - rm -rf rust.git - if ! cargo build-dev ; then - echo "next_step=create_issue" >> $GITHUB_ENV - else - if ! ./scripts/kani-regression.sh ; then - echo "next_step=create_issue" >> $GITHUB_ENV - fi - fi - else - echo "next_step=none" >> $GITHUB_ENV - fi + source scripts/toolchain_update.sh + + - name: Clean untracked files + run: git clean -f + - name: Create Pull Request if: ${{ env.next_step == 'create_pr' }} uses: peter-evans/create-pull-request@v6 diff --git a/.gitignore b/.gitignore index aae8f479aac9..a2defc0df119 100644 --- a/.gitignore +++ b/.gitignore @@ -48,6 +48,10 @@ no_llvm_build /tmp/ # Created by default with `src/ci/docker/run.sh` /obj/ +# Created by kani-compiler +*.rlib +*.rmeta +*.mir ## Temporary files *~ diff --git a/rust-toolchain.toml b/rust-toolchain.toml index be42da187e10..2d65b1576d5f 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-04-15" +channel = "nightly-2024-04-18" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/scripts/toolchain_update.sh b/scripts/toolchain_update.sh new file mode 100755 index 000000000000..856c346e542c --- /dev/null +++ b/scripts/toolchain_update.sh @@ -0,0 +1,65 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# This script is part of our CI nightly job to bump the toolchain version. +# It will potentially update the rust-toolchain.toml file, and run the +# regression. +# +# In order to manually run this script, you will need to do the following: +# +# 1. Set $GITHUB_ENV to point to an output file. +# 2. Install and configure GitHub CLI + +set -eu + +current_toolchain_date=$(grep ^channel rust-toolchain.toml | sed 's/.*nightly-\(.*\)"/\1/') +echo "current_toolchain_date=$current_toolchain_date" >> $GITHUB_ENV + +current_toolchain_epoch=$(date --date $current_toolchain_date +%s) +next_toolchain_date=$(date --date "@$(($current_toolchain_epoch + 86400))" +%Y-%m-%d) +echo "next_toolchain_date=$next_toolchain_date" >> $GITHUB_ENV + +echo "------ Start upgrade ------" +echo "- current: ${current_toolchain_date}" +echo "- next: ${next_toolchain_date}" +echo "---------------------------" + +if gh issue list -S \ + "Toolchain upgrade to nightly-$next_toolchain_date failed" \ + --json number,title | grep title +then + echo "Skip update: Found existing issue" + echo "next_step=none" >> $GITHUB_ENV +elif ! git ls-remote --exit-code origin toolchain-$next_toolchain_date +then + echo "next_step=create_pr" >> $GITHUB_ENV + + # Modify rust-toolchain file + sed -i "/^channel/ s/$current_toolchain_date/$next_toolchain_date/" rust-toolchain.toml + + git diff + git clone --filter=tree:0 https://github.com/rust-lang/rust rust.git + cd rust.git + current_toolchain_hash=$(curl https://static.rust-lang.org/dist/$current_toolchain_date/channel-rust-nightly-git-commit-hash.txt) + echo "current_toolchain_hash=$current_toolchain_hash" >> $GITHUB_ENV + + next_toolchain_hash=$(curl https://static.rust-lang.org/dist/$next_toolchain_date/channel-rust-nightly-git-commit-hash.txt) + echo "next_toolchain_hash=$next_toolchain_hash" >> $GITHUB_ENV + + EOF=$(dd if=/dev/urandom bs=15 count=1 status=none | base64) + echo "git_log<<$EOF" >> $GITHUB_ENV + + git log --oneline $current_toolchain_hash..$next_toolchain_hash | \ + sed 's#^#https://github.com/rust-lang/rust/commit/#' >> $GITHUB_ENV + echo "$EOF" >> $GITHUB_ENV + + cd .. + rm -rf rust.git + if ! ./scripts/kani-regression.sh ; then + echo "next_step=create_issue" >> $GITHUB_ENV + fi +else + echo "Skip update: Found existing branch" + echo "next_step=none" >> $GITHUB_ENV +fi From 72d03caa720a0f257a2ae1fe9d594eb2f7b02507 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Fri, 19 Apr 2024 09:47:32 +0200 Subject: [PATCH 07/15] Automatic toolchain upgrade to nightly-2024-04-19 (#3150) Update Rust toolchain from nightly-2024-04-18 to nightly-2024-04-19 without any other source changes. This is an automatically generated pull request. If any of the CI checks fail, manual intervention is required. In such a case, review the changes at https://github.com/rust-lang/rust from https://github.com/rust-lang/rust/commit/becebb3158149a115cad8a402612e25436a7e37b up to https://github.com/rust-lang/rust/commit/e3181b091e88321f5ea149afed6db0edf0a4f37b. --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 2d65b1576d5f..b1cbf7169fea 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-04-18" +channel = "nightly-2024-04-19" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] From c7067cf9dc35f48c6d1e7ac20ab2be107f3c4021 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 19 Apr 2024 13:41:28 -0700 Subject: [PATCH 08/15] Stabilize cover statement and update contracts RFC (#3091) I would like to propose that we stabilize the cover statement as is. Any further improvements or changes can be done separately, with or without an RFC. I am also updating the contracts RFC status since parts of it have been integrated to Kani, but it is still unstable. ### Call-out This PR requires at least 2 approvals. --- library/kani/src/mem.rs | 2 +- rfc/src/rfcs/0003-cover-statement.md | 12 ++++++++---- rfc/src/rfcs/0009-function-contracts.md | 7 ++++--- scripts/build-docs.sh | 4 +++- 4 files changed, 16 insertions(+), 9 deletions(-) diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs index 203eae2229c4..43062ebed6a1 100644 --- a/library/kani/src/mem.rs +++ b/library/kani/src/mem.rs @@ -44,7 +44,7 @@ use std::ptr::{DynMetadata, NonNull, Pointee}; /// Note that an unaligned pointer is still considered valid. /// /// TODO: Kani should automatically add those checks when a de-reference happens. -/// https://github.com/model-checking/kani/issues/2975 +/// /// /// This function will either panic or return `true`. This is to make it easier to use it in /// contracts. diff --git a/rfc/src/rfcs/0003-cover-statement.md b/rfc/src/rfcs/0003-cover-statement.md index 6839af22f929..de452654392b 100644 --- a/rfc/src/rfcs/0003-cover-statement.md +++ b/rfc/src/rfcs/0003-cover-statement.md @@ -1,8 +1,8 @@ - **Feature Name:** Cover statement (`cover-statement`) - **Feature Request Issue:** - **RFC PR:** -- **Status:** Unstable -- **Version:** 1 +- **Status:** Stable +- **Version:** 2 ------------------- @@ -138,8 +138,12 @@ However, if the condition can indeed be covered, verification would fail due to ## Open questions -Should we allow format arguments in the macro, e.g. `kani::cover!(x > y, "{} can be greater than {}", x, y)`? -Users may expect this to be supported since the macro looks similar to the `assert` macro, but Kani doesn't include the formatted string in the message description, since it's not available at compile time. +- ~Should we allow format arguments in the macro, e.g. `kani::cover!(x > y, "{} can be greater than {}", x, y)`? +Users may expect this to be supported since the macro looks similar to the `assert` macro, but Kani doesn't include the formatted string in the message description, since it's not available at compile time.~ + - For now, this macro will not accept format arguments, since this + is not well handled by Kani. + This is an extesion to this API that can be easily added later on if Kani + ever supports runtime formatting. ## Other Considerations diff --git a/rfc/src/rfcs/0009-function-contracts.md b/rfc/src/rfcs/0009-function-contracts.md index e26592080822..dae805a7db72 100644 --- a/rfc/src/rfcs/0009-function-contracts.md +++ b/rfc/src/rfcs/0009-function-contracts.md @@ -1,8 +1,8 @@ - **Feature Name:** Function Contracts - **Feature Request Issue:** [#2652](https://github.com/model-checking/kani/issues/2652) and [Milestone](https://github.com/model-checking/kani/milestone/31) - **RFC PR:** [#2620](https://github.com/model-checking/kani/pull/2620) -- **Status:** Under Review -- **Version:** 0 +- **Status:** Unstable +- **Version:** 1 - **Proof-of-concept:** [features/contracts](https://github.com/model-checking/kani/tree/features/contracts) - **Feature Gate:** `-Zfunction-contracts`, enforced by compile time error[^gate] @@ -893,4 +893,5 @@ times larger than what they expect the function will touch). [^stubcheck]: Kani cannot report the occurrence of a contract function to check in abstracted functions as errors, because the mechanism is needed to verify - mutually recursive functions. \ No newline at end of file + mutually recursive functions. + diff --git a/scripts/build-docs.sh b/scripts/build-docs.sh index cd40a2edabad..2e2c10b052f6 100755 --- a/scripts/build-docs.sh +++ b/scripts/build-docs.sh @@ -28,8 +28,10 @@ else curl -sSL -o "$FILE" "$URL" echo "$EXPECTED_HASH $FILE" | sha256sum -c - tar zxf $FILE + MDBOOK=${SCRIPT_DIR}/mdbook + else + MDBOOK=mdbook fi - MDBOOK=${SCRIPT_DIR}/mdbook fi KANI_DIR=$SCRIPT_DIR/.. From de6a255a232523357dbeae8490508e8fdd6947f2 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Mon, 22 Apr 2024 14:51:45 +0200 Subject: [PATCH 09/15] Automatic toolchain upgrade to nightly-2024-04-20 (#3154) Update Rust toolchain from nightly-2024-04-19 to nightly-2024-04-20 without any other source changes. This is an automatically generated pull request. If any of the CI checks fail, manual intervention is required. In such a case, review the changes at https://github.com/rust-lang/rust from https://github.com/rust-lang/rust/commit/e3181b091e88321f5ea149afed6db0edf0a4f37b up to https://github.com/rust-lang/rust/commit/f9b16149208c8a8a349c32813312716f6603eb6f. --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index b1cbf7169fea..f4634f5b7b43 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-04-19" +channel = "nightly-2024-04-20" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] From 9b297a36d6b80e5f09dbbf0183c44b6578d9273c Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 22 Apr 2024 13:24:51 +0000 Subject: [PATCH 10/15] Bump tests/perf/s2n-quic from `2d5e891` to `5f88e54` (#3140) Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `2d5e891` to `5f88e54`. --- 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 2d5e891f3fdc..5f88e5498215 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit 2d5e891f3fdc8a88b2d457baceedea5751efaa0d +Subproject commit 5f88e549821518e71b550faf353a8b9970a29deb From 4ee5eb5e55302d8cbbe8475c313af6862e2b891c Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Mon, 22 Apr 2024 17:07:41 +0200 Subject: [PATCH 11/15] Automatic cargo update to 2024-04-22 (#3157) Dependency upgrade resulting from `cargo update`. --- Cargo.lock | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 821dbd9c346c..6f45be0e419e 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -174,7 +174,7 @@ dependencies = [ "heck 0.5.0", "proc-macro2", "quote", - "syn 2.0.59", + "syn 2.0.60", ] [[package]] @@ -480,7 +480,7 @@ dependencies = [ "proc-macro-error", "proc-macro2", "quote", - "syn 2.0.59", + "syn 2.0.60", ] [[package]] @@ -860,9 +860,9 @@ checksum = "d626bb9dae77e28219937af045c257c28bfd3f69333c512553507f5f9798cb76" [[package]] name = "rustix" -version = "0.38.32" +version = "0.38.33" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "65e04861e65f21776e67888bfbea442b3642beaa0138fdb1dd7a84a52dffdb89" +checksum = "e3cc72858054fcff6d7dea32df2aeaee6a7c24227366d7ea429aada2f26b16ad" dependencies = [ "bitflags 2.5.0", "errno", @@ -924,7 +924,7 @@ checksum = "e88edab869b01783ba905e7d0153f9fc1a6505a96e4ad3018011eedb838566d9" dependencies = [ "proc-macro2", "quote", - "syn 2.0.59", + "syn 2.0.60", ] [[package]] @@ -1030,7 +1030,7 @@ dependencies = [ "proc-macro2", "quote", "rustversion", - "syn 2.0.59", + "syn 2.0.60", ] [[package]] @@ -1045,9 +1045,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.59" +version = "2.0.60" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4a6531ffc7b071655e4ce2e04bd464c4830bb585a61cabb96cf808f05172615a" +checksum = "909518bc7b1c9b779f1bbf07f2929d35af9f0f37e47c6e9ef7f9dddc1e1821f3" dependencies = [ "proc-macro2", "quote", @@ -1068,22 +1068,22 @@ dependencies = [ [[package]] name = "thiserror" -version = "1.0.58" +version = "1.0.59" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "03468839009160513471e86a034bb2c5c0e4baae3b43f79ffc55c4a5427b3297" +checksum = "f0126ad08bff79f29fc3ae6a55cc72352056dfff61e3ff8bb7129476d44b23aa" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "1.0.58" +version = "1.0.59" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c61f3ba182994efc43764a46c018c347bc492c79f024e705f46567b418f6d4f7" +checksum = "d1cd413b5d558b4c5bf3680e324a6fa5014e7b7c067a51e69dbdf47eb7148b66" dependencies = [ "proc-macro2", "quote", - "syn 2.0.59", + "syn 2.0.60", ] [[package]] @@ -1119,9 +1119,9 @@ dependencies = [ [[package]] name = "toml_edit" -version = "0.22.9" +version = "0.22.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8e40bb779c5187258fd7aad0eb68cb8706a0a81fa712fbea808ab43c4b8374c4" +checksum = "d3328d4f68a705b2a4498da1d580585d39a6510f98318a2cec3018a7ec61ddef" dependencies = [ "indexmap", "serde", @@ -1149,7 +1149,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" dependencies = [ "proc-macro2", "quote", - "syn 2.0.59", + "syn 2.0.60", ] [[package]] @@ -1471,5 +1471,5 @@ checksum = "9ce1b18ccd8e73a9321186f97e46f9f04b778851177567b1975109d26a08d2a6" dependencies = [ "proc-macro2", "quote", - "syn 2.0.59", + "syn 2.0.60", ] From 86d5f30f108a7db9894db1241cccba50b126a6d2 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Mon, 22 Apr 2024 15:39:21 +0000 Subject: [PATCH 12/15] Automatic toolchain upgrade to nightly-2024-04-21 (#3158) Update Rust toolchain from nightly-2024-04-20 to nightly-2024-04-21 without any other source changes. This is an automatically generated pull request. If any of the CI checks fail, manual intervention is required. In such a case, review the changes at https://github.com/rust-lang/rust from https://github.com/rust-lang/rust/commit/f9b16149208c8a8a349c32813312716f6603eb6f up to https://github.com/rust-lang/rust/commit/dbce3b43b6cb34dd3ba12c3ec6f708fe68e9c3df. --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index f4634f5b7b43..70848743b686 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-04-20" +channel = "nightly-2024-04-21" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] From 734f6817dc8846330c5717d6c4a7089c17f2dd28 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 22 Apr 2024 10:28:02 -0700 Subject: [PATCH 13/15] Bump tests/perf/s2n-quic from `5f88e54` to `9730578` (#3159) Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `5f88e54` to `9730578`.
Commits
  • 9730578 chore: release 1.37.0 (#2187)
  • b862ad9 s2n-quic-dc: initial commit (#2185)
  • e0f224b feat(s2n-quic-core): allow forced PTO transmissions (#2130)
  • bfb921d feat(s2n-quic-core): Add ability to create an incremental reader initialized ...
  • 23b07e4 feat(s2n-quic): allow disabling active connection migration support (#2182)
  • See full diff in compare view

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> --- 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 5f88e5498215..9730578c0d56 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit 5f88e549821518e71b550faf353a8b9970a29deb +Subproject commit 9730578c0d562d80bbbe663161b3a5408ed3116c From a4e69eb0b1f55387e8543d1f27493f3979028d76 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Date: Mon, 22 Apr 2024 19:45:21 -0400 Subject: [PATCH 14/15] Fix cargo audit error (#3160) Fixes cargo audit CI job by updating `rustix`. 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 | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 6f45be0e419e..627755fd91b3 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -860,9 +860,9 @@ checksum = "d626bb9dae77e28219937af045c257c28bfd3f69333c512553507f5f9798cb76" [[package]] name = "rustix" -version = "0.38.33" +version = "0.38.34" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e3cc72858054fcff6d7dea32df2aeaee6a7c24227366d7ea429aada2f26b16ad" +checksum = "70dc5ec042f7a43c4a73241207cecc9873a06d45debb38b329f8541d85c2730f" dependencies = [ "bitflags 2.5.0", "errno", From 180e10c54199240e0648252a497916020f5924e2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 23 Apr 2024 02:31:55 +0200 Subject: [PATCH 15/15] Fix cbmc-update CI job (#3156) We had a spurious update attempt logged in #3155 for the job prior to this fix would empty out the version strings. This was caused by use of undefined variables. Resolves: #3155 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- .github/workflows/cbmc-update.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/cbmc-update.yml b/.github/workflows/cbmc-update.yml index 6f9a6ae3a74b..5fe8a866c0e4 100644 --- a/.github/workflows/cbmc-update.yml +++ b/.github/workflows/cbmc-update.yml @@ -30,7 +30,7 @@ jobs: env: GH_TOKEN: ${{ github.token }} run: | - grep ^CBMC_VERSION kani-dependencies >> $GITHUB_ENV + grep ^CBMC_VERSION kani-dependencies | sed 's/"//g' >> $GITHUB_ENV CBMC_LATEST=$(gh -R diffblue/cbmc release list | grep Latest | awk '{print $1}' | cut -f2 -d-) echo "CBMC_LATEST=$CBMC_LATEST" >> $GITHUB_ENV # check whether the version has changed at all @@ -47,8 +47,8 @@ jobs: elif ! git ls-remote --exit-code origin cbmc-$CBMC_LATEST ; then CBMC_LATEST_MAJOR=$(echo $CBMC_LATEST | cut -f1 -d.) CBMC_LATEST_MINOR=$(echo $CBMC_LATEST | cut -f2 -d.) - sed -i "s/^CBMC_MAJOR=.*/CBMC_MAJOR=\"$CBMC_MAJOR\"/" kani-dependencies - sed -i "s/^CBMC_MINOR=.*/CBMC_MINOR=\"$CBMC_MINOR\"/" kani-dependencies + sed -i "s/^CBMC_MAJOR=.*/CBMC_MAJOR=\"$CBMC_LATEST_MAJOR\"/" kani-dependencies + sed -i "s/^CBMC_MINOR=.*/CBMC_MINOR=\"$CBMC_LATEST_MINOR\"/" kani-dependencies sed -i "s/^CBMC_VERSION=.*/CBMC_VERSION=\"$CBMC_LATEST\"/" kani-dependencies git diff if ! ./scripts/kani-regression.sh ; then