Perform reachability analysis on a per-harness basis (#2439)

Kani compiler used to generate one `goto-program` for all harnesses in one crate. In some cases, this actually had a negative impact on the harness verification time. This was first reported in #1659

The main changes were done in the compiler's module `compiler_interface` and the module `project` from the driver. The compiler will now gather all the harnesses beforehand and it will perform reachability + codegen steps for each harness. All files related to a harness `goto-program` will follow the naming convention bellow:
```
<BASE_NAME>_<MANGLED_NAME>.<EXTENSION>
```
This applies to symtab / goto / type_map / restriction files.

The metadata file is still generated once per target crate, and its name is still the same (`<BASE_NAME>.kani-metadata.json`).

On the driver side, the way we process the artifacts have changed. The driver will now read the metadata for each crate, and collect all artifacts based on the symtab goto file that is recorded in the metadata of each harness.

These changes do not apply for `--function`. We still keep all artifacts based on the crate's `<BASE_NAME>` and we have a separate logic to handle that. Fixing this is captured by #2129.

cprover_bindings/src/irep/goto_binary_serde.rs

@@ -9,7 +9,7 @@ use std::fs::File;
 use std::hash::Hash;
 use std::io::{self, BufReader};
 use std::io::{BufWriter, Bytes, Error, ErrorKind, Read, Write};
-use std::path::PathBuf;
+use std::path::Path;
 
 /// Writes a symbol table to a file in goto binary format in version 5.
 ///
@@ -18,7 +18,7 @@ use std::path::PathBuf;
 /// - src/util/irep_serialization.h
 /// - src/util/irep_hash_container.h
 /// - src/util/irep_hash.h
-pub fn write_goto_binary_file(filename: &PathBuf, source: &crate::goto_program::SymbolTable) {
+pub fn write_goto_binary_file(filename: &Path, source: &crate::goto_program::SymbolTable) {
     let out_file = File::create(filename).unwrap();
     let mut writer = BufWriter::new(out_file);
     let mut serializer = GotoBinarySerializer::new(&mut writer);
@@ -33,7 +33,7 @@ pub fn write_goto_binary_file(filename: &PathBuf, source: &crate::goto_program::
 /// - src/util/irep_serialization.h
 /// - src/util/irep_hash_container.h
 /// - src/util/irep_hash.h
-pub fn read_goto_binary_file(filename: &PathBuf) -> io::Result<()> {
+pub fn read_goto_binary_file(filename: &Path) -> io::Result<()> {
     let file = File::open(filename)?;
     let reader = BufReader::new(file);
     let mut deserializer = GotoBinaryDeserializer::new(reader);

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

@@ -4,10 +4,8 @@
 //! This file contains functions related to codegenning MIR functions into gotoc
 
 use crate::codegen_cprover_gotoc::GotocCtx;
-use crate::kani_middle::attributes::{extract_harness_attributes, is_test_harness_closure};
 use cbmc::goto_program::{Expr, Stmt, Symbol};
 use cbmc::InternString;
-use kani_metadata::{HarnessAttributes, HarnessMetadata};
 use rustc_middle::mir::traversal::reverse_postorder;
 use rustc_middle::mir::{Body, HasLocalDecls, Local};
 use rustc_middle::ty::{self, Instance};
@@ -89,9 +87,6 @@ impl<'tcx> GotocCtx<'tcx> {
             let stmts = self.current_fn_mut().extract_block();
             let body = Stmt::block(stmts, loc);
             self.symbol_table.update_fn_declaration_with_definition(&name, body);
-
-            self.record_kani_attributes();
-            self.record_test_harness_metadata();
         }
         self.reset_current_fn();
     }
@@ -244,50 +239,4 @@ impl<'tcx> GotocCtx<'tcx> {
         });
         self.reset_current_fn();
     }
-
-    /// 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 is_test_harness_closure(self.tcx, def_id) {
-            self.test_harnesses.push(self.generate_metadata(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 record_kani_attributes(&mut self) {
-        let def_id = self.current_fn().instance().def_id();
-        let attributes = extract_harness_attributes(self.tcx, def_id);
-        if attributes.is_some() {
-            self.proof_harnesses.push(self.generate_metadata(attributes));
-        }
-    }
-
-    /// Create the default proof harness for the current function
-    fn generate_metadata(&self, attributes: Option<HarnessAttributes>) -> HarnessMetadata {
-        let current_fn = self.current_fn();
-        let pretty_name = current_fn.readable_name().to_owned();
-        let mangled_name = current_fn.name();
-        let loc = self.codegen_span(&current_fn.mir().span);
-
-        HarnessMetadata {
-            pretty_name,
-            mangled_name,
-            crate_name: current_fn.krate(),
-            original_file: loc.filename().unwrap(),
-            original_start_line: loc.start_line().unwrap() as usize,
-            original_end_line: loc.end_line().unwrap() as usize,
-            attributes: attributes.unwrap_or_default(),
-            // We record the actual path after codegen before we dump the metadata into a file.
-            goto_file: None,
-        }
-    }
 }

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

@@ -3,32 +3,21 @@
 
 //! MIR Span related functions
 
-use crate::codegen_cprover_gotoc::GotocCtx;
+use crate::{codegen_cprover_gotoc::GotocCtx, kani_middle::SourceLocation};
 use cbmc::goto_program::Location;
 use rustc_middle::mir::{Local, VarDebugInfo, VarDebugInfoContents};
 use rustc_span::Span;
 
 impl<'tcx> GotocCtx<'tcx> {
     pub fn codegen_span(&self, sp: &Span) -> Location {
-        let smap = self.tcx.sess.source_map();
-        let lo = smap.lookup_char_pos(sp.lo());
-        let start_line = lo.line;
-        let start_col = 1 + lo.col_display;
-        let hi = smap.lookup_char_pos(sp.hi());
-        let end_line = hi.line;
-        let end_col = 1 + hi.col_display;
-        let filename0 = lo.file.name.prefer_local().to_string_lossy().to_string();
-        let filename1 = match std::fs::canonicalize(filename0.clone()) {
-            Ok(pathbuf) => pathbuf.to_str().unwrap().to_string(),
-            Err(_) => filename0,
-        };
+        let loc = SourceLocation::new(self.tcx, sp);
         Location::new(
-            filename1,
+            loc.filename,
             self.current_fn.as_ref().map(|x| x.readable_name().to_string()),
-            start_line,
-            Some(start_col),
-            end_line,
-            Some(end_col),
+            loc.start_line,
+            Some(loc.start_col),
+            loc.end_line,
+            Some(loc.end_col),
         )
     }