From 08af576e8e3c1543e8fd02e96e95563ca780a582 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 17 Mar 2025 11:22:44 -0400 Subject: [PATCH 1/2] Don't panic on _ argument --- kani-compiler/src/kani_middle/codegen_units.rs | 6 +++--- .../cargo_autoharness_filter/filter.expected | 2 ++ tests/script-based-pre/cargo_autoharness_filter/src/lib.rs | 3 +++ 3 files changed, 8 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 189c14b246b3..a0f63463053d 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -425,14 +425,14 @@ fn automatic_harness_partition( if !implements_arbitrary { // Find the name of the argument by referencing var_debug_info. // Note that enumerate() starts at 0, while StableMIR argument_index starts at 1, hence the idx+1. - let arg_debug_info = body + let arg_name = body .var_debug_info .iter() .find(|var| { var.argument_index.is_some_and(|arg_idx| idx + 1 == usize::from(arg_idx)) }) - .expect("Arguments should have corresponding var debug info"); - problematic_args.push(arg_debug_info.name.to_string()) + .map_or("_".to_string(), |debug_info| debug_info.name.to_string()); + problematic_args.push(arg_name) } } if !problematic_args.is_empty() { diff --git a/tests/script-based-pre/cargo_autoharness_filter/filter.expected b/tests/script-based-pre/cargo_autoharness_filter/filter.expected index 5e60f3a426be..f324effe3d9b 100644 --- a/tests/script-based-pre/cargo_autoharness_filter/filter.expected +++ b/tests/script-based-pre/cargo_autoharness_filter/filter.expected @@ -147,6 +147,8 @@ If you believe that the provided reason is incorrect and Kani should have genera |----------------------------------------+------------------------------------------------------| | no_harness::unsupported_mut_pointer | Missing Arbitrary implementation for argument(s): _y | |----------------------------------------+------------------------------------------------------| +| no_harness::unsupported_no_arg_name | Missing Arbitrary implementation for argument(s): _ | +|----------------------------------------+------------------------------------------------------| | no_harness::unsupported_ref | Missing Arbitrary implementation for argument(s): _y | |----------------------------------------+------------------------------------------------------| | no_harness::unsupported_slice | Missing Arbitrary implementation for argument(s): _y | diff --git a/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs b/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs index bb278c73a2e7..0237606e2931 100644 --- a/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs +++ b/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs @@ -207,4 +207,7 @@ mod no_harness { ) -> DoesntImplementArbitrary { x } + // Test that we correctly render the name of the argument "_" in the table of skipped functions + // (this argument will have no var_debug_info from StableMIR, unlike arguments with names) + fn unsupported_no_arg_name(_: &()) {} } From f970d2c9d57e2a5ed2be596324b1e4be1dcffffc Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 17 Mar 2025 12:05:02 -0400 Subject: [PATCH 2/2] add autoharness suffix to goto files --- kani-compiler/src/kani_middle/metadata.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index f8de975802e1..b24b39578df5 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -101,7 +101,8 @@ pub fn gen_automatic_proof_metadata( // Leave the concrete playback instrumentation for now, but this feature does not actually support concrete playback. let loc = SourceLocation::new(fn_to_verify.body().unwrap().span); - let file_stem = format!("{}_{mangled_name}", base_name.file_stem().unwrap().to_str().unwrap()); + let file_stem = + format!("{}_{mangled_name}_autoharness", base_name.file_stem().unwrap().to_str().unwrap()); let model_file = base_name.with_file_name(file_stem).with_extension(ArtifactType::SymTabGoto); let kani_attributes = KaniAttributes::for_instance(tcx, *fn_to_verify);