diff --git a/.github/workflows/audit.yml b/.github/workflows/audit.yml index bf852429459c..3ae9d192f376 100644 --- a/.github/workflows/audit.yml +++ b/.github/workflows/audit.yml @@ -16,7 +16,7 @@ jobs: audit: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - uses: EmbarkStudios/cargo-deny-action@v1 with: arguments: --all-features --workspace diff --git a/.github/workflows/bench.yml b/.github/workflows/bench.yml index 615a8ff6c0aa..ad0bbf81f2c2 100644 --- a/.github/workflows/bench.yml +++ b/.github/workflows/bench.yml @@ -30,14 +30,14 @@ jobs: echo "NEW_REF=${{ github.event.pull_request.head.sha }}" | tee -a "$GITHUB_ENV" - name: Check out Kani (old variant) - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: path: ./old ref: ${{ env.OLD_REF }} fetch-depth: 2 - name: Check out Kani (new variant) - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: path: ./new ref: ${{ env.NEW_REF }} diff --git a/.github/workflows/cbmc-latest.yml b/.github/workflows/cbmc-latest.yml index 287215e554b7..9cb8082ae4b7 100644 --- a/.github/workflows/cbmc-latest.yml +++ b/.github/workflows/cbmc-latest.yml @@ -22,7 +22,7 @@ jobs: os: [macos-12, ubuntu-20.04, ubuntu-22.04] steps: - name: Checkout Kani under "kani" - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: path: kani @@ -37,7 +37,7 @@ jobs: run: cargo build-dev - name: Checkout CBMC under "cbmc" - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: repository: diffblue/cbmc path: cbmc @@ -58,7 +58,7 @@ jobs: runs-on: ubuntu-20.04 steps: - name: Checkout Kani under "kani" - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: path: kani @@ -73,7 +73,7 @@ jobs: run: cargo build-dev -- --release - name: Checkout CBMC under "cbmc" - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: repository: diffblue/cbmc path: cbmc diff --git a/.github/workflows/cbmc-update.yml b/.github/workflows/cbmc-update.yml index 3b8d6cbcd37e..e5f33e935e09 100644 --- a/.github/workflows/cbmc-update.yml +++ b/.github/workflows/cbmc-update.yml @@ -19,7 +19,7 @@ jobs: runs-on: ubuntu-22.04 steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup diff --git a/.github/workflows/extra_jobs.yml b/.github/workflows/extra_jobs.yml index d4da80fbe132..45ca6968c4ba 100644 --- a/.github/workflows/extra_jobs.yml +++ b/.github/workflows/extra_jobs.yml @@ -33,7 +33,7 @@ jobs: runs-on: ubuntu-latest steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Label PR id: labeler diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml index 6a8267b09231..5ab7dcb1b9c3 100644 --- a/.github/workflows/format-check.yml +++ b/.github/workflows/format-check.yml @@ -14,7 +14,7 @@ jobs: runs-on: ubuntu-latest steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Execute copyright check run: ./scripts/ci/run-copyright-check.sh @@ -33,7 +33,7 @@ jobs: runs-on: ubuntu-20.04 steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup diff --git a/.github/workflows/kani-m1.yml b/.github/workflows/kani-m1.yml index e9f973c82919..36f2b615c4aa 100644 --- a/.github/workflows/kani-m1.yml +++ b/.github/workflows/kani-m1.yml @@ -16,7 +16,7 @@ jobs: runs-on: macos-13-xlarge steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index a22ed971ec12..e866eaf635de 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -20,7 +20,7 @@ jobs: os: [macos-12, ubuntu-20.04, ubuntu-22.04] steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup @@ -37,7 +37,7 @@ jobs: runs-on: ubuntu-20.04 steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup @@ -58,7 +58,7 @@ jobs: runs-on: ubuntu-20.04 steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Install benchcomp dependencies run: | @@ -81,7 +81,7 @@ jobs: runs-on: ubuntu-20.04 steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup @@ -102,7 +102,7 @@ jobs: contents: write steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 22ffa75d4d39..e753320c158f 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -30,7 +30,7 @@ jobs: crate_version: ${{ steps.bundle.outputs.crate_version }} steps: - name: Checkout code - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup @@ -135,7 +135,7 @@ jobs: cargo kani setup --use-local-bundle ./${{ matrix.prev_job.bundle }} - name: Checkout tests - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Run tests # TODO: Customize compiletest to run custom kani. For now, just run a few cargo kani tests. @@ -160,7 +160,7 @@ jobs: KANI_SRC: ./kani_src steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: path: ${{ env.KANI_SRC }} @@ -204,7 +204,7 @@ jobs: upload_url: ${{ steps.create_release.outputs.upload_url }} steps: - name: Checkout code - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Get version run: | @@ -258,7 +258,7 @@ jobs: target: x86_64-unknown-linux-gnu steps: - name: Checkout code - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup @@ -271,7 +271,7 @@ jobs: cargo package -p kani-verifier - name: 'Login to GitHub Container Registry' - uses: docker/login-action@v2 + uses: docker/login-action@v3 with: registry: ghcr.io username: ${{ github.repository_owner }} @@ -284,7 +284,7 @@ jobs: OWNER: '${{ github.repository_owner }}' - name: Build and push - uses: docker/build-push-action@v3 + uses: docker/build-push-action@v5 with: context: . file: scripts/ci/Dockerfile.bundle-release-20-04 diff --git a/.github/workflows/slow-tests.yml b/.github/workflows/slow-tests.yml index 2c0a4acd9564..b177b6d5f400 100644 --- a/.github/workflows/slow-tests.yml +++ b/.github/workflows/slow-tests.yml @@ -21,7 +21,7 @@ jobs: os: [macos-12, ubuntu-20.04, ubuntu-22.04] steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup diff --git a/.github/workflows/toolchain-upgrade.yml b/.github/workflows/toolchain-upgrade.yml index 8d54ebe189ff..32266375cb5f 100644 --- a/.github/workflows/toolchain-upgrade.yml +++ b/.github/workflows/toolchain-upgrade.yml @@ -19,7 +19,7 @@ jobs: runs-on: ubuntu-22.04 steps: - name: Checkout Kani - uses: actions/checkout@v3 + uses: actions/checkout@v4 - name: Setup Kani Dependencies uses: ./.github/actions/setup diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 5d60f15f69a5..11e4721dfb31 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -1729,7 +1729,7 @@ impl<'tcx> GotocCtx<'tcx> { // [u32; n]: translated wrapped in a struct let indexes = fargs.remove(0); - let (_, vec_subtype) = rust_arg_types[0].simd_size_and_type(self.tcx); + let (in_type_len, vec_subtype) = rust_arg_types[0].simd_size_and_type(self.tcx); let (ret_type_len, ret_type_subtype) = rust_ret_type.simd_size_and_type(self.tcx); if ret_type_len != n { let err_msg = format!( @@ -1749,7 +1749,7 @@ impl<'tcx> GotocCtx<'tcx> { // An unsigned type here causes an invariant violation in CBMC. // Issue: https://github.com/diffblue/cbmc/issues/6298 let st_rep = Type::ssize_t(); - let n_rep = Expr::int_constant(n, st_rep.clone()); + let n_rep = Expr::int_constant(in_type_len, st_rep.clone()); // P = indexes.expanded_map(v -> if v < N then vec1[v] else vec2[v-N]) let elems = (0..n) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index d297d9d90a52..59a18348d582 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -421,7 +421,8 @@ impl<'tcx> GotocCtx<'tcx> { } (Scalar::Ptr(ptr, _size), _) => { let res_t = self.codegen_ty(ty); - let (alloc_id, offset) = ptr.into_parts(); + let (prov, offset) = ptr.into_parts(); + let alloc_id = prov.alloc_id(); self.codegen_alloc_pointer(res_t, alloc_id, offset, span) } _ => unimplemented!(), @@ -646,7 +647,8 @@ impl<'tcx> GotocCtx<'tcx> { Size::from_bytes(self.symbol_table.machine_model().pointer_width_in_bytes()); let mut next_offset = Size::ZERO; - for &(offset, alloc_id) in alloc.provenance().ptrs().iter() { + for &(offset, prov) in alloc.provenance().ptrs().iter() { + let alloc_id = prov.alloc_id(); if offset > next_offset { let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter( next_offset.bytes_usize()..offset.bytes_usize(), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index c781f272fb2d..8ded0b7f421a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -11,7 +11,7 @@ use crate::kani_middle::coercion::{ }; use crate::unwrap_or_return_codegen_unimplemented; use cbmc::goto_program::{ - arithmetic_overflow_result_type, BinaryOperator, Expr, Location, Stmt, Symbol, Type, + arithmetic_overflow_result_type, BinaryOperator, Expr, Location, Stmt, Type, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD, }; use cbmc::MachineModel; @@ -1169,7 +1169,7 @@ impl<'tcx> GotocCtx<'tcx> { idx: usize, ) -> Expr { debug!(?instance, typ=?t, %idx, "codegen_vtable_method_field"); - let vtable_field_name = self.vtable_field_name(instance.def_id(), idx); + let vtable_field_name = self.vtable_field_name(idx); let vtable_type = Type::struct_tag(self.vtable_name(t)); let field_type = vtable_type.lookup_field_type(vtable_field_name, &self.symbol_table).unwrap(); @@ -1232,34 +1232,10 @@ impl<'tcx> GotocCtx<'tcx> { .address_of() .cast_to(trait_fn_ty) } else { - // We skip an entire submodule of the standard library, so drop is missing - // for it. Build and insert a function that just calls an unimplemented block - // to maintain soundness. - let drop_sym_name = format!("drop_unimplemented_{}", self.symbol_name(drop_instance)); - let pretty_name = - format!("drop_unimplemented<{}>", self.readable_instance_name(drop_instance)); - let drop_sym = self.ensure(&drop_sym_name, |ctx, name| { - // Function body - let unimplemented = ctx.codegen_unimplemented_stmt( - format!("drop_in_place for {drop_instance}").as_str(), - Location::none(), - "https://github.com/model-checking/kani/issues/281", - ); - - // Declare symbol for the single, self parameter - let param_typ = ctx.codegen_ty(trait_ty).to_pointer(); - let param_sym = ctx.gen_function_parameter(0, &drop_sym_name, param_typ); - - // Build and insert the function itself - Symbol::function( - name, - Type::code(vec![param_sym.to_function_parameter()], Type::empty()), - Some(Stmt::block(vec![unimplemented], Location::none())), - pretty_name, - Location::none(), - ) - }); - drop_sym.to_expr().address_of().cast_to(trait_fn_ty) + unreachable!( + "Missing drop implementation for {}", + self.readable_instance_name(drop_instance) + ); } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs index 9f88bbbe7b55..3fbfd3629775 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs @@ -5,9 +5,10 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::Location; -use rustc_middle::mir::{Local, VarDebugInfo, VarDebugInfoContents}; +use rustc_middle::mir::{Local, VarDebugInfoContents}; use rustc_smir::rustc_internal; use rustc_span::Span; +use stable_mir::mir::VarDebugInfo; impl<'tcx> GotocCtx<'tcx> { pub fn codegen_span(&self, sp: &Span) -> Location { @@ -43,10 +44,12 @@ impl<'tcx> GotocCtx<'tcx> { sp.map_or(Location::none(), |x| self.codegen_span(&x)) } - pub fn find_debug_info(&self, l: &Local) -> Option<&VarDebugInfo<'tcx>> { - self.current_fn().mir().var_debug_info.iter().find(|info| match info.value { - VarDebugInfoContents::Place(p) => p.local == *l && p.projection.len() == 0, - VarDebugInfoContents::Const(_) => false, - }) + pub fn find_debug_info(&self, l: &Local) -> Option { + rustc_internal::stable(self.current_fn().mir().var_debug_info.iter().find(|info| { + match info.value { + VarDebugInfoContents::Place(p) => p.local == *l && p.projection.len() == 0, + VarDebugInfoContents::Const(_) => false, + } + })) } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index a4597885716a..d673c7d37c83 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -6,7 +6,6 @@ use super::PropertyClass; use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::{Expr, Location, Stmt, Type}; -use rustc_hir::def_id::DefId; use rustc_middle::mir; use rustc_middle::mir::{ AssertKind, BasicBlock, NonDivergingIntrinsic, Operand, Place, Statement, StatementKind, @@ -541,16 +540,9 @@ impl<'tcx> GotocCtx<'tcx> { return Stmt::goto(self.current_fn().find_label(&target.unwrap()), loc); } // Handle a virtual function call via a vtable lookup - InstanceDef::Virtual(def_id, idx) => { + InstanceDef::Virtual(_, idx) => { let self_ty = self.operand_ty(&args[0]); - self.codegen_virtual_funcall( - self_ty, - def_id, - idx, - destination, - &mut fargs, - loc, - ) + self.codegen_virtual_funcall(self_ty, idx, destination, &mut fargs, loc) } // Normal, non-virtual function calls InstanceDef::Item(..) @@ -623,13 +615,12 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_virtual_funcall( &mut self, self_ty: Ty<'tcx>, - def_id: DefId, idx: usize, place: &Place<'tcx>, fargs: &mut [Expr], loc: Location, ) -> Vec { - let vtable_field_name = self.vtable_field_name(def_id, idx); + let vtable_field_name = self.vtable_field_name(idx); trace!(?self_ty, ?place, ?vtable_field_name, "codegen_virtual_funcall"); debug!(?fargs, "codegen_virtual_funcall"); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index aec9d8143818..3a9d54a384af 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -332,11 +332,11 @@ impl<'tcx> GotocCtx<'tcx> { ty: Ty<'tcx>, args: ty::GenericArgsRef<'tcx>, ) -> ty::PolyFnSig<'tcx> { - let sig = args.as_coroutine().poly_sig(); + let sig = args.as_coroutine().sig(); - let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter( - sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))), - ); + let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter(iter::once( + ty::BoundVariableKind::Region(ty::BrEnv), + )); let br = ty::BoundRegion { var: ty::BoundVar::from_usize(bound_vars.len() - 1), kind: ty::BoundRegionKind::BrEnv, @@ -349,7 +349,6 @@ impl<'tcx> GotocCtx<'tcx> { let pin_args = self.tcx.mk_args(&[env_ty.into()]); let env_ty = Ty::new_adt(self.tcx, pin_adt_ref, pin_args); - let sig = sig.skip_binder(); // The `FnSig` and the `ret_ty` here is for a coroutines main // `coroutine::resume(...) -> CoroutineState` function in case we // have an ordinary coroutine, or the `Future::poll(...) -> Poll` @@ -482,7 +481,7 @@ impl<'tcx> GotocCtx<'tcx> { let fn_ptr = fn_ty.to_pointer(); // vtable field name, i.e., 3_vol (idx_method) - let vtable_field_name = self.vtable_field_name(instance.def_id(), idx); + let vtable_field_name = self.vtable_field_name(idx); DatatypeComponent::field(vtable_field_name, fn_ptr) } diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index df472518c9a3..7b94dad06db4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -33,6 +33,7 @@ use rustc_data_structures::temp_dir::MaybeTempDir; use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE}; use rustc_hir::def_id::LOCAL_CRATE; use rustc_hir::definitions::DefPathHash; +use rustc_metadata::creader::MetadataLoaderDyn; use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME}; use rustc_metadata::EncodedMetadata; use rustc_middle::dep_graph::{WorkProduct, WorkProductId}; @@ -40,7 +41,6 @@ use rustc_middle::mir::mono::MonoItem; use rustc_middle::ty::TyCtxt; use rustc_middle::util::Providers; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; -use rustc_session::cstore::MetadataLoaderDyn; use rustc_session::output::out_filename; use rustc_session::Session; use rustc_smir::rustc_internal; 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 01fb198d16fa..6619a6949681 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -138,11 +138,6 @@ impl<'tcx> GotocCtx<'tcx> { self.gen_stack_variable(c, fname, "var", t, Location::none(), false) } - // Generate a Symbol Expression representing a function parameter from the MIR - pub fn gen_function_parameter(&mut self, c: u64, fname: &str, t: Type) -> Symbol { - self.gen_stack_variable(c, fname, "var", t, Location::none(), true) - } - /// Given a counter `c` a function name `fname, and a prefix `prefix`, generates a new function local variable /// It is an error to reuse an existing `c`, `fname` `prefix` tuple. fn gen_stack_variable( diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs index 98f6f533cd12..2782f2cee47c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs @@ -5,7 +5,6 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::InternedString; -use rustc_hir::def_id::DefId; use rustc_hir::def_id::LOCAL_CRATE; use rustc_middle::mir::mono::CodegenUnitNameBuilder; use rustc_middle::mir::Local; @@ -22,7 +21,7 @@ impl<'tcx> GotocCtx<'tcx> { pub fn codegen_var_base_name(&self, l: &Local) -> String { match self.find_debug_info(l) { None => format!("var_{}", l.index()), - Some(info) => format!("{}", info.name), + Some(info) => info.name, } } @@ -83,12 +82,8 @@ impl<'tcx> GotocCtx<'tcx> { /// The name for the struct field on a vtable for a given function. Because generic /// functions can share the same name, we need to use the index of the entry in the /// vtable. This is the same index that will be passed in virtual function calls as - /// InstanceDef::Virtual(def_id, idx). We could use solely the index as a key into - /// the vtable struct, but we add the method name for debugging readability. - /// Example: 3_vol - pub fn vtable_field_name(&self, _def_id: DefId, idx: usize) -> InternedString { - // format!("{}_{}", idx, with_no_trimmed_paths!(|| self.tcx.item_name(def_id))) - // TODO: use def_id https://github.com/model-checking/kani/issues/364 + /// InstanceDef::Virtual(def_id, idx). + pub fn vtable_field_name(&self, idx: usize) -> InternedString { idx.to_string().into() } diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs index 011907c14ea4..b23fb99f83ff 100644 --- a/kani-compiler/src/kani_middle/analysis.rs +++ b/kani-compiler/src/kani_middle/analysis.rs @@ -151,7 +151,6 @@ impl From<&Terminator> for Key { TerminatorKind::Assert { .. } => Key("Assert"), TerminatorKind::Call { .. } => Key("Call"), TerminatorKind::Drop { .. } => Key("Drop"), - TerminatorKind::CoroutineDrop => Key("CoroutineDrop"), TerminatorKind::Goto { .. } => Key("Goto"), TerminatorKind::InlineAsm { .. } => Key("InlineAsm"), TerminatorKind::Resume { .. } => Key("Resume"), diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index d56b7b5db65d..216feb66fb87 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -266,7 +266,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { /// Collect an instance depending on how it is used (invoked directly or via fn_ptr). fn collect_instance(&mut self, instance: Instance, is_direct_call: bool) { let should_collect = match instance.kind { - InstanceKind::Virtual | InstanceKind::Intrinsic => { + InstanceKind::Virtual { .. } | InstanceKind::Intrinsic => { // Instance definition has no body. assert!(is_direct_call, "Expected direct call {instance:?}"); false @@ -453,8 +453,7 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> { TerminatorKind::Abort { .. } | TerminatorKind::Assert { .. } => { // We generate code for this without invoking any lang item. } - TerminatorKind::CoroutineDrop { .. } - | TerminatorKind::Goto { .. } + TerminatorKind::Goto { .. } | TerminatorKind::SwitchInt { .. } | TerminatorKind::Resume | TerminatorKind::Return diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index 03298456c522..6af0b442c8d4 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -46,6 +46,7 @@ pub fn harness_stub_map( pub fn validate_instance(tcx: TyCtxt, instance: Instance) -> bool { let internal_instance = rustc_internal::internal(instance); if get_stub(tcx, internal_instance.def_id()).is_some() { + debug!(?instance, "validate_instance"); let item = CrateItem::try_from(instance).unwrap(); let mut checker = StubConstChecker::new(tcx, internal_instance, item); checker.visit_body(&item.body()); diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs index 492369fb32eb..53c3a92dd94c 100644 --- a/kani-driver/src/concrete_playback/test_generator.rs +++ b/kani-driver/src/concrete_playback/test_generator.rs @@ -163,7 +163,7 @@ impl KaniSession { let mut curr_line_num = 0; // Use a buffered reader/writer to generate the unit test line by line - for line in source_reader.lines().flatten() { + for line in source_reader.lines().map_while(Result::ok) { curr_line_num += 1; writeln!(temp_file, "{line}")?; if curr_line_num == proof_harness_end_line { diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs index 8b3f771756dc..194f220595c0 100644 --- a/library/kani/src/models/mod.rs +++ b/library/kani/src/models/mod.rs @@ -137,8 +137,8 @@ mod test { /// masks with lanes represented using i16. #[test] fn test_bitmask_i16() { - check_portable_bitmask::<_, i16, 16>(mask16x16::splat(false)); - check_portable_bitmask::<_, i16, 16>(mask16x16::splat(true)); + check_portable_bitmask::<_, i16, 16, u16>(mask16x16::splat(false)); + check_portable_bitmask::<_, i16, 16, u16>(mask16x16::splat(true)); } /// Tests that the model correctly fails if an invalid value is given. @@ -165,11 +165,11 @@ mod test { /// These values shouldn't be symmetric and ensure that we also handle endianness correctly. #[test] fn test_bitmask_i32() { - check_portable_bitmask::<_, i32, 8>(mask32x8::from([ + check_portable_bitmask::<_, i32, 8, u8>(mask32x8::from([ true, true, false, true, false, false, false, true, ])); - check_portable_bitmask::<_, i32, 4>(mask32x4::from([true, false, false, true])); + check_portable_bitmask::<_, i32, 4, u8>(mask32x4::from([true, false, false, true])); } #[repr(simd)] @@ -185,15 +185,16 @@ mod test { } /// Compare the value returned by our model and the portable simd representation. - fn check_portable_bitmask(mask: T) + fn check_portable_bitmask(mask: Mask) where - T: ToBitMask + Clone, - T::BitMask: Debug + PartialEq, + T: std::simd::MaskElement, + LaneCount: SupportedLaneCount, E: kani_intrinsic::MaskElement, [u8; kani_intrinsic::mask_len(LANES)]: Sized, + u64: From, { assert_eq!( - unsafe { kani_intrinsic::simd_bitmask::<_, T::BitMask, E, LANES>(mask.clone()) }, + unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, M, E, LANES>(mask.clone())) }, mask.to_bitmask() ); } @@ -211,4 +212,19 @@ mod test { unsafe { simd_bitmask::(mask) } ); } + + /// Similar to portable simd_harness. + #[test] + fn check_mask_harness() { + // From array doesn't work either. Manually build [false, true, false, true] + let mut mask = mask32x4::splat(false); + mask.set(1, true); + mask.set(3, true); + let bitmask = mask.to_bitmask(); + assert_eq!(bitmask, 0b1010); + + let kani_mask = + unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, u8, u32, 4>(mask.clone())) }; + assert_eq!(kani_mask, bitmask); + } } diff --git a/rust-toolchain.toml b/rust-toolchain.toml index e016b6b50492..6c7de32c5e63 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2023-12-01" +channel = "nightly-2023-12-08" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 161a96dbe1af..20782abe5cbc 100755 --- a/scripts/kani-regression.sh +++ b/scripts/kani-regression.sh @@ -100,14 +100,6 @@ FEATURES_MANIFEST_PATH="$KANI_DIR/tests/cargo-kani/cargo-features-flag/Cargo.tom cargo kani --manifest-path "$FEATURES_MANIFEST_PATH" --harness trivial_success cargo clean --manifest-path "$FEATURES_MANIFEST_PATH" -# Check that documentation compiles. -echo "Current disk usage:" -df -h -echo "Starting doc tests:" -cargo doc --workspace --no-deps --exclude std -echo "Disk usage after documentation build:" -df -h - echo echo "All Kani regression tests completed successfully." echo diff --git a/tests/expected/any_vec/exact_length.expected b/tests/expected/any_vec/exact_length.expected index 641db7843ff1..082f3fb61570 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: dereference failure: pointer outside object bounds\ -in check_access_length_17 +Failed Checks: assumption failed\ +in >::get_unchecked Checking harness check_access_length_zero... -Failed Checks: dereference failure: pointer outside object bounds\ -in check_access_length_zero +Failed Checks: assumption failed\ +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 167fefe6d6f4..24121aee4ee8 100644 --- a/tests/expected/any_vec/out_bounds.expected +++ b/tests/expected/any_vec/out_bounds.expected @@ -1,61 +1,6 @@ -check_always_out_bounds::check_0.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer NULL"\ -function check_always_out_bounds::check_0 - -check_always_out_bounds::check_0.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_0 - -check_always_out_bounds::check_0.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: invalid integer address"\ -function check_always_out_bounds::check_0 - -check_always_out_bounds::check_1.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_1 - -check_always_out_bounds::check_2.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_2 - -check_always_out_bounds::check_3.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_3 - -check_always_out_bounds::check_4.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_4 - -check_always_out_bounds::check_5.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_5 - -check_always_out_bounds::check_6.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_6 - -check_always_out_bounds::check_7.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_7 - -check_always_out_bounds::check_8.pointer_dereference\ -Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -function check_always_out_bounds::check_8 - -check_always_out_bounds::check_9.cover\ -Status: UNREACHABLE\ -Description: "cover condition: *val == 0"\ -function check_always_out_bounds::check_9 +Checking harness check_always_out_bounds... +Failed Checks: assumption failed +in >::get_unchecked +Verification failed for - check_always_out_bounds diff --git a/tests/kani/Intrinsics/SIMD/Shuffle/main.rs b/tests/kani/Intrinsics/SIMD/Shuffle/main.rs index b3b0d41f0dff..6d822a18bdc1 100644 --- a/tests/kani/Intrinsics/SIMD/Shuffle/main.rs +++ b/tests/kani/Intrinsics/SIMD/Shuffle/main.rs @@ -45,3 +45,13 @@ fn main() { assert!(c == i64x4(2, 4, 6, 8)); } } + +#[kani::proof] +fn check_shuffle() { + { + let y = i64x2(0, 1); + let z = i64x2(1, 2); + const I: [u32; 4] = [1, 2, 0, 3]; + let _x: i64x4 = unsafe { simd_shuffle(y, z, I) }; + } +} diff --git a/tests/kani/SIMD/portable_simd.rs b/tests/kani/SIMD/portable_simd.rs index c8995de410e0..64cfb4b1fcf3 100644 --- a/tests/kani/SIMD/portable_simd.rs +++ b/tests/kani/SIMD/portable_simd.rs @@ -4,7 +4,7 @@ //! Ensure we have basic support of portable SIMD. #![feature(portable_simd)] -use std::simd::{mask32x4, u64x16, ToBitMask}; +use std::simd::{mask32x4, u32x4, u64x16}; #[kani::proof] fn check_sum_any() { @@ -23,3 +23,10 @@ fn check_mask() { let bitmask = mask.to_bitmask(); assert_eq!(bitmask, 0b1010); } + +#[kani::proof] +fn check_resize() { + let x = u32x4::from_array([0, 1, 2, 3]); + assert_eq!(x.resize::<8>(9).to_array(), [0, 1, 2, 3, 9, 9, 9, 9]); + assert_eq!(x.resize::<2>(9).to_array(), [0, 1]); +} diff --git a/tests/kani/SIMD/swizzle.rs b/tests/kani/SIMD/swizzle.rs new file mode 100644 index 000000000000..26781743dbfa --- /dev/null +++ b/tests/kani/SIMD/swizzle.rs @@ -0,0 +1,31 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Ensure we can safely swizzle between SIMD types of different sizes. +#![feature(portable_simd)] + +use std::simd::{simd_swizzle, u32x4, u32x8}; + +#[kani::proof] +fn harness_from_u32x4_to_u32x4() { + let a = u32x4::from_array([0, 1, 2, 3]); + let b = u32x4::from_array([4, 5, 6, 7]); + let r: u32x4 = simd_swizzle!(a, b, [0, 1, 6, 7]); + assert_eq!(r.to_array(), [0, 1, 6, 7]); +} + +#[kani::proof] +fn harness_from_u32x4_to_u32x8() { + let a = u32x4::from_array([0, 1, 2, 3]); + let b = u32x4::from_array([4, 5, 6, 7]); + let r: u32x8 = simd_swizzle!(a, b, [0, 1, 2, 3, 4, 5, 6, 7]); + assert_eq!(r.to_array(), [0, 1, 2, 3, 4, 5, 6, 7]); +} + +#[kani::proof] +fn harness_from_u32x8_to_u32x4() { + let a = u32x8::from_array([0, 1, 2, 3, 4, 5, 6, 7]); + let b = u32x8::from_array([0, 1, 2, 3, 4, 5, 6, 7]); + let r: u32x4 = simd_swizzle!(a, b, [0, 1, 2, 3]); + assert_eq!(r.to_array(), [0, 1, 2, 3]); +}