Make kani-verifier the root crate (rust-lang#1085)

* Make kani-verifier the root crate

* clean up after cbmc install

Author: tedinski

.github/workflows/kani.yml

@@ -21,7 +21,7 @@ jobs:
       - name: Build Kani
         run: |
           export RUST_BACKTRACE=1
-          cargo build
+          cargo build --workspace
 
       - name: Execute Kani regression
         run: ./scripts/kani-regression.sh
@@ -42,7 +42,7 @@ jobs:
       - name: Build Kani
         run: |
           export RUST_BACKTRACE=1
-          cargo build
+          cargo build --workspace
 
       - name: Install book runner dependencies
         run: ./scripts/setup/install_bookrunner_deps.sh

Cargo.toml

@@ -1,17 +1,47 @@
 # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
+[package]
+name = "kani-verifier"
+version = "0.1.0"
+edition = "2021"
+description = "A bit-precise model checker for Rust."
+readme = "README.md"
+keywords = ["model-checking", "verification"]
+categories = ["development-tools"]
+license = "MIT OR Apache-2.0"
+repository = "https://github.com/model-checking/kani"
+documentation = "https://model-checking.github.io/kani/"
+homepage = "https://github.com/model-checking/kani"
+
+[dependencies]
+anyhow = "1"
+home = "0.5"
+
+[[bin]]
+name = "kani"
+path = "src/bin/kani.rs"
+
+[[bin]]
+name = "cargo-kani"
+path = "src/bin/cargo_kani.rs"
+
+[profile.release]
+strip = "debuginfo"
+
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
 [workspace]
 members = [
   "library/kani",
   "library/std",
   "tools/bookrunner",
   "tools/compiletest",
   "tools/make-kani-release",
-  "src/kani-verifier",
-  "src/kani-driver",
-  "src/kani-compiler",
-  "src/kani_metadata",
+  "kani-driver",
+  "kani-compiler",
+  "kani_metadata",
   # `librustdoc` is still needed by bookrunner.
   "tools/bookrunner/librustdoc",
 ]

src/kani-driver/build.rs renamed to build.rs

@@ -10,7 +10,7 @@ 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 }
+cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = true }
 clap = "2.33.0"
 kani_queries = {path = "kani_queries"}
 kani_metadata = { path = "../kani_metadata", optional = true }

docs/src/cheat-sheets.md

@@ -19,7 +19,7 @@ macro_rules! path_str {
 
 /// Build the target library, and setup cargo to rerun them if the source has changed.
 fn setup_lib(out_dir: &str, lib_out: &str, lib: &str) {
-    let kani_lib = vec!["..", "..", "library", lib];
+    let kani_lib = vec!["..", "library", lib];
     println!("cargo:rerun-if-changed={}", path_str!(kani_lib));
 
     let mut kani_lib_toml = kani_lib;
@@ -35,7 +35,14 @@ fn setup_lib(out_dir: &str, lib_out: &str, lib: &str) {
         "--target-dir",
         &out_dir,
     ];
-    Command::new("cargo").env("CARGO_ENCODED_RUSTFLAGS", "--cfg=kani").args(args).status().unwrap();
+    let result = Command::new("cargo")
+        .env("CARGO_ENCODED_RUSTFLAGS", "--cfg=kani")
+        .args(args)
+        .status()
+        .unwrap();
+    if !result.success() {
+        std::process::exit(1);
+    }
 }
 
 /// Configure the compiler to build kani-compiler binary. We currently support building

src/kani-compiler/Cargo.lock renamed to kani-compiler/Cargo.lock

@@ -10,4 +10,4 @@ edition = "2021"
 
 [dependencies]
 serde = {version = "1", features = ["derive"]}
-cbmc = { path = "../../cprover_bindings", package = "cprover_bindings" }
+cbmc = { path = "../cprover_bindings", package = "cprover_bindings" }

src/kani-compiler/Cargo.toml renamed to kani-compiler/Cargo.toml

@@ -29,7 +29,7 @@ ${SCRIPT_DIR}/kani-fmt.sh --check
 PYTHONPATH=${SCRIPT_DIR} python3 -m unittest ${SCRIPT_DIR}/test_cbmc_json_parser.py
 
 # Build all packages in the workspace
-cargo build
+cargo build --workspace
 
 # Unit tests
 cargo test -p cprover_bindings

src/kani-compiler/README.md renamed to kani-compiler/README.md

@@ -15,3 +15,6 @@ wget -O "$FILE" "$URL"
 sudo dpkg -i "$FILE"
 
 cbmc --version
+
+# Clean up on success
+rm $FILE

src/kani-compiler/build.rs renamed to kani-compiler/build.rs

@@ -353,6 +353,10 @@ fn common_inputs_stamp() -> Stamp {
 
     // Add source, library and script directories
     stamp.add_dir(&rust_src_dir.join("src/"));
+    stamp.add_dir(&rust_src_dir.join("kani-compiler/"));
+    stamp.add_dir(&rust_src_dir.join("kani-driver/"));
+    stamp.add_dir(&rust_src_dir.join("kani_metadata/"));
+    stamp.add_dir(&rust_src_dir.join("cprover_bindings/"));
     stamp.add_dir(&rust_src_dir.join("library/"));
     stamp.add_dir(&rust_src_dir.join("scripts/"));
 

src/kani-compiler/kani_queries/Cargo.toml renamed to kani-compiler/kani_queries/Cargo.toml

@@ -46,8 +46,8 @@ fn parse_args() -> Result<String> {
 /// Ensures everything is good to go before we begin to build the release bundle.
 /// Notably, builds Kani in release mode.
 fn prebundle(dir: &Path) -> Result<()> {
-    if !Path::new("src/kani-compiler").exists() {
-        bail!("Run from project root directory. Couldn't find 'src/kani-compiler'.");
+    if !Path::new("kani-compiler").exists() {
+        bail!("Run from project root directory. Couldn't find 'kani-compiler'.");
     }
 
     if dir.exists() {
@@ -62,7 +62,7 @@ fn prebundle(dir: &Path) -> Result<()> {
     }
 
     // Before we begin, ensure Kani is built successfully in release mode.
-    Command::new("cargo").args(&["build", "--release"]).run()?;
+    Command::new("cargo").args(&["build", "--release", "--workspace"]).run()?;
 
     Ok(())
 }