Skip to content

Commit

Permalink
remove contracts count; reduce rfc detail
Browse files Browse the repository at this point in the history
  • Loading branch information
carolynzech committed Oct 2, 2024
1 parent 15dd78a commit 3f583d3
Show file tree
Hide file tree
Showing 10 changed files with 95 additions and 305 deletions.
34 changes: 21 additions & 13 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,16 +2,15 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT
use crate::codegen_cprover_gotoc::{GotocCtx, codegen::ty_stable::pointee_type_stable};
use crate::kani_middle::attributes::KaniAttributes;
use crate::kani_middle::find_closure_in_body;
use cbmc::goto_program::FunctionContract;
use cbmc::goto_program::{Expr, Lambda, Location, Type};
use kani_metadata::AssignsContract;
use rustc_hir::def_id::DefId as InternalDefId;
use rustc_smir::rustc_internal;
use stable_mir::CrateDef;
use stable_mir::mir::Local;
use stable_mir::mir::mono::{Instance, MonoItem};
use stable_mir::ty::{RigidTy, TyKind};
use stable_mir::mir::{Local, VarDebugInfoContents};
use stable_mir::ty::{FnDef, RigidTy, TyKind};

impl<'tcx> GotocCtx<'tcx> {
/// Given the `proof_for_contract` target `function_under_contract` and the reachable `items`,
Expand Down Expand Up @@ -88,24 +87,33 @@ impl<'tcx> GotocCtx<'tcx> {
recursion_tracker
}

fn find_closure(&mut self, inside: Instance, name: &str) -> Option<Instance> {
let body = self.transformer.body(self.tcx, inside);
find_closure_in_body(&body, name)
}

/// Find the modifies recursively since we may have a recursion wrapper.
/// I.e.: [recursion_wrapper ->]? check -> modifies.
fn find_modifies(&mut self, instance: Instance) -> Option<Instance> {
let contract_attrs =
KaniAttributes::for_instance(self.tcx, instance).contract_attributes()?;
let mut find_closure = |inside: Instance, name: &str| {
let body = self.transformer.body(self.tcx, inside);
body.var_debug_info.iter().find_map(|var_info| {
if var_info.name.as_str() == name {
let ty = match &var_info.value {
VarDebugInfoContents::Place(place) => place.ty(body.locals()).unwrap(),
VarDebugInfoContents::Const(const_op) => const_op.ty(),
};
if let TyKind::RigidTy(RigidTy::Closure(def, args)) = ty.kind() {
return Some(Instance::resolve(FnDef(def.def_id()), &args).unwrap());
}
}
None
})
};
let check_instance = if contract_attrs.has_recursion {
let recursion_check =
self.find_closure(instance, contract_attrs.recursion_check.as_str())?;
self.find_closure(recursion_check, contract_attrs.checked_with.as_str())?
let recursion_check = find_closure(instance, contract_attrs.recursion_check.as_str())?;
find_closure(recursion_check, contract_attrs.checked_with.as_str())?
} else {
self.find_closure(instance, contract_attrs.checked_with.as_str())?
find_closure(instance, contract_attrs.checked_with.as_str())?
};
self.find_closure(check_instance, contract_attrs.modifies_wrapper.as_str())
find_closure(check_instance, contract_attrs.modifies_wrapper.as_str())
}

/// Convert the Kani level contract into a CBMC level contract by creating a
Expand Down
99 changes: 29 additions & 70 deletions kani-compiler/src/kani_middle/metadata.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,18 +6,13 @@
use std::collections::HashMap;
use std::path::Path;

use crate::kani_middle::attributes::test_harness_name;
use crate::kani_middle::attributes::{
ContractAttributes, KaniAttributes, matches_diagnostic as matches_function,
};
use crate::kani_middle::{InternalDefId, SourceLocation, find_closure_in_body};
use crate::kani_middle::attributes::{KaniAttributes, test_harness_name};
use crate::kani_middle::{InternalDefId, SourceLocation};
use kani_metadata::ContractedFunction;
use kani_metadata::{ArtifactType, HarnessAttributes, HarnessKind, HarnessMetadata};
use rustc_middle::ty::TyCtxt;
use rustc_smir::rustc_internal;
use stable_mir::mir::mono::Instance;
use stable_mir::mir::{Body, TerminatorKind};
use stable_mir::ty::{RigidTy, TyKind};
use stable_mir::{CrateDef, CrateItems};

/// Create the harness metadata for a proof harness for a given function.
Expand Down Expand Up @@ -47,81 +42,45 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) ->
}
}

/// Map each function under contract to its contract harnesses
fn fns_to_contract_harnesses(tcx: TyCtxt) -> HashMap<InternalDefId, Vec<String>> {
/// Collects contract and contract harness metadata.
///
/// For each function with contracts (or that is a target of a contract harness),
/// construct a ContractedFunction object for it.
pub fn gen_contracts_metadata(tcx: TyCtxt) -> Vec<ContractedFunction> {
// We work with stable_mir::CrateItem instead of stable_mir::Instance to include generic items
let crate_items: CrateItems = stable_mir::all_local_items();

let mut fns_to_harnesses: HashMap<InternalDefId, Vec<String>> = HashMap::new();
let mut fn_to_data: HashMap<InternalDefId, ContractedFunction> = HashMap::new();

for item in crate_items {
let def_id = rustc_internal::internal(tcx, item.def_id());
let fn_name = tcx.def_path_str(def_id);
let attributes = KaniAttributes::for_item(tcx, def_id);
let internal_def_id = rustc_internal::internal(tcx, item.def_id());

let function = item.name();
let file = SourceLocation::new(item.span()).filename;
let attributes = KaniAttributes::for_def_id(tcx, item.def_id());

if attributes.has_contract() {
fns_to_harnesses.insert(def_id, vec![]);
} else if let Some((_, target_def_id, _)) = attributes.interpret_for_contract_attribute() {
if let Some(harnesses) = fns_to_harnesses.get_mut(&target_def_id) {
harnesses.push(fn_name);
fn_to_data.insert(internal_def_id, ContractedFunction {
function,
file,
harnesses: vec![],
});
} else if let Some((target_name, target_def_id, _)) =
attributes.interpret_for_contract_attribute()
{
if let Some(cf) = fn_to_data.get_mut(&target_def_id) {
cf.harnesses.push(function);
} else {
fns_to_harnesses.insert(target_def_id, vec![fn_name]);
fn_to_data.insert(target_def_id, ContractedFunction {
function: target_name.to_string(),
file,
harnesses: vec![function],
});
}
}
}

fns_to_harnesses
}

/// Count the number of contracts in `check_body`, where `check_body` is the body of the
/// kanitool::checked_with closure (c.f. kani_macros::sysroot::contracts).
/// In this closure, preconditions are denoted by kani::assume() calls and postconditions by kani::assert() calls.
/// The number of contracts is the number of times these functions are called inside the closure
fn count_contracts(tcx: TyCtxt, check_body: &Body) -> usize {
let mut count = 0;

for bb in &check_body.blocks {
if let TerminatorKind::Call { ref func, .. } = bb.terminator.kind {
let fn_ty = func.ty(check_body.locals()).unwrap();
if let TyKind::RigidTy(RigidTy::FnDef(fn_def, args)) = fn_ty.kind() {
if let Ok(instance) = Instance::resolve(fn_def, &args) {
// For each precondition or postcondition, increment the count
if matches_function(tcx, instance.def, "KaniAssume")
|| matches_function(tcx, instance.def, "KaniAssert")
{
count += 1;
}
}
}
}
}
count
}

/// Collects contract and contract harness metadata.
///
/// For each function with contracts (or that is a target of a contract harness),
/// construct a ContractedFunction object for it.
pub fn gen_contracts_metadata(tcx: TyCtxt) -> Vec<ContractedFunction> {
let mut contracted_fns = vec![];
for (fn_def_id, harnesses) in fns_to_contract_harnesses(tcx) {
let attrs: ContractAttributes =
KaniAttributes::for_item(tcx, fn_def_id).contract_attributes().unwrap();
let body: Body = rustc_internal::stable(tcx.optimized_mir(fn_def_id));
let check_body: Body =
find_closure_in_body(&body, attrs.checked_with.as_str()).unwrap().body().unwrap();

let total_contracts = count_contracts(tcx, &check_body);

contracted_fns.push(ContractedFunction {
function: tcx.def_path_str(fn_def_id),
file: SourceLocation::new(rustc_internal::stable(tcx.def_span(fn_def_id))).filename,
harnesses,
total_contracts,
});
}

contracted_fns
fn_to_data.into_values().collect()
}

/// Create the harness metadata for a test description.
Expand Down
19 changes: 1 addition & 18 deletions kani-compiler/src/kani_middle/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,7 @@ use rustc_span::source_map::respan;
use rustc_target::abi::call::FnAbi;
use rustc_target::abi::{HasDataLayout, TargetDataLayout};
use stable_mir::CrateDef;
use stable_mir::mir::mono::{Instance, MonoItem};
use stable_mir::mir::{Body, VarDebugInfoContents};
use stable_mir::mir::mono::MonoItem;
use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, Ty, TyKind};
use stable_mir::visitor::{Visitable, Visitor as TyVisitor};
use std::ops::ControlFlow;
Expand Down Expand Up @@ -239,19 +238,3 @@ pub fn stable_fn_def(tcx: TyCtxt, def_id: InternalDefId) -> Option<FnDef> {
None
}
}

/// Find the user-declared closure by the name `name` in `body`.
pub fn find_closure_in_body(body: &Body, name: &str) -> Option<Instance> {
body.var_debug_info.iter().find_map(|var_info| {
if var_info.name.as_str() == name {
let ty = match &var_info.value {
VarDebugInfoContents::Place(place) => place.ty(body.locals()).unwrap(),
VarDebugInfoContents::Const(const_op) => const_op.ty(),
};
if let TyKind::RigidTy(RigidTy::Closure(def, args)) = ty.kind() {
return Some(Instance::resolve(FnDef(def.def_id()), &args).unwrap());
}
}
None
})
}
12 changes: 5 additions & 7 deletions kani-driver/src/list/collect_metadata.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,15 +16,18 @@ use crate::{
use anyhow::Result;
use kani_metadata::{ContractedFunction, HarnessKind, KaniMetadata};

/// Process the KaniMetadata output from kani-compiler and output the list subcommand results
fn process_metadata(metadata: Vec<KaniMetadata>, format: Format) -> Result<()> {
// Map each file to a vector of its harnesses
// We use ordered maps and sets so that the output is in lexographic order (and consistent across invocations).

// Map each file to a vector of its harnesses.
let mut standard_harnesses: BTreeMap<String, BTreeSet<String>> = BTreeMap::new();
let mut contract_harnesses: BTreeMap<String, BTreeSet<String>> = BTreeMap::new();

let mut contracted_functions: BTreeSet<ContractedFunction> = BTreeSet::new();

let mut total_standard_harnesses = 0;
let mut total_contract_harnesses = 0;
let mut total_contracts = 0;

for kani_meta in metadata {
for harness_meta in kani_meta.proof_harnesses {
Expand Down Expand Up @@ -57,18 +60,13 @@ fn process_metadata(metadata: Vec<KaniMetadata>, format: Format) -> Result<()> {
}
}

for cf in &kani_meta.contracted_functions {
total_contracts += cf.total_contracts;
}

contracted_functions.extend(kani_meta.contracted_functions.into_iter());
}

let totals = Totals {
standard_harnesses: total_standard_harnesses,
contract_harnesses: total_contract_harnesses,
contracted_functions: contracted_functions.len(),
contracts: total_contracts,
};

match format {
Expand Down
1 change: 0 additions & 1 deletion kani-driver/src/list/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,5 +9,4 @@ struct Totals {
standard_harnesses: usize,
contract_harnesses: usize,
contracted_functions: usize,
contracts: usize,
}
37 changes: 11 additions & 26 deletions kani-driver/src/list/output.rs
Original file line number Diff line number Diff line change
Expand Up @@ -27,83 +27,70 @@ fn construct_contracts_table(
) -> Vec<String> {
const NO_HARNESSES_MSG: &str = "NONE";

// Since the harnesses will be separated by newlines, the harness length is equal to the length of the longest harness
fn harnesses_len(harnesses: &[String]) -> usize {
// Since the harnesses will be separated by newlines, the column length is equal to the length of the longest harness
fn column_len(harnesses: &[String]) -> usize {
harnesses.iter().map(|s| s.len()).max().unwrap_or(NO_HARNESSES_MSG.len())
}

// Contracts table headers
const FUNCTION_HEADER: &str = "Function";
const CONTRACTS_COUNT_HEADER: &str = "# of Contracts";
const CONTRACT_HARNESSES_HEADER: &str = "Contract Harnesses (#[kani::proof_for_contract])";

// Contracts table totals row
const TOTALS_HEADER: &str = "Total";
let functions_total = totals.contracted_functions.to_string();
let contracts_total = totals.contracts.to_string();
let harnesses_total = totals.contract_harnesses.to_string();

let mut table_rows: Vec<String> = vec![];
let mut max_function_fmt_width = max(FUNCTION_HEADER.len(), functions_total.len());
let mut max_contracts_count_fmt_width =
max(CONTRACTS_COUNT_HEADER.len(), contracts_total.len());
let mut max_contract_harnesses_fmt_width =
max(CONTRACT_HARNESSES_HEADER.len(), harnesses_total.len());

let mut data_rows: Vec<(String, String, Vec<String>)> = vec![];
let mut data_rows: Vec<(String, Vec<String>)> = vec![];

for cf in contracted_functions {
max_function_fmt_width = max(max_function_fmt_width, cf.function.len());
max_contracts_count_fmt_width = max(max_contracts_count_fmt_width, cf.total_contracts);
max_contract_harnesses_fmt_width =
max(max_contract_harnesses_fmt_width, harnesses_len(&cf.harnesses));
max(max_contract_harnesses_fmt_width, column_len(&cf.harnesses));

data_rows.push((cf.function, cf.total_contracts.to_string(), cf.harnesses));
data_rows.push((cf.function, cf.harnesses));
}

let function_sep = "-".repeat(max_function_fmt_width);
let contracts_count_sep = "-".repeat(max_contracts_count_fmt_width);
let contract_harnesses_sep = "-".repeat(max_contract_harnesses_fmt_width);
let totals_sep = "-".repeat(TOTALS_HEADER.len());

let sep_row = format!(
"| {totals_sep} | {function_sep} | {contracts_count_sep} | {contract_harnesses_sep} |"
);
let sep_row = format!("| {totals_sep} | {function_sep} | {contract_harnesses_sep} |");
table_rows.push(sep_row.clone());

let function_space = " ".repeat(max_function_fmt_width - FUNCTION_HEADER.len());
let contracts_count_space =
" ".repeat(max_contracts_count_fmt_width - CONTRACTS_COUNT_HEADER.len());
let contract_harnesses_space =
" ".repeat(max_contract_harnesses_fmt_width - CONTRACT_HARNESSES_HEADER.len());
let totals_space = " ".repeat(TOTALS_HEADER.len());

let header_row = format!(
"| {totals_space} | {FUNCTION_HEADER}{function_space} | {CONTRACTS_COUNT_HEADER}{contracts_count_space} | {CONTRACT_HARNESSES_HEADER}{contract_harnesses_space} |"
"| {totals_space} | {FUNCTION_HEADER}{function_space} | {CONTRACT_HARNESSES_HEADER}{contract_harnesses_space} |"
);
table_rows.push(header_row);
table_rows.push(sep_row.clone());

for (function, total_contracts, harnesses) in data_rows {
for (function, harnesses) in data_rows {
let function_space = " ".repeat(max_function_fmt_width - function.len());
let contracts_count_space =
" ".repeat(max_contracts_count_fmt_width - total_contracts.len());
let first_harness = harnesses.first().map_or(NO_HARNESSES_MSG, |v| v);
let contract_harnesses_space =
" ".repeat(max_contract_harnesses_fmt_width - first_harness.len());

let first_row = format!(
"| {totals_space} | {function}{function_space} | {total_contracts}{contracts_count_space} | {first_harness}{contract_harnesses_space} |"
"| {totals_space} | {function}{function_space} | {first_harness}{contract_harnesses_space} |"
);
table_rows.push(first_row);

for subsequent_harness in harnesses.iter().skip(1) {
let function_space = " ".repeat(max_function_fmt_width);
let contracts_count_space = " ".repeat(max_contracts_count_fmt_width);
let contract_harnesses_space =
" ".repeat(max_contract_harnesses_fmt_width - subsequent_harness.len());
let row = format!(
"| {totals_space} | {function_space} | {contracts_count_space} | {subsequent_harness}{contract_harnesses_space} |"
"| {totals_space} | {function_space} | {subsequent_harness}{contract_harnesses_space} |"
);
table_rows.push(row);
}
Expand All @@ -112,12 +99,11 @@ fn construct_contracts_table(
}

let total_function_space = " ".repeat(max_function_fmt_width - functions_total.len());
let total_contracts_space = " ".repeat(max_contracts_count_fmt_width - contracts_total.len());
let total_harnesses_space =
" ".repeat(max_contract_harnesses_fmt_width - harnesses_total.len());

let totals_row = format!(
"| {TOTALS_HEADER} | {functions_total}{total_function_space} | {contracts_total}{total_contracts_space} | {harnesses_total}{total_harnesses_space} |"
"| {TOTALS_HEADER} | {functions_total}{total_function_space} | {harnesses_total}{total_harnesses_space} |"
);

table_rows.push(totals_row);
Expand Down Expand Up @@ -185,7 +171,6 @@ pub fn json(
"standard-harnesses": totals.standard_harnesses,
"contract-harnesses": totals.contract_harnesses,
"functions-under-contract": totals.contracted_functions,
"contracts": totals.contracts,
}
});

Expand Down
2 changes: 0 additions & 2 deletions kani_metadata/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -41,8 +41,6 @@ pub struct ContractedFunction {
pub function: String,
/// The (currently full-) path to the file this function was declared within.
pub file: String,
/// The number of contracts applied to this function
pub total_contracts: usize,
/// The pretty names of the proof harnesses (`#[kani::proof_for_contract]`) for this function
pub harnesses: Vec<String>,
}
Expand Down
Loading

0 comments on commit 3f583d3

Please sign in to comment.