Autoformat

Author: adpaco-aws

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<CodeRegion> {
+    pub fn coverage_span<'tcx>(
+        tcx: TyCtxt<'tcx>,
+        coverage: CovTerm,
+        instance: Instance,
+    ) -> Option<CodeRegion> {
         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::<u32>().unwrap();
-                Some(CovTerm::Counter(num.into()))
+            let num = num_str.parse::<u32>().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::<u32>().unwrap();
             Some(CovTerm::Expression(num.into()))
-        } else { None }
+        } else {
+            None
+        }
     }
 }

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

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::*;
 

kani-driver/src/call_cbmc.rs

@@ -5,22 +5,22 @@ 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::{
     extract_results, process_cbmc_output, CheckStatus, Property, VerificationOutput,
 };
 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<CoverageResults> {
-    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<CoverageR
 
             let term = CoverageTerm::Counter(counter_num.parse().unwrap());
             let region = CoverageRegion::from_str(span);
-            
+
             let cov_check = CoverageCheck::new(function, term, region, status);
             let file = cov_check.region.file.clone();
 
@@ -473,7 +481,6 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option<CoverageR
     }
 
     Some(CoverageResults::new(coverage_results))
-
 }
 /// Solve Unwind Value from conflicting inputs of unwind values. (--default-unwind, annotation-unwind, --unwind)
 pub fn resolve_unwind_value(

kani-driver/src/call_single_file.rs

@@ -126,7 +126,8 @@ impl KaniSession {
         if self.args.coverage {
             flags.extend_from_slice(
                 // &["-C", "instrument-coverage", "-Z", "no-profiler-runtime", "--emit=mir"].map(OsString::from),
-                &["-C", "instrument-coverage", "-Z", "no-profiler-runtime", "-C", "opt-level=0"].map(OsString::from),
+                &["-C", "instrument-coverage", "-Z", "no-profiler-runtime", "-C", "opt-level=0"]
+                    .map(OsString::from),
             );
         }
         flags.extend_from_slice(

kani-driver/src/cbmc_property_renderer.rs

@@ -4,7 +4,9 @@
 use crate::args::OutputFormat;
 use crate::call_cbmc::{FailedProperties, VerificationStatus};
 use crate::cbmc_output_parser::{CheckStatus, ParserItem, Property, TraceItem};
-use crate::coverage::cov_results::{self, fmt_coverage_results, CoverageCheck, CoverageRegion, CoverageResults, CoverageTerm};
+use crate::coverage::cov_results::{
+    self, fmt_coverage_results, CoverageCheck, CoverageRegion, CoverageResults, CoverageTerm,
+};
 use console::style;
 use once_cell::sync::Lazy;
 use regex::Regex;
@@ -455,7 +457,6 @@ fn format_result_new_coverage(cov_results: &CoverageResults) -> 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<Vec<TraceItem>>) -> String {

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<String
                 .or_insert_with(Vec::new)
                 .push(check.clone());
         }
-        
+
         for (function, checks) in checks_by_function {
             writeln!(fmt_string, "{file} ({function})")?;
             let mut sorted_checks: Vec<CoverageCheck> = 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 }
     }
 }
 

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

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;

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;

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