Fix autoharness termination test & print metadata in alphabetical order (#3971)

#3968 [failed in the merge
queue](https://github.com/model-checking/kani/actions/runs/14180398658/job/39724995535)
because the `cargo_autoharness_termination` test assumed that the
recursion test wouldn't time out, but it did. This doesn't happen often,
since this test has worked up until now, but in the interest of having
robust tests, this PR splits the termination test into two:

- `autoharness_timeout`, which tests that the default timeout of 60s
kicks in
- `autoharness_unwind`, which tests that the default unwind bound of 20
kicks in

The unwind test specifies a timeout of 5m to ensure that the unwind
bound takes effect before the timeout.

While I was fixing this, I also fixed some inconsistencies with the
printed metadata:
- We use "Chosen Function" in one table and "Selected Function" in
another--changed it to "Selected Function" in both to be consistent
- The functions aren't printed alphabetically in 2/3 tables--fixed so
that they're always sorted

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

Author: Carolyn Zech

kani-compiler/src/kani_middle/codegen_units.rs

@@ -92,9 +92,11 @@ impl CodegenUnits {
                     args,
                     *kani_fns.get(&KaniModel::Any.into()).unwrap(),
                 );
-                let chosen_fn_names = chosen.iter().map(|func| func.name()).collect::<Vec<_>>();
                 AUTOHARNESS_MD
-                    .set(AutoHarnessMetadata { chosen: chosen_fn_names, skipped })
+                    .set(AutoHarnessMetadata {
+                        chosen: chosen.iter().map(|func| func.name()).collect::<BTreeSet<_>>(),
+                        skipped,
+                    })
                     .expect("Initializing the autoharness metdata failed");
 
                 let automatic_harnesses = get_all_automatic_harnesses(

kani-driver/src/autoharness/mod.rs

@@ -83,7 +83,7 @@ fn postprocess_project(
 /// Print automatic harness metadata to the terminal.
 fn print_autoharness_metadata(metadata: Vec<KaniMetadata>) {
     let mut chosen_table = PrettyTable::new();
-    chosen_table.set_header(vec!["Chosen Function"]);
+    chosen_table.set_header(vec!["Selected Function"]);
 
     let mut skipped_table = PrettyTable::new();
     skipped_table.set_header(vec!["Skipped Function", "Reason for Skipping"]);
@@ -122,7 +122,7 @@ fn print_autoharness_metadata(metadata: Vec<KaniMetadata>) {
 fn print_chosen_table(table: &mut PrettyTable) {
     if table.is_empty() {
         println!(
-            "\nChosen Functions: None. Kani did not generate automatic harnesses for any functions in the available crate(s)."
+            "\nSelected Functions: None. Kani did not generate automatic harnesses for any functions in the available crate(s)."
         );
         return;
     }
@@ -178,7 +178,8 @@ impl KaniSession {
     }
 
     /// Prints the results from running the `autoharness` subcommand.
-    pub fn print_autoharness_summary(&self, automatic: Vec<&HarnessResult<'_>>) -> Result<()> {
+    pub fn print_autoharness_summary(&self, mut automatic: Vec<&HarnessResult<'_>>) -> Result<()> {
+        automatic.sort_by(|a, b| a.harness.pretty_name.cmp(&b.harness.pretty_name));
         let (successes, failures): (Vec<_>, Vec<_>) =
             automatic.into_iter().partition(|r| r.result.status == VerificationStatus::Success);
 

kani_metadata/src/lib.rs

@@ -5,7 +5,7 @@ extern crate clap;
 
 use serde::{Deserialize, Serialize};
 use std::{
-    collections::{BTreeMap, HashSet},
+    collections::{BTreeMap, BTreeSet, HashSet},
     path::PathBuf,
 };
 use strum_macros::{Display, EnumString};
@@ -43,12 +43,12 @@ pub struct KaniMetadata {
 
 /// For the autoharness subcommand, all of the user-defined functions we found,
 /// which are "chosen" if we generated an automatic harness for them, and "skipped" otherwise.
+/// We use ordered data structures so that the metadata is in alphabetical order.
 #[derive(Debug, Clone, Serialize, Deserialize)]
 pub struct AutoHarnessMetadata {
     /// Functions we generated automatic harnesses for.
-    pub chosen: Vec<String>,
+    pub chosen: BTreeSet<String>,
     /// Map function names to the reason why we did not generate an automatic harness for that function.
-    /// We use an ordered map so that when we print the data, it is ordered alphabetically by function name.
     pub skipped: BTreeMap<String, AutoHarnessSkipReason>,
 }
 

tests/script-based-pre/cargo_autoharness_contracts/contracts.expected

@@ -1,16 +1,16 @@
 Kani generated automatic harnesses for 5 function(s):
 +--------------------------------+
-| Chosen Function                |
+| Selected Function              |
 +================================+
-| should_pass::div               |
+| should_fail::max               |
 |--------------------------------|
-| should_pass::has_recursion_gcd |
+| should_pass::div               |
 |--------------------------------|
 | should_pass::has_loop_contract |
 |--------------------------------|
-| should_pass::unchecked_mul     |
+| should_pass::has_recursion_gcd |
 |--------------------------------|
-| should_fail::max               |
+| should_pass::unchecked_mul     |
 +--------------------------------+
 
 Skipped Functions: None. Kani generated automatic harnesses for all functions in the available crate(s).
@@ -44,13 +44,13 @@ Autoharness Summary:
 +--------------------------------+-----------------------------+---------------------+
 | Selected Function              | Kind of Automatic Harness   | Verification Result |
 +====================================================================================+
-| should_pass::unchecked_mul     | #[kani::proof_for_contract] | Success             |
+| should_pass::div               | #[kani::proof_for_contract] | Success             |
 |--------------------------------+-----------------------------+---------------------|
 | should_pass::has_loop_contract | #[kani::proof]              | Success             |
 |--------------------------------+-----------------------------+---------------------|
 | should_pass::has_recursion_gcd | #[kani::proof_for_contract] | Success             |
 |--------------------------------+-----------------------------+---------------------|
-| should_pass::div               | #[kani::proof_for_contract] | Success             |
+| should_pass::unchecked_mul     | #[kani::proof_for_contract] | Success             |
 |--------------------------------+-----------------------------+---------------------|
 | should_fail::max               | #[kani::proof_for_contract] | Failure             |
 +--------------------------------+-----------------------------+---------------------+

tests/script-based-pre/cargo_autoharness_dependencies/dependencies.expected

@@ -1,9 +1,9 @@
 Kani generated automatic harnesses for 1 function(s):
-+-----------------+
-| Chosen Function |
-+=================+
-| yes_harness     |
-+-----------------+
++-------------------+
+| Selected Function |
++===================+
+| yes_harness       |
++-------------------+
 
 Skipped Functions: None. Kani generated automatic harnesses for all functions in the available crate(s).
 

tests/script-based-pre/cargo_autoharness_exclude/exclude.expected

@@ -1,9 +1,9 @@
 Kani generated automatic harnesses for 1 function(s):
-+-----------------+
-| Chosen Function |
-+=================+
-| include::simple |
-+-----------------+
++-------------------+
+| Selected Function |
++===================+
+| include::simple   |
++-------------------+
 
 Kani did not generate automatic harnesses for 2 function(s).
 If you believe that the provided reason is incorrect and Kani should have generated an automatic harness, please comment on this issue: https://github.com/model-checking/kani/issues/3832