Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adopt Rust's source-based code coverage instrumentation #3119

Merged
merged 66 commits into from
Aug 27, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
66 commits
Select commit Hold shift + click to select a range
b786e18
Adopt Rust's region-based coverage instrumentation
adpaco-aws Feb 8, 2024
8741945
Add missing file
adpaco-aws Apr 2, 2024
b3813fd
Serialize results
adpaco-aws Apr 3, 2024
99eda5a
Print where coverage results are saved
adpaco-aws Apr 3, 2024
42836c1
Match on parentheses, all props need to match
adpaco-aws Apr 5, 2024
ec1f196
Better splits
adpaco-aws Apr 8, 2024
a30de87
Autoformat
adpaco-aws Apr 18, 2024
3dfa074
Fixes for toolchain upgrade sync
adpaco-aws Apr 20, 2024
89dc04b
Missing copyright
adpaco-aws Apr 20, 2024
fe0ee14
Remove `cov` subcommand
adpaco-aws Apr 22, 2024
6fd483b
Update unstable option for source coverage
adpaco-aws Apr 22, 2024
12216ec
fixes for `clippy`
adpaco-aws Apr 22, 2024
e010665
Use square brackets to match on func. name
adpaco-aws Apr 22, 2024
d512c4b
Use curly brackets instead
adpaco-aws Apr 22, 2024
fa8e2bd
Merge branch 'main' into region-cov-basic
adpaco-aws Jul 29, 2024
c68c7ed
Fix issues related to toolchain update
adpaco-aws Jul 30, 2024
77d53c2
Save timestamped coverage metadata and results
adpaco-aws Aug 12, 2024
d9ad862
Followup fix warnings and format
adpaco-aws Aug 12, 2024
655ee69
Comment out debugging statements
adpaco-aws Aug 12, 2024
ecf1f7e
Do not instrument stdlib
adpaco-aws Aug 12, 2024
e086ef1
Better names in `codegen_coverage`
adpaco-aws Aug 12, 2024
a8d5c8f
Update RFC number
adpaco-aws Aug 12, 2024
0b5faa5
Add placeholder to show coverage summary
adpaco-aws Aug 12, 2024
bd5dee6
Merge branch 'main' into region-cov-basic
adpaco-aws Aug 13, 2024
0229a40
Cleanup and document coverage-related compiler APIs
adpaco-aws Aug 13, 2024
e4dda7a
Improve coverage checks postprocessing
adpaco-aws Aug 13, 2024
b01cb64
Implement `Display` for `CoverageResults` and use
adpaco-aws Aug 13, 2024
f79e074
Clarify comment in `format_coverage`
adpaco-aws Aug 13, 2024
c0008d5
Reformat
adpaco-aws Aug 14, 2024
9730d5f
Deal with `clippy` issues
adpaco-aws Aug 14, 2024
e88a056
Reformat
adpaco-aws Aug 14, 2024
dc37cfd
Bless coverage tests with source coverage results
adpaco-aws Aug 14, 2024
f029874
Bless tests more
adpaco-aws Aug 14, 2024
6eefd6f
Fix postprocess with closures - bless test too
adpaco-aws Aug 14, 2024
0262056
Fix format in tests..
adpaco-aws Aug 14, 2024
be21bd7
Manual `cargo update` to see if lock errors go away
adpaco-aws Aug 14, 2024
db1b1a3
Scaffold coverage results saving for standalone mdoe
adpaco-aws Aug 14, 2024
0162d30
Save coverage results with standalone mode
adpaco-aws Aug 15, 2024
9620601
Format fixes
adpaco-aws Aug 15, 2024
8511087
Add test for saving coverage results
adpaco-aws Aug 15, 2024
a94800e
Merge branch 'main' into region-cov-basic
adpaco-aws Aug 15, 2024
93faa8a
Format new test
adpaco-aws Aug 15, 2024
d484c54
Add running test to `coverage`
adpaco-aws Aug 15, 2024
9afd0a3
Fix `variant.rs` test
adpaco-aws Aug 15, 2024
a8bb841
Merge branch 'main' into region-cov-basic
adpaco-aws Aug 15, 2024
e630a32
Avoid problems with functions with cov info
adpaco-aws Aug 16, 2024
7bfd919
Temp: Run `kani-perf.sh` with coverage on
adpaco-aws Aug 16, 2024
95e8788
Use $ as the separator for function names
adpaco-aws Aug 16, 2024
a79c9d6
Remove comment and `-C opt-level=0`
adpaco-aws Aug 20, 2024
5a574f7
Undo change in `compiletest` to run with coverage
adpaco-aws Aug 20, 2024
0943ee3
Format
adpaco-aws Aug 20, 2024
f86595b
Merge branch 'main' into region-cov-basic
adpaco-aws Aug 20, 2024
e6165a2
Use `time` instead of `chrono`
adpaco-aws Aug 20, 2024
ecf1d7e
Change in format
adpaco-aws Aug 20, 2024
047f24d
Fix test description
adpaco-aws Aug 20, 2024
88ba7e5
Paste link to issue
adpaco-aws Aug 20, 2024
c0cc10d
Reorganize and document tests
adpaco-aws Aug 20, 2024
fb7c9e9
Fix up some `expected` outputs
adpaco-aws Aug 21, 2024
cf3b465
Make `parse_coverage_opaque` return a `CovTerm` directly
adpaco-aws Aug 22, 2024
a7ea4ee
Add documentation to `parse_coverage_opaque`
adpaco-aws Aug 22, 2024
0d56bdd
Remove `coverage_args` module
adpaco-aws Aug 22, 2024
8912288
Add timestamp comment
adpaco-aws Aug 23, 2024
1f821fd
Fix args and comment in postprocessing
adpaco-aws Aug 23, 2024
7ad9c8d
Add comment on regex
adpaco-aws Aug 23, 2024
41882b4
Merge branch 'main' into region-cov-basic
adpaco-aws Aug 23, 2024
50e1378
Merge branch 'main' into region-cov-basic
adpaco-aws Aug 23, 2024
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
53 changes: 53 additions & 0 deletions Cargo.lock
Original file line number Diff line number Diff line change
Expand Up @@ -316,6 +316,15 @@ dependencies = [
"memchr",
]

[[package]]
name = "deranged"
version = "0.3.11"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b42b6fa04a440b495c8b04d0e71b707c585f83cb9cb28cf8cd0d976c315e31b4"
dependencies = [
"powerfmt",
]

[[package]]
name = "either"
version = "1.13.0"
Expand Down Expand Up @@ -500,6 +509,7 @@ dependencies = [
"strum",
"strum_macros",
"tempfile",
"time",
"toml",
"tracing",
"tracing-subscriber",
Expand Down Expand Up @@ -660,6 +670,12 @@ dependencies = [
"num-traits",
]

[[package]]
name = "num-conv"
version = "0.1.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "51d515d32fb182ee37cda2ccdcb92950d6a3c2893aa280e540671c2cd0f3b1d9"

[[package]]
name = "num-integer"
version = "0.1.46"
Expand Down Expand Up @@ -767,6 +783,12 @@ version = "0.2.14"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "bda66fc9667c18cb2758a2ac84d1167245054bcf85d5d1aaa6923f45801bdd02"

[[package]]
name = "powerfmt"
version = "0.2.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "439ee305def115ba05938db6eb1644ff94165c5ab5e9420d1c1bcedbba909391"

[[package]]
name = "ppv-lite86"
version = "0.2.20"
Expand Down Expand Up @@ -1179,6 +1201,37 @@ dependencies = [
"once_cell",
]

[[package]]
name = "time"
version = "0.3.36"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5dfd88e563464686c916c7e46e623e520ddc6d79fa6641390f2e3fa86e83e885"
dependencies = [
"deranged",
"itoa",
"num-conv",
"powerfmt",
"serde",
"time-core",
"time-macros",
]

[[package]]
name = "time-core"
version = "0.1.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "ef927ca75afb808a4d64dd374f00a2adf8d0fcff8e7b184af886c3c87ec4a3f3"

[[package]]
name = "time-macros"
version = "0.2.18"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3f252a68540fde3a3877aeea552b832b40ab9a69e318efd078774a01ddee1ccf"
dependencies = [
"num-conv",
"time-core",
]

[[package]]
name = "toml"
version = "0.8.19"
Expand Down
16 changes: 9 additions & 7 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@
use crate::codegen_cprover_gotoc::GotocCtx;
use cbmc::goto_program::{Expr, Location, Stmt, Type};
use cbmc::InternedString;
use rustc_middle::mir::coverage::CodeRegion;
use stable_mir::mir::{Place, ProjectionElem};
use stable_mir::ty::{Span as SpanStable, TypeAndMut};
use strum_macros::{AsRefStr, EnumString};
Expand Down Expand Up @@ -148,18 +149,19 @@ impl<'tcx> GotocCtx<'tcx> {
}

/// Generate a cover statement for code coverage reports.
pub fn codegen_coverage(&self, span: SpanStable) -> Stmt {
pub fn codegen_coverage(
&self,
counter_data: &str,
span: SpanStable,
code_region: CodeRegion,
) -> Stmt {
let loc = self.codegen_caller_span_stable(span);
// Should use Stmt::cover, but currently this doesn't work with CBMC
// unless it is run with '--cover cover' (see
// https://github.com/diffblue/cbmc/issues/6613). So for now use
// `assert(false)`.
self.codegen_assert(
Expr::bool_false(),
PropertyClass::CodeCoverage,
"code coverage for location",
loc,
)
let msg = format!("{counter_data} - {code_region:?}");
self.codegen_assert(Expr::bool_false(), PropertyClass::CodeCoverage, &msg, loc)
}

// The above represent the basic operations we can perform w.r.t. assert/assume/cover
Expand Down
33 changes: 2 additions & 31 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,53 +20,24 @@ 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() {
0 => {
let term = &bbd.terminator;
let tcode = self.codegen_terminator(term);
// When checking coverage, the `coverage` check should be
adpaco-aws marked this conversation as resolved.
Show resolved Hide resolved
// labelled instead.
if check_coverage {
let span = term.span;
let cover = self.codegen_coverage(span);
self.current_fn_mut().push_onto_block(cover.with_label(label));
self.current_fn_mut().push_onto_block(tcode);
} else {
self.current_fn_mut().push_onto_block(tcode.with_label(label));
}
self.current_fn_mut().push_onto_block(tcode.with_label(label));
}
_ => {
let stmt = &bbd.statements[0];
let scode = self.codegen_statement(stmt);
// When checking coverage, the `coverage` check should be
// labelled instead.
if check_coverage {
let span = stmt.span;
let cover = self.codegen_coverage(span);
self.current_fn_mut().push_onto_block(cover.with_label(label));
self.current_fn_mut().push_onto_block(scode);
} else {
self.current_fn_mut().push_onto_block(scode.with_label(label));
}
self.current_fn_mut().push_onto_block(scode.with_label(label));

for s in &bbd.statements[1..] {
if check_coverage {
let span = s.span;
let cover = self.codegen_coverage(span);
self.current_fn_mut().push_onto_block(cover);
}
let stmt = self.codegen_statement(s);
self.current_fn_mut().push_onto_block(stmt);
}
let term = &bbd.terminator;
if check_coverage {
let span = term.span;
let cover = self.codegen_coverage(span);
self.current_fn_mut().push_onto_block(cover);
}
let tcode = self.codegen_terminator(term);
self.current_fn_mut().push_onto_block(tcode);
}
Expand Down
71 changes: 71 additions & 0 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
Original file line number Diff line number Diff line change
Expand Up @@ -216,3 +216,74 @@ impl<'tcx> GotocCtx<'tcx> {
self.reset_current_fn();
}
}

pub mod rustc_smir {
zhassan-aws marked this conversation as resolved.
Show resolved Hide resolved
use crate::stable_mir::CrateDef;
use rustc_middle::mir::coverage::CodeRegion;
use rustc_middle::mir::coverage::CovTerm;
use rustc_middle::mir::coverage::MappingKind::Code;
use rustc_middle::ty::TyCtxt;
use stable_mir::mir::mono::Instance;
use stable_mir::Opaque;

type CoverageOpaque = stable_mir::Opaque;

/// Retrieves the `CodeRegion` associated with the data in a
/// `CoverageOpaque` object.
pub fn region_from_coverage_opaque(
tcx: TyCtxt,
coverage_opaque: &CoverageOpaque,
instance: Instance,
) -> Option<CodeRegion> {
let cov_term = parse_coverage_opaque(coverage_opaque);
region_from_coverage(tcx, cov_term, instance)
}

/// Retrieves the `CodeRegion` associated with a `CovTerm` object.
///
/// Note: This function could be in the internal `rustc` impl for `Coverage`.
pub fn region_from_coverage(
tcx: TyCtxt<'_>,
coverage: CovTerm,
instance: Instance,
) -> Option<CodeRegion> {
// We need to pull the coverage info from the internal MIR instance.
let instance_def = rustc_smir::rustc_internal::internal(tcx, instance.def.def_id());
let body = tcx.instance_mir(rustc_middle::ty::InstanceKind::Item(instance_def));

// Some functions, like `std` ones, may not have coverage info attached
// to them because they have been compiled without coverage flags.
if let Some(cov_info) = &body.function_coverage_info {
// Iterate over the coverage mappings and match with the coverage term.
for mapping in &cov_info.mappings {
let Code(term) = mapping.kind else { unreachable!() };
if term == coverage {
return Some(mapping.code_region.clone());
}
}
}
None
}

/// Parse a `CoverageOpaque` item and return the corresponding `CovTerm`:
/// <https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/coverage/enum.CovTerm.html>
///
/// At present, a `CovTerm` can be one of the following:
/// - `CounterIncrement(<num>)`: A physical counter.
/// - `ExpressionUsed(<num>)`: An expression-based counter.
/// - `Zero`: A counter with a constant zero value.
fn parse_coverage_opaque(coverage_opaque: &Opaque) -> CovTerm {
let coverage_str = coverage_opaque.to_string();
if let Some(rest) = coverage_str.strip_prefix("CounterIncrement(") {
let (num_str, _rest) = rest.split_once(')').unwrap();
let num = num_str.parse::<u32>().unwrap();
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();
CovTerm::Expression(num.into())
} else {
CovTerm::Zero
}
}
}
19 changes: 18 additions & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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::region_from_coverage_opaque;
use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
use crate::unwrap_or_return_codegen_unimplemented_stmt;
use cbmc::goto_program::{Expr, Location, Stmt, Type};
Expand Down Expand Up @@ -158,12 +159,28 @@ impl<'tcx> GotocCtx<'tcx> {
location,
)
}
StatementKind::Coverage(coverage_opaque) => {
let function_name = self.current_fn().readable_name();
let instance = self.current_fn().instance_stable();
let counter_data = format!("{coverage_opaque:?} ${function_name}$");
let maybe_code_region =
region_from_coverage_opaque(self.tcx, &coverage_opaque, instance);
if let Some(code_region) = maybe_code_region {
let coverage_stmt =
self.codegen_coverage(&counter_data, stmt.span, code_region);
// TODO: Avoid single-statement blocks when conversion of
// standalone statements to the irep format is fixed.
// More details in <https://github.com/model-checking/kani/issues/3012>
Stmt::block(vec![coverage_stmt], location)
} else {
Stmt::skip(location)
}
}
StatementKind::PlaceMention(_) => todo!(),
StatementKind::FakeRead(..)
| StatementKind::Retag(_, _)
| StatementKind::AscribeUserType { .. }
| StatementKind::Nop
| StatementKind::Coverage { .. }
| StatementKind::ConstEvalCounter => Stmt::skip(location),
}
.with_location(location)
Expand Down
1 change: 1 addition & 0 deletions kani-driver/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_de
tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]}
rand = "0.8"
which = "6"
time = {version = "0.3.36", features = ["formatting"]}

# A good set of suggested dependencies can be found in rustup:
# https://github.com/rust-lang/rustup/blob/master/Cargo.toml
Expand Down
4 changes: 2 additions & 2 deletions kani-driver/src/args/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -615,12 +615,12 @@ impl ValidateArgs for VerificationArgs {
}

if self.coverage
&& !self.common_args.unstable_features.contains(UnstableFeature::LineCoverage)
&& !self.common_args.unstable_features.contains(UnstableFeature::SourceCoverage)
{
return Err(Error::raw(
ErrorKind::MissingRequiredArgument,
"The `--coverage` argument is unstable and requires `-Z \
line-coverage` to be used.",
source-coverage` to be used.",
));
}

Expand Down
2 changes: 1 addition & 1 deletion kani-driver/src/call_cargo.rs
Original file line number Diff line number Diff line change
Expand Up @@ -206,7 +206,7 @@ impl KaniSession {
})
}

fn cargo_metadata(&self, build_target: &str) -> Result<Metadata> {
pub fn cargo_metadata(&self, build_target: &str) -> Result<Metadata> {
let mut cmd = MetadataCommand::new();

// restrict metadata command to host platform. References:
Expand Down
Loading
Loading