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

…ndle the intrinsics
model-checking · Dec 8, 2023 · 6678f87 · 6678f87
1 parent 3c4289c
commit 6678f87
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 14 deletions.
diff --git a/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs b/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).

diff --git a/kani-compiler/src/codegen_boogie/context/kani_intrinsic.rs b/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 {