You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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":
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.
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)
u32: 70, e.g. core::core_arch::x86::avx512bw::_kshiftli_mask32
AtomicOrdering: 17, e.g. core::intrinsics::atomic_cxchg
bool: 5, e.g. core::sync::atomic::atomic_load
SimdAlign: 2, simd_masked_load and simd_masked_store
u64: 1, _bextri_u64
About 98% are core_arch x86 intrinsics.
Test case
pubfnwith_usize<constN:usize>(x:u8) -> u8{
x.wrapping_add(Nasu8)}pubfnwith_bool<constFLAG:bool>(x:u8) -> u8{ifFLAG{ x }else{0}}pubfnwith_i32<constIMM:i32>(x:i32) -> i32{
x.wrapping_add(IMM)}// Same shape as stdarch's static_assert_uimm_bits!pubfnwith_imm_assert<constIMM8:i32>(x:i32) -> i32{const{assert!(0 <= IMM8 && IMM8 < 256)}
x.wrapping_shl(IMM8asu32)}
Running cargo kani autoharness -Z autoharness --list on current main (4e31125):
with_usize is selected as with_usize::<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.
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
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.
bool: only two values, so either one fixed value or a harness for each.
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:
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.
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.
Requested feature
Autoharness currently skips any function with a const generic parameter whose type is not
usize. Onlyusizeconst parameters are instantiated, always with the fixed value2; 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;
usizesupport 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 --listrun on verify-rust-std (x86_64 Linux), 1,581 functions are skipped for this reason.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 asi32)u32: 70, e.g.core::core_arch::x86::avx512bw::_kshiftli_mask32AtomicOrdering: 17, e.g.core::intrinsics::atomic_cxchgbool: 5, e.g.core::sync::atomic::atomic_loadSimdAlign: 2,simd_masked_loadandsimd_masked_storeu64: 1,_bextri_u64About 98% are
core_archx86 intrinsics.Test case
Running
cargo kani autoharness -Z autoharness --liston currentmain(4e31125):with_usizeis selected aswith_usize::<2>with_bool,with_i32andwith_imm_assertare all skipped withGeneric Function: non-usize const generic parameters are not supported yetwith_imm_assertis included for the #4820 interaction described below: today it is stopped by the non-usizecheck before theconst {}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 withE0080.stdarch's immediate checks are implemented exactly this way:
static_assert!expands toconst { assert!(...) }, and bothstatic_assert_uimm_bits!andstatic_assert_simm_bits!are built on it (library/stdarch/crates/core_arch/src/macros.rs). So if non-usizeintegers 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
i32,u32,u64): instantiate with0rather than2.0satisfies bothstatic_assert_uimm_bits!(0 <= imm < 2^bits) andstatic_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 that0doesn't satisfy.bool: only two values, so either one fixed value or a harness for each.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 beRelease), so the choice needs care.Two limitations worth stating up front:
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.Possibly related: impl-level const parameters
The non-
usizecheck 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-usizeconst parameter seems to get ausizevalue of2substituted, then fails the trait-bound check, and the function is reported under the "no candidate type" message instead of the non-usizeone.Example:
core::field::FieldRepresentingTypehasconst VARIANT: u32, FIELD: u32on 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
adt_const_params: Tracking Issue for more complex const parameter types:feature(adt_const_params)rust-lang/rust#95174