Refactor the loop contracts with closures

cprover_bindings/src/irep/to_irep.rs

@@ -520,7 +520,10 @@ impl ToIrep for StmtBody {
  let stmt_goto = code_irep(IrepId::Goto, vec![])
  .with_named_sub(IrepId::Destination, Irep::just_string_id(dest.to_string()));
  if let Some(inv) = loop_invariants {
- stmt_goto.with_named_sub(IrepId::CSpecLoopInvariant, inv.to_irep(mm))
+ stmt_goto.with_named_sub(
+ IrepId::CSpecLoopInvariant,
+ inv.clone().and(Expr::bool_true()).to_irep(mm),
+ )
  } else {
  stmt_goto
  }

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

@@ -20,55 +20,25 @@ impl<'tcx> GotocCtx<'tcx> {
  pub fn codegen_block(&mut self, bb: BasicBlockIdx, bbd: &BasicBlock) {
  debug!(?bb, "codegen_block");
  let label = bb_label(bb);
-
- // record the seen bbidx if loop contracts enabled
- if self.loop_contracts_ctx.loop_contracts_enabled() {
- self.loop_contracts_ctx.add_new_seen_bbidx(bb);
- }
-
  // the first statement should be labelled. if there is no statements, then the
  // terminator should be labelled.
  match bbd.statements.len() {
  0 => {
  let term = &bbd.terminator;
- let tcode = if self.loop_contracts_ctx.loop_contracts_enabled() {
- let codegen_result = self.codegen_terminator(term);
- self.loop_contracts_ctx.push_onto_block(codegen_result)
- } else {
- self.codegen_terminator(term)
- };
-
+ let tcode = self.codegen_terminator(term);
  self.current_fn_mut().push_onto_block(tcode.with_label(label));
  }
  _ => {
  let stmt = &bbd.statements[0];
- let scode = if self.loop_contracts_ctx.loop_contracts_enabled() {
- let codegen_result = self.codegen_statement(stmt);
- self.loop_contracts_ctx.push_onto_block(codegen_result)
- } else {
- self.codegen_statement(stmt)
- };
-
+ let scode = self.codegen_statement(stmt);
  self.current_fn_mut().push_onto_block(scode.with_label(label));
 
  for s in &bbd.statements[1..] {
- let stmt = if self.loop_contracts_ctx.loop_contracts_enabled() {
- let codegen_result = self.codegen_statement(s);
- self.loop_contracts_ctx.push_onto_block(codegen_result)
- } else {
- self.codegen_statement(s)
- };
+ let stmt = self.codegen_statement(s);
  self.current_fn_mut().push_onto_block(stmt);
  }
  let term = &bbd.terminator;
-
- let tcode = if self.loop_contracts_ctx.loop_contracts_enabled() {
- let codegen_result = self.codegen_terminator(term);
- self.loop_contracts_ctx.push_onto_block(codegen_result)
- } else {
- self.codegen_terminator(term)
- };
-
+ let tcode = self.codegen_terminator(term);
  self.current_fn_mut().push_onto_block(tcode);
  }
  }

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

@@ -56,9 +56,6 @@ impl<'tcx> GotocCtx<'tcx> {
  let old_sym = self.symbol_table.lookup(&name).unwrap();
 
  let _trace_span = debug_span!("CodegenFunction", name = instance.name()).entered();
- if self.loop_contracts_ctx.loop_contracts_enabled() {
- self.loop_contracts_ctx.enter_new_function();
- }
  if old_sym.is_function_definition() {
  debug!("Double codegen of {:?}", old_sym);
  } else {

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

@@ -192,21 +192,12 @@ impl<'tcx> GotocCtx<'tcx> {
  ///
  /// See also [`GotocCtx::codegen_statement`] for ordinary [Statement]s.
  pub fn codegen_terminator(&mut self, term: &Terminator) -> Stmt {
- let loc: Location = self.codegen_span_stable(term.span);
+ let loc = self.codegen_span_stable(term.span);
  let _trace_span = debug_span!("CodegenTerminator", statement = ?term.kind).entered();
  debug!("handling terminator {:?}", term);
  //TODO: Instead of doing location::none(), and updating, just putit in when we make the stmt.
  match &term.kind {
- TerminatorKind::Goto { target } => {
- if self.loop_contracts_ctx.loop_contracts_enabled()
- && self.loop_contracts_ctx.is_loop_latch(target)
- {
- Stmt::goto(bb_label(*target), loc)
- .with_loop_contracts(self.loop_contracts_ctx.extract_block(loc))
- } else {
- Stmt::goto(bb_label(*target), loc)
- }
- }
+ TerminatorKind::Goto { target } => Stmt::goto(bb_label(*target), loc),
  TerminatorKind::SwitchInt { discr, targets } => {
  self.codegen_switch_int(discr, targets, loc)
  }

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -15,7 +15,6 @@
 //! Any MIR specific functionality (e.g. codegen etc) should live in specialized files that use
 //! this structure as input.
 use super::current_fn::CurrentFnCtx;
-use super::loop_contracts_ctx::LoopContractsCtx;
 use super::vtable_ctx::VtableCtx;
 use crate::codegen_cprover_gotoc::overrides::{fn_hooks, GotocHooks};
 use crate::codegen_cprover_gotoc::utils::full_crate_name;
@@ -75,8 +74,6 @@ pub struct GotocCtx<'tcx> {
  pub concurrent_constructs: UnsupportedConstructs,
  /// The body transformation agent.
  pub transformer: BodyTransformation,
- /// The context for loop contracts code generation.
- pub loop_contracts_ctx: LoopContractsCtx,
 }
 
 /// Constructor
@@ -90,8 +87,6 @@ impl<'tcx> GotocCtx<'tcx> {
  let fhks = fn_hooks();
  let symbol_table = SymbolTable::new(machine_model.clone());
  let emit_vtable_restrictions = queries.args().emit_vtable_restrictions;
- let loop_contracts_enabled =
- queries.args().unstable_features.contains(&"loop-contracts".to_string());
  GotocCtx {
  tcx,
  queries,
@@ -108,7 +103,6 @@ impl<'tcx> GotocCtx<'tcx> {
  unsupported_constructs: FxHashMap::default(),
  concurrent_constructs: FxHashMap::default(),
  transformer,
- loop_contracts_ctx: LoopContractsCtx::new(loop_contracts_enabled),
  }
  }
 }

kani-compiler/src/codegen_cprover_gotoc/context/mod.rs

@@ -8,7 +8,6 @@
 
 mod current_fn;
 mod goto_ctx;
-mod loop_contracts_ctx;
 mod vtable_ctx;
 
 pub use goto_ctx::GotocCtx;

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -8,7 +8,7 @@
 //! It would be too nasty if we spread around these sort of undocumented hooks in place, so
 //! this module addresses this issue.
 
-use super::loop_contracts_hooks::{LoopInvariantBegin, LoopInvariantEnd};
+use super::loop_contracts_hooks::LoopInvariantRegister;
 use crate::codegen_cprover_gotoc::codegen::{bb_label, PropertyClass};
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::kani_middle::attributes::matches_diagnostic as matches_function;
@@ -556,8 +556,7 @@ pub fn fn_hooks() -> GotocHooks {
  Rc::new(MemCmp),
  Rc::new(UntrackedDeref),
  Rc::new(InitContracts),
- Rc::new(LoopInvariantBegin),
- Rc::new(LoopInvariantEnd),
+ Rc::new(LoopInvariantRegister),
  ],
  }
 }

kani-compiler/src/codegen_cprover_gotoc/overrides/loop_contracts_hooks.rs

@@ -4,61 +4,34 @@
 use super::hooks::GotocHook;
 use crate::codegen_cprover_gotoc::codegen::bb_label;
 use crate::codegen_cprover_gotoc::GotocCtx;
-use crate::kani_middle::attributes::matches_diagnostic as matches_function;
-use cbmc::goto_program::{Expr, Stmt};
+use crate::kani_middle::attributes::KaniAttributes;
+use cbmc::goto_program::{CIntType, Expr, Stmt, Type};
 use rustc_middle::ty::TyCtxt;
+use rustc_span::Symbol;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{BasicBlockIdx, Place};
 use stable_mir::ty::Span;
 
-pub struct LoopInvariantBegin;
+pub struct LoopInvariantRegister;
 
-impl GotocHook for LoopInvariantBegin {
+impl GotocHook for LoopInvariantRegister {
  fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
- matches_function(tcx, instance.def, "KaniLoopInvariantBegin")
+ KaniAttributes::for_instance(tcx, instance).fn_marker()
+ == Some(Symbol::intern("kani_register_loop_contract"))
  }
 
  fn handle(
  &self,
  gcx: &mut GotocCtx,
- _instance: Instance,
+ instance: Instance,
  fargs: Vec<Expr>,
  _assign_to: &Place,
  target: Option<BasicBlockIdx>,
  span: Span,
  ) -> Stmt {
- assert_eq!(fargs.len(), 0);
  let loc = gcx.codegen_span_stable(span);
-
- // Start to record loop invariant statement
- gcx.loop_contracts_ctx.enter_loop_invariant_block();
-
- Stmt::goto(bb_label(target.unwrap()), loc)
- }
-}
-
-pub struct LoopInvariantEnd;
-
-impl GotocHook for LoopInvariantEnd {
- fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
- matches_function(tcx, instance.def, "KaniLoopInvariantEnd")
- }
-
- fn handle(
- &self,
- gcx: &mut GotocCtx,
- _instance: Instance,
- fargs: Vec<Expr>,
- _assign_to: &Place,
- target: Option<BasicBlockIdx>,
- span: Span,
- ) -> Stmt {
- assert_eq!(fargs.len(), 0);
- let loc = gcx.codegen_span_stable(span);
-
- // Stop to record loop invariant statement
- gcx.loop_contracts_ctx.exit_loop_invariant_block();
-
+ let func_exp = gcx.codegen_func_expr(instance, loc);
  Stmt::goto(bb_label(target.unwrap()), loc)
+ .with_loop_contracts(func_exp.call(fargs).cast_to(Type::CInteger(CIntType::Bool)))
  }
 }