Add a new perf test

.github/workflows/kani.yml

@@ -303,6 +303,9 @@ jobs:
       - name: Build Kani (old variant)
         run: pushd old && cargo build-dev
 
+      - name: Copy benchmarks from new to old
+        run: rm -rf ./old/tests/perf ; cp -r ./new/tests/perf ./old/tests/
+
       - name: Run benchcomp
         run: |
           new/tools/benchcomp/bin/benchcomp \

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,
         ]
     }
 }

docs/src/cheat-sheets.md

@@ -81,6 +81,22 @@ kani --gen-c file.rs
 RUSTFLAGS="--emit mir" kani ${INPUT}.rs
 ```
 
+The `KANI_REACH_DEBUG` environment variable can be used to debug Kani's reachability analysis.
+If defined, Kani will generate a DOT graph `${INPUT}.dot` with the graph traversed during reachability analysis.
+If defined and not empty, the graph will be filtered to end at functions that contains the substring
+from `KANI_REACH_DEBUG`.
+
+Note that this will only work on debug builds.
+
+```bash
+# Generate a DOT graph ${INPUT}.dot with the graph traversed during reachability analysis
+KANI_REACH_DEBUG= kani ${INPUT}.rs
+
+# Generate a DOT graph ${INPUT}.dot with the sub-graph traversed during the reachability analysis
+# that connect to the given target.
+KANI_REACH_DEBUG="${TARGET_ITEM}" kani ${INPUT}.rs
+```
+
 ## CBMC
 
 ```bash

kani-compiler/kani_queries/src/lib.rs

@@ -9,8 +9,6 @@ use strum_macros::{AsRefStr, EnumString, EnumVariantNames};
 pub enum ReachabilityType {
     /// Start the cross-crate reachability analysis from all harnesses in the local crate.
     Harnesses,
-    /// Use standard rustc monomorphizer algorithm.
-    Legacy,
     /// Don't perform any reachability analysis. This will skip codegen for this crate.
     #[default]
     None,

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,
+        )
+    }
+}

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;

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)
     }
 

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

@@ -331,7 +331,6 @@ impl<'tcx> GotocCtx<'tcx> {
         };
         let overall_t = self.codegen_ty(ty);
         let direct_fields = overall_t.lookup_field("direct_fields", &self.symbol_table).unwrap();
-        let mut operands_iter = operands.iter();
         let direct_fields_expr = Expr::struct_expr_from_values(
             direct_fields.typ(),
             layout
@@ -342,13 +341,12 @@ impl<'tcx> GotocCtx<'tcx> {
                     if idx == *discriminant_field {
                         Expr::int_constant(0, self.codegen_ty(field_ty))
                     } else {
-                        self.codegen_operand(operands_iter.next().unwrap())
+                        self.codegen_operand(&operands[idx])
                     }
                 })
                 .collect(),
             &self.symbol_table,
         );
-        assert!(operands_iter.next().is_none());
         Expr::union_expr(overall_t, "direct_fields", direct_fields_expr, &self.symbol_table)
     }
 

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -30,7 +30,7 @@ use rustc_hir::def_id::LOCAL_CRATE;
 use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME};
 use rustc_metadata::EncodedMetadata;
 use rustc_middle::dep_graph::{WorkProduct, WorkProductId};
-use rustc_middle::mir::mono::{CodegenUnit, MonoItem};
+use rustc_middle::mir::mono::MonoItem;
 use rustc_middle::mir::write_mir_pretty;
 use rustc_middle::ty::query::Providers;
 use rustc_middle::ty::{self, InstanceDef, TyCtxt};
@@ -400,15 +400,6 @@ fn collect_codegen_items<'tcx>(gcx: &GotocCtx<'tcx>) -> Vec<MonoItem<'tcx>> {
     let reach = gcx.queries.get_reachability_analysis();
     debug!(?reach, "collect_codegen_items");
     match reach {
-        ReachabilityType::Legacy => {
-            // Use rustc monomorphizer to retrieve items to codegen.
-            let codegen_units: &'tcx [CodegenUnit<'_>] = tcx.collect_and_partition_mono_items(()).1;
-            codegen_units
-                .iter()
-                .flat_map(|cgu| cgu.items_in_deterministic_order(tcx))
-                .map(|(item, _)| item)
-                .collect()
-        }
         ReachabilityType::Harnesses => {
             // Cross-crate collecting of all items that are reachable from the crate harnesses.
             let harnesses = filter_crate_items(tcx, |_, def_id| is_proof_harness(gcx.tcx, def_id));