Skip to content

Commit

Permalink
Fix static exclude for recursion tracker
Browse files Browse the repository at this point in the history
  • Loading branch information
@JustusAdam
JustusAdam committed Nov 22, 2023
1 parent 64f7e5f commit 0c3cea7
Show file tree
Hide file tree
Showing 4 changed files with 59 additions and 76 deletions.
81 changes: 52 additions & 29 deletions kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,7 @@ use tempfile::Builder as TempFileBuilder;
use tracing::{debug, error, info};

pub type UnsupportedConstructs = FxHashMap<InternedString, Vec<Location>>;

#[derive(Clone)]
pub struct GotocCodegenBackend {
/// The query is shared with `KaniCompiler` and it is initialized as part of `rustc`
Expand Down Expand Up @@ -146,33 +147,7 @@ impl GotocCodegenBackend {
}
}

check_contract.map(|check_contract_def| {
let check_contract_attrs = KaniAttributes::for_item(tcx, check_contract_def);
let wrapper_def = check_contract_attrs.inner_check().unwrap().unwrap();

let mut instances_of_check = items.iter().copied().filter_map(|i| match i {
MonoItem::Fn(instance @ Instance { def: InstanceDef::Item(did), .. }) => {
(wrapper_def == did).then_some(instance)
}
_ => None,
});
let instance_of_check = instances_of_check.next().unwrap();
assert!(instances_of_check.next().is_none());
let attrs = KaniAttributes::for_item(tcx, instance_of_check.def_id());
let assigns_contract = attrs.modifies_contract().unwrap_or_else(|| {
debug!(?instance_of_check, "had no assigns contract specified");
vec![]
});
gcx.attach_contract(instance_of_check, assigns_contract);

let tracker_def = check_contract_attrs.recursion_tracker().unwrap().unwrap();

let span = tcx.def_span(tracker_def);
let location = SourceLocation::new(tcx, &span);
let full_name = format!("{}:{}", location.filename, tcx.item_name(tracker_def));

(tcx.symbol_name(instance_of_check).to_string(), full_name)
})
check_contract.map(|check_id| gcx.handle_check_contract(check_id, &items))
},
"codegen",
);
Expand Down Expand Up @@ -215,6 +190,51 @@ impl GotocCodegenBackend {
}
}

impl<'tcx> GotocCtx<'tcx> {
fn handle_check_contract(
&mut self,
function_under_contract: DefId,
items: &[MonoItem<'tcx>],
) -> (String, String) {
let tcx = self.tcx;
let function_under_contract_attrs = KaniAttributes::for_item(tcx, function_under_contract);
let wrapped_fn = function_under_contract_attrs.inner_check().unwrap().unwrap();

let mut instance_under_contract = items.iter().copied().filter_map(|i| match i {
MonoItem::Fn(instance @ Instance { def: InstanceDef::Item(did), .. }) => {
(wrapped_fn == did).then_some(instance)
}
_ => None,
});
let instance_of_check = instance_under_contract.next().unwrap();
assert!(
instance_under_contract.next().is_none(),
"Only one instance of a checked function may be in scope"
);
let attrs_of_wrapped_fn = KaniAttributes::for_item(tcx, wrapped_fn);
let assigns_contract = attrs_of_wrapped_fn.modifies_contract().unwrap_or_else(|| {
debug!(?instance_of_check, "had no assigns contract specified");
vec![]
});
self.attach_contract(instance_of_check, assigns_contract);

let wrapper_name = tcx.symbol_name(instance_of_check).to_string();

let recursion_wrapper_id =
function_under_contract_attrs.checked_with_id().unwrap().unwrap();
let span_of_recursion_wrapper = tcx.def_span(recursion_wrapper_id);
let location_of_recursion_wrapper = SourceLocation::new(tcx, &span_of_recursion_wrapper);

let full_name = format!(
"{}:{}::REENTRY",
location_of_recursion_wrapper.filename,
tcx.item_name(recursion_wrapper_id),
);

(wrapper_name, full_name)
}
}

fn contract_metadata_for_harness(
tcx: TyCtxt,
def_id: DefId,
Expand Down Expand Up @@ -317,8 +337,11 @@ impl CodegenBackend for GotocCodegenBackend {
results.extend(gcx, items, None);

for (test_fn, test_desc) in harnesses.iter().zip(descriptions.iter()) {
let instance =
if let MonoItem::Fn(instance) = test_fn { instance } else { continue };
let instance = if let MonoItem::Fn(instance) = test_fn {
instance
} else {
continue;
};
let metadata = gen_test_metadata(tcx, *test_desc, *instance, &base_filename);
let test_model_path = &metadata.goto_file.as_ref().unwrap();
std::fs::copy(&model_path, test_model_path).expect(&format!(
Expand Down
36 changes: 2 additions & 34 deletions kani-compiler/src/kani_middle/attributes.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,6 @@ enum KaniAttributeKind {
IsContractGenerated,
Modifies,
InnerCheck,
RecursionTracker,
}

impl KaniAttributeKind {
Expand All @@ -78,7 +77,6 @@ impl KaniAttributeKind {
| KaniAttributeKind::ReplacedWith
| KaniAttributeKind::CheckedWith
| KaniAttributeKind::Modifies
| KaniAttributeKind::RecursionTracker
| KaniAttributeKind::InnerCheck
| KaniAttributeKind::IsContractGenerated => false,
}
Expand Down Expand Up @@ -225,34 +223,8 @@ impl<'tcx> KaniAttributes<'tcx> {
}

/// Retrieves the global, static recursion tracker variable.
pub fn recursion_tracker(&self) -> Option<Result<DefId, ErrorGuaranteed>> {
self.expect_maybe_one(KaniAttributeKind::RecursionTracker).map(|target| {
let name = expect_key_string_value(self.tcx.sess, target)?;
let all_items = self.tcx.hir_crate_items(());
let hir_map = self.tcx.hir();

// I don't like the way this is currently implemented. I search
// through all items defined in the crate for one with the correct
// name. That works but this should do something better like
// `eval_sibling_attribute`, which is less likely to have any
// conflicts or alternatively use resolution for a path.
//
// The efficient thing to do is figure out where (relative to the
// annotated item) rustc actually stores the tracker (which `mod`)
// and the retrieve it (like `eval_sibling_attribute` does).

let owner = all_items
.items()
.find(|it| hir_map.opt_name(it.hir_id()) == Some(name))
.ok_or_else(|| {
self.tcx.sess.span_err(
self.tcx.def_span(self.item),
format!("Could not find recursion tracker '{name}' in crate"),
)
})?;

Ok(owner.owner_id.def_id.to_def_id())
})
pub fn checked_with_id(&self) -> Option<Result<DefId, ErrorGuaranteed>> {
self.eval_sibling_attribute(KaniAttributeKind::CheckedWith)
}

fn eval_sibling_attribute(
Expand Down Expand Up @@ -373,9 +345,6 @@ impl<'tcx> KaniAttributes<'tcx> {
KaniAttributeKind::InnerCheck => {
self.inner_check();
}
KaniAttributeKind::RecursionTracker => {
self.recursion_tracker();
}
}
}
}
Expand Down Expand Up @@ -479,7 +448,6 @@ impl<'tcx> KaniAttributes<'tcx> {
| KaniAttributeKind::IsContractGenerated
| KaniAttributeKind::Modifies
| KaniAttributeKind::InnerCheck
| KaniAttributeKind::RecursionTracker
| KaniAttributeKind::ReplacedWith => {
self.tcx.sess.span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref()));
}
Expand Down
2 changes: 1 addition & 1 deletion kani-driver/src/call_goto_instrument.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -178,7 +178,7 @@ impl KaniSession {
vec!["--dfcc".into(), (&harness.mangled_name).into()];

if let Some((function, recursion_tracker)) = check {
println!("enforcing function contract for {function}");
println!("enforcing function contract for {function} with tracker {recursion_tracker}");
args.extend([
"--enforce-contract".into(),
function.into(),
Expand Down
16 changes: 4 additions & 12 deletions library/kani_macros/src/sysroot/contracts.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1003,11 +1003,6 @@ fn requires_ensures_main(
"recursion_wrapper",
item_hash,
);
let recursion_tracker_name = identifier_for_generated_function(
&original_function_name,
"recursion_tracker",
item_hash,
);

// Constructing string literals explicitly here, because `stringify!`
// doesn't work. Let's say we have an identifier `check_fn` and we were
Expand All @@ -1021,8 +1016,6 @@ fn requires_ensures_main(
syn::LitStr::new(&handler.make_wrapper_name().to_string(), Span::call_site());
let recursion_wrapper_name_str =
syn::LitStr::new(&recursion_wrapper_name.to_string(), Span::call_site());
let recursion_tracker_name_str =
syn::LitStr::new(&recursion_tracker_name.to_string(), Span::call_site());

// The order of `attrs` and `kanitool::{checked_with,
// is_contract_generated}` is important here, because macros are
Expand All @@ -1039,7 +1032,6 @@ fn requires_ensures_main(
#[kanitool::checked_with = #recursion_wrapper_name_str]
#[kanitool::replaced_with = #replace_fn_name_str]
#[kanitool::inner_check = #wrapper_fn_name_str]
#[kanitool::recursion_tracker = #recursion_tracker_name_str]
#vis #sig {
#block
}
Expand All @@ -1061,13 +1053,13 @@ fn requires_ensures_main(
#[allow(dead_code, unused_variables)]
#[kanitool::is_contract_generated(recursion_wrapper)]
#wrapper_sig {
static mut #recursion_tracker_name: bool = false;
if unsafe { #recursion_tracker_name } {
static mut REENTRY: bool = false;
if unsafe { REENTRY } {
#call_replace(#(#args),*)
} else {
unsafe { #recursion_tracker_name = true };
unsafe { REENTRY = true };
let result = #call_check(#(#also_args),*);
unsafe { #recursion_tracker_name = false };
unsafe { REENTRY = false };
result
}
}
Expand Down

0 comments on commit 0c3cea7

Please sign in to comment.