Emit concurrency warning with macro

model-checking · Feb 11, 2022 · 8e87a06 · 8e87a06
1 parent 17e201d
commit 8e87a06
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 18 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,24 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! this module handles intrinsics
-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;
+use tracing::{debug, warn};
+
+macro_rules! emit_concurrency_warning {
+    ($intrinsic: expr, $loc: expr) => {{
+        warn!(
+            "Kani does not support concurrency for now. `{}` in {} treated as a sequential operation.",
+            $intrinsic,
+            $loc.short_string()
+        );
+    }};
+}
 
 struct SizeAlign {
     size: Expr,
@@ -280,7 +289,7 @@ impl<'tcx> GotocCtx<'tcx> {
         macro_rules! codegen_atomic_binop {
             ($op: ident) => {{
                 let loc = self.codegen_span_option(span);
-                emit_concurrency_warning(intrinsic, loc);
+                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();
@@ -519,7 +528,10 @@ impl<'tcx> GotocCtx<'tcx> {
             "volatile_copy_memory" => codegen_intrinsic_copy!(Memmove),
             "volatile_copy_nonoverlapping_memory" => codegen_intrinsic_copy!(Memcpy),
             "volatile_load" => self.codegen_expr_to_place(p, fargs.remove(0).dereference()),
-            "volatile_store" => self.codegen_volatile_store(instance, intrinsic, fargs, loc),
+            "volatile_store" => {
+                assert!(self.place_ty(p).is_unit());
+                self.codegen_volatile_store(instance, intrinsic, fargs, loc)
+            }
             "wrapping_add" => codegen_wrapping_op!(plus),
             "wrapping_mul" => codegen_wrapping_op!(mul),
             "wrapping_sub" => codegen_wrapping_op!(sub),
@@ -658,7 +670,7 @@ impl<'tcx> GotocCtx<'tcx> {
         p: &Place<'tcx>,
         loc: Location,
     ) -> Stmt {
-        emit_concurrency_warning(intrinsic, loc);
+        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);
@@ -686,7 +698,7 @@ impl<'tcx> GotocCtx<'tcx> {
         p: &Place<'tcx>,
         loc: Location,
     ) -> Stmt {
-        emit_concurrency_warning(intrinsic, loc);
+        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();
@@ -722,7 +734,7 @@ impl<'tcx> GotocCtx<'tcx> {
         p: &Place<'tcx>,
         loc: Location,
     ) -> Stmt {
-        emit_concurrency_warning(intrinsic, loc);
+        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();
@@ -735,7 +747,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);
+        emit_concurrency_warning!(intrinsic, loc);
         let skip_stmt = Stmt::skip(loc.clone());
         Stmt::atomic_block(vec![skip_stmt], loc)
     }
@@ -1008,7 +1020,7 @@ impl<'tcx> GotocCtx<'tcx> {
         mut fargs: Vec<Expr>,
         loc: Location,
     ) -> Stmt {
-        emit_concurrency_warning(intrinsic, loc);
+        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, ExprValue, Location, Stmt, SymbolTable, Type};
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::TyS;
-use tracing::{debug, warn};
+use tracing::debug;
 
 // Should move into rvalue
 //make this a member function
@@ -18,14 +18,6 @@ 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()
-    );
-}
-
 /// Tries to extract a string message from an `Expr`.
 /// If the expression represents a pointer to a string constant, this will return the string
 /// constant. Otherwise, return `None`.