Skip to content

Commit

Permalink
Support for disabling automatically generated pointer checks to avoid…
Browse files Browse the repository at this point in the history 
… reinstrumentation (#3344)

Recently added memory initialization checks (see #3300 for an overview)
code suffers from re-instrumentation due to automatically added pointer
checks to the instrumentation code.

This PR adds an internal `kanitool::disable_checks` attribute to disable
automatically generated CBMC checks inside internal instrumentation.
This, in turn, relies on CBMC pragmas
(https://www.cprover.org/cprover-manual/properties/#usinggotoinstrument).

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
  • Loading branch information
@artemagvanian
artemagvanian authored Jul 19, 2024
1 parent ac823d3 commit 96d1147
Show file tree
Hide file tree
Showing 9 changed files with 204 additions and 23 deletions.
35 changes: 24 additions & 11 deletions cprover_bindings/src/goto_program/location.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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 },
Expand Down Expand Up @@ -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>,
Expand All @@ -117,6 +120,7 @@ impl Location {
start_col: start_col_into,
end_line: end_line_into,
end_col: end_col_into,
pragmas,
}
}

Expand All @@ -128,6 +132,7 @@ impl Location {
col: Option<T>,
comment: U,
property_name: U,
pragmas: &'static [&'static str],
) -> Location
where
T: TryInto<u64>,
Expand All @@ -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
Expand All @@ -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
Expand Down
46 changes: 37 additions & 9 deletions cprover_bindings/src/irep/to_irep.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)),
Expand All @@ -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![
Expand Down
68 changes: 68 additions & 0 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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(),
Expand All @@ -23,6 +75,7 @@ impl<'tcx> GotocCtx<'tcx> {
Some(loc.start_col),
loc.end_line,
Some(loc.end_col),
pragmas,
)
}

Expand All @@ -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
}
}
14 changes: 13 additions & 1 deletion kani-compiler/src/kani_middle/attributes.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -93,7 +96,8 @@ impl KaniAttributeKind {
| KaniAttributeKind::CheckedWith
| KaniAttributeKind::Modifies
| KaniAttributeKind::InnerCheck
| KaniAttributeKind::IsContractGenerated => false,
| KaniAttributeKind::IsContractGenerated
| KaniAttributeKind::DisableChecks => false,
}
}

Expand Down Expand Up @@ -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.
}
}
}
}
Expand Down Expand Up @@ -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
Expand Down
Loading

0 comments on commit 96d1147

Please sign in to comment.