Fix ICEs due to mismatched arguments

cprover_bindings/src/goto_program/expr.rs

@@ -508,13 +508,13 @@ impl Expr {
 
     /// `(typ) self`.
     pub fn cast_to(self, typ: Type) -> Self {
-        assert!(self.can_cast_to(&typ), "Can't cast\n\n{self:?} ({:?})\n\n{typ:?}", self.typ);
         if self.typ == typ {
             self
         } else if typ.is_bool() {
             let zero = self.typ.zero();
             self.neq(zero)
         } else {
+            assert!(self.can_cast_to(&typ), "Can't cast\n\n{self:?} ({:?})\n\n{typ:?}", self.typ);
             expr!(Typecast(self), typ)
         }
     }
@@ -688,7 +688,8 @@ impl Expr {
     pub fn call(self, arguments: Vec<Expr>) -> Self {
         assert!(
             Expr::typecheck_call(&self, &arguments),
-            "Function call does not type check:\nfunc: {self:?}\nargs: {arguments:?}"
+            "Function call does not type check:\nfunc params: {:?}\nargs: {arguments:?}",
+            self.typ().parameters().unwrap_or(&vec![])
         );
         let typ = self.typ().return_type().unwrap().clone();
         expr!(FunctionCall { function: self, arguments }, typ)

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

@@ -11,13 +11,14 @@ use std::collections::HashSet;
 
 use crate::codegen_cprover_gotoc::codegen::PropertyClass;
 use crate::codegen_cprover_gotoc::GotocCtx;
-use crate::kani_middle;
+use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
 use cbmc::{InternString, InternedString};
 use lazy_static::lazy_static;
-use rustc_smir::rustc_internal;
-use rustc_target::abi::call::Conv;
+use stable_mir::abi::{CallConvention, PassMode};
 use stable_mir::mir::mono::Instance;
+use stable_mir::mir::Place;
+use stable_mir::ty::{RigidTy, TyKind};
 use stable_mir::CrateDef;
 use tracing::{debug, trace};
 
@@ -48,14 +49,12 @@ impl<'tcx> GotocCtx<'tcx> {
     /// handled later.
     pub fn codegen_foreign_fn(&mut self, instance: Instance) -> &Symbol {
         debug!(?instance, "codegen_foreign_function");
-        let instance_internal = rustc_internal::internal(instance);
         let fn_name = self.symbol_name_stable(instance).intern();
         if self.symbol_table.contains(fn_name) {
             // Symbol has been added (either a built-in CBMC function or a Rust allocation function).
             self.symbol_table.lookup(fn_name).unwrap()
         } else if RUST_ALLOC_FNS.contains(&fn_name)
-            || (self.is_cffi_enabled()
-                && kani_middle::fn_abi(self.tcx, instance_internal).conv == Conv::C)
+            || (self.is_cffi_enabled() && instance.fn_abi().unwrap().conv == CallConvention::C)
         {
             // Add a Rust alloc lib function as is declared by core.
             // When C-FFI feature is enabled, we just trust the rust declaration.
@@ -84,6 +83,40 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
+    /// Generate a function call to a foreign function by potentially casting arguments and return value, since
+    /// the external function definition may not match exactly its Rust declaration.
+    /// See <https://github.com/model-checking/kani/issues/1350#issuecomment-1192036619> for more details.
+    pub fn codegen_foreign_call(
+        &mut self,
+        fn_expr: Expr,
+        args: Vec<Expr>,
+        ret_place: &Place,
+        loc: Location,
+    ) -> Stmt {
+        let expected_args = fn_expr
+            .typ()
+            .parameters()
+            .unwrap()
+            .iter()
+            .zip(args)
+            .map(|(param, arg)| arg.cast_to(param.typ().clone()))
+            .collect::<Vec<_>>();
+        let call_expr = fn_expr.call(expected_args);
+
+        let ret_kind = self.place_ty_stable(ret_place).kind();
+        if ret_kind.is_unit() || matches!(ret_kind, TyKind::RigidTy(RigidTy::Never)) {
+            call_expr.as_stmt(loc)
+        } else {
+            let ret_expr = unwrap_or_return_codegen_unimplemented_stmt!(
+                self,
+                self.codegen_place_stable(ret_place)
+            )
+            .goto_expr;
+            let ret_type = ret_expr.typ().clone();
+            ret_expr.assign(call_expr.cast_to(ret_type), loc)
+        }
+    }
+
     /// Checks whether C-FFI has been enabled or not.
     /// When enabled, we blindly encode the function type as is.
     fn is_cffi_enabled(&self) -> bool {
@@ -102,24 +135,24 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Generate type for the given foreign instance.
     fn codegen_ffi_type(&mut self, instance: Instance) -> Type {
         let fn_name = self.symbol_name_stable(instance);
-        let fn_abi = kani_middle::fn_abi(self.tcx, rustc_internal::internal(instance));
+        let fn_abi = instance.fn_abi().unwrap();
         let loc = self.codegen_span_stable(instance.def.span());
         let params = fn_abi
             .args
             .iter()
             .enumerate()
-            .filter(|&(_, arg)| (!arg.is_ignore()))
+            .filter(|&(_, arg)| (arg.mode != PassMode::Ignore))
             .map(|(idx, arg)| {
                 let arg_name = format!("{fn_name}::param_{idx}");
                 let base_name = format!("param_{idx}");
-                let arg_type = self.codegen_ty(arg.layout.ty);
+                let arg_type = self.codegen_ty_stable(arg.ty);
                 let sym = Symbol::variable(&arg_name, &base_name, arg_type.clone(), loc)
                     .with_is_parameter(true);
                 self.symbol_table.insert(sym);
                 arg_type.as_parameter(Some(arg_name.into()), Some(base_name.into()))
             })
             .collect();
-        let ret_type = self.codegen_ty(fn_abi.ret.layout.ty);
+        let ret_type = self.codegen_ty_stable(fn_abi.ret.ty);
 
         if fn_abi.c_variadic {
             Type::variadic_code(params, ret_type)
@@ -140,9 +173,9 @@ impl<'tcx> GotocCtx<'tcx> {
         let entry = self.unsupported_constructs.entry("foreign function".into()).or_default();
         entry.push(loc);
 
-        let call_conv = kani_middle::fn_abi(self.tcx, rustc_internal::internal(instance)).conv;
+        let call_conv = instance.fn_abi().unwrap().conv;
         let msg = format!("call to foreign \"{call_conv:?}\" function `{fn_name}`");
-        let url = if call_conv == Conv::C {
+        let url = if call_conv == CallConvention::C {
             "https://github.com/model-checking/kani/issues/2423"
         } else {
             "https://github.com/model-checking/kani/issues/new/choose"

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

@@ -210,7 +210,7 @@ impl<'tcx> GotocCtx<'tcx> {
         self.ensure(&self.symbol_name_stable(instance), |ctx, fname| {
             Symbol::function(
                 fname,
-                ctx.fn_typ(&body),
+                ctx.fn_typ(instance, &body),
                 None,
                 instance.name(),
                 ctx.codegen_span_stable(instance.def.span()),

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

@@ -574,13 +574,7 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     /// Ensure that the given instance is in the symbol table, returning the symbol.
-    ///
-    /// FIXME: The function should not have to return the type of the function symbol as well
-    /// because the symbol should have the type. The problem is that the type in the symbol table
-    /// sometimes subtly differs from the type that codegen_function_sig returns.
-    /// This is tracked in <https://github.com/model-checking/kani/issues/1350>.
-    fn codegen_func_symbol(&mut self, instance: Instance) -> (&Symbol, Type) {
-        let funct = self.codegen_function_sig_stable(self.fn_sig_of_instance_stable(instance));
+    fn codegen_func_symbol(&mut self, instance: Instance) -> &Symbol {
         let sym = if instance.is_foreign_item() {
             // Get the symbol that represents a foreign instance.
             self.codegen_foreign_fn(instance)
@@ -592,7 +586,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 .lookup(&func)
                 .unwrap_or_else(|| panic!("Function `{func}` should've been declared before usage"))
         };
-        (sym, funct)
+        sym
     }
 
     /// Generate a goto expression that references the function identified by `instance`.
@@ -601,8 +595,8 @@ impl<'tcx> GotocCtx<'tcx> {
     ///
     /// This should not be used where Rust expects a "function item" (See `codegen_fn_item`)
     pub fn codegen_func_expr(&mut self, instance: Instance, span: Option<Span>) -> Expr {
-        let (func_symbol, func_typ) = self.codegen_func_symbol(instance);
-        Expr::symbol_expression(func_symbol.name, func_typ)
+        let func_symbol = self.codegen_func_symbol(instance);
+        Expr::symbol_expression(func_symbol.name, func_symbol.typ.clone())
             .with_location(self.codegen_span_option_stable(span))
     }
 
@@ -612,7 +606,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// This is the Rust "function item". See <https://doc.rust-lang.org/reference/types/function-item.html>
     /// This is not the function pointer, for that use `codegen_func_expr`.
     fn codegen_fn_item(&mut self, instance: Instance, span: Option<Span>) -> Expr {
-        let (func_symbol, _) = self.codegen_func_symbol(instance);
+        let func_symbol = self.codegen_func_symbol(instance);
         let mangled_name = func_symbol.name;
         let fn_item_struct_ty = self.codegen_fndef_type_stable(instance);
         // This zero-sized object that a function name refers to in Rust is globally unique, so we create such a global object.

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

@@ -135,7 +135,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 "https://github.com/model-checking/kani/issues/692",
             ),
             TerminatorKind::Return => {
-                let rty = self.current_fn().sig().output();
+                let rty = self.current_fn().instance_stable().fn_abi().unwrap().ret.ty;
                 if rty.kind().is_unit() {
                     self.codegen_ret_unit()
                 } else {
@@ -145,7 +145,8 @@ impl<'tcx> GotocCtx<'tcx> {
                         self.codegen_place_stable(&place)
                     )
                     .goto_expr;
-                    if self.place_ty_stable(&place).kind().is_bool() {
+                    assert_eq!(rty, self.place_ty_stable(&place), "Unexpected return type");
+                    if rty.kind().is_bool() {
                         place_expr.cast_to(Type::c_bool()).ret(loc)
                     } else {
                         place_expr.ret(loc)
@@ -555,10 +556,17 @@ impl<'tcx> GotocCtx<'tcx> {
                         // We need to handle FnDef items in a special way because `codegen_operand` compiles them to dummy structs.
                         // (cf. the function documentation)
                         let func_exp = self.codegen_func_expr(instance, None);
-                        vec![
-                            self.codegen_expr_to_place_stable(destination, func_exp.call(fargs))
+                        if instance.is_foreign_item() {
+                            vec![self.codegen_foreign_call(func_exp, fargs, destination, loc)]
+                        } else {
+                            vec![
+                                self.codegen_expr_to_place_stable(
+                                    destination,
+                                    func_exp.call(fargs),
+                                )
                                 .with_location(loc),
-                        ]
+                            ]
+                        }
                     }
                 };
                 stmts.push(self.codegen_end_call(*target, loc));

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

@@ -9,7 +9,6 @@
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Type;
 use rustc_middle::ty::layout::{LayoutOf, TyAndLayout};
-use rustc_middle::ty::{self};
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{Local, Operand, Place, Rvalue};
@@ -53,13 +52,6 @@ impl<'tcx> GotocCtx<'tcx> {
         )
     }
 
-    pub fn fn_sig_of_instance_stable(&self, instance: Instance) -> FnSig {
-        let fn_sig = self.fn_sig_of_instance(rustc_internal::internal(instance));
-        let fn_sig =
-            self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), fn_sig);
-        rustc_internal::stable(fn_sig)
-    }
-
     pub fn use_fat_pointer_stable(&self, pointer_ty: Ty) -> bool {
         self.use_fat_pointer(rustc_internal::internal(pointer_ty))
     }