From 71fee81c94bec8bb90935cb7510beafcc4646045 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 12 Feb 2025 11:05:41 -0800 Subject: [PATCH 1/8] update-toolchain --- .../src/codegen_cprover_gotoc/codegen/function.rs | 10 ++++++++-- rust-toolchain.toml | 2 +- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index bf64f0dd2e66..7bf156541715 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -251,13 +251,19 @@ pub mod rustc_smir { // 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)); - + let instance_internal = rustc_smir::rustc_internal::internal(tcx, instance); + let cov_ids_info = tcx.coverage_ids_info(instance_internal.def).unwrap(); + let bcb_to_covterm = cov_ids_info.term_for_bcb.clone(); // 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!() }; + let Code { bcb } = mapping.kind else { unreachable!() }; + let term = match bcb_to_covterm[bcb] { + Some(term) => term, + _ => CovTerm::Zero, + }; let source_map = tcx.sess.source_map(); let file = source_map.lookup_source_file(cov_info.body_span.lo()); if term == coverage { diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 307d7e8a6120..066f744f4675 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-02-10" +channel = "nightly-2025-02-11" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From 6ce02ee73db81b733354572ecd00ded9e5721ab4 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 13 Feb 2025 12:51:22 -0800 Subject: [PATCH 2/8] some more debugging --- .../codegen_cprover_gotoc/codegen/function.rs | 37 +++++++++---------- kani-driver/src/call_cbmc.rs | 11 ++++-- 2 files changed, 24 insertions(+), 24 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 7bf156541715..170024647abe 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -220,8 +220,8 @@ impl GotocCtx<'_> { pub mod rustc_smir { use crate::codegen_cprover_gotoc::codegen::source_region::{SourceRegion, make_source_region}; use crate::stable_mir::CrateDef; - use rustc_middle::mir::coverage::CovTerm; use rustc_middle::mir::coverage::MappingKind::Code; + use rustc_middle::mir::coverage::{BasicCoverageBlock}; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; @@ -236,8 +236,8 @@ pub mod rustc_smir { coverage_opaque: &CoverageOpaque, instance: Instance, ) -> Option<(SourceRegion, Filename)> { - let cov_term = parse_coverage_opaque(coverage_opaque); - region_from_coverage(tcx, cov_term, instance) + let bcb = parse_coverage_opaque(coverage_opaque); + region_from_coverage(tcx, bcb, instance) } /// Retrieves the `SourceRegion` associated with a `CovTerm` object. @@ -245,28 +245,28 @@ pub mod rustc_smir { /// Note: This function could be in the internal `rustc` impl for `Coverage`. pub fn region_from_coverage( tcx: TyCtxt<'_>, - coverage: CovTerm, + coverage: BasicCoverageBlock, instance: Instance, ) -> Option<(SourceRegion, Filename)> { // 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)); - let instance_internal = rustc_smir::rustc_internal::internal(tcx, instance); - let cov_ids_info = tcx.coverage_ids_info(instance_internal.def).unwrap(); - let bcb_to_covterm = cov_ids_info.term_for_bcb.clone(); + //let instance_internal = rustc_smir::rustc_internal::internal(tcx, instance); + //let cov_ids_info = tcx.coverage_ids_info(instance_internal.def).unwrap(); + //let bcb_to_covterm = cov_ids_info.term_for_bcb.clone(); // 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 { bcb } = mapping.kind else { unreachable!() }; - let term = match bcb_to_covterm[bcb] { - Some(term) => term, - _ => CovTerm::Zero, - }; + //let term = match bcb_to_covterm[bcb] { + // Some(term) => term, + // _ => CovTerm::Zero, + //}; let source_map = tcx.sess.source_map(); let file = source_map.lookup_source_file(cov_info.body_span.lo()); - if term == coverage { + if bcb == coverage { return Some(( make_source_region(source_map, cov_info, &file, mapping.span).unwrap(), rustc_internal::stable(cov_info.body_span).get_filename(), @@ -284,18 +284,15 @@ pub mod rustc_smir { /// - `CounterIncrement()`: A physical counter. /// - `ExpressionUsed()`: An expression-based counter. /// - `Zero`: A counter with a constant zero value. - fn parse_coverage_opaque(coverage_opaque: &Opaque) -> CovTerm { + fn parse_coverage_opaque(coverage_opaque: &Opaque) -> BasicCoverageBlock { let coverage_str = coverage_opaque.to_string(); - if let Some(rest) = coverage_str.strip_prefix("CounterIncrement(") { + if let Some(rest) = coverage_str.strip_prefix("VirtualCounter(bcb") { let (num_str, _rest) = rest.split_once(')').unwrap(); let num = num_str.parse::().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::().unwrap(); - CovTerm::Expression(num.into()) + println!("cover {:?}", num); + BasicCoverageBlock::from_u32(num) } else { - CovTerm::Zero + unreachable!(); } } } diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index b26b84ca2632..5411d1d863ef 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -501,7 +501,8 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option = OnceLock::new(); COUNTER_RE.get_or_init(|| { Regex::new( - r#"^(?CounterIncrement|ExpressionUsed)\((?[0-9]+)\) \$(?[^\$]+)\$ - (?.+)"#, + //r#"^(?CounterIncrement|ExpressionUsed)\((?[0-9]+)\) \$(?[^\$]+)\$ - (?.+)"#, + r#"^(?VirtualCounter\(bcb)(?[0-9]+)\) \$(?[^\$]+)\$ - (?.+)"#, ) .unwrap() }) @@ -511,20 +512,22 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option CoverageTerm::Counter(counter_id), "ExpressionUsed" => CoverageTerm::Expression(counter_id), _ => unreachable!("counter kind could not be recognized: {:?}", kind), - }; + };*/ + let term = CoverageTerm::Counter(counter_id); let region = CoverageRegion::from_str(span); let cov_check = CoverageCheck::new(function, term, region, status); From d9eab3ce871485eab9f5cc47e7b54dddf974808e Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 13 Feb 2025 12:53:58 -0800 Subject: [PATCH 3/8] minor fix --- kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 170024647abe..67e44a475b23 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -221,7 +221,7 @@ pub mod rustc_smir { use crate::codegen_cprover_gotoc::codegen::source_region::{SourceRegion, make_source_region}; use crate::stable_mir::CrateDef; use rustc_middle::mir::coverage::MappingKind::Code; - use rustc_middle::mir::coverage::{BasicCoverageBlock}; + use rustc_middle::mir::coverage::BasicCoverageBlock; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; From 23ba5bf47783c8318fd25ccb65089dea30a3eda6 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 13 Feb 2025 13:01:43 -0800 Subject: [PATCH 4/8] minor fix --- kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 67e44a475b23..65e15fb08315 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -220,8 +220,8 @@ impl GotocCtx<'_> { pub mod rustc_smir { use crate::codegen_cprover_gotoc::codegen::source_region::{SourceRegion, make_source_region}; use crate::stable_mir::CrateDef; - use rustc_middle::mir::coverage::MappingKind::Code; use rustc_middle::mir::coverage::BasicCoverageBlock; + use rustc_middle::mir::coverage::MappingKind::Code; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; From 029b771aa79448ab969820caca7d0447008736f6 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 13 Feb 2025 14:06:46 -0800 Subject: [PATCH 5/8] delete commented code --- .../src/codegen_cprover_gotoc/codegen/function.rs | 10 ---------- kani-driver/src/call_cbmc.rs | 9 --------- 2 files changed, 19 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 65e15fb08315..d35e881f4674 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -251,19 +251,10 @@ pub mod rustc_smir { // 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)); - //let instance_internal = rustc_smir::rustc_internal::internal(tcx, instance); - //let cov_ids_info = tcx.coverage_ids_info(instance_internal.def).unwrap(); - //let bcb_to_covterm = cov_ids_info.term_for_bcb.clone(); - // 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 { bcb } = mapping.kind else { unreachable!() }; - //let term = match bcb_to_covterm[bcb] { - // Some(term) => term, - // _ => CovTerm::Zero, - //}; let source_map = tcx.sess.source_map(); let file = source_map.lookup_source_file(cov_info.body_span.lo()); if bcb == coverage { @@ -289,7 +280,6 @@ pub mod rustc_smir { if let Some(rest) = coverage_str.strip_prefix("VirtualCounter(bcb") { let (num_str, _rest) = rest.split_once(')').unwrap(); let num = num_str.parse::().unwrap(); - println!("cover {:?}", num); BasicCoverageBlock::from_u32(num) } else { unreachable!(); diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 5411d1d863ef..92c82f25888d 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -501,7 +501,6 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option = OnceLock::new(); COUNTER_RE.get_or_init(|| { Regex::new( - //r#"^(?CounterIncrement|ExpressionUsed)\((?[0-9]+)\) \$(?[^\$]+)\$ - (?.+)"#, r#"^(?VirtualCounter\(bcb)(?[0-9]+)\) \$(?[^\$]+)\$ - (?.+)"#, ) .unwrap() @@ -512,21 +511,13 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option CoverageTerm::Counter(counter_id), - "ExpressionUsed" => CoverageTerm::Expression(counter_id), - _ => unreachable!("counter kind could not be recognized: {:?}", kind), - };*/ let term = CoverageTerm::Counter(counter_id); let region = CoverageRegion::from_str(span); From e20dd33b46460d5d240a837a04aeb7939c582be0 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 14 Feb 2025 10:16:00 -0800 Subject: [PATCH 6/8] remove Expression variant for CoverageKind and turn it into a struct --- .../src/codegen_cprover_gotoc/codegen/function.rs | 12 ++++-------- kani-driver/src/call_cbmc.rs | 2 +- kani-driver/src/coverage/cov_results.rs | 5 ++--- 3 files changed, 7 insertions(+), 12 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index d35e881f4674..ee3de03217c0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -240,7 +240,7 @@ pub mod rustc_smir { region_from_coverage(tcx, bcb, instance) } - /// Retrieves the `SourceRegion` associated with a `CovTerm` object. + /// Retrieves the `SourceRegion` associated with a `BasicCoverageBlock` object. /// /// Note: This function could be in the internal `rustc` impl for `Coverage`. pub fn region_from_coverage( @@ -268,13 +268,7 @@ pub mod rustc_smir { None } - /// Parse a `CoverageOpaque` item and return the corresponding `CovTerm`: - /// - /// - /// At present, a `CovTerm` can be one of the following: - /// - `CounterIncrement()`: A physical counter. - /// - `ExpressionUsed()`: An expression-based counter. - /// - `Zero`: A counter with a constant zero value. + /// Parse a `CoverageOpaque` item and return the corresponding `BasicCoverageBlock`: fn parse_coverage_opaque(coverage_opaque: &Opaque) -> BasicCoverageBlock { let coverage_str = coverage_opaque.to_string(); if let Some(rest) = coverage_str.strip_prefix("VirtualCounter(bcb") { @@ -282,6 +276,8 @@ pub mod rustc_smir { let num = num_str.parse::().unwrap(); BasicCoverageBlock::from_u32(num) } else { + // When the coverage statement is injected into mir_body, it always has the form CoverageKind::VirtualCounter { bcb } + // https://github.com/rust-lang/rust/pull/136053/files#diff-c99ec9a281dce4a381fa7e11cf2d04f55dba5573d1d14389d47929fe0a154d24R209-R212 unreachable!(); } } diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 92c82f25888d..ee92a5c495b6 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -518,7 +518,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option Date: Fri, 14 Feb 2025 12:47:27 -0800 Subject: [PATCH 7/8] change CoverageTerm back to enum --- kani-driver/src/call_cbmc.rs | 2 +- kani-driver/src/coverage/cov_results.rs | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index ee92a5c495b6..92c82f25888d 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -518,7 +518,7 @@ fn coverage_results_from_properties(properties: &[Property]) -> Option Date: Fri, 21 Feb 2025 10:03:21 -0800 Subject: [PATCH 8/8] Add comment back --- kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index ee3de03217c0..15a4e6357349 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -251,6 +251,9 @@ pub mod rustc_smir { // 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 {