Introduce prototype cargo-kani assess feature to help find places to start writing proofs (rust-lang#1756)

Author: tedinski

Cargo.lock

@@ -190,6 +190,18 @@ dependencies = [
  "os_str_bytes",
 ]
 
+[[package]]
+name = "comfy-table"
+version = "6.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "121d8a5b0346092c18a4b2fd6f620d7a06f0eb7ac0a45860939a0884bc579c56"
+dependencies = [
+ "crossterm",
+ "strum",
+ "strum_macros",
+ "unicode-width",
+]
+
 [[package]]
 name = "compiletest"
 version = "0.0.0"
@@ -265,26 +277,49 @@ dependencies = [
 
 [[package]]
 name = "crossbeam-epoch"
-version = "0.9.10"
+version = "0.9.11"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "045ebe27666471bb549370b4b0b3e51b07f56325befa4284db65fc89c02511b1"
+checksum = "f916dfc5d356b0ed9dae65f1db9fc9770aa2851d2662b988ccf4fe3516e86348"
 dependencies = [
  "autocfg",
  "cfg-if",
  "crossbeam-utils",
  "memoffset",
- "once_cell",
  "scopeguard",
 ]
 
 [[package]]
 name = "crossbeam-utils"
-version = "0.8.11"
+version = "0.8.12"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "51887d4adc7b564537b15adcfb307936f8075dfcd5f00dde9a9f1d29383682bc"
+checksum = "edbafec5fa1f196ca66527c1b12c2ec4745ca14b50f1ad8f9f6f720b55d11fac"
 dependencies = [
  "cfg-if",
- "once_cell",
+]
+
+[[package]]
+name = "crossterm"
+version = "0.23.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a2102ea4f781910f8a5b98dd061f4c2023f479ce7bb1236330099ceb5a93cf17"
+dependencies = [
+ "bitflags",
+ "crossterm_winapi",
+ "libc",
+ "mio",
+ "parking_lot",
+ "signal-hook",
+ "signal-hook-mio",
+ "winapi",
+]
+
+[[package]]
+name = "crossterm_winapi"
+version = "0.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2ae1b35a484aa10e07fe0638d02301c5ad24de82d310ccbd2f3693da5f09bf1c"
+dependencies = [
+ "winapi",
 ]
 
 [[package]]
@@ -432,6 +467,7 @@ dependencies = [
  "anyhow",
  "cargo_metadata",
  "clap 2.34.0",
+ "comfy-table",
  "console",
  "glob",
  "kani_metadata",
@@ -545,6 +581,18 @@ dependencies = [
  "autocfg",
 ]
 
+[[package]]
+name = "mio"
+version = "0.8.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "57ee1c23c7c63b0c9250c339ffdc69255f110b298b901b9f6c82547b7b87caaf"
+dependencies = [
+ "libc",
+ "log",
+ "wasi",
+ "windows-sys",
+]
+
 [[package]]
 name = "num"
 version = "0.4.0"
@@ -916,6 +964,36 @@ version = "1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "24188a676b6ae68c3b2cb3a01be17fbf7240ce009799bb56d5b1409051e78fde"
 
+[[package]]
+name = "signal-hook"
+version = "0.3.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a253b5e89e2698464fc26b545c9edceb338e18a89effeeecfea192c3025be29d"
+dependencies = [
+ "libc",
+ "signal-hook-registry",
+]
+
+[[package]]
+name = "signal-hook-mio"
+version = "0.2.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "29ad2e15f37ec9a6cc544097b78a1ec90001e9f71b81338ca39f430adaca99af"
+dependencies = [
+ "libc",
+ "mio",
+ "signal-hook",
+]
+
+[[package]]
+name = "signal-hook-registry"
+version = "1.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e51e73328dc4ac0c7ccbda3a494dfa03df1de2f46018127f60c693f2648455b0"
+dependencies = [
+ "libc",
+]
+
 [[package]]
 name = "smallvec"
 version = "1.9.0"

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -123,6 +123,7 @@ impl<'tcx> GotocCtx<'tcx> {
             self.symbol_table.update_fn_declaration_with_definition(&name, body);
 
             self.handle_kanitool_attributes();
+            self.record_test_harness_metadata();
         }
         self.reset_current_fn();
     }
@@ -316,12 +317,53 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
+    /// We record test harness information in kani-metadata, just like we record
+    /// proof harness information. This is used to support e.g. cargo-kani assess.
+    ///
+    /// Note that we do not actually spot the function that was annotated by `#[test]`
+    /// but instead the closure that gets put into the "test description" that macro
+    /// expands into. (See comment below) This ends up being preferrable, actually,
+    /// as it add asserts for tests that return `Result` types.
+    fn record_test_harness_metadata(&mut self) {
+        let def_id = self.current_fn().instance().def_id();
+        if def_id.is_local() {
+            let local_def_id = def_id.expect_local();
+            let hir_id = self.tcx.hir().local_def_id_to_hir_id(local_def_id);
+
+            // We want to detect the case where we're codegen'ing the closure inside what test "descriptions"
+            // are macro-expanded to:
+            //
+            // #[rustc_test_marker]
+            // pub const check_2: test::TestDescAndFn = test::TestDescAndFn {
+            //     desc: ...,
+            //     testfn: test::StaticTestFn(|| test::assert_test_result(check_2())),
+            // };
+
+            // The parent item of the closure appears to reliably be the `const` declaration item.
+            let parent_id = self.tcx.hir().get_parent_item(hir_id);
+            let attrs = self.tcx.get_attrs_unchecked(parent_id.to_def_id());
+
+            if self.tcx.sess.contains_name(attrs, rustc_span::symbol::sym::rustc_test_marker) {
+                let loc = self.codegen_span(&self.current_fn().mir().span);
+                self.test_harnesses.push(HarnessMetadata {
+                    pretty_name: self.current_fn().readable_name().to_owned(),
+                    mangled_name: self.current_fn().name(),
+                    original_file: loc.filename().unwrap(),
+                    original_start_line: loc.start_line().unwrap() as usize,
+                    original_end_line: loc.end_line().unwrap() as usize,
+                    unwind_value: None,
+                })
+            }
+        }
+    }
+
     /// This updates the goto context with any information that should be accumulated from a function's
     /// attributes.
     ///
     /// Handle all attributes i.e. `#[kani::x]` (which kani_macros translates to `#[kanitool::x]` for us to handle here)
     fn handle_kanitool_attributes(&mut self) {
-        let all_attributes = self.tcx.get_attrs_unchecked(self.current_fn().instance().def_id());
+        let def_id = self.current_fn().instance().def_id();
+        let all_attributes = self.tcx.get_attrs_unchecked(def_id);
         let (proof_attributes, other_attributes) = partition_kanitool_attributes(all_attributes);
         if !proof_attributes.is_empty() {
             self.create_proof_harness(other_attributes);

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -129,6 +129,8 @@ impl CodegenBackend for GotocCodegenBackend {
         // Print compilation report.
         print_report(&gcx, tcx);
 
+        let unsupported_features = gcx.unsupported_metadata();
+
         // perform post-processing symbol table passes
         let passes = self.queries.get_symbol_table_passes();
         let symtab = symtab_transformer::do_passes(gcx.symbol_table, &passes);
@@ -144,7 +146,11 @@ impl CodegenBackend for GotocCodegenBackend {
             None
         };
 
-        let metadata = KaniMetadata { proof_harnesses: gcx.proof_harnesses };
+        let metadata = KaniMetadata {
+            proof_harnesses: gcx.proof_harnesses,
+            unsupported_features,
+            test_harnesses: gcx.test_harnesses,
+        };
 
         // No output should be generated if user selected no_codegen.
         if !tcx.sess.opts.unstable_opts.no_codegen && tcx.sess.opts.output_types.should_codegen() {

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -21,7 +21,7 @@ use cbmc::goto_program::{DatatypeComponent, Expr, Location, Stmt, Symbol, Symbol
 use cbmc::utils::aggr_tag;
 use cbmc::InternedString;
 use cbmc::{MachineModel, RoundingMode};
-use kani_metadata::HarnessMetadata;
+use kani_metadata::{HarnessMetadata, UnsupportedFeature};
 use kani_queries::{QueryDb, UserInput};
 use rustc_data_structures::fx::FxHashMap;
 use rustc_data_structures::owning_ref::OwningRef;
@@ -59,6 +59,7 @@ pub struct GotocCtx<'tcx> {
     pub current_fn: Option<CurrentFnCtx<'tcx>>,
     pub type_map: FxHashMap<InternedString, Ty<'tcx>>,
     pub proof_harnesses: Vec<HarnessMetadata>,
+    pub test_harnesses: Vec<HarnessMetadata>,
     /// a global counter for generating unique IDs for checks
     pub global_checks_count: u64,
     /// A map of unsupported constructs that were found while codegen
@@ -84,6 +85,7 @@ impl<'tcx> GotocCtx<'tcx> {
             current_fn: None,
             type_map: FxHashMap::default(),
             proof_harnesses: vec![],
+            test_harnesses: vec![],
             global_checks_count: 0,
             unsupported_constructs: FxHashMap::default(),
         }
@@ -99,6 +101,32 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn current_fn_mut(&mut self) -> &mut CurrentFnCtx<'tcx> {
         self.current_fn.as_mut().unwrap()
     }
+
+    /// Maps the goto-context "unsupported features" data into the
+    /// KaniMetadata "unsupported features" format.
+    ///
+    /// These are different because the KaniMetadata is a flat serializable list,
+    /// while we need a more richly structured HashMap in the goto context.
+    pub(crate) fn unsupported_metadata(&self) -> Vec<UnsupportedFeature> {
+        self.unsupported_constructs
+            .iter()
+            .map(|(construct, location)| UnsupportedFeature {
+                feature: construct.to_string(),
+                locations: location
+                    .iter()
+                    .map(|l| {
+                        // We likely (and should) have no instances of
+                        // calling `codegen_unimplemented` without file/line.
+                        // So while we map out of `Option` here, we expect them to always be `Some`
+                        (
+                            l.filename().unwrap_or_default(),
+                            l.start_line().map(|x| x.to_string()).unwrap_or_default(),
+                        )
+                    })
+                    .collect(),
+            })
+            .collect()
+    }
 }
 
 /// Generate variables

kani-driver/Cargo.toml

@@ -31,6 +31,7 @@ regex = "1.6"
 rustc-demangle = "0.1.21"
 pathdiff = "0.2.1"
 rayon = "1.5.3"
+comfy-table = "6.0.0"
 
 # A good set of suggested dependencies can be found in rustup:
 # https://github.com/rust-lang/rustup/blob/master/Cargo.toml

kani-driver/src/args.rs

@@ -35,14 +35,29 @@ pub struct StandaloneArgs {
     setting = structopt::clap::AppSettings::AllArgsOverrideSelf
 )]
 pub struct CargoKaniArgs {
+    #[structopt(subcommand)]
+    pub command: Option<CargoKaniSubcommand>,
+
     #[structopt(flatten)]
     pub common_opts: KaniArgs,
 }
 
+// cargo-kani takes optional subcommands to request specialized behavior
+#[derive(Debug, StructOpt)]
+pub enum CargoKaniSubcommand {
+    #[structopt(setting(structopt::clap::AppSettings::Hidden))]
+    Assess,
+}
+
 // Common arguments for invoking Kani. This gets put into KaniContext, whereas
 // anything above is "local" to "main"'s control flow.
 #[derive(Debug, StructOpt)]
 pub struct KaniArgs {
+    /// Temporary option to trigger assess mode for out test suite
+    /// where we are able to add options but not subcommands
+    #[structopt(long, hidden = true, requires("enable-unstable"))]
+    pub assess: bool,
+
     /// Generate visualizer report to <target-dir>/report/html/index.html
     #[structopt(long)]
     pub visualize: bool,