Fix the error that Kani panics when there is no external parameter in quantifier's closure.

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

@@ -12,6 +12,7 @@ use rustc_abi::{FieldsShape, Primitive, TagEncoding, Variants};
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::{List, TypingEnv};
 use rustc_smir::rustc_internal;
+use stable_mir::CrateDef;
 use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
 use stable_mir::mir::mono::{Instance, InstanceKind};
 use stable_mir::mir::{
@@ -567,12 +568,41 @@ impl GotocCtx<'_> {
     /// Generate Goto-C for each argument to a function call.
     ///
     /// N.B. public only because instrinsics use this directly, too.
-    pub(crate) fn codegen_funcall_args(&mut self, fn_abi: &FnAbi, args: &[Operand]) -> Vec<Expr> {
+    pub(crate) fn codegen_funcall_args_for_quantifiers(
+        &mut self,
+        fn_abi: &FnAbi,
+        args: &[Operand],
+    ) -> Vec<Expr> {
         let fargs: Vec<Expr> = args
             .iter()
             .enumerate()
             .filter_map(|(i, op)| {
                 // Functions that require caller info will have an extra parameter.
+                let arg_abi = &fn_abi.args.get(i);
+                let ty = self.operand_ty_stable(op);
+                if ty.kind().is_bool() {
+                    Some(self.codegen_operand_stable(op).cast_to(Type::c_bool()))
+                } else if ty.kind().is_closure()
+                    || (arg_abi.is_none_or(|abi| abi.mode != PassMode::Ignore))
+                {
+                    Some(self.codegen_operand_stable(op))
+                } else {
+                    None
+                }
+            })
+            .collect();
+        debug!(?fargs, args_abi=?fn_abi.args, "codegen_funcall_args");
+        fargs
+    }
+
+    /// Generate Goto-C for each argument to a function call.
+    ///
+    /// N.B. public only because instrinsics use this directly, too.
+    pub(crate) fn codegen_funcall_args(&mut self, fn_abi: &FnAbi, args: &[Operand]) -> Vec<Expr> {
+        let fargs: Vec<Expr> = args
+            .iter()
+            .enumerate()
+            .filter_map(|(i, op)| {
                 let arg_abi = &fn_abi.args.get(i);
                 let ty = self.operand_ty_stable(op);
                 if ty.kind().is_bool() {
@@ -639,7 +669,13 @@ impl GotocCtx<'_> {
                 let mut fargs = if args.is_empty()
                     || fn_def.fn_sig().unwrap().value.abi != Abi::RustCall
                 {
-                    self.codegen_funcall_args(&fn_abi, args)
+                    if instance.def.name() == "kani::internal::kani_forall"
+                        || (instance.def.name() == "kani::internal::kani_exists")
+                    {
+                        self.codegen_funcall_args_for_quantifiers(&fn_abi, args)
+                    } else {
+                        self.codegen_funcall_args(&fn_abi, args)
+                    }
                 } else {
                     let (untupled, first_args) = args.split_last().unwrap();
                     let mut fargs = self.codegen_funcall_args(&fn_abi, first_args);

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

@@ -823,8 +823,13 @@ fn handle_quantifier(
     let upper_bound = &fargs[1];
     let closure_call_expr = find_closure_call_expr(&instance, gcx, loc)
         .unwrap_or_else(|| unreachable!("Failed to find closure call expression"));
-
-    let predicate = Expr::address_of(fargs[2].clone());
+    let closure_arg = fargs[2].clone();
+    let predicate = if closure_arg.is_symbol() {
+        Expr::address_of(closure_arg)
+    } else {
+        let predicate_ty = fargs[2].typ().clone().to_pointer();
+        Expr::nondet(predicate_ty)
+    };
 
     // Quantified variable.
     let base_name = "kani_quantified_var".to_string();

tests/expected/quantifiers/quantifier_with_no_external_variable.expected

@@ -0,0 +1,5 @@
+- Status: SUCCESS\
+- Description: "assertion failed: quan"
+
+VERIFICATION:- SUCCESSFUL
+

tests/expected/quantifiers/quantifier_with_no_external_variable.rs

@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+/// Quantifier with no external variable in the closure
+
+#[kani::proof]
+fn test() {
+    let quan = kani::exists!(|j in (0, 100)| j == 0);
+    assert!(quan);
+}