Skip to content

Autoharness: support non-usize const generic parameters #4876

Description

@CYJ904

Requested feature

Autoharness currently skips any function with a const generic parameter whose type is not usize. Only usize const parameters are instantiated, always with the fixed value 2; any other type is rejected with "non-usize const generic parameters are not supported yet":

https://github.com/model-checking/kani/blob/4e31125fd/kani-compiler/src/kani_middle/codegen_units.rs#L911-L921

When #4679 (merged) added generic function support, it listed const generic parameters as still skipped; usize support was added later in the same code, but other types remain unsupported and no issue tracks them. This issue proposes extending const generic instantiation to other primitive integer types, bool, and possibly enum-typed const parameters.

Use case

In a kani autoharness --list run on verify-rust-std (x86_64 Linux), 1,581 functions are skipped for this reason.

  1. i32: 1,488, almost all x86 SIMD intrinsics that take an immediate operand, e.g. core::core_arch::x86::aes::_mm_aeskeygenassist_si128 (_MM_* aliases counted as i32)
  2. u32: 70, e.g. core::core_arch::x86::avx512bw::_kshiftli_mask32
  3. AtomicOrdering: 17, e.g. core::intrinsics::atomic_cxchg
  4. bool: 5, e.g. core::sync::atomic::atomic_load
  5. SimdAlign: 2, simd_masked_load and simd_masked_store
  6. u64: 1, _bextri_u64

About 98% are core_arch x86 intrinsics.

Test case

pub fn with_usize<const N: usize>(x: u8) -> u8 {
    x.wrapping_add(N as u8)
}

pub fn with_bool<const FLAG: bool>(x: u8) -> u8 {
    if FLAG { x } else { 0 }
}

pub fn with_i32<const IMM: i32>(x: i32) -> i32 {
    x.wrapping_add(IMM)
}

// Same shape as stdarch's static_assert_uimm_bits!
pub fn with_imm_assert<const IMM8: i32>(x: i32) -> i32 {
    const { assert!(0 <= IMM8 && IMM8 < 256) }
    x.wrapping_shl(IMM8 as u32)
}

Running cargo kani autoharness -Z autoharness --list on current main (4e31125):

  1. with_usize is selected as with_usize::<2>
  2. with_bool, with_i32 and with_imm_assert are all skipped with Generic Function: non-usize const generic parameters are not supported yet

with_imm_assert is included for the #4820 interaction described below: today it is stopped by the non-usize check before the const {} block check is reached.

Interaction with #4820

Picking a default value per type is not enough on its own. #4820 added a check that skips any function whose body (or a callee instantiated with its const parameter) contains a const {} block depending on a const generic, because a failing evaluation aborts the whole run with E0080.

stdarch's immediate checks are implemented exactly this way: static_assert! expands to const { assert!(...) }, and both static_assert_uimm_bits! and static_assert_simm_bits! are built on it (library/stdarch/crates/core_arch/src/macros.rs). So if non-usize integers were instantiated with a fixed value today, most of the SIMD intrinsics above would likely just move to the #4820 skip message instead of being generated.

Possible direction

  1. Integer types (i32, u32, u64): instantiate with 0 rather than 2. 0 satisfies both static_assert_uimm_bits! (0 <= imm < 2^bits) and static_assert_simm_bits! (signed range). The Autoharness: skip const-generic fns with const-block preconditions #4820 check would also need to let these through. Since a failing evaluation can't be recovered from (which is why Autoharness: skip const-generic fns with const-block preconditions #4820 skips conservatively), recognizing these standard assertion macros may be more practical than evaluating the block. We haven't checked whether all 1,488 intrinsics use these two macros; some may assert other conditions that 0 doesn't satisfy.
  2. bool: only two values, so either one fixed value or a harness for each.
  3. Enum types (AtomicOrdering, SimdAlign): a variant has to be chosen per type rather than a numeric value. For atomics, not every ordering is valid in every position (e.g. the failure ordering of a compare-exchange can't be Release), so the choice needs care.

Two limitations worth stating up front:

  1. As with usize, a single instantiation only covers one value of the parameter. For SIMD intrinsics behavior differs a lot between immediates, so this turns functions from skipped into generated, but doesn't verify them across all immediates.
  2. We haven't checked how many of these intrinsics Kani can actually verify once a harness is generated.

Possibly related: impl-level const parameters

The non-usize check only looks at the function's own generic parameters (own_params), not const parameters declared on the enclosing impl. From reading the code (not verified by running it), an impl-level non-usize const parameter seems to get a usize value of 2 substituted, then fails the trait-bound check, and the function is reported under the "no candidate type" message instead of the non-usize one.

Example: core::field::FieldRepresentingType has const VARIANT: u32, FIELD: u32 on its impls, and its 7 trait methods show up under the no-candidate-type message. The effect is only on classification (these functions are skipped either way), but it makes the counts for the two messages inaccurate. Happy to split this into a separate issue if that's preferred.

Relevant documentation

  1. Const generics in the Rust reference: https://doc.rust-lang.org/reference/items/generics.html#const-generics
  2. Enum-typed const parameters rely on adt_const_params: Tracking Issue for more complex const parameter types: feature(adt_const_params) rust-lang/rust#95174

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    [C] Feature / EnhancementA new feature request or enhancement to an existing feature.

    Type

    No type

    Projects

    No projects

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions