Report memory usage for verification step

[zhassan-aws]

Requested feature: As of https://github.com/model-checking/kani/pull/1247, Kani reports the runtime of the verification step. It would be useful to also report memory usage to aid with performance comparisons.

I've been incorrectly using /usr/bin/time --verbose, but found out that the memory usage it reports does not include the child processes (e.g. CBMC).

[zhassan-aws]

For example, if I run the following program with Kani:

const N: usize = 5;

#[cfg_attr(kani, kani::proof, kani::unwind(6))]
fn main() {
    let mut v: Vec<String> = Vec::new();
    //let mut v: Vec<String> = Vec::with_capacity(N);
    for _i in 0..N {
        v.push(String::from("ABC"));
    }
    assert_eq!(v.len(), N);
    let index: usize = kani::any();
    kani::assume(index < v.len());
    let x = &v[index];
    assert_eq!(*x, "ABC");
}

using: /usr/bin/time --verbose kani push_string.rs

I observed memory usage in htop reaching 4445 MB (Virtual) and 4100 (Resident), but time only reported 134 MB:

     Command being timed: "kani push_string.rs"
     User time (seconds): 1.82
     System time (seconds): 0.22
     Percent of CPU this job got: 2%
     Elapsed (wall clock) time (h:mm:ss or m:ss): 1:17.34
     Average shared text size (kbytes): 0
     Average unshared data size (kbytes): 0
     Average stack size (kbytes): 0
     Average total size (kbytes): 0
     Maximum resident set size (kbytes): 133996
     Average resident set size (kbytes): 0
     Major (requiring I/O) page faults: 0
     Minor (reclaiming a frame) page faults: 70065
     Voluntary context switches: 704
     Involuntary context switches: 4
     Swaps: 0
     File system inputs: 48
     File system outputs: 17696
     Socket messages sent: 0
     Socket messages received: 0
     Signals delivered: 0
     Page size (bytes): 4096
     Exit status: 0

[zhassan-aws]

For the record, this is a patch I'm using locally to measure memory usage:

diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index de50499a5f6..e8685f1c477 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -24,7 +24,9 @@ pub fn run_cbmc(&self, file: &Path, harness: &HarnessMetadata) -> Result<Verific
         let args: Vec<OsString> = self.cbmc_flags(file, harness)?;
 
         // TODO get cbmc path from self
-        let mut cmd = Command::new("cbmc");
+        let mut cmd = Command::new("/usr/bin/time");
+        cmd.arg("--verbose");
+        cmd.arg("cbmc");
         cmd.args(args);
 
         let now = Instant::now();

This doesn't work on macOS though.

[tedinski]

Programmatic tools are APIs like wait4

maybe https://github.com/lu-zero/wait4-rs