Add cargo-saw-build and saw-rustc commands

Cargo.toml

@@ -23,6 +23,13 @@ path = "src/bin/wrapper.rs"
 name = "cargo-crux-test_real"
 path = "src/bin/cargo-crux-test.rs"
 
+[[bin]]
+name = "cargo-saw-build"
+path = "src/bin/wrapper.rs"
+[[bin]]
+name = "cargo-saw-build_real"
+path = "src/bin/cargo-saw-build.rs"
+
 [[bin]]
 name = "cargo-mir-json"
 path = "src/bin/wrapper.rs"
@@ -64,3 +71,10 @@ path = "src/bin/wrapper.rs"
 [[bin]]
 name = "mir-json_real"
 path = "src/bin/mir-json.rs"
+
+[[bin]]
+name = "saw-rustc"
+path = "src/bin/wrapper.rs"
+[[bin]]
+name = "saw-rustc_real"
+path = "src/bin/saw-rustc.rs"

README.md

@@ -1,5 +1,5 @@
-`mir-json` provides `rustc` and `cargo` integration for
-[mir-verifier][mir-verifier-repo].
+`mir-json` provides `rustc` and `cargo` integration for interfacing with
+[crux-mir][crux-mir-repo].
 
 ## Installation instructions
 
@@ -34,7 +34,7 @@ book](https://doc.rust-lang.org/book/2018-edition/ch01-01-installation.html)).
 
 ## Usage
 
-See the [mir-verifier][mir-verifier-repo] README for usage instructions.
+See the [crux-mir][crux-mir-repo] README for usage instructions.
 
 
-[mir-verifier-repo]: https://github.com/GaloisInc/mir-verifier
+[crux-mir-repo]: https://github.com/GaloisInc/crucible/tree/master/crux-mir

doc/rustc.md

@@ -1,13 +1,17 @@
 # `rustc` integration in `crux-mir`
 
 `mir-json` (the component of `crux-mir` responsible for interfacing with
-`cargo` and `rustc`) consists of two main binaries:
+`cargo` and `rustc`) consists of three main binaries:
 
 * `cargo-crux-test`, a `cargo` subcommand, is the main user-facing entry point
   for `crux-mir`.
+* `cargo-saw-build`, a `cargo` subcommand, is the main user-facing entry point
+  for SAW's MIR verification support.
 * `mir-json-rustc-wrapper`, a `RUSTC_WRAPPER` binary, uses `rustc_interface` to
   invoke normal `rustc` compilation with some additional callbacks installed.
 
+## `cargo-crux-test`
+
 In general, `crux-mir` tries to reuse as much of the normal `cargo`
 functionality as possible.  `cargo-crux-test` makes some minor adjustments to
 the command line arguments, sets up some environment variables (notably
@@ -17,6 +21,16 @@ a special `RUSTC_WRAPPER`, it supports almost all the standard `cargo`
 features, such as `build.rs` files, dependencies on proc-macro crates, and test
 filtering flags like `--lib`/`--bin`.
 
+## `cargo-saw-build`
+
+`cargo-saw-build` is very similar in operation to `cargo-crux-test` in that
+both will compile Rust code into a MIR JSON file. The difference between
+`cargo-saw-build` and `cargo-crux-test` is that the former will stop after
+producing the JSON file, whereas the latter will proceed to run `crux-mir` on
+the JSON afterwards. The former is more useful for SAW's needs.
+
+## `mir-json-rustc-wrapper`
+
 `mir-json-rustc-wrapper` has three modes of operation:
 
 1. If it detects that it's being invoked to build a `cargo` "host" dependency,
@@ -39,6 +53,40 @@ filtering flags like `--lib`/`--bin`.
    all its dependencies, and replaces the test binary output with a script that
    invokes `crux-mir`'s symbolic execution backend on the linked `.mir`.
 
+`mir-json-rustc-wrapper`'s behavior is controlled by a variety of environment
+variables:
+
+* `CRUX_RUST_LIBRARY_PATH`: The path containing `.rlib` files for crate
+   dependencies.
+* `CRUX_USE_OVERRIDE_CRATES`: The list of crates for which `crucible-mir`
+   overrides should be used.
+* `EXPORT_ALL`: If this environment variable is set, then the MIR JSON file
+  will export all top-level functions. Otherwise, it will only export those
+  functions with a `#[crux_test]` attribute.
+
+## Other binaries
+
+Besides the main binaries above, `mir-json` also provides a variety of other
+binaries for specialized purposes:
+
+* `cargo-mir-json`: This invokes `cargo rustc`, but replacing `rustc` with
+  `mir-json`.
+* `crux-rustc`: A helper that invokes `mir-json-rustc-wrapper` the same way that
+  `cargo-crux-test` would run it. This is useful for testing a single file,
+  e.g., `crux-rustc --test foo.rs`.
+* `mir-json-callgraph`: This prints the reverse callgraph of a function, which
+  can be helpful for debugging.
+* `mir-json-dce`: This takes in several `.mir` files, combines them, and then
+  runs dead-code elimination on them. It is unlikely that you will need to use
+  this binary directly, as dead-code elimination is performed as an intermediate
+  step in other binaries.
+* `mir-json`: This produces a `.mir` file from a single `.rs` file and does not
+  do anything else, such as testing with `crux-mir`. It is unlikely that you
+  will need to use this binary directly, as producing `.mir` files is performed
+  as an intermediate step in other binaries.
+* `saw-rustc`: A helper that invokes `mir-json-rustc-wrapper` the same way that
+  `cargo-saw-build` would run it. This is useful for building a single file,
+  e.g., `saw-rustc foo.rs`.
 
 ## `TyCtxt` usage
 

src/analyz/mod.rs

@@ -66,7 +66,7 @@ impl<'tcx> ToJson<'tcx> for mir::AggregateKind<'tcx> {
             &mir::AggregateKind::Closure(_, _) => {
                 json!({
                     "kind": "Closure",
-                    // mir-verifier uses the same representation for closures as it does for
+                    // crucible-mir uses the same representation for closures as it does for
                     // tuples, so no additional information is needed.
                 })
             }
@@ -699,7 +699,7 @@ fn init_instances_from_mono_items(ms: &mut MirState) -> io::Result<()> {
 fn init_instances_from_tests(ms: &mut MirState, out: &mut impl JsonOutput) -> io::Result<()> {
     let tcx = ms.state.tcx;
     for &def_id in tcx.mir_keys(def_id::LOCAL_CRATE) {
-        if !has_test_attr(tcx, def_id) {
+        if ms.export_style == ExportStyle::ExportCruxTests && !has_test_attr(tcx, def_id) {
             continue;
         }
 
@@ -884,6 +884,7 @@ fn emit_fn<'tcx>(
         state: ms.state,
         tys: ms.tys,
         match_span_map: ms.match_span_map,
+        export_style: ms.export_style,
     };
     let ms = &mut ms;
 
@@ -945,6 +946,7 @@ pub struct AnalysisData<O> {
 fn analyze_inner<'tcx, O: JsonOutput, F: FnOnce(&Path) -> io::Result<O>>(
     sess: &Session,
     queries: &'tcx Queries<'tcx>,
+    export_style: ExportStyle,
     mk_output: F,
 ) -> Result<Option<AnalysisData<O>>, serde_cbor::Error> {
     let mut mir_path = None;
@@ -993,6 +995,7 @@ fn analyze_inner<'tcx, O: JsonOutput, F: FnOnce(&Path) -> io::Result<O>>(
             state: &state,
             tys: &mut tys,
             match_span_map: &get_match_spans(),
+            export_style: export_style,
         };
 
         // Traits and top-level statics can be enumerated directly.
@@ -1037,8 +1040,9 @@ fn analyze_inner<'tcx, O: JsonOutput, F: FnOnce(&Path) -> io::Result<O>>(
 pub fn analyze_nonstreaming<'tcx>(
     sess: &Session,
     queries: &'tcx Queries<'tcx>,
+    export_style: ExportStyle,
 ) -> Result<Option<AnalysisData<()>>, serde_cbor::Error> {
-    let opt_ad = analyze_inner(sess, queries, |_| { Ok(lib_util::Output::default()) })?;
+    let opt_ad = analyze_inner(sess, queries, export_style, |_| { Ok(lib_util::Output::default()) })?;
     let AnalysisData { mir_path, extern_mir_paths, output: out } = match opt_ad {
         Some(x) => x,
         None => return Ok(None),
@@ -1067,8 +1071,9 @@ pub fn analyze_nonstreaming<'tcx>(
 pub fn analyze_streaming<'tcx>(
     sess: &Session,
     queries: &'tcx Queries<'tcx>,
+    export_style: ExportStyle,
 ) -> Result<Option<AnalysisData<()>>, serde_cbor::Error> {
-    let opt_ad = analyze_inner(sess, queries, lib_util::start_streaming)?;
+    let opt_ad = analyze_inner(sess, queries, export_style, lib_util::start_streaming)?;
     let AnalysisData { mir_path, extern_mir_paths, output } = match opt_ad {
         Some(x) => x,
         None => return Ok(None),
@@ -1078,6 +1083,7 @@ pub fn analyze_streaming<'tcx>(
 }
 
 pub use self::analyze_streaming as analyze;
+pub use analyz::to_json::ExportStyle;
 
 fn make_attr(key: &str, value: &str) -> ast::Attribute {
     ast::Attribute {

src/analyz/to_json.rs

@@ -247,6 +247,21 @@ impl<'tcx> TyIntern<'tcx> {
     }
 }
 
+/// How many functions should be exported in the JSON output?
+#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)]
+pub enum ExportStyle {
+    /// Only export functions annotated with the `#[crux_test]` attribute.
+    ExportCruxTests,
+    /// Export all functions.
+    ExportAll
+}
+
+impl Default for ExportStyle {
+    fn default() -> Self {
+        ExportStyle::ExportCruxTests
+    }
+}
+
 pub struct MirState<'a, 'tcx : 'a> {
     pub mir: Option<&'tcx Body<'tcx>>,
     pub used: &'a mut Used<'tcx>,
@@ -263,6 +278,7 @@ pub struct MirState<'a, 'tcx : 'a> {
     /// rewritten.  This seems okay for now since the user is mostly interested in coverage in
     /// their own top-level crate anyway.
     pub match_span_map: &'a HashMap<Span, Span>,
+    pub export_style: ExportStyle,
 }
 
 /// Trait for converting MIR elements to JSON.

src/analyz/ty_json.rs

@@ -414,7 +414,7 @@ impl<'tcx> ToJson<'tcx> for ty::Ty<'tcx> {
                     "kind": "Closure",
                     "upvar_tys": substs.as_closure().upvar_tys(defid, mir.state.tcx)
                         .collect::<Vec<_>>().to_json(mir),
-                    // mir-verifier uses the same representation for closures as it does for
+                    // crucible-mir uses the same representation for closures as it does for
                     // tuples, so no additional information is needed.
                 })
             }
@@ -653,7 +653,7 @@ impl<'tcx> ToJson<'tcx> for ty::subst::GenericArg<'tcx> {
     fn to_json(&self, mir: &mut MirState<'_, 'tcx>) -> serde_json::Value {
         match self.unpack() {
             ty::subst::GenericArgKind::Type(ref ty) => ty.to_json(mir),
-            // In mir-verifier, all substs entries are considered "types", and there are dummy
+            // In crucible-mir, all substs entries are considered "types", and there are dummy
             // TyLifetime and TyConst variants to handle non-type entries.  We emit something that
             // looks vaguely like an interned type's ID here, and handle it specially in MIR.JSON.
             ty::subst::GenericArgKind::Lifetime(_) => json!("nonty::Lifetime"),