diff --git a/cprover_bindings/src/goto_program/builtin.rs b/cprover_bindings/src/goto_program/builtin.rs index 35e68ad9a6ca6..dc703ce83edcb 100644 --- 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 new file mode 100644 index 0000000000000..cec0be67cff3e --- /dev/null +++ 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: + /// + static ref RUST_ALLOC_FNS: HashSet = { + 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 index 7ae375b8e187b..4dbd0385f62c9 100644 --- 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 index f33a454ee79d8..2b6c26a7592b5 100644 --- 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 . 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 index 80c9a970ea0e1..6d6f98cf300bf 100644 --- 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 index dc5a8986c409f..fba7094a3cc4b 100644 --- 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 index 012fcaca0aa07..d50672ec42080 100644 --- 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 new file mode 100644 index 0000000000000..c0cf7d189bead --- /dev/null +++ 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 new file mode 100644 index 0000000000000..61ed6285e7412 --- /dev/null +++ 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 new file mode 100644 index 0000000000000..5c55c5a5232d0 --- /dev/null +++ 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 new file mode 100644 index 0000000000000..d939728ef72f3 --- /dev/null +++ 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` to represent the optional +//! destructor, while the C one takes a function pointer. +//! +//! See 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 new file mode 100644 index 0000000000000..3a8e39f0911c2 --- /dev/null +++ b/tests/expected/foreign-function/expected @@ -0,0 +1,10 @@ +Checking harness check_fn_ptr_not_called... +VERIFICATION:- SUCCESSFUL + +Checking harness check_fn_ptr_called... +Failed Checks: call to foreign "C" function `foreign` is not currently supported by Kani +VERIFICATION:- FAILED + +Summary:\ +Verification failed for - check_fn_ptr_called\ +Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/expected/foreign-function/ffi_ptr.rs b/tests/expected/foreign-function/ffi_ptr.rs new file mode 100644 index 0000000000000..7e50f49b336d2 --- /dev/null +++ b/tests/expected/foreign-function/ffi_ptr.rs @@ -0,0 +1,29 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check Kani handling of C-FFI function pointers when C-FFI support is disabled. + +extern "C" { + fn foreign(i: u32) -> u32; +} + +fn call_on(input: u32, func: unsafe extern "C" fn(u32) -> u32) -> u32 { + unsafe { func(input) } +} + +fn may_not_call(call: bool, input: u32, func: unsafe extern "C" fn(u32) -> u32) -> Option { + call.then(|| unsafe { func(input) }) +} + +#[kani::proof] +fn check_fn_ptr_called() { + let input: u32 = kani::any(); + assert_eq!(call_on(input, foreign), input); +} + +#[kani::proof] +fn check_fn_ptr_not_called() { + let input: u32 = kani::any(); + let should_call = kani::any_where(|v| !v); + assert_eq!(may_not_call(should_call, input, foreign), None); +} diff --git a/tests/kani/ForeignItems/extern_fn_ptr.rs b/tests/kani/ForeignItems/extern_fn_ptr.rs new file mode 100644 index 0000000000000..e884f93160102 --- /dev/null +++ b/tests/kani/ForeignItems/extern_fn_ptr.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z c-ffi --c-lib tests/kani/ForeignItems/lib.c + +//! Check that Kani correctly handles function pointers to C functions. +//! Note that Kani today trusts that the extern declaration is compatible with the C definition. +//! Failures to do so will result in a CBMC type mismatch. + +extern "C" { + /// Returns i + 2 + fn takes_int(i: u32) -> u32; +} + +fn call_on(input: u32, func: Option u32>) -> Option { + func.and_then(|f| Some(unsafe { f(input) })) +} + +#[kani::proof] +fn check_extern_fn_ptr() { + let input: u32 = kani::any(); + assert_eq!(call_on(0, None), None); + assert_eq!(call_on(input, Some(takes_int)).unwrap(), unsafe { takes_int(input) }); +} diff --git a/tests/kani/FunctionCall/Variadic/fixme_main.rs b/tests/kani/FunctionCall/Variadic/fixme_main.rs index ab312836dec22..1693218e975bb 100644 --- a/tests/kani/FunctionCall/Variadic/fixme_main.rs +++ b/tests/kani/FunctionCall/Variadic/fixme_main.rs @@ -17,8 +17,10 @@ pub unsafe extern "C" fn my_add(num: c_long, mut args: ...) -> c_long { #[kani::proof] fn main() { let arg0: c_long = 2; - let arg1: c_long = 3; let arg1: c_long = 4; let x = unsafe { my_add(0, arg0, arg1) }; - assert!(x == 7); + assert!(x == 0); + + let x = unsafe { my_add(2, arg0, arg1) }; + assert!(x == 6); } diff --git a/tests/ui/missing-function/extern_c/extern_c.rs b/tests/ui/missing-function/extern_c/extern_c.rs index 75059a8a4263c..db3d322f62e24 100644 --- a/tests/ui/missing-function/extern_c/extern_c.rs +++ b/tests/ui/missing-function/extern_c/extern_c.rs @@ -1,11 +1,11 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --harness harness +// kani-flags: --harness harness -Z c-ffi // This test is to check Kani's error handling for missing functions. -// TODO: Verify that this prints a compiler warning: -// - https://github.com/model-checking/kani/issues/576 +// When the support to c-ffi is enabled, any reachable missing function definition will trigger a +// verification failure. extern "C" { fn missing_function() -> u32;