From adebe367f26f1eacbe23e9b336599627c5590d51 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Date: Wed, 8 Jun 2022 12:05:00 -0700
Subject: [PATCH] Report CBMC verification time (#1247)

---
 kani-driver/src/call_cbmc.rs                  |  4 ++++
 .../report/verification-time/expected         |  1 +
 .../expected/report/verification-time/main.rs | 22 +++++++++++++++++++
 3 files changed, 27 insertions(+)
 create mode 100644 tests/expected/report/verification-time/expected
 create mode 100644 tests/expected/report/verification-time/main.rs

diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index 994de0aa56b52..636a0df574dcf 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -6,6 +6,7 @@ use kani_metadata::HarnessMetadata;
 use std::ffi::OsString;
 use std::path::Path;
 use std::process::Command;
+use std::time::Instant;
 
 use crate::args::KaniArgs;
 use crate::session::KaniSession;
@@ -40,7 +41,9 @@ impl KaniSession {
             // extra argument
             cmd.arg("--json-ui");
 
+            let now = Instant::now();
             let _cbmc_result = self.run_redirect(cmd, &output_filename)?;
+            let elapsed = now.elapsed().as_secs_f32();
             let format_result = self.format_cbmc_output(&output_filename);
 
             if format_result.is_err() {
@@ -51,6 +54,7 @@ impl KaniSession {
                 // the best possible fix is port to rust instead of using python, or getting more
                 // feedback than just exit status (or using a particular magic exit code?)
             }
+            println!("Verification Time: {}s", elapsed);
         }
 
         Ok(VerificationStatus::Success)
diff --git a/tests/expected/report/verification-time/expected b/tests/expected/report/verification-time/expected
new file mode 100644
index 0000000000000..fc97e04aefdbd
--- /dev/null
+++ b/tests/expected/report/verification-time/expected
@@ -0,0 +1 @@
+Verification Time:
diff --git a/tests/expected/report/verification-time/main.rs b/tests/expected/report/verification-time/main.rs
new file mode 100644
index 0000000000000..26e8d1361e8ea
--- /dev/null
+++ b/tests/expected/report/verification-time/main.rs
@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test is meant for checking that the "Verification time:" line (which
+// reports the time spent in CBMC) is printed in the output
+
+fn is_sorted(s: &[i32]) -> bool {
+    for i in 0..s.len() - 1 {
+        if !(s[i] <= s[i + 1]) {
+            return false;
+        }
+    }
+    true
+}
+
+#[kani::proof]
+#[kani::unwind(6)]
+fn check_sorted() {
+    let mut arr: [i32; 5] = kani::any();
+    arr.sort();
+    assert!(is_sorted(&arr));
+}