Merge branch 'master' into rustup-2023-01-23

Cargo.toml

@@ -26,6 +26,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"
@@ -67,3 +74,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

@@ -65,7 +65,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.
  })
  }
@@ -796,7 +796,7 @@ fn init_instances_from_tests(ms: &mut MirState, out: &mut impl JsonOutput) -> io
  let tcx = ms.state.tcx;
  for &local_def_id in tcx.mir_keys(()) {
  let def_id = local_def_id.to_def_id();
- if !has_test_attr(tcx, def_id) {
+ if ms.export_style == ExportStyle::ExportCruxTests && !has_test_attr(tcx, def_id) {
  continue;
  }
 
@@ -988,6 +988,7 @@ fn emit_fn<'tcx>(
  tys: ms.tys,
  match_span_map: ms.match_span_map,
  allocs: ms.allocs,
+ export_style: ms.export_style,
  };
  let ms = &mut ms;
 
@@ -1053,6 +1054,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;
@@ -1103,6 +1105,7 @@ fn analyze_inner<'tcx, O: JsonOutput, F: FnOnce(&Path) -> io::Result<O>>(
  tys: &mut tys,
  match_span_map: &get_match_spans(),
  allocs: &mut allocs,
+ export_style: export_style,
  };
 
  // Traits and top-level statics can be enumerated directly.
@@ -1147,8 +1150,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),
@@ -1177,8 +1181,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),
@@ -1188,6 +1193,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

@@ -269,6 +269,20 @@ 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
+ }
+}
 
 #[derive(Default, Debug)]
 pub struct AllocIntern<'tcx> {
@@ -318,6 +332,7 @@ pub struct MirState<'a, 'tcx : 'a> {
  /// their own top-level crate anyway.
  pub match_span_map: &'a HashMap<Span, Span>,
  pub allocs: &'a mut AllocIntern<'tcx>,
+ pub export_style: ExportStyle,
 }
 
 /// Trait for converting MIR elements to JSON.

src/analyz/ty_json.rs

@@ -419,7 +419,7 @@ impl<'tcx> ToJson<'tcx> for ty::Ty<'tcx> {
  "kind": "Closure",
  "upvar_tys": substs.as_closure().upvar_tys()
  .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.
  })
  }
@@ -647,7 +647,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"),