Codegen the arguments to Kani intrinsics inside the functions that ha…

…ndle the intrinsics (#2924)

This is a refactor change: currently, the functions that codegen Kani
intrinsics (asserts, assumes, etc.) take the arguments to the intrinsics
as Boogie expressions (`boogie_ast::boogie_program::Expr`). In other
words, the MIR arguments (`rustc_middle::mir::syntax::Operand`) are
converted to Boogie expressions before passing them to the functions.

This PR changes the functions to take the MIR arguments directly, and
perform the codegen into Boogie expressions inside the functions. This
allows those functions to query any information in the MIR `Operand`,
that is not available after codegen to Boogie expressions.

Note: it may make sense to do the same change for the Goto backend to
avoid having to pattern match on the expressions (e.g.
https://github.com/model-checking/kani/blob/2aca488ba9d64d2aaeae3b7774acf367bea42be9/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs#L74),
and instead get the information needed from the MIR operand directly.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

kani-compiler/src/codegen_boogie/context/boogie_ctx.rs

@@ -339,7 +339,6 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> {
  span: Span,
  ) -> Stmt {
  debug!(?func, ?args, ?destination, ?span, "codegen_funcall");
- let fargs = self.codegen_funcall_args(args);
  let funct = self.operand_ty(func);
  // TODO: Only Kani intrinsics are handled currently
  match &funct.kind() {
@@ -355,12 +354,13 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> {
  return self.codegen_kani_intrinsic(
  intrinsic,
  instance,
- fargs,
+ args,
  *destination,
  *target,
  Some(span),
  );
  }
+ let _fargs = self.codegen_funcall_args(args);
  todo!()
  }
  _ => todo!(),
@@ -383,7 +383,7 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> {
  .collect()
  }
 
- fn codegen_operand(&self, o: &Operand<'tcx>) -> Expr {
+ pub(crate) fn codegen_operand(&self, o: &Operand<'tcx>) -> Expr {
  trace!(operand=?o, "codegen_operand");
  // A MIR operand is either a constant (literal or `const` declaration)
  // or a place (being moved or copied for this operation).

kani-compiler/src/codegen_boogie/context/kani_intrinsic.rs

@@ -7,8 +7,8 @@
 
 use super::boogie_ctx::FunctionCtx;
 
-use boogie_ast::boogie_program::{Expr, Stmt};
-use rustc_middle::mir::{BasicBlock, Place};
+use boogie_ast::boogie_program::Stmt;
+use rustc_middle::mir::{BasicBlock, Operand, Place};
 use rustc_middle::ty::{Instance, TyCtxt};
 use rustc_span::Span;
 use std::str::FromStr;
@@ -49,32 +49,32 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> {
  &self,
  intrinsic: KaniIntrinsic,
  instance: Instance<'tcx>,
- fargs: Vec<Expr>,
+ args: &[Operand<'tcx>],
  assign_to: Place<'tcx>,
  target: Option<BasicBlock>,
  span: Option<Span>,
  ) -> Stmt {
  match intrinsic {
  KaniIntrinsic::KaniAssert => {
- self.codegen_kani_assert(instance, fargs, assign_to, target, span)
+ self.codegen_kani_assert(instance, args, assign_to, target, span)
  }
  KaniIntrinsic::KaniAssume => {
- self.codegen_kani_assume(instance, fargs, assign_to, target, span)
+ self.codegen_kani_assume(instance, args, assign_to, target, span)
  }
  }
  }
 
  pub fn codegen_kani_assert(
  &self,
  _instance: Instance<'tcx>,
- mut fargs: Vec<Expr>,
+ args: &[Operand<'tcx>],
  _assign_to: Place<'tcx>,
  _target: Option<BasicBlock>,
  _span: Option<Span>,
  ) -> Stmt {
  // TODO: ignoring the `'static str` argument for now
- assert_eq!(fargs.len(), 1); // 2);
- let cond = fargs.remove(0);
+ assert_eq!(args.len(), 2);
+ let cond = self.codegen_operand(&args[0]);
  // TODO: handle message
  // TODO: handle location
 
@@ -89,13 +89,13 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> {
  pub fn codegen_kani_assume(
  &self,
  _instance: Instance<'tcx>,
- mut fargs: Vec<Expr>,
+ args: &[Operand<'tcx>],
  _assign_to: Place<'tcx>,
  _target: Option<BasicBlock>,
  _span: Option<Span>,
  ) -> Stmt {
- assert_eq!(fargs.len(), 1);
- let cond = fargs.remove(0);
+ assert_eq!(args.len(), 1);
+ let cond = self.codegen_operand(&args[0]);
  // TODO: handle location
 
  Stmt::Block {