Skip to content

Commit

Permalink
Merge #882
Browse files Browse the repository at this point in the history 
882: Small fixes r=Aurel300 a=JonasAlaif

Kinda fixes #878 but would prefer if `@vakaras` looked at it/made it less hacky

Co-authored-by: Jonas <jonas.fiala.cardiff@gmail.com>
Co-authored-by: Aurel Bílý <aurel.bily@gmail.com>
  • Loading branch information
@bors @JonasAlaif @Aurel300
3 people authored Apr 11, 2022
2 parents f704d86 + 0a96d54 commit 36b94f7
Show file tree
Hide file tree
Showing 45 changed files with 626 additions and 460 deletions.
46 changes: 36 additions & 10 deletions prusti-interface/src/environment/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,11 +61,19 @@ struct CachedBody<'tcx> {
borrowck_facts: Rc<BorrowckFacts>,
}

struct CachedExternalBody<'tcx> {
/// MIR body as known to the compiler.
base_body: Rc<mir::Body<'tcx>>,
/// Copies of the MIR body with the given substs applied.
monomorphised_bodies: HashMap<SubstsRef<'tcx>, Rc<mir::Body<'tcx>>>,
}

/// Facade to the Rust compiler.
// #[derive(Copy, Clone)]
pub struct Environment<'tcx> {
/// Cached MIR bodies.
bodies: RefCell<HashMap<LocalDefId, CachedBody<'tcx>>>,
external_bodies: RefCell<HashMap<DefId, CachedExternalBody<'tcx>>>,
tcx: TyCtxt<'tcx>,
}

Expand All @@ -75,6 +83,7 @@ impl<'tcx> Environment<'tcx> {
Environment {
tcx,
bodies: RefCell::new(HashMap::new()),
external_bodies: RefCell::new(HashMap::new()),
}
}

Expand Down Expand Up @@ -300,8 +309,28 @@ impl<'tcx> Environment<'tcx> {
}

/// Get the MIR body of an external procedure.
pub fn external_mir<'a>(&self, def_id: DefId) -> &'a mir::Body<'tcx> {
self.tcx().optimized_mir(def_id)
pub fn external_mir(
&self,
def_id: DefId,
substs: SubstsRef<'tcx>,
) -> Rc<mir::Body<'tcx>> {
let mut bodies = self.external_bodies.borrow_mut();
let body = bodies.entry(def_id)
.or_insert_with(|| {
let body = self.tcx.optimized_mir(def_id);
CachedExternalBody {
base_body: Rc::new(body.clone()),
monomorphised_bodies: HashMap::new(),
}
});
body
.monomorphised_bodies
.entry(substs)
.or_insert_with(|| {
use crate::rustc_middle::ty::subst::Subst;
body.base_body.clone().subst(self.tcx, substs)
})
.clone()
}

/// Get all relevant trait declarations for some type.
Expand Down Expand Up @@ -456,14 +485,11 @@ impl<'tcx> Environment<'tcx> {
}

let param_env = self.tcx.param_env(caller_def_id);
let instance = self.tcx
.resolve_instance(param_env.and((called_def_id, call_substs)))
.unwrap();
if let Some(instance) = instance {
(instance.def_id(), instance.substs)
} else {
(called_def_id, call_substs)
}
traits::resolve_instance(self.tcx, param_env.and((called_def_id, call_substs)))
.map(|opt_instance| opt_instance
.map(|instance| (instance.def_id(), instance.substs))
.unwrap_or((called_def_id, call_substs)))
.unwrap_or((called_def_id, call_substs))
}

pub fn type_is_allowed_in_pure_functions(&self, ty: ty::Ty<'tcx>, param_env: ty::ParamEnv<'tcx>) -> bool {
Expand Down
26 changes: 12 additions & 14 deletions prusti-interface/src/specs/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ pub struct SpecCollector<'a, 'tcx: 'a> {

/// Map from functions/loops and their specifications.
procedure_specs: HashMap<LocalDefId, ProcedureSpecRefs>,
loop_specs: Vec<LocalDefId>, // HashMap<LocalDefId, Vec<SpecificationId>>,
loop_specs: Vec<LocalDefId>,
}

impl<'a, 'tcx> SpecCollector<'a, 'tcx> {
Expand Down Expand Up @@ -116,8 +116,9 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> {
let kind = SpecificationItem::Inherent(kind);

def_spec.specs.insert(
*local_id,
local_id.to_def_id(),
typed::SpecificationSet::Procedure(typed::ProcedureSpecification {
span: Some(self.env.get_def_span(local_id.to_def_id())),
pres,
posts,
pledges,
Expand All @@ -133,25 +134,22 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> {
for (extern_spec_decl, spec_id) in self.extern_resolver.extern_fn_map.iter() {
let target_def_id = extern_spec_decl.get_target_def_id();

if let Some(local_id) = target_def_id.as_local() {
if def_spec.specs.contains_key(&local_id) {
PrustiError::incorrect(
format!("external specification provided for {}, which already has a specification",
self.env.get_item_name(target_def_id)),
MultiSpan::from_span(self.env.get_def_span(*spec_id)),
).emit(self.env);
}
if def_spec.specs.contains_key(&target_def_id) {
PrustiError::incorrect(
format!("external specification provided for {}, which already has a specification",
self.env.get_item_name(target_def_id)),
MultiSpan::from_span(self.env.get_def_span(*spec_id)),
).emit(self.env);
}

if def_spec.specs.get(&spec_id.expect_local()).is_some() {
def_spec.extern_specs.insert(target_def_id, spec_id.expect_local());
}
let spec = def_spec.specs.remove(spec_id).unwrap();
def_spec.specs.insert(target_def_id, spec);
}
}

fn determine_loop_specs(&self, def_spec: &mut typed::DefSpecificationMap) {
for local_id in self.loop_specs.iter() {
def_spec.specs.insert(*local_id, typed::SpecificationSet::Loop(typed::LoopSpecification {
def_spec.specs.insert(local_id.to_def_id(), typed::SpecificationSet::Loop(typed::LoopSpecification {
invariant: *local_id,
}));
}
Expand Down
17 changes: 7 additions & 10 deletions prusti-interface/src/specs/typed.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ use prusti_specs::specifications::common;
use rustc_hir::def_id::{DefId, LocalDefId};
use std::{collections::HashMap, fmt::Debug};
use std::fmt::{Display, Formatter};

use rustc_span::Span;

#[derive(Debug, Clone)]
pub enum SpecificationSet {
Expand Down Expand Up @@ -259,6 +259,7 @@ impl<T: Debug + Clone + PartialEq> Refinable for SpecificationItem<T> {
impl Refinable for ProcedureSpecification {
fn refine(self, other: &Self) -> Self {
ProcedureSpecification {
span: self.span.or(other.span),
pres: self.pres.refine(&other.pres),
posts: self.posts.refine(&other.posts),
pledges: self.pledges.refine(&other.pledges),
Expand All @@ -282,6 +283,7 @@ impl Refinable for SpecificationSet {

#[derive(Debug, Clone)]
pub struct ProcedureSpecification {
pub span: Option<Span>,
pub kind: SpecificationItem<ProcedureSpecificationKind>,
pub pres: SpecificationItem<Vec<LocalDefId>>,
pub posts: SpecificationItem<Vec<LocalDefId>>,
Expand All @@ -292,6 +294,7 @@ pub struct ProcedureSpecification {
impl ProcedureSpecification {
pub fn empty() -> Self {
ProcedureSpecification {
span: None,
kind: SpecificationItem::Empty,
pres: SpecificationItem::Empty,
posts: SpecificationItem::Empty,
Expand Down Expand Up @@ -324,24 +327,18 @@ pub struct LoopSpecification {
pub invariant: LocalDefId,
}

/// A map of specifications keyed by crate-local DefIds.
/// A map of specifications keyed by local or external DefIds.
#[derive(Default, Debug, Clone)]
pub struct DefSpecificationMap {
pub specs: HashMap<LocalDefId, SpecificationSet>,
pub extern_specs: HashMap<DefId, LocalDefId>,
pub specs: HashMap<DefId, SpecificationSet>,
}

impl DefSpecificationMap {
pub fn new() -> Self {
Self::default()
}
pub fn get(&self, def_id: &DefId) -> Option<&SpecificationSet> {
let id = if let Some(spec_id) = self.extern_specs.get(def_id) {
*spec_id
} else {
def_id.as_local()?
};
self.specs.get(&id)
self.specs.get(def_id)
}
}

Expand Down
2 changes: 1 addition & 1 deletion prusti-tests/tests/cargo_verify/prusti_toml/output.stdout
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,4 +23,4 @@ pub fn test2() {
if !false { ::core::panicking::panic("assertion failed: false") };
}
pub fn test3(x: usize) { let _y: usize = 1 - x; }
Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:6 ~ prusti_toml[..]::prusti_post_item_test1_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) })
Procedure(ProcedureSpecification { span: Some(src/lib.rs:4:1: 4:15 (#0)), kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:6 ~ prusti_toml[..]::prusti_post_item_test1_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) })
6 changes: 3 additions & 3 deletions prusti-tests/tests/parse/ui/after_expiry.stdout
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,6 @@ fn prusti_pledge_item_test3_$(NUM_UUID)(x: u32,
#[prusti::pledge_spec_id_ref = "$(NUM_UUID)"]
fn test3(x: u32) -> u32 { 1 }
fn main() {}
Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Empty, pledges: Inherent([Pledge { reference: None, lhs: None, rhs: DefId(0:5 ~ after_expiry[$(CRATE_ID)]::prusti_pledge_item_test1_$(NUM_UUID)) }]), trusted: Inherent(false) })
Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Empty, pledges: Inherent([Pledge { reference: None, lhs: None, rhs: DefId(0:7 ~ after_expiry[$(CRATE_ID)]::prusti_pledge_item_test2_$(NUM_UUID)) }]), trusted: Inherent(false) })
Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Empty, pledges: Inherent([Pledge { reference: None, lhs: None, rhs: DefId(0:9 ~ after_expiry[$(CRATE_ID)]::prusti_pledge_item_test3_$(NUM_UUID)) }]), trusted: Inherent(false) })
Procedure(ProcedureSpecification { span: Some($DIR/after_expiry.rs:9:1: 9:18 (#0)), kind: Inherent(Impure), pres: Empty, posts: Empty, pledges: Inherent([Pledge { reference: None, lhs: None, rhs: DefId(0:5 ~ after_expiry[$(CRATE_ID)]::prusti_pledge_item_test1_$(NUM_UUID)) }]), trusted: Inherent(false) })
Procedure(ProcedureSpecification { span: Some($DIR/after_expiry.rs:12:1: 12:18 (#0)), kind: Inherent(Impure), pres: Empty, posts: Empty, pledges: Inherent([Pledge { reference: None, lhs: None, rhs: DefId(0:7 ~ after_expiry[$(CRATE_ID)]::prusti_pledge_item_test2_$(NUM_UUID)) }]), trusted: Inherent(false) })
Procedure(ProcedureSpecification { span: Some($DIR/after_expiry.rs:21:1: 21:24 (#0)), kind: Inherent(Impure), pres: Empty, posts: Empty, pledges: Inherent([Pledge { reference: None, lhs: None, rhs: DefId(0:9 ~ after_expiry[$(CRATE_ID)]::prusti_pledge_item_test3_$(NUM_UUID)) }]), trusted: Inherent(false) })
10 changes: 5 additions & 5 deletions prusti-tests/tests/parse/ui/and.stdout
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,8 +59,8 @@ fn prusti_pre_item_test5_$(NUM_UUID)() -> bool {
#[prusti::pre_spec_id_ref = "$(NUM_UUID)"]
fn test5() {}
fn main() {}
Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:5 ~ and[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) })
Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:7 ~ and[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) })
Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:9 ~ and[$(CRATE_ID)]::prusti_pre_item_test3_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) })
Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:11 ~ and[$(CRATE_ID)]::prusti_pre_item_test4_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) })
Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:13 ~ and[$(CRATE_ID)]::prusti_pre_item_test5_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) })
Procedure(ProcedureSpecification { span: Some($DIR/and.rs:9:1: 9:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:5 ~ and[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) })
Procedure(ProcedureSpecification { span: Some($DIR/and.rs:12:1: 12:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:7 ~ and[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) })
Procedure(ProcedureSpecification { span: Some($DIR/and.rs:15:1: 15:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:9 ~ and[$(CRATE_ID)]::prusti_pre_item_test3_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) })
Procedure(ProcedureSpecification { span: Some($DIR/and.rs:18:1: 18:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:11 ~ and[$(CRATE_ID)]::prusti_pre_item_test4_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) })
Procedure(ProcedureSpecification { span: Some($DIR/and.rs:21:1: 21:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:13 ~ and[$(CRATE_ID)]::prusti_pre_item_test5_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) })
6 changes: 3 additions & 3 deletions prusti-tests/tests/parse/ui/assert_on_expiry.stdout
View file
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,6 @@ fn prusti_pledge_item_test3_$(NUM_UUID)(x: u32,
#[prusti::assert_pledge_spec_id_ref_rhs = "$(NUM_UUID)"]
fn test3(x: u32) -> u32 { 1 }
fn main() {}
Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Empty, pledges: Inherent([Pledge { reference: None, lhs: Some(DefId(0:5 ~ assert_on_expiry[$(CRATE_ID)]::prusti_pledge_item_test1_$(NUM_UUID))), rhs: DefId(0:6 ~ assert_on_expiry[$(CRATE_ID)]::prusti_pledge_item_test1_$(NUM_UUID)) }]), trusted: Inherent(false) })
Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Empty, pledges: Inherent([Pledge { reference: None, lhs: Some(DefId(0:8 ~ assert_on_expiry[$(CRATE_ID)]::prusti_pledge_item_test2_$(NUM_UUID))), rhs: DefId(0:9 ~ assert_on_expiry[$(CRATE_ID)]::prusti_pledge_item_test2_$(NUM_UUID)) }]), trusted: Inherent(false) })
Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Empty, pledges: Inherent([Pledge { reference: None, lhs: Some(DefId(0:11 ~ assert_on_expiry[$(CRATE_ID)]::prusti_pledge_item_test3_$(NUM_UUID))), rhs: DefId(0:12 ~ assert_on_expiry[$(CRATE_ID)]::prusti_pledge_item_test3_$(NUM_UUID)) }]), trusted: Inherent(false) })
Procedure(ProcedureSpecification { span: Some($DIR/assert_on_expiry.rs:9:1: 9:18 (#0)), kind: Inherent(Impure), pres: Empty, posts: Empty, pledges: Inherent([Pledge { reference: None, lhs: Some(DefId(0:5 ~ assert_on_expiry[$(CRATE_ID)]::prusti_pledge_item_test1_$(NUM_UUID))), rhs: DefId(0:6 ~ assert_on_expiry[$(CRATE_ID)]::prusti_pledge_item_test1_$(NUM_UUID)) }]), trusted: Inherent(false) })
Procedure(ProcedureSpecification { span: Some($DIR/assert_on_expiry.rs:12:1: 12:18 (#0)), kind: Inherent(Impure), pres: Empty, posts: Empty, pledges: Inherent([Pledge { reference: None, lhs: Some(DefId(0:8 ~ assert_on_expiry[$(CRATE_ID)]::prusti_pledge_item_test2_$(NUM_UUID))), rhs: DefId(0:9 ~ assert_on_expiry[$(CRATE_ID)]::prusti_pledge_item_test2_$(NUM_UUID)) }]), trusted: Inherent(false) })
Procedure(ProcedureSpecification { span: Some($DIR/assert_on_expiry.rs:22:1: 22:24 (#0)), kind: Inherent(Impure), pres: Empty, posts: Empty, pledges: Inherent([Pledge { reference: None, lhs: Some(DefId(0:11 ~ assert_on_expiry[$(CRATE_ID)]::prusti_pledge_item_test3_$(NUM_UUID))), rhs: DefId(0:12 ~ assert_on_expiry[$(CRATE_ID)]::prusti_pledge_item_test3_$(NUM_UUID)) }]), trusted: Inherent(false) })
Loading

0 comments on commit 36b94f7

Please sign in to comment.