Support for disabling automatically generated pointer checks to avoid reinstrumentation

cprover_bindings/src/goto_program/location.rs

@@ -19,6 +19,7 @@ pub enum Location {
         start_col: Option<u64>,
         end_line: u64,
         end_col: Option<u64>,
+        pragmas: &'static [&'static str], // CBMC `#pragma check` statements per location.
     },
     /// Location for Statements that use Property Class and Description - Assert, Assume, Cover etc.
     Property {
@@ -28,6 +29,7 @@ pub enum Location {
         col: Option<u64>,
         comment: InternedString,
         property_class: InternedString,
+        pragmas: &'static [&'static str], // CBMC `#pragma check` statements per location.
     },
     /// Covers cases where Location Details are unknown or set as None but Property Class is needed.
     PropertyUnknownLocation { comment: InternedString, property_class: InternedString },
@@ -99,6 +101,7 @@ impl Location {
         start_col: Option<T>,
         end_line: T,
         end_col: Option<T>,
+        pragmas: &'static [&'static str],
     ) -> Location
     where
         T: TryInto<u64>,
@@ -117,6 +120,7 @@ impl Location {
             start_col: start_col_into,
             end_line: end_line_into,
             end_col: end_col_into,
+            pragmas,
         }
     }
 
@@ -128,6 +132,7 @@ impl Location {
         col: Option<T>,
         comment: U,
         property_name: U,
+        pragmas: &'static [&'static str],
     ) -> Location
     where
         T: TryInto<u64>,
@@ -140,7 +145,7 @@ impl Location {
         let function = function.intern();
         let property_class = property_name.into();
         let comment = comment.into();
-        Location::Property { file, function, line, col, comment, property_class }
+        Location::Property { file, function, line, col, comment, property_class, pragmas }
     }
 
     /// Create a Property type Location from an already existing Location type
@@ -157,17 +162,25 @@ impl Location {
                 None,
                 comment.into(),
                 property_name.into(),
+                &[],
+            ),
+            Location::Loc {
+                file,
+                function,
+                start_line,
+                start_col,
+                end_line: _,
+                end_col: _,
+                pragmas,
+            } => Location::property_location(
+                file.into(),
+                function.intern(),
+                start_line,
+                start_col,
+                comment.into(),
+                property_name.into(),
+                pragmas,
             ),
-            Location::Loc { file, function, start_line, start_col, end_line: _, end_col: _ } => {
-                Location::property_location(
-                    file.into(),
-                    function.intern(),
-                    start_line,
-                    start_col,
-                    comment.into(),
-                    property_name.into(),
-                )
-            }
             Location::Property { .. } => location,
             Location::PropertyUnknownLocation { .. } => location,
             // This converts None type Locations to PropertyUnknownLocation type which inserts Property Class and Description

cprover_bindings/src/irep/to_irep.rs

@@ -389,15 +389,32 @@ impl ToIrep for Location {
                 (IrepId::Function, Irep::just_string_id(function_name.to_string())),
             ])
             .with_named_sub_option(IrepId::Line, line.map(Irep::just_int_id)),
-            Location::Loc { file, function, start_line, start_col, end_line: _, end_col: _ } => {
-                Irep::just_named_sub(linear_map![
-                    (IrepId::File, Irep::just_string_id(file.to_string())),
-                    (IrepId::Line, Irep::just_int_id(*start_line)),
-                ])
-                .with_named_sub_option(IrepId::Column, start_col.map(Irep::just_int_id))
-                .with_named_sub_option(IrepId::Function, function.map(Irep::just_string_id))
-            }
-            Location::Property { file, function, line, col, property_class, comment } => {
+            Location::Loc {
+                file,
+                function,
+                start_line,
+                start_col,
+                end_line: _,
+                end_col: _,
+                pragmas,
+            } => Irep::just_named_sub(linear_map![
+                (IrepId::File, Irep::just_string_id(file.to_string())),
+                (IrepId::Line, Irep::just_int_id(*start_line)),
+            ])
+            .with_named_sub_option(IrepId::Column, start_col.map(Irep::just_int_id))
+            .with_named_sub_option(IrepId::Function, function.map(Irep::just_string_id))
+            .with_named_sub_option(
+                IrepId::Pragma,
+                Some(Irep::just_named_sub(
+                    pragmas
+                        .iter()
+                        .map(|pragma| {
+                            (IrepId::from_string(*pragma), Irep::just_id(IrepId::EmptyString))
+                        })
+                        .collect(),
+                )),
+            ),
+            Location::Property { file, function, line, col, property_class, comment, pragmas } => {
                 Irep::just_named_sub(linear_map![
                     (IrepId::File, Irep::just_string_id(file.to_string())),
                     (IrepId::Line, Irep::just_int_id(*line)),
@@ -409,6 +426,17 @@ impl ToIrep for Location {
                     IrepId::PropertyClass,
                     Irep::just_string_id(property_class.to_string()),
                 )
+                .with_named_sub_option(
+                    IrepId::Pragma,
+                    Some(Irep::just_named_sub(
+                        pragmas
+                            .iter()
+                            .map(|pragma| {
+                                (IrepId::from_string(*pragma), Irep::just_id(IrepId::EmptyString))
+                            })
+                            .collect(),
+                    )),
+                )
             }
             Location::PropertyUnknownLocation { property_class, comment } => {
                 Irep::just_named_sub(linear_map![

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

@@ -5,16 +5,68 @@
 
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Location;
+use lazy_static::lazy_static;
+use rustc_ast::Attribute;
 use rustc_smir::rustc_internal;
 use rustc_span::Span;
 use stable_mir::ty::Span as SpanStable;
+use std::collections::HashMap;
+
+lazy_static! {
+    /// Pragmas key-value store to prevent CBMC from generating automatic checks.
+    /// This list is taken from https://github.com/diffblue/cbmc/blob/develop/regression/cbmc/pragma_cprover_enable_all/main.c.
+    static ref PRAGMAS: HashMap<&'static str, &'static str> =
+        [("bounds", "disable:bounds-check"),
+         ("pointer", "disable:pointer-check"),
+         ("div-by-zero", "disable:div-by-zero-check"),
+         ("float-div-by-zero", "disable:float-div-by-zero-check"),
+         ("enum-range", "disable:enum-range-check"),
+         ("signed-overflow", "disable:signed-overflow-check"),
+         ("unsigned-overflow", "disable:unsigned-overflow-check"),
+         ("pointer-overflow", "disable:pointer-overflow-check"),
+         ("float-overflow", "disable:float-overflow-check"),
+         ("conversion", "disable:conversion-check"),
+         ("undefined-shift", "disable:undefined-shift-check"),
+         ("nan", "disable:nan-check"),
+         ("pointer-primitive", "disable:pointer-primitive-check")].iter().copied().collect();
+}
 
 impl<'tcx> GotocCtx<'tcx> {
     pub fn codegen_span(&self, sp: &Span) -> Location {
         self.codegen_span_stable(rustc_internal::stable(sp))
     }
 
     pub fn codegen_span_stable(&self, sp: SpanStable) -> Location {
+        // Attribute to mark functions as where automatic pointer checks should not be generated.
+        let should_skip_ptr_checks_attr = vec![
+            rustc_span::symbol::Symbol::intern("kanitool"),
+            rustc_span::symbol::Symbol::intern("disable_checks"),
+        ];
+        let pragmas: &'static [&str] = {
+            let disabled_checks: Vec<_> = self
+                .current_fn
+                .as_ref()
+                .map(|current_fn| {
+                    let instance = current_fn.instance();
+                    self.tcx
+                        .get_attrs_by_path(instance.def.def_id(), &should_skip_ptr_checks_attr)
+                        .collect()
+                })
+                .unwrap_or_default();
+            disabled_checks
+                .iter()
+                .map(|attr| {
+                    let arg = parse_word(attr).expect(
+                        "incorrect value passed to `disable_checks`, expected a single identifier",
+                    );
+                    *PRAGMAS.get(arg.as_str()).expect(format!(
+                        "attempting to disable an unexisting check, the possible options are {:?}",
+                        PRAGMAS.keys()
+                    ).as_str())
+                })
+                .collect::<Vec<_>>()
+                .leak() // This is to preserve `Location` being Copy, but could blow up the memory utilization of compiler. 
+        };
         let loc = sp.get_lines();
         Location::new(
             sp.get_filename().to_string(),
@@ -23,6 +75,7 @@ impl<'tcx> GotocCtx<'tcx> {
             Some(loc.start_col),
             loc.end_line,
             Some(loc.end_col),
+            pragmas,
         )
     }
 
@@ -39,3 +92,18 @@ impl<'tcx> GotocCtx<'tcx> {
         self.codegen_span(&topmost)
     }
 }
+
+/// Extracts the single argument from the attribute provided as a string.
+/// For example, `disable_checks(foo)` return `Some("foo")`
+fn parse_word(attr: &Attribute) -> Option<String> {
+    // Vector of meta items , that contain the arguments given the attribute
+    let attr_args = attr.meta_item_list()?;
+    // Only extracts one string ident as a string
+    if attr_args.len() == 1 {
+        attr_args[0].ident().map(|ident| ident.to_string())
+    }
+    // Return none if there are no attributes or if there's too many attributes
+    else {
+        None
+    }
+}

kani-compiler/src/kani_middle/attributes.rs

@@ -74,6 +74,9 @@ enum KaniAttributeKind {
     /// We use this attribute to properly instantiate `kani::any_modifies` in
     /// cases when recursion is present given our contracts instrumentation.
     Recursion,
+    /// Used to mark functions where generating automatic pointer checks should be disabled. This is
+    /// used later to automatically attach pragma statements to locations.
+    DisableChecks,
 }
 
 impl KaniAttributeKind {
@@ -93,7 +96,8 @@ impl KaniAttributeKind {
             | KaniAttributeKind::CheckedWith
             | KaniAttributeKind::Modifies
             | KaniAttributeKind::InnerCheck
-            | KaniAttributeKind::IsContractGenerated => false,
+            | KaniAttributeKind::IsContractGenerated
+            | KaniAttributeKind::DisableChecks => false,
         }
     }
 
@@ -382,6 +386,10 @@ impl<'tcx> KaniAttributes<'tcx> {
                 KaniAttributeKind::InnerCheck => {
                     self.inner_check();
                 }
+                KaniAttributeKind::DisableChecks => {
+                    // Ignored here, because it should be an internal attribute. Actual validation
+                    // happens when pragmas are generated.
+                }
             }
         }
     }
@@ -490,6 +498,10 @@ impl<'tcx> KaniAttributes<'tcx> {
                 | KaniAttributeKind::InnerCheck
                 | KaniAttributeKind::ReplacedWith => {
                     self.tcx.dcx().span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref()));
+                },
+                KaniAttributeKind::DisableChecks => {
+                    // Internal attribute which shouldn't exist here.
+                    unreachable!()
                 }
             };
             harness