Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Perform reachability analysis on a per-harness basis #2439

Merged
merged 8 commits into from
May 16, 2023
Merged
Show file tree
Hide file tree
Changes from 5 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions cprover_bindings/src/irep/goto_binary_serde.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
///
Expand All @@ -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);
Expand All @@ -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);
Expand Down
51 changes: 0 additions & 51 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down Expand Up @@ -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();
}
Expand Down Expand Up @@ -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,
}
}
}
25 changes: 7 additions & 18 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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),
)
}

Expand Down
Loading