From fc95b2d3601f6e2f204433bf8481d5d63d1fdcd4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 4 Jul 2025 11:14:45 +0000 Subject: [PATCH] Cleanup links to issues that have been addressed Over time, some issues got fixed yet our comments still claimed there was work to be done. Remove or replace these comments by more up-to-date ones. --- .github/workflows/extra_jobs.yml | 2 +- docs/src/rust-feature-support.md | 17 +++++------------ docs/src/rust-feature-support/intrinsics.md | 2 +- .../codegen/foreign_function.rs | 1 - .../src/codegen_cprover_gotoc/codegen/place.rs | 7 ------- .../codegen_cprover_gotoc/codegen/statement.rs | 7 ------- .../src/codegen_cprover_gotoc/codegen/typ.rs | 5 ----- library/kani_core/src/mem.rs | 3 --- 8 files changed, 7 insertions(+), 37 deletions(-) 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.