From 25effdf005046e3b6c47a8dbe977cfe97e2ea4d6 Mon Sep 17 00:00:00 2001
From: Chris Hawblitzel <Chris.Hawblitzel@microsoft.com>
Date: Sun, 26 Jan 2025 11:59:27 -0800
Subject: [PATCH] When printing --time statistics, include all buckets in total
 times

---
 source/rust_verify/src/main.rs | 28 ++++++++++++++++++----------
 1 file changed, 18 insertions(+), 10 deletions(-)

diff --git a/source/rust_verify/src/main.rs b/source/rust_verify/src/main.rs
index 08de7cb6af..fea8e23cf0 100644
--- a/source/rust_verify/src/main.rs
+++ b/source/rust_verify/src/main.rs
@@ -107,6 +107,13 @@ pub fn main() {
     let total_time = total_time_1 - total_time_0;
 
     let times_ms_json_data = if verifier.args.time {
+        fn compute_total(
+            verifier: &rust_verify::verifier::Verifier,
+            f: impl Fn(&rust_verify::verifier::BucketStats) -> std::time::Duration,
+        ) -> u128 {
+            verifier.bucket_stats.iter().map(|(_, v)| f(v)).sum::<std::time::Duration>().as_millis()
+        }
+
         let mut smt_init_times = verifier
             .bucket_stats
             .iter()
@@ -114,7 +121,7 @@ pub fn main() {
             .map(|(k, v)| (k.module(), v.time_smt_init.as_millis()))
             .collect::<Vec<_>>();
         smt_init_times.sort_by(|(_, a), (_, b)| b.cmp(a));
-        let total_smt_init: u128 = smt_init_times.iter().map(|(_, v)| v).sum();
+        let total_smt_init: u128 = compute_total(&verifier, |v| v.time_smt_init);
 
         struct SmtStats {
             time_millis: u128,
@@ -136,7 +143,7 @@ pub fn main() {
             })
             .collect::<Vec<_>>();
         smt_run_stats.sort_by(|(_, a), (_, b)| b.time_millis.cmp(&a.time_millis));
-        let total_smt_run: u128 = smt_run_stats.iter().map(|(_, v)| v.time_millis).sum();
+        let total_smt_run: u128 = compute_total(&verifier, |v| v.time_smt_run);
         let rlimit_counts: Option<Vec<u64>> =
             smt_run_stats.iter().map(|(_, v)| v.rlimit_count).collect();
         let total_rlimit_count: Option<u64> =
@@ -182,7 +189,8 @@ pub fn main() {
             })
             .collect::<Vec<_>>();
         air_times.sort_by(|(_, a), (_, b)| b.cmp(a));
-        let total_air: u128 = air_times.iter().map(|(_, v)| v).sum();
+        let total_air: u128 =
+            compute_total(&verifier, |v| v.time_air - (v.time_smt_init + v.time_smt_run));
 
         let mut verify_times = verifier
             .bucket_stats
@@ -191,7 +199,7 @@ pub fn main() {
             .map(|(k, v)| (k.module(), (v.time_verify).as_millis()))
             .collect::<Vec<_>>();
         verify_times.sort_by(|(_, a), (_, b)| b.cmp(a));
-        let total_verify: u128 = verify_times.iter().map(|(_, v)| v).sum();
+        let total_verify: u128 = compute_total(&verifier, |v| v.time_verify);
 
         // Rust time:
         let rust_init = stats.time_rustc;
@@ -342,7 +350,7 @@ pub fn main() {
                 }
             }
             println!(
-                "    total air-time:        {:>10} ms   ({} threads)",
+                "        total air-time:        {:>10} ms   ({} threads)",
                 total_air, verifier.num_threads
             );
             if verifier.args.time_expanded {
@@ -357,18 +365,18 @@ pub fn main() {
             }
             if !verifier.encountered_vir_error {
                 println!(
-                    "    total smt-time:        {:>10} ms   ({} threads)",
+                    "        total smt-time:        {:>10} ms   ({} threads)",
                     (total_smt_init + total_smt_run),
                     verifier.num_threads
                 );
                 println!(
-                    "        total smt-init:        {:>10} ms   ({} threads)",
+                    "            total smt-init:        {:>10} ms   ({} threads)",
                     total_smt_init, verifier.num_threads
                 );
                 if verifier.args.time_expanded {
                     for (i, (m, t)) in smt_init_times.iter().take(3).enumerate() {
                         println!(
-                            "            {}. {:<40} {:>10} ms",
+                            "                {}. {:<40} {:>10} ms",
                             i + 1,
                             rust_verify::verifier::module_name(m),
                             t
@@ -376,7 +384,7 @@ pub fn main() {
                     }
                 }
                 println!(
-                    "        total smt-run:         {:>10} ms{} ({} threads)",
+                    "            total smt-run:         {:>10} ms{} ({} threads)",
                     total_smt_run,
                     total_rlimit_count
                         .map(|rc| format!(", {:>8} rlimit", rc))
@@ -386,7 +394,7 @@ pub fn main() {
                 if verifier.args.time_expanded {
                     for (i, (m, t)) in smt_run_stats.iter().take(3).enumerate() {
                         println!(
-                            "            {}. {:<40} {:>10} ms{}",
+                            "                {}. {:<40} {:>10} ms{}",
                             i + 1,
                             rust_verify::verifier::module_name(m),
                             t.time_millis,