Plumbing for Boogie backend (#2506)

kani-compiler/Cargo.toml

@@ -29,7 +29,8 @@ tracing-tree = "0.2.2"
 
 # Future proofing: enable backend dependencies using feature.
 [features]
-default = ['cprover']
+default = ['boogie', 'cprover']
+boogie = ['serde']
 cprover = ['cbmc', 'num', 'serde']
 write_json_symtab = []
 

kani-compiler/src/codegen_boogie/context/boogie_ctx.rs

@@ -0,0 +1,26 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use crate::kani_queries::QueryDb;
+use rustc_middle::ty::{Instance, TyCtxt};
+use tracing::debug;
+
+/// A context that provides the main methods for translating MIR constructs to
+/// Boogie and stores what has been codegen so far
+pub struct BoogieCtx<'tcx> {
+ /// the typing context
+ pub tcx: TyCtxt<'tcx>,
+ /// a snapshot of the query values. The queries shouldn't change at this point,
+ /// so we just keep a copy.
+ pub queries: QueryDb,
+}
+
+impl<'tcx> BoogieCtx<'tcx> {
+ pub fn new(tcx: TyCtxt<'tcx>, queries: QueryDb) -> BoogieCtx<'tcx> {
+ BoogieCtx { tcx, queries }
+ }
+
+ pub fn declare_function(&mut self, instance: Instance) {
+ debug!(?instance, "boogie_codegen_declare_function");
+ }
+}

kani-compiler/src/codegen_boogie/context/mod.rs

@@ -0,0 +1,9 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module hosts the context used by Kani to convert MIR into Boogie. See
+//! the file level comments for more details.
+
+mod boogie_ctx;
+
+pub use boogie_ctx::BoogieCtx;

kani-compiler/src/codegen_boogie/mod.rs

@@ -0,0 +1,9 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+mod compiler_interface;
+mod context;
+//mod utils;
+
+pub use compiler_interface::BoogieCodegenBackend;
+pub use context::BoogieCtx;

kani-compiler/src/kani_compiler.rs

@@ -15,14 +15,16 @@
 //! in order to apply the stubs. For the subsequent runs, we add the stub configuration to
 //! `-C llvm-args`.
 
+#[cfg(feature = "boogie")]
+use crate::codegen_boogie::BoogieCodegenBackend;
 #[cfg(feature = "cprover")]
 use crate::codegen_cprover_gotoc::GotocCodegenBackend;
 use crate::kani_middle::attributes::is_proof_harness;
 use crate::kani_middle::check_crate_items;
 use crate::kani_middle::metadata::gen_proof_metadata;
 use crate::kani_middle::reachability::filter_crate_items;
 use crate::kani_middle::stubbing::{self, harness_stub_map};
-use crate::kani_queries::{QueryDb, ReachabilityType};
+use crate::kani_queries::{BackendOption, QueryDb, ReachabilityType};
 use crate::parser::{self, KaniCompilerParser};
 use crate::session::init_session;
 use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata};
@@ -52,16 +54,53 @@ pub fn run(args: Vec<String>) -> ExitCode {
  }
 }
 
-/// Configure the cprover backend that generate goto-programs.
-#[cfg(feature = "cprover")]
+/// Configure the boogie backend that generates boogie programs.
+fn boogie_backend(_queries: Arc<Mutex<QueryDb>>) -> Box<dyn CodegenBackend> {
+ #[cfg(feature = "boogie")]
+ return Box::new(BoogieCodegenBackend::new(_queries));
+ #[cfg(not(feature = "boogie"))]
+ rustc_session::early_error(
+ ErrorOutputType::default(),
+ "`--backend boogie` requires enabling the `boogie` feature",
+ );
+}
+
+/// Configure the cprover backend that generates goto-programs.
+fn cprover_backend(_queries: Arc<Mutex<QueryDb>>) -> Box<dyn CodegenBackend> {
+ #[cfg(feature = "cprover")]
+ return Box::new(GotocCodegenBackend::new(_queries));
+ #[cfg(not(feature = "cprover"))]
+ rustc_session::early_error(
+ ErrorOutputType::default(),
+ "`--backend cprover` requires enabling the `cprover` feature",
+ );
+}
+
+#[cfg(any(feature = "cprover", feature = "boogie"))]
 fn backend(queries: Arc<Mutex<QueryDb>>) -> Box<dyn CodegenBackend> {
- Box::new(GotocCodegenBackend::new(queries))
+ let backend = queries.lock().unwrap().backend;
+ match backend {
+ BackendOption::None => {
+ // priority list of backends
+ if cfg!(feature = "cprover") {
+ return cprover_backend(queries);
+ } else if cfg!(feature = "boogie") {
+ return boogie_backend(queries);
+ } else {
+ unreachable!();
+ }
+ }
+ BackendOption::CProver => cprover_backend(queries),
+ BackendOption::Boogie => boogie_backend(queries),
+ }
 }
 
 /// Fallback backend. It will trigger an error if no backend has been enabled.
-#[cfg(not(feature = "cprover"))]
+#[cfg(not(any(feature = "cprover", feature = "boogie")))]
 fn backend(queries: Arc<Mutex<QueryDb>>) -> Box<CodegenBackend> {
- compile_error!("No backend is available. Only supported value today is `cprover`");
+ compile_error!(
+ "No backend is available. Only supported values today are `cprover` and `boogie`"
+ );
 }
 
 /// A stable (across compilation sessions) identifier for the harness function.
@@ -353,6 +392,7 @@ impl Callbacks for KaniCompiler {
  queries.write_json_symtab =
  cfg!(feature = "write_json_symtab") || matches.get_flag(parser::WRITE_JSON_SYMTAB);
  queries.reachability_analysis = matches.reachability_type();
+ queries.backend = matches.backend();
 
  if let Some(features) = matches.get_many::<String>(parser::UNSTABLE_FEATURE) {
  queries.unstable_features = features.cloned().collect::<Vec<_>>();

kani-compiler/src/kani_queries/mod.rs

@@ -10,6 +10,20 @@ use std::{
 };
 use strum_macros::{AsRefStr, EnumString, EnumVariantNames};
 
+#[derive(Debug, Default, Clone, Copy, AsRefStr, EnumString, EnumVariantNames, PartialEq, Eq)]
+#[strum(serialize_all = "snake_case")]
+pub enum BackendOption {
+ /// Boogie backend
+ Boogie,
+
+ /// CProver (Goto) backend
+ CProver,
+
+ /// Backend option was not explicitly set
+ #[default]
+ None,
+}
+
 #[derive(Debug, Default, Clone, Copy, AsRefStr, EnumString, EnumVariantNames, PartialEq, Eq)]
 #[strum(serialize_all = "snake_case")]
 pub enum ReachabilityType {
@@ -27,6 +41,7 @@ pub enum ReachabilityType {
 /// This structure should only be used behind a synchronized reference or a snapshot.
 #[derive(Debug, Default, Clone)]
 pub struct QueryDb {
+ pub backend: BackendOption,
  pub check_assertion_reachability: bool,
  pub emit_vtable_restrictions: bool,
  pub output_pretty_json: bool,

kani-compiler/src/main.rs

@@ -32,6 +32,8 @@ extern crate rustc_target;
 // We can't add this directly as a dependency because we need the version to match rustc
 extern crate tempfile;
 
+#[cfg(feature = "boogie")]
+mod codegen_boogie;
 #[cfg(feature = "cprover")]
 mod codegen_cprover_gotoc;
 mod kani_compiler;

kani-compiler/src/parser.rs

@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use crate::kani_queries::ReachabilityType;
+use crate::kani_queries::{BackendOption, ReachabilityType};
 use clap::{builder::PossibleValuesParser, command, Arg, ArgAction, ArgMatches, Command};
 use std::env;
 use std::str::FromStr;
@@ -10,9 +10,6 @@ use strum::VariantNames as _;
 /// Option name used to set log level.
 pub const LOG_LEVEL: &str = "log-level";
 
-/// Option name used to enable goto-c compilation.
-pub const GOTO_C: &str = "goto-c";
-
 /// Option name used to override Kani library path.
 pub const KANI_LIB: &str = "kani-lib";
 
@@ -40,6 +37,9 @@ pub const WRITE_JSON_SYMTAB: &str = "write-json-symtab";
 /// Option name used to select which reachability analysis to perform.
 pub const REACHABILITY: &str = "reachability";
 
+/// Option name used to select which backend to use.
+pub const BACKEND: &str = "backend";
+
 /// Option name used to enable stubbing.
 pub const ENABLE_STUBBING: &str = "enable-stubbing";
 
@@ -56,12 +56,6 @@ pub fn parser() -> Command {
  .help("Sets the path to locate the kani library.")
  .action(ArgAction::Set),
  )
- .arg(
- Arg::new(GOTO_C)
- .long(GOTO_C)
- .help("Enables compilation to goto-c intermediate representation.")
- .action(ArgAction::SetTrue),
- )
  .arg(
  Arg::new(LOG_LEVEL)
  .long(LOG_LEVEL)
@@ -107,6 +101,15 @@ pub fn parser() -> Command {
  .help("Selects the type of reachability analysis to perform.")
  .action(ArgAction::Set),
  )
+ .arg(
+ Arg::new(BACKEND)
+ .long(BACKEND)
+ .value_parser(PossibleValuesParser::new(BackendOption::VARIANTS))
+ .required(false)
+ .default_value(BackendOption::None.as_ref())
+ .help("Selects the backend to use.")
+ .action(ArgAction::Set),
+ )
  .arg(
  Arg::new(PRETTY_OUTPUT_FILES)
  .long(PRETTY_OUTPUT_FILES)
@@ -149,13 +152,19 @@ pub fn parser() -> Command {
 
 pub trait KaniCompilerParser {
  fn reachability_type(&self) -> ReachabilityType;
+ fn backend(&self) -> BackendOption;
 }
 
 impl KaniCompilerParser for ArgMatches {
  fn reachability_type(&self) -> ReachabilityType {
  self.get_one::<String>(REACHABILITY)
  .map_or(ReachabilityType::None, |arg| ReachabilityType::from_str(arg).unwrap())
  }
+
+ fn backend(&self) -> BackendOption {
+ self.get_one::<String>(BACKEND)
+ .map_or(BackendOption::None, |arg| BackendOption::from_str(arg).unwrap())
+ }
 }
 
 /// Return whether we should run our flavour of the compiler, and which arguments to pass to rustc.
@@ -195,9 +204,9 @@ mod parser_test {
 
  #[test]
  fn test_kani_flags() {
- let args = vec!["kani-compiler", "--goto-c", "--kani-lib", "some/path"];
+ let args = vec!["kani-compiler", "--backend=c_prover", "--kani-lib", "some/path"];
  let matches = parser().get_matches_from(args);
- assert!(matches.get_flag("goto-c"));
+ assert_eq!(matches.get_one::<String>("backend"), Some(&"c_prover".to_string()));
  assert_eq!(matches.get_one::<String>("kani-lib"), Some(&"some/path".to_string()));
  }
 

kani-driver/src/args/common.rs

@@ -42,6 +42,8 @@ pub enum UnstableFeatures {
  CFfi,
  /// Enable concrete playback flow.
  ConcretePlayback,
+ /// Boogie backend.
+ Boogie,
 }
 
 impl ValidateArgs for CommonArgs {

kani-driver/src/call_cargo.rs

@@ -102,6 +102,9 @@ impl KaniSession {
  // Arguments that will only be passed to the target package.
  let mut pkg_args: Vec<String> = vec![];
  pkg_args.extend(["--".to_string(), self.reachability_arg()]);
+ if let Some(backend_arg) = self.backend_arg() {
+ pkg_args.push(backend_arg);
+ }
 
  let mut found_target = false;
  let packages = packages_to_verify(&self.args, &metadata)?;

kani-driver/src/call_single_file.rs

@@ -6,6 +6,7 @@ use std::ffi::OsString;
 use std::path::{Path, PathBuf};
 use std::process::Command;
 
+use crate::args::common::UnstableFeatures;
 use crate::session::{lib_folder, KaniSession};
 
 impl KaniSession {
@@ -20,6 +21,14 @@ impl KaniSession {
  let mut kani_args = self.kani_compiler_flags();
  kani_args.push(format!("--reachability={}", self.reachability_mode()));
 
+ // This argument will select the Kani flavour of the compiler. It will be removed before
+ // rustc driver is invoked.
+ if self.args.common_args.unstable_features.contains(&UnstableFeatures::Boogie) {
+ kani_args.push("--backend=boogie".into());
+ } else {
+ kani_args.push("--backend=c_prover".into());
+ }
+
  let mut rustc_args = self.kani_rustc_flags();
  rustc_args.push(file.into());
  rustc_args.push("--out-dir".into());
@@ -64,6 +73,14 @@ impl KaniSession {
  to_rustc_arg(vec![format!("--reachability={}", self.reachability_mode())])
  }
 
+ pub fn backend_arg(&self) -> Option<String> {
+ if self.args.common_args.unstable_features.contains(&UnstableFeatures::Boogie) {
+ Some(to_rustc_arg(vec!["--backend=boogie".into()]))
+ } else {
+ None
+ }
+ }
+
  /// These arguments are arguments passed to kani-compiler that are `kani` compiler specific.
  pub fn kani_compiler_flags(&self) -> Vec<String> {
  let mut flags = vec![check_version()];
@@ -104,10 +121,6 @@ impl KaniSession {
  .map(|feature| format!("--unstable={feature}")),
  );
 
- // This argument will select the Kani flavour of the compiler. It will be removed before
- // rustc driver is invoked.
- flags.push("--goto-c".into());
-
  flags
  }
 

scripts/codegen-firecracker.sh

@@ -42,7 +42,7 @@ RUST_FLAGS=(
  "--kani-compiler"
  "-Cpanic=abort"
  "-Zalways-encode-mir"
- "-Cllvm-args=--goto-c"
+ "-Cllvm-args=--backend=c_prover"
  "-Cllvm-args=--ignore-global-asm"
  "-Cllvm-args=--reachability=pub_fns"
  "--sysroot=${KANI_DIR}/target/kani"

scripts/std-lib-regression.sh

@@ -71,7 +71,7 @@ RUST_FLAGS=(
  "--kani-compiler"
  "-Cpanic=abort"
  "-Zalways-encode-mir"
- "-Cllvm-args=--goto-c"
+ "-Cllvm-args=--backend=c_prover"
  "-Cllvm-args=--ignore-global-asm"
  "-Cllvm-args=--reachability=pub_fns"
 )

tests/cargo-kani/boogie/hello/Cargo.toml

@@ -0,0 +1,18 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "hello"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+
+[package.metadata.kani.unstable]
+boogie = true
+
+[package.metadata.kani.flags]
+# Make sure the compiler is run even if the output artifacts exist
+force-build = true

tests/cargo-kani/boogie/hello/expected

@@ -0,0 +1 @@
+Hello, Boogie!

tests/cargo-kani/boogie/hello/src/lib.rs

@@ -0,0 +1,8 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This is an initial test for the Boogie backend that checks that "Hello,
+//! Boogie!" is printed when the `--boogie` option is used
+
+#[kani::proof]
+fn check_boogie_option() {}

tests/expected/boogie/hello/expected

@@ -0,0 +1 @@
+Hello, Boogie!

tests/expected/boogie/hello/test.rs

@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This is an initial test for the Boogie backend that checks that "Hello,
+//! Boogie!" is printed when the `--boogie` option is used
+
+// kani-flags: -Zboogie
+
+#[kani::proof]
+fn check_boogie_option() {}