Print in alphabetical order

Author: carolynzech

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

@@ -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

@@ -2,15 +2,15 @@ Kani generated automatic harnesses for 5 function(s):
 +--------------------------------+
 | 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             |
 +--------------------------------+-----------------------------+---------------------+