Minor changes to new coverage output

adpaco-aws · Feb 20, 2024 · fe3ebeb · fe3ebeb
1 parent bf99800
commit fe3ebeb
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 7 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -3,6 +3,7 @@
 use super::typ::TypeExt;
 use super::typ::FN_RETURN_VOID_VAR_NAME;
 use super::{bb_label, PropertyClass};
+use crate::codegen_cprover_gotoc::codegen::function;
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
@@ -97,7 +98,8 @@ impl<'tcx> GotocCtx<'tcx> {
             StatementKind::Coverage(cov) => {
                 // debug!(?opaque, "StatementKind::Coverage Opaque");
                 // self.codegen_coverage(stmt.span)
-                let cov_info = format!("{cov:?}");
+                let fun = self.current_fn().name();
+                let cov_info = format!("{cov:?} {fun}");
                 if cov_info.starts_with("Coverage { kind: CounterIncrement(") {
                     let coverage_stmt = self.codegen_coverage(&cov_info, stmt.span);
                     Stmt::block(vec![coverage_stmt], location)

diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs
@@ -510,20 +510,21 @@ fn format_result_new_coverage(properties: &[Property]) -> String {
         static RE: OnceLock<Regex> = OnceLock::new();
         RE.get_or_init(|| {
             Regex::new(
-                r#"^Coverage \{ kind: CounterIncrement\((?<counter_num>[0-9]+)\) \}"#,
+                r#"^Coverage \{ kind: CounterIncrement\((?<counter_num>[0-9]+)\) \} (?<func_name>[_\d\w]+)"#,
             )
             .unwrap()
         })
     };
     for prop in properties {
-        // println!("{prop:?}");
+        println!("{prop:?}");
         // let src = prop.source_location.clone();
         // we expect these to always refer to a function
-        let function = prop.source_location.function.as_ref().unwrap().clone();
+        // let function = prop.source_location.function.as_ref().unwrap().clone(); 
         let captures = re.captures(&prop.description).unwrap();
-        let name_hash = &captures["counter_num"];
+        let function = demangle(&captures["func_name"]);
+        let counter_num = &captures["counter_num"];
         let status = prop.status;
-        let new_str = format!("{function} {name_hash} {status}\n");
+        let new_str = format!("{function}, {counter_num}, {status}\n");
         formatted_output.push_str(&new_str);
         // let file_entries = coverage_results.entry(|v| v.push().or_default();
         // let check_status = if prop.status == CheckStatus::Covered {

diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs
@@ -74,7 +74,7 @@ pub fn build_lib(bin_folder: &Path) -> Result<()> {
 fn build_verification_lib(compiler_path: &Path) -> Result<()> {
     let extra_args =
         ["-Z", "build-std=panic_abort,std,test", "--config", "profile.dev.panic=\"abort\""];
-    let compiler_args = ["--kani-compiler", "-Cllvm-args=--ignore-global-asm --build-std"];
+    let compiler_args = ["--kani-compiler", "-Cllvm-args=--ignore-global-asm --build-std", "-Cinstrument-coverage", "-Z", "no-profiler-runtime"];
     build_kani_lib(compiler_path, &kani_sysroot_lib(), &extra_args, &compiler_args)
 }