diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index a9e4c974c6eb..b032f8c70858 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -27,7 +27,8 @@ tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt" # Future proofing: enable backend dependencies using feature. [features] -default = ['cprover'] +default = ['boogie', 'cprover'] +boogie = ['serde'] cprover = ['cbmc', 'num', 'serde'] write_json_symtab = [] diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index b174795b7259..9acc7a59e168 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -4,6 +4,20 @@ use strum_macros::{AsRefStr, EnumString, EnumVariantNames}; use tracing_subscriber::filter::Directive; +#[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 { @@ -68,7 +82,6 @@ pub struct Arguments { #[clap(long)] /// Pass the kani version to the compiler to ensure cache coherence. check_version: Option, - #[clap(long)] - /// A legacy flag that is now ignored. - goto_c: bool, + #[clap(long = "backend", default_value = "none")] + pub backend: BackendOption, } diff --git a/kani-compiler/src/codegen_boogie/compiler_interface.rs b/kani-compiler/src/codegen_boogie/compiler_interface.rs new file mode 100644 index 000000000000..30a44e015107 --- /dev/null +++ b/kani-compiler/src/codegen_boogie/compiler_interface.rs @@ -0,0 +1,669 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This file contains the code necessary to interface with the boogie backend + +use crate::args::ReachabilityType; +use crate::codegen_boogie::BoogieCtx; +use crate::kani_middle::analysis; +use crate::kani_middle::attributes::is_test_harness_description; +use crate::kani_middle::metadata::gen_test_metadata; +use crate::kani_middle::provide; +use crate::kani_middle::reachability::{ + collect_reachable_items, filter_const_crate_items, filter_crate_items, +}; +use crate::kani_middle::{check_reachable_items, dump_mir_items}; +use crate::kani_queries::QueryDb; +use kani_metadata::artifact::convert_type; +use kani_metadata::CompilerArtifactStub; +use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata}; +use rustc_codegen_ssa::back::archive::{ + get_native_object_symbols, ArArchiveBuilder, ArchiveBuilder, +}; +use rustc_codegen_ssa::back::metadata::create_wrapper_file; +use rustc_codegen_ssa::traits::CodegenBackend; +use rustc_codegen_ssa::{CodegenResults, CrateInfo}; +use rustc_data_structures::fx::{FxHashMap, FxIndexMap}; +use rustc_data_structures::temp_dir::MaybeTempDir; +use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE}; +use rustc_hir::def_id::LOCAL_CRATE; +use rustc_hir::definitions::DefPathHash; +use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME}; +use rustc_metadata::EncodedMetadata; +use rustc_middle::dep_graph::{WorkProduct, WorkProductId}; +use rustc_middle::mir::mono::MonoItem; +use rustc_middle::query::{ExternProviders, Providers}; +use rustc_middle::ty::TyCtxt; +use rustc_session::config::{CrateType, OutputFilenames, OutputType}; +use rustc_session::cstore::MetadataLoaderDyn; +use rustc_session::output::out_filename; +use rustc_session::Session; +use rustc_target::abi::Endian; +use rustc_target::spec::PanicStrategy; +use std::any::Any; +use std::collections::BTreeMap; +use std::collections::HashSet; +use std::fmt::Write; +use std::fs::File; +use std::io::BufWriter; +use std::path::Path; +use std::sync::{Arc, Mutex}; +use std::time::Instant; +use tempfile::Builder as TempFileBuilder; +use tracing::{debug, info}; + +pub type UnsupportedConstructs = FxHashMap; + +#[derive(Clone, Debug)] +pub struct MachineModel { + /// Is the architecture big endian? + /// Minimum architectural alignment, in bytes + /// The name of the architecture + /// Width of a pointer, in bits + pub alignment: u64, + pub architecture: String, + pub bool_width: u64, + pub char_is_unsigned: bool, + pub char_width: u64, + pub double_width: u64, + pub float_width: u64, + pub int_width: u64, + pub is_big_endian: bool, + pub long_double_width: u64, + pub long_int_width: u64, + pub long_long_int_width: u64, + pub memory_operand_size: u64, + pub null_is_zero: bool, + pub pointer_width: u64, + pub rounding_mode: RoundingMode, + pub short_int_width: u64, + pub single_width: u64, + pub wchar_t_is_unsigned: bool, + pub wchar_t_width: u64, + pub word_size: u64, +} + +/// The different rounding modes supported by cbmc. +/// +#[derive(Clone, Copy, Debug)] +pub enum RoundingMode { + ToNearest = 0, + Downward = 1, + Upward = 2, + TowardsZero = 3, +} + +impl From for i32 { + fn from(rm: RoundingMode) -> Self { + rm as Self + } +} + +impl From for i128 { + fn from(rm: RoundingMode) -> Self { + rm as Self + } +} + +#[derive(Clone)] +pub struct BoogieCodegenBackend { + /// The query is shared with `KaniCompiler` and it is initialized as part of `rustc` + /// initialization, which may happen after this object is created. + /// Since we don't have any guarantees on when the compiler creates the Backend object, neither + /// in which thread it will be used, we prefer to explicitly synchronize any query access. + queries: Arc>, +} + +impl BoogieCodegenBackend { + pub fn new(queries: Arc>) -> Self { + BoogieCodegenBackend { queries } + } + + /// Generate code that is reachable from the given starting points. + fn codegen_items<'tcx>( + &self, + tcx: TyCtxt<'tcx>, + starting_items: &[MonoItem<'tcx>], + boogie_file: &Path, + _machine_model: &MachineModel, + ) -> (BoogieCtx<'tcx>, Vec>) { + let items = with_timer( + || collect_reachable_items(tcx, starting_items), + "codegen reachability analysis", + ); + dump_mir_items(tcx, &items, &boogie_file.with_extension("kani.mir")); + + // Follow rustc naming convention (cx is abbrev for context). + // https://rustc-dev-guide.rust-lang.org/conventions.html#naming-conventions + let mut bcx = BoogieCtx::new(tcx, (*self.queries.lock().unwrap()).clone()); + check_reachable_items(tcx, &bcx.queries, &items); + + println!("Hello, Boogie!"); + + with_timer( + || { + // we first declare all items + for item in &items { + match *item { + MonoItem::Fn(instance) => { + bcx.declare_function(instance); + } + MonoItem::Static(_def_id) => {} + MonoItem::GlobalAsm(_) => {} // Ignore this. We have already warned about it. + } + } + + // then we move on to codegen + for item in &items { + match *item { + MonoItem::Fn(_instance) => {} + MonoItem::Static(_def_id) => {} + MonoItem::GlobalAsm(_) => {} // We have already warned above + } + } + }, + "codegen", + ); + + (bcx, items) + } +} + +impl CodegenBackend for BoogieCodegenBackend { + fn metadata_loader(&self) -> Box { + Box::new(rustc_codegen_ssa::back::metadata::DefaultMetadataLoader) + } + + fn provide(&self, providers: &mut Providers) { + provide::provide(providers, &self.queries.lock().unwrap()); + } + + fn provide_extern(&self, providers: &mut ExternProviders) { + provide::provide_extern(providers, &self.queries.lock().unwrap()); + } + + fn print_version(&self) { + println!("Kani-boogie version: {}", env!("CARGO_PKG_VERSION")); + } + + fn locale_resource(&self) -> &'static str { + // We don't currently support multiple languages. + DEFAULT_LOCALE_RESOURCE + } + + fn codegen_crate( + &self, + tcx: TyCtxt, + rustc_metadata: EncodedMetadata, + _need_metadata_module: bool, + ) -> Box { + // Queries shouldn't change today once codegen starts. + let queries = self.queries.lock().unwrap().clone(); + check_target(tcx.sess); + check_options(tcx.sess); + + // Codegen all items that need to be processed according to the selected reachability mode: + // + // - Harnesses: Generate one model per local harnesses (marked with `kani::proof` attribute). + // - Tests: Generate one model per test harnesses. + // - PubFns: Generate code for all reachable logic starting from the local public functions. + // - None: Don't generate code. This is used to compile dependencies. + let base_filename = tcx.output_filenames(()).output_path(OutputType::Object); + let reachability = queries.args().reachability_analysis; + let mut results = BoogieCodegenResults::new(tcx, reachability); + match reachability { + ReachabilityType::Harnesses => { + // Cross-crate collecting of all items that are reachable from the crate harnesses. + let harnesses = queries.target_harnesses(); + let mut items: HashSet = HashSet::with_capacity(harnesses.len()); + items.extend(harnesses); + let harnesses = + filter_crate_items(tcx, |_, def_id| items.contains(&tcx.def_path_hash(def_id))); + for harness in harnesses { + let model_path = + queries.harness_model_path(&tcx.def_path_hash(harness.def_id())).unwrap(); + let (gcx, items) = + self.codegen_items(tcx, &[harness], model_path, &results.machine_model); + results.extend(gcx, items, None); + } + } + ReachabilityType::Tests => { + // We're iterating over crate items here, so what we have to codegen is the "test description" containing the + // test closure that we want to execute + // TODO: Refactor this code so we can guarantee that the pair (test_fn, test_desc) actually match. + let mut descriptions = vec![]; + let harnesses = filter_const_crate_items(tcx, |_, def_id| { + if is_test_harness_description(tcx, def_id) { + descriptions.push(def_id); + true + } else { + false + } + }); + // Codegen still takes a considerable amount, thus, we only generate one model for + // all harnesses and copy them for each harness. + // We will be able to remove this once we optimize all calls to CBMC utilities. + // https://github.com/model-checking/kani/issues/1971 + let model_path = base_filename.with_extension(ArtifactType::SymTabGoto); + let (bcx, items) = + self.codegen_items(tcx, &harnesses, &model_path, &results.machine_model); + results.extend(bcx, items, None); + + for (test_fn, test_desc) in harnesses.iter().zip(descriptions.iter()) { + let instance = + if let MonoItem::Fn(instance) = test_fn { instance } else { continue }; + let metadata = gen_test_metadata(tcx, *test_desc, *instance, &base_filename); + let test_model_path = &metadata.goto_file.as_ref().unwrap(); + std::fs::copy(&model_path, &test_model_path).expect(&format!( + "Failed to copy {} to {}", + model_path.display(), + test_model_path.display() + )); + results.harnesses.push(metadata); + } + } + ReachabilityType::None => {} + ReachabilityType::PubFns => { + let entry_fn = tcx.entry_fn(()).map(|(id, _)| id); + let local_reachable = filter_crate_items(tcx, |_, def_id| { + (tcx.is_reachable_non_generic(def_id) && tcx.def_kind(def_id).is_fn_like()) + || entry_fn == Some(def_id) + }); + let model_path = base_filename.with_extension(ArtifactType::SymTabGoto); + let (bcx, items) = + self.codegen_items(tcx, &local_reachable, &model_path, &results.machine_model); + results.extend(bcx, items, None); + } + } + + if reachability != ReachabilityType::None { + // Print compilation report. + results.print_report(tcx); + + if reachability != ReachabilityType::Harnesses { + // In a workspace, cargo seems to be using the same file prefix to build a crate that is + // a package lib and also a dependency of another package. + // To avoid overriding the metadata for its verification, we skip this step when + // reachability is None, even because there is nothing to record. + write_file( + &base_filename, + ArtifactType::Metadata, + &results.generate_metadata(), + queries.args().output_pretty_json, + ); + } + } + codegen_results(tcx, rustc_metadata, &results.machine_model) + } + + fn join_codegen( + &self, + ongoing_codegen: Box, + _sess: &Session, + _filenames: &OutputFilenames, + ) -> Result<(CodegenResults, FxIndexMap), ErrorGuaranteed> { + match ongoing_codegen.downcast::<(CodegenResults, FxIndexMap)>() + { + Ok(val) => Ok(*val), + Err(val) => panic!("unexpected error: {:?}", (*val).type_id()), + } + } + + /// Emit output files during the link stage if it was requested. + /// + /// We need to emit `rlib` files normally if requested. Cargo expects these in some + /// circumstances and sends them to subsequent builds with `-L`. + /// + /// We CAN NOT invoke the native linker, because that will fail. We don't have real objects. + /// What determines whether the native linker is invoked or not is the set of `crate_types`. + /// Types such as `bin`, `cdylib`, `dylib` will trigger the native linker. + /// + /// Thus, we manually build the rlib file including only the `rmeta` file. + /// + /// For cases where no metadata file was requested, we stub the file requested by writing the + /// path of the `kani-metadata.json` file so `kani-driver` can safely find the latest metadata. + /// See for more details. + fn link( + &self, + sess: &Session, + codegen_results: CodegenResults, + outputs: &OutputFilenames, + ) -> Result<(), ErrorGuaranteed> { + let requested_crate_types = &codegen_results.crate_info.crate_types; + for crate_type in requested_crate_types { + let out_fname = out_filename( + sess, + *crate_type, + outputs, + codegen_results.crate_info.local_crate_name, + ); + let out_path = out_fname.as_path(); + debug!(?crate_type, ?out_path, "link"); + if *crate_type == CrateType::Rlib { + // Emit the `rlib` that contains just one file: `.rmeta` + let mut builder = Box::new(ArArchiveBuilder::new(sess, get_native_object_symbols)); + let tmp_dir = TempFileBuilder::new().prefix("kani").tempdir().unwrap(); + let path = MaybeTempDir::new(tmp_dir, sess.opts.cg.save_temps); + let (metadata, _metadata_position) = create_wrapper_file( + sess, + b".rmeta".to_vec(), + codegen_results.metadata.raw_data(), + ); + let metadata = emit_wrapper_file(sess, &metadata, &path, METADATA_FILENAME); + builder.add_file(&metadata); + builder.build(&out_path); + } else { + // Write the location of the kani metadata file in the requested compiler output file. + let base_filename = outputs.output_path(OutputType::Object); + let content_stub = CompilerArtifactStub { + metadata_path: base_filename.with_extension(ArtifactType::Metadata), + }; + let out_file = File::create(out_path).unwrap(); + serde_json::to_writer(out_file, &content_stub).unwrap(); + } + } + Ok(()) + } +} + +fn check_target(session: &Session) { + // The requirement below is needed to build a valid CBMC machine model + // in function `machine_model_from_session` from + // src/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs + let is_linux_target = session.target.llvm_target == "x86_64-unknown-linux-gnu"; + // Comparison with `x86_64-apple-darwin` does not work well because the LLVM + // target may become `x86_64-apple-macosx10.7.0` (or similar) and fail + let is_x86_64_darwin_target = session.target.llvm_target.starts_with("x86_64-apple-"); + // looking for `arm64-apple-*` + let is_arm64_darwin_target = session.target.llvm_target.starts_with("arm64-apple-"); + + if !is_linux_target && !is_x86_64_darwin_target && !is_arm64_darwin_target { + let err_msg = format!( + "Kani requires the target platform to be `x86_64-unknown-linux-gnu` or \ + `x86_64-apple-*` or `arm64-apple-*`, but it is {}", + &session.target.llvm_target + ); + session.err(err_msg); + } + + session.abort_if_errors(); +} + +fn check_options(session: &Session) { + // The requirements for `min_global_align` and `endian` are needed to build + // a valid CBMC machine model in function `machine_model_from_session` from + // src/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs + match session.target.options.min_global_align { + Some(1) => (), + Some(align) => { + let err_msg = format!( + "Kani requires the target architecture option `min_global_align` to be 1, but it is {align}." + ); + session.err(err_msg); + } + _ => (), + } + + if session.target.options.endian != Endian::Little { + session.err("Kani requires the target architecture option `endian` to be `little`."); + } + + if !session.overflow_checks() { + session.err("Kani requires overflow checks in order to provide a sound analysis."); + } + + if session.panic_strategy() != PanicStrategy::Abort { + session.err( + "Kani can only handle abort panic strategy (-C panic=abort). See for more details \ + https://github.com/model-checking/kani/issues/692", + ); + } + + session.abort_if_errors(); +} + +/// Return a struct that contains information about the codegen results as expected by `rustc`. +fn codegen_results( + tcx: TyCtxt, + rustc_metadata: EncodedMetadata, + machine: &MachineModel, +) -> Box { + let work_products = FxIndexMap::::default(); + Box::new(( + CodegenResults { + modules: vec![], + allocator_module: None, + metadata_module: None, + metadata: rustc_metadata, + crate_info: CrateInfo::new(tcx, machine.architecture.clone()), + }, + work_products, + )) +} + +pub fn write_file(base_path: &Path, file_type: ArtifactType, source: &T, pretty: bool) +where + T: serde::Serialize, +{ + let filename = convert_type(base_path, ArtifactType::SymTabGoto, file_type); + debug!(?filename, "write_json"); + let out_file = File::create(&filename).unwrap(); + let writer = BufWriter::new(out_file); + if pretty { + serde_json::to_writer_pretty(writer, &source).unwrap(); + } else { + serde_json::to_writer(writer, &source).unwrap(); + } +} + +struct BoogieCodegenResults<'tcx> { + reachability: ReachabilityType, + harnesses: Vec, + unsupported_constructs: UnsupportedConstructs, + concurrent_constructs: UnsupportedConstructs, + items: Vec>, + crate_name: String, + machine_model: MachineModel, +} + +impl<'tcx> BoogieCodegenResults<'tcx> { + pub fn new(tcx: TyCtxt, reachability: ReachabilityType) -> Self { + BoogieCodegenResults { + reachability, + harnesses: vec![], + unsupported_constructs: UnsupportedConstructs::default(), + concurrent_constructs: UnsupportedConstructs::default(), + items: vec![], + crate_name: tcx.crate_name(LOCAL_CRATE).as_str().into(), + machine_model: new_machine_model(tcx.sess), + } + } + + /// Method that generates `KaniMetadata` from the given compilation results. + pub fn generate_metadata(&self) -> KaniMetadata { + // TODO: populate unsupported features + let unsupported_features = Vec::new(); + let (proofs, tests) = if self.reachability == ReachabilityType::Harnesses { + (self.harnesses.clone(), vec![]) + } else { + (vec![], self.harnesses.clone()) + }; + KaniMetadata { + crate_name: self.crate_name.to_string(), + proof_harnesses: proofs, + unsupported_features, + test_harnesses: tests, + } + } + + fn extend( + &mut self, + _bcx: BoogieCtx, + items: Vec>, + metadata: Option, + ) { + let mut items = items; + self.harnesses.extend(metadata); + self.items.append(&mut items); + } + + /// Prints a report at the end of the compilation. + fn print_report(&self, tcx: TyCtxt<'tcx>) { + // Print all unsupported constructs. + if !self.unsupported_constructs.is_empty() { + // Sort alphabetically. + let unsupported: BTreeMap = + self.unsupported_constructs.iter().map(|(key, val)| (key.clone(), val)).collect(); + let mut msg = String::from("Found the following unsupported constructs:\n"); + unsupported.iter().for_each(|(construct, locations)| { + writeln!(&mut msg, " - {construct} ({})", locations).unwrap(); + }); + msg += "\nVerification will fail if one or more of these constructs is reachable."; + msg += "\nSee https://model-checking.github.io/kani/rust-feature-support.html for more \ + details."; + tcx.sess.warn(msg); + } + + if !self.concurrent_constructs.is_empty() { + let mut msg = String::from( + "Kani currently does not support concurrency. The following constructs will be treated \ + as sequential operations:\n", + ); + for (construct, locations) in self.concurrent_constructs.iter() { + writeln!(&mut msg, " - {construct} ({})", locations).unwrap(); + } + tcx.sess.warn(msg); + } + + // Print some compilation stats. + if tracing::enabled!(tracing::Level::INFO) { + analysis::print_stats(tcx, &self.items); + } + } +} + +/// Builds a machine model which is required by CBMC +fn new_machine_model(sess: &Session) -> MachineModel { + // The model assumes a `x86_64-unknown-linux-gnu`, `x86_64-apple-darwin` + // or `aarch64-apple-darwin` platform. We check the target platform in function + // `check_target` from src/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs + // and error if it is not any of the ones we expect. + let architecture = &sess.target.arch; + let pointer_width = sess.target.pointer_width.into(); + + // The model assumes the following values for session options: + // * `min_global_align`: 1 + // * `endian`: `Endian::Little` + // + // We check these options in function `check_options` from + // src/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs + // and error if their values are not the ones we expect. + let alignment = sess.target.options.min_global_align.unwrap_or(1); + let is_big_endian = match sess.target.options.endian { + Endian::Little => false, + Endian::Big => true, + }; + + // The values below cannot be obtained from the session so they are + // hardcoded using standard ones for the supported platforms + // see /tools/sizeofs/main.cpp. + // For reference, the definition in CBMC: + //https://github.com/diffblue/cbmc/blob/develop/src/util/config.cpp + match architecture.as_ref() { + "x86_64" => { + let bool_width = 8; + let char_is_unsigned = false; + let char_width = 8; + let double_width = 64; + let float_width = 32; + let int_width = 32; + let long_double_width = 128; + let long_int_width = 64; + let long_long_int_width = 64; + let short_int_width = 16; + let single_width = 32; + let wchar_t_is_unsigned = false; + let wchar_t_width = 32; + + MachineModel { + architecture: architecture.to_string(), + alignment, + bool_width, + char_is_unsigned, + char_width, + double_width, + float_width, + int_width, + is_big_endian, + long_double_width, + long_int_width, + long_long_int_width, + memory_operand_size: int_width / 8, + null_is_zero: true, + pointer_width, + rounding_mode: RoundingMode::ToNearest, + short_int_width, + single_width, + wchar_t_is_unsigned, + wchar_t_width, + word_size: int_width, + } + } + "aarch64" => { + let bool_width = 8; + let char_is_unsigned = true; + let char_width = 8; + let double_width = 64; + let float_width = 32; + let int_width = 32; + let long_double_width = 64; + let long_int_width = 64; + let long_long_int_width = 64; + let short_int_width = 16; + let single_width = 32; + let wchar_t_is_unsigned = false; + let wchar_t_width = 32; + + MachineModel { + // CBMC calls it arm64, not aarch64 + architecture: "arm64".to_string(), + alignment, + bool_width, + char_is_unsigned, + char_width, + double_width, + float_width, + int_width, + is_big_endian, + long_double_width, + long_int_width, + long_long_int_width, + memory_operand_size: int_width / 8, + null_is_zero: true, + pointer_width, + rounding_mode: RoundingMode::ToNearest, + short_int_width, + single_width, + wchar_t_is_unsigned, + wchar_t_width, + word_size: int_width, + } + } + _ => { + panic!("Unsupported architecture: {architecture}"); + } + } +} + +/// Execute the provided function and measure the clock time it took for its execution. +/// Log the time with the given description. +pub fn with_timer(func: F, description: &str) -> T +where + F: FnOnce() -> T, +{ + let start = Instant::now(); + let ret = func(); + let elapsed = start.elapsed(); + info!("Finished {description} in {}s", elapsed.as_secs_f32()); + ret +} diff --git a/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs b/kani-compiler/src/codegen_boogie/context/boogie_ctx.rs new file mode 100644 index 000000000000..4ef902f0c36a --- /dev/null +++ b/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"); + } +} diff --git a/kani-compiler/src/codegen_boogie/context/mod.rs b/kani-compiler/src/codegen_boogie/context/mod.rs new file mode 100644 index 000000000000..3164f967c1b9 --- /dev/null +++ b/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; diff --git a/kani-compiler/src/codegen_boogie/mod.rs b/kani-compiler/src/codegen_boogie/mod.rs new file mode 100644 index 000000000000..d59e77e6a271 --- /dev/null +++ b/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; diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index fc04b68ec747..c4e1a9549b9e 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -15,7 +15,9 @@ //! in order to apply the stubs. For the subsequent runs, we add the stub configuration to //! `-C llvm-args`. -use crate::args::{Arguments, ReachabilityType}; +use crate::args::{Arguments, BackendOption, ReachabilityType}; +#[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; @@ -55,16 +57,53 @@ pub fn run(args: Vec) -> 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>) -> Box { + #[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>) -> Box { + #[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>) -> Box { - Box::new(GotocCodegenBackend::new(queries)) + let backend = queries.lock().unwrap().args().backend; + match backend { + BackendOption::None => { + // priority list of backends + if cfg!(feature = "cprover") { + cprover_backend(queries) + } else if cfg!(feature = "boogie") { + 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>) -> Box { - 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. diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 4316d188c02d..33d64951bc07 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -34,6 +34,8 @@ extern crate stable_mir; extern crate tempfile; mod args; +#[cfg(feature = "boogie")] +mod codegen_boogie; #[cfg(feature = "cprover")] mod codegen_cprover_gotoc; mod kani_compiler; diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 66166913c9cb..81ceb695e69f 100644 --- a/kani-driver/src/call_cargo.rs +++ b/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 = 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)?; diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index 9b6e0598daa5..73d2ee7f2eb5 100644 --- a/kani-driver/src/call_single_file.rs +++ b/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::UnstableFeature; use crate::session::{lib_folder, KaniSession}; impl KaniSession { @@ -20,6 +21,12 @@ impl KaniSession { 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::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 +71,14 @@ impl KaniSession { to_rustc_arg(vec![format!("--reachability={}", self.reachability_mode())]) } + pub fn backend_arg(&self) -> Option { + if self.args.common_args.unstable_features.contains(UnstableFeature::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 { let mut flags = vec![check_version()]; @@ -102,10 +117,6 @@ impl KaniSession { flags.extend(self.args.common_args.unstable_features.as_arguments().map(str::to_string)); - // 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 } diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index 060508666735..d93643d90a21 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -82,6 +82,8 @@ pub enum UnstableFeature { LineCoverage, /// Enable function contracts [RFC 9](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html) FunctionContracts, + /// Boogie backend. + Boogie, } impl UnstableFeature { diff --git a/scripts/codegen-firecracker.sh b/scripts/codegen-firecracker.sh index 3ac7dfa6585d..c6be47542c03 100755 --- a/scripts/codegen-firecracker.sh +++ b/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" diff --git a/scripts/std-lib-regression.sh b/scripts/std-lib-regression.sh index a7881f1dc19a..a1474945ee41 100755 --- a/scripts/std-lib-regression.sh +++ b/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" "-Cllvm-args=--build-std" diff --git a/tests/cargo-kani/boogie/hello/Cargo.toml b/tests/cargo-kani/boogie/hello/Cargo.toml new file mode 100644 index 000000000000..2e9786cc8426 --- /dev/null +++ b/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 diff --git a/tests/cargo-kani/boogie/hello/expected b/tests/cargo-kani/boogie/hello/expected new file mode 100644 index 000000000000..f237bd80dd30 --- /dev/null +++ b/tests/cargo-kani/boogie/hello/expected @@ -0,0 +1 @@ +Hello, Boogie! diff --git a/tests/cargo-kani/boogie/hello/src/lib.rs b/tests/cargo-kani/boogie/hello/src/lib.rs new file mode 100644 index 000000000000..3931ebdc149d --- /dev/null +++ b/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() {} diff --git a/tests/expected/boogie/hello/expected b/tests/expected/boogie/hello/expected new file mode 100644 index 000000000000..f237bd80dd30 --- /dev/null +++ b/tests/expected/boogie/hello/expected @@ -0,0 +1 @@ +Hello, Boogie! diff --git a/tests/expected/boogie/hello/test.rs b/tests/expected/boogie/hello/test.rs new file mode 100644 index 000000000000..1dcc8bf488f7 --- /dev/null +++ b/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() {} diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index ee89c252dc4f..efcbb729fba4 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -183,7 +183,7 @@ impl<'test> TestCx<'test> { fn check(&self) { let mut rustc = Command::new("kani-compiler"); rustc - .args(["--goto-c"]) + .args(["--backend=c_prover"]) .args(self.props.compile_flags.clone()) .args(["-Z", "no-codegen"]) .arg(&self.testpaths.file); @@ -203,7 +203,7 @@ impl<'test> TestCx<'test> { fn codegen(&self) { let mut rustc = Command::new("kani-compiler"); rustc - .args(["--goto-c"]) + .args(["--backend=c_prover"]) .args(self.props.compile_flags.clone()) .args(["--out-dir"]) .arg(self.output_base_dir())