From 5e7172b9f46dbbaea88bde936c2af0499a6f0753 Mon Sep 17 00:00:00 2001 From: Vytautas Astrauskas Date: Fri, 25 Jun 2021 18:30:31 +0200 Subject: [PATCH 1/2] Remove Polonius hack. --- Cargo.lock | 12 - .../definitely_initialized.rs | 39 +- prusti-interface/Cargo.toml | 1 - .../src/environment/borrowck/facts.rs | 415 +++--------------- .../src/environment/borrowck/regions.rs | 104 ++--- .../src/environment/dump_borrowck_info.rs | 49 ++- .../src/environment/mir_storage.rs | 51 +++ prusti-interface/src/environment/mod.rs | 55 ++- .../src/environment/polonius_info.rs | 197 ++++----- prusti-interface/src/environment/procedure.rs | 14 +- prusti-interface/src/lib.rs | 3 + prusti-interface/src/specs/mod.rs | 20 +- prusti-interface/src/specs/typed.rs | 72 +-- .../tests/verify/pass/arrays/static_const.rs | 11 + prusti-viper/src/encoder/borrows.rs | 13 +- prusti-viper/src/encoder/encoder.rs | 5 +- prusti-viper/src/encoder/loop_encoder.rs | 4 +- prusti-viper/src/encoder/procedure_encoder.rs | 33 +- .../src/encoder/spec_function_encoder.rs | 6 +- .../src/encoder/stub_procedure_encoder.rs | 4 +- prusti/src/callbacks.rs | 32 +- prusti/src/driver.rs | 17 +- rust-toolchain | 2 +- 23 files changed, 465 insertions(+), 694 deletions(-) create mode 100644 prusti-interface/src/environment/mir_storage.rs create mode 100644 prusti-tests/tests/verify/pass/arrays/static_const.rs diff --git a/Cargo.lock b/Cargo.lock index 90752776550..14a33f2c908 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1768,17 +1768,6 @@ version = "0.3.19" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3831453b3449ceb48b6d9c7ad7c96d5ea673e9b470a1dc578c2ce6521230884c" -[[package]] -name = "polonius-engine" -version = "0.12.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ef2558a4b464e185b36ee08a2937ebb62ea5464c38856cfb1465c97cb38db52d" -dependencies = [ - "datafrog", - "log 0.4.14", - "rustc-hash", -] - [[package]] name = "ppv-lite86" version = "0.2.10" @@ -1874,7 +1863,6 @@ dependencies = [ "datafrog", "lazy_static", "log 0.4.14", - "polonius-engine", "prusti-common", "prusti-specs", "prusti-utils", diff --git a/analysis/src/abstract_domains/definitely_initialized.rs b/analysis/src/abstract_domains/definitely_initialized.rs index 4255c695d7f..8b1d6ca8abe 100644 --- a/analysis/src/abstract_domains/definitely_initialized.rs +++ b/analysis/src/abstract_domains/definitely_initialized.rs @@ -40,24 +40,27 @@ impl<'a, 'tcx: 'a> fmt::Debug for DefinitelyInitializedState<'a, 'tcx> { impl<'a, 'tcx: 'a> PartialEq for DefinitelyInitializedState<'a, 'tcx> { fn eq(&self, other: &Self) -> bool { - debug_assert_eq!( - { - let mut stable_hasher = StableHasher::new(); - self.mir.hash_stable( - &mut self.tcx.get_stable_hashing_context(), - &mut stable_hasher, - ); - stable_hasher.finish::() - }, - { - let mut stable_hasher = StableHasher::new(); - other.mir.hash_stable( - &mut other.tcx.get_stable_hashing_context(), - &mut stable_hasher, - ); - stable_hasher.finish::() - }, - ); + // TODO: This assert is commented out because the stable hasher crashes + // on MIR that has region ids. + // + // debug_assert_eq!( + // { + // let mut stable_hasher = StableHasher::new(); + // self.mir.hash_stable( + // &mut self.tcx.get_stable_hashing_context(), + // &mut stable_hasher, + // ); + // stable_hasher.finish::() + // }, + // { + // let mut stable_hasher = StableHasher::new(); + // other.mir.hash_stable( + // &mut other.tcx.get_stable_hashing_context(), + // &mut stable_hasher, + // ); + // stable_hasher.finish::() + // }, + // ); self.def_init_places == other.def_init_places } } diff --git a/prusti-interface/Cargo.toml b/prusti-interface/Cargo.toml index da5ed9cf1e8..a5ad0cb4ce2 100644 --- a/prusti-interface/Cargo.toml +++ b/prusti-interface/Cargo.toml @@ -17,7 +17,6 @@ prusti-common = { path = "../prusti-common" } prusti-utils = { path = "../prusti-utils" } log = { version = "0.4", features = ["release_max_level_info"] } lazy_static = "1.4.0" -polonius-engine = "0.12.1" csv = "1" serde = { version = "1.0", features = ["derive"] } regex = "1.5" diff --git a/prusti-interface/src/environment/borrowck/facts.rs b/prusti-interface/src/environment/borrowck/facts.rs index 2f525819a26..a9d62675ef8 100644 --- a/prusti-interface/src/environment/borrowck/facts.rs +++ b/prusti-interface/src/environment/borrowck/facts.rs @@ -4,113 +4,47 @@ // License, v. 2.0. If a copy of the MPL was not distributed with this // file, You can obtain one at http://mozilla.org/MPL/2.0/. -/// Code for loading an manipulating Polonius facts. -/// -/// This code was adapted from the -/// [Polonius](https://github.com/rust-lang-nursery/polonius/blob/master/src/facts.rs) -/// source code. -use csv::ReaderBuilder; -use polonius_engine; -use prusti_common::vir::borrows::Borrow; -use regex::Regex; -use rustc_middle::mir; -// use rustc_data_structures::indexed_vec::Idx; -use rustc_index::vec::Idx; -use serde::de::DeserializeOwned; -use std::collections::HashMap; -use std::fmt; -use std::hash::Hash; -use std::path::Path; -use std::str::FromStr; -use serde::{Serialize, Deserialize}; - -/// Macro for declaring index types for referencing interned facts. -macro_rules! index_type { - ($typ:ident, $debug_str:ident) => { - #[derive(Ord, PartialOrd, Eq, PartialEq, Clone, Copy, Hash, Serialize, Deserialize)] - pub struct $typ(usize); - - impl From for $typ { - fn from(index: usize) -> $typ { - $typ { 0: index } - } - } - - impl Into for $typ { - fn into(self) -> usize { - self.0 as usize - } - } - - impl polonius_engine::Atom for $typ { - fn index(self) -> usize { - self.into() - } - } - - impl fmt::Debug for $typ { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - write!(f, "{}{}", stringify!($debug_str), self.0) - } - } - }; -} +use std::panic::Location; -index_type!(PointIndex, P); -// A unique identifier of a loan. -index_type!(Loan, L); -// A unique identifier of a region. -index_type!(Region, R); -// A unique identifier of a variable. -index_type!(Variable, V); -// A unique identifier of a path. -index_type!(Place, X); +use polonius_engine::FactTypes; +use rustc_mir::consumers::{RustcFacts, LocationTable, RichLocation}; +use rustc_middle::mir; +use std::rc::Rc; +use std::cell::RefCell; -pub fn loan_id(loan: Loan) -> usize { - loan.into() -} +pub type Region = ::Origin; +pub type Loan = ::Loan; +pub type PointIndex = ::Point; +pub type Variable = ::Variable; +pub type Path = ::Path; -impl Into for Loan { - fn into(self) -> Borrow { - self.0.into() - } -} +pub type AllInputFacts = rustc_mir::consumers::PoloniusInput; +pub type AllOutputFacts = rustc_mir::consumers::PoloniusOutput; -impl<'a> Into for &'a Loan { - fn into(self) -> Borrow { - self.0.into() - } +trait LocationTableExt { + fn to_mir_location(self, point: PointIndex) -> mir::Location; } -impl FromStr for Region { - type Err = (); - - fn from_str(region: &str) -> Result { - lazy_static! { - static ref RE: Regex = Regex::new(r"^'_#(?P\d+)r$").unwrap(); +impl LocationTableExt for LocationTable { + fn to_mir_location(self, point: PointIndex) -> mir::Location { + match self.to_location(point) { + RichLocation::Start(location) | RichLocation::Mid(location) => location, } - let caps = RE.captures(region).unwrap(); - let id: usize = caps["id"].parse().unwrap(); - Ok(Self { 0: id }) } } -impl FromStr for Loan { - type Err = (); - - fn from_str(loan: &str) -> Result { - lazy_static! { - static ref RE: Regex = Regex::new(r"^bw(?P\d+)$").unwrap(); - } - let caps = RE.captures(loan).unwrap(); - let id: usize = caps["id"].parse().unwrap(); - Ok(Self { 0: id }) - } +pub struct BorrowckFacts { + /// Polonius input facts. + pub input_facts: RefCell>, + /// Polonius output facts. + pub output_facts: Rc, + /// The table that maps Polonius points to locations in the table. + pub location_table: RefCell>, } /// The type of the point. Either the start of a statement or in the /// middle of it. -#[derive(Debug, PartialEq, Eq, Hash, Clone)] +#[derive(Debug, PartialEq, Eq, Hash, Clone, Copy)] pub enum PointType { Start, Mid, @@ -134,23 +68,8 @@ impl std::cmp::Ord for PointType { } } -#[derive(Debug)] -pub struct UnknownPointTypeError(String); - -impl FromStr for PointType { - type Err = UnknownPointTypeError; - - fn from_str(point_type: &str) -> Result { - match point_type { - "Start" => Ok(PointType::Start), - "Mid" => Ok(PointType::Mid), - _ => Err(UnknownPointTypeError(String::from(point_type))), - } - } -} - /// A program point used in the borrow checker analysis. -#[derive(Debug, PartialEq, Eq, Hash, Clone, PartialOrd, Ord)] +#[derive(Debug, PartialEq, Eq, Hash, Clone, Copy, PartialOrd, Ord)] pub struct Point { pub location: mir::Location, pub typ: PointType, @@ -168,272 +87,36 @@ impl std::fmt::Display for Point { } } -impl FromStr for Point { - type Err = (); - - fn from_str(point: &str) -> Result { - lazy_static! { - static ref RE: Regex = - Regex::new(r"^(?PMid|Start)\(bb(?P\d+)\[(?P\d+)\]\)$").unwrap(); - } - let caps = RE.captures(point).unwrap(); - let point_type: PointType = caps["type"].parse().unwrap(); - let basic_block: usize = caps["bb"].parse().unwrap(); - let statement_index: usize = caps["stmt"].parse().unwrap(); - Ok(Self { - location: mir::Location { - block: mir::BasicBlock::new(basic_block), - statement_index: statement_index, - }, - typ: point_type, - }) - } -} - -impl FromStr for Variable { - type Err = (); - - fn from_str(variable: &str) -> Result { - Ok(Self(variable[1..].parse().unwrap())) - } -} - -impl FromStr for Place { - type Err = (); - - fn from_str(place: &str) -> Result { - assert_eq!(place.chars().nth(0).unwrap(), 'm'); - assert_eq!(place.chars().nth(1).unwrap(), 'p'); - Ok(Self(place[2..].parse().unwrap())) - } -} - -#[derive(Debug, Clone, Copy)] -pub struct PoloniusFactTypes; - -impl polonius_engine::FactTypes for PoloniusFactTypes { - type Origin = Region; - type Loan = Loan; - type Point = PointIndex; - type Variable = Variable; - type Path = Place; -} - -pub type AllInputFacts = polonius_engine::AllFacts; -pub type AllOutputFacts = polonius_engine::Output; - -/// A table that stores a mapping between interned elements of type -/// `SourceType` and their indices. -pub struct InternerTable + Copy> { - /// For looking up from index type to source type. - interned_elements: Vec, - /// For looking up from source type into index type. - index_elements: HashMap, -} - -impl InternerTable -where - SourceType: Eq + Hash + Clone, - IndexType: Into + From + Copy, -{ - fn new() -> Self { - Self { - interned_elements: Vec::new(), - index_elements: HashMap::new(), - } - } - fn get_or_create_index(&mut self, element: SourceType) -> IndexType { - if let Some(&interned) = self.index_elements.get(&element) { - return interned; - } - - let index = IndexType::from(self.index_elements.len()); - self.interned_elements.push(element.clone()); - *self.index_elements.entry(element).or_insert(index) - } - fn get_index(&self, element: &SourceType) -> IndexType { - self.index_elements[element] - } - fn get_element(&self, index: IndexType) -> &SourceType { - let index: usize = index.into(); - &self.interned_elements[index] - } -} - -trait InternTo { - fn intern(&mut self, element: FromType) -> ToType; -} - pub struct Interner { - points: InternerTable, + location_table: LocationTable, } impl Interner { - pub fn get_point_index(&self, point: &Point) -> PointIndex { - self.points.get_index(point) - } - - pub fn get_point(&self, index: PointIndex) -> &Point { - self.points.get_element(index) - } -} - -impl InternTo for Interner { - fn intern(&mut self, element: String) -> Region { - element.parse().unwrap() + pub fn new(location_table: LocationTable) -> Self { + Self { location_table } } -} - -impl InternTo for Interner { - fn intern(&mut self, element: String) -> Loan { - element.parse().unwrap() - } -} - -impl InternTo for Interner { - fn intern(&mut self, element: String) -> PointIndex { - let point = element.parse().unwrap(); - self.points.get_or_create_index(point) - } -} - -impl InternTo for Interner { - fn intern(&mut self, element: String) -> Variable { - element.parse().unwrap() - } -} - -impl InternTo for Interner { - fn intern(&mut self, element: String) -> Place { - element.parse().unwrap() - } -} - -impl InternTo<(String, String), (A, B)> for Interner -where - Interner: InternTo, - Interner: InternTo, -{ - fn intern(&mut self, (e1, e2): (String, String)) -> (A, B) { - (self.intern(e1), self.intern(e2)) - } -} - -impl InternTo<(String, String, String), (A, B, C)> for Interner -where - Interner: InternTo, - Interner: InternTo, - Interner: InternTo, -{ - fn intern(&mut self, (e1, e2, e3): (String, String, String)) -> (A, B, C) { - (self.intern(e1), self.intern(e2), self.intern(e3)) - } -} - -fn load_facts_from_file(facts_dir: &Path, facts_type: &str) -> Vec { - let filename = format!("{}.facts", facts_type); - let facts_file = facts_dir.join(&filename); - let mut reader = ReaderBuilder::new() - .delimiter(b'\t') - .has_headers(false) - .from_path(&facts_file) - .unwrap_or_else(|err| panic!("failed to read file {:?} with err: {}", facts_file, err)); - reader.deserialize().map(|row| row.unwrap()).collect() -} -impl Interner { - pub fn new() -> Self { - Self { - points: InternerTable::new(), + pub fn get_point_index(&self, point: &Point) -> PointIndex { + // self.points.get_index(point) + match point.typ { + PointType::Start => self.location_table.start_index(point.location), + PointType::Mid => self.location_table.mid_index(point.location), } } -} -pub struct FactLoader { - pub interner: Interner, - pub facts: AllInputFacts, -} - -impl FactLoader { - pub fn new() -> Self { - Self { - interner: Interner::new(), - facts: AllInputFacts::default(), + pub fn get_point(&self, index: PointIndex) -> Point { + // self.points.get_element(index) + match self.location_table.to_location(index) { + RichLocation::Start(location) => { + Point { + location, typ: PointType::Start + } + } + RichLocation::Mid(location) => { + Point { + location, typ: PointType::Mid + } + } } } - pub fn load_all_facts(&mut self, facts_dir: &Path) { - let facts = load_facts::<(String, String, String), _>( - &mut self.interner, - facts_dir, - "borrow_region", - ); - self.facts.borrow_region.extend(facts); - - let facts = load_facts::(&mut self.interner, facts_dir, "universal_region"); - self.facts.universal_region.extend(facts); - - let facts = load_facts::<(String, String), _>(&mut self.interner, facts_dir, "cfg_edge"); - self.facts.cfg_edge.extend(facts); - - let facts = load_facts::<(String, String), _>(&mut self.interner, facts_dir, "killed"); - self.facts.killed.extend(facts); - - let facts = - load_facts::<(String, String, String), _>(&mut self.interner, facts_dir, "outlives"); - self.facts.outlives.extend(facts); - - let facts = load_facts::<(String, String), _>(&mut self.interner, facts_dir, "invalidates"); - self.facts.invalidates.extend(facts); - - let facts = load_facts::<(String, String), _>(&mut self.interner, facts_dir, "var_used_at"); - self.facts.var_used_at.extend(facts); - - let facts = load_facts::<(String, String), _>(&mut self.interner, facts_dir, "var_defined_at"); - self.facts.var_defined_at.extend(facts); - - let facts = load_facts::<(String, String), _>(&mut self.interner, facts_dir, "var_dropped_at"); - self.facts.var_dropped_at.extend(facts); - - let facts = load_facts::<(String, String), _>(&mut self.interner, facts_dir, "use_of_var_derefs_origin"); - self.facts.use_of_var_derefs_origin.extend(facts); - - let facts = load_facts::<(String, String), _>(&mut self.interner, facts_dir, "drop_of_var_derefs_origin"); - self.facts.drop_of_var_derefs_origin.extend(facts); - - let facts = load_facts::<(String, String), _>(&mut self.interner, facts_dir, "child_path"); - self.facts.child_path.extend(facts); - - let facts = load_facts::<(String, String), _>(&mut self.interner, facts_dir, "path_is_var"); - self.facts.path_is_var.extend(facts); - - let facts = load_facts::<(String, String), _>(&mut self.interner, facts_dir, "path_assigned_at_base"); - self.facts.path_assigned_at_base.extend(facts); - - let facts = load_facts::<(String, String), _>(&mut self.interner, facts_dir, "path_moved_at_base"); - self.facts.path_moved_at_base.extend(facts); - - let facts = load_facts::<(String, String), _>(&mut self.interner, facts_dir, "path_accessed_at_base"); - self.facts.path_accessed_at_base.extend(facts); - - let facts = load_facts::<(String, String), _>(&mut self.interner, facts_dir, "known_subset"); - self.facts.known_subset.extend(facts); - - let facts = load_facts::<(String, String), _>(&mut self.interner, facts_dir, "placeholder"); - self.facts.placeholder.extend(facts); - - } -} - -fn load_facts( - interner: &mut Interner, - facts_dir: &Path, - facts_type: &str, -) -> Vec -where - Interner: InternTo, -{ - load_facts_from_file(facts_dir, facts_type) - .into_iter() - .map(|fact| Interner::intern(interner, fact)) - .collect() } diff --git a/prusti-interface/src/environment/borrowck/regions.rs b/prusti-interface/src/environment/borrowck/regions.rs index f1d9dbc79a7..3de6b7daf50 100644 --- a/prusti-interface/src/environment/borrowck/regions.rs +++ b/prusti-interface/src/environment/borrowck/regions.rs @@ -7,6 +7,8 @@ ///! Code for finding `rustc::ty::sty::RegionVid` associated with local ///! reference typed variables. +use rustc_mir::consumers::BodyWithBorrowckFacts; + use std::collections::HashMap; use std::fs::File; use std::io; @@ -18,26 +20,10 @@ use log::trace; use regex::Regex; use rustc_index::vec::Idx; -use rustc_middle::mir; +use rustc_middle::{mir, ty}; use crate::environment::borrowck::facts; -lazy_static! { - static ref FN_SIG: Regex = - Regex::new(r"^fn [a-zA-Z\d_]+\((?P.*)\) -> (?P.*)\{$").unwrap(); - - static ref ARG: Regex = - Regex::new(r"^_(?P\d+): &'_#(?P\d+)r (mut)? [a-zA-Z\d_]+\s*$").unwrap(); - - static ref LOCAL: Regex = - Regex::new(r"let( mut)? _(?P\d+): &'_#(?P\d+)r ").unwrap(); - - static ref LOCAL_TUPLE: Regex = - Regex::new(r"let( mut)? _(?P\d+): \((?P.*)\);").unwrap(); - - static ref REF: Regex = Regex::new(r"&'_#(?P\d+)r ").unwrap(); -} - #[derive(Debug)] pub struct PlaceRegions(HashMap<(mir::Local, Vec), facts::Region>); @@ -114,62 +100,50 @@ impl PlaceRegions { } } -pub fn load_place_regions(path: &Path) -> io::Result { - trace!("[enter] load_place_regions(path={:?})", path); - let mut place_regions = PlaceRegions::new(); - let file = File::open(path)?; - for line in io::BufReader::new(file).lines() { - let line = line?; - regions_for_fn_sig(&mut place_regions, &line); - regions_for_local_ref(&mut place_regions, &line); - regions_for_local_tuple(&mut place_regions, &line) +fn extract_region_id(region: &ty::RegionKind) -> facts::Region { + match region { + ty::RegionKind::ReVar(rvid) => { + *rvid + }, + _ => unimplemented!("region: {:?}", region), } - trace!("[exit] load_place_regions"); - Ok(place_regions) } -/// This loads regions for parameters and return values in function signatures. -fn regions_for_fn_sig(place_regions: &mut PlaceRegions, line: &String) { - if let Some(caps) = FN_SIG.captures(&line) { - debug!("args: {} result: {}", &caps["args"], &caps["result"]); - for arg_str in (&caps["args"]).split(", ") { - if let Some(arg_caps) = ARG.captures(arg_str) { - debug!("arg {} rvid {}", &arg_caps["local"], &arg_caps["rvid"]); - let local_arg: usize = (&arg_caps["local"]).parse().unwrap(); - let rvid: usize = (&arg_caps["rvid"]).parse().unwrap(); - place_regions.add_local(mir::Local::new(local_arg), rvid.into()); +fn extract_region(place_regions: &mut PlaceRegions, local: mir::Local, ty: ty::Ty<'_>) { + match ty.kind() { + ty::TyKind::Ref(region, _, _) => { + place_regions.add_local(local, extract_region_id(region)); + debug!("region: {:?}", region); + } + ty::TyKind::Tuple(substs) => { + for (i, ty) in substs.types().enumerate() { + match ty.kind() { + ty::TyKind::Ref(region, _, _) => { + place_regions.add(local, vec![i], extract_region_id(region)) + } + _ => { + debug!("does not contain regions: {:?}[{}]: {:?} {:?}", local, i, ty, ty.kind()); + } + } + } } + _ => { + debug!("does not contain regions: {:?}: {:?} {:?}", local, ty, ty.kind()); + } } } -/// This loads regions for reference-typed local variables. For a local variable declaration like -/// let _3: &'2rv mut i32; -/// it would record that the place _3 has region 2. -fn regions_for_local_ref(place_regions: &mut PlaceRegions, line: &String) { - if let Some(local_caps) = LOCAL.captures(&line) { - debug!( - "local {} rvid {}", - &local_caps["local"], &local_caps["rvid"] - ); - let local_arg: usize = (&local_caps["local"]).parse().unwrap(); - let rvid: usize = (&local_caps["rvid"]).parse().unwrap(); - place_regions.add_local(mir::Local::new(local_arg), rvid.into()); - } -} +pub fn load_place_regions(body: &mir::Body<'_>) -> io::Result { + trace!("[enter] load_place_regions()"); + let mut place_regions = PlaceRegions::new(); -/// This loads regions for tuples. For a local variable declaration like -/// ```ignore -/// let _5: (&'6rv mut i32, &'7rv mut i32); -/// ``` -/// it would record that the place _5.0 has region 6 and the place _5.1 has region 7. -fn regions_for_local_tuple(place_regions: &mut PlaceRegions, line: &String) { - if let Some(m) = LOCAL_TUPLE.captures(&line) { - let local = mir::Local::new(m["local"].parse().unwrap()); - let items = &m["items"]; - for (i, m) in REF.captures_iter(&items).enumerate() { - let rvid: usize = m["rvid"].parse().unwrap(); - place_regions.add(local, vec![i], rvid.into()); - } + for (local, local_decl) in body.local_decls.iter_enumerated() { + let ty = local_decl.ty; + debug!("local: {:?} {:?}", local, ty); + extract_region(&mut place_regions, local, ty); } + + trace!("[exit] load_place_regions"); + Ok(place_regions) } diff --git a/prusti-interface/src/environment/dump_borrowck_info.rs b/prusti-interface/src/environment/dump_borrowck_info.rs index c9a146dda97..1ea21b9a27e 100644 --- a/prusti-interface/src/environment/dump_borrowck_info.rs +++ b/prusti-interface/src/environment/dump_borrowck_info.rs @@ -4,6 +4,7 @@ // License, v. 2.0. If a copy of the MPL was not distributed with this // file, You can obtain one at http://mozilla.org/MPL/2.0/. +use super::Environment; use super::borrowck::facts; use super::loops; use super::loops_utils::*; @@ -29,10 +30,10 @@ use log::{trace, debug}; use prusti_common::config; use crate::environment::mir_utils::RealEdges; -pub fn dump_borrowck_info<'a, 'tcx>(tcx: TyCtxt<'tcx>, procedures: &Vec) { +pub fn dump_borrowck_info<'a, 'tcx>(env: &'a Environment<'tcx>, procedures: &Vec) { trace!("[dump_borrowck_info] enter"); - let printer = InfoPrinter { tcx: tcx }; + let printer = InfoPrinter { env, tcx: env.tcx() }; //intravisit::walk_crate(&mut printer, tcx.hir.krate()); //tcx.hir.krate().visit_all_item_likes(&mut printer); @@ -43,11 +44,12 @@ pub fn dump_borrowck_info<'a, 'tcx>(tcx: TyCtxt<'tcx>, procedures: &Vec { - pub tcx: TyCtxt<'tcx>, +struct InfoPrinter<'a, 'tcx: 'a> { + env: &'a Environment<'tcx>, + tcx: TyCtxt<'tcx>, } -impl<'tcx> InfoPrinter<'tcx> { +impl<'a, 'tcx: 'a> InfoPrinter<'a, 'tcx> { fn print_info(&self, def_id: ProcedureDefId) { trace!("[print_info] enter {:?}", def_id); @@ -60,7 +62,7 @@ impl<'tcx> InfoPrinter<'tcx> { _ => {}, };*/ - let procedure = Procedure::new(self.tcx, def_id); + let procedure = Procedure::new(self.env, def_id); let local_def_id = def_id.expect_local(); let _ = self.tcx.mir_borrowck(local_def_id); @@ -68,8 +70,7 @@ impl<'tcx> InfoPrinter<'tcx> { // Read Polonius facts. let def_path = self.tcx.hir().def_path(local_def_id); - let (mir, _) = self.tcx.mir_promoted(ty::WithOptConstParam::unknown(local_def_id)); - let mir = mir.borrow(); + let mir = procedure.get_mir(); let real_edges = RealEdges::new(&mir); let loop_info = loops::ProcedureLoops::new(&mir, &real_edges); @@ -88,7 +89,7 @@ impl<'tcx> InfoPrinter<'tcx> { // FIXME: this computes the wrong loop invariant permission let loop_invariant_block = HashMap::new(); - super::polonius_info::graphviz(self.tcx, &def_path, &mir).unwrap(); + super::polonius_info::graphviz(self.env, &def_path, def_id).unwrap(); let mir_info_printer = MirInfoPrinter { def_path: def_path, tcx: self.tcx, @@ -97,7 +98,7 @@ impl<'tcx> InfoPrinter<'tcx> { loops: loop_info, initialization: initialization, liveness: liveness, - polonius_info: PoloniusInfo::new(&procedure, &loop_invariant_block).ok().unwrap(), + polonius_info: PoloniusInfo::new(self.env, &procedure, &loop_invariant_block).ok().unwrap(), }; mir_info_printer.print_info().unwrap(); @@ -183,7 +184,7 @@ macro_rules! to_sorted_string { impl<'a, 'tcx> MirInfoPrinter<'a, 'tcx> { pub fn print_info(mut self) -> Result<(), io::Error> { //self.dump_to_file("/tmp/requires", - //&self.polonius_info.borrowck_out_facts.restricts); + //&self.polonius_info.borrowck_out_facts.origin_contains_loan_at); //self.dump_to_file("/tmp/zrequires", //&self.polonius_info.additional_facts.zombie_requires); @@ -257,7 +258,7 @@ impl<'a, 'tcx> MirInfoPrinter<'a, 'tcx> { Ok(()) } - /// Print the restricts relation as a tree of loans. + /// Print the origin_contains_loan_at relation as a tree of loans. fn print_restricts(&self) -> Result<(), io::Error> { if !self.show_restricts() { return Ok(()); @@ -265,7 +266,7 @@ impl<'a, 'tcx> MirInfoPrinter<'a, 'tcx> { write_graph!(self, "subgraph cluster_restricts {{"); let mut interesting_restricts = Vec::new(); let mut loans = Vec::new(); - for &(region, loan, point) in self.polonius_info.borrowck_in_facts.borrow_region.iter() { + for &(region, loan, point) in self.polonius_info.borrowck_in_facts.loan_issued_at.iter() { write_graph!( self, "\"region_live_at_{:?}_{:?}_{:?}\" [ ", @@ -309,14 +310,14 @@ impl<'a, 'tcx> MirInfoPrinter<'a, 'tcx> { } } for (region, point) in interesting_restricts.iter() { - if let Some(restricts_map) = self.polonius_info.borrowck_out_facts.restricts.get(&point) + if let Some(restricts_map) = self.polonius_info.borrowck_out_facts.origin_contains_loan_at.get(&point) { if let Some(loans) = restricts_map.get(®ion) { for loan in loans.iter() { write_graph!(self, "\"restricts_{:?}_{:?}_{:?}\" [ ", point, region, loan); write_graph!( self, - "label=\"restricts({:?}, {:?}, {:?})\" ];", + "label=\"origin_contains_loan_at({:?}, {:?}, {:?})\" ];", point, region, loan @@ -401,7 +402,7 @@ impl<'a, 'tcx> MirInfoPrinter<'a, 'tcx> { return Ok(()); } write_graph!(self, "subgraph cluster_Loans {{"); - for (region, loan, point) in self.polonius_info.borrowck_in_facts.borrow_region.iter() { + for (region, loan, point) in self.polonius_info.borrowck_in_facts.loan_issued_at.iter() { write_graph!(self, "subgraph cluster_{:?} {{", loan); let subset_map = &self.polonius_info.borrowck_out_facts.subset; if let Some(ref subset) = subset_map.get(&point).as_ref() { @@ -736,7 +737,7 @@ impl<'a, 'tcx> MirInfoPrinter<'a, 'tcx> { statement_index: 0, }; let start_point = self.get_point(start_location, facts::PointType::Start); - let restricts_map = &self.polonius_info.borrowck_out_facts.restricts; + let restricts_map = &self.polonius_info.borrowck_out_facts.origin_contains_loan_at; if let Some(ref restricts_relation) = restricts_map.get(&start_point).as_ref() { for (region, all_loans) in restricts_relation.iter() { // Filter out reborrows. @@ -773,8 +774,8 @@ impl<'a, 'tcx> MirInfoPrinter<'a, 'tcx> { write_graph!(self, "{:?}_{:?} -> {:?}_{:?}", bb, region, bb, loan); write_graph!(self, "subgraph cluster_{:?}_{:?} {{", bb, loan); - let borrow_region = &self.polonius_info.borrowck_in_facts.borrow_region; - for (region, l, point) in borrow_region.iter() { + let loan_issued_at = &self.polonius_info.borrowck_in_facts.loan_issued_at; + for (region, l, point) in loan_issued_at.iter() { if loan == l { // Write the original loan's region. write_graph!( @@ -886,7 +887,7 @@ impl<'a, 'tcx> MirInfoPrinter<'a, 'tcx> { if let Some(ref blas) = self .polonius_info .borrowck_out_facts - .borrow_live_at + .loan_live_at .get(&start_point) .as_ref() { @@ -900,7 +901,7 @@ impl<'a, 'tcx> MirInfoPrinter<'a, 'tcx> { let borrow_regions: Vec<_> = self .polonius_info .borrowck_in_facts - .borrow_region + .loan_issued_at .iter() .filter(|(_, _, point)| *point == start_point) .cloned() @@ -910,7 +911,7 @@ impl<'a, 'tcx> MirInfoPrinter<'a, 'tcx> { let borrow_regions: Vec<_> = self .polonius_info .borrowck_in_facts - .borrow_region + .loan_issued_at .iter() .filter(|(_, _, point)| *point == mid_point) .cloned() @@ -1230,7 +1231,7 @@ impl<'a, 'tcx> MirInfoPrinter<'a, 'tcx> { /// Print the HTML cell with loans at given location. fn write_mid_point_blas(&self, location: mir::Location) -> Result<(), io::Error> { let mid_point = self.get_point(location, facts::PointType::Mid); - let borrow_live_at_map = &self.polonius_info.borrowck_out_facts.borrow_live_at; + let borrow_live_at_map = &self.polonius_info.borrowck_out_facts.loan_live_at; let mut blas = if let Some(ref blas) = borrow_live_at_map.get(&mid_point).as_ref() { (**blas).clone() } else { @@ -1351,7 +1352,7 @@ impl<'a, 'tcx> MirInfoPrinter<'a, 'tcx> { &zombie_loans, location, ).ok().unwrap(); - //let restricts_map = &self.polonius_info.borrowck_out_facts.restricts; + //let restricts_map = &self.polonius_info.borrowck_out_facts.origin_contains_loan_at; write_graph!(self, ""); write_graph!(self, "Package"); write_graph!(self, "{}", to_sorted_string!(all_loans)); diff --git a/prusti-interface/src/environment/mir_storage.rs b/prusti-interface/src/environment/mir_storage.rs new file mode 100644 index 00000000000..955bed6f70c --- /dev/null +++ b/prusti-interface/src/environment/mir_storage.rs @@ -0,0 +1,51 @@ +//! This module allows storing mir bodies with borrowck facts in a thread-local +//! storage. Unfortunately, thread local storage requires all data stored in it +//! to have a `'static` lifetime. Therefore, we transmute the lifetime `'tcx` +//! away when storing the data. To ensure that nothing gets meessed up, we +//! require the client to provide a witness: an instance of type `TyCtxt<'tcx>` +//! that is used to show that the lifetime that the client provided is indeed +//! `'tcx`. + +use rustc_hir::def_id::LocalDefId; +use rustc_middle::ty::TyCtxt; +use rustc_mir::consumers::BodyWithBorrowckFacts; +use std::{cell::RefCell, collections::HashMap, thread_local}; + +thread_local! { + pub static SHARED_STATE: + RefCell>> = + RefCell::new(HashMap::new()); +} + +/// # Safety +/// +/// See the module level comment. +pub unsafe fn store_mir_body<'tcx>( + _tcx: TyCtxt<'tcx>, + def_id: LocalDefId, + body_with_facts: BodyWithBorrowckFacts<'tcx>, +) { + // SAFETY: See the module level comment. + let body_with_facts: BodyWithBorrowckFacts<'static> = + unsafe { std::mem::transmute(body_with_facts) }; + SHARED_STATE.with(|state| { + let mut map = state.borrow_mut(); + assert!(map.insert(def_id, body_with_facts).is_none()); + }); +} + +/// # Safety +/// +/// See the module level comment. +#[allow(clippy::needless_lifetimes)] // We want to be very explicit about lifetimes here. +pub(super) unsafe fn retrieve_mir_body<'tcx>( + _tcx: TyCtxt<'tcx>, + def_id: LocalDefId, +) -> BodyWithBorrowckFacts<'tcx> { + let body_with_facts: BodyWithBorrowckFacts<'static> = SHARED_STATE.with(|state| { + let mut map = state.borrow_mut(); + map.remove(&def_id).unwrap() + }); + // SAFETY: See the module level comment. + unsafe { std::mem::transmute(body_with_facts) } +} diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index 7a3e693a323..a8323c9fccd 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -18,6 +18,9 @@ use std::cell::Ref; use rustc_span::{Span, MultiSpan, symbol::Symbol}; use std::collections::HashSet; use log::debug; +use std::rc::Rc; +use std::collections::HashMap; +use std::cell::RefCell; pub mod borrowck; mod collect_prusti_spec_visitor; @@ -26,6 +29,7 @@ mod dump_borrowck_info; mod loops; mod loops_utils; pub mod mir_analyses; +pub mod mir_storage; pub mod mir_utils; pub mod place_set; pub mod polonius_info; @@ -37,6 +41,7 @@ use rustc_hir::intravisit::Visitor; pub use self::loops::{PlaceAccess, PlaceAccessKind, ProcedureLoops}; pub use self::loops_utils::*; pub use self::procedure::{BasicBlockIndex, Procedure}; +use self::borrowck::facts::BorrowckFacts; // use config; use crate::data::ProcedureDefId; // use syntax::codemap::CodeMap; @@ -47,13 +52,21 @@ use rustc_span::source_map::SourceMap; /// Facade to the Rust compiler. // #[derive(Copy, Clone)] pub struct Environment<'tcx> { + /// Cached MIR bodies. + bodies: RefCell>>>, + /// Cached borrowck information. + borrowck_facts: RefCell>>, tcx: TyCtxt<'tcx>, } impl<'tcx> Environment<'tcx> { /// Builds an environment given a compiler state. pub fn new(tcx: TyCtxt<'tcx>) -> Self { - Environment { tcx } + Environment { + tcx, + bodies: RefCell::new(HashMap::new()), + borrowck_facts: RefCell::new(HashMap::new()), + } } /// Returns the path of the source that is being compiled @@ -186,7 +199,7 @@ impl<'tcx> Environment<'tcx> { /// Mostly used for experiments and debugging. pub fn dump_borrowck_info(&self, procedures: &Vec) { if prusti_common::config::dump_borrowck_info() { - dump_borrowck_info::dump_borrowck_info(self.tcx(), procedures) + dump_borrowck_info::dump_borrowck_info(self, procedures) } } @@ -214,15 +227,41 @@ impl<'tcx> Environment<'tcx> { } /// Get a Procedure. - pub fn get_procedure<'a>(&'a self, proc_def_id: ProcedureDefId) -> Procedure<'a, 'tcx> { - Procedure::new(self.tcx(), proc_def_id) + pub fn get_procedure(&self, proc_def_id: ProcedureDefId) -> Procedure<'tcx> { + Procedure::new(self, proc_def_id) } /// Get the MIR body of a local procedure. - pub fn local_mir<'a>(&self, def_id: LocalDefId) -> Ref<'a, mir::Body<'tcx>> { - self.tcx().mir_promoted( - ty::WithOptConstParam::unknown(def_id) - ).0.borrow() + pub fn local_mir(&self, def_id: LocalDefId) -> Rc> { + let mut bodies = self.bodies.borrow_mut(); + if let Some(body) = bodies.get(&def_id) { + body.clone() + } else { + // SAFETY: This is safe because we are feeding in the same `tcx` + // that was used to store the data. + let body_with_facts = unsafe { + self::mir_storage::retrieve_mir_body(self.tcx, def_id) + }; + let body = body_with_facts.body; + let facts = BorrowckFacts { + input_facts: RefCell::new(Some(body_with_facts.input_facts)), + output_facts: body_with_facts.output_facts, + location_table: RefCell::new(Some(body_with_facts.location_table)), + }; + + let mut borrowck_facts = self.borrowck_facts.borrow_mut(); + borrowck_facts.insert(def_id, Rc::new(facts)); + + bodies.entry(def_id).or_insert_with(|| { + Rc::new(body) + }).clone() + } + } + + /// Get Polonius facts of a local procedure. + pub fn local_mir_borrowck_facts(&self, def_id: LocalDefId) -> Rc { + let borrowck_facts = self.borrowck_facts.borrow(); + borrowck_facts.get(&def_id).unwrap().clone() } /// Get the MIR body of an external procedure. diff --git a/prusti-interface/src/environment/polonius_info.rs b/prusti-interface/src/environment/polonius_info.rs index 3276a966d8e..ba3da2d95ce 100644 --- a/prusti-interface/src/environment/polonius_info.rs +++ b/prusti-interface/src/environment/polonius_info.rs @@ -17,12 +17,13 @@ use log::trace; use polonius_engine::Algorithm; use polonius_engine::Atom; use polonius_engine::Output; -use rustc_hash::FxHashMap; +use rustc_data_structures::fx::FxHashMap; use rustc_index::vec::Idx; use rustc_middle::mir; use rustc_middle::ty; -use rustc_span::def_id::LOCAL_CRATE; +use rustc_span::def_id::{DefId, LOCAL_CRATE}; use rustc_span::Span; +use rustc_index::vec::IndexVec; use crate::environment::borrowck::facts::PointType; use crate::environment::borrowck::regions::{PlaceRegions, PlaceRegionsError}; @@ -41,6 +42,7 @@ use super::mir_analyses::initialization::DefinitelyInitializedAnalysisResult; use super::mir_analyses::liveness::compute_liveness; use super::mir_analyses::liveness::LivenessAnalysisResult; use super::procedure::Procedure; +use super::Environment; use prusti_common::config; use crate::environment::mir_utils::RealEdges; @@ -272,9 +274,9 @@ pub enum PoloniusInfoError { } pub fn graphviz<'tcx>( - tcx: rustc_middle::ty::TyCtxt<'tcx>, + env: &Environment<'tcx>, def_path: &rustc_hir::definitions::DefPath, - _mir: &mir::Body<'tcx>, + def_id: DefId, ) -> std::io::Result<()> { macro_rules! to_html { ( $o:expr ) => {{ @@ -295,9 +297,10 @@ pub fn graphviz<'tcx>( }}; } - let facts_loader = load_polonius_facts(tcx, def_path); - let interner = facts_loader.interner; - let borrowck_in_facts = facts_loader.facts; + let facts = env.local_mir_borrowck_facts(def_id.expect_local()); + let interner = facts::Interner::new(facts.location_table.take().unwrap()); + + let borrowck_in_facts = facts.input_facts.take().unwrap(); let borrowck_out_facts = Output::compute(&borrowck_in_facts, Algorithm::Naive, true); use std::io::Write; @@ -344,7 +347,7 @@ pub fn graphviz<'tcx>( write!(graph, "{:?}\n", block)?; write!(graph, "")?; write!(graph, "point")?; - write!(graph, "borrow_live_at")?; + write!(graph, "loan_live_at")?; write!(graph, "\n")?; let mut points: Vec<_> = point_indices.iter().map(|index| interner.get_point(*index)).collect(); points.sort(); @@ -353,7 +356,7 @@ pub fn graphviz<'tcx>( write!(graph, "{}\n", point)?; write!(graph, "")?; let point_index = interner.get_point_index(&point); - for loan in &borrowck_out_facts.borrow_live_at[&point_index] { + for loan in &borrowck_out_facts.loan_live_at[&point_index] { write!(graph, "{:?},", loan)?; } write!(graph, "")?; @@ -368,18 +371,6 @@ pub fn graphviz<'tcx>( Ok(()) } -fn load_polonius_facts<'tcx>( - _tcx: rustc_middle::ty::TyCtxt<'tcx>, - def_path: &rustc_hir::definitions::DefPath, -) -> facts::FactLoader { - let dir_path = PathBuf::from(config::log_dir()) - .join("nll-facts") - .join(def_path.to_filename_friendly_no_crate()); - debug!("Reading facts from: {:?}", dir_path); - let mut facts_loader = facts::FactLoader::new(); - facts_loader.load_all_facts(&dir_path); - facts_loader -} pub struct PoloniusInfo<'a, 'tcx: 'a> { pub(crate) tcx: ty::TyCtxt<'tcx>, @@ -431,7 +422,7 @@ fn add_fake_facts<'a, 'tcx: 'a>( let mut incompatible_loans = Vec::new(); let mut last_loan_id = Iterator::chain( - all_facts.borrow_region.iter() + all_facts.loan_issued_at.iter() .map(|(_, loan, _)| loan.index()), all_facts.placeholder.iter() .map(|(_, loan)| loan.index()) @@ -445,18 +436,18 @@ fn add_fake_facts<'a, 'tcx: 'a>( // Create a map from points to (region1, region2) vectors. let universal_region = &all_facts.universal_region; let mut outlives_at_point = HashMap::new(); - for &(region1, region2, point) in all_facts.outlives.iter() { + for &(region1, region2, point) in all_facts.subset_base.iter() { if !universal_region.contains(®ion1) && !universal_region.contains(®ion2) { - let outlives = outlives_at_point.entry(point).or_insert(vec![]); - outlives.push((region1, region2)); + let subset_base = outlives_at_point.entry(point).or_insert(vec![]); + subset_base.push((region1, region2)); } } - // Create new borrow_region facts for points where is only one outlives - // fact and there is not a borrow_region fact already. - let borrow_region = &mut all_facts.borrow_region; + // Create new loan_issued_at facts for points where is only one subset_base + // fact and there is not a loan_issued_at fact already. + let loan_issued_at = &mut all_facts.loan_issued_at; for (point, regions) in outlives_at_point { - if borrow_region + if loan_issued_at .iter() .all(|(_, _, loan_point)| *loan_point != point) { @@ -476,7 +467,7 @@ fn add_fake_facts<'a, 'tcx: 'a>( if let Some(var_region) = place_regions.for_local(local) { let loan = new_loan(); debug!("var_region = {:?} loan = {:?}", var_region, loan); - borrow_region.push((var_region, loan, point)); + loan_issued_at.push((var_region, loan, point)); call_magic_wands.insert(loan, local); } } @@ -485,7 +476,7 @@ fn add_fake_facts<'a, 'tcx: 'a>( if let Some(var_region) = place_regions.for_local(arg) { let loan = new_loan(); debug!("var_region = {:?} loan = {:?}", var_region, loan); - borrow_region.push((var_region, loan, point)); + loan_issued_at.push((var_region, loan, point)); argument_moves.push(loan); } } @@ -514,7 +505,7 @@ fn add_fake_facts<'a, 'tcx: 'a>( for lhs_region in lhs_regions { let loan = new_loan(); reference_moves.push(loan); - borrow_region.push((lhs_region, loan, point)); + loan_issued_at.push((lhs_region, loan, point)); new_incompatible.push(loan); debug!("Adding generic: _ {:?} {:?} {:?}", lhs_region, location, loan); @@ -629,18 +620,18 @@ fn compute_loan_conflict_sets( let mir = procedure.get_mir(); - for &(_r, loan, _) in &borrowck_in_facts.borrow_region { + for &(_r, loan, _) in &borrowck_in_facts.loan_issued_at { loan_conflict_sets.insert(loan, HashSet::new()); } - for &(_r, loan_created, point) in &borrowck_in_facts.borrow_region { + for &(_r, loan_created, point) in &borrowck_in_facts.loan_issued_at { let location = loan_position[&loan_created]; if !procedure.is_reachable_block(location.block) || procedure.is_spec_block(location.block) { continue; } for borrowed_place in get_borrowed_places(mir, loan_position, loan_created)? { - if let Some(live_borrows) = borrowck_out_facts.borrow_live_at.get(&point) { + if let Some(live_borrows) = borrowck_out_facts.loan_live_at.get(&point) { for loan_alive in live_borrows { if loan_created == *loan_alive { continue; @@ -674,37 +665,38 @@ fn compute_loan_conflict_sets( impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> { pub fn new( - procedure: &'a Procedure<'a, 'tcx>, + env: &'a Environment<'tcx>, + procedure: &'a Procedure<'tcx>, _loop_invariant_block: &HashMap, ) -> Result { let tcx = procedure.get_tcx(); let def_id = procedure.get_id(); let mir = procedure.get_mir(); - let def_path = tcx.hir().def_path(def_id.expect_local()); // Read Polonius facts. - let facts_loader = load_polonius_facts(tcx, &def_path); - - // Read relations between region IDs and local variables. - let renumber_path = PathBuf::from(config::log_dir()) - .join("mir") - .join(format!( - "{}.{}.-------.renumber.0.mir", - tcx.crate_name(LOCAL_CRATE), - def_path.to_filename_friendly_no_crate() - )); - debug!("Renumber path: {:?}", renumber_path); - let place_regions = regions::load_place_regions(&renumber_path).unwrap(); + let facts = env.local_mir_borrowck_facts(def_id.expect_local()); + + // // Read relations between region IDs and local variables. + // let renumber_path = PathBuf::from(config::log_dir()) + // .join("mir") + // .join(format!( + // "{}.{}.-------.renumber.0.mir", + // tcx.crate_name(LOCAL_CRATE), + // def_path.to_filename_friendly_no_crate() + // )); + // debug!("Renumber path: {:?}", renumber_path); + let place_regions = regions::load_place_regions(mir).unwrap(); let mut call_magic_wands = HashMap::new(); - let mut all_facts = facts_loader.facts; + let mut all_facts = facts.input_facts.take().unwrap(); + let interner = facts::Interner::new(facts.location_table.take().unwrap()); let real_edges = RealEdges::new(&mir); let loop_info = loops::ProcedureLoops::new(&mir, &real_edges); let (reference_moves, argument_moves, incompatible_loans) = add_fake_facts( &mut all_facts, - &facts_loader.interner, + &interner, tcx, &mir, &place_regions, @@ -719,15 +711,14 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> { let output = Output::compute(&all_facts, Algorithm::Naive, true); let all_facts_without_back_edges = remove_back_edges( all_facts.clone(), - &facts_loader.interner, + &interner, &loop_info.back_edges, ); let output_without_back_edges = Output::compute(&all_facts_without_back_edges, Algorithm::Naive, true); - let interner = facts_loader.interner; let loan_position: HashMap<_, _> = all_facts - .borrow_region + .loan_issued_at .iter() .map(|&(_, loan, point_index)| { let point = interner.get_point(point_index); @@ -735,7 +726,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> { }) .collect(); let loan_at_position: HashMap<_, _> = all_facts - .borrow_region + .loan_issued_at .iter() .map(|&(_, loan, point_index)| { let point = interner.get_point(point_index); @@ -743,7 +734,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> { }) .collect(); let call_loan_at_position: HashMap<_, _> = all_facts - .borrow_region + .loan_issued_at .iter() .filter(|&(_, loan, _)| call_magic_wands.contains_key(loan)) .map(|&(_, loan, point_index)| { @@ -809,7 +800,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> { let universal_region = &all_facts.universal_region; let is_universal = |r: &facts::Region| universal_region.contains(r); let is_input_region = |r: &facts::Region| input_regions.contains(r); - all_facts.outlives.retain(|(r1, r2, _)| ( + all_facts.subset_base.retain(|(r1, r2, _)| ( !is_universal(r1) || is_input_region(r2) ) && ( !is_universal(r2) @@ -884,7 +875,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> { region: facts::Region, ) -> (Vec, Vec) { let mut loans = - self.get_loans_kept_alive_by(point, region, &self.borrowck_out_facts.restricts); + self.get_loans_kept_alive_by(point, region, &self.borrowck_out_facts.origin_contains_loan_at); let zombie_loans = self.get_loans_kept_alive_by(point, region, &self.additional_facts.zombie_requires); loans.extend(zombie_loans.iter().cloned()); @@ -904,7 +895,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> { restricts_map .get(&point) .as_ref() - .and_then(|restricts| restricts.get(®ion)) + .and_then(|origin_contains_loan_at| origin_contains_loan_at.get(®ion)) .map(|loans| loans.iter().cloned().collect()) .unwrap_or(Vec::new()) } @@ -934,21 +925,21 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> { if zombie { &self.additional_facts.zombie_borrow_live_at } else { - &self.borrowck_out_facts.borrow_live_at + &self.borrowck_out_facts.loan_live_at } } /// Get loans that are active (including those that are about to die) at the given location. pub fn get_active_loans(&self, location: mir::Location, zombie: bool) -> Vec { - let borrow_live_at = self.get_borrow_live_at(zombie); + let loan_live_at = self.get_borrow_live_at(zombie); let start_point = self.get_point(location, facts::PointType::Start); let mid_point = self.get_point(location, facts::PointType::Mid); - let mut loans = if let Some(mid_loans) = borrow_live_at.get(&mid_point) { + let mut loans = if let Some(mid_loans) = loan_live_at.get(&mid_point) { let mut mid_loans = mid_loans.clone(); mid_loans.sort(); let default_vec = vec![]; - let start_loans = borrow_live_at.get(&start_point).unwrap_or(&default_vec); + let start_loans = loan_live_at.get(&start_point).unwrap_or(&default_vec); let mut start_loans = start_loans.clone(); start_loans.sort(); debug!("start_loans = {:?}", start_loans); @@ -959,11 +950,11 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> { mid_loans } else { - assert!(borrow_live_at.get(&start_point).is_none()); + assert!(loan_live_at.get(&start_point).is_none()); vec![] }; if !zombie { - for (_, loan, point) in self.borrowck_in_facts.borrow_region.iter() { + for (_, loan, point) in self.borrowck_in_facts.loan_issued_at.iter() { if point == &mid_point && !loans.contains(loan) { loans.push(*loan); } @@ -1011,7 +1002,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> { /// Get loans that die *at* (that is, exactly after) the given location. pub fn get_loans_dying_at(&self, location: mir::Location, zombie: bool) -> Vec { - let borrow_live_at = self.get_borrow_live_at(zombie); + let loan_live_at = self.get_borrow_live_at(zombie); let successors = self.get_successors(location); let is_return = is_return(self.mir, location); let mid_point = self.get_point(location, facts::PointType::Mid); @@ -1026,7 +1017,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> { .filter(|loan| { let alive_in_successor = successors.iter().any(|successor_location| { let point = self.get_point(*successor_location, facts::PointType::Start); - borrow_live_at + loan_live_at .get(&point) .map_or(false, |successor_loans| successor_loans.contains(loan)) }); @@ -1060,8 +1051,8 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> { trace!("becoming_zombie_loans={:?}", becoming_zombie_loans); let final_loc_point = self.get_point(final_loc, facts::PointType::Start); trace!( - "borrow_live_at final {:?}", - self.borrowck_out_facts.borrow_live_at.get(&final_loc_point) + "loan_live_at final {:?}", + self.borrowck_out_facts.loan_live_at.get(&final_loc_point) ); let dying_loans = self .get_active_loans(initial_loc, zombie) @@ -1140,7 +1131,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> { ) -> Vec { if let Some(all_conflicting_loans) = self.loan_conflict_sets.get(&loan) { let point = self.get_point(location, facts::PointType::Mid); - if let Some(alive_loans) = self.borrowck_out_facts.borrow_live_at.get(&point) { + if let Some(alive_loans) = self.borrowck_out_facts.loan_live_at.get(&point) { let alive_conflicting_loans = all_conflicting_loans .iter() .filter(|loan| alive_loans.contains(loan)) @@ -1236,7 +1227,7 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> { return Ok(assignments.pop()); } - let region = self.get_borrow_region_for_loan(loan); + let region = self.get_loan_issued_at_for_loan(loan); // Drops all assignments where the LHS region isn't equal to the region of the loan we're // interested in. The reason this works is a bit subtle. First, if execution reaches this @@ -1272,10 +1263,10 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> { /// let _1: &'1rv u32; /// _1 = &'2rv 123; /// ``` - fn get_borrow_region_for_loan(&self, loan: facts::Loan) -> facts::Region { + fn get_loan_issued_at_for_loan(&self, loan: facts::Loan) -> facts::Region { let location = self.get_loan_location(&loan); let point = self.get_point(location, PointType::Mid); - let regions = self.borrowck_in_facts.borrow_region.iter() + let regions = self.borrowck_in_facts.loan_issued_at.iter() .filter_map(|&(r, l, p)| if p == point && l == loan { Some(r) @@ -1321,11 +1312,11 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> { // ReborrowingKind::ArgumentMove { ref loan } => { // let index = self // .borrowck_in_facts -// .borrow_region +// .loan_issued_at // .iter() // .position(|(_, l, _)| l == loan) // .unwrap(); -// let (region, _, _) = self.borrowck_in_facts.borrow_region[index]; +// let (region, _, _) = self.borrowck_in_facts.loan_issued_at[index]; // let variable = self.find_variable(region).unwrap(); // variable // } @@ -2005,8 +1996,8 @@ pub struct AdditionalFacts { /// ```datalog /// reborrows(Loan, Loan); /// reborrows(L1, L2) :- - /// borrow_region(R, L1, P), - /// restricts(R, P, L2). + /// loan_issued_at(R, L1, P), + /// origin_contains_loan_at(R, P, L2). /// reborrows(L1, L3) :- /// reborrows(L1, L2), /// reborrows(L2, L3). @@ -2015,13 +2006,13 @@ pub struct AdditionalFacts { /// Non-transitive `reborrows`. pub reborrows_direct: Vec<(facts::Loan, facts::Loan)>, /// The ``zombie_requires`` facts are ``requires`` facts for the loans - /// that were killed. + /// that were loan_killed_at. /// /// ```datalog /// zombie_requires(Region, Loan, Point); /// zombie_requires(R, L, Q) :- /// requires(R, L, P), - /// killed(L, P), + /// loan_killed_at(L, P), /// cfg_edge(P, Q), /// origin_live_on_entry(R, Q). /// zombie_requires(R2, L, P) :- @@ -2034,8 +2025,8 @@ pub struct AdditionalFacts { /// ``` pub zombie_requires: FxHashMap>>, - /// The ``zombie_borrow_live_at`` facts are ``borrow_live_at`` facts - /// for the loans that were killed. + /// The ``zombie_borrow_live_at`` facts are ``loan_live_at`` facts + /// for the loans that were loan_killed_at. /// /// ```datalog /// zombie_borrow_live_at(L, P) :- @@ -2043,7 +2034,7 @@ pub struct AdditionalFacts { /// origin_live_on_entry(R, P). /// ``` pub zombie_borrow_live_at: FxHashMap>, - /// Which loans were killed (become zombies) at a given point. + /// Which loans were loan_killed_at (become zombies) at a given point. pub borrow_become_zombie_at: FxHashMap>, } @@ -2070,7 +2061,7 @@ impl AdditionalFacts { // Variables for initial data. let requires_lp = iteration.variable::<((Loan, Point), Region)>("requires_lp"); - let killed = iteration.variable::<((Loan, Point), ())>("killed"); + let loan_killed_at = iteration.variable::<((Loan, Point), ())>("loan_killed_at"); let cfg_edge_p = iteration.variable::<(Point, Point)>("cfg_edge_p"); let origin_live_on_entry = iteration.variable::<((Region, Point), ())>("origin_live_on_entry"); let subset_r1p = iteration.variable::<((Region, Point), Region)>("subset_r1p"); @@ -2084,16 +2075,16 @@ impl AdditionalFacts { let zombie_requires_4 = iteration.variable_indistinct("zombie_requires_4"); // Load initial facts. - requires_lp.insert(Relation::from_iter(output.restricts.iter().flat_map( + requires_lp.insert(Relation::from_iter(output.origin_contains_loan_at.iter().flat_map( |(&point, region_map)| { region_map.iter().flat_map(move |(®ion, loans)| { loans.iter().map(move |&loan| ((loan, point), region)) }) }, ))); - killed.insert(Relation::from_iter( + loan_killed_at.insert(Relation::from_iter( all_facts - .killed + .loan_killed_at .iter() .map(|&(loan, point)| ((loan, point), ())), )); @@ -2139,10 +2130,10 @@ impl AdditionalFacts { // zombie_requires(R, L, Q) :- // requires(R, L, P), - // killed(L, P), + // loan_killed_at(L, P), // cfg_edge(P, Q), // origin_live_on_entry(R, Q). - zombie_requires_1.from_join(&requires_lp, &killed, |&(l, p), &r, _| (p, (l, r))); + zombie_requires_1.from_join(&requires_lp, &loan_killed_at, |&(l, p), &r, _| (p, (l, r))); zombie_requires_2.from_join(&zombie_requires_1, &cfg_edge_p, |&_p, &(l, r), &q| { ((r, q), l) }); @@ -2231,9 +2222,9 @@ impl AdditionalFacts { let (zombie_requires, zombie_borrow_live_at, borrow_become_zombie_at) = Self::derive_zombie_requires(all_facts, output); - let restricts = output.restricts.iter().chain(zombie_requires.iter()); - let borrow_regions = all_facts.borrow_region.iter(); - let reborrows = Self::load_reborrows(restricts, borrow_regions, incompatible_loans); + let origin_contains_loan_at = output.origin_contains_loan_at.iter().chain(zombie_requires.iter()); + let loan_issued_ats = all_facts.loan_issued_at.iter(); + let reborrows = Self::load_reborrows(origin_contains_loan_at, loan_issued_ats, incompatible_loans); let mut reborrows = Self::transitive_closure(reborrows); @@ -2244,7 +2235,7 @@ impl AdditionalFacts { let reborrows_direct = Self::derive_nontransitive(&reborrows); // Compute the sorted list of all loans. - let mut loans: Vec<_> = all_facts.borrow_region.iter().map(|&(_, l, _)| l).collect(); + let mut loans: Vec<_> = all_facts.loan_issued_at.iter().map(|&(_, l, _)| l).collect(); loans.sort(); AdditionalFacts { @@ -2254,11 +2245,11 @@ impl AdditionalFacts { } fn load_reborrows<'a>( - restricts: impl Iterator> )>, - borrow_regions: impl Iterator("reborrows"); // Variables for initial data. - let v_restricts = iteration.variable::<((Point, Region), Loan)>("restricts"); - let v_borrow_region = iteration.variable::<((Point, Region), Loan)>("borrow_region"); + let v_restricts = iteration.variable::<((Point, Region), Loan)>("origin_contains_loan_at"); + let v_loan_issued_at = iteration.variable::<((Point, Region), Loan)>("loan_issued_at"); // Load initial data. - let restricts_items = restricts.flat_map(|(&point, region_map)| + let restricts_items = origin_contains_loan_at.flat_map(|(&point, region_map)| region_map.iter().flat_map(move |(®ion, loans)| loans.iter().map(move |&loan| ((point, region), loan)))); v_restricts.insert(datafrog::Relation::from_iter(restricts_items)); - let borrow_region_items = borrow_regions.map(|&(r, l, p)| ((p, r), l)); - v_borrow_region.insert(datafrog::Relation::from_iter(borrow_region_items)); + let loan_issued_at_items = loan_issued_ats.map(|&(r, l, p)| ((p, r), l)); + v_loan_issued_at.insert(datafrog::Relation::from_iter(loan_issued_at_items)); while iteration.changed() { // reborrows(L1, L2) :- - // borrow_region(R, L1, P), - // restricts(R, P, L2). - v_reborrows.from_join(&v_borrow_region, &v_restricts, |_, &l1, &l2| (l1, l2)); + // loan_issued_at(R, L1, P), + // origin_contains_loan_at(R, P, L2). + v_reborrows.from_join(&v_loan_issued_at, &v_restricts, |_, &l1, &l2| (l1, l2)); } let mut reborrows = v_reborrows.complete().elements; @@ -2299,7 +2290,7 @@ impl AdditionalFacts { // creates two (fake) loans (if the fields of _3 are references) that are associated with // the same program location. Assume these two loans are L0 and L1 and include regions R1 // and R2, respectively. When R1 and R2 must be equal due to later constraints in the - // program, both R1 and R2 restrict both loans (as defined by the restricts relation). This + // program, both R1 and R2 restrict both loans (as defined by the origin_contains_loan_at relation). This // means we will infer reborrows(L1, L2) and reborrows(L2, L1), even though neither loan // reborrows the other. This would not happen if L1 and L2 were created at different // program locations, which is why this problem is unique to references in tuples. diff --git a/prusti-interface/src/environment/procedure.rs b/prusti-interface/src/environment/procedure.rs index 8cb583e3408..2547dfbfc1e 100644 --- a/prusti-interface/src/environment/procedure.rs +++ b/prusti-interface/src/environment/procedure.rs @@ -10,6 +10,7 @@ use rustc_middle::mir::{self, Body as Mir, Rvalue, AggregateKind}; use rustc_middle::mir::{BasicBlock, BasicBlockData, Terminator, TerminatorKind}; use rustc_middle::ty::{self, Ty, TyCtxt}; use std::cell::Ref; +use std::rc::Rc; use std::collections::{HashSet, HashMap}; use rustc_span::Span; use log::{trace, debug}; @@ -17,28 +18,29 @@ use rustc_middle::mir::StatementKind; use rustc_hir::def_id; use std::iter::FromIterator; use crate::environment::mir_utils::RealEdges; +use crate::environment::Environment; /// Index of a Basic Block pub type BasicBlockIndex = mir::BasicBlock; /// A facade that provides information about the Rust procedure. -pub struct Procedure<'a, 'tcx: 'a> { +pub struct Procedure<'tcx> { tcx: TyCtxt<'tcx>, proc_def_id: ProcedureDefId, - mir: Ref<'a, Mir<'tcx>>, + mir: Rc>, real_edges: RealEdges, loop_info: loops::ProcedureLoops, reachable_basic_blocks: HashSet, nonspec_basic_blocks: HashSet, } -impl<'a, 'tcx> Procedure<'a, 'tcx> { +impl<'tcx> Procedure<'tcx> { /// Builds an implementation of the Procedure interface, given a typing context and the /// identifier of a procedure - pub fn new(tcx: TyCtxt<'tcx>, proc_def_id: ProcedureDefId) -> Self { + pub fn new(env: &Environment<'tcx>, proc_def_id: ProcedureDefId) -> Self { trace!("Encoding procedure {:?}", proc_def_id); - let (mir, _) = tcx.mir_promoted(ty::WithOptConstParam::unknown(proc_def_id.expect_local())); - let mir = mir.borrow(); + let tcx = env.tcx(); + let mir = env.local_mir(proc_def_id.expect_local()); let real_edges = RealEdges::new(&mir); let reachable_basic_blocks = build_reachable_basic_blocks(&mir, &real_edges); let nonspec_basic_blocks = build_nonspec_basic_blocks(&mir, &real_edges, &tcx); diff --git a/prusti-interface/src/lib.rs b/prusti-interface/src/lib.rs index 838d185a983..97faf614699 100644 --- a/prusti-interface/src/lib.rs +++ b/prusti-interface/src/lib.rs @@ -8,6 +8,7 @@ #![allow(unused_imports)] #![deny(unused_must_use)] +#![deny(unsafe_op_in_unsafe_fn)] // #![deny(unused_imports)] // #![deny(unused_mut)] @@ -26,12 +27,14 @@ extern crate config as config_crate; extern crate rustc_hir; extern crate rustc_middle; +extern crate rustc_mir; extern crate rustc_span; extern crate rustc_ast; extern crate rustc_attr; extern crate rustc_data_structures; extern crate rustc_index; extern crate rustc_trait_selection; +extern crate polonius_engine; #[macro_use] extern crate lazy_static; diff --git a/prusti-interface/src/specs/mod.rs b/prusti-interface/src/specs/mod.rs index d9ee179d001..605523913e8 100644 --- a/prusti-interface/src/specs/mod.rs +++ b/prusti-interface/src/specs/mod.rs @@ -50,8 +50,9 @@ struct ProcedureSpecRef { /// HIR. After the visit, [determine_def_specs] can be used to get back /// a mapping of DefIds (which may not be local due to extern specs) to their /// [SpecificationSet], i.e. procedures, loop invariants, and structs. -pub struct SpecCollector<'tcx> { +pub struct SpecCollector<'a, 'tcx: 'a> { tcx: TyCtxt<'tcx>, + env: &'a Environment<'tcx>, extern_resolver: ExternSpecResolver<'tcx>, /// Collected assertions before deserialisation. @@ -67,16 +68,17 @@ pub struct SpecCollector<'tcx> { loop_specs: HashMap>, } -impl<'tcx> SpecCollector<'tcx> { - pub fn new(tcx: TyCtxt<'tcx>) -> Self { +impl<'a, 'tcx> SpecCollector<'a, 'tcx> { + pub fn new(env: &'a Environment<'tcx>) -> Self { Self { - tcx: tcx, + tcx: env.tcx(), + env, spec_items: Vec::new(), typed_specs: HashMap::new(), procedure_specs: HashMap::new(), loop_specs: HashMap::new(), typed_expressions: HashMap::new(), - extern_resolver: ExternSpecResolver::new(tcx), + extern_resolver: ExternSpecResolver::new(env.tcx()), } } @@ -88,7 +90,7 @@ impl<'tcx> SpecCollector<'tcx> { let assertion = reconstruct_typed_assertion( spec_item.specification, &self.typed_expressions, - self.tcx + self.env ); (spec_item.spec_id, assertion) }) @@ -239,9 +241,9 @@ fn get_procedure_spec_ids(def_id: DefId, attrs: &[ast::Attribute]) -> Option( assertion: JsonAssertion, typed_expressions: &HashMap, - tcx: TyCtxt<'tcx> + env: &Environment<'tcx> ) -> typed::Assertion<'tcx> { - assertion.to_typed(typed_expressions, tcx) + assertion.to_typed(typed_expressions, env) } fn deserialize_spec_from_attrs(attrs: &[ast::Attribute]) -> JsonAssertion { @@ -250,7 +252,7 @@ fn deserialize_spec_from_attrs(attrs: &[ast::Attribute]) -> JsonAssertion { JsonAssertion::from_json_string(&json_string) } -impl<'tcx> intravisit::Visitor<'tcx> for SpecCollector<'tcx> { +impl<'a, 'tcx> intravisit::Visitor<'tcx> for SpecCollector<'a, 'tcx> { type Map = Map<'tcx>; fn nested_visit_map(&mut self) -> intravisit::NestedVisitorMap { diff --git a/prusti-interface/src/specs/typed.rs b/prusti-interface/src/specs/typed.rs index ec7c4eab5d6..2fa62248a6b 100644 --- a/prusti-interface/src/specs/typed.rs +++ b/prusti-interface/src/specs/typed.rs @@ -8,6 +8,7 @@ use std::collections::HashMap; pub use common::{ExpressionId, SpecType, SpecificationId, SpecIdRef}; use crate::data::ProcedureDefId; +use crate::environment::Environment; // FIXME: these comments are not terribly useful and are a copy of the untyped ones... /// A specification that has no types associated with it. @@ -140,11 +141,15 @@ impl<'tcx> Spanned<'tcx> for Assertion<'tcx> { } pub trait StructuralToTyped<'tcx, Target> { - fn to_typed(self, typed_expressions: &HashMap, tcx: TyCtxt<'tcx>) -> Target; + fn to_typed( + self, + typed_expressions: &HashMap, + env: &Environment<'tcx>, + ) -> Target; } impl<'tcx> StructuralToTyped<'tcx, Expression> for json::Expression { - fn to_typed(self, typed_expressions: &HashMap, _tcx: TyCtxt<'tcx>) -> Expression { + fn to_typed(self, typed_expressions: &HashMap, _env: &Environment<'tcx>) -> Expression { let local_id = typed_expressions[&format!("{}_{}", self.spec_id, self.expr_id)]; Expression { spec_id: self.spec_id, @@ -155,32 +160,35 @@ impl<'tcx> StructuralToTyped<'tcx, Expression> for json::Expression { } impl<'tcx> StructuralToTyped<'tcx, TriggerSet> for json::TriggerSet { - fn to_typed(self, typed_expressions: &HashMap, tcx: TyCtxt<'tcx>) -> TriggerSet { + fn to_typed(self, typed_expressions: &HashMap, env: &Environment<'tcx>) -> TriggerSet { common::TriggerSet( self.0 .into_iter() - .map(|x| x.to_typed(typed_expressions, tcx)) + .map(|x| x.to_typed(typed_expressions, env)) .collect() ) } } impl<'tcx> StructuralToTyped<'tcx, Trigger> for json::Trigger { - fn to_typed(self, typed_expressions: &HashMap, tcx: TyCtxt<'tcx>) -> Trigger { + fn to_typed(self, typed_expressions: &HashMap, env: &Environment<'tcx>) -> Trigger { common::Trigger( self.0 .into_iter() - .map(|x| x.to_typed(typed_expressions, tcx)) + .map(|x| x.to_typed(typed_expressions, env)) .collect() ) } } impl<'tcx> StructuralToTyped<'tcx, QuantifierVars<'tcx>> for json::QuantifierVars { - fn to_typed(self, typed_expressions: &HashMap, tcx: TyCtxt<'tcx>) -> QuantifierVars<'tcx> { + fn to_typed( + self, + typed_expressions: &HashMap, + env: &Environment<'tcx>, + ) -> QuantifierVars<'tcx> { let local_id = typed_expressions[&format!("{}_{}", self.spec_id, self.expr_id)]; - let (body, _) = tcx.mir_promoted(ty::WithOptConstParam::unknown(local_id)); - let body = body.borrow(); + let body = env.local_mir(local_id); // the first argument to the node is the closure itself and the // following ones are the variables; therefore, we need to skip @@ -205,13 +213,15 @@ impl<'tcx> StructuralToTyped<'tcx, QuantifierVars<'tcx>> for json::QuantifierVar } impl<'tcx> StructuralToTyped<'tcx, SpecEntailmentVars<'tcx>> for json::SpecEntailmentVars { - fn to_typed(self, typed_expressions: &HashMap, tcx: TyCtxt<'tcx>) -> SpecEntailmentVars<'tcx> { + fn to_typed( + self, + typed_expressions: &HashMap, + env: &Environment<'tcx> + ) -> SpecEntailmentVars<'tcx> { let local_pre_id = typed_expressions[&format!("{}_{}", self.spec_id, self.pre_expr_id)]; let local_post_id = typed_expressions[&format!("{}_{}", self.spec_id, self.post_expr_id)]; - let (pre_body, _) = tcx.mir_promoted(ty::WithOptConstParam::unknown(local_pre_id)); - let (post_body, _) = tcx.mir_promoted(ty::WithOptConstParam::unknown(local_post_id)); - let pre_body = pre_body.borrow(); - let post_body = post_body.borrow(); + let pre_body = env.local_mir(local_pre_id); + let post_body = env.local_mir(local_post_id); let pre_args: Vec<(mir::Local, ty::Ty)> = pre_body .args_iter() @@ -245,37 +255,37 @@ impl<'tcx> StructuralToTyped<'tcx, SpecEntailmentVars<'tcx>> for json::SpecEntai } impl<'tcx> StructuralToTyped<'tcx, AssertionKind<'tcx>> for json::AssertionKind { - fn to_typed(self, typed_expressions: &HashMap, tcx: TyCtxt<'tcx>) -> AssertionKind<'tcx> { + fn to_typed(self, typed_expressions: &HashMap, env: &Environment<'tcx>) -> AssertionKind<'tcx> { use json::AssertionKind::*; match self { - Expr(expr) => AssertionKind::Expr(expr.to_typed(typed_expressions, tcx)), + Expr(expr) => AssertionKind::Expr(expr.to_typed(typed_expressions, env)), And(assertions) => AssertionKind::And( assertions.into_iter() - .map(|assertion| assertion.to_typed(typed_expressions, tcx)) + .map(|assertion| assertion.to_typed(typed_expressions, env)) .collect() ), Implies(lhs, rhs) => AssertionKind::Implies( - lhs.to_typed(typed_expressions, tcx), - rhs.to_typed(typed_expressions, tcx) + lhs.to_typed(typed_expressions, env), + rhs.to_typed(typed_expressions, env) ), ForAll(vars, body, triggers) => AssertionKind::ForAll( - vars.to_typed(typed_expressions, tcx), - triggers.to_typed(typed_expressions, tcx), - body.to_typed(typed_expressions, tcx), + vars.to_typed(typed_expressions, env), + triggers.to_typed(typed_expressions, env), + body.to_typed(typed_expressions, env), ), Exists(vars, body, triggers) => AssertionKind::Exists( - vars.to_typed(typed_expressions, tcx), - triggers.to_typed(typed_expressions, tcx), - body.to_typed(typed_expressions, tcx), + vars.to_typed(typed_expressions, env), + triggers.to_typed(typed_expressions, env), + body.to_typed(typed_expressions, env), ), SpecEntailment {closure, arg_binders, pres, posts} => AssertionKind::SpecEntailment { - closure: closure.to_typed(typed_expressions, tcx), - arg_binders: arg_binders.to_typed(typed_expressions, tcx), + closure: closure.to_typed(typed_expressions, env), + arg_binders: arg_binders.to_typed(typed_expressions, env), pres: pres.into_iter() - .map(|pre| pre.to_typed(typed_expressions, tcx)) + .map(|pre| pre.to_typed(typed_expressions, env)) .collect(), posts: posts.into_iter() - .map(|post| post.to_typed(typed_expressions, tcx)) + .map(|post| post.to_typed(typed_expressions, env)) .collect(), }, } @@ -283,9 +293,9 @@ impl<'tcx> StructuralToTyped<'tcx, AssertionKind<'tcx>> for json::AssertionKind } impl<'tcx> StructuralToTyped<'tcx, Assertion<'tcx>> for json::Assertion { - fn to_typed(self, typed_expressions: &HashMap, tcx: TyCtxt<'tcx>) -> Assertion<'tcx> { + fn to_typed(self, typed_expressions: &HashMap, env: &Environment<'tcx>) -> Assertion<'tcx> { Assertion { - kind: box self.kind.to_typed(typed_expressions, tcx), + kind: box self.kind.to_typed(typed_expressions, env), } } } diff --git a/prusti-tests/tests/verify/pass/arrays/static_const.rs b/prusti-tests/tests/verify/pass/arrays/static_const.rs new file mode 100644 index 00000000000..0426873ab39 --- /dev/null +++ b/prusti-tests/tests/verify/pass/arrays/static_const.rs @@ -0,0 +1,11 @@ +use prusti_contracts::*; + +#[ensures(result == 1)] +const fn foo() -> usize { + 1 +} + +fn main() { + let bar: [usize; foo()] = [1]; + assert!(bar[0] == foo()); +} diff --git a/prusti-viper/src/encoder/borrows.rs b/prusti-viper/src/encoder/borrows.rs index 29dd2e4ceeb..08d47c81574 100644 --- a/prusti-viper/src/encoder/borrows.rs +++ b/prusti-viper/src/encoder/borrows.rs @@ -6,6 +6,7 @@ use crate::encoder::places; use prusti_interface::data::ProcedureDefId; +use prusti_interface::environment::Environment; // use prusti_interface::specifications::{ // AssertionKind, SpecificationSet, TypedAssertion, TypedExpression, TypedSpecification, // TypedSpecificationSet, @@ -289,6 +290,7 @@ impl<'tcx> BorrowInfoCollectingVisitor<'tcx> { ), &ty::RegionKind::ReStatic => None, &ty::RegionKind::ReErased => None, + &ty::RegionKind::ReVar(_) => None, // &ty::RegionKind::ReScope(_scope) => None, x => unimplemented!("{:?}", x), } @@ -419,7 +421,7 @@ impl<'tcx> TypeVisitor<'tcx> for BorrowInfoCollectingVisitor<'tcx> { pub fn compute_procedure_contract<'p, 'a, 'tcx>( proc_def_id: ProcedureDefId, - tcx: TyCtxt<'tcx>, + env: &Environment<'tcx>, specification: typed::SpecificationSet<'tcx>, maybe_tymap: Option<&HashMap, ty::Ty<'tcx>>>, ) -> EncodingResult> @@ -432,10 +434,10 @@ where let args_ty:Vec<(mir::Local, ty::Ty<'tcx>)>; let return_ty; - if !tcx.is_closure(proc_def_id) { + if !env.tcx().is_closure(proc_def_id) { // FIXME: "skip_binder" is most likely wrong // FIXME: Replace with FakeMirEncoder. - let fn_sig: FnSig = tcx.fn_sig(proc_def_id).skip_binder(); + let fn_sig: FnSig = env.tcx().fn_sig(proc_def_id).skip_binder(); if fn_sig.c_variadic { return Err(EncodingError::unsupported( "variadic functions are not supported" @@ -446,8 +448,7 @@ where .collect(); return_ty = fn_sig.output(); // FIXME: Shouldn't this also go through maybe_tymap? } else { - let (mir, _) = tcx.mir_promoted(ty::WithOptConstParam::unknown(proc_def_id.expect_local())); - let mir = mir.borrow(); + let mir = env.local_mir(proc_def_id.expect_local()); // local_decls: // _0 - return, with closure's return type // _1 - closure's self @@ -471,7 +472,7 @@ where }); } - let mut visitor = BorrowInfoCollectingVisitor::new(tcx); + let mut visitor = BorrowInfoCollectingVisitor::new(env.tcx()); for (arg, arg_ty) in fake_mir_args.iter().zip(fake_mir_args_ty) { visitor.analyse_arg(*arg, arg_ty)?; } diff --git a/prusti-viper/src/encoder/encoder.rs b/prusti-viper/src/encoder/encoder.rs index a8806a337a7..867c78650c7 100644 --- a/prusti-viper/src/encoder/encoder.rs +++ b/prusti-viper/src/encoder/encoder.rs @@ -371,7 +371,7 @@ impl<'v, 'tcx> Encoder<'v, 'tcx> { self.get_procedure_specs(proc_def_id) .unwrap_or_else(|| typed::ProcedureSpecification::empty()) ); - compute_procedure_contract(proc_def_id, self.env().tcx(), spec, None) + compute_procedure_contract(proc_def_id, self.env(), spec, None) } /// Extract scalar value, invoking const evaluation if necessary. @@ -469,7 +469,7 @@ impl<'v, 'tcx> Encoder<'v, 'tcx> { let contract = compute_procedure_contract( proc_def_id, - self.env().tcx(), + self.env(), typed::SpecificationSet::Procedure(final_spec), Some(&tymap[0]) )?; @@ -862,6 +862,7 @@ impl<'v, 'tcx> Encoder<'v, 'tcx> { /// by either being a primitive type or by deriving the Eq trait. pub fn has_structural_eq_impl(&self, ty: ty::Ty<'tcx>) -> bool { let ty = ty.peel_refs(); + let ty = self.env().tcx().erase_regions_ty(ty); match ty.kind() { ty::TyKind::Bool | ty::TyKind::Int(_) diff --git a/prusti-viper/src/encoder/loop_encoder.rs b/prusti-viper/src/encoder/loop_encoder.rs index 8672e661f02..11531d85847 100644 --- a/prusti-viper/src/encoder/loop_encoder.rs +++ b/prusti-viper/src/encoder/loop_encoder.rs @@ -18,14 +18,14 @@ pub enum LoopEncoderError { } pub struct LoopEncoder<'p, 'tcx: 'p> { - procedure: &'p Procedure<'p, 'tcx>, + procedure: &'p Procedure<'tcx>, tcx: ty::TyCtxt<'tcx>, initialization: DefinitelyInitializedAnalysisResult<'tcx>, } impl<'p, 'tcx: 'p> LoopEncoder<'p, 'tcx> { pub fn new( - procedure: &'p Procedure<'p, 'tcx>, + procedure: &'p Procedure<'tcx>, tcx: ty::TyCtxt<'tcx>, ) -> Self { LoopEncoder { diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 46b1c172f4a..70fe9fe3617 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -72,7 +72,7 @@ use std::convert::TryInto; pub struct ProcedureEncoder<'p, 'v: 'p, 'tcx: 'v> { encoder: &'p Encoder<'v, 'tcx>, proc_def_id: ProcedureDefId, - procedure: &'p Procedure<'p, 'tcx>, + procedure: &'p Procedure<'tcx>, mir: &'p mir::Body<'tcx>, cfg_method: vir::CfgMethod, locals: LocalVariableManager<'tcx>, @@ -116,7 +116,7 @@ pub struct ProcedureEncoder<'p, 'v: 'p, 'tcx: 'v> { impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { pub fn new( encoder: &'p Encoder<'v, 'tcx>, - procedure: &'p Procedure<'p, 'tcx> + procedure: &'p Procedure<'tcx> ) -> SpannedEncodingResult { debug!("ProcedureEncoder constructor"); @@ -365,7 +365,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { // Load Polonius info self.polonius_info = Some( - PoloniusInfo::new(&self.procedure, &self.cached_loop_invariant_block) + PoloniusInfo::new(self.encoder.env(), &self.procedure, &self.cached_loop_invariant_block) .map_err(|err| self.translate_polonius_error(err))?, ); @@ -475,7 +475,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { .polonius_info() .loan_locations() .iter() - .map(|(loan, location)| (loan.into(), *location)) + .map(|(loan, location)| (loan.index().into(), *location)) .collect(); let method_pos = self .encoder @@ -1575,7 +1575,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { let guard = self.construct_location_guard(loan_location); vir::borrows::Node::new( guard, - node.loan.into(), + node.loan.index().into(), convert_loans_to_borrows(&node.reborrowing_loans), convert_loans_to_borrows(&node.reborrowed_loans), Vec::new(), @@ -1682,7 +1682,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { Ok(vir::borrows::Node::new( guard, - node.loan.into(), + node.loan.index().into(), convert_loans_to_borrows(&node.reborrowing_loans), convert_loans_to_borrows(&node.reborrowed_loans), self.set_stmts_default_pos(stmts, span), @@ -1781,19 +1781,19 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { let magic_wand = vir::Expr::MagicWand( box lhs.clone(), box rhs.clone(), - Some(loan.into()), + Some(loan.index().into()), pos, ); stmts.push(vir::Stmt::Inhale(magic_wand)); // Emit the apply statement. - let statement = vir::Stmt::apply_magic_wand(lhs, rhs, loan.into(), pos); + let statement = vir::Stmt::apply_magic_wand(lhs, rhs, loan.index().into(), pos); debug!("{:?} at {:?}", statement, loan_location); stmts.push(statement); let guard = self.construct_location_guard(loan_location); Ok(vir::borrows::Node::new( guard, - node.loan.into(), + node.loan.index().into(), convert_loans_to_borrows(&node.reborrowing_loans), convert_loans_to_borrows(&node.reborrowed_loans), stmts, @@ -3598,7 +3598,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { self.magic_wand_at_location .insert(location, (post_label.to_string(), lhs.clone(), rhs.clone())); } - magic_wands.push(vir::Expr::magic_wand(lhs, rhs, loan.map(|l| l.into()))); + magic_wands.push(vir::Expr::magic_wand(lhs, rhs, loan.map(|l| l.index().into()))); } // Encode permissions for return type @@ -4681,8 +4681,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { kind => unreachable!("Only calls are expected. Found: {:?}", kind), } } else { - let ref_mir = self.encoder.env().local_mir(containing_def_id.expect_local()); - let mir = ref_mir.borrow(); + let mir = self.encoder.env().local_mir(containing_def_id.expect_local()); let return_ty = mir.return_ty(); let arg_tys = mir.args_iter().map(|arg| mir.local_decls[arg].ty).collect(); FakeMirEncoder::new(self.encoder, arg_tys, Some(return_ty)) @@ -4916,12 +4915,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { lhs.clone(), ref_field.clone(), location, - vir::AssignKind::SharedBorrow(loan.into()), + vir::AssignKind::SharedBorrow(loan.index().into()), )?; stmts.push(vir::Stmt::Assign( lhs.clone().field(ref_field.clone()), src.field(ref_field), - vir::AssignKind::SharedBorrow(loan.into()), + vir::AssignKind::SharedBorrow(loan.index().into()), )); stmts } @@ -5272,7 +5271,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { let loan = self.polonius_info().get_loan_at_location(location); let (vir_assign_kind, array_encode_kind) = match mir_borrow_kind { mir::BorrowKind::Shared => - (vir::AssignKind::SharedBorrow(loan.into()), ArrayAccessKind::Shared), + (vir::AssignKind::SharedBorrow(loan.index().into()), ArrayAccessKind::Shared), mir::BorrowKind::Unique => { return Err(EncodingError::unsupported( "unsuported creation of unique borrows (implicitly created in closure bindings)" @@ -5284,7 +5283,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { )).with_span(span); } mir::BorrowKind::Mut { .. } => - (vir::AssignKind::MutableBorrow(loan.into()), ArrayAccessKind::Mutable(Some(loan.into()), location)), + (vir::AssignKind::MutableBorrow(loan.index().into()), ArrayAccessKind::Mutable(Some(loan.index().into()), location)), }; let (encoded_value, mut stmts, _, _) = self.encode_place(place, array_encode_kind).with_span(span)?; // Initialize ref_var.ref_field @@ -6107,7 +6106,7 @@ enum ArrayAccessKind { } fn convert_loans_to_borrows(loans: &[facts::Loan]) -> Vec { - loans.iter().map(|l| l.into()).collect() + loans.iter().map(|l| l.index().into()).collect() } /// Check if size of ProcedureContract::borrow_infos is as required diff --git a/prusti-viper/src/encoder/spec_function_encoder.rs b/prusti-viper/src/encoder/spec_function_encoder.rs index 3bbd53316ed..a5e5ac431d5 100644 --- a/prusti-viper/src/encoder/spec_function_encoder.rs +++ b/prusti-viper/src/encoder/spec_function_encoder.rs @@ -25,7 +25,7 @@ pub enum SpecFunctionKind { pub struct SpecFunctionEncoder<'p, 'v: 'p, 'tcx: 'v> { encoder: &'p Encoder<'v, 'tcx>, - procedure: &'p Procedure<'p, 'tcx>, + procedure: &'p Procedure<'tcx>, span: Span, proc_def_id: ProcedureDefId, is_closure: bool, @@ -35,7 +35,7 @@ pub struct SpecFunctionEncoder<'p, 'v: 'p, 'tcx: 'v> { impl<'p, 'v: 'p, 'tcx: 'v> SpecFunctionEncoder<'p, 'v, 'tcx> { pub fn new(encoder: &'p Encoder<'v, 'tcx>, - procedure: &'p Procedure<'p, 'tcx>) -> Self { + procedure: &'p Procedure<'tcx>) -> Self { Self { encoder: encoder, procedure: procedure, @@ -61,7 +61,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> SpecFunctionEncoder<'p, 'v, 'tcx> { let contract = compute_procedure_contract( self.proc_def_id, - self.encoder.env().tcx(), + self.encoder.env(), typed::SpecificationSet::Procedure(specs), Some(&self.encoder.current_tymap()) ).with_span(self.span)?.to_def_site_contract(); diff --git a/prusti-viper/src/encoder/stub_procedure_encoder.rs b/prusti-viper/src/encoder/stub_procedure_encoder.rs index 4c734708caf..59174563f52 100644 --- a/prusti-viper/src/encoder/stub_procedure_encoder.rs +++ b/prusti-viper/src/encoder/stub_procedure_encoder.rs @@ -21,11 +21,11 @@ pub struct StubProcedureEncoder<'p, 'v: 'p, 'tcx: 'v> mir: &'p mir::Body<'tcx>, mir_encoder: MirEncoder<'p, 'v, 'tcx>, def_id: DefId, - procedure: &'p Procedure<'v, 'tcx>, + procedure: &'p Procedure<'tcx>, } impl<'p, 'v: 'p, 'tcx: 'v> StubProcedureEncoder<'p, 'v, 'tcx> { - pub fn new(encoder: &'p Encoder<'v, 'tcx>, procedure: &'p Procedure<'v, 'tcx>) -> Self { + pub fn new(encoder: &'p Encoder<'v, 'tcx>, procedure: &'p Procedure<'tcx>) -> Self { let def_id = procedure.get_id(); trace!("StubProcedureEncoder constructor: {:?}", def_id); diff --git a/prusti/src/callbacks.rs b/prusti/src/callbacks.rs index 99b0a2f8056..f13361837e3 100644 --- a/prusti/src/callbacks.rs +++ b/prusti/src/callbacks.rs @@ -1,16 +1,42 @@ -use prusti_interface::{specs, environment::Environment}; +use prusti_interface::{specs, environment::{Environment, mir_storage}}; use rustc_driver::Compilation; use rustc_hir::intravisit; use rustc_interface::interface::Compiler; -use rustc_interface::Queries; +use rustc_interface::{Queries, Config}; use regex::Regex; use prusti_common::config; use crate::verifier::verify; +use rustc_middle::ty::query::query_values::mir_borrowck; +use rustc_middle::ty::query::Providers; +use rustc_session::Session; +use rustc_hir::def_id::LocalDefId; +use rustc_middle::ty::{self, TyCtxt}; #[derive(Default)] pub struct PrustiCompilerCalls; +fn mir_borrowck<'tcx>(tcx: TyCtxt<'tcx>, def_id: LocalDefId) -> mir_borrowck<'tcx> { + let body_with_facts = rustc_mir::consumers::get_body_with_borrowck_facts( + tcx, ty::WithOptConstParam::unknown(def_id)); + // SAFETY: This is safe because we are feeding in the same `tcx` that is + // going to be used as a witness when pulling out the data. + unsafe { mir_storage::store_mir_body(tcx, def_id, body_with_facts); } + let mut providers = Providers::default(); + rustc_mir::provide(&mut providers); + let original_mir_borrowck = providers.mir_borrowck; + original_mir_borrowck(tcx, def_id) +} + +fn override_queries(_session: &Session, local: &mut Providers, external: &mut Providers) { + local.mir_borrowck = mir_borrowck; + external.mir_borrowck = mir_borrowck; +} + impl rustc_driver::Callbacks for PrustiCompilerCalls { + fn config(&mut self, config: &mut Config) { + assert!(config.override_queries.is_none()); + config.override_queries = Some(override_queries); + } fn after_expansion<'tcx>( &mut self, compiler: &Compiler, @@ -46,7 +72,7 @@ impl rustc_driver::Callbacks for PrustiCompilerCalls { spec_checker.report_errors(&env); compiler.session().abort_if_errors(); - let mut spec_collector = specs::SpecCollector::new(tcx); + let mut spec_collector = specs::SpecCollector::new(&env); intravisit::walk_crate(&mut spec_collector, &krate); let def_spec = spec_collector.build_def_specs(&env); if config::print_typeckd_specs() { diff --git a/prusti/src/driver.rs b/prusti/src/driver.rs index b4b9c79c7f3..1a7ce68b207 100644 --- a/prusti/src/driver.rs +++ b/prusti/src/driver.rs @@ -21,6 +21,7 @@ extern crate rustc_hir; extern crate rustc_interface; extern crate rustc_metadata; extern crate rustc_middle; +extern crate rustc_mir; extern crate rustc_parse; extern crate rustc_resolve; extern crate rustc_session; @@ -34,7 +35,7 @@ mod callbacks; mod verifier; mod arg_value; -use std::{env, panic, borrow::Cow, path::PathBuf}; +use std::{env, panic, borrow::Cow}; use prusti_common::report::user; use lazy_static::lazy_static; use callbacks::PrustiCompilerCalls; @@ -155,21 +156,7 @@ fn main() { info!("Prusti version: {}", get_prusti_version_info()); env::set_var("POLONIUS_ALGORITHM", "Naive"); - rustc_args.push("-Zborrowck=mir".to_owned()); rustc_args.push("-Zpolonius".to_owned()); - rustc_args.push("-Znll-facts".to_owned()); - rustc_args.push(format!( - "-Znll-facts-dir={}", - PathBuf::from(config::log_dir()).join("nll-facts").to_str() - .expect("failed to configure nll-facts-dir") - )); - rustc_args.push("-Zidentify-regions".to_owned()); - rustc_args.push(format!( - "-Zdump-mir-dir={}", - PathBuf::from(config::log_dir()).join("mir").to_str() - .expect("failed to configure dump-mir-dir") - )); - rustc_args.push("-Zdump-mir=renumber".to_owned()); rustc_args.push("-Zalways-encode-mir".to_owned()); rustc_args.push("-Zcrate-attr=feature(register_tool)".to_owned()); rustc_args.push("-Zcrate-attr=register_tool(prusti)".to_owned()); diff --git a/rust-toolchain b/rust-toolchain index 0674eb50e44..c331bd66965 100644 --- a/rust-toolchain +++ b/rust-toolchain @@ -1,4 +1,4 @@ [toolchain] -channel = "nightly-2021-08-15" +channel = "nightly-2021-08-19" components = [ "rustc-dev", "llvm-tools-preview" ] profile = "minimal" From daef46a2a1f3abfe46867db102bdf6cc63523f3a Mon Sep 17 00:00:00 2001 From: Vytautas Astrauskas Date: Thu, 19 Aug 2021 15:37:57 +0200 Subject: [PATCH 2/2] Try to make the counter-example UI test more deterministic. --- .../tests/verify/ui/counterexamples/loop.rs | 1 + .../verify/ui/counterexamples/loop.stderr | 36 +++++++++---------- 2 files changed, 19 insertions(+), 18 deletions(-) diff --git a/prusti-tests/tests/verify/ui/counterexamples/loop.rs b/prusti-tests/tests/verify/ui/counterexamples/loop.rs index b0734afc2a5..bcbf91abc4a 100644 --- a/prusti-tests/tests/verify/ui/counterexamples/loop.rs +++ b/prusti-tests/tests/verify/ui/counterexamples/loop.rs @@ -1,4 +1,5 @@ // compile-flags: -Pcounterexample=true +// normalize-stderr-test: "final value:\s*-?[0-9]+" -> "$(FINAL_VALUE)" use prusti_contracts::*; diff --git a/prusti-tests/tests/verify/ui/counterexamples/loop.stderr b/prusti-tests/tests/verify/ui/counterexamples/loop.stderr index ed356805380..b14c2ea1a05 100644 --- a/prusti-tests/tests/verify/ui/counterexamples/loop.stderr +++ b/prusti-tests/tests/verify/ui/counterexamples/loop.stderr @@ -1,37 +1,37 @@ error: [Prusti: verification error] postcondition might not hold. - --> $DIR/loop.rs:5:11 + --> $DIR/loop.rs:6:11 | -5 | #[ensures(result != 16)] +6 | #[ensures(result != 16)] | ^^^^^^^^^^^^ | note: the error originates here - --> $DIR/loop.rs:6:1 + --> $DIR/loop.rs:7:1 | -6 | / fn spurious() -> i32 { -7 | | let mut x = 10; -8 | | let mut y = 1; -9 | | while (x > 0) { +7 | / fn spurious() -> i32 { +8 | | let mut x = 10; +9 | | let mut y = 1; +10 | | while (x > 0) { ... | -16 | | y -17 | | } +17 | | y +18 | | } | |_^ note: counterexample for "x" - final value: 0 - --> $DIR/loop.rs:7:9 + $(FINAL_VALUE) + --> $DIR/loop.rs:8:9 | -7 | let mut x = 10; +8 | let mut x = 10; | ^^^^^ note: counterexample for "y" - final value: 16 - --> $DIR/loop.rs:8:9 + $(FINAL_VALUE) + --> $DIR/loop.rs:9:9 | -8 | let mut y = 1; +9 | let mut y = 1; | ^^^^^ note: counterexample for result - final value: 16 - --> $DIR/loop.rs:6:18 + $(FINAL_VALUE) + --> $DIR/loop.rs:7:18 | -6 | fn spurious() -> i32 { +7 | fn spurious() -> i32 { | ^^^ error: aborting due to previous error