|
| 1 | +// Copyright Kani Contributors |
| 2 | +// SPDX-License-Identifier: Apache-2.0 OR MIT |
| 3 | +//! This module implements foreign function handling. |
| 4 | +//! |
| 5 | +//! Kani currently only support CBMC built-in functions that are declared in the `cprover_bindings` |
| 6 | +//! crate, and allocation functions defined in `kani_lib.c`. |
| 7 | +//! |
| 8 | +//! All other functions will be replaced by an unimplemented check, due to current issues with |
| 9 | +//! linking and usability unless unstable C-FFI support is enabled. |
| 10 | +use std::collections::HashSet; |
| 11 | + |
| 12 | +use crate::codegen_cprover_gotoc::codegen::PropertyClass; |
| 13 | +use crate::codegen_cprover_gotoc::GotocCtx; |
| 14 | +use crate::kani_middle; |
| 15 | +use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type}; |
| 16 | +use cbmc::{InternString, InternedString}; |
| 17 | +use kani_queries::UserInput; |
| 18 | +use lazy_static::lazy_static; |
| 19 | +use rustc_middle::ty::Instance; |
| 20 | +use rustc_target::abi::call::Conv; |
| 21 | +use tracing::{debug, trace}; |
| 22 | + |
| 23 | +lazy_static! { |
| 24 | + /// The list of Rust allocation functions that are declared in the `core::alloc` module |
| 25 | + /// but defined by each backend. |
| 26 | + /// For our `goto-program` backend, these functions are defined inside `kani_lib.c`. |
| 27 | + /// For now, we blindly trust that the definitions in `kani_lib.c` are kept in sync with the |
| 28 | + /// declarations from the standard library, provided here: |
| 29 | + /// <https://stdrs.dev/nightly/x86_64-unknown-linux-gnu/alloc/alloc/index.html> |
| 30 | + static ref RUST_ALLOC_FNS: HashSet<InternedString> = { |
| 31 | + HashSet::from([ |
| 32 | + "__rust_alloc".into(), |
| 33 | + "__rust_alloc_zeroed".into(), |
| 34 | + "__rust_dealloc".into(), |
| 35 | + "__rust_realloc".into(), |
| 36 | + ]) |
| 37 | + }; |
| 38 | +} |
| 39 | + |
| 40 | +impl<'tcx> GotocCtx<'tcx> { |
| 41 | + /// Generate the symbol and symbol table entry for foreign items. |
| 42 | + /// |
| 43 | + /// CBMC built-in functions that are supported by Kani are always added to the symbol table, and |
| 44 | + /// this function will return them. |
| 45 | + /// |
| 46 | + /// For other foreign items, we declare a shim and add to the list of foreign shims to be |
| 47 | + /// handled later. |
| 48 | + pub fn codegen_foreign_fn(&mut self, instance: Instance<'tcx>) -> &Symbol { |
| 49 | + debug!(?instance, "codegen_foreign_function"); |
| 50 | + let fn_name = self.symbol_name(instance).intern(); |
| 51 | + if self.symbol_table.contains(fn_name) { |
| 52 | + // Symbol has been added (either a built-in CBMC function or a Rust allocation function). |
| 53 | + self.symbol_table.lookup(fn_name).unwrap() |
| 54 | + } else if RUST_ALLOC_FNS.contains(&fn_name) |
| 55 | + || (self.is_cffi_enabled() && kani_middle::fn_abi(self.tcx, instance).conv == Conv::C) |
| 56 | + { |
| 57 | + // Add a Rust alloc lib function as is declared by core. |
| 58 | + // When C-FFI feature is enabled, we just trust the rust declaration. |
| 59 | + // TODO: Add proper casting and clashing definitions check. |
| 60 | + // https://github.com/model-checking/kani/issues/1350 |
| 61 | + // https://github.com/model-checking/kani/issues/2426 |
| 62 | + self.ensure(fn_name, |gcx, _| { |
| 63 | + let typ = gcx.codegen_ffi_type(instance); |
| 64 | + Symbol::function( |
| 65 | + fn_name, |
| 66 | + typ, |
| 67 | + None, |
| 68 | + gcx.readable_instance_name(instance), |
| 69 | + Location::none(), |
| 70 | + ) |
| 71 | + .with_is_extern(true) |
| 72 | + }) |
| 73 | + } else { |
| 74 | + let shim_name = format!("{fn_name}_ffi_shim"); |
| 75 | + trace!(?shim_name, "codegen_foreign_function"); |
| 76 | + self.ensure(&shim_name, |gcx, _| { |
| 77 | + // Generate a shim with an unsupported C-FFI error message. |
| 78 | + let typ = gcx.codegen_ffi_type(instance); |
| 79 | + Symbol::function( |
| 80 | + &shim_name, |
| 81 | + typ, |
| 82 | + Some(gcx.codegen_ffi_shim(shim_name.as_str().into(), instance)), |
| 83 | + gcx.readable_instance_name(instance), |
| 84 | + Location::none(), |
| 85 | + ) |
| 86 | + }) |
| 87 | + } |
| 88 | + } |
| 89 | + |
| 90 | + /// Checks whether C-FFI has been enabled or not. |
| 91 | + /// When enabled, we blindly encode the function type as is. |
| 92 | + fn is_cffi_enabled(&self) -> bool { |
| 93 | + self.queries.get_unstable_features().contains(&"c-ffi".to_string()) |
| 94 | + } |
| 95 | + |
| 96 | + /// Generate code for a foreign function shim. |
| 97 | + fn codegen_ffi_shim(&mut self, shim_name: InternedString, instance: Instance<'tcx>) -> Stmt { |
| 98 | + debug!(?shim_name, ?instance, sym=?self.symbol_table.lookup(shim_name), "generate_foreign_shim"); |
| 99 | + |
| 100 | + let loc = self.codegen_span(&self.tcx.def_span(instance.def_id())); |
| 101 | + let unsupported_check = self.codegen_ffi_unsupported(instance, loc); |
| 102 | + Stmt::block(vec![unsupported_check], loc) |
| 103 | + } |
| 104 | + |
| 105 | + /// Generate type for the given foreign instance. |
| 106 | + fn codegen_ffi_type(&mut self, instance: Instance<'tcx>) -> Type { |
| 107 | + let fn_name = self.symbol_name(instance); |
| 108 | + let fn_abi = kani_middle::fn_abi(self.tcx, instance); |
| 109 | + let loc = self.codegen_span(&self.tcx.def_span(instance.def_id())); |
| 110 | + let params = fn_abi |
| 111 | + .args |
| 112 | + .iter() |
| 113 | + .enumerate() |
| 114 | + .filter_map(|(idx, arg)| { |
| 115 | + (!arg.is_ignore()).then(|| { |
| 116 | + let arg_name = format!("{fn_name}::param_{idx}"); |
| 117 | + let base_name = format!("param_{idx}"); |
| 118 | + let arg_type = self.codegen_ty(arg.layout.ty); |
| 119 | + let sym = Symbol::variable(&arg_name, &base_name, arg_type.clone(), loc) |
| 120 | + .with_is_parameter(true); |
| 121 | + self.symbol_table.insert(sym); |
| 122 | + arg_type.as_parameter(Some(arg_name.into()), Some(base_name.into())) |
| 123 | + }) |
| 124 | + }) |
| 125 | + .collect(); |
| 126 | + let ret_type = self.codegen_ty(fn_abi.ret.layout.ty); |
| 127 | + |
| 128 | + if fn_abi.c_variadic { |
| 129 | + Type::variadic_code(params, ret_type) |
| 130 | + } else { |
| 131 | + Type::code(params, ret_type) |
| 132 | + } |
| 133 | + } |
| 134 | + |
| 135 | + /// Kani does not currently support FFI functions except for built-in CBMC functions. |
| 136 | + /// |
| 137 | + /// This will behave like `codegen_unimplemented_stmt` but print a message that includes |
| 138 | + /// the name of the function not supported and the calling convention. |
| 139 | + pub fn codegen_ffi_unsupported(&mut self, instance: Instance<'tcx>, loc: Location) -> Stmt { |
| 140 | + let fn_name = &self.symbol_name(instance); |
| 141 | + debug!(?fn_name, ?loc, "codegen_ffi_unsupported"); |
| 142 | + |
| 143 | + // Save this occurrence so we can emit a warning in the compilation report. |
| 144 | + let entry = self.unsupported_constructs.entry("foreign function".into()).or_default(); |
| 145 | + entry.push(loc); |
| 146 | + |
| 147 | + let call_conv = kani_middle::fn_abi(self.tcx, instance).conv; |
| 148 | + let msg = format!("call to foreign \"{call_conv:?}\" function `{fn_name}`"); |
| 149 | + let url = if call_conv == Conv::C { |
| 150 | + "https://github.com/model-checking/kani/issues/2423" |
| 151 | + } else { |
| 152 | + "https://github.com/model-checking/kani/issues/new/choose" |
| 153 | + }; |
| 154 | + self.codegen_assert_assume( |
| 155 | + Expr::bool_false(), |
| 156 | + PropertyClass::UnsupportedConstruct, |
| 157 | + &GotocCtx::unsupported_msg(&msg, Some(url)), |
| 158 | + loc, |
| 159 | + ) |
| 160 | + } |
| 161 | +} |
0 commit comments