Merge branch 'main' into issue-1915-cdylib

.github/workflows/kani.yml

@@ -96,7 +96,10 @@ jobs:
       - name: Print book runner text results
         run: cat build/output/latest/html/bookrunner.txt
 
-      - name: Detect unpexpected book runner failures
+      - name: Print book runner failures grouped by stage
+        run: python3 scripts/ci/bookrunner_failures_by_stage.py build/output/latest/html/index.html
+
+      - name: Detect unexpected book runner failures
         run: ./scripts/ci/detect_bookrunner_failures.sh build/output/latest/html/bookrunner.txt
 
       # On one OS only, build the documentation, too.

docs/src/rust-feature-support/intrinsics.md

@@ -252,16 +252,18 @@ code to be sequential.
 
 ### Platform intrinsics
 
+Intrinsics from [the `platform_intrinsics` feature](https://rust-lang.github.io/rfcs/1199-simd-infrastructure.html#operations).
+
 Name | Support | Notes |
 --- | --- | --- |
 `simd_add` | Yes | |
 `simd_and`  | Yes | |
 `simd_div`  | Yes | Doesn't check for overflow cases [#1970](https://github.com/model-checking/kani/issues/1970) |
 `simd_eq`  | Yes | |
-`simd_extract`  | No | |
+`simd_extract`  | Yes | |
 `simd_ge`  | Yes | |
 `simd_gt`  | Yes | |
-`simd_insert`  | No | |
+`simd_insert`  | Yes | |
 `simd_le`  | Yes | |
 `simd_lt`  | Yes | |
 `simd_mul`  | Yes | |

docs/src/rust-feature-support/unstable.md

@@ -7,4 +7,3 @@ The following are examples of unstable features that are not supported
 in Kani:
  * Generators
  * C-variadics
- * `repr(simd)` and related intrinsics

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

@@ -21,6 +21,7 @@
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
 use cbmc::InternedString;
+use kani_queries::UserInput;
 use rustc_span::Span;
 use std::convert::AsRef;
 use strum_macros::{AsRefStr, EnumString};
@@ -59,6 +60,9 @@ pub enum PropertyClass {
     ///
     /// SPECIAL BEHAVIOR: None TODO: Why should this exist?
     FiniteCheck,
+    /// Checks added by Kani compiler to determine whether a property (e.g.
+    /// `PropertyClass::Assertion` or `PropertyClass:Cover`) is reachable
+    ReachabilityCheck,
     /// Checks added by Kani compiler to detect safety conditions violation.
     /// E.g., things that trigger UB or unstable behavior.
     ///
@@ -134,9 +138,41 @@ impl<'tcx> GotocCtx<'tcx> {
     // The above represent the basic operations we can perform w.r.t. assert/assume/cover
     // Below are various helper functions for constructing the above more easily.
 
-    /// A shorthand for cover(true)
-    pub fn codegen_cover_loc(&self, msg: &str, span: Option<Span>) -> Stmt {
-        self.codegen_cover(Expr::bool_true(), msg, span)
+    /// Given the message for a property, generate a reachability check that is
+    /// meant to check whether the property is reachable. The function returns a
+    /// modified version of the provided message that should be used for the
+    /// property to allow the CBMC output parser to pair the property with its
+    /// reachability check.
+    /// If reachability checks are disabled, the function returns the message
+    /// unmodified and an empty (skip) statement.
+    pub fn codegen_reachability_check(
+        &mut self,
+        msg: String,
+        span: Option<Span>,
+    ) -> (String, Stmt) {
+        let loc = self.codegen_caller_span(&span);
+        if self.queries.get_check_assertion_reachability() {
+            // Generate a unique ID for the assert
+            let assert_id = self.next_check_id();
+            // Generate a message for the reachability check that includes the unique ID
+            let reach_msg = assert_id.clone();
+            // Also add the unique ID as a prefix to the assert message so that it can be
+            // easily paired with the reachability check
+            let msg = GotocCtx::add_prefix_to_msg(&msg, &assert_id);
+            // inject a reachability check, which is a (non-blocking)
+            // assert(false) whose failure indicates that this line is reachable.
+            // The property class (`PropertyClass:ReachabilityCheck`) is used by
+            // the CBMC output parser to distinguish those checks from others.
+            let check = self.codegen_assert(
+                Expr::bool_false(),
+                PropertyClass::ReachabilityCheck,
+                &reach_msg,
+                loc,
+            );
+            (msg, check)
+        } else {
+            (msg, Stmt::skip(loc))
+        }
     }
 
     /// A shorthand for generating a CBMC assert-assume(false)

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

@@ -6,7 +6,6 @@ use super::PropertyClass;
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
-use kani_queries::UserInput;
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir;
 use rustc_middle::mir::{
@@ -18,7 +17,7 @@ use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::{Instance, InstanceDef, Ty};
 use rustc_span::Span;
 use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants};
-use tracing::{debug, info_span, trace};
+use tracing::{debug, debug_span, trace};
 
 impl<'tcx> GotocCtx<'tcx> {
     /// Generate Goto-C for MIR [Statement]s.
@@ -27,7 +26,7 @@ impl<'tcx> GotocCtx<'tcx> {
     ///
     /// See [GotocCtx::codegen_terminator] for those.
     pub fn codegen_statement(&mut self, stmt: &Statement<'tcx>) -> Stmt {
-        let _trace_span = info_span!("CodegenStatement", statement = ?stmt).entered();
+        let _trace_span = debug_span!("CodegenStatement", statement = ?stmt).entered();
         debug!(?stmt, kind=?stmt.kind, "handling_statement");
         let location = self.codegen_span(&stmt.source_info.span);
         match &stmt.kind {
@@ -159,7 +158,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// See also [`GotocCtx::codegen_statement`] for ordinary [Statement]s.
     pub fn codegen_terminator(&mut self, term: &Terminator<'tcx>) -> Stmt {
         let loc = self.codegen_span(&term.source_info.span);
-        let _trace_span = info_span!("CodegenTerminator", statement = ?term.kind).entered();
+        let _trace_span = debug_span!("CodegenTerminator", statement = ?term.kind).entered();
         debug!("handling terminator {:?}", term);
         //TODO: Instead of doing location::none(), and updating, just putit in when we make the stmt.
         match &term.kind {
@@ -226,16 +225,8 @@ impl<'tcx> GotocCtx<'tcx> {
                     msg.description()
                 };
 
-                // TODO: switch to tagging assertions via the property class once CBMC allows that:
-                // https://github.com/diffblue/cbmc/issues/6692
-                let (msg_str, reach_stmt) = if self.queries.get_check_assertion_reachability() {
-                    let check_id = self.next_check_id();
-                    let msg_str = GotocCtx::add_prefix_to_msg(msg, &check_id);
-                    let reach_msg = GotocCtx::reachability_check_message(&check_id);
-                    (msg_str, self.codegen_cover_loc(&reach_msg, Some(term.source_info.span)))
-                } else {
-                    (msg.to_string(), Stmt::skip(loc))
-                };
+                let (msg_str, reach_stmt) =
+                    self.codegen_reachability_check(msg.to_owned(), Some(term.source_info.span));
 
                 Stmt::block(
                     vec![

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -12,7 +12,6 @@ use crate::codegen_cprover_gotoc::codegen::PropertyClass;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
-use kani_queries::UserInput;
 use rustc_middle::mir::{BasicBlock, Place};
 use rustc_middle::ty::print::with_no_trimmed_paths;
 use rustc_middle::ty::{Instance, TyCtxt};
@@ -75,14 +74,16 @@ impl<'tcx> GotocHook<'tcx> for Cover {
         let msg = tcx.extract_const_message(&msg).unwrap();
         let target = target.unwrap();
         let caller_loc = tcx.codegen_caller_span(&span);
-        let loc = tcx.codegen_span_option(span);
+
+        let (msg, reach_stmt) = tcx.codegen_reachability_check(msg, span);
 
         Stmt::block(
             vec![
+                reach_stmt,
                 tcx.codegen_cover(cond, &msg, span),
                 Stmt::goto(tcx.current_fn().find_label(&target), caller_loc),
             ],
-            loc,
+            caller_loc,
         )
     }
 }
@@ -139,20 +140,7 @@ impl<'tcx> GotocHook<'tcx> for Assert {
         let target = target.unwrap();
         let caller_loc = tcx.codegen_caller_span(&span);
 
-        // TODO: switch to tagging assertions via the property class once CBMC allows that:
-        // https://github.com/diffblue/cbmc/issues/6692
-        let (msg, reach_stmt) = if tcx.queries.get_check_assertion_reachability() {
-            // Generate a unique ID for the assert
-            let assert_id = tcx.next_check_id();
-            // Add this ID as a prefix to the assert message so that it can be
-            // easily paired with the reachability check
-            let msg = GotocCtx::add_prefix_to_msg(&msg, &assert_id);
-            let reach_msg = GotocCtx::reachability_check_message(&assert_id);
-            // inject a reachability (cover) check to the current location
-            (msg, tcx.codegen_cover_loc(&reach_msg, span))
-        } else {
-            (msg, Stmt::skip(caller_loc))
-        };
+        let (msg, reach_stmt) = tcx.codegen_reachability_check(msg, span);
 
         // Since `cond` might have side effects, assign it to a temporary
         // variable so that it's evaluated once, then assert and assume it

kani-compiler/src/codegen_cprover_gotoc/utils/names.rs

@@ -117,15 +117,6 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn add_prefix_to_msg(msg: &str, prefix: &str) -> String {
         format!("[{prefix}] {msg}")
     }
-
-    /// Generate a message for the reachability check of an assert with ID
-    /// `check_id`. The message is of the form:
-    /// \[KANI_REACHABILITY_CHECK\] `<ID of assert>`
-    /// The check_id is generated using the GotocCtx::next_check_id method and
-    /// is a unique string identifier for that check.
-    pub fn reachability_check_message(check_id: &str) -> String {
-        format!("[KANI_REACHABILITY_CHECK] {check_id}")
-    }
 }
 
 /// The full crate name should use the Codegen Unit builder to include full name resolution,

kani-driver/src/cbmc_property_renderer.rs

@@ -151,7 +151,6 @@ static CBMC_ALT_DESCRIPTIONS: Lazy<CbmcAltDescriptions> = Lazy::new(|| {
 const UNSUPPORTED_CONSTRUCT_DESC: &str = "is not currently supported by Kani";
 const UNWINDING_ASSERT_DESC: &str = "unwinding assertion loop";
 const DEFAULT_ASSERTION: &str = "assertion";
-const REACH_CHECK_DESC: &str = "[KANI_REACHABILITY_CHECK]";
 
 impl ParserItem {
     /// Determines if an item must be skipped or not.
@@ -591,6 +590,9 @@ fn update_properties_with_reach_status(
 /// fails, then the cover property is satisfied and vice versa.
 /// - SUCCESS -> UNSATISFIABLE
 /// - FAILURE -> SATISFIED
+/// Note that if the cover property was unreachable, its status at this point
+/// will be `CheckStatus::Unreachable` and not `CheckStatus::Success` since
+/// `update_properties_with_reach_status` is called beforehand
 fn update_results_of_cover_checks(mut properties: Vec<Property>) -> Vec<Property> {
     for prop in properties.iter_mut() {
         if prop.is_cover_property() {
@@ -622,25 +624,12 @@ fn remove_check_ids_from_description(mut properties: Vec<Property>) -> Vec<Prope
     properties
 }
 
-/// Given a description, this splits properties into two groups:
-///  1. Properties that don't contain the description
-///  2. Properties that contain the description
-fn filter_properties(properties: Vec<Property>, message: &str) -> (Vec<Property>, Vec<Property>) {
-    let mut filtered_properties = Vec::<Property>::new();
-    let mut removed_properties = Vec::<Property>::new();
-    for prop in properties {
-        if prop.description.contains(message) {
-            removed_properties.push(prop);
-        } else {
-            filtered_properties.push(prop);
-        }
-    }
-    (filtered_properties, removed_properties)
-}
-
-/// Filters reachability checks with `filter_properties`
+/// Partitions `properties` into reachability checks (identified by the
+/// "reachability_check" property class) and non-reachability checks
 fn filter_reach_checks(properties: Vec<Property>) -> (Vec<Property>, Vec<Property>) {
-    filter_properties(properties, REACH_CHECK_DESC)
+    let (reach_checks, other_checks): (Vec<_>, Vec<_>) =
+        properties.into_iter().partition(|prop| prop.property_class() == "reachability_check");
+    (other_checks, reach_checks)
 }
 
 /// Filters out Kani-generated sanity checks with a `SUCCESS` status
@@ -680,11 +669,11 @@ fn filter_ptr_checks(properties: Vec<Property>) -> Vec<Property> {
 /// includes the ID of the assert for which we want to check its reachability.
 /// The description of a reachability check uses the following template:
 /// ```text
-/// [KANI_REACHABILITY_CHECK] <ID of original assert>
+/// <ID of original assert>
 /// ```
 /// e.g.:
 /// ```text
-/// [KANI_REACHABILITY_CHECK] KANI_CHECK_ID_foo.6875c808::foo_0
+/// KANI_CHECK_ID_foo.6875c808::foo_0
 /// ```
 /// This function first collects all data from reachability checks. Then,
 /// it updates the reachability status for all properties accordingly.

library/kani/src/lib.rs

@@ -78,6 +78,7 @@ pub const fn assert(_cond: bool, _msg: &'static str) {
 /// Cover properties are reported as:
 ///  - SATISFIED: if Kani found an execution that satisfies the condition
 ///  - UNSATISFIABLE: if Kani proved that the condition cannot be satisfied
+///  - UNREACHABLE: if Kani proved that the cover property itself is unreachable (i.e. it is vacuously UNSATISFIABLE)
 ///
 /// This function is called by the [`cover!`] macro. The macro is more
 /// convenient to use.
@@ -135,7 +136,13 @@ pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
 #[inline(never)]
 #[allow(dead_code)]
 fn any_raw_inner<T>() -> T {
-    unimplemented!("Kani any_raw_inner");
+    // while we could use `unreachable!()` or `panic!()` as the body of this
+    // function, both cause Kani to produce a warning on any program that uses
+    // kani::any() (see https://github.com/model-checking/kani/issues/2010).
+    // This function is handled via a hook anyway, so we just need to put a body
+    // that rustc does not complain about. An infinite loop works out nicely.
+    #[allow(clippy::empty_loop)]
+    loop {}
 }
 
 /// Function used to generate panic with a static message as this is the only one currently

scripts/ci/bookrunner_failures_by_stage.py

@@ -0,0 +1,36 @@
+#!/usr/bin/python3
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+import argparse
+from bs4 import BeautifulSoup
+
+def main():
+    parser = argparse.ArgumentParser(
+        description='Scans an HTML dashboard file and prints'
+                    'the number of failures grouped by stage')
+    parser.add_argument('input')
+    args = parser.parse_args()
+
+    with open(args.input) as fp:
+        run = BeautifulSoup(fp, 'html.parser')
+
+    failures = [0] * 3
+
+    for row in run.find_all('div', attrs={'class': 'pipeline-row'}):
+        stages = row.find_all('div', attrs={'class': 'pipeline-stage'})
+        i = 0
+        for stage in stages:
+            if stage.a['class'][1] == 'fail':
+                failures[i] += 1
+                break
+            i += 1
+
+    print('bookrunner failures grouped by stage:')
+    print(' * rustc-compilation: ' + str(failures[0]))
+    print(' * kani-codegen: ' + str(failures[1]))
+    print(' * cbmc-verification: ' + str(failures[2]))
+
+
+if __name__ == "__main__":
+    main()

tests/expected/cover/cover-fail/expected

@@ -1,6 +1,6 @@
 Status: UNSATISFIABLE\
-Description: "cover location"\
-main.rs:29:23 in function cover_overconstrained
+Description: "cover condition: x != 0"\
+in function cover_overconstrained
 
  ** 0 of 1 cover properties satisfied
 

tests/expected/cover/cover-fail/main.rs

@@ -22,11 +22,10 @@ fn get_sign(x: i32) -> Sign {
 #[kani::proof]
 fn cover_overconstrained() {
     let x: i32 = kani::any();
-    kani::assume(x != 0);
     let sign = get_sign(x);
 
     match sign {
-        Sign::Zero => kani::cover!(),
+        Sign::Zero => kani::cover!(x != 0),
         _ => {}
     }
 }

tests/expected/cover/cover-unreachable/expected

@@ -0,0 +1,16 @@
+Status: UNREACHABLE\
+Description: "cover condition: x == 2"\
+in function cover_unreachable
+
+Status: UNREACHABLE\
+Description: "Unreachable with a message"\
+in function cover_unreachable
+
+Status: SATISFIED\
+Description: "cover condition: x == 5"\
+in function cover_unreachable
+
+
+ ** 1 of 3 cover properties satisfied (2 unreachable)
+
+VERIFICATION:- SUCCESSFUL