diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 93ac1434a5e9..8fdf817ee94a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -218,12 +218,12 @@ impl<'tcx> GotocCtx<'tcx> { } pub mod rustc_smir { + use crate::stable_mir::CrateDef; + use rustc_middle::mir::coverage::CodeRegion; use rustc_middle::mir::coverage::CovTerm; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; use stable_mir::Opaque; - use crate::stable_mir::CrateDef; - use rustc_middle::mir::coverage::CodeRegion; type CoverageOpaque = stable_mir::Opaque; @@ -238,7 +238,11 @@ pub mod rustc_smir { } /// Function that should be the internal implementation of opaque - pub fn coverage_span<'tcx>(tcx: TyCtxt<'tcx>, coverage: CovTerm, instance: Instance) -> Option { + pub fn coverage_span<'tcx>( + tcx: TyCtxt<'tcx>, + coverage: CovTerm, + instance: Instance, + ) -> Option { let instance_def = rustc_smir::rustc_internal::internal(tcx, instance.def.def_id()); let body = tcx.instance_mir(rustc_middle::ty::InstanceDef::Item(instance_def)); let cov_info = &body.function_coverage_info.clone().unwrap(); @@ -264,12 +268,14 @@ pub mod rustc_smir { return Some(CovTerm::Zero); } else if let Some(rest) = coverage_str.strip_prefix("CounterIncrement(") { let (num_str, _rest) = rest.split_once(")").unwrap(); - let num = num_str.parse::().unwrap(); - Some(CovTerm::Counter(num.into())) + let num = num_str.parse::().unwrap(); + Some(CovTerm::Counter(num.into())) } else if let Some(rest) = coverage_str.strip_prefix("ExpressionUsed(") { let (num_str, _rest) = rest.split_once(")").unwrap(); let num = num_str.parse::().unwrap(); Some(CovTerm::Expression(num.into())) - } else { None } + } else { + None + } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index a5a1c0c4b58c..cc3cbbcefb85 100644 --- 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::rustc_smir::coverage_opaque_span; use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::{Expr, Location, Stmt, Type}; @@ -17,7 +18,6 @@ use stable_mir::mir::{ Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, RETURN_LOCAL, }; use stable_mir::ty::{Abi, RigidTy, Span, Ty, TyKind, VariantIdx}; -use crate::codegen_cprover_gotoc::codegen::function::rustc_smir::coverage_opaque_span; use tracing::{debug, debug_span, trace}; impl<'tcx> GotocCtx<'tcx> { @@ -112,7 +112,7 @@ impl<'tcx> GotocCtx<'tcx> { StatementKind::Coverage(cov) => { // debug!(?opaque, "StatementKind::Coverage Opaque"); // self.codegen_coverage(stmt.span) - + let fun = self.current_fn().readable_name(); let instance = self.current_fn().instance_stable(); let cov_info = format!("{cov:?} ({fun})"); diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 2d7ce3415a84..9d50927cbe64 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -5,8 +5,8 @@ pub mod assess_args; pub mod cargo; pub mod common; -pub mod playback_args; pub mod coverage_args; +pub mod playback_args; pub use assess_args::*; diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index bc32ff597202..f777d8aa79fc 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -5,13 +5,13 @@ use anyhow::{bail, Result}; use kani_metadata::{CbmcSolver, HarnessMetadata}; use regex::Regex; use rustc_demangle::demangle; +use std::collections::BTreeMap; use std::ffi::OsString; use std::fmt::Write; use std::path::Path; use std::process::Command; use std::sync::OnceLock; use std::time::{Duration, Instant}; -use std::collections::BTreeMap; use crate::args::{OutputFormat, VerificationArgs}; use crate::cbmc_output_parser::{ @@ -19,8 +19,8 @@ use crate::cbmc_output_parser::{ }; use crate::cbmc_property_renderer::{format_coverage, format_result, kani_cbmc_output_filter}; use crate::coverage::cov_results::{self, CoverageCheck, CoverageResults}; -use crate::session::KaniSession; use crate::coverage::cov_results::{CoverageRegion, CoverageTerm}; +use crate::session::KaniSession; /// We will use Cadical by default since it performed better than MiniSAT in our analysis. /// Note: Kissat was marginally better, but it is an external solver which could be more unstable. @@ -324,7 +324,14 @@ impl VerificationResult { let show_checks = matches!(output_format, OutputFormat::Regular); let mut result = if let Some(cov_results) = &self.coverage_results { - format_coverage(results, cov_results, status, should_panic, failed_properties, show_checks) + format_coverage( + results, + cov_results, + status, + should_panic, + failed_properties, + show_checks, + ) } else { format_result(results, status, should_panic, failed_properties, show_checks) }; @@ -401,7 +408,8 @@ fn determine_failed_properties(properties: &[Property]) -> FailedProperties { } fn coverage_results_from_properties(properties: &[Property]) -> Option { - let cov_properties: Vec<&Property> = properties.iter().filter(|p| p.is_code_coverage_property()).collect(); + let cov_properties: Vec<&Property> = + properties.iter().filter(|p| p.is_code_coverage_property()).collect(); if cov_properties.is_empty() { return None; @@ -439,7 +447,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option Option String { fmt_coverage_results(&cov_results).expect("error: couldn't format coverage results") } - /// Attempts to build a message for a failed property with as much detailed /// information on the source location as possible. fn build_failure_message(description: String, trace: &Option>) -> String { diff --git a/kani-driver/src/coverage/cov_results.rs b/kani-driver/src/coverage/cov_results.rs index d42d642c460e..5cd594325d69 100644 --- a/kani-driver/src/coverage/cov_results.rs +++ b/kani-driver/src/coverage/cov_results.rs @@ -1,8 +1,8 @@ use crate::cbmc_output_parser::CheckStatus; -use std::{collections::BTreeMap, fmt::Display}; -use std::fmt::{self, Write}; use anyhow::Result; use serde::{Deserialize, Serialize}; +use std::fmt::{self, Write}; +use std::{collections::BTreeMap, fmt::Display}; #[derive(Clone, Debug, Serialize, Deserialize)] pub struct CoverageResults { @@ -27,7 +27,7 @@ pub fn fmt_coverage_results(coverage_results: &CoverageResults) -> Result = checks.to_vec(); @@ -50,8 +50,13 @@ pub struct CoverageCheck { } impl CoverageCheck { - pub fn new(function: String, term: CoverageTerm, region: CoverageRegion, status: CheckStatus) -> Self { - Self {function, term, region, status } + pub fn new( + function: String, + term: CoverageTerm, + region: CoverageRegion, + status: CheckStatus, + ) -> Self { + Self { function, term, region, status } } } diff --git a/kani-driver/src/coverage/coverage.rs b/kani-driver/src/coverage/coverage.rs index 94922261dac4..56241cd9d9b3 100644 --- a/kani-driver/src/coverage/coverage.rs +++ b/kani-driver/src/coverage/coverage.rs @@ -6,10 +6,10 @@ use std::fs::File; use std::io::Write; use crate::args::coverage_args::CargoCoverageArgs; -use crate::KaniSession; -use crate::project; use crate::harness_runner; use crate::harness_runner::HarnessResult; +use crate::project; +use crate::KaniSession; use anyhow::Result; use tracing::debug; @@ -34,15 +34,15 @@ impl KaniSession { let build_target = env!("TARGET"); let metadata = self.cargo_metadata(build_target)?; let target_dir = self - .args - .target_dir - .as_ref() - .unwrap_or(&metadata.target_directory.clone().into()) - .clone() - .join("kani"); - + .args + .target_dir + .as_ref() + .unwrap_or(&metadata.target_directory.clone().into()) + .clone() + .join("kani"); + let outdir = target_dir.join(build_target).join("cov"); - + if !outdir.exists() { fs::create_dir(&outdir)?; } diff --git a/kani-driver/src/coverage/mod.rs b/kani-driver/src/coverage/mod.rs index 8bac21cc742c..b03e6dfc8968 100644 --- a/kani-driver/src/coverage/mod.rs +++ b/kani-driver/src/coverage/mod.rs @@ -1,4 +1,4 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -pub mod coverage; pub mod cov_results; +pub mod coverage; diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 71fa8ff8196a..56f3ed7d1ecf 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -11,7 +11,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::coverage::coverage::coverage_cargo; use crate::project::Project; use crate::session::KaniSession; use crate::version::print_kani_version; diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs index ad0d61e539a2..4fb9b3a62f3a 100644 --- a/tools/build-kani/src/sysroot.rs +++ b/tools/build-kani/src/sysroot.rs @@ -74,7 +74,13 @@ 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", "-Cinstrument-coverage", "-Z", "no-profiler-runtime"]; + 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) }