Don't crash benchcomp when rounding non-numeric values

Cargo.lock

@@ -169,7 +169,7 @@ dependencies = [
  "heck 0.5.0",
  "proc-macro2",
  "quote",
- "syn 2.0.65",
+ "syn 2.0.66",
 ]
 
 [[package]]
@@ -481,7 +481,7 @@ dependencies = [
  "proc-macro-error",
  "proc-macro2",
  "quote",
- "syn 2.0.65",
+ "syn 2.0.66",
 ]
 
 [[package]]
@@ -667,9 +667,9 @@ checksum = "b15813163c1d831bf4a13c3610c05c0d03b39feb07f7e09fa234dac9b15aaf39"
 
 [[package]]
 name = "parking_lot"
-version = "0.12.2"
+version = "0.12.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7e4af0ca4f6caed20e900d564c242b8e5d4903fdacf31d3daf527b66fe6f42fb"
+checksum = "f1bf18183cf54e8d6059647fc3063646a1801cf30896933ec2311622cc4b9a27"
 dependencies = [
  "lock_api",
  "parking_lot_core",
@@ -732,9 +732,9 @@ dependencies = [
 
 [[package]]
 name = "proc-macro2"
-version = "1.0.83"
+version = "1.0.84"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0b33eb56c327dec362a9e55b3ad14f9d2f0904fb5a5b03b513ab5465399e9f43"
+checksum = "ec96c6a92621310b51366f1e28d05ef11489516e93be030060e5fc12024a49d6"
 dependencies = [
  "unicode-ident",
 ]
@@ -908,22 +908,22 @@ dependencies = [
 
 [[package]]
 name = "serde"
-version = "1.0.202"
+version = "1.0.203"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "226b61a0d411b2ba5ff6d7f73a476ac4f8bb900373459cd00fab8512828ba395"
+checksum = "7253ab4de971e72fb7be983802300c30b5a7f0c2e56fab8abfc6a214307c0094"
 dependencies = [
  "serde_derive",
 ]
 
 [[package]]
 name = "serde_derive"
-version = "1.0.202"
+version = "1.0.203"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6048858004bcff69094cd972ed40a32500f153bd3be9f716b2eed2e8217c4838"
+checksum = "500cbc0ebeb6f46627f50f3f5811ccf6bf00643be300b4c3eabc0ef55dc5b5ba"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.65",
+ "syn 2.0.66",
 ]
 
 [[package]]
@@ -1029,7 +1029,7 @@ dependencies = [
  "proc-macro2",
  "quote",
  "rustversion",
- "syn 2.0.65",
+ "syn 2.0.66",
 ]
 
 [[package]]
@@ -1044,9 +1044,9 @@ dependencies = [
 
 [[package]]
 name = "syn"
-version = "2.0.65"
+version = "2.0.66"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d2863d96a84c6439701d7a38f9de935ec562c8832cc55d1dde0f513b52fad106"
+checksum = "c42f3f41a2de00b01c0aaad383c5a45241efc8b2d1eda5661812fda5f3cdcff5"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -1082,7 +1082,7 @@ checksum = "46c3384250002a6d5af4d114f2845d37b57521033f30d5c3f46c4d70e1197533"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.65",
+ "syn 2.0.66",
 ]
 
 [[package]]
@@ -1148,7 +1148,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.65",
+ "syn 2.0.66",
 ]
 
 [[package]]
@@ -1413,5 +1413,5 @@ checksum = "15e934569e47891f7d9411f1a451d947a60e000ab3bd24fbb970f000387d1b3b"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.65",
+ "syn 2.0.66",
 ]

cprover_bindings/src/goto_program/expr.rs

@@ -1055,6 +1055,7 @@ impl Expr {
     ///     <https://github.com/rust-lang/rfcs/blob/master/text/1199-simd-infrastructure.md#comparisons>).
     ///     The signedness doesn't matter, as the result for each element is
     ///     either "all ones" (true) or "all zeros" (false).
+    ///
     /// For example, one can use `simd_eq` on two `f64x4` vectors and assign the
     /// result to a `u64x4` vector. But it's not possible to assign it to: (1) a
     /// `u64x2` because they don't have the same length; or (2) another `f64x4`
@@ -1665,7 +1666,7 @@ impl Expr {
                         continue;
                     }
                     let name = field.name();
-                    exprs.insert(name, self.clone().member(&name.to_string(), symbol_table));
+                    exprs.insert(name, self.clone().member(name.to_string(), symbol_table));
                 }
             }
         }

cprover_bindings/src/irep/goto_binary_serde.rs

@@ -78,11 +78,9 @@ pub fn read_goto_binary_file(filename: &Path) -> io::Result<()> {
 /// [NumberedIrep] from its unique number.
 ///
 /// In practice:
-/// - the forward directon from [IrepKey] to unique numbers is
-/// implemented using a `HashMap<IrepKey,usize>`
-/// - the inverse direction from unique numbers to [NumberedIrep] is implemented
-/// using a `Vec<NumberedIrep>` called the `index` that stores [NumberedIrep]
-/// under their unique number.
+/// - the forward directon from [IrepKey] to unique numbers is implemented using a `HashMap<IrepKey,usize>`
+/// - the inverse direction from unique numbers to [NumberedIrep] is implemented usign a `Vec<NumberedIrep>`
+///   called the `index` that stores [NumberedIrep] under their unique number.
 ///
 /// Earlier we said that an [NumberedIrep] is conceptually a pair formed of
 /// an [IrepKey] and its unique number. It is represented using only

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -204,7 +204,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let body = self.transformer.body(self.tcx, instance);
         self.set_current_fn(instance, &body);
         debug!(krate=?instance.def.krate(), is_std=self.current_fn().is_std(), "declare_function");
-        self.ensure(&self.symbol_name_stable(instance), |ctx, fname| {
+        self.ensure(self.symbol_name_stable(instance), |ctx, fname| {
             Symbol::function(
                 fname,
                 ctx.fn_typ(instance, &body),

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -871,6 +871,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// its primary argument and returns a tuple that contains:
     ///  * the previous value
     ///  * a boolean value indicating whether the operation was successful or not
+    ///
     /// In a sequential context, the update is always sucessful so we assume the
     /// second value to be true.
     /// -------------------------
@@ -955,9 +956,10 @@ impl<'tcx> GotocCtx<'tcx> {
     ///  * Both `src`/`dst` must be valid for reads/writes of `count *
     ///      size_of::<T>()` bytes (done by calls to `memmove`)
     ///  * (Exclusive to nonoverlapping copy) The region of memory beginning
-    ///      at `src` with a size of `count * size_of::<T>()` bytes must *not*
-    ///      overlap with the region of memory beginning at `dst` with the same
-    ///      size.
+    ///    at `src` with a size of `count * size_of::<T>()` bytes must *not*
+    ///    overlap with the region of memory beginning at `dst` with the same
+    ///    size.
+    ///
     /// In addition, we check that computing `count` in bytes (i.e., the third
     /// argument of the copy built-in call) would not overflow.
     pub fn codegen_copy(
@@ -1834,7 +1836,7 @@ impl<'tcx> GotocCtx<'tcx> {
     ///
     /// TODO: Add a check for the condition:
     ///  * `src` must point to a properly initialized value of type `T`
-    /// See <https://github.com/model-checking/kani/issues/920> for more details
+    ///    See <https://github.com/model-checking/kani/issues/920> for more details
     fn codegen_volatile_load(
         &mut self,
         mut fargs: Vec<Expr>,
@@ -1894,6 +1896,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Undefined behavior if any of these conditions are violated:
     ///  * `dst` must be valid for writes (done by memset writable check)
     ///  * `dst` must be properly aligned (done by `align_check` below)
+    ///
     /// In addition, we check that computing `bytes` (i.e., the third argument
     /// for the `memset` call) would not overflow
     fn codegen_write_bytes(

kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

@@ -393,7 +393,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// Generate a goto expression for a pointer to a static or thread-local variable.
     fn codegen_instance_pointer(&mut self, instance: Instance, is_thread_local: bool) -> Expr {
-        let sym = self.ensure(&instance.mangled_name(), |ctx, name| {
+        let sym = self.ensure(instance.mangled_name(), |ctx, name| {
             // Rust has a notion of "extern static" variables. These are in an "extern" block,
             // and so aren't initialized in the current codegen unit. For example (from std):
             //      extern "C" {

kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

@@ -333,8 +333,9 @@ impl<'tcx> GotocCtx<'tcx> {
     ///      assert!(v.0 == [1, 2]); // refers to the entire array
     ///    }
     /// ```
-    /// * Note that projection inside SIMD structs may eventually become illegal.
-    /// See <https://github.com/rust-lang/stdarch/pull/1422#discussion_r1176415609> thread.
+    ///
+    /// Note that projection inside SIMD structs may eventually become illegal.
+    /// See thread <https://github.com/rust-lang/stdarch/pull/1422#discussion_r1176415609>.
     ///
     /// Since the goto representation for both is the same, we use the expected type to decide
     /// what to return.

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

@@ -73,7 +73,7 @@ impl TypeExt for Type {
                     && components.iter().any(|x| x.name() == "vtable" && x.typ().is_pointer())
             }
             Type::StructTag(tag) => {
-                st.lookup(&tag.to_string()).unwrap().typ.is_rust_trait_fat_ptr(st)
+                st.lookup(tag.to_string()).unwrap().typ.is_rust_trait_fat_ptr(st)
             }
             _ => false,
         }
@@ -1140,7 +1140,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Mapping enums to CBMC types is rather complicated. There are a few cases to consider:
     /// 1. When there is only 0 or 1 variant, this is straightforward as the code shows
     /// 2. When there are more variants, rust might decides to apply the typical encoding which
-    /// regard enums as tagged union, or an optimized form, called niche encoding.
+    ///    regard enums as tagged union, or an optimized form, called niche encoding.
     ///
     /// The direct encoding is straightforward. Enums are just mapped to C as a struct of union of structs.
     /// e.g.

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -11,6 +11,7 @@
 //! This file is for defining the data-structure itself.
 //!   1. Defines `GotocCtx<'tcx>`
 //!   2. Provides constructors, getters and setters for the context.
+//!
 //! Any MIR specific functionality (e.g. codegen etc) should live in specialized files that use
 //! this structure as input.
 use super::current_fn::CurrentFnCtx;

kani-compiler/src/kani_compiler.rs

@@ -110,9 +110,10 @@ struct CrateInfo {
 ///      compilation. The crate metadata is stored here (even if no codegen was actually performed).
 ///    - [CompilationStage::CompilationSkipped] no compilation was actually performed.
 ///      No work needs to be done.
-/// - Note: In a scenario where the compilation fails, the compiler will exit immediately,
-///  independent on the stage. Any artifact produced shouldn't be used.
-/// I.e.:
+///
+/// Note: In a scenario where the compilation fails, the compiler will exit immediately,
+/// independent on the stage. Any artifact produced shouldn't be used. I.e.:
+///
 /// ```dot
 /// graph CompilationStage {
 ///   Init -> {CodegenNoStubs, CompilationSkipped}

kani-compiler/src/kani_middle/reachability.rs

@@ -303,7 +303,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
 /// 1. Every function / method / closures that may be directly invoked.
 /// 2. Every function / method / closures that may have their address taken.
 /// 3. Every method that compose the impl of a trait for a given type when there's a conversion
-/// from the type to the trait.
+///    from the type to the trait.
 ///    - I.e.: If we visit the following code:
 ///      ```
 ///      let var = MyType::new();
@@ -313,7 +313,8 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
 /// 4. Every Static variable that is referenced in the function or constant used in the function.
 /// 5. Drop glue.
 /// 6. Static Initialization
-/// This code has been mostly taken from `rustc_monomorphize::collector::MirNeighborCollector`.
+///
+/// Remark: This code has been mostly taken from `rustc_monomorphize::collector::MirNeighborCollector`.
 impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
     /// Collect the following:
     /// - Trait implementations when casting from concrete to dyn Trait.

kani-driver/src/args_toml.rs

@@ -90,8 +90,11 @@ fn cargo_locate_project(input_args: &[OsString]) -> Result<PathBuf> {
 /// We currently support the following entries:
 /// - flags: Flags that get directly passed to Kani.
 /// - unstable: Unstable features (it will be passed using `-Z` flag).
+///
 /// The tables supported are:
-/// "workspace.metadata.kani", "package.metadata.kani", "kani"
+/// - "workspace.metadata.kani"
+/// - "package.metadata.kani"
+/// - "kani"
 fn toml_to_args(tomldata: &str) -> Result<(Vec<OsString>, Vec<OsString>)> {
     let config = tomldata.parse::<Value>()?;
     // To make testing easier, our function contract is to produce a stable ordering of flags for a given input.

kani-driver/src/call_cargo.rs

@@ -112,7 +112,7 @@ impl KaniSession {
                 let mut cmd = setup_cargo_command()?;
                 cmd.args(&cargo_args)
                     .args(vec!["-p", &package.name])
-                    .args(&verification_target.to_args())
+                    .args(verification_target.to_args())
                     .args(&pkg_args)
                     .env("RUSTC", &self.kani_compiler)
                     // Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See
@@ -315,13 +315,16 @@ fn validate_package_names(package_names: &[String], packages: &[Package]) -> Res
 }
 
 /// Extract the packages that should be verified.
-/// If `--package <pkg>` is given, return the list of packages selected.
-/// If `--exclude <pkg>` is given, return the list of packages not excluded.
-/// If `--workspace` is given, return the list of workspace members.
-/// If no argument provided, return the root package if there's one or all members.
+///
+/// The result is build following these rules:
+/// - If `--package <pkg>` is given, return the list of packages selected.
+/// - If `--exclude <pkg>` is given, return the list of packages not excluded.
+/// - If `--workspace` is given, return the list of workspace members.
+/// - If no argument provided, return the root package if there's one or all members.
 ///   - I.e.: Do whatever cargo does when there's no `default_members`.
 ///   - This is because `default_members` is not available in cargo metadata.
 ///     See <https://github.com/rust-lang/cargo/issues/8033>.
+///
 /// In addition, if either `--package <pkg>` or `--exclude <pkg>` is given,
 /// validate that `<pkg>` is a package name in the workspace, or return an error
 /// otherwise.

kani-driver/src/cbmc_property_renderer.rs

@@ -700,6 +700,7 @@ fn update_properties_with_reach_status(
 /// Update the results of `code_coverage` (NOT `cover`) properties.
 /// - `SUCCESS` -> `UNCOVERED`
 /// - `FAILURE` -> `COVERED`
+///
 /// Note that these statuses are intermediate statuses that aren't reported to
 /// users but rather internally consumed and reported finally as `PARTIAL`, `FULL`
 /// or `NONE` based on aggregated line coverage results.
@@ -720,9 +721,10 @@ fn update_results_of_code_covererage_checks(mut properties: Vec<Property>) -> Ve
 
 /// Update the results of cover properties.
 /// We encode cover(cond) as assert(!cond), so if the assertion
-/// fails, then the cover property is satisfied and vice versa.
+/// fails, then the cover property is satisfied and vice versa:
 /// - SUCCESS -> UNSATISFIABLE
 /// - FAILURE -> SATISFIED
+///
 /// Note that if the cover property was unreachable, its status at this point
 /// will be `CheckStatus::Unreachable` and not `CheckStatus::Success` since
 /// `update_properties_with_reach_status` is called beforehand

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-05-17"
+channel = "nightly-2024-05-23"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

scripts/setup/ubuntu/install_deps.sh

@@ -16,6 +16,7 @@ DEPS=(
   gpg-agent
   jq
   libssl-dev
+  lld
   lsb-release
   make
   ninja-build

tests/script-based-pre/build-rs-conditional/Cargo.toml

@@ -7,3 +7,5 @@ edition = "2021"
 
 [dependencies]
 
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }

tests/script-based-pre/cargo_playback_build/sample_crate/Cargo.toml

@@ -4,3 +4,6 @@
 name = "sample_crate"
 version = "0.1.0"
 edition = "2021"
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }

tests/script-based-pre/cargo_playback_opts/sample_crate/Cargo.toml

@@ -4,3 +4,6 @@
 name = "sample_crate"
 version = "0.1.0"
 edition = "2021"
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }

tests/script-based-pre/cargo_playback_target/sample_crate/Cargo.toml

@@ -15,3 +15,5 @@ doctest = false
 name = "bar"
 doctest = false
 
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }

tests/script-based-pre/concrete_playback_e2e/sample_crate/Cargo.toml

@@ -10,3 +10,6 @@ concrete-playback = "inplace"
 
 [package.metadata.kani.unstable]
 concrete-playback = true
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }