From 809ac4a276d128bc41993da28faa536422637358 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 26 Feb 2024 21:52:37 +0000 Subject: [PATCH 01/12] Update Rust toolchain to `nightly-2024-02-18` --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 42f6af899b43..d6965b24e190 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-02-17" +channel = "nightly-2024-02-18" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] From f1618834c055203a2806db9cb3a6eb3b5df9cbcf Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 26 Feb 2024 21:59:06 +0000 Subject: [PATCH 02/12] Change `join_codegen` to be infallible --- kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 810c5707aad4..cc217815c700 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -353,10 +353,10 @@ impl CodegenBackend for GotocCodegenBackend { ongoing_codegen: Box, _sess: &Session, _filenames: &OutputFilenames, - ) -> Result<(CodegenResults, FxIndexMap), ErrorGuaranteed> { + ) -> (CodegenResults, FxIndexMap) { match ongoing_codegen.downcast::<(CodegenResults, FxIndexMap)>() { - Ok(val) => Ok(*val), + Ok(val) => *val, Err(val) => panic!("unexpected error: {:?}", (*val).type_id()), } } From 43a05a2fdfbfe91683564dc0c66e5eba3e1f45ab Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 26 Feb 2024 22:00:17 +0000 Subject: [PATCH 03/12] Separate tests for `likely` and `unlikely` --- tests/kani/Intrinsics/Likely/main.rs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/tests/kani/Intrinsics/Likely/main.rs b/tests/kani/Intrinsics/Likely/main.rs index 524fbd18ddc8..14643241ef90 100644 --- a/tests/kani/Intrinsics/Likely/main.rs +++ b/tests/kani/Intrinsics/Likely/main.rs @@ -28,9 +28,15 @@ fn check_unlikely(x: i32, y: i32) { } #[kani::proof] -fn main() { +fn check_likely_main() { let x = kani::any(); let y = kani::any(); check_likely(x, y); +} + +#[kani::proof] +fn check_unlikely_main() { + let x = kani::any(); + let y = kani::any(); check_unlikely(x, y); } From 9e43394494a0a5205105bdbec2ba8234b3028f17 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 28 Feb 2024 15:18:04 +0000 Subject: [PATCH 04/12] Use trimmed name for intrinsics --- .../src/codegen_cprover_gotoc/codegen/intrinsic.rs | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index e497cfc6b47c..0696b00074a5 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -112,7 +112,7 @@ impl<'tcx> GotocCtx<'tcx> { place: &Place, span: Span, ) -> Stmt { - let intrinsic_sym = instance.mangled_name(); + let intrinsic_sym = instance.trimmed_name(); let intrinsic = intrinsic_sym.as_str(); let loc = self.codegen_span_stable(span); debug!(?instance, "codegen_intrinsic"); @@ -268,6 +268,12 @@ impl<'tcx> GotocCtx<'tcx> { }}; } + // If the intrinsic is defined on generic types, its trimmed name will + // include type arguments (e.g., `arith_offset::`). In that case, we + // remove them to simplify the match below. + let intrinsic_split = intrinsic.split_once("::"); + let intrinsic = if let Some((base_name, _type_args)) = intrinsic_split { base_name } else { intrinsic }; + if let Some(stripped) = intrinsic.strip_prefix("simd_shuffle") { assert!(fargs.len() == 3, "`simd_shuffle` had unexpected arguments {fargs:?}"); let n: u64 = self.simd_shuffle_length(stripped, farg_types, span); From cb9f559f99669c9ed3c21fb95205c9b4207d45c3 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 28 Feb 2024 15:32:45 +0000 Subject: [PATCH 05/12] fmt --- kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 0696b00074a5..70b05f931d19 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -272,7 +272,8 @@ impl<'tcx> GotocCtx<'tcx> { // include type arguments (e.g., `arith_offset::`). In that case, we // remove them to simplify the match below. let intrinsic_split = intrinsic.split_once("::"); - let intrinsic = if let Some((base_name, _type_args)) = intrinsic_split { base_name } else { intrinsic }; + let intrinsic = + if let Some((base_name, _type_args)) = intrinsic_split { base_name } else { intrinsic }; if let Some(stripped) = intrinsic.strip_prefix("simd_shuffle") { assert!(fargs.len() == 3, "`simd_shuffle` had unexpected arguments {fargs:?}"); From dff1482f42640cbe2adb1ef20cd77238fd3a8775 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 28 Feb 2024 15:44:40 +0000 Subject: [PATCH 06/12] Update to 02-25, remove erronous redundant imports --- cprover_bindings/src/goto_program/location.rs | 1 - cprover_bindings/src/goto_program/typ.rs | 1 - kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs | 1 - kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs | 1 - kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs | 1 - kani-compiler/src/kani_middle/metadata.rs | 1 - kani-compiler/src/kani_middle/provide.rs | 1 - kani-compiler/src/kani_middle/reachability.rs | 2 +- rust-toolchain.toml | 2 +- 9 files changed, 2 insertions(+), 9 deletions(-) diff --git a/cprover_bindings/src/goto_program/location.rs b/cprover_bindings/src/goto_program/location.rs index 79b123ad8b0e..4097d075276d 100644 --- a/cprover_bindings/src/goto_program/location.rs +++ b/cprover_bindings/src/goto_program/location.rs @@ -1,7 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT use crate::cbmc_string::{InternStringOption, InternedString}; -use std::convert::TryInto; use std::fmt::Debug; /// A `Location` represents a source location. diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs index dd07c150bb3f..da943b26ab19 100644 --- a/cprover_bindings/src/goto_program/typ.rs +++ b/cprover_bindings/src/goto_program/typ.rs @@ -7,7 +7,6 @@ use super::super::MachineModel; use super::{Expr, SymbolTable}; use crate::cbmc_string::InternedString; use std::collections::BTreeMap; -use std::convert::TryInto; use std::fmt::Debug; /////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index 68573cd2a1cd..cad3595bca50 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -22,7 +22,6 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::{Expr, Location, Stmt, Type}; use cbmc::InternedString; use stable_mir::ty::Span as SpanStable; -use std::convert::AsRef; use strum_macros::{AsRefStr, EnumString}; use tracing::debug; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index d4061d4271db..78c7e2b6cbd6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -12,7 +12,6 @@ use stable_mir::mir::{Body, Local}; use stable_mir::ty::{RigidTy, TyKind}; use stable_mir::CrateDef; use std::collections::BTreeMap; -use std::iter::FromIterator; use tracing::{debug, debug_span}; /// Codegen MIR functions into gotoc diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index cc217815c700..91e6c2538195 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -53,7 +53,6 @@ use std::ffi::OsString; use std::fmt::Write; use std::fs::File; use std::io::BufWriter; -use std::iter::FromIterator; use std::path::{Path, PathBuf}; use std::process::Command; use std::sync::{Arc, Mutex}; diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index 02f5da107556..9236de48308f 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -3,7 +3,6 @@ //! This module handles Kani metadata generation. For example, generating HarnessMetadata for a //! given function. -use std::default::Default; use std::path::Path; use crate::kani_middle::attributes::test_harness_name; diff --git a/kani-compiler/src/kani_middle/provide.rs b/kani-compiler/src/kani_middle/provide.rs index 70e046d6f9d6..d5495acb67a7 100644 --- a/kani-compiler/src/kani_middle/provide.rs +++ b/kani-compiler/src/kani_middle/provide.rs @@ -10,7 +10,6 @@ use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_ite use crate::kani_middle::stubbing; use crate::kani_queries::QueryDb; use rustc_hir::def_id::{DefId, LocalDefId}; -use rustc_interface; use rustc_middle::util::Providers; use rustc_middle::{mir::Body, query::queries, ty::TyCtxt}; use stable_mir::mir::mono::MonoItem; diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 63ed41bfd4c1..11ba57cb1cff 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -31,7 +31,7 @@ use stable_mir::mir::{ TerminatorKind, }; use stable_mir::ty::{Allocation, ClosureKind, ConstantKind, RigidTy, Ty, TyKind}; -use stable_mir::{self, CrateItem}; +use stable_mir::CrateItem; use stable_mir::{CrateDef, ItemKind}; use crate::kani_middle::coercion; diff --git a/rust-toolchain.toml b/rust-toolchain.toml index d6965b24e190..408b2e859604 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-02-18" +channel = "nightly-2024-02-25" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] From aceb134df827f575ced1d94191649661e22bd2c6 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 28 Feb 2024 15:58:45 +0000 Subject: [PATCH 07/12] Replace assumption failed source in expected output --- tests/expected/any_vec/exact_length.expected | 4 ++-- tests/expected/any_vec/out_bounds.expected | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/expected/any_vec/exact_length.expected b/tests/expected/any_vec/exact_length.expected index 93feecb214e5..f64d2830a7b8 100644 --- a/tests/expected/any_vec/exact_length.expected +++ b/tests/expected/any_vec/exact_length.expected @@ -1,12 +1,12 @@ Checking harness check_access_length_17... Failed Checks: assumption failed\ -in std::hint::assert_unchecked +in >::get_unchecked Checking harness check_access_length_zero... Failed Checks: assumption failed\ -in std::hint::assert_unchecked +in >::get_unchecked Verification failed for - check_access_length_17 Verification failed for - check_access_length_zero diff --git a/tests/expected/any_vec/out_bounds.expected b/tests/expected/any_vec/out_bounds.expected index 71132a64f67d..24121aee4ee8 100644 --- a/tests/expected/any_vec/out_bounds.expected +++ b/tests/expected/any_vec/out_bounds.expected @@ -1,6 +1,6 @@ Checking harness check_always_out_bounds... Failed Checks: assumption failed -in std::hint::assert_unchecked +in >::get_unchecked Verification failed for - check_always_out_bounds From 7e0cdc35e2fdf6421020cd6f76f5b60fb8f94b9e Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 28 Feb 2024 16:11:31 +0000 Subject: [PATCH 08/12] Remove redundant imports causing warnings --- kani-compiler/src/kani_compiler.rs | 4 +--- kani-driver/src/args/playback_args.rs | 2 -- tools/compiletest/src/runtest.rs | 1 - 3 files changed, 1 insertion(+), 6 deletions(-) diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 118821f5995f..48b4318db5bf 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -465,10 +465,8 @@ fn metadata_output_path(tcx: TyCtxt) -> PathBuf { #[cfg(test)] mod tests { use super::*; - use kani_metadata::{HarnessAttributes, HarnessMetadata}; + use kani_metadata::HarnessAttributes; use rustc_data_structures::fingerprint::Fingerprint; - use rustc_hir::definitions::DefPathHash; - use std::collections::HashMap; fn mock_next_harness_id() -> HarnessId { static mut COUNTER: u64 = 0; diff --git a/kani-driver/src/args/playback_args.rs b/kani-driver/src/args/playback_args.rs index bdad446a1158..ad82d9632a7a 100644 --- a/kani-driver/src/args/playback_args.rs +++ b/kani-driver/src/args/playback_args.rs @@ -100,8 +100,6 @@ impl ValidateArgs for PlaybackArgs { #[cfg(test)] mod tests { - use clap::Parser; - use super::*; #[test] diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index ee89c252dc4f..7925ed83e6e5 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -23,7 +23,6 @@ use std::process::{Command, ExitStatus, Output, Stdio}; use std::str; use serde::{Deserialize, Serialize}; -use serde_yaml; use tracing::*; use wait_timeout::ChildExt; From 9ea43ff6380a1226a40c9f99705c87be61a6dc21 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 28 Feb 2024 16:51:16 +0000 Subject: [PATCH 09/12] Remove import in bookrunner --- tools/bookrunner/librustdoc/html/markdown.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/tools/bookrunner/librustdoc/html/markdown.rs b/tools/bookrunner/librustdoc/html/markdown.rs index 1bcd5dad7532..3f827b77ff2b 100644 --- a/tools/bookrunner/librustdoc/html/markdown.rs +++ b/tools/bookrunner/librustdoc/html/markdown.rs @@ -7,7 +7,6 @@ use rustc_span::edition::Edition; -use std::default::Default; use std::str; use std::{borrow::Cow, marker::PhantomData}; From 5ecc28ee26dac9ce4bca9df08f7670798e6628fc Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 29 Feb 2024 16:16:29 +0000 Subject: [PATCH 10/12] Check for more than one separator --- .../codegen/intrinsic.rs | 22 ++++++++++++++----- 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 70b05f931d19..edf3fd34a93b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -268,12 +268,22 @@ impl<'tcx> GotocCtx<'tcx> { }}; } - // If the intrinsic is defined on generic types, its trimmed name will - // include type arguments (e.g., `arith_offset::`). In that case, we - // remove them to simplify the match below. - let intrinsic_split = intrinsic.split_once("::"); - let intrinsic = - if let Some((base_name, _type_args)) = intrinsic_split { base_name } else { intrinsic }; + /// Gets the basename of an intrinsic given its trimmed name. + /// + /// For example, given `arith_offset::` this returns `arith_offset`. + fn intrinsic_basename(name: &str) -> &str { + let scope_sep_count = name.matches("::").count(); + // We expect at most one `::` separator from trimmed intrinsic names + assert!( + scope_sep_count < 2, + "expected at most one `::` in intrinsic name, but found {scope_sep_count} in `{name}`" + ); + let name_split = name.split_once("::"); + if let Some((base_name, _type_args)) = name_split { base_name } else { name } + } + // The trimmed name includes type arguments if the intrinsic was defined + // on generic types, but we only need the basename for the match below. + let intrinsic = intrinsic_basename(intrinsic); if let Some(stripped) = intrinsic.strip_prefix("simd_shuffle") { assert!(fargs.len() == 3, "`simd_shuffle` had unexpected arguments {fargs:?}"); From 287eaf838d3917ebe1c08424d1b8477cd28aaf23 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 29 Feb 2024 20:39:48 +0000 Subject: [PATCH 11/12] Change `assert!` to `debug_assert!` --- kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index edf3fd34a93b..c185ca61d8d7 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -274,7 +274,7 @@ impl<'tcx> GotocCtx<'tcx> { fn intrinsic_basename(name: &str) -> &str { let scope_sep_count = name.matches("::").count(); // We expect at most one `::` separator from trimmed intrinsic names - assert!( + debug_assert!( scope_sep_count < 2, "expected at most one `::` in intrinsic name, but found {scope_sep_count} in `{name}`" ); From db1eb1c60005d1d9f2aa05dd39e4e3e01c2b5ffd Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 29 Feb 2024 21:31:13 +0000 Subject: [PATCH 12/12] Use `without_provenance_ptr` in `AtomicPtr` test --- tests/kani/Intrinsics/Atomic/Stable/AtomicPtr/main.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/kani/Intrinsics/Atomic/Stable/AtomicPtr/main.rs b/tests/kani/Intrinsics/Atomic/Stable/AtomicPtr/main.rs index c703c7c7125f..4e9d68619fd7 100644 --- a/tests/kani/Intrinsics/Atomic/Stable/AtomicPtr/main.rs +++ b/tests/kani/Intrinsics/Atomic/Stable/AtomicPtr/main.rs @@ -18,7 +18,7 @@ fn check_fetch_byte_add() { #[kani::proof] fn check_fetch_byte_sub() { - let atom = AtomicPtr::::new(core::ptr::invalid_mut(1)); + let atom = AtomicPtr::::new(core::ptr::without_provenance_mut(1)); assert_eq!(atom.fetch_byte_sub(1, Ordering::Relaxed).addr(), 1); assert_eq!(atom.load(Ordering::Relaxed).addr(), 0); }