[Lean] Rename user-facing options from Aeneas to Lean (#3630)

This is a follow-up on #3514. As @celinval suggested
([here](#3514 (comment))),
renaming all user-facing options from "Aeneas" to Lean.

Inside the Kani compiler which is only concerned with producing LLBC
(and doesn't know about Lean/Aeneas), I'm renaming the relevant feature
from `aeneas` to `llbc`, and the backend is now called the LLBC backend
as opposed to the Aeneas backend.

Towards #3585 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: zhassan-aws

kani-compiler/Cargo.toml

@@ -31,8 +31,8 @@ tracing-tree = "0.4.0"
 
 # Future proofing: enable backend dependencies using feature.
 [features]
-default = ['aeneas', 'cprover']
-aeneas = ['charon']
+default = ['cprover', 'llbc']
+llbc = ['charon']
 cprover = ['cbmc', 'num', 'serde']
 write_json_symtab = []
 

kani-compiler/src/args.rs

@@ -7,15 +7,15 @@ use tracing_subscriber::filter::Directive;
 #[derive(Debug, Default, Display, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)]
 #[strum(serialize_all = "snake_case")]
 pub enum BackendOption {
-    /// Aeneas (LLBC) backend
-    #[cfg(feature = "aeneas")]
-    Aeneas,
-
     /// CProver (Goto) backend
     #[cfg(feature = "cprover")]
     #[strum(serialize = "cprover")]
     #[default]
     CProver,
+
+    /// LLBC backend (Aeneas's IR)
+    #[cfg(feature = "llbc")]
+    Llbc,
 }
 
 #[derive(Debug, Default, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)]
@@ -87,7 +87,7 @@ pub struct Arguments {
     /// Option name used to select which backend to use.
     #[clap(long = "backend", default_value_t = BackendOption::CProver)]
     pub backend: BackendOption,
-    /// Print the final LLBC file to stdout. This requires `-Zaeneas`.
+    /// Print the final LLBC file to stdout.
     #[clap(long)]
     pub print_llbc: bool,
 }

kani-compiler/src/kani_compiler.rs

@@ -16,7 +16,7 @@
 //! `-C llvm-args`.
 
 use crate::args::{Arguments, BackendOption};
-#[cfg(feature = "aeneas")]
+#[cfg(feature = "llbc")]
 use crate::codegen_aeneas_llbc::LlbcCodegenBackend;
 #[cfg(feature = "cprover")]
 use crate::codegen_cprover_gotoc::GotocCodegenBackend;
@@ -44,11 +44,11 @@ pub fn run(args: Vec<String>) -> ExitCode {
     }
 }
 
-/// Configure the Aeneas backend that generates LLBC.
-fn aeneas_backend(_queries: Arc<Mutex<QueryDb>>) -> Box<dyn CodegenBackend> {
-    #[cfg(feature = "aeneas")]
+/// Configure the LLBC backend (Aeneas's IR).
+fn llbc_backend(_queries: Arc<Mutex<QueryDb>>) -> Box<dyn CodegenBackend> {
+    #[cfg(feature = "llbc")]
     return Box::new(LlbcCodegenBackend::new(_queries));
-    #[cfg(not(feature = "aeneas"))]
+    #[cfg(not(feature = "llbc"))]
     unreachable!()
 }
 
@@ -60,21 +60,21 @@ fn cprover_backend(_queries: Arc<Mutex<QueryDb>>) -> Box<dyn CodegenBackend> {
     unreachable!()
 }
 
-#[cfg(any(feature = "aeneas", feature = "cprover"))]
+#[cfg(any(feature = "cprover", feature = "llbc"))]
 fn backend(queries: Arc<Mutex<QueryDb>>) -> Box<dyn CodegenBackend> {
     let backend = queries.lock().unwrap().args().backend;
     match backend {
-        #[cfg(feature = "aeneas")]
-        BackendOption::Aeneas => aeneas_backend(queries),
         #[cfg(feature = "cprover")]
         BackendOption::CProver => cprover_backend(queries),
+        #[cfg(feature = "llbc")]
+        BackendOption::Llbc => llbc_backend(queries),
     }
 }
 
 /// Fallback backend. It will trigger an error if no backend has been enabled.
-#[cfg(not(any(feature = "aeneas", feature = "cprover")))]
+#[cfg(not(any(feature = "cprover", feature = "llbc")))]
 fn backend(queries: Arc<Mutex<QueryDb>>) -> Box<CodegenBackend> {
-    compile_error!("No backend is available. Use `aeneas` or `cprover`.");
+    compile_error!("No backend is available. Use `cprover` or `llbc`.");
 }
 
 /// This object controls the compiler behavior.

kani-compiler/src/main.rs

@@ -38,7 +38,7 @@ extern crate stable_mir;
 extern crate tempfile;
 
 mod args;
-#[cfg(feature = "aeneas")]
+#[cfg(feature = "llbc")]
 mod codegen_aeneas_llbc;
 #[cfg(feature = "cprover")]
 mod codegen_cprover_gotoc;

kani-driver/src/args/mod.rs

@@ -277,7 +277,7 @@ pub struct VerificationArgs {
     #[arg(long, hide_short_help = true)]
     pub coverage: bool,
 
-    /// Print final LLBC for Aeneas backend. This requires the `-Z aeneas` option.
+    /// Print final LLBC for Lean backend. This requires the `-Z lean` option.
     #[arg(long, hide = true)]
     pub print_llbc: bool,
 
@@ -621,21 +621,20 @@ impl ValidateArgs for VerificationArgs {
             ));
         }
 
-        if self.print_llbc && !self.common_args.unstable_features.contains(UnstableFeature::Aeneas)
-        {
+        if self.print_llbc && !self.common_args.unstable_features.contains(UnstableFeature::Lean) {
             return Err(Error::raw(
                 ErrorKind::MissingRequiredArgument,
-                "The `--print-llbc` argument is unstable and requires `-Z aeneas` to be used.",
+                "The `--print-llbc` argument is unstable and requires `-Z lean` to be used.",
             ));
         }
 
         // TODO: error out for other CBMC-backend-specific arguments
-        if self.common_args.unstable_features.contains(UnstableFeature::Aeneas)
+        if self.common_args.unstable_features.contains(UnstableFeature::Lean)
             && !self.cbmc_args.is_empty()
         {
             return Err(Error::raw(
                 ErrorKind::ArgumentConflict,
-                "The `--cbmc-args` argument cannot be used with -Z aeneas.",
+                "The `--cbmc-args` argument cannot be used with -Z lean.",
             ));
         }
         Ok(())
@@ -930,8 +929,8 @@ mod tests {
     }
 
     #[test]
-    fn check_cbmc_args_aeneas_backend() {
-        let args = "kani input.rs -Z aeneas --enable-unstable --cbmc-args --object-bits 10"
+    fn check_cbmc_args_lean_backend() {
+        let args = "kani input.rs -Z lean --enable-unstable --cbmc-args --object-bits 10"
             .split_whitespace();
         let err = StandaloneArgs::try_parse_from(args).unwrap().validate().unwrap_err();
         assert_eq!(err.kind(), ErrorKind::ArgumentConflict);

kani-driver/src/call_single_file.rs

@@ -53,8 +53,8 @@ impl KaniSession {
     ) -> Result<()> {
         let mut kani_args = self.kani_compiler_flags();
         kani_args.push(format!("--reachability={}", self.reachability_mode()));
-        if self.args.common_args.unstable_features.contains(UnstableFeature::Aeneas) {
-            kani_args.push("--backend=aeneas".into());
+        if self.args.common_args.unstable_features.contains(UnstableFeature::Lean) {
+            kani_args.push("--backend=llbc".into());
         }
 
         let lib_path = lib_folder().unwrap();
@@ -99,8 +99,8 @@ impl KaniSession {
     }
 
     pub fn backend_arg(&self) -> Option<String> {
-        if self.args.common_args.unstable_features.contains(UnstableFeature::Aeneas) {
-            Some(to_rustc_arg(vec!["--backend=aeneas".into()]))
+        if self.args.common_args.unstable_features.contains(UnstableFeature::Lean) {
+            Some(to_rustc_arg(vec!["--backend=llbc".into()]))
         } else {
             None
         }

kani_metadata/src/unstable.rs

@@ -90,8 +90,8 @@ pub enum UnstableFeature {
     /// Automatically check that no invalid value is produced which is considered UB in Rust.
     /// Note that this does not include checking uninitialized value.
     ValidValueChecks,
-    /// Aeneas/LLBC
-    Aeneas,
+    /// Enabled Lean backend (Aeneas/LLBC)
+    Lean,
     /// Ghost state and shadow memory APIs.
     GhostState,
     /// Automatically check that uninitialized memory is not used.

tests/expected/llbc/basic0/test.rs

@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zaeneas --print-llbc
+// kani-flags: -Zlean --print-llbc
 
 //! This test checks that Kani's LLBC backend handles basic expressions, in this
 //! case an equality between a variable and a constant

tests/expected/llbc/basic1/test.rs

@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Zaeneas --print-llbc
+// kani-flags: -Zlean --print-llbc
 
 //! This test checks that Kani's LLBC backend handles basic expressions, in this
 //! case an if condition