Create new coverage subcommand

kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs

@@ -19,7 +19,6 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn codegen_block(&mut self, bb: BasicBlockIdx, bbd: &BasicBlock) {
         debug!(?bb, "codegen_block");
         let label = bb_label(bb);
-        let check_coverage = self.queries.args().check_coverage;
         // the first statement should be labelled. if there is no statements, then the
         // terminator should be labelled.
         match bbd.statements.len() {

kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

@@ -3,7 +3,6 @@
 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};

kani-driver/src/args/coverage_args.rs

@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+use crate::args::CommonArgs;
+use clap::Parser;
+
+#[derive(Debug, Parser)]
+pub struct CargoCoverageArgs {
+    #[command(flatten)]
+    pub coverage: CoverageArgs,
+}
+
+#[derive(Debug, clap::Args)]
+pub struct CoverageArgs {
+    /// Common args always available to Kani subcommands.
+    #[command(flatten)]
+    pub common_opts: CommonArgs,
+}

kani-driver/src/args/mod.rs

@@ -6,10 +6,12 @@ pub mod assess_args;
 pub mod cargo;
 pub mod common;
 pub mod playback_args;
+pub mod coverage_args;
 
 pub use assess_args::*;
 
 use self::common::*;
+use self::coverage_args::CargoCoverageArgs;
 use crate::args::cargo::CargoTargetArgs;
 use crate::util::warning;
 use cargo::CargoCommonArgs;
@@ -112,6 +114,9 @@ pub enum CargoKaniSubcommand {
 
     /// Execute concrete playback testcases of a local package.
     Playback(Box<playback_args::CargoPlaybackArgs>),
+
+    /// TBD
+    Coverage(Box<coverage_args::CargoCoverageArgs>),
 }
 
 // Common arguments for invoking Kani for verification purpose. This gets put into KaniContext,
@@ -478,6 +483,7 @@ impl ValidateArgs for CargoKaniSubcommand {
         match self {
             // Assess doesn't implement validation yet.
             CargoKaniSubcommand::Assess(_) => Ok(()),
+            CargoKaniSubcommand::Coverage(_) => Ok(()),
             CargoKaniSubcommand::Playback(playback) => playback.validate(),
         }
     }

kani-driver/src/cbmc_property_renderer.rs

@@ -503,7 +503,7 @@ fn format_result_new_coverage(properties: &[Property]) -> String {
     let mut formatted_output = String::new();
     formatted_output.push_str("\nCoverage Results (NEW):\n");
 
-    let mut coverage_results: BTreeMap<String, Vec<(usize, CheckStatus)>> =
+    let coverage_results: BTreeMap<String, Vec<(usize, CheckStatus)>> =
         BTreeMap::default();
 
     let re = {

kani-driver/src/coverage/coverage.rs

@@ -0,0 +1,10 @@
+use crate::args::coverage_args::CargoCoverageArgs;
+use anyhow::Result;
+
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+pub fn coverage_cargo(_args: CargoCoverageArgs) -> Result<()> {
+    Ok(())
+    //let install = InstallType::new()?;
+    //cargo_test(&install, args)
+}

kani-driver/src/coverage/mod.rs

@@ -0,0 +1,3 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+pub mod coverage;

kani-driver/src/main.rs

@@ -12,6 +12,7 @@ use args_toml::join_args;
 
 use crate::args::StandaloneSubcommand;
 use crate::concrete_playback::playback::{playback_cargo, playback_standalone};
+use crate::coverage::coverage::{coverage_cargo};
 use crate::project::Project;
 use crate::session::KaniSession;
 use crate::version::print_kani_version;
@@ -31,6 +32,7 @@ mod call_single_file;
 mod cbmc_output_parser;
 mod cbmc_property_renderer;
 mod concrete_playback;
+mod coverage;
 mod harness_runner;
 mod metadata;
 mod project;
@@ -79,6 +81,9 @@ fn cargokani_main(input_args: Vec<OsString>) -> Result<()> {
         Some(CargoKaniSubcommand::Playback(args)) => {
             return playback_cargo(*args);
         }
+        Some(CargoKaniSubcommand::Coverage(args)) => {
+            return coverage_cargo(*args);
+        }
         None => {}
     }