Autoharness: Don't panic on _ argument and add _autoharness suffix to GOTO files (#3942)

Turns out that if an argument is just `_`, it doesn't have
`var_debug_info` in StableMIR. So this PR changes autoharness behavior
to provide `_` for the argument name when `var_debug_info` is None
(instead of panicking).

I don't currently know of any other cases where there wouldn't be
`var_debug_info`, but we should pay extra attention to the cases where
autoharness reports `_` as an argument name and update this logic if
need be.

I also added an `_autoharness` suffix to the generated GOTO files so
that it's easier to tell which files are from autoharness and which
aren't.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: carolynzech

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() {

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);

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 |

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(_: &()) {}
 }