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() {}