model-checking · celinval · Jan 17, 2023 · Jan 17, 2023 · Jan 17, 2023 · Jan 17, 2023
@@ -3,6 +3,7 @@
 
 #[cfg(feature = "unsound_experiments")]
 use crate::unsound_experiments::UnsoundExperimentArgs;
+use crate::util::warning;
 
 use clap::{error::Error, error::ErrorKind, CommandFactory, ValueEnum};
 use std::ffi::OsString;
@@ -98,7 +99,7 @@ pub struct KaniArgs {
     /// 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", "legacy_linker"]))]
+        conflicts_with_all(&["function"]))]
     pub gen_c: bool,
 
     /// Directory for all generated artifacts.
@@ -135,17 +136,12 @@ pub struct KaniArgs {
     #[arg(long, hide_short_help = true)]
     pub only_codegen: bool,
 
-    /// Disable the new MIR Linker. Using this option may result in missing symbols from the
-    /// `std` library. See <https://github.com/model-checking/kani/issues/1213> for more details.
-    #[arg(long, hide = true)]
+    /// Deprecated flag. This is a no-op since we no longer support the legacy linker and
+    /// it will be removed in a future Kani release.
+    #[arg(long, hide = true, conflicts_with("mir_linker"))]
     pub legacy_linker: bool,
-
-    /// Enable the new MIR Linker. This is already the default option and it will be removed once
-    /// the linker is stable.
-    /// The MIR Linker affects how Kani prunes the code to be analyzed. It also fixes previous
-    /// issues with missing `std` function definitions.
-    /// See <https://model-checking.github.io/kani/rfc/rfcs/0001-mir-linker.html> for more details.
-    #[arg(long, conflicts_with("legacy_linker"), hide = true)]
+    /// Deprecated flag. This is a no-op since we no longer support any other linker.
+    #[arg(long, hide = true)]
     pub mir_linker: bool,
 
     /// Specify the value used for loop unwinding in CBMC
@@ -472,6 +468,14 @@ impl KaniArgs {
             );
         }
 
+        if self.mir_linker {
+            self.print_deprecated("--mir-linker");
+        }
+
+        if self.legacy_linker {
+            self.print_deprecated("--legacy-linker");
+        }
+
         // TODO: these conflicting flags reflect what's necessary to pass current tests unmodified.
         // We should consider improving the error messages slightly in a later pull request.
         if natives_unwind && extra_unwind {
@@ -535,6 +539,14 @@ impl KaniArgs {
 
         Ok(())
     }
+
+    fn print_deprecated(&self, option: &str) {
+        if !self.quiet {
+            warning(&format!(
+                "The `{option}` option is deprecated. This option no longer has any effect and should be removed"
+            ))
+        }
+    }
 }
 
 #[cfg(test)]

@@ -95,10 +95,6 @@ impl KaniSession {
         // Arguments that will only be passed to the target package.
         let mut pkg_args: Vec<OsString> = vec![];
         match self.reachability_mode() {
-            ReachabilityMode::Legacy => {
-                // For this mode, we change `kani_args` not `pkg_args`
-                kani_args.push("--reachability=legacy".into());
-            }
             ReachabilityMode::ProofHarnesses => {
                 pkg_args.extend(["--".into(), "--reachability=harnesses".into()]);
             }

@@ -20,7 +20,6 @@ impl KaniSession {
         let mut kani_args = self.kani_specific_flags();
         kani_args.push(
             match self.reachability_mode() {
-                ReachabilityMode::Legacy => "--reachability=legacy",
                 ReachabilityMode::ProofHarnesses => "--reachability=harnesses",
                 ReachabilityMode::AllPubFns => "--reachability=pub_fns",
                 ReachabilityMode::Tests => "--reachability=tests",

@@ -4,16 +4,13 @@
 //! The goal is to provide one project view independent on the build system (cargo / standalone
 //! rustc) and its configuration (e.g.: linker type).
 //!
-//! For `--legacy-linker` and `--function`, we still have a hack in-place that merges all the
-//! artifacts together. The reason is the following:
-//!  - For `--legacy-linker`, the compiler generate one goto file per crate, including each
-//!    target and all their dependencies. Ideally, the linking be done on a per-target base, but
-//!    this would require extra logic. Since we are planning to remove the `--legacy-linker` in
-//!    the near future, we decided not to invest time there.
+//! For `--function`, we still have a hack in-place that merges all the artifacts together.
+//! The reason is the following:
 //!  - For `--function`, the compiler doesn't generate any metadata that indicates which
 //!    functions each goto model includes. Thus, we don't have an easy way to tell which goto
 //!    files are relevant for the function verification. This is also another flag that we don't
-//!    expect to stabilize, so we also opted to use the same hack of merging everything together.
+//!    expect to stabilize, so we also opted to use the same hack as implemented before the MIR
+//!    Linker was introduced to merge everything together.
 //!
 //! Note that for `--function` we also inject a mock `HarnessMetadata` to the project. This
 //! allows the rest of the driver to handle a function under verification the same way it handle
@@ -53,8 +50,8 @@ pub struct Project {
     artifacts: Vec<Artifact>,
     /// A flag that indicated whether all artifacts have been merged or not.
     ///
-    /// This allow us to provide a consistent behavior for `--legacy-linker` and `--function`.
-    /// For these two options, we still merge all the artifacts together, so the
+    /// This allow us to provide a consistent behavior for `--function`.
+    /// For these this option, we still merge all the artifacts together, so the
     /// `merged_artifacts` flag will be set to `true`.
     /// When this flag is `true`, there should only be up to one artifact of any given type.
     /// When this flag is `false`, there may be multiple artifacts for any given type. However,
@@ -152,8 +149,8 @@ pub fn cargo_project(session: &KaniSession) -> Result<Project> {
     let outputs = session.cargo_build()?;
     let mut artifacts = vec![];
     let outdir = outputs.outdir.canonicalize()?;
-    if session.args.legacy_linker || session.args.function.is_some() {
-        // For the legacy linker or `--function` support, we still use a glob to link everything.
+    if session.args.function.is_some() {
+        // For the `--function` support, we still use a glob to link everything.
         // Yes, this is broken, but it has been broken for quite some time. :(
         // Merge goto files.
         let joined_name = "cbmc-linked";

@@ -74,9 +74,7 @@ impl KaniSession {
     /// Determine which symbols Kani should codegen (i.e. by slicing away symbols
     /// that are considered unreachable.)
     pub fn reachability_mode(&self) -> ReachabilityMode {
-        if self.args.legacy_linker {
-            ReachabilityMode::Legacy
-        } else if self.codegen_tests {
+        if self.codegen_tests {
             ReachabilityMode::Tests
         } else if self.args.function.is_some() {
             ReachabilityMode::AllPubFns
@@ -87,7 +85,6 @@ impl KaniSession {
 }
 
 pub enum ReachabilityMode {
-    Legacy,
     ProofHarnesses,
     AllPubFns,
     Tests,

@@ -88,6 +88,13 @@ pub fn specialized_harness_name(linked_obj: &Path, harness_filename: &str) -> Pa
     alter_extension(linked_obj, &format!("for-{harness_filename}.out"))
 }
 
+/// Print a warning message. This will add a "warning:" tag before the message and style accordinly.
+pub fn warning(msg: &str) {
+    let warning = console::style("warning:").bold().yellow();
+    let msg_fmt = console::style(msg).bold();
+    println!("{warning} {msg_fmt}")
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;

@@ -23,12 +23,11 @@ echo
 
 # At the moment, we only test codegen for the virtio module
 cd $KANI_DIR/firecracker/src/devices/src/virtio/
-# Disable warnings until https://github.com/model-checking/kani/issues/573 is fixed
+export KANI_LOG=error
 export RUSTC_LOG=error
 export RUST_BACKTRACE=1
-# Use the legacy linker for now since we want to maximize the code that we are compiling from firecracker.
-# The MIR Linker will by default only collect code relevant to proof harnesses, however, firecracker has none.
-cargo kani --only-codegen --legacy-linker
+# Use cargo assess since this is now our default way of assessing Kani suitability to verify a crate.
+cargo kani --enable-unstable --only-codegen assess
 
 echo
 echo "Finished Firecracker codegen regression successfully..."