Implement SourceRegion locally in Kani

The original SourceRegion was moved to the llvm backend and made
private by rust-lang/rust#134497.
We implement our own local version of it to maintain our handling
of SourceRegion for coverage properties.

Author: Remi Delmas

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

@@ -18,10 +18,10 @@
 //! 7. `codegen_sanity` : `assert` but not normally displayed as failure would be a Kani bug
 //!
 
+use super::source_region::SourceRegion;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::InternedString;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
-use rustc_middle::mir::coverage::SourceRegion;
 use stable_mir::mir::{Place, ProjectionElem};
 use stable_mir::ty::{Span as SpanStable, Ty};
 use strum_macros::{AsRefStr, EnumString};

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

@@ -218,10 +218,10 @@ 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::SourceRegion;
     use rustc_middle::ty::TyCtxt;
     use rustc_smir::rustc_internal;
     use stable_mir::mir::mono::Instance;
@@ -258,9 +258,12 @@ pub mod rustc_smir {
             // 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 source_map = tcx.sess.source_map();
+                let file = source_map.lookup_source_file(cov_info.body_span.lo());
                 if term == coverage {
                     return Some((
-                        mapping.source_region.clone(),
+                        make_source_region(source_map, cov_info, &file, mapping.span.clone())
+                            .unwrap(),
                         rustc_internal::stable(cov_info.body_span).get_filename(),
                     ));
                 }

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

@@ -12,6 +12,7 @@ mod intrinsic;
 mod operand;
 mod place;
 mod rvalue;
+mod source_region;
 mod span;
 mod statement;
 mod static_var;

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

@@ -0,0 +1,135 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This file contains our own local version of
+//! the `Span` to `CoverageRegion` conversion defined in
+//! https://github.com/rust-lang/rust/tree/master/compiler/rustc_codegen_llvm/src/coverageinfo/mapgen/spans.rs
+
+use rustc_middle::mir::coverage::FunctionCoverageInfo;
+use rustc_span::Span;
+use rustc_span::source_map::SourceMap;
+use rustc_span::{BytePos, SourceFile};
+use std::fmt::{self, Debug, Formatter};
+use tracing::debug;
+
+#[derive(Clone, Hash, PartialEq, Eq, PartialOrd, Ord)]
+pub struct SourceRegion {
+    pub start_line: u32,
+    pub start_col: u32,
+    pub end_line: u32,
+    pub end_col: u32,
+}
+
+impl Debug for SourceRegion {
+    fn fmt(&self, fmt: &mut Formatter<'_>) -> fmt::Result {
+        let &Self { start_line, start_col, end_line, end_col } = self;
+        write!(fmt, "{start_line}:{start_col} - {end_line}:{end_col}")
+    }
+}
+
+fn ensure_non_empty_span(
+    source_map: &SourceMap,
+    fn_cov_info: &FunctionCoverageInfo,
+    span: Span,
+) -> Option<Span> {
+    if !span.is_empty() {
+        return Some(span);
+    }
+    let lo = span.lo();
+    let hi = span.hi();
+    // The span is empty, so try to expand it to cover an adjacent '{' or '}',
+    // but only within the bounds of the body span.
+    let try_next = hi < fn_cov_info.body_span.hi();
+    let try_prev = fn_cov_info.body_span.lo() < lo;
+    if !(try_next || try_prev) {
+        return None;
+    }
+    source_map
+        .span_to_source(span, |src, start, end| try {
+            // Adjusting span endpoints by `BytePos(1)` is normally a bug,
+            // but in this case we have specifically checked that the character
+            // we're skipping over is one of two specific ASCII characters, so
+            // adjusting by exactly 1 byte is correct.
+            if try_next && src.as_bytes()[end] == b'{' {
+                Some(span.with_hi(hi + BytePos(1)))
+            } else if try_prev && src.as_bytes()[start - 1] == b'}' {
+                Some(span.with_lo(lo - BytePos(1)))
+            } else {
+                None
+            }
+        })
+        .ok()?
+}
+
+/// If `llvm-cov` sees a source region that is improperly ordered (end < start),
+/// it will immediately exit with a fatal error. To prevent that from happening,
+/// discard regions that are improperly ordered, or might be interpreted in a
+/// way that makes them improperly ordered.
+fn check_source_region(source_region: SourceRegion) -> Option<SourceRegion> {
+    let SourceRegion { start_line, start_col, end_line, end_col } = source_region;
+    // Line/column coordinates are supposed to be 1-based. If we ever emit
+    // coordinates of 0, `llvm-cov` might misinterpret them.
+    let all_nonzero = [start_line, start_col, end_line, end_col].into_iter().all(|x| x != 0);
+    // Coverage mappings use the high bit of `end_col` to indicate that a
+    // region is actually a "gap" region, so make sure it's unset.
+    let end_col_has_high_bit_unset = (end_col & (1 << 31)) == 0;
+    // If a region is improperly ordered (end < start), `llvm-cov` will exit
+    // with a fatal error, which is inconvenient for users and hard to debug.
+    let is_ordered = (start_line, start_col) <= (end_line, end_col);
+    if all_nonzero && end_col_has_high_bit_unset && is_ordered {
+        Some(source_region)
+    } else {
+        debug!(
+            ?source_region,
+            ?all_nonzero,
+            ?end_col_has_high_bit_unset,
+            ?is_ordered,
+            "Skipping source region that would be misinterpreted or rejected by LLVM"
+        );
+        // If this happens in a debug build, ICE to make it easier to notice.
+        debug_assert!(false, "Improper source region: {source_region:?}");
+        None
+    }
+}
+
+/// Converts the span into its start line and column, and end line and column.
+///
+/// Line numbers and column numbers are 1-based. Unlike most column numbers emitted by
+/// the compiler, these column numbers are denoted in **bytes**, because that's what
+/// LLVM's `llvm-cov` tool expects to see in coverage maps.
+///
+/// Returns `None` if the conversion failed for some reason. This shouldn't happen,
+/// but it's hard to rule out entirely (especially in the presence of complex macros
+/// or other expansions), and if it does happen then skipping a span or function is
+/// better than an ICE or `llvm-cov` failure that the user might have no way to avoid.
+pub(crate) fn make_source_region(
+    source_map: &SourceMap,
+    fn_cov_info: &FunctionCoverageInfo,
+    file: &SourceFile,
+    span: Span,
+) -> Option<SourceRegion> {
+    let span = ensure_non_empty_span(source_map, fn_cov_info, span)?;
+    let lo = span.lo();
+    let hi = span.hi();
+    // Column numbers need to be in bytes, so we can't use the more convenient
+    // `SourceMap` methods for looking up file coordinates.
+    let line_and_byte_column = |pos: BytePos| -> Option<(usize, usize)> {
+        let rpos = file.relative_position(pos);
+        let line_index = file.lookup_line(rpos)?;
+        let line_start = file.lines()[line_index];
+        // Line numbers and column numbers are 1-based, so add 1 to each.
+        Some((line_index + 1, ((rpos - line_start).0 as usize) + 1))
+    };
+    let (mut start_line, start_col) = line_and_byte_column(lo)?;
+    let (mut end_line, end_col) = line_and_byte_column(hi)?;
+    // Apply an offset so that code in doctests has correct line numbers.
+    // FIXME(#79417): Currently we have no way to offset doctest _columns_.
+    start_line = source_map.doctest_offset_line(&file.name, start_line);
+    end_line = source_map.doctest_offset_line(&file.name, end_line);
+    check_source_region(SourceRegion {
+        start_line: start_line as u32,
+        start_col: start_col as u32,
+        end_line: end_line as u32,
+        end_col: end_col as u32,
+    })
+}

kani-compiler/src/main.rs

@@ -17,6 +17,7 @@
 #![feature(f16)]
 #![feature(non_exhaustive_omitted_patterns_lint)]
 #![feature(float_next_up_down)]
+#![feature(try_blocks)]
 extern crate rustc_abi;
 extern crate rustc_ast;
 extern crate rustc_ast_pretty;