Fix autoharness termination test & print metadata in alphabetical order

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