Join and format warnings about concurrent constructs

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

@@ -13,22 +13,7 @@ use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::{self, Ty};
 use rustc_middle::ty::{Instance, InstanceDef};
 use rustc_span::Span;
-use tracing::{debug, warn};
-
-#[macro_export]
-macro_rules! emit_concurrency_warning {
-    ($intrinsic: expr, $loc: expr) => {{
-        emit_concurrency_warning!($intrinsic, $loc, "a sequential operation");
-    }};
-    ($intrinsic: expr, $loc: expr, $treated_as: expr) => {{
-        warn!(
-            "Kani does not support concurrency for now. `{}` in {} treated as {}.",
-            $intrinsic,
-            $loc.short_string(),
-            $treated_as,
-        );
-    }};
-}
+use tracing::debug;
 
 struct SizeAlign {
     size: Expr,
@@ -345,7 +330,7 @@ impl<'tcx> GotocCtx<'tcx> {
         macro_rules! codegen_atomic_binop {
             ($op: ident) => {{
                 let loc = self.codegen_span_option(span);
-                emit_concurrency_warning!(intrinsic, loc);
+                self.store_concurrent_construct(intrinsic, loc);
                 let var1_ref = fargs.remove(0);
                 let var1 = var1_ref.dereference();
                 let (tmp, decl_stmt) =
@@ -833,7 +818,7 @@ impl<'tcx> GotocCtx<'tcx> {
         p: &Place<'tcx>,
         loc: Location,
     ) -> Stmt {
-        emit_concurrency_warning!(intrinsic, loc);
+        self.store_concurrent_construct(intrinsic, loc);
         let var1_ref = fargs.remove(0);
         let var1 = var1_ref.dereference().with_location(loc);
         let res_stmt = self.codegen_expr_to_place(p, var1);
@@ -861,7 +846,7 @@ impl<'tcx> GotocCtx<'tcx> {
         p: &Place<'tcx>,
         loc: Location,
     ) -> Stmt {
-        emit_concurrency_warning!(intrinsic, loc);
+        self.store_concurrent_construct(intrinsic, loc);
         let var1_ref = fargs.remove(0);
         let var1 = var1_ref.dereference().with_location(loc);
         let (tmp, decl_stmt) =
@@ -897,7 +882,7 @@ impl<'tcx> GotocCtx<'tcx> {
         p: &Place<'tcx>,
         loc: Location,
     ) -> Stmt {
-        emit_concurrency_warning!(intrinsic, loc);
+        self.store_concurrent_construct(intrinsic, loc);
         let var1_ref = fargs.remove(0);
         let var1 = var1_ref.dereference().with_location(loc);
         let (tmp, decl_stmt) =
@@ -910,7 +895,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// Atomic no-ops (e.g., atomic_fence) are transformed into SKIP statements
     fn codegen_atomic_noop(&mut self, intrinsic: &str, loc: Location) -> Stmt {
-        emit_concurrency_warning!(intrinsic, loc);
+        self.store_concurrent_construct(intrinsic, loc);
         let skip_stmt = Stmt::skip(loc);
         Stmt::atomic_block(vec![skip_stmt], loc)
     }

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

@@ -8,7 +8,7 @@ use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use crate::kani_middle::coercion::{
     extract_unsize_casting, CoerceUnsizedInfo, CoerceUnsizedIterator, CoercionBase,
 };
-use crate::{emit_concurrency_warning, unwrap_or_return_codegen_unimplemented};
+use crate::unwrap_or_return_codegen_unimplemented;
 use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
 use cbmc::MachineModel;
 use cbmc::{btree_string_map, InternString, InternedString};
@@ -408,7 +408,7 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             Rvalue::ThreadLocalRef(def_id) => {
                 // Since Kani is single-threaded, we treat a thread local like a static variable:
-                emit_concurrency_warning!("thread local", loc, "a static variable");
+                self.store_concurrent_construct("thread local (replaced by static variable)", loc);
                 self.codegen_static_pointer(*def_id, true)
             }
             // A CopyForDeref is equivalent to a read from a place at the codegen level.

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -339,6 +339,17 @@ fn print_report(ctx: &GotocCtx, tcx: TyCtxt) {
         details.";
         tcx.sess.warn(&msg);
     }
+
+    if !ctx.concurrent_constructs.is_empty() {
+        let mut msg = String::from(
+            "Kani currently does not support concurrency. The following constructs will be treated \
+            as sequential operations:\n",
+        );
+        for (construct, locations) in ctx.concurrent_constructs.iter() {
+            writeln!(&mut msg, "    - {construct} ({})", locations.len()).unwrap();
+        }
+        tcx.sess.warn(&msg);
+    }
 }
 
 /// Return a struct that contains information about the codegen results as expected by `rustc`.

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -71,6 +71,10 @@ pub struct GotocCtx<'tcx> {
     pub global_checks_count: u64,
     /// A map of unsupported constructs that were found while codegen
     pub unsupported_constructs: FxHashMap<InternedString, Vec<Location>>,
+    /// A map of concurrency constructs that are treated sequentially.
+    /// We collect them and print one warning at the end if not empty instead of printing one
+    /// warning at each occurrence.
+    pub concurrent_constructs: FxHashMap<InternedString, Vec<Location>>,
 }
 
 /// Constructor
@@ -96,6 +100,7 @@ impl<'tcx> GotocCtx<'tcx> {
             test_harnesses: vec![],
             global_checks_count: 0,
             unsupported_constructs: FxHashMap::default(),
+            concurrent_constructs: FxHashMap::default(),
         }
     }
 }

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

@@ -3,10 +3,11 @@
 use super::super::codegen::TypeExt;
 use crate::codegen_cprover_gotoc::codegen::typ::{is_pointer, pointee_type};
 use crate::codegen_cprover_gotoc::GotocCtx;
-use cbmc::btree_string_map;
-use cbmc::goto_program::{Expr, ExprValue, SymbolTable, Type};
+use cbmc::goto_program::{Expr, ExprValue, Location, SymbolTable, Type};
+use cbmc::{btree_string_map, InternedString};
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::{Instance, Ty};
+use tracing::debug;
 
 // Should move into rvalue
 //make this a member function
@@ -66,6 +67,20 @@ impl<'tcx> GotocCtx<'tcx> {
             _ => None,
         }
     }
+
+    /// Store an occurrence of a concurrent construct that was treated as a sequential operation.
+    ///
+    /// Kani does not currently support concurrency and the compiler assumes that when generating
+    /// code for some specialized concurrent constructs that this is the case. We store all types of
+    /// operations that had this special handling and print a warning at the end of the compilation.
+    pub fn store_concurrent_construct(&mut self, operation_name: &str, loc: Location) {
+        debug!(op=?operation_name, location=?loc.short_string(), "store_seq_construct");
+
+        // Save this occurrence so we can emit a warning in the compilation report.
+        let key: InternedString = operation_name.into();
+        let entry = self.concurrent_constructs.entry(key).or_default();
+        entry.push(loc);
+    }
 }
 
 /// Members traverse path to get to the raw pointer of a box (b.0.pointer.pointer).