Turn goto-c backend library into a module. (rust-lang#871)

celinval · tedinski · commit 140a2f338424 · 2022-03-04T12:10:51.000-08:00
* Change backend library to be a module in the compiler

Also rename from rustc_codegen_kani to codegen_cprover_gotoc

Keeping cprover dependencies separate in case we ever decided to add
another backend.
diff --git a/Cargo.lock b/Cargo.lock
@@ -417,9 +417,20 @@ name = "kani-compiler"
 version = "0.1.0"
 dependencies = [
  "atty",
+ "bitflags",
  "clap",
+ "cprover_bindings",
+ "cstr",
  "kani_queries",
- "rustc_codegen_kani",
+ "kani_restrictions",
+ "libc",
+ "measureme",
+ "num",
+ "rustc-demangle",
+ "serde",
+ "serde_json",
+ "smallvec",
+ "snap",
  "tracing",
  "tracing-subscriber",
  "tracing-tree",
@@ -896,26 +907,6 @@ version = "1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "08d43f7aa6b08d49f382cde6a7982047c3426db949b1424bc4b7ec9ae12c6ce2"
 
-[[package]]
-name = "rustc_codegen_kani"
-version = "0.0.0"
-dependencies = [
- "bitflags",
- "cprover_bindings",
- "cstr",
- "kani_queries",
- "kani_restrictions",
- "libc",
- "measureme",
- "num",
- "rustc-demangle",
- "serde",
- "serde_json",
- "smallvec",
- "snap",
- "tracing",
-]
-
 [[package]]
 name = "rustdoc"
 version = "0.0.0"
diff --git a/src/kani-compiler/Cargo.toml b/src/kani-compiler/Cargo.toml
@@ -9,13 +9,30 @@ license = "MIT OR Apache-2.0"
 
 [dependencies]
 atty = "0.2.14"
+bitflags = { version = "1.0", optional = true }
+cbmc = { path = "../../cprover_bindings", package = "cprover_bindings", optional = true }
 clap = "2.33.0"
+cstr = { version = "0.2", optional = true }
 kani_queries = {path = "kani_queries"}
-rustc_codegen_kani = {path = "rustc_codegen_kani"}
+kani_restrictions = { path = "../../library/kani_restrictions", optional = true }
+libc = { version = "0.2", optional = true }
+measureme = { version = "9.1.0", optional = true }
+num = { version = "0.4.0", optional = true }
+rustc-demangle = { version = "0.1.21", optional = true }
+serde = { version = "1", optional = true }
+serde_json = { version = "1", optional = true }
+smallvec = { version = "1.6.1", features = ["union", "may_dangle"], optional = true }
+snap = { version = "1", optional = true }
 tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_info"]}
 tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]}
 tracing-tree = "0.2.0"
 
+# Future proofing: enable backend dependencies using feature.
+[features]
+default = ['cprover']
+cprover = ['bitflags', 'cbmc', 'cstr', 'kani_restrictions', 'libc', 'measureme', 'num', 'rustc-demangle', 'serde',
+    'serde_json', 'smallvec', 'snap']
+
 [package.metadata.rust-analyzer]
 # This package uses rustc crates.
 rustc_private=true
diff --git a/src/kani-compiler/rustc_codegen_kani/Cargo.toml b/src/kani-compiler/rustc_codegen_kani/Cargo.toml
diff --git a/src/kani-compiler/rustc_codegen_kani/src/lib.rs b/src/kani-compiler/rustc_codegen_kani/src/lib.rs
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs
@@ -3,7 +3,7 @@
 
 //! This file contains functions related to codegenning MIR blocks into gotoc
 
-use crate::GotocCtx;
+use crate::codegen_cprover_gotoc::GotocCtx;
 use rustc_middle::mir::{BasicBlock, BasicBlockData};
 
 impl<'tcx> GotocCtx<'tcx> {
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
@@ -3,8 +3,8 @@
 
 //! This file contains functions related to codegenning MIR functions into gotoc
 
-use crate::context::metadata::HarnessMetadata;
-use crate::GotocCtx;
+use crate::codegen_cprover_gotoc::context::metadata::HarnessMetadata;
+use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{Expr, Stmt, Symbol};
 use cbmc::InternString;
 use rustc_ast::ast;
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -1,7 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! this module handles intrinsics
-use crate::GotocCtx;
+use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
 use rustc_middle::mir::Place;
 use rustc_middle::ty::layout::LayoutOf;
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -1,7 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-use crate::utils::slice_fat_ptr;
-use crate::GotocCtx;
+use crate::codegen_cprover_gotoc::utils::slice_fat_ptr;
+use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
 use cbmc::NO_PRETTY_NAME;
 use rustc_ast::ast::Mutability;
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -6,8 +6,8 @@
 //! in [codegen_place] below.
 
 use super::typ::TypeExt;
-use crate::utils::slice_fat_ptr;
-use crate::GotocCtx;
+use crate::codegen_cprover_gotoc::utils::slice_fat_ptr;
+use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{Expr, Type};
 use rustc_hir::Mutability;
 use rustc_middle::ty::layout::LayoutOf;
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -1,8 +1,8 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 use super::typ::{is_pointer, pointee_type, TypeExt};
-use crate::utils::{dynamic_fat_ptr, slice_fat_ptr};
-use crate::{GotocCtx, VtableCtx};
+use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
+use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
 use cbmc::utils::{aggr_tag, BUG_REPORT_URL};
 use cbmc::MachineModel;
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
@@ -3,7 +3,7 @@
 
 //! MIR Span related functions
 
-use crate::GotocCtx;
+use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Location;
 use rustc_middle::mir::{Local, VarDebugInfo, VarDebugInfoContents};
 use rustc_span::Span;
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 use super::typ::TypeExt;
 use super::typ::FN_RETURN_VOID_VAR_NAME;
-use crate::utils;
-use crate::{GotocCtx, VtableCtx};
+use crate::codegen_cprover_gotoc::utils;
+use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir;
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/static_var.rs
@@ -3,7 +3,7 @@
 
 //! This file contains functions related to codegenning MIR static variables into gotoc
 
-use crate::GotocCtx;
+use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Symbol;
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir::mono::MonoItem;
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/src/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -1,6 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-use crate::GotocCtx;
+use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{DatatypeComponent, Expr, Parameter, Symbol, SymbolTable, Type};
 use cbmc::utils::aggr_tag;
 use cbmc::{btree_map, NO_PRETTY_NAME};
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/src/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -3,8 +3,8 @@
 
 //! This file contains the code necessary to interface with the compiler backend
 
-use crate::context::metadata::KaniMetadata;
-use crate::GotocCtx;
+use crate::codegen_cprover_gotoc::context::metadata::KaniMetadata;
+use crate::codegen_cprover_gotoc::GotocCtx;
 use bitflags::_core::any::Any;
 use cbmc::goto_program::symtab_transformer;
 use cbmc::InternedString;
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs b/src/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
@@ -1,7 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use crate::GotocCtx;
+use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Stmt;
 use rustc_middle::mir::BasicBlock;
 use rustc_middle::mir::Body;
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/src/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
@@ -16,8 +16,8 @@
 use super::current_fn::CurrentFnCtx;
 use super::metadata::HarnessMetadata;
 use super::vtable_ctx::VtableCtx;
-use crate::overrides::{fn_hooks, GotocHooks};
-use crate::utils::full_crate_name;
+use crate::codegen_cprover_gotoc::overrides::{fn_hooks, GotocHooks};
+use crate::codegen_cprover_gotoc::utils::full_crate_name;
 use cbmc::goto_program::{DatatypeComponent, Expr, Location, Stmt, Symbol, SymbolTable, Type};
 use cbmc::utils::aggr_tag;
 use cbmc::{InternStringOption, InternedString, NO_PRETTY_NAME};
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/context/metadata.rs b/src/kani-compiler/src/codegen_cprover_gotoc/context/metadata.rs
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/context/mod.rs b/src/kani-compiler/src/codegen_cprover_gotoc/context/mod.rs
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs b/src/kani-compiler/src/codegen_cprover_gotoc/context/vtable_ctx.rs
@@ -15,7 +15,7 @@
 ///
 /// For the current CBMC implementation of function restrictions, see:
 ///     http://cprover.diffblue.com/md__home_travis_build_diffblue_cbmc_doc_architectural_restrict-function-pointer.html
-use crate::GotocCtx;
+use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{Stmt, Type};
 use cbmc::InternedString;
 use kani_restrictions::{CallSite, PossibleMethodEntry, TraitDefinedMethod, VtableCtxResults};
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/mod.rs b/src/kani-compiler/src/codegen_cprover_gotoc/mod.rs
@@ -0,0 +1,11 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+mod codegen;
+mod compiler_interface;
+mod context;
+mod overrides;
+mod utils;
+
+pub use compiler_interface::GotocCodegenBackend;
+pub use context::GotocCtx;
+pub use context::VtableCtx;
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/src/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
@@ -8,8 +8,8 @@
 //! It would be too nasty if we spread around these sort of undocumented hooks in place, so
 //! this module addresses this issue.
 
-use crate::utils;
-use crate::GotocCtx;
+use crate::codegen_cprover_gotoc::utils;
+use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Symbol, Type};
 use cbmc::NO_PRETTY_NAME;
 use kani_queries::UserInput;
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/overrides/mod.rs b/src/kani-compiler/src/codegen_cprover_gotoc/overrides/mod.rs
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs b/src/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs
@@ -3,7 +3,7 @@
 
 //! This file contains functionality that makes Kani easier to debug
 
-use crate::GotocCtx;
+use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Location;
 use rustc_middle::mir::Body;
 use rustc_middle::ty::print::with_no_trimmed_paths;
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/utils/mod.rs b/src/kani-compiler/src/codegen_cprover_gotoc/utils/mod.rs
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/src/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
@@ -3,7 +3,7 @@
 
 //! Functions that make names for things
 
-use crate::GotocCtx;
+use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::InternedString;
 use rustc_hir::def_id::DefId;
 use rustc_hir::def_id::LOCAL_CRATE;
diff --git a/src/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs b/src/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
@@ -1,7 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 use super::super::codegen::TypeExt;
-use crate::GotocCtx;
+use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::btree_string_map;
 use cbmc::goto_program::{Expr, ExprValue, Location, Stmt, SymbolTable, Type};
 use rustc_middle::ty::layout::LayoutOf;
diff --git a/src/kani-compiler/src/main.rs b/src/kani-compiler/src/main.rs
@@ -7,11 +7,35 @@
 //! Like miri, clippy, and other tools developed on the top of rustc, we rely on the
 //! rustc_private feature and a specific version of rustc.
 
-#![feature(rustc_private, once_cell)]
+#![feature(bool_to_option)]
+#![feature(crate_visibility_modifier)]
+#![feature(extern_types)]
+#![feature(in_band_lifetimes)]
+#![feature(nll)]
+#![recursion_limit = "256"]
+#![feature(box_patterns)]
+#![feature(once_cell)]
+#![feature(rustc_private)]
+extern crate rustc_arena;
+extern crate rustc_ast;
+extern crate rustc_attr;
 extern crate rustc_codegen_ssa;
+extern crate rustc_data_structures;
 extern crate rustc_driver;
+extern crate rustc_errors;
+extern crate rustc_fs_util;
+extern crate rustc_hir;
+extern crate rustc_index;
+extern crate rustc_llvm;
+extern crate rustc_metadata;
+extern crate rustc_middle;
+extern crate rustc_serialize;
 extern crate rustc_session;
+extern crate rustc_span;
+extern crate rustc_target;
 
+#[cfg(feature = "cprover")]
+mod codegen_cprover_gotoc;
 mod parser;
 mod session;
 
@@ -83,9 +107,14 @@ fn main() -> Result<(), &'static str> {
     let mut callbacks = KaniCallbacks {};
     let mut compiler = RunCompiler::new(&rustc_args, &mut callbacks);
     if matches.is_present("goto-c") {
-        compiler.set_make_codegen_backend(Some(Box::new(move |_cfg| {
-            rustc_codegen_kani::GotocCodegenBackend::new(&Rc::new(queries))
-        })));
+        if cfg!(feature = "cprover") {
+            compiler.set_make_codegen_backend(Some(Box::new(move |_cfg| {
+                codegen_cprover_gotoc::GotocCodegenBackend::new(&Rc::new(queries))
+            })));
+        } else {
+            return Err("Kani was configured without 'cprover' feature. You must enable this \
+            feature in order to use --goto-c argument.");
+        }
     }
     compiler.run().or(Err("Failed to compile crate."))
 }
