Represent FnDefs as zero-sized structs instead of Code (#1338)

Author: fzaiser

cprover_bindings/src/goto_program/typ.rs

@@ -185,13 +185,12 @@ impl DatatypeComponent {
     }
 
     pub fn field<T: Into<InternedString>>(name: T, typ: Type) -> Self {
-        // TODO <https://github.com/model-checking/kani/issues/1243>
-        // assert!(
-        //     Self::typecheck_datatype_field(&typ),
-        //     "Illegal field.\n\tName: {}\n\tType: {:?}",
-        //     name.into(),
-        //     typ
-        // );
+        assert!(
+            Self::typecheck_datatype_field(&typ),
+            "Illegal field.\n\tName: {}\n\tType: {:?}",
+            name.into(),
+            typ
+        );
         let name = name.into();
         Field { name, typ }
     }

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

@@ -349,7 +349,7 @@ impl<'tcx> GotocCtx<'tcx> {
     ) -> Expr {
         let instance =
             Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), d, substs).unwrap().unwrap();
-        self.codegen_func_expr(instance, span)
+        self.codegen_fn_item(instance, span)
     }
 
     fn codegen_alloc_pointer(
@@ -627,11 +627,17 @@ impl<'tcx> GotocCtx<'tcx> {
         self.find_function(&fname).unwrap().call(vec![init])
     }
 
-    pub fn codegen_func_expr(&mut self, instance: Instance<'tcx>, span: Option<&Span>) -> Expr {
+    /// 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>.
+    pub fn codegen_func_symbol(&mut self, instance: Instance<'tcx>) -> (&Symbol, Type) {
         let func = self.symbol_name(instance);
         let funct = self.codegen_function_sig(self.fn_sig_of_instance(instance).unwrap());
         // make sure the functions imported from other modules are in the symbol table
-        self.ensure(&func, |ctx, _| {
+        let sym = self.ensure(&func, |ctx, _| {
             Symbol::function(
                 &func,
                 funct.clone(),
@@ -641,6 +647,40 @@ impl<'tcx> GotocCtx<'tcx> {
             )
             .with_is_extern(true)
         });
-        Expr::symbol_expression(func, funct).with_location(self.codegen_span_option(span.cloned()))
+        (sym, funct)
+    }
+
+    /// For a given function instance, generates an expression for the function symbol of type `Code`.
+    ///
+    /// Note: use `codegen_func_expr_zst` in the general case because GotoC does not allow functions to be used in all contexts
+    /// (e.g. struct fields).
+    ///
+    /// For details, see <https://github.com/model-checking/kani/pull/1338>
+    pub fn codegen_func_expr(&mut self, instance: Instance<'tcx>, span: Option<&Span>) -> Expr {
+        let (func_symbol, func_typ) = self.codegen_func_symbol(instance);
+        Expr::symbol_expression(func_symbol.name, func_typ)
+            .with_location(self.codegen_span_option(span.cloned()))
+    }
+
+    /// For a given function instance, generates a zero-sized dummy symbol of type `Struct`.
+    ///
+    /// This is often necessary because GotoC does not allow functions to be used in all contexts (e.g. struct fields).
+    /// For details, see <https://github.com/model-checking/kani/pull/1338>
+    ///
+    /// Note: use `codegen_func_expr` instead if you want to call the function immediately.
+    fn codegen_fn_item(&mut self, instance: Instance<'tcx>, span: Option<&Span>) -> Expr {
+        let (func_symbol, _) = self.codegen_func_symbol(instance);
+        let func = func_symbol.name;
+        let fn_struct_ty = self.codegen_fndef_type(instance);
+        // This zero-sized object that a function name refers to in Rust is globally unique, so we create such a global object.
+        let fn_singleton_name = format!("{func}::FnDefSingleton");
+        let fn_singleton = self.ensure_global_var(
+            &fn_singleton_name,
+            false,
+            fn_struct_ty.clone(),
+            Location::none(),
+            |_, _| None, // zero-sized, so no initialization necessary
+        );
+        fn_singleton.with_location(self.codegen_span_option(span.cloned()))
     }
 }

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

@@ -696,7 +696,18 @@ impl<'tcx> GotocCtx<'tcx> {
         t: Ty<'tcx>,
     ) -> Expr {
         match k {
-            PointerCast::ReifyFnPointer => self.codegen_operand(o).address_of(),
+            PointerCast::ReifyFnPointer => match self.operand_ty(o).kind() {
+                ty::FnDef(def_id, substs) => {
+                    let instance =
+                        Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, substs)
+                            .unwrap()
+                            .unwrap();
+                    // We need to handle this case in a special way because `codegen_operand` compiles FnDefs to dummy structs.
+                    // (cf. the function documentation)
+                    self.codegen_func_expr(instance, None).address_of()
+                }
+                _ => unreachable!(),
+            },
             PointerCast::UnsafeFnPointer => self.codegen_operand(o),
             PointerCast::ClosureFnPointer(_) => {
                 let dest_typ = self.codegen_ty(t);

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

@@ -431,7 +431,9 @@ impl<'tcx> GotocCtx<'tcx> {
                     | InstanceDef::ReifyShim(..)
                     | InstanceDef::ClosureOnceShim { .. }
                     | InstanceDef::CloneShim(..) => {
-                        let func_exp = self.codegen_operand(func);
+                        // 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(destination, func_exp.call(fargs))
                                 .with_location(loc),

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

@@ -611,9 +611,12 @@ impl<'tcx> GotocCtx<'tcx> {
             ty::Slice(e) => self.codegen_ty(*e).flexible_array_of(),
             ty::Str => Type::c_char().flexible_array_of(),
             ty::Ref(_, t, _) | ty::RawPtr(ty::TypeAndMut { ty: t, .. }) => self.codegen_ty_ref(*t),
-            ty::FnDef(_, _) => {
-                let sig = self.monomorphize(ty.fn_sig(self.tcx));
-                self.codegen_function_sig(sig)
+            ty::FnDef(def_id, substs) => {
+                let instance =
+                    Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, substs)
+                        .unwrap()
+                        .unwrap();
+                self.codegen_fndef_type(instance)
             }
             ty::FnPtr(sig) => self.codegen_function_sig(*sig).to_pointer(),
             ty::Closure(_, subst) => self.codegen_ty_closure(ty, subst),
@@ -989,6 +992,22 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
+    /// Creates a zero-sized struct for a FnDef.
+    ///
+    /// A FnDef instance in Rust is a zero-sized type, which can be passed around directly, without creating a pointer.
+    /// (Rust docs: <https://doc.rust-lang.org/reference/types/function-item.html>)
+    /// To mirror this in GotoC, we create a dummy struct for the function, similarly to what we do for closures.
+    ///
+    /// For details, see <https://github.com/model-checking/kani/pull/1338>
+    pub fn codegen_fndef_type(&mut self, instance: Instance<'tcx>) -> Type {
+        let func = self.symbol_name(instance);
+        self.ensure_struct(
+            format!("{func}::FnDefStruct"),
+            Some(self.readable_instance_name(instance)),
+            |_, _| vec![],
+        )
+    }
+
     /// codegen for struct
     ///
     /// they are literally codegen'ed in the corresponding way (except the order of fields might not be preserved)
@@ -1374,7 +1393,6 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Whether a variable of type ty should be ignored as a parameter to a function
     pub fn ignore_var_ty(&self, ty: Ty<'tcx>) -> bool {
         match ty.kind() {
-            ty::FnDef(_, _) => true,
             // Ignore variables of the generator type until we add support for
             // them:
             // https://github.com/model-checking/kani/issues/416

tests/kani/FunctionSymbols/fixme_main.rs

@@ -0,0 +1,8 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// size_of is not supported yet:
+#[kani::proof]
+fn assert_fndef_zst() {
+    assert_eq!(std::mem::size_of_val(&h), 0);
+}

tests/kani/FunctionSymbols/issue1243.rs

@@ -0,0 +1,32 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Examples discovered while debugging issue https://github.com/model-checking/kani/issues/1243
+
+#[kani::proof]
+fn example1() {
+    f(h);
+}
+
+fn f(g: impl Fn() -> ()) {
+    move || g();
+}
+
+fn h() {}
+
+#[kani::proof]
+fn example2() {
+    std::iter::empty().try_fold(0, map_try_fold(&mut |x: usize| x, usize::checked_add));
+}
+
+fn map_try_fold<'a, T, B, Acc, R>(
+    f: &'a mut impl FnMut(T) -> B,
+    mut g: impl FnMut(Acc, B) -> R + 'a,
+) -> impl FnMut(Acc, T) -> R + 'a {
+    move |acc, elt| g(acc, f(elt))
+}
+
+#[kani::proof]
+fn example3() {
+    Vec::<String>::new().join("");
+}

tests/kani/FunctionSymbols/main.rs

@@ -0,0 +1,35 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Test code generation for FnDef items
+
+#[kani::proof]
+fn test_reify_fn_pointer() {
+    assert!(poly::<usize> as fn() == poly::<usize> as fn());
+    assert!(poly::<isize> as fn() != poly::<usize> as fn());
+}
+
+fn poly<T>() {}
+
+#[kani::proof]
+fn test_fn_pointer_call() {
+    let x: bool = kani::any();
+    assert_eq!(id(x), x);
+    assert_eq!((id::<bool> as fn(bool) -> bool)(x), x);
+}
+
+fn id<T>(x: T) -> T {
+    x
+}
+
+struct Wrapper<T> {
+    inner: T,
+}
+
+#[kani::proof]
+fn test_fn_wrapper() {
+    let w = Wrapper { inner: id::<bool> };
+    assert!(w.inner as fn(bool) -> bool == id::<bool> as fn(bool) -> bool);
+    let x: bool = kani::any();
+    assert_eq!((w.inner)(x), x);
+}