Limit FFI calls by default to explicitly supported ones (rust-lang#2428)

celinval · zhassan-aws · web-flow · commit 6e91d1386f8a · 2023-05-05T14:09:48.000-07:00
C-FFI is fairly unstable right now and the lack of error handling causes a poor experience when things go wrong.

In this PR, we limit its usage to only support CBMC built-in functions that are explicitly included in Kani and alloc functions from kani_lib.c. User's should still be enable to go back to previous behavior by enabling unstable C-FFI support

Co-authored-by: Zyad Hassan &lt;88045115+zhassan-aws@users.noreply.github.com&gt;
diff --git a/cprover_bindings/src/goto_program/builtin.rs b/cprover_bindings/src/goto_program/builtin.rs
@@ -17,6 +17,8 @@ pub enum BuiltinFn {
     Copysignf,
     Cos,
     Cosf,
+    Error,
+    ErrorNoLocation,
     Exp,
     Exp2,
     Exp2f,
@@ -60,6 +62,7 @@ pub enum BuiltinFn {
     Sqrtf,
     Trunc,
     Truncf,
+    Unlink,
 }
 
 impl ToString for BuiltinFn {
@@ -76,6 +79,8 @@ impl ToString for BuiltinFn {
             Copysignf => "copysignf",
             Cos => "cos",
             Cosf => "cosf",
+            Error => "__error",
+            ErrorNoLocation => "__errno_location",
             Exp => "exp",
             Exp2 => "exp2",
             Exp2f => "exp2f",
@@ -119,6 +124,7 @@ impl ToString for BuiltinFn {
             Sqrtf => "sqrtf",
             Trunc => "trunc",
             Truncf => "truncf",
+            Unlink => "unlink",
         }
         .to_string()
     }
@@ -139,6 +145,8 @@ impl BuiltinFn {
             Copysignf => vec![Type::float(), Type::float()],
             Cos => vec![Type::double()],
             Cosf => vec![Type::float()],
+            Error => vec![],
+            ErrorNoLocation => vec![],
             Exp => vec![Type::double()],
             Exp2 => vec![Type::double()],
             Exp2f => vec![Type::float()],
@@ -179,6 +187,7 @@ impl BuiltinFn {
             Sqrtf => vec![Type::float()],
             Trunc => vec![Type::double()],
             Truncf => vec![Type::float()],
+            Unlink => vec![Type::c_char().to_pointer()],
         }
     }
 
@@ -195,6 +204,8 @@ impl BuiltinFn {
             Copysignf => Type::float(),
             Cos => Type::double(),
             Cosf => Type::float(),
+            Error => Type::c_int().to_pointer(),
+            ErrorNoLocation => Type::c_int().to_pointer(),
             Exp => Type::double(),
             Exp2 => Type::double(),
             Exp2f => Type::float(),
@@ -238,6 +249,7 @@ impl BuiltinFn {
             Sqrtf => Type::float(),
             Trunc => Type::double(),
             Truncf => Type::float(),
+            Unlink => Type::c_int(),
         }
     }
 
@@ -254,6 +266,8 @@ impl BuiltinFn {
             Copysignf,
             Cos,
             Cosf,
+            Error,
+            ErrorNoLocation,
             Exp,
             Exp2,
             Exp2f,
@@ -297,6 +311,7 @@ impl BuiltinFn {
             Sqrtf,
             Trunc,
             Truncf,
+            Unlink,
         ]
     }
 }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs
@@ -0,0 +1,161 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! This module implements foreign function handling.
+//!
+//! Kani currently only support CBMC built-in functions that are declared in the `cprover_bindings`
+//! crate, and allocation functions defined in `kani_lib.c`.
+//!
+//! All other functions will be replaced by an unimplemented check, due to current issues with
+//! linking and usability unless unstable C-FFI support is enabled.
+use std::collections::HashSet;
+
+use crate::codegen_cprover_gotoc::codegen::PropertyClass;
+use crate::codegen_cprover_gotoc::GotocCtx;
+use crate::kani_middle;
+use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
+use cbmc::{InternString, InternedString};
+use kani_queries::UserInput;
+use lazy_static::lazy_static;
+use rustc_middle::ty::Instance;
+use rustc_target::abi::call::Conv;
+use tracing::{debug, trace};
+
+lazy_static! {
+    /// The list of Rust allocation functions that are declared in the `core::alloc` module
+    /// but defined by each backend.
+    /// For our `goto-program` backend, these functions are defined inside `kani_lib.c`.
+    /// For now, we blindly trust that the definitions in `kani_lib.c` are kept in sync with the
+    /// declarations from the standard library, provided here:
+    /// <https://stdrs.dev/nightly/x86_64-unknown-linux-gnu/alloc/alloc/index.html>
+    static ref RUST_ALLOC_FNS: HashSet<InternedString> = {
+        HashSet::from([
+            "__rust_alloc".into(),
+            "__rust_alloc_zeroed".into(),
+            "__rust_dealloc".into(),
+            "__rust_realloc".into(),
+        ])
+    };
+}
+
+impl<'tcx> GotocCtx<'tcx> {
+    /// Generate the symbol and symbol table entry for foreign items.
+    ///
+    /// CBMC built-in functions that are supported by Kani are always added to the symbol table, and
+    /// this function will return them.
+    ///
+    /// For other foreign items, we declare a shim and add to the list of foreign shims to be
+    /// handled later.
+    pub fn codegen_foreign_fn(&mut self, instance: Instance<'tcx>) -> &Symbol {
+        debug!(?instance, "codegen_foreign_function");
+        let fn_name = self.symbol_name(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).conv == Conv::C)
+        {
+            // Add a Rust alloc lib function as is declared by core.
+            // When C-FFI feature is enabled, we just trust the rust declaration.
+            // TODO: Add proper casting and clashing definitions check.
+            // https://github.com/model-checking/kani/issues/1350
+            // https://github.com/model-checking/kani/issues/2426
+            self.ensure(fn_name, |gcx, _| {
+                let typ = gcx.codegen_ffi_type(instance);
+                Symbol::function(
+                    fn_name,
+                    typ,
+                    None,
+                    gcx.readable_instance_name(instance),
+                    Location::none(),
+                )
+                .with_is_extern(true)
+            })
+        } else {
+            let shim_name = format!("{fn_name}_ffi_shim");
+            trace!(?shim_name, "codegen_foreign_function");
+            self.ensure(&shim_name, |gcx, _| {
+                // Generate a shim with an unsupported C-FFI error message.
+                let typ = gcx.codegen_ffi_type(instance);
+                Symbol::function(
+                    &shim_name,
+                    typ,
+                    Some(gcx.codegen_ffi_shim(shim_name.as_str().into(), instance)),
+                    gcx.readable_instance_name(instance),
+                    Location::none(),
+                )
+            })
+        }
+    }
+
+    /// 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 {
+        self.queries.get_unstable_features().contains(&"c-ffi".to_string())
+    }
+
+    /// Generate code for a foreign function shim.
+    fn codegen_ffi_shim(&mut self, shim_name: InternedString, instance: Instance<'tcx>) -> Stmt {
+        debug!(?shim_name, ?instance, sym=?self.symbol_table.lookup(shim_name), "generate_foreign_shim");
+
+        let loc = self.codegen_span(&self.tcx.def_span(instance.def_id()));
+        let unsupported_check = self.codegen_ffi_unsupported(instance, loc);
+        Stmt::block(vec![unsupported_check], loc)
+    }
+
+    /// Generate type for the given foreign instance.
+    fn codegen_ffi_type(&mut self, instance: Instance<'tcx>) -> Type {
+        let fn_name = self.symbol_name(instance);
+        let fn_abi = kani_middle::fn_abi(self.tcx, instance);
+        let loc = self.codegen_span(&self.tcx.def_span(instance.def_id()));
+        let params = fn_abi
+            .args
+            .iter()
+            .enumerate()
+            .filter_map(|(idx, arg)| {
+                (!arg.is_ignore()).then(|| {
+                    let arg_name = format!("{fn_name}::param_{idx}");
+                    let base_name = format!("param_{idx}");
+                    let arg_type = self.codegen_ty(arg.layout.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);
+
+        if fn_abi.c_variadic {
+            Type::variadic_code(params, ret_type)
+        } else {
+            Type::code(params, ret_type)
+        }
+    }
+
+    /// Kani does not currently support FFI functions except for built-in CBMC functions.
+    ///
+    /// This will behave like `codegen_unimplemented_stmt` but print a message that includes
+    /// the name of the function not supported and the calling convention.
+    pub fn codegen_ffi_unsupported(&mut self, instance: Instance<'tcx>, loc: Location) -> Stmt {
+        let fn_name = &self.symbol_name(instance);
+        debug!(?fn_name, ?loc, "codegen_ffi_unsupported");
+
+        // Save this occurrence so we can emit a warning in the compilation report.
+        let entry = self.unsupported_constructs.entry("foreign function".into()).or_default();
+        entry.push(loc);
+
+        let call_conv = kani_middle::fn_abi(self.tcx, instance).conv;
+        let msg = format!("call to foreign \"{call_conv:?}\" function `{fn_name}`");
+        let url = if call_conv == Conv::C {
+            "https://github.com/model-checking/kani/issues/2423"
+        } else {
+            "https://github.com/model-checking/kani/issues/new/choose"
+        };
+        self.codegen_assert_assume(
+            Expr::bool_false(),
+            PropertyClass::UnsupportedConstruct,
+            &GotocCtx::unsupported_msg(&msg, Some(url)),
+            loc,
+        )
+    }
+}
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs
@@ -6,6 +6,7 @@
 
 mod assert;
 mod block;
+mod foreign_function;
 mod function;
 mod intrinsic;
 mod operand;
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -743,19 +743,18 @@ impl<'tcx> GotocCtx<'tcx> {
     /// 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<'tcx>) -> (&Symbol, Type) {
-        let func = self.symbol_name(instance);
         let funct = self.codegen_function_sig(self.fn_sig_of_instance(instance));
-        // make sure the functions imported from other modules (or externs) are in the symbol table
-        let sym = self.ensure(&func, |ctx, _| {
-            Symbol::function(
-                &func,
-                funct.clone(),
-                None,
-                ctx.readable_instance_name(instance),
-                Location::none(),
-            )
-            .with_is_extern(true)
-        });
+        let sym = if self.tcx.is_foreign_item(instance.def_id()) {
+            // Get the symbol that represents a foreign instance.
+            self.codegen_foreign_fn(instance)
+        } else {
+            // All non-foreign functions should've been declared beforehand.
+            trace!(func=?instance, "codegen_func_symbol");
+            let func = self.symbol_name(instance);
+            self.symbol_table
+                .lookup(func)
+                .expect("Function `{func}` should've been declared before usage")
+        };
         (sym, funct)
     }
 
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
@@ -8,16 +8,13 @@ use kani_metadata::{CbmcSolver, HarnessAttributes, Stub};
 use rustc_ast::{AttrKind, Attribute, LitKind, MetaItem, MetaItemKind, NestedMetaItem};
 use rustc_errors::ErrorGuaranteed;
 use rustc_hir::{def::DefKind, def_id::DefId};
-use rustc_middle::ty::{self, Instance, TyCtxt};
+use rustc_middle::ty::{Instance, TyCtxt};
 use rustc_span::Span;
 use std::str::FromStr;
 use strum_macros::{AsRefStr, EnumString};
 
-use rustc_middle::ty::layout::FnAbiOf;
 use tracing::{debug, trace};
 
-use crate::kani_middle::CompilerHelpers;
-
 use super::resolve;
 
 #[derive(Debug, Clone, Copy, AsRefStr, EnumString, PartialEq, Eq, PartialOrd, Ord)]
@@ -227,8 +224,7 @@ fn check_proof_attribute(tcx: TyCtxt, def_id: DefId, proof_attributes: &Vec<&Att
         tcx.sess.span_err(span, "the `proof` attribute cannot be applied to generic functions");
     } else {
         let instance = Instance::mono(tcx, def_id);
-        let helper = CompilerHelpers { tcx };
-        if !helper.fn_abi_of_instance(instance, ty::List::empty()).args.is_empty() {
+        if !super::fn_abi(tcx, instance).args.is_empty() {
             tcx.sess.span_err(span, "functions used as harnesses cannot have any arguments");
         }
     }
diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs
@@ -10,10 +10,10 @@ use rustc_hir::{def::DefKind, def_id::LOCAL_CRATE};
 use rustc_middle::mir::mono::MonoItem;
 use rustc_middle::span_bug;
 use rustc_middle::ty::layout::{
-    FnAbiError, FnAbiOfHelpers, FnAbiRequest, HasParamEnv, HasTyCtxt, LayoutError, LayoutOfHelpers,
-    TyAndLayout,
+    FnAbiError, FnAbiOf, FnAbiOfHelpers, FnAbiRequest, HasParamEnv, HasTyCtxt, LayoutError,
+    LayoutOfHelpers, TyAndLayout,
 };
-use rustc_middle::ty::{self, Ty, TyCtxt};
+use rustc_middle::ty::{self, Instance, Ty, TyCtxt};
 use rustc_span::source_map::respan;
 use rustc_span::Span;
 use rustc_target::abi::call::FnAbi;
@@ -72,6 +72,12 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem])
     tcx.sess.abort_if_errors();
 }
 
+/// Get the FnAbi of a given instance with no extra variadic arguments.
+pub fn fn_abi<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> &'tcx FnAbi<'tcx, Ty<'tcx>> {
+    let helper = CompilerHelpers { tcx };
+    helper.fn_abi_of_instance(instance, ty::List::empty())
+}
+
 struct CompilerHelpers<'tcx> {
     tcx: TyCtxt<'tcx>,
 }
diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs
@@ -410,7 +410,7 @@ pub fn format_result(
         result_str.push_str(
             "** WARNING: A Rust construct that is not currently supported \
         by Kani was found to be reachable. Check the results for \
-        more details.",
+        more details.\n",
         );
     }
     if has_unwinding_assertion_failures(properties) {
diff --git a/tests/cargo-kani/libc/Cargo.toml b/tests/cargo-kani/libc/Cargo.toml
@@ -0,0 +1,13 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "libc_checks"
+version = "0.1.0"
+edition = "2021"
+description = "Test integration with libc"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+libc = "0.2"
diff --git a/tests/cargo-kani/libc/check_create.expected b/tests/cargo-kani/libc/check_create.expected
@@ -0,0 +1,3 @@
+warning: Found the following unsupported constructs:\
+- foreign function
+Failed Checks: call to foreign "C" function `pthread_key_create` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/2423
diff --git a/tests/cargo-kani/libc/src/lib.rs b/tests/cargo-kani/libc/src/lib.rs
@@ -0,0 +1,4 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+pub mod pthread_key_create;
diff --git a/tests/cargo-kani/libc/src/pthread_key_create.rs b/tests/cargo-kani/libc/src/pthread_key_create.rs
@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Check that Kani doesn't crash if it invokes calls to pthread_key_create.
+//!
+//! The declaration of `pthread_key_create` in the libc crate differs in type from the C one.
+//! The rust libc crate uses `Option<unsafe extern "C" fn(*mut u8)>` to represent the optional
+//! destructor, while the C one takes a function pointer.
+//!
+//! See <https://github.com/model-checking/kani/issues/1781> for more details.
+//!
+//! Until we add full support to C-FFI, functions that are not explicitly declared in the Kani
+//! compiler setup will be codegen as unsupported.
+//!
+//! This test ensures that a harness only fails during verification if the call is reachable.
+use libc;
+
+#[kani::proof]
+pub fn check_create() {
+    let mut key = 0;
+    let _res = unsafe { libc::pthread_key_create(&mut key, None) };
+}
diff --git a/tests/expected/foreign-function/expected b/tests/expected/foreign-function/expected
diff --git a/tests/expected/foreign-function/ffi_ptr.rs b/tests/expected/foreign-function/ffi_ptr.rs
diff --git a/tests/kani/ForeignItems/extern_fn_ptr.rs b/tests/kani/ForeignItems/extern_fn_ptr.rs
diff --git a/tests/kani/FunctionCall/Variadic/fixme_main.rs b/tests/kani/FunctionCall/Variadic/fixme_main.rs
diff --git a/tests/ui/missing-function/extern_c/extern_c.rs b/tests/ui/missing-function/extern_c/extern_c.rs

Original file line number	Diff line number	Diff line change
`@@ -410,7 +410,7 @@ pub fn format_result(`
`410`	`410`	`result_str.push_str(`
`411`	`411`	`"** WARNING: A Rust construct that is not currently supported \`
`412`	`412`	`by Kani was found to be reachable. Check the results for \`
`413`		`- more details.",`
	`413`	`+ more details.\n",`
`414`	`414`	`);`
`415`	`415`	`}`
`416`	`416`	`if has_unwinding_assertion_failures(properties) {`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+warning: Found the following unsupported constructs:\`
	`2`	`+- foreign function`
	`3`	+Failed Checks: call to foreign "C" function `pthread_key_create` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/2423