Report CBMC verification time (rust-lang#1247)

Author: zhassan-aws

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)

tests/expected/report/verification-time/expected

@@ -0,0 +1 @@
+Verification Time:

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));
+}