Create util function for concurrency warnings

model-checking · Feb 4, 2022 · a4910a6 · a4910a6
1 parent b33a6e9
commit a4910a6
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 24 deletions.
diff --git a/src/kani-compiler/rustc_codegen_kani/src/codegen/intrinsic.rs b/src/kani-compiler/rustc_codegen_kani/src/codegen/intrinsic.rs
@@ -1,15 +1,15 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! this module handles intrinsics
-use tracing::{debug, warn};
-
+use crate::utils::emit_concurrency_warning;
 use crate::GotocCtx;
 use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
 use rustc_middle::mir::Place;
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::Instance;
 use rustc_middle::ty::{self, Ty, TyS};
 use rustc_span::Span;
+use tracing::debug;
 
 struct SizeAlign {
     size: Expr,
@@ -279,8 +279,8 @@ impl<'tcx> GotocCtx<'tcx> {
         // Note: Atomic arithmetic operations wrap around on overflow.
         macro_rules! codegen_atomic_binop {
             ($op: ident) => {{
-                warn!("Kani does not support concurrency for now. {} treated as a sequential operation.", intrinsic);
                 let loc = self.codegen_span_option(span);
+                emit_concurrency_warning(intrinsic, loc);
                 let var1_ref = fargs.remove(0);
                 let var1 = var1_ref.dereference();
                 let tmp = self.gen_temp_variable(var1.typ().clone(), loc.clone()).to_expr();
@@ -616,10 +616,7 @@ impl<'tcx> GotocCtx<'tcx> {
         p: &Place<'tcx>,
         loc: Location,
     ) -> Stmt {
-        warn!(
-            "Kani does not support concurrency for now. {} treated as a sequential operation.",
-            intrinsic
-        );
+        emit_concurrency_warning(intrinsic, loc);
         let var1_ref = fargs.remove(0);
         let var1 = var1_ref.dereference().with_location(loc.clone());
         let res_stmt = self.codegen_expr_to_place(p, var1);
@@ -647,10 +644,7 @@ impl<'tcx> GotocCtx<'tcx> {
         p: &Place<'tcx>,
         loc: Location,
     ) -> Stmt {
-        warn!(
-            "Kani does not support concurrency for now. {} treated as a sequential operation.",
-            intrinsic
-        );
+        emit_concurrency_warning(intrinsic, loc);
         let var1_ref = fargs.remove(0);
         let var1 = var1_ref.dereference().with_location(loc.clone());
         let tmp = self.gen_temp_variable(var1.typ().clone(), loc.clone()).to_expr();
@@ -686,10 +680,7 @@ impl<'tcx> GotocCtx<'tcx> {
         p: &Place<'tcx>,
         loc: Location,
     ) -> Stmt {
-        warn!(
-            "Kani does not support concurrency for now. {} treated as a sequential operation.",
-            intrinsic
-        );
+        emit_concurrency_warning(intrinsic, loc);
         let var1_ref = fargs.remove(0);
         let var1 = var1_ref.dereference().with_location(loc.clone());
         let tmp = self.gen_temp_variable(var1.typ().clone(), loc.clone()).to_expr();
@@ -702,10 +693,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 {
-        warn!(
-            "Kani does not support concurrency for now. {} treated as a sequential operation.",
-            intrinsic
-        );
+        emit_concurrency_warning(intrinsic, loc);
         let skip_stmt = Stmt::skip(loc.clone());
         Stmt::atomic_block(vec![skip_stmt], loc)
     }
@@ -978,10 +966,7 @@ impl<'tcx> GotocCtx<'tcx> {
         mut fargs: Vec<Expr>,
         loc: Location,
     ) -> Stmt {
-        warn!(
-            "Kani does not support concurrency for now. {} treated as a sequential operation.",
-            intrinsic
-        );
+        emit_concurrency_warning(intrinsic, loc);
         let dst = fargs.remove(0);
         let src = fargs.remove(0);
         let typ = instance.substs.type_at(0);

diff --git a/src/kani-compiler/rustc_codegen_kani/src/utils/utils.rs b/src/kani-compiler/rustc_codegen_kani/src/utils/utils.rs
@@ -6,7 +6,7 @@ use cbmc::btree_string_map;
 use cbmc::goto_program::{Expr, Location, Stmt, SymbolTable, Type};
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::TyS;
-use tracing::debug;
+use tracing::{debug, warn};
 
 // Should move into rvalue
 //make this a member function
@@ -18,6 +18,14 @@ pub fn dynamic_fat_ptr(typ: Type, data: Expr, vtable: Expr, symbol_table: &Symbo
     Expr::struct_expr(typ, btree_string_map![("data", data), ("vtable", vtable)], symbol_table)
 }
 
+pub fn emit_concurrency_warning(intrinsic: &str, loc: Location) {
+    warn!(
+        "Kani does not support concurrency for now. `{}` in {} treated as a sequential operation.",
+        intrinsic,
+        loc.short_string()
+    );
+}
+
 impl<'tcx> GotocCtx<'tcx> {
     /// Kani does not currently support all MIR constructs.
     /// When we hit a construct we don't handle, we have two choices: