Changing how contracts communicate

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -19,9 +19,9 @@ use cbmc::irep::goto_binary_serde::write_goto_binary_file;
 use cbmc::RoundingMode;
 use cbmc::{InternedString, MachineModel};
 use kani_metadata::artifact::convert_type;
-use kani_metadata::CompilerArtifactStub;
 use kani_metadata::UnsupportedFeature;
 use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata};
+use kani_metadata::{AssignsContract, CompilerArtifactStub};
 use rustc_codegen_ssa::back::archive::{
  get_native_object_symbols, ArArchiveBuilder, ArchiveBuilder,
 };
@@ -62,18 +62,22 @@ use tracing::{debug, error, info};
 
 pub type UnsupportedConstructs = FxHashMap<InternedString, Vec<Location>>;
 
+pub type ContractInfoChannel = std::sync::mpsc::Sender<(DefPathHash, AssignsContract)>;
+
 #[derive(Clone)]
 pub struct GotocCodegenBackend {
  /// The query is shared with `KaniCompiler` and it is initialized as part of `rustc`
  /// initialization, which may happen after this object is created.
  /// Since we don't have any guarantees on when the compiler creates the Backend object, neither
  /// in which thread it will be used, we prefer to explicitly synchronize any query access.
  queries: Arc<Mutex<QueryDb>>,
+
+ contract_channel: ContractInfoChannel,
 }
 
 impl GotocCodegenBackend {
- pub fn new(queries: Arc<Mutex<QueryDb>>) -> Self {
- GotocCodegenBackend { queries }
+ pub fn new(queries: Arc<Mutex<QueryDb>>, contract_channel: ContractInfoChannel) -> Self {
+ GotocCodegenBackend { queries, contract_channel }
  }
 
  /// Generate code that is reachable from the given starting points.
@@ -84,7 +88,7 @@ impl GotocCodegenBackend {
  symtab_goto: &Path,
  machine_model: &MachineModel,
  check_contract: Option<DefId>,
- ) -> (GotocCtx<'tcx>, Vec<MonoItem<'tcx>>) {
+ ) -> (GotocCtx<'tcx>, Vec<MonoItem<'tcx>>, Option<AssignsContract>) {
  let items = with_timer(
  || collect_reachable_items(tcx, starting_items),
  "codegen reachability analysis",
@@ -182,11 +186,9 @@ impl GotocCodegenBackend {
  if let Some(restrictions) = vtable_restrictions {
  write_file(&symtab_goto, ArtifactType::VTableRestriction, &restrictions, pretty);
  }
-
- write_file(symtab_goto, ArtifactType::ContractMetadata, &contract_info, pretty);
  }
 
- (gcx, items)
+ (gcx, items, contract_info)
  }
 }
 
@@ -195,7 +197,7 @@ impl<'tcx> GotocCtx<'tcx> {
  &mut self,
  function_under_contract: DefId,
  items: &[MonoItem<'tcx>],
- ) -> (String, String) {
+ ) -> AssignsContract {
  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();
@@ -231,7 +233,7 @@ impl<'tcx> GotocCtx<'tcx> {
  tcx.item_name(recursion_wrapper_id),
  );
 
- (wrapper_name, full_name)
+ AssignsContract { recursion_tracker: full_name, contracted_function_name: wrapper_name }
  }
 }
 
@@ -299,14 +301,19 @@ impl CodegenBackend for GotocCodegenBackend {
  else {
  continue;
  };
- let (gcx, items) = self.codegen_items(
+ let (gcx, items, contract_info) = self.codegen_items(
  tcx,
  &[harness],
  model_path,
  &results.machine_model,
  contract_metadata,
  );
  results.extend(gcx, items, None);
+ if let Some(assigns_contract) = contract_info {
+ self.contract_channel
+ .send((tcx.def_path_hash(harness.def_id()), assigns_contract))
+ .unwrap();
+ }
  }
  }
  ReachabilityType::Tests => {
@@ -327,7 +334,7 @@ impl CodegenBackend for GotocCodegenBackend {
  // We will be able to remove this once we optimize all calls to CBMC utilities.
  // https://github.com/model-checking/kani/issues/1971
  let model_path = base_filename.with_extension(ArtifactType::SymTabGoto);
- let (gcx, items) = self.codegen_items(
+ let (gcx, items, contract_info) = self.codegen_items(
  tcx,
  &harnesses,
  &model_path,
@@ -336,6 +343,8 @@ impl CodegenBackend for GotocCodegenBackend {
  );
  results.extend(gcx, items, None);
 
+ assert!(contract_info.is_none());
+
  for (test_fn, test_desc) in harnesses.iter().zip(descriptions.iter()) {
  let instance = if let MonoItem::Fn(instance) = test_fn {
  instance
@@ -360,13 +369,14 @@ impl CodegenBackend for GotocCodegenBackend {
  || entry_fn == Some(def_id)
  });
  let model_path = base_filename.with_extension(ArtifactType::SymTabGoto);
- let (gcx, items) = self.codegen_items(
+ let (gcx, items, contract_info) = self.codegen_items(
  tcx,
  &local_reachable,
  &model_path,
  &results.machine_model,
  Default::default(),
  );
+ assert!(contract_info.is_none());
  results.extend(gcx, items, None);
  }
  }

kani-compiler/src/codegen_cprover_gotoc/mod.rs

@@ -6,6 +6,6 @@ mod context;
 mod overrides;
 mod utils;
 
-pub use compiler_interface::{GotocCodegenBackend, UnsupportedConstructs};
+pub use compiler_interface::{ContractInfoChannel, GotocCodegenBackend, UnsupportedConstructs};
 pub use context::GotocCtx;
 pub use context::VtableCtx;

kani-compiler/src/kani_compiler.rs

@@ -17,7 +17,7 @@
 
 use crate::args::{Arguments, ReachabilityType};
 #[cfg(feature = "cprover")]
-use crate::codegen_cprover_gotoc::GotocCodegenBackend;
+use crate::codegen_cprover_gotoc::{ContractInfoChannel, GotocCodegenBackend};
 use crate::kani_middle::attributes::is_proof_harness;
 use crate::kani_middle::check_crate_items;
 use crate::kani_middle::metadata::gen_proof_metadata;
@@ -26,7 +26,7 @@ use crate::kani_middle::stubbing::{self, harness_stub_map};
 use crate::kani_queries::QueryDb;
 use crate::session::init_session;
 use clap::Parser;
-use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata};
+use kani_metadata::{ArtifactType, AssignsContract, HarnessMetadata, KaniMetadata};
 use rustc_codegen_ssa::traits::CodegenBackend;
 use rustc_driver::{Callbacks, Compilation, RunCompiler};
 use rustc_hir::def_id::LOCAL_CRATE;
@@ -56,8 +56,11 @@ pub fn run(args: Vec<String>) -> ExitCode {
 
 /// Configure the cprover backend that generate goto-programs.
 #[cfg(feature = "cprover")]
-fn backend(queries: Arc<Mutex<QueryDb>>) -> Box<dyn CodegenBackend> {
- Box::new(GotocCodegenBackend::new(queries))
+fn backend(
+ queries: Arc<Mutex<QueryDb>>,
+ contract_channel: ContractInfoChannel,
+) -> Box<dyn CodegenBackend> {
+ Box::new(GotocCodegenBackend::new(queries, contract_channel))
 }
 
 /// Fallback backend. It will trigger an error if no backend has been enabled.
@@ -191,12 +194,20 @@ impl KaniCompiler {
  }
  CompilationStage::CodegenWithStubs { target_harnesses, all_harnesses, .. } => {
  assert!(!target_harnesses.is_empty(), "expected at least one target harness");
- let target_harness = &target_harnesses[0];
- let extra_arg =
-  stubbing::mk_rustc_arg(&all_harnesses[&target_harness].stub_map);
+ let target_harness_name = &target_harnesses[0];
+ let target_harness = &all_harnesses[target_harness_name];
+ let extra_arg = stubbing::mk_rustc_arg(&target_harness.stub_map);
  let mut args = orig_args.clone();
  args.push(extra_arg);
- self.run_compilation_session(&args)?;
+ let contract_spec = self.run_compilation_session(&args)?;
+ let CompilationStage::CodegenWithStubs { all_harnesses, .. } = &mut self.stage
+ else {
+ unreachable!()
+ };
+ for (target, spec) in contract_spec {
+ let target_harness = all_harnesses.get_mut(&target).unwrap();
+ target_harness.metadata.contract = spec.into();
+ }
  }
  CompilationStage::Done { metadata: Some((kani_metadata, crate_info)) } => {
  // Only store metadata for harnesses for now.
@@ -249,7 +260,7 @@ impl KaniCompiler {
  } else {
  CompilationStage::Done {
  metadata: Some((
- generate_metadata(&crate_info, all_harnesses),
+ generate_metadata(&crate_info, &all_harnesses),
  crate_info.clone(),
  )),
  }
@@ -262,12 +273,17 @@ impl KaniCompiler {
  }
 
  /// Run the Rust compiler with the given arguments and pass `&mut self` to handle callbacks.
- fn run_compilation_session(&mut self, args: &[String]) -> Result<(), ErrorGuaranteed> {
+ fn run_compilation_session(
+ &mut self,
+ args: &[String],
+ ) -> Result<Vec<(DefPathHash, AssignsContract)>, ErrorGuaranteed> {
  debug!(?args, "run_compilation_session");
  let queries = self.queries.clone();
  let mut compiler = RunCompiler::new(args, self);
- compiler.set_make_codegen_backend(Some(Box::new(move |_cfg| backend(queries))));
- compiler.run()
+ let (send, receive) = std::sync::mpsc::channel();
+ compiler.set_make_codegen_backend(Some(Box::new(move |_cfg| backend(queries, send))));
+ compiler.run();
+ Ok(receive.iter().collect())
  }
 
  /// Gather and process all harnesses from this crate that shall be compiled.
@@ -459,6 +475,7 @@ mod tests {
  original_end_line: 20,
  goto_file: None,
  attributes: HarnessAttributes::default(),
+ contract: Default::default(),
  }
  }
 

kani-compiler/src/kani_middle/metadata.rs

@@ -3,6 +3,7 @@
 //! This module handles Kani metadata generation. For example, generating HarnessMetadata for a
 //! given function.
 
+use std::default::Default;
 use std::path::Path;
 
 use crate::kani_middle::attributes::test_harness_name;
@@ -39,6 +40,7 @@ pub fn gen_proof_metadata(tcx: TyCtxt, def_id: DefId, base_name: &Path) -> Harne
  attributes,
  // TODO: This no longer needs to be an Option.
  goto_file: Some(model_file),
+ contract: Default::default(),
  }
 }
 
@@ -67,5 +69,6 @@ pub fn gen_test_metadata<'tcx>(
  attributes: HarnessAttributes::default(),
  // TODO: This no longer needs to be an Option.
  goto_file: Some(model_file),
+ contract: Default::default(),
  }
 }

kani-driver/src/call_goto_instrument.rs

@@ -12,7 +12,7 @@ use crate::metadata::collect_and_link_function_pointer_restrictions;
 use crate::project::Project;
 use crate::session::KaniSession;
 use crate::util::alter_extension;
-use kani_metadata::{ArtifactType, HarnessMetadata};
+use kani_metadata::{ArtifactType, AssignsContract, HarnessMetadata};
 
 impl KaniSession {
  /// Instrument and optimize a goto binary in-place.
@@ -22,7 +22,6 @@ impl KaniSession {
  output: &Path,
  project: &Project,
  harness: &HarnessMetadata,
- contract_info: Option<(String, String)>,
  ) -> Result<()> {
  // We actually start by calling goto-cc to start the specialization:
  self.specialize_to_proof_harness(input, output, &harness.mangled_name)?;
@@ -38,7 +37,7 @@ impl KaniSession {
  self.goto_sanity_check(output)?;
  }
 
- self.instrument_contracts(harness, output, contract_info)?;
+ self.instrument_contracts(harness, output)?;
 
  if self.args.checks.undefined_function_on() {
  self.add_library(output)?;
@@ -164,26 +163,22 @@ impl KaniSession {
  }
 
  /// Make CBMC enforce a function contract.
- pub fn instrument_contracts(
- &self,
- harness: &HarnessMetadata,
- file: &Path,
- check: Option<(String, String)>,
- ) -> Result<()> {
+ pub fn instrument_contracts(&self, harness: &HarnessMetadata, file: &Path) -> Result<()> {
+ let check = harness.contract.as_ref();
  if check.is_none() {
  return Ok(());
  }
 
  let mut args: Vec<std::ffi::OsString> =
  vec!["--dfcc".into(), (&harness.mangled_name).into()];
 
- if let Some((function, recursion_tracker)) = check {
- println!("enforcing function contract for {function} with tracker {recursion_tracker}");
+ if let Some(assigns) = check {
+ println!("enforcing function contract for {assigns:?}");
  args.extend([
  "--enforce-contract".into(),
- function.into(),
+ assigns.contracted_function_name.as_str().into(),
  "--nondet-static-exclude".into(),
- recursion_tracker.into(),
+ assigns.recursion_tracker.as_str().into(),
  ]);
  }
 

kani-driver/src/harness_runner.rs

@@ -57,18 +57,8 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> {
  let report_dir = self.project.outdir.join(format!("report-{harness_filename}"));
  let goto_file =
  self.project.get_harness_artifact(&harness, ArtifactType::Goto).unwrap();
- // TODO: Fix upstream.
- // This error is ignored for now, because it fails on cargo kani projects.
- // I suspect that the metadata file is just not being registered correctly.
- let contract_info = self.get_contract_info(harness).ok().flatten();
-
- self.sess.instrument_model(
- goto_file,
- goto_file,
- &self.project,
- &harness,
- contract_info,
- )?;
+
+ self.sess.instrument_model(goto_file, goto_file, &self.project, &harness)?;
 
  if self.sess.args.synthesize_loop_contracts {
  self.sess.synthesize_loop_contracts(goto_file, &goto_file, &harness)?;
@@ -83,18 +73,6 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> {
  Ok(results)
  }
 
- fn get_contract_info(&self, harness: &'pr HarnessMetadata) -> Result<Option<(String, String)>> {
- let contract_info_artifact = self
- .project
- .get_harness_artifact(&harness, ArtifactType::ContractMetadata)
- .ok_or_else(|| {
- anyhow!("no contract metadata file is present for harness {}", harness.pretty_name)
- })?;
-
- let reader = std::io::BufReader::new(std::fs::File::open(contract_info_artifact)?);
- Ok(serde_json::from_reader(reader)?)
- }
-
  /// Return an error if the user is trying to verify a harness with stubs without enabling the
  /// experimental feature.
  fn check_stubbing(&self, harnesses: &[&HarnessMetadata]) -> Result<()> {

kani-driver/src/metadata.rs

@@ -184,6 +184,7 @@ pub fn mock_proof_harness(
  original_end_line: 0,
  attributes: HarnessAttributes { unwind_value, proof: true, ..Default::default() },
  goto_file: model_file,
+ contract: Default::default(),
  }
 }
 

kani-driver/src/project.rs

@@ -130,12 +130,10 @@ impl Project {
 
  // All other harness artifacts that may have been generated as part of the build.
  artifacts.extend(
- [SymTab, TypeMap, VTableRestriction, PrettyNameMap, ContractMetadata]
- .iter()
- .filter_map(|typ| {
- let artifact = Artifact::try_from(&symtab_out, *typ).ok()?;
- Some(artifact)
- }),
+ [SymTab, TypeMap, VTableRestriction, PrettyNameMap].iter().filter_map(|typ| {
+ let artifact = Artifact::try_from(&symtab_out, *typ).ok()?;
+ Some(artifact)
+ }),
  );
  artifacts.push(symtab_out);
  artifacts.push(goto);
@@ -227,7 +225,7 @@ pub fn cargo_project(session: &KaniSession, keep_going: bool) -> Result<Project>
  .iter()
  .map(|artifact| convert_type(&artifact, Metadata, SymTabGoto))
  .collect::<Vec<_>>();
- artifacts.push(Artifact::try_new(goto.as_path(), ContractMetadata)?);
+
  session.link_goto_binary(&all_gotos, &goto)?;
  let goto_artifact = Artifact::try_new(&goto, Goto)?;