model-checking · adpaco-aws · Feb 29, 2024 · Feb 26, 2024 · Feb 26, 2024 · Feb 26, 2024
@@ -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.

@@ -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;
 
 ///////////////////////////////////////////////////////////////////////////////////////////////

@@ -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;
 

@@ -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

@@ -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,13 @@ impl<'tcx> GotocCtx<'tcx> {
  }};
  }
 
  // If the intrinsic is defined on generic types, its trimmed name will
  // include type arguments (e.g., `arith_offset::<u8>`). 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);

@@ -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};
@@ -353,10 352,10 @@ impl CodegenBackend for GotocCodegenBackend {
  ongoing_codegen: Box<dyn Any>,
  _sess: &Session,
  _filenames: &OutputFilenames,
- ) -> Result<(CodegenResults, FxIndexMap<WorkProductId, WorkProduct>), ErrorGuaranteed> {
  ) -> (CodegenResults, FxIndexMap<WorkProductId, WorkProduct>) {
  match ongoing_codegen.downcast::<(CodegenResults, FxIndexMap<WorkProductId, WorkProduct>)>()
  {
- Ok(val) => Ok(*val),
  Ok(val) => *val,
  Err(val) => panic!("unexpected error: {:?}", (*val).type_id()),
  }
  }

@@ -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;

@@ -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;

@@ -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;

@@ -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;

@@ -100,8 100,6 @@ impl ValidateArgs for PlaybackArgs {
 
 #[cfg(test)]
 mod tests {
- use clap::Parser;
-
  use super::*;
 
  #[test]

@@ -2,5 2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-02-17"
 channel = "nightly-2024-02-25"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
@@ -1,12 1,12 @@
 Checking harness check_access_length_17...
 
 Failed Checks: assumption failed\
-in std::hint::assert_unchecked
 in <usize as std::slice::SliceIndex<[u8]>>::get_unchecked
 
 Checking harness check_access_length_zero...
 
 Failed Checks: assumption failed\
-in std::hint::assert_unchecked
 in <usize as std::slice::SliceIndex<[u8]>>::get_unchecked
 
 Verification failed for - check_access_length_17
 Verification failed for - check_access_length_zero
@@ -1,6 1,6 @@
 Checking harness check_always_out_bounds...
 
 Failed Checks: assumption failed
-in std::hint::assert_unchecked
 in <usize as std::slice::SliceIndex<[u8]>>::get_unchecked
 
 Verification failed for - check_always_out_bounds
@@ -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);
 }
@@ -7,7 7,6 @@
 
 use rustc_span::edition::Edition;
 
-use std::default::Default;
 use std::str;
 use std::{borrow::Cow, marker::PhantomData};
 

@@ -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;