Remove support for the unstable argument --function (#3278)

This is a legacy argument that we have very limited support to. We kept
it around for bookrunner tests, which has been removed already.

Resolves #2129

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

@@ -95,7 +95,7 @@ impl<'tcx> GotocCtx<'tcx> {
             vec![]
         });
         self.attach_modifies_contract(instance_of_check, assigns_contract);
-        let wrapper_name = self.symbol_name_stable(instance_of_check);
+        let wrapper_name = instance_of_check.mangled_name();
 
         AssignsContract {
             recursion_tracker: full_recursion_tracker_name,

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

@@ -49,7 +49,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// handled later.
     pub fn codegen_foreign_fn(&mut self, instance: Instance) -> &Symbol {
         debug!(?instance, "codegen_foreign_function");
-        let fn_name = self.symbol_name_stable(instance).intern();
+        let fn_name = instance.mangled_name().intern();
         let loc = self.codegen_span_stable(instance.def.span());
         if self.symbol_table.contains(fn_name) {
             // Symbol has been added (either a built-in CBMC function or a Rust allocation function).
@@ -134,7 +134,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// Generate type for the given foreign instance.
     fn codegen_ffi_type(&mut self, instance: Instance) -> Type {
-        let fn_name = self.symbol_name_stable(instance);
+        let fn_name = instance.mangled_name();
         let fn_abi = instance.fn_abi().unwrap();
         let loc = self.codegen_span_stable(instance.def.span());
         let params = fn_abi
@@ -166,7 +166,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// This will behave like `codegen_unimplemented_stmt` but print a message that includes
     /// the name of the function not supported and the calling convention.
     fn codegen_ffi_unsupported(&mut self, instance: Instance, loc: Location) -> Stmt {
-        let fn_name = &self.symbol_name_stable(instance);
+        let fn_name = &instance.mangled_name();
         debug!(?fn_name, ?loc, "codegen_ffi_unsupported");
 
         // Save this occurrence so we can emit a warning in the compilation report.

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

@@ -52,7 +52,7 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn codegen_function(&mut self, instance: Instance) {
-        let name = self.symbol_name_stable(instance);
+        let name = instance.mangled_name();
         let old_sym = self.symbol_table.lookup(&name).unwrap();
 
         let _trace_span = debug_span!("CodegenFunction", name = instance.name()).entered();
@@ -204,7 +204,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let body = self.transformer.body(self.tcx, instance);
         self.set_current_fn(instance, &body);
         debug!(krate=?instance.def.krate(), is_std=self.current_fn().is_std(), "declare_function");
-        self.ensure(self.symbol_name_stable(instance), |ctx, fname| {
+        self.ensure(instance.mangled_name(), |ctx, fname| {
             Symbol::function(
                 fname,
                 ctx.fn_typ(instance, &body),

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

@@ -628,7 +628,7 @@ impl<'tcx> GotocCtx<'tcx> {
         } else {
             // All non-foreign functions should've been declared beforehand.
             trace!(func=?instance, "codegen_func_symbol");
-            let func = self.symbol_name_stable(instance);
+            let func = instance.mangled_name();
             self.symbol_table
                 .lookup(&func)
                 .unwrap_or_else(|| panic!("Function `{func}` should've been declared before usage"))

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

@@ -1299,7 +1299,7 @@ impl<'tcx> GotocCtx<'tcx> {
         debug!(?vtable_field_name, ?vtable_type, "codegen_vtable_method_field");
 
         // Lookup in the symbol table using the full symbol table name/key
-        let fn_name = self.symbol_name_stable(instance);
+        let fn_name = instance.mangled_name();
 
         if let Some(fn_symbol) = self.symbol_table.lookup(&fn_name) {
             if self.vtable_ctx.emit_vtable_restrictions {

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

@@ -44,7 +44,7 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn codegen_fndef_type_stable(&mut self, instance: Instance) -> Type {
-        let func = self.symbol_name_stable(instance);
+        let func = instance.mangled_name();
         self.ensure_struct(
             format!("{func}::FnDefStruct"),
             format!("{}::FnDefStruct", instance.name()),

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -133,7 +133,7 @@ impl GotocCodegenBackend {
                                 format!(
                                     "codegen_function: {}\n{}",
                                     instance.name(),
-                                    gcx.symbol_name_stable(instance)
+                                    instance.mangled_name()
                                 ),
                                 instance.def,
                             );

kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs

@@ -39,8 +39,7 @@ impl<'tcx> CurrentFnCtx<'tcx> {
     pub fn new(instance: Instance, gcx: &GotocCtx<'tcx>, body: &Body) -> Self {
         let instance_internal = rustc_internal::internal(gcx.tcx, instance);
         let readable_name = instance.name();
-        let name =
-            if &readable_name == "main" { readable_name.clone() } else { instance.mangled_name() };
+        let name = instance.mangled_name();
         let locals = body.locals().to_vec();
         let local_names = body
             .var_debug_info

kani-compiler/src/codegen_cprover_gotoc/utils/names.rs

@@ -8,7 +8,6 @@ use cbmc::InternedString;
 use rustc_hir::def_id::LOCAL_CRATE;
 use rustc_middle::mir::mono::CodegenUnitNameBuilder;
 use rustc_middle::ty::TyCtxt;
-use stable_mir::mir::mono::Instance;
 use stable_mir::mir::Local;
 
 impl<'tcx> GotocCtx<'tcx> {
@@ -50,15 +49,6 @@ impl<'tcx> GotocCtx<'tcx> {
         format!("{var_name}_init")
     }
 
-    /// Return the mangled name to be used in the symbol table.
-    ///
-    /// We special case main function in order to support `--function main`.
-    // TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129
-    pub fn symbol_name_stable(&self, instance: Instance) -> String {
-        let pretty = instance.name();
-        if pretty == "main" { pretty } else { instance.mangled_name() }
-    }
-
     /// The name for a tuple field
     pub fn tuple_fld_name(n: usize) -> String {
         format!("{n}")

kani-compiler/src/kani_middle/metadata.rs

@@ -13,19 +13,12 @@ use stable_mir::CrateDef;
 
 use super::{attributes::KaniAttributes, SourceLocation};
 
-pub fn canonical_mangled_name(instance: Instance) -> String {
-    let pretty_name = instance.name();
-    // Main function a special case in order to support `--function main`
-    // TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129
-    if pretty_name == "main" { pretty_name } else { instance.mangled_name() }
-}
-
 /// Create the harness metadata for a proof harness for a given function.
 pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> HarnessMetadata {
     let def = instance.def;
     let kani_attributes = KaniAttributes::for_instance(tcx, instance);
     let pretty_name = instance.name();
-    let mangled_name = canonical_mangled_name(instance);
+    let mangled_name = instance.mangled_name();
 
     // We get the body span to include the entire function definition.
     // This is required for concrete playback to properly position the generated test.

kani-driver/src/args/mod.rs

@@ -150,8 +150,7 @@ pub struct VerificationArgs {
 
     /// Generate C file equivalent to inputted program.
     /// This feature is unstable and it requires `--enable-unstable` to be used
-    #[arg(long, hide_short_help = true, requires("enable_unstable"),
-        conflicts_with_all(&["function"]))]
+    #[arg(long, hide_short_help = true, requires("enable_unstable"))]
     pub gen_c: bool,
 
     /// Directory for all generated artifacts.
@@ -169,19 +168,10 @@ pub struct VerificationArgs {
     #[command(flatten)]
     pub checks: CheckArgs,
 
-    /// Entry point for verification (symbol name).
-    /// This is an unstable feature. Consider using --harness instead
-    #[arg(long, hide = true, requires("enable_unstable"))]
-    pub function: Option<String>,
     /// If specified, only run harnesses that match this filter. This option can be provided
     /// multiple times, which will run all tests matching any of the filters.
     /// If used with --exact, the harness filter will only match the exact fully qualified name of a harness.
-    #[arg(
-        long = "harness",
-        conflicts_with = "function",
-        num_args(1),
-        value_name = "HARNESS_FILTER"
-    )]
+    #[arg(long = "harness", num_args(1), value_name = "HARNESS_FILTER")]
     pub harnesses: Vec<String>,
 
     /// When specified, the harness filter will only match the exact fully qualified name of a harness
@@ -569,7 +559,7 @@ impl ValidateArgs for VerificationArgs {
         if self.cbmc_args.contains(&OsString::from("--function")) {
             return Err(Error::raw(
                 ErrorKind::ArgumentConflict,
-                "Invalid flag: --function should be provided to Kani directly, not via --cbmc-args.",
+                "Invalid flag: --function is not supported in Kani.",
             ));
         }
         if self.common_args.quiet && self.concrete_playback == Some(ConcretePlaybackMode::Print) {

kani-driver/src/assess/mod.rs

@@ -56,14 +56,8 @@ fn assess_project(mut session: KaniSession) -> Result<AssessMetadata> {
     let project = project::cargo_project(&session, true)?;
     let cargo_metadata = project.cargo_metadata.as_ref().expect("built with cargo");
 
-    let packages_metadata = if project.merged_artifacts {
-        // With the legacy linker we can't expect to find the metadata structure we'd expect
-        // so we just use it as-is. This does mean the "package count" will be wrong, but
-        // we will at least continue to see everything.
-        project.metadata.clone()
-    } else {
-        reconstruct_metadata_structure(&session, cargo_metadata, &project.metadata)?
-    };
+    let packages_metadata =
+        reconstruct_metadata_structure(&session, cargo_metadata, &project.metadata)?;
 
     // We don't really have a list of crates that went into building our various targets,
     // so we can't easily count them.

kani-driver/src/call_cbmc.rs

@@ -402,7 +402,7 @@ pub fn resolve_unwind_value(
 #[cfg(test)]
 mod tests {
     use crate::args;
-    use crate::metadata::mock_proof_harness;
+    use crate::metadata::tests::mock_proof_harness;
     use clap::Parser;
 
     use super::*;

kani-driver/src/call_single_file.rs

@@ -70,14 +70,10 @@ impl KaniSession {
                 rustc_args.push(t);
             }
         } else {
-            // If we specifically request "--function main" then don't override crate type
-            if Some("main".to_string()) != self.args.function {
-                // We only run against proof harnesses normally, and this change
-                // 1. Means we do not require a `fn main` to exist
-                // 2. Don't forget it also changes visibility rules.
-                rustc_args.push("--crate-type".into());
-                rustc_args.push("lib".into());
-            }
+            // We only run against proof harnesses, so always compile as a library.
+            // This ensures compilation passes if the crate does not have a `main` function.
+            rustc_args.push("--crate-type".into());
+            rustc_args.push("lib".into());
         }
 
         // Note that the order of arguments is important. Kani specific flags should precede

kani-driver/src/harness_runner.rs

@@ -10,7 +10,6 @@ use crate::args::OutputFormat;
 use crate::call_cbmc::{VerificationResult, VerificationStatus};
 use crate::project::Project;
 use crate::session::KaniSession;
-use crate::util::error;
 
 /// A HarnessRunner is responsible for checking all proof harnesses. The data in this structure represents
 /// "background information" that the controlling driver (e.g. cargo-kani or kani) computed.
@@ -173,26 +172,22 @@ impl KaniSession {
                     "Complete - {succeeding} successfully verified harnesses, {failing} failures, {total} total."
                 );
             } else {
-                match (self.args.harnesses.as_slice(), &self.args.function) {
-                    ([], None) =>
+                match self.args.harnesses.as_slice() {
+                    [] =>
                     // TODO: This could use a better message, possibly with links to Kani documentation.
                     // New users may encounter this and could use a pointer to how to write proof harnesses.
                     {
                         println!(
                             "No proof harnesses (functions with #[kani::proof]) were found to verify."
                         )
                     }
-                    ([harness], None) => {
+                    [harness] => {
                         bail!("no harnesses matched the harness filter: `{harness}`")
                     }
-                    (harnesses, None) => bail!(
+                    harnesses => bail!(
                         "no harnesses matched the harness filters: `{}`",
                         harnesses.join("`, `")
                     ),
-                    ([], Some(func)) => error(&format!("No function named {func} was found")),
-                    _ => unreachable!(
-                        "invalid configuration. Cannot specify harness and function at the same time"
-                    ),
                 };
             }
         }

kani-driver/src/metadata.rs

@@ -2,12 +2,11 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use anyhow::{bail, Result};
-use std::path::{Path, PathBuf};
+use std::path::Path;
 use tracing::{debug, trace};
 
 use kani_metadata::{
-    HarnessAttributes, HarnessMetadata, InternedString, KaniMetadata, TraitDefinedMethod,
-    VtableCtxResults,
+    HarnessMetadata, InternedString, KaniMetadata, TraitDefinedMethod, VtableCtxResults,
 };
 use std::collections::{BTreeSet, HashMap};
 use std::fs::File;
@@ -115,12 +114,7 @@ impl KaniSession {
         &self,
         all_harnesses: &[&'a HarnessMetadata],
     ) -> Result<Vec<&'a HarnessMetadata>> {
-        let harnesses = if self.args.harnesses.is_empty() {
-            BTreeSet::from_iter(self.args.function.iter())
-        } else {
-            BTreeSet::from_iter(self.args.harnesses.iter())
-        };
-
+        let harnesses = BTreeSet::from_iter(self.args.harnesses.iter());
         let total_harnesses = harnesses.len();
         let all_targets = &harnesses;
 
@@ -169,25 +163,6 @@ pub fn sort_harnesses_by_loc<'a>(harnesses: &[&'a HarnessMetadata]) -> Vec<&'a H
     harnesses_clone
 }
 
-pub fn mock_proof_harness(
-    name: &str,
-    unwind_value: Option<u32>,
-    krate: Option<&str>,
-    model_file: Option<PathBuf>,
-) -> HarnessMetadata {
-    HarnessMetadata {
-        pretty_name: name.into(),
-        mangled_name: name.into(),
-        crate_name: krate.unwrap_or("<unknown>").into(),
-        original_file: "<unknown>".into(),
-        original_start_line: 0,
-        original_end_line: 0,
-        attributes: HarnessAttributes { unwind_value, proof: true, ..Default::default() },
-        goto_file: model_file,
-        contract: Default::default(),
-    }
-}
-
 /// Search for a proof harness with a particular name.
 /// At the present time, we use `no_mangle` so collisions shouldn't happen,
 /// but this function is written to be robust against that changing in the future.
@@ -223,8 +198,29 @@ fn find_proof_harnesses<'a>(
 }
 
 #[cfg(test)]
-mod tests {
+pub mod tests {
     use super::*;
+    use kani_metadata::HarnessAttributes;
+    use std::path::PathBuf;
+
+    pub fn mock_proof_harness(
+        name: &str,
+        unwind_value: Option<u32>,
+        krate: Option<&str>,
+        model_file: Option<PathBuf>,
+    ) -> HarnessMetadata {
+        HarnessMetadata {
+            pretty_name: name.into(),
+            mangled_name: name.into(),
+            crate_name: krate.unwrap_or("<unknown>").into(),
+            original_file: "<unknown>".into(),
+            original_start_line: 0,
+            original_end_line: 0,
+            attributes: HarnessAttributes { unwind_value, proof: true, ..Default::default() },
+            goto_file: model_file,
+            contract: Default::default(),
+        }
+    }
 
     #[test]
     fn check_find_proof_harness_without_exact() {