From 8c9ee5828a5a6bff18fe3ba8b9e72eb35de75e4d Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Wed, 23 Oct 2024 11:25:08 -0700 Subject: [PATCH] [Lean] Rename user-facing options from Aeneas to Lean (#3630) This is a follow-up on #3514. As @celinval suggested ([here](https://github.com/model-checking/kani/pull/3514#discussion_r1790949304)), 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. --- kani-compiler/Cargo.toml | 4 ++-- kani-compiler/src/args.rs | 10 +++++----- kani-compiler/src/kani_compiler.rs | 20 ++++++++++---------- kani-compiler/src/main.rs | 2 +- kani-driver/src/args/mod.rs | 15 +++++++-------- kani-driver/src/call_single_file.rs | 8 ++++---- kani_metadata/src/unstable.rs | 4 ++-- tests/expected/llbc/basic0/test.rs | 2 +- tests/expected/llbc/basic1/test.rs | 2 +- 9 files changed, 33 insertions(+), 34 deletions(-) diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 7b17e6073bb3..6cc98a6cace6 100644 --- a/kani-compiler/Cargo.toml +++ b/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 = [] diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index b5b799321cf3..eca9b3862b3d 100644 --- a/kani-compiler/src/args.rs +++ b/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, } diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index a6b6cf3a03af..d0f41ca0e2dc 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/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) -> ExitCode { } } -/// Configure the Aeneas backend that generates LLBC. -fn aeneas_backend(_queries: Arc>) -> Box { - #[cfg(feature = "aeneas")] +/// Configure the LLBC backend (Aeneas's IR). +fn llbc_backend(_queries: Arc>) -> Box { + #[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>) -> Box { unreachable!() } -#[cfg(any(feature = "aeneas", feature = "cprover"))] +#[cfg(any(feature = "cprover", feature = "llbc"))] fn backend(queries: Arc>) -> Box { 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>) -> Box { - 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. diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 1ba05d990955..52b9331fb29d 100644 --- a/kani-compiler/src/main.rs +++ b/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; diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 8aa758219524..b0811915aaf7 100644 --- a/kani-driver/src/args/mod.rs +++ b/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); diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index e33fbe874946..b04c283cb163 100644 --- a/kani-driver/src/call_single_file.rs +++ b/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 { - 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 } diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index 705732b6700e..ff2ca5c4830a 100644 --- a/kani_metadata/src/unstable.rs +++ b/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. diff --git a/tests/expected/llbc/basic0/test.rs b/tests/expected/llbc/basic0/test.rs index 5025994ab31c..410cf1848d44 100644 --- a/tests/expected/llbc/basic0/test.rs +++ b/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 diff --git a/tests/expected/llbc/basic1/test.rs b/tests/expected/llbc/basic1/test.rs index 92818fb93bfb..80f39e91ea9e 100644 --- a/tests/expected/llbc/basic1/test.rs +++ b/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