diff --git a/.github/workflows/extra_jobs.yml b/.github/workflows/extra_jobs.yml index 416fe94072db..a9fe1785b0f1 100644 --- a/.github/workflows/extra_jobs.yml +++ b/.github/workflows/extra_jobs.yml @@ -15,7 +15,7 @@ # Note that this also means that the workflow version run is the one currently in `main`, # not the one from the PR. This is only relevant if a PR is changing this workflow. # -# See for more details. +# See https://github.com/actions/labeler?tab=readme-ov-file#recommended-permissions for more details. name: Kani Extra on: diff --git a/docs/src/rust-feature-support.md b/docs/src/rust-feature-support.md index d66636dd092d..0f7075ab395b 100644 --- a/docs/src/rust-feature-support.md +++ b/docs/src/rust-feature-support.md @@ -153,18 +153,11 @@ The semantics around some advanced features (traits, types, etc.) from Rust are not formally defined which makes it harder to ensure that we can properly model all their use cases. -In particular, there are some outstanding issues to note here: - * Sanity check `Variant` type in projections - [#448](https://github.com/model-checking/kani/issues/448). - * Unexpected fat pointer results in - [#277](https://github.com/model-checking/kani/issues/277), - [#327](https://github.com/model-checking/kani/issues/327) and - [#676](https://github.com/model-checking/kani/issues/676). - -We are particularly interested in bug reports concerning -these features, so please [file a bug -report](https://github.com/model-checking/kani/issues/new?assignees=&labels=bug&template=bug_report.md) -if you're aware of one. +We are aware of a lack of sanity checking the `Variant` type in projections +[#448](https://github.com/model-checking/kani/issues/448). +If you become aware of other issues concerning +these features, please [file a bug +report](https://github.com/model-checking/kani/issues/new?assignees=&labels=bug&template=bug_report.md). ### Panic strategies diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index b847d75f63e1..8034d6df8f5d 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -156,7 +156,7 @@ fabsf32 | Yes | | fabsf64 | Yes | | fadd_fast | Yes | | fdiv_fast | Partial | [#809](https://github.com/model-checking/kani/issues/809) | -float_to_int_unchecked | Partial | [#3629](https://github.com/model-checking/kani/issues/3629) | +float_to_int_unchecked | Yes | | floorf32 | Yes | | floorf64 | Yes | | fmaf32 | Partial | Results are overapproximated | diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs index 1683147ce30e..c55f43a32b26 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs @@ -70,7 +70,6 @@ impl GotocCtx<'_> { } else if self.is_cffi_enabled() && instance.fn_abi().unwrap().conv == CallConvention::C { // When C-FFI feature is enabled, we just trust the rust declaration. // TODO: Add proper casting and clashing definitions check. - // https://github.com/model-checking/kani/issues/1350 // https://github.com/model-checking/kani/issues/2426 self.ensure(mangled_fn_name, |gcx, _| { let typ = gcx.codegen_ffi_type(instance); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 721082c20bd6..d77f8dcd1eac 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -176,13 +176,6 @@ impl ProjectedPlace { "Unexpected type mismatch in projection:\n{goto_expr:?}\nExpr type\n{expr_ty:?}\nType from MIR\n{ty_from_mir:?}" ); warn!("{}", msg); - // TODO: there's an expr type mismatch with the rust 2022-11-20 toolchain - // for simd: - // https://github.com/model-checking/kani/issues/1926 - // Disabling it for this specific case. - if !(expr_ty.is_integer() && ty_from_mir.is_struct_tag()) { - debug_assert!(false, "{}", msg); - } return Err(Box::new(UnimplementedData::new( "Projection mismatch", "https://github.com/model-checking/kani/issues/277", diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index e740cdf3ab96..526bc0014c37 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -522,13 +522,6 @@ impl GotocCtx<'_> { // The only argument should be a self reference let args = vec![place_ref]; - // We have a known issue where nested Arc and Mutex objects result in - // drop_in_place call implementations that fail to typecheck. Skipping - // drop entirely causes unsound verification results in common cases - // like vector extend, so for now, add a sound special case workaround - // for calls that fail the typecheck. - // https://github.com/model-checking/kani/issues/426 - // Unblocks: https://github.com/model-checking/kani/issues/435 func.call(args).as_stmt(loc) } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index d950d4262300..bb116e7115ba 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -464,11 +464,6 @@ impl<'tcx> GotocCtx<'tcx> { /// Gives the vtable name for a type. /// In some cases, we have &T, in other cases T, so normalize. - /// - /// TODO: to handle trait upcasting, this will need to use a - /// poly existential trait type as a part of the key as well. - /// See compiler/rustc_middle/src/ty/vtable.rs - /// pub fn vtable_name(&self, t: Ty<'tcx>) -> String { format!("{}::vtable", self.normalized_trait_name(t)) } diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index aec0c6ddc0de..966eea8a9e39 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -61,9 +61,6 @@ macro_rules! kani_mem { /// and 3, /// and the value stored must respect the validity invariants for type `T`. /// - /// TODO: Kani should automatically add those checks when a de-reference happens. - /// - /// /// This function will panic today if the pointer is not null, and it points to an unallocated or /// deallocated memory location. This is an existing Kani limitation. /// See for more details.