When printing --time statistics, include all buckets in total times (#…

…1409)
verus-lang · Feb 6, 2025 · cec767d · cec767d
1 parent 5e8df04
commit cec767d
Showing 1 changed file with 18 additions and 10 deletions.
diff --git a/source/rust_verify/src/main.rs b/source/rust_verify/src/main.rs
@@ -107,14 +107,21 @@ 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()
             .filter(|(k, _)| k.function().is_none())
             .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,26 +365,26 @@ 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
                         );
                     }
                 }
                 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,