Perform reachability analysis on a per-harness basis

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),
         )
     }