Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/main' into issue-2383-toolchain
Browse files Browse the repository at this point in the history 
Conflicts:
    kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
    kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

Required change:
    kani-compiler/src/kani_middle/attributes.rs
  • Loading branch information
@celinval
celinval committed May 16, 2023
2 parents bf99cf0 + 2a09d79 commit 67c7f3c
Show file tree
Hide file tree
Showing 22 changed files with 738 additions and 546 deletions.
60 changes: 30 additions & 30 deletions Cargo.lock
View file
Original file line number Diff line number Diff line change
Expand Up @@ -196,9 +196,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"

[[package]]
name = "clap"
version = "4.2.5"
version = "4.2.7"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "8a1f23fa97e1d1641371b51f35535cb26959b8e27ab50d167a8b996b5bada819"
checksum = "34d21f9bf1b425d2968943631ec91202fe5e837264063503708b83013f8fc938"
dependencies = [
"clap_builder",
"clap_derive",
Expand All @@ -207,9 +207,9 @@ dependencies = [

[[package]]
name = "clap_builder"
version = "4.2.5"
version = "4.2.7"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0fdc5d93c358224b4d6867ef1356d740de2303e9892edc06c5340daeccd96bab"
checksum = "914c8c79fb560f238ef6429439a30023c862f7a28e688c58f7203f12b29970bd"
dependencies = [
"anstream",
"anstyle",
Expand All @@ -228,7 +228,7 @@ dependencies = [
"heck",
"proc-macro2",
"quote",
"syn 2.0.15",
"syn 2.0.16",
]

[[package]]
Expand Down Expand Up @@ -656,9 +656,9 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646"

[[package]]
name = "libc"
version = "0.2.142"
version = "0.2.144"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6a987beff54b60ffa6d51982e1aa1146bc42f19bd26be28b0586f252fccf5317"
checksum = "2b00cc1c228a6782d0f076e7b232802e0c5689d41bb5df366f2a6b6621cfdfe1"

[[package]]
name = "linear-map"
Expand All @@ -672,9 +672,9 @@ dependencies = [

[[package]]
name = "linux-raw-sys"
version = "0.3.6"
version = "0.3.7"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b64f40e5e03e0d54f03845c8197d0291253cdbedfb1cb46b13c2c117554a9f4c"
checksum = "ece97ea872ece730aed82664c424eb4c8291e1ff2480247ccf7409044bc6479f"

[[package]]
name = "lock_api"
Expand Down Expand Up @@ -934,9 +934,9 @@ dependencies = [

[[package]]
name = "proc-macro2"
version = "1.0.56"
version = "1.0.57"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "2b63bdb0cd06f1f4dedf69b254734f9b45af66e4a031e42a7480257d9898b435"
checksum = "c4ec6d5fe0b140acb27c9a0444118cf55bfbb4e0b259739429abb4521dd67c16"
dependencies = [
"unicode-ident",
]
Expand All @@ -954,9 +954,9 @@ dependencies = [

[[package]]
name = "quote"
version = "1.0.26"
version = "1.0.27"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "4424af4bf778aae2051a77b60283332f386554255d722233d09fbfc7e30da2fc"
checksum = "8f4f29d145265ec1c483c7c654450edde0bfe043d3938d6972630663356d9500"
dependencies = [
"proc-macro2",
]
Expand Down Expand Up @@ -1069,9 +1069,9 @@ dependencies = [

[[package]]
name = "rustix"
version = "0.37.18"
version = "0.37.19"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "8bbfc1d1c7c40c01715f47d71444744a81669ca84e8b63e25a55e169b1f86433"
checksum = "acf8729d8542766f1b2cf77eb034d52f40d375bb8b615d0b147089946e16613d"
dependencies = [
"bitflags",
"errno",
Expand Down Expand Up @@ -1119,22 +1119,22 @@ dependencies = [

[[package]]
name = "serde"
version = "1.0.160"
version = "1.0.163"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "bb2f3770c8bce3bcda7e149193a069a0f4365bda1fa5cd88e03bca26afc1216c"
checksum = "2113ab51b87a539ae008b5c6c02dc020ffa39afd2d83cffcb3f4eb2722cebec2"
dependencies = [
"serde_derive",
]

[[package]]
name = "serde_derive"
version = "1.0.160"
version = "1.0.163"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "291a097c63d8497e00160b166a967a4a79c64f3facdd01cbd7502231688d77df"
checksum = "8c805777e3930c8883389c602315a24224bcc738b63905ef87cd1420353ea93e"
dependencies = [
"proc-macro2",
"quote",
"syn 2.0.15",
"syn 2.0.16",
]

[[package]]
Expand All @@ -1159,9 +1159,9 @@ dependencies = [

[[package]]
name = "serde_test"
version = "1.0.160"
version = "1.0.163"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3c95a500e3923258f7fc3a16bf29934e403aef5ca1096e184d85e3b1926675e8"
checksum = "100168a8017b89fd4bcbeb8d857d95a8cfcbde829a7147c09cc82d3ab8d8cb41"
dependencies = [
"serde",
]
Expand Down Expand Up @@ -1286,9 +1286,9 @@ dependencies = [

[[package]]
name = "syn"
version = "2.0.15"
version = "2.0.16"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "a34fcf3e8b60f57e6a14301a2e916d323af98b0ea63c599441eec8558660c822"
checksum = "a6f671d4b5ffdb8eadec19c0ae67fe2639df8684bd7bc4b83d986b8db549cf01"
dependencies = [
"proc-macro2",
"quote",
Expand All @@ -1312,7 +1312,7 @@ checksum = "f9456a42c5b0d803c8cd86e73dd7cc9edd429499f37a3550d286d5e86720569f"
dependencies = [
"proc-macro2",
"quote",
"syn 2.0.15",
"syn 2.0.16",
]

[[package]]
Expand Down Expand Up @@ -1379,14 +1379,14 @@ checksum = "0f57e3ca2a01450b1a921183a9c9cbfda207fd822cef4ccb00a65402cbba7a74"
dependencies = [
"proc-macro2",
"quote",
"syn 2.0.15",
"syn 2.0.16",
]

[[package]]
name = "tracing-core"
version = "0.1.30"
version = "0.1.31"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "24eb03ba0eab1fd845050058ce5e616558e8f8d8fca633e6b163fe25c797213a"
checksum = "0955b8137a1df6f1a2e9a37d8a6656291ff0297c1a97c24e0d8425fe2312f79a"
dependencies = [
"once_cell",
"valuable",
Expand Down Expand Up @@ -1709,9 +1709,9 @@ checksum = "1a515f5799fe4961cb532f983ce2b23082366b898e52ffbce459c86f67c8378a"

[[package]]
name = "winnow"
version = "0.4.4"
version = "0.4.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "5617da7e1f97bf363947d767b91aaf3c2bbc19db7fda9c65af1278713d58e0a2"
checksum = "61de7bac303dc551fe038e2b3cef0f571087a47571ea6e79a87692ac99b99699"
dependencies = [
"memchr",
]
6 changes: 3 additions & 3 deletions cprover_bindings/src/irep/goto_binary_serde.rs
View file
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
View file
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
View file
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

0 comments on commit 67c7f3c

Please sign in to comment.