diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index d138aa59c7d..d8e287ceb30 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -61,11 +61,19 @@ struct CachedBody<'tcx> { borrowck_facts: Rc, } +struct CachedExternalBody<'tcx> { + /// MIR body as known to the compiler. + base_body: Rc>, + /// Copies of the MIR body with the given substs applied. + monomorphised_bodies: HashMap, Rc>>, +} + /// Facade to the Rust compiler. // #[derive(Copy, Clone)] pub struct Environment<'tcx> { /// Cached MIR bodies. bodies: RefCell>>, + external_bodies: RefCell>>, tcx: TyCtxt<'tcx>, } @@ -75,6 +83,7 @@ impl<'tcx> Environment<'tcx> { Environment { tcx, bodies: RefCell::new(HashMap::new()), + external_bodies: RefCell::new(HashMap::new()), } } @@ -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> { + 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. @@ -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 { diff --git a/prusti-interface/src/specs/mod.rs b/prusti-interface/src/specs/mod.rs index b45f6e2d289..da3dc160b1c 100644 --- a/prusti-interface/src/specs/mod.rs +++ b/prusti-interface/src/specs/mod.rs @@ -43,7 +43,7 @@ pub struct SpecCollector<'a, 'tcx: 'a> { /// Map from functions/loops and their specifications. procedure_specs: HashMap, - loop_specs: Vec, // HashMap>, + loop_specs: Vec, } impl<'a, 'tcx> SpecCollector<'a, 'tcx> { @@ -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, @@ -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, })); } diff --git a/prusti-interface/src/specs/typed.rs b/prusti-interface/src/specs/typed.rs index 4a98cfa1eb1..791b24a2917 100644 --- a/prusti-interface/src/specs/typed.rs +++ b/prusti-interface/src/specs/typed.rs @@ -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 { @@ -259,6 +259,7 @@ impl Refinable for SpecificationItem { 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), @@ -282,6 +283,7 @@ impl Refinable for SpecificationSet { #[derive(Debug, Clone)] pub struct ProcedureSpecification { + pub span: Option, pub kind: SpecificationItem, pub pres: SpecificationItem>, pub posts: SpecificationItem>, @@ -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, @@ -324,11 +327,10 @@ 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, - pub extern_specs: HashMap, + pub specs: HashMap, } impl DefSpecificationMap { @@ -336,12 +338,7 @@ impl DefSpecificationMap { 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) } } diff --git a/prusti-tests/tests/cargo_verify/prusti_toml/output.stdout b/prusti-tests/tests/cargo_verify/prusti_toml/output.stdout index 382c756a33e..8e679d72da6 100644 --- a/prusti-tests/tests/cargo_verify/prusti_toml/output.stdout +++ b/prusti-tests/tests/cargo_verify/prusti_toml/output.stdout @@ -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) }) diff --git a/prusti-tests/tests/parse/ui/after_expiry.stdout b/prusti-tests/tests/parse/ui/after_expiry.stdout index 1fdf06d2e66..08a8f55c669 100644 --- a/prusti-tests/tests/parse/ui/after_expiry.stdout +++ b/prusti-tests/tests/parse/ui/after_expiry.stdout @@ -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) }) diff --git a/prusti-tests/tests/parse/ui/and.stdout b/prusti-tests/tests/parse/ui/and.stdout index a793b15b6f7..b8e4821880d 100644 --- a/prusti-tests/tests/parse/ui/and.stdout +++ b/prusti-tests/tests/parse/ui/and.stdout @@ -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) }) diff --git a/prusti-tests/tests/parse/ui/assert_on_expiry.stdout b/prusti-tests/tests/parse/ui/assert_on_expiry.stdout index 9cb894145aa..032c68d7379 100644 --- a/prusti-tests/tests/parse/ui/assert_on_expiry.stdout +++ b/prusti-tests/tests/parse/ui/assert_on_expiry.stdout @@ -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) }) diff --git a/prusti-tests/tests/parse/ui/composite.stdout b/prusti-tests/tests/parse/ui/composite.stdout index b8d34acd90a..2bfb2ab18af 100644 --- a/prusti-tests/tests/parse/ui/composite.stdout +++ b/prusti-tests/tests/parse/ui/composite.stdout @@ -279,27 +279,27 @@ fn prusti_pre_item_test26_$(NUM_UUID)() -> bool { #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] fn test26() {} fn main() {} -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:5 ~ composite[$(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 ~ composite[$(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 ~ composite[$(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 ~ composite[$(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 ~ composite[$(CRATE_ID)]::prusti_pre_item_test5_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:15 ~ composite[$(CRATE_ID)]::prusti_pre_item_test6_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:17 ~ composite[$(CRATE_ID)]::prusti_pre_item_test7_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:19 ~ composite[$(CRATE_ID)]::prusti_pre_item_test8_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:21 ~ composite[$(CRATE_ID)]::prusti_pre_item_test9_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:23 ~ composite[$(CRATE_ID)]::prusti_pre_item_test10_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:26 ~ composite[$(CRATE_ID)]::prusti_pre_item_test12_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:29 ~ composite[$(CRATE_ID)]::prusti_pre_item_test13_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:32 ~ composite[$(CRATE_ID)]::prusti_pre_item_test14_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:35 ~ composite[$(CRATE_ID)]::prusti_pre_item_test15_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:38 ~ composite[$(CRATE_ID)]::prusti_pre_item_test16_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:42 ~ composite[$(CRATE_ID)]::prusti_pre_item_test17_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:45 ~ composite[$(CRATE_ID)]::prusti_pre_item_test19_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:48 ~ composite[$(CRATE_ID)]::prusti_pre_item_test20_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:51 ~ composite[$(CRATE_ID)]::prusti_pre_item_test21_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:54 ~ composite[$(CRATE_ID)]::prusti_pre_item_test22_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:57 ~ composite[$(CRATE_ID)]::prusti_pre_item_test23_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:61 ~ composite[$(CRATE_ID)]::prusti_pre_item_test24_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:63 ~ composite[$(CRATE_ID)]::prusti_pre_item_test25_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:67 ~ composite[$(CRATE_ID)]::prusti_pre_item_test26_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:9:1: 9:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:5 ~ composite[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:12:1: 12:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:7 ~ composite[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:15:1: 15:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:9 ~ composite[$(CRATE_ID)]::prusti_pre_item_test3_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:18:1: 18:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:11 ~ composite[$(CRATE_ID)]::prusti_pre_item_test4_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:21:1: 21:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:13 ~ composite[$(CRATE_ID)]::prusti_pre_item_test5_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:24:1: 24:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:15 ~ composite[$(CRATE_ID)]::prusti_pre_item_test6_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:27:1: 27:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:17 ~ composite[$(CRATE_ID)]::prusti_pre_item_test7_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:30:1: 30:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:19 ~ composite[$(CRATE_ID)]::prusti_pre_item_test8_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:33:1: 33:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:21 ~ composite[$(CRATE_ID)]::prusti_pre_item_test9_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:36:1: 36:12 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:23 ~ composite[$(CRATE_ID)]::prusti_pre_item_test10_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:39:1: 39:12 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:26 ~ composite[$(CRATE_ID)]::prusti_pre_item_test12_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:42:1: 42:12 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:29 ~ composite[$(CRATE_ID)]::prusti_pre_item_test13_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:45:1: 45:12 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:32 ~ composite[$(CRATE_ID)]::prusti_pre_item_test14_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:48:1: 48:12 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:35 ~ composite[$(CRATE_ID)]::prusti_pre_item_test15_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:51:1: 51:12 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:38 ~ composite[$(CRATE_ID)]::prusti_pre_item_test16_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:54:1: 54:12 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:42 ~ composite[$(CRATE_ID)]::prusti_pre_item_test17_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:57:1: 57:12 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:45 ~ composite[$(CRATE_ID)]::prusti_pre_item_test19_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:60:1: 60:12 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:48 ~ composite[$(CRATE_ID)]::prusti_pre_item_test20_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:63:1: 63:12 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:51 ~ composite[$(CRATE_ID)]::prusti_pre_item_test21_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:66:1: 66:12 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:54 ~ composite[$(CRATE_ID)]::prusti_pre_item_test22_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:69:1: 69:12 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:57 ~ composite[$(CRATE_ID)]::prusti_pre_item_test23_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:72:1: 72:12 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:61 ~ composite[$(CRATE_ID)]::prusti_pre_item_test24_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:75:1: 75:12 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:63 ~ composite[$(CRATE_ID)]::prusti_pre_item_test25_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/composite.rs:78:1: 78:12 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:67 ~ composite[$(CRATE_ID)]::prusti_pre_item_test26_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) diff --git a/prusti-tests/tests/parse/ui/exists.stdout b/prusti-tests/tests/parse/ui/exists.stdout index af169917dc6..b992e77fc8b 100644 --- a/prusti-tests/tests/parse/ui/exists.stdout +++ b/prusti-tests/tests/parse/ui/exists.stdout @@ -92,9 +92,9 @@ fn prusti_pre_item_test6_$(NUM_UUID)() -> bool { #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] fn test6() {} fn main() {} -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:5 ~ exists[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:8 ~ exists[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:11 ~ exists[$(CRATE_ID)]::prusti_pre_item_test3_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:14 ~ exists[$(CRATE_ID)]::prusti_pre_item_test4_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:19 ~ exists[$(CRATE_ID)]::prusti_pre_item_test5_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:25 ~ exists[$(CRATE_ID)]::prusti_pre_item_test6_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/exists.rs:9:1: 9:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:5 ~ exists[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/exists.rs:12:1: 12:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:8 ~ exists[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/exists.rs:15:1: 15:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:11 ~ exists[$(CRATE_ID)]::prusti_pre_item_test3_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/exists.rs:18:1: 18:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:14 ~ exists[$(CRATE_ID)]::prusti_pre_item_test4_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/exists.rs:21:1: 21:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:19 ~ exists[$(CRATE_ID)]::prusti_pre_item_test5_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/exists.rs:24:1: 24:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:25 ~ exists[$(CRATE_ID)]::prusti_pre_item_test6_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) diff --git a/prusti-tests/tests/parse/ui/expression.stdout b/prusti-tests/tests/parse/ui/expression.stdout index 6bd12434e9c..ab0458deb05 100644 --- a/prusti-tests/tests/parse/ui/expression.stdout +++ b/prusti-tests/tests/parse/ui/expression.stdout @@ -33,5 +33,5 @@ fn prusti_post_item_test2_$(NUM_UUID)(result: ()) #[prusti::post_spec_id_ref = "$(NUM_UUID)"] fn test2() {} fn main() {} -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:5 ~ expression[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:7 ~ expression[$(CRATE_ID)]::prusti_post_item_test2_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/expression.rs:9:1: 9:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:5 ~ expression[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/expression.rs:12:1: 12:11 (#0)), kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:7 ~ expression[$(CRATE_ID)]::prusti_post_item_test2_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) diff --git a/prusti-tests/tests/parse/ui/forall.stdout b/prusti-tests/tests/parse/ui/forall.stdout index bdcc415919b..51f403243b0 100644 --- a/prusti-tests/tests/parse/ui/forall.stdout +++ b/prusti-tests/tests/parse/ui/forall.stdout @@ -92,9 +92,9 @@ fn prusti_pre_item_test6_$(NUM_UUID)() -> bool { #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] fn test6() {} fn main() {} -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:5 ~ forall[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:8 ~ forall[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:11 ~ forall[$(CRATE_ID)]::prusti_pre_item_test3_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:14 ~ forall[$(CRATE_ID)]::prusti_pre_item_test4_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:19 ~ forall[$(CRATE_ID)]::prusti_pre_item_test5_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:25 ~ forall[$(CRATE_ID)]::prusti_pre_item_test6_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall.rs:9:1: 9:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:5 ~ forall[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall.rs:12:1: 12:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:8 ~ forall[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall.rs:15:1: 15:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:11 ~ forall[$(CRATE_ID)]::prusti_pre_item_test3_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall.rs:18:1: 18:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:14 ~ forall[$(CRATE_ID)]::prusti_pre_item_test4_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall.rs:21:1: 21:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:19 ~ forall[$(CRATE_ID)]::prusti_pre_item_test5_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall.rs:24:1: 24:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:25 ~ forall[$(CRATE_ID)]::prusti_pre_item_test6_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) diff --git a/prusti-tests/tests/parse/ui/implies.stdout b/prusti-tests/tests/parse/ui/implies.stdout index f7854dd4644..c4f5fc009f9 100644 --- a/prusti-tests/tests/parse/ui/implies.stdout +++ b/prusti-tests/tests/parse/ui/implies.stdout @@ -104,13 +104,13 @@ fn prusti_pre_item_test25_$(NUM_UUID)() -> bool { #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] fn test25() {} fn main() {} -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:5 ~ implies[$(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 ~ implies[$(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 ~ implies[$(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 ~ implies[$(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 ~ implies[$(CRATE_ID)]::prusti_pre_item_test5_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:15 ~ implies[$(CRATE_ID)]::prusti_pre_item_test21_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:17 ~ implies[$(CRATE_ID)]::prusti_pre_item_test22_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:19 ~ implies[$(CRATE_ID)]::prusti_pre_item_test23_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:21 ~ implies[$(CRATE_ID)]::prusti_pre_item_test24_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:23 ~ implies[$(CRATE_ID)]::prusti_pre_item_test25_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/implies.rs:9:1: 9:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:5 ~ implies[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/implies.rs:12:1: 12:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:7 ~ implies[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/implies.rs:15:1: 15:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:9 ~ implies[$(CRATE_ID)]::prusti_pre_item_test3_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/implies.rs:18:1: 18:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:11 ~ implies[$(CRATE_ID)]::prusti_pre_item_test4_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/implies.rs:21:1: 21:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:13 ~ implies[$(CRATE_ID)]::prusti_pre_item_test5_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/implies.rs:24:1: 24:12 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:15 ~ implies[$(CRATE_ID)]::prusti_pre_item_test21_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/implies.rs:27:1: 27:12 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:17 ~ implies[$(CRATE_ID)]::prusti_pre_item_test22_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/implies.rs:30:1: 30:12 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:19 ~ implies[$(CRATE_ID)]::prusti_pre_item_test23_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/implies.rs:33:1: 33:12 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:21 ~ implies[$(CRATE_ID)]::prusti_pre_item_test24_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/implies.rs:36:1: 36:12 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:23 ~ implies[$(CRATE_ID)]::prusti_pre_item_test25_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) diff --git a/prusti-tests/tests/parse/ui/predicates-visibility.stdout b/prusti-tests/tests/parse/ui/predicates-visibility.stdout index 1671f8dac5f..1ea70e0e75f 100644 --- a/prusti-tests/tests/parse/ui/predicates-visibility.stdout +++ b/prusti-tests/tests/parse/ui/predicates-visibility.stdout @@ -47,5 +47,5 @@ fn prusti_pre_item_test_pub_pred_$(NUM_UUID)() -> bool { #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] fn test_pub_pred() {} fn main() {} -Procedure(ProcedureSpecification { kind: Inherent(Predicate(DefId(0:13 ~ predicates_visibility[$(CRATE_ID)]::foo::prusti_pred_item_pred1_$(NUM_UUID)))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(true) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:16 ~ predicates_visibility[$(CRATE_ID)]::prusti_pre_item_test_pub_pred_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/predicates-visibility.rs:13:9: 13:38 (#0)), kind: Inherent(Predicate(DefId(0:13 ~ predicates_visibility[$(CRATE_ID)]::foo::prusti_pred_item_pred1_$(NUM_UUID)))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(true) }) +Procedure(ProcedureSpecification { span: Some($DIR/predicates-visibility.rs:20:1: 20:19 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:16 ~ predicates_visibility[$(CRATE_ID)]::prusti_pre_item_test_pub_pred_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) diff --git a/prusti-tests/tests/parse/ui/predicates.stdout b/prusti-tests/tests/parse/ui/predicates.stdout index c14695caaac..5ebe982b713 100644 --- a/prusti-tests/tests/parse/ui/predicates.stdout +++ b/prusti-tests/tests/parse/ui/predicates.stdout @@ -108,9 +108,9 @@ fn exists_implication() -> bool { &[]))])) } fn main() {} -Procedure(ProcedureSpecification { kind: Inherent(Predicate(DefId(0:5 ~ predicates[$(CRATE_ID)]::prusti_pred_item_pred1_$(NUM_UUID)))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(true) }) -Procedure(ProcedureSpecification { kind: Inherent(Predicate(DefId(0:10 ~ predicates[$(CRATE_ID)]::prusti_pred_item_pred2_$(NUM_UUID)))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(true) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:8 ~ predicates[$(CRATE_ID)]::prusti_pre_item_use_pred1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:13 ~ predicates[$(CRATE_ID)]::prusti_pre_item_use_pred2_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Predicate(DefId(0:15 ~ predicates[$(CRATE_ID)]::prusti_pred_item_forall_implication_$(NUM_UUID)))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(true) }) -Procedure(ProcedureSpecification { kind: Inherent(Predicate(DefId(0:18 ~ predicates[$(CRATE_ID)]::prusti_pred_item_exists_implication_$(NUM_UUID)))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(true) }) +Procedure(ProcedureSpecification { span: Some($DIR/predicates.rs:11:5: 11:30 (#0)), kind: Inherent(Predicate(DefId(0:5 ~ predicates[$(CRATE_ID)]::prusti_pred_item_pred1_$(NUM_UUID)))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(true) }) +Procedure(ProcedureSpecification { span: Some($DIR/predicates.rs:20:5: 20:30 (#0)), kind: Inherent(Predicate(DefId(0:10 ~ predicates[$(CRATE_ID)]::prusti_pred_item_pred2_$(NUM_UUID)))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(true) }) +Procedure(ProcedureSpecification { span: Some($DIR/predicates.rs:17:1: 17:15 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:8 ~ predicates[$(CRATE_ID)]::prusti_pre_item_use_pred1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/predicates.rs:26:1: 26:15 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:13 ~ predicates[$(CRATE_ID)]::prusti_pre_item_use_pred2_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/predicates.rs:29:5: 29:36 (#0)), kind: Inherent(Predicate(DefId(0:15 ~ predicates[$(CRATE_ID)]::prusti_pred_item_forall_implication_$(NUM_UUID)))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(true) }) +Procedure(ProcedureSpecification { span: Some($DIR/predicates.rs:35:5: 35:36 (#0)), kind: Inherent(Predicate(DefId(0:18 ~ predicates[$(CRATE_ID)]::prusti_pred_item_exists_implication_$(NUM_UUID)))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(true) }) diff --git a/prusti-tests/tests/parse/ui/trait-bounds.stdout b/prusti-tests/tests/parse/ui/trait-bounds.stdout index ca8eb05b47f..b75baab8c37 100644 --- a/prusti-tests/tests/parse/ui/trait-bounds.stdout +++ b/prusti-tests/tests/parse/ui/trait-bounds.stdout @@ -46,4 +46,4 @@ impl<'a, T: PartialEq, const L : usize> } } fn main() {} -Procedure(ProcedureSpecification { kind: Inherent(Pure), pres: Empty, posts: Inherent([DefId(0:30 ~ trait_bounds[$(CRATE_ID)]::{impl#1}::prusti_post_item_bar_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(true) }) +Procedure(ProcedureSpecification { span: Some($DIR/trait-bounds.rs:19:5: 19:35 (#0)), kind: Inherent(Pure), pres: Empty, posts: Inherent([DefId(0:30 ~ trait_bounds[$(CRATE_ID)]::{impl#1}::prusti_post_item_bar_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(true) }) diff --git a/prusti-tests/tests/parse/ui/traits.stdout b/prusti-tests/tests/parse/ui/traits.stdout index a01b31ff257..a0ae571d230 100644 --- a/prusti-tests/tests/parse/ui/traits.stdout +++ b/prusti-tests/tests/parse/ui/traits.stdout @@ -174,15 +174,15 @@ trait Test4 { fn test2(&self); } fn main() {} -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:9 ~ traits[$(CRATE_ID)]::Test1::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:13 ~ traits[$(CRATE_ID)]::Test1::prusti_pre_item_test3_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:23 ~ traits[$(CRATE_ID)]::Test3::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:27 ~ traits[$(CRATE_ID)]::Test3::prusti_pre_item_test3_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:11 ~ traits[$(CRATE_ID)]::Test1::prusti_post_item_test2_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:15 ~ traits[$(CRATE_ID)]::Test1::prusti_post_item_test4_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:25 ~ traits[$(CRATE_ID)]::Test3::prusti_post_item_test2_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:29 ~ traits[$(CRATE_ID)]::Test3::prusti_post_item_test4_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:17 ~ traits[$(CRATE_ID)]::Test2::prusti_pre_item_test1_$(NUM_UUID))]), posts: Inherent([DefId(0:18 ~ traits[$(CRATE_ID)]::Test2::prusti_post_item_test1_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:20 ~ traits[$(CRATE_ID)]::Test2::prusti_pre_item_test2_$(NUM_UUID))]), posts: Inherent([DefId(0:21 ~ traits[$(CRATE_ID)]::Test2::prusti_post_item_test2_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:31 ~ traits[$(CRATE_ID)]::Test4::prusti_pre_item_test1_$(NUM_UUID))]), posts: Inherent([DefId(0:32 ~ traits[$(CRATE_ID)]::Test4::prusti_post_item_test1_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:34 ~ traits[$(CRATE_ID)]::Test4::prusti_pre_item_test2_$(NUM_UUID))]), posts: Inherent([DefId(0:35 ~ traits[$(CRATE_ID)]::Test4::prusti_post_item_test2_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/traits.rs:11:5: 11:15 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:9 ~ traits[$(CRATE_ID)]::Test1::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/traits.rs:17:5: 17:16 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:13 ~ traits[$(CRATE_ID)]::Test1::prusti_pre_item_test3_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/traits.rs:39:5: 39:20 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:23 ~ traits[$(CRATE_ID)]::Test3::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/traits.rs:45:5: 45:21 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:27 ~ traits[$(CRATE_ID)]::Test3::prusti_pre_item_test3_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/traits.rs:14:5: 14:15 (#0)), kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:11 ~ traits[$(CRATE_ID)]::Test1::prusti_post_item_test2_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/traits.rs:20:5: 20:16 (#0)), kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:15 ~ traits[$(CRATE_ID)]::Test1::prusti_post_item_test4_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/traits.rs:42:5: 42:20 (#0)), kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:25 ~ traits[$(CRATE_ID)]::Test3::prusti_post_item_test2_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/traits.rs:48:5: 48:21 (#0)), kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:29 ~ traits[$(CRATE_ID)]::Test3::prusti_post_item_test4_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/traits.rs:28:5: 28:15 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:17 ~ traits[$(CRATE_ID)]::Test2::prusti_pre_item_test1_$(NUM_UUID))]), posts: Inherent([DefId(0:18 ~ traits[$(CRATE_ID)]::Test2::prusti_post_item_test1_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/traits.rs:32:5: 32:16 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:20 ~ traits[$(CRATE_ID)]::Test2::prusti_pre_item_test2_$(NUM_UUID))]), posts: Inherent([DefId(0:21 ~ traits[$(CRATE_ID)]::Test2::prusti_post_item_test2_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/traits.rs:56:5: 56:20 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:31 ~ traits[$(CRATE_ID)]::Test4::prusti_pre_item_test1_$(NUM_UUID))]), posts: Inherent([DefId(0:32 ~ traits[$(CRATE_ID)]::Test4::prusti_post_item_test1_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/traits.rs:60:5: 60:21 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:34 ~ traits[$(CRATE_ID)]::Test4::prusti_pre_item_test2_$(NUM_UUID))]), posts: Inherent([DefId(0:35 ~ traits[$(CRATE_ID)]::Test4::prusti_post_item_test2_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) diff --git a/prusti-tests/tests/parse/ui/true.stdout b/prusti-tests/tests/parse/ui/true.stdout index 5b8b401db19..8e367a57c54 100644 --- a/prusti-tests/tests/parse/ui/true.stdout +++ b/prusti-tests/tests/parse/ui/true.stdout @@ -82,6 +82,6 @@ fn test4() { fn main() {} Loop(LoopSpecification { invariant: DefId(0:10 ~ true[$(CRATE_ID)]::test3::{closure#0}) }) Loop(LoopSpecification { invariant: DefId(0:14 ~ true[$(CRATE_ID)]::test4::{closure#0}) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:6 ~ true[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:8 ~ true[$(CRATE_ID)]::prusti_post_item_test2_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:11 ~ true[$(CRATE_ID)]::prusti_pre_item_test4_$(NUM_UUID))]), posts: Inherent([DefId(0:12 ~ true[$(CRATE_ID)]::prusti_post_item_test4_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/true.rs:9:1: 9:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:6 ~ true[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/true.rs:12:1: 12:11 (#0)), kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:8 ~ true[$(CRATE_ID)]::prusti_post_item_test2_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/true.rs:22:1: 22:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:11 ~ true[$(CRATE_ID)]::prusti_pre_item_test4_$(NUM_UUID))]), posts: Inherent([DefId(0:12 ~ true[$(CRATE_ID)]::prusti_post_item_test4_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) diff --git a/prusti-tests/tests/typecheck/ui/forall_encode_typeck.stdout b/prusti-tests/tests/typecheck/ui/forall_encode_typeck.stdout index 3be869571f4..fe81949c785 100644 --- a/prusti-tests/tests/typecheck/ui/forall_encode_typeck.stdout +++ b/prusti-tests/tests/typecheck/ui/forall_encode_typeck.stdout @@ -40,5 +40,5 @@ fn prusti_pre_item_test2_$(NUM_UUID)() -> bool { #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] fn test2() {} fn main() {} -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:5 ~ forall_encode_typeck[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:11 ~ forall_encode_typeck[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall_encode_typeck.rs:9:1: 9:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:5 ~ forall_encode_typeck[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall_encode_typeck.rs:12:1: 12:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:11 ~ forall_encode_typeck[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) diff --git a/prusti-tests/tests/typecheck/ui/forall_triggers.stdout b/prusti-tests/tests/typecheck/ui/forall_triggers.stdout index 1c71d3d858a..be98f1fa11d 100644 --- a/prusti-tests/tests/typecheck/ui/forall_triggers.stdout +++ b/prusti-tests/tests/typecheck/ui/forall_triggers.stdout @@ -126,11 +126,11 @@ fn prusti_pre_item_test8_$(NUM_UUID)() -> bool { #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] fn test8() {} fn main() {} -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:5 ~ forall_triggers[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:9 ~ forall_triggers[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:14 ~ forall_triggers[$(CRATE_ID)]::prusti_pre_item_test3_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:20 ~ forall_triggers[$(CRATE_ID)]::prusti_pre_item_test4_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:26 ~ forall_triggers[$(CRATE_ID)]::prusti_pre_item_test5_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:30 ~ forall_triggers[$(CRATE_ID)]::prusti_pre_item_test6_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:35 ~ forall_triggers[$(CRATE_ID)]::prusti_pre_item_test7_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:41 ~ forall_triggers[$(CRATE_ID)]::prusti_pre_item_test8_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall_triggers.rs:9:1: 9:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:5 ~ forall_triggers[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall_triggers.rs:12:1: 12:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:9 ~ forall_triggers[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall_triggers.rs:15:1: 15:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:14 ~ forall_triggers[$(CRATE_ID)]::prusti_pre_item_test3_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall_triggers.rs:18:1: 18:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:20 ~ forall_triggers[$(CRATE_ID)]::prusti_pre_item_test4_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall_triggers.rs:21:1: 21:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:26 ~ forall_triggers[$(CRATE_ID)]::prusti_pre_item_test5_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall_triggers.rs:24:1: 24:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:30 ~ forall_triggers[$(CRATE_ID)]::prusti_pre_item_test6_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall_triggers.rs:27:1: 27:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:35 ~ forall_triggers[$(CRATE_ID)]::prusti_pre_item_test7_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall_triggers.rs:30:1: 30:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:41 ~ forall_triggers[$(CRATE_ID)]::prusti_pre_item_test8_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) diff --git a/prusti-tests/tests/typecheck/ui/nested_forall.stdout b/prusti-tests/tests/typecheck/ui/nested_forall.stdout index 891fb9c6248..ddb35e9abb0 100644 --- a/prusti-tests/tests/typecheck/ui/nested_forall.stdout +++ b/prusti-tests/tests/typecheck/ui/nested_forall.stdout @@ -113,9 +113,9 @@ fn prusti_pre_item_test6_$(NUM_UUID)() -> bool { #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] fn test6() {} fn main() {} -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:5 ~ nested_forall[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:9 ~ nested_forall[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:13 ~ nested_forall[$(CRATE_ID)]::prusti_pre_item_test3_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:18 ~ nested_forall[$(CRATE_ID)]::prusti_pre_item_test4_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:22 ~ nested_forall[$(CRATE_ID)]::prusti_pre_item_test5_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:26 ~ nested_forall[$(CRATE_ID)]::prusti_pre_item_test6_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/nested_forall.rs:9:1: 9:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:5 ~ nested_forall[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/nested_forall.rs:12:1: 12:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:9 ~ nested_forall[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/nested_forall.rs:15:1: 15:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:13 ~ nested_forall[$(CRATE_ID)]::prusti_pre_item_test3_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/nested_forall.rs:18:1: 18:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:18 ~ nested_forall[$(CRATE_ID)]::prusti_pre_item_test4_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/nested_forall.rs:21:1: 21:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:22 ~ nested_forall[$(CRATE_ID)]::prusti_pre_item_test5_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/nested_forall.rs:24:1: 24:11 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:26 ~ nested_forall[$(CRATE_ID)]::prusti_pre_item_test6_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) diff --git a/prusti-tests/tests/verify/fail/unsupported/type_param_array.rs b/prusti-tests/tests/verify/fail/unsupported/type_param_array.rs deleted file mode 100644 index 6cfdfc9b71e..00000000000 --- a/prusti-tests/tests/verify/fail/unsupported/type_param_array.rs +++ /dev/null @@ -1,7 +0,0 @@ -// ignore-test slices of generics - -fn foo (bar: &mut [T]) { - let _ = bar[0] == bar[0]; //~ ERROR type is not supported -} - -fn main() {} diff --git a/prusti-tests/tests/verify/pass/slices/type_param_slice.rs b/prusti-tests/tests/verify/pass/slices/type_param_slice.rs new file mode 100644 index 00000000000..b2211575658 --- /dev/null +++ b/prusti-tests/tests/verify/pass/slices/type_param_slice.rs @@ -0,0 +1,7 @@ +fn foo (bar: &mut [T]) { + if bar.len() >= 1 { + let _ = bar[0] == bar[0]; + } +} + +fn main() {} diff --git a/prusti-tests/tests/verify/ui/calls.stdout b/prusti-tests/tests/verify/ui/calls.stdout index e4f5cd0602a..c6c615a48b6 100644 --- a/prusti-tests/tests/verify/ui/calls.stdout +++ b/prusti-tests/tests/verify/ui/calls.stdout @@ -62,5 +62,5 @@ fn prusti_post_item_test_max3_$(NUM_UUID)(result: i32) #[prusti::post_spec_id_ref = "$(NUM_UUID)"] fn test_max3() -> i32 { let a = 4; let b = 3; max(a, b) } fn main() {} -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:10 ~ calls[$(CRATE_ID)]::prusti_post_item_test_max3_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:7 ~ calls[$(CRATE_ID)]::prusti_post_item_max_$(NUM_UUID)), DefId(0:8 ~ calls[$(CRATE_ID)]::prusti_post_item_max_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/calls.rs:44:1: 44:22 (#0)), kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:10 ~ calls[$(CRATE_ID)]::prusti_post_item_test_max3_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/calls.rs:10:1: 10:30 (#0)), kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:7 ~ calls[$(CRATE_ID)]::prusti_post_item_max_$(NUM_UUID)), DefId(0:8 ~ calls[$(CRATE_ID)]::prusti_post_item_max_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) diff --git a/prusti-tests/tests/verify/ui/false.stdout b/prusti-tests/tests/verify/ui/false.stdout index 5eee8363eef..114254ecaef 100644 --- a/prusti-tests/tests/verify/ui/false.stdout +++ b/prusti-tests/tests/verify/ui/false.stdout @@ -28,4 +28,4 @@ fn test2() { if !false { ::core::panicking::panic("assertion failed: false") }; } fn main() {} -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:6 ~ false[$(CRATE_ID)]::prusti_post_item_test1_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/false.rs:9:1: 9:11 (#0)), kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:6 ~ false[$(CRATE_ID)]::prusti_post_item_test1_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) diff --git a/prusti-tests/tests/verify/ui/forall_verify.stdout b/prusti-tests/tests/verify/ui/forall_verify.stdout index acdde8c772f..f52fbc00102 100644 --- a/prusti-tests/tests/verify/ui/forall_verify.stdout +++ b/prusti-tests/tests/verify/ui/forall_verify.stdout @@ -99,10 +99,10 @@ fn prusti_post_item_test6_$(NUM_UUID)(result: ()) #[prusti::post_spec_id_ref = "$(NUM_UUID)"] fn test6() {} fn main() {} -Procedure(ProcedureSpecification { kind: Inherent(Pure), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:6 ~ forall_verify[$(CRATE_ID)]::prusti_post_item_test1_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:9 ~ forall_verify[$(CRATE_ID)]::prusti_post_item_test2_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:12 ~ forall_verify[$(CRATE_ID)]::prusti_post_item_test3_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:15 ~ forall_verify[$(CRATE_ID)]::prusti_post_item_test4_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:22 ~ forall_verify[$(CRATE_ID)]::prusti_post_item_test6_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:18 ~ forall_verify[$(CRATE_ID)]::prusti_post_item_test5_$(NUM_UUID)), DefId(0:19 ~ forall_verify[$(CRATE_ID)]::prusti_post_item_test5_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall_verify.rs:9:1: 9:27 (#0)), kind: Inherent(Pure), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall_verify.rs:12:1: 12:11 (#0)), kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:6 ~ forall_verify[$(CRATE_ID)]::prusti_post_item_test1_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall_verify.rs:15:1: 15:11 (#0)), kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:9 ~ forall_verify[$(CRATE_ID)]::prusti_post_item_test2_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall_verify.rs:18:1: 18:11 (#0)), kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:12 ~ forall_verify[$(CRATE_ID)]::prusti_post_item_test3_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall_verify.rs:21:1: 21:11 (#0)), kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:15 ~ forall_verify[$(CRATE_ID)]::prusti_post_item_test4_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall_verify.rs:31:1: 31:11 (#0)), kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:22 ~ forall_verify[$(CRATE_ID)]::prusti_post_item_test6_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/forall_verify.rs:25:1: 25:11 (#0)), kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:18 ~ forall_verify[$(CRATE_ID)]::prusti_post_item_test5_$(NUM_UUID)), DefId(0:19 ~ forall_verify[$(CRATE_ID)]::prusti_post_item_test5_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) diff --git a/prusti-tests/tests/verify/ui/pledges.stdout b/prusti-tests/tests/verify/ui/pledges.stdout index 39e7cf36c8a..7411a663398 100644 --- a/prusti-tests/tests/verify/ui/pledges.stdout +++ b/prusti-tests/tests/verify/ui/pledges.stdout @@ -63,4 +63,4 @@ fn reborrow_caller(a: T) { if !(a.f == 5) { ::core::panicking::panic("assertion failed: a.f == 5") }; } fn main() {} -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Empty, pledges: Inherent([Pledge { reference: None, lhs: None, rhs: DefId(0:12 ~ pledges[$(CRATE_ID)]::prusti_pledge_item_reborrow_$(NUM_UUID)) }]), trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/pledges.rs:38:1: 38:45 (#0)), kind: Inherent(Impure), pres: Empty, posts: Empty, pledges: Inherent([Pledge { reference: None, lhs: None, rhs: DefId(0:12 ~ pledges[$(CRATE_ID)]::prusti_pledge_item_reborrow_$(NUM_UUID)) }]), trusted: Inherent(false) }) diff --git a/prusti-tests/tests/verify/ui/predicate.stdout b/prusti-tests/tests/verify/ui/predicate.stdout index 6319ddc0cd3..4535a4af972 100644 --- a/prusti-tests/tests/verify/ui/predicate.stdout +++ b/prusti-tests/tests/verify/ui/predicate.stdout @@ -162,12 +162,12 @@ fn main() { test_identity_2(); precond_or_correctly(); } -Procedure(ProcedureSpecification { kind: Inherent(Pure), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Predicate(DefId(0:6 ~ predicate[$(CRATE_ID)]::prusti_pred_item_true_p1_$(NUM_UUID)))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(true) }) -Procedure(ProcedureSpecification { kind: Inherent(Predicate(DefId(0:9 ~ predicate[$(CRATE_ID)]::prusti_pred_item_true_p2_$(NUM_UUID)))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(true) }) -Procedure(ProcedureSpecification { kind: Inherent(Predicate(DefId(0:25 ~ predicate[$(CRATE_ID)]::prusti_pred_item_false_p_$(NUM_UUID)))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(true) }) -Procedure(ProcedureSpecification { kind: Inherent(Predicate(DefId(0:12 ~ predicate[$(CRATE_ID)]::prusti_pred_item_forall_identity_$(NUM_UUID)))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(true) }) -Procedure(ProcedureSpecification { kind: Inherent(Predicate(DefId(0:15 ~ predicate[$(CRATE_ID)]::prusti_pred_item_exists_identity_$(NUM_UUID)))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(true) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:27 ~ predicate[$(CRATE_ID)]::prusti_pre_item_precond_or_correctly_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:19 ~ predicate[$(CRATE_ID)]::prusti_pre_item_test_identity_1_$(NUM_UUID)), DefId(0:20 ~ predicate[$(CRATE_ID)]::prusti_pre_item_test_identity_1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:22 ~ predicate[$(CRATE_ID)]::prusti_pre_item_test_identity_2_$(NUM_UUID)), DefId(0:23 ~ predicate[$(CRATE_ID)]::prusti_pre_item_test_identity_2_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/predicate.rs:10:1: 10:27 (#0)), kind: Inherent(Pure), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/predicate.rs:13:5: 13:25 (#0)), kind: Inherent(Predicate(DefId(0:6 ~ predicate[$(CRATE_ID)]::prusti_pred_item_true_p1_$(NUM_UUID)))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(true) }) +Procedure(ProcedureSpecification { span: Some($DIR/predicate.rs:19:5: 19:25 (#0)), kind: Inherent(Predicate(DefId(0:9 ~ predicate[$(CRATE_ID)]::prusti_pred_item_true_p2_$(NUM_UUID)))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(true) }) +Procedure(ProcedureSpecification { span: Some($DIR/predicate.rs:45:5: 45:25 (#0)), kind: Inherent(Predicate(DefId(0:25 ~ predicate[$(CRATE_ID)]::prusti_pred_item_false_p_$(NUM_UUID)))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(true) }) +Procedure(ProcedureSpecification { span: Some($DIR/predicate.rs:25:5: 25:33 (#0)), kind: Inherent(Predicate(DefId(0:12 ~ predicate[$(CRATE_ID)]::prusti_pred_item_forall_identity_$(NUM_UUID)))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(true) }) +Procedure(ProcedureSpecification { span: Some($DIR/predicate.rs:31:5: 31:33 (#0)), kind: Inherent(Predicate(DefId(0:15 ~ predicate[$(CRATE_ID)]::prusti_pred_item_exists_identity_$(NUM_UUID)))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(true) }) +Procedure(ProcedureSpecification { span: Some($DIR/predicate.rs:53:1: 53:34 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:27 ~ predicate[$(CRATE_ID)]::prusti_pre_item_precond_or_correctly_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/predicate.rs:38:1: 38:21 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:19 ~ predicate[$(CRATE_ID)]::prusti_pre_item_test_identity_1_$(NUM_UUID)), DefId(0:20 ~ predicate[$(CRATE_ID)]::prusti_pre_item_test_identity_1_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/predicate.rs:42:1: 42:21 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:22 ~ predicate[$(CRATE_ID)]::prusti_pre_item_test_identity_2_$(NUM_UUID)), DefId(0:23 ~ predicate[$(CRATE_ID)]::prusti_pre_item_test_identity_2_$(NUM_UUID))]), posts: Empty, pledges: Empty, trusted: Inherent(false) }) diff --git a/prusti-tests/tests/verify/ui/pure.stdout b/prusti-tests/tests/verify/ui/pure.stdout index 809030a5673..d50ec9f914a 100644 --- a/prusti-tests/tests/verify/ui/pure.stdout +++ b/prusti-tests/tests/verify/ui/pure.stdout @@ -102,9 +102,9 @@ fn prusti_post_item_test_max5_$(NUM_UUID)(a: i32, b: i32, #[prusti::post_spec_id_ref = "$(NUM_UUID)"] fn test_max5(a: i32, b: i32) -> i32 { a } fn main() {} -Procedure(ProcedureSpecification { kind: Inherent(Pure), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Pure), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:12 ~ pure[$(CRATE_ID)]::prusti_post_item_test_max3_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:9 ~ pure[$(CRATE_ID)]::prusti_post_item_test_identity2_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:14 ~ pure[$(CRATE_ID)]::prusti_pre_item_test_max4_$(NUM_UUID))]), posts: Inherent([DefId(0:15 ~ pure[$(CRATE_ID)]::prusti_post_item_test_max4_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) -Procedure(ProcedureSpecification { kind: Inherent(Impure), pres: Inherent([DefId(0:17 ~ pure[$(CRATE_ID)]::prusti_pre_item_test_max5_$(NUM_UUID))]), posts: Inherent([DefId(0:18 ~ pure[$(CRATE_ID)]::prusti_post_item_test_max5_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/pure.rs:9:1: 9:27 (#0)), kind: Inherent(Pure), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/pure.rs:20:1: 20:30 (#0)), kind: Inherent(Pure), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/pure.rs:54:1: 54:22 (#0)), kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:12 ~ pure[$(CRATE_ID)]::prusti_post_item_test_max3_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/pure.rs:16:1: 16:20 (#0)), kind: Inherent(Impure), pres: Empty, posts: Inherent([DefId(0:9 ~ pure[$(CRATE_ID)]::prusti_post_item_test_identity2_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/pure.rs:62:1: 62:36 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:14 ~ pure[$(CRATE_ID)]::prusti_pre_item_test_max4_$(NUM_UUID))]), posts: Inherent([DefId(0:15 ~ pure[$(CRATE_ID)]::prusti_post_item_test_max4_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) +Procedure(ProcedureSpecification { span: Some($DIR/pure.rs:68:1: 68:36 (#0)), kind: Inherent(Impure), pres: Inherent([DefId(0:17 ~ pure[$(CRATE_ID)]::prusti_pre_item_test_max5_$(NUM_UUID))]), posts: Inherent([DefId(0:18 ~ pure[$(CRATE_ID)]::prusti_post_item_test_max5_$(NUM_UUID))]), pledges: Empty, trusted: Inherent(false) }) diff --git a/prusti-tests/tests/verify_overflow/fail/extern-spec/trait-impls/traits-2.rs b/prusti-tests/tests/verify_overflow/fail/extern-spec/trait-impls/traits-2.rs index 54b238679b0..b5e8334cfaa 100644 --- a/prusti-tests/tests/verify_overflow/fail/extern-spec/trait-impls/traits-2.rs +++ b/prusti-tests/tests/verify_overflow/fail/extern-spec/trait-impls/traits-2.rs @@ -22,7 +22,7 @@ impl Max for Point { #[pure] #[ensures(result >= self.0 && result >= self.1)] #[ensures(result == self.0 || result == self.1)] - fn max(&mut self) -> i32; //~ ERROR: pure function parameters must be Copy + fn max(&mut self) -> i32; //~ ERROR: pure function parameters must be Copy } fn main() { diff --git a/prusti-tests/tests/verify_overflow/pass/issues/issue-878.rs b/prusti-tests/tests/verify_overflow/pass/issues/issue-878.rs new file mode 100644 index 00000000000..8757945799e --- /dev/null +++ b/prusti-tests/tests/verify_overflow/pass/issues/issue-878.rs @@ -0,0 +1,18 @@ +use prusti_contracts::*; +use std::cmp::{Ord, Ordering}; +fn main() {} + +#[extern_spec] +trait Ord { + #[pure] + fn cmp(&self, other: &Self) -> Ordering; +} + +#[pure] +pub fn eq(a: &T, b: &T) -> bool { + match a.cmp(b) { + Ordering::Equal => true, + Ordering::Less => false, + Ordering::Greater => false, + } +} diff --git a/prusti-tests/tests/verify_overflow/pass/quantifiers/generics.rs b/prusti-tests/tests/verify_overflow/pass/quantifiers/generics.rs new file mode 100644 index 00000000000..f7d1e890229 --- /dev/null +++ b/prusti-tests/tests/verify_overflow/pass/quantifiers/generics.rs @@ -0,0 +1,58 @@ +use prusti_contracts::*; +use std::cmp::{Ord, Ordering::{self, Equal, Less}}; + +fn main() { + let mut v = 42; + client(&mut v, true); +} + +#[pure] +fn tautology(_arg: &T, _arg2: &T) -> bool { true } + +#[requires(forall(|other: &T| tautology(&x, other)))] +#[ensures(forall(|other: T| tautology(&other, &result)))] +fn foo(x: T) -> T { x } + +#[extern_spec] +trait Ord { + #[pure] + fn cmp(&self, other: &Self) -> Ordering; +} + +#[extern_spec] +impl Ord for i32 { + #[pure] + #[ensures( + (*self == *other) == matches!(result, Ordering::Equal) + && (*self < *other) == matches!(result, Ordering::Less) + && (*self > *other) == matches!(result, Ordering::Greater) + )] + fn cmp(&self, other: &Self) -> Ordering; +} + +// TODO: this encodes correctly but we don't yet have API invariants to ensure +// e.g. that `cmp` is transitive. (Lemma method is a possible workaround.) + +//#[requires(forall(|other: &T| +// matches!(_lower.cmp(other), Less) +// && matches!(other.cmp(_upper), Less) +// ==> matches!(_only_middle.cmp(other), Equal)))] +#[requires(forall(|other: &T| + matches!(_lower.cmp(other), Less) + && matches!(other.cmp(_upper), Less) + ==> true))] +fn bar(_lower: &T, _only_middle: &T, _upper: &T) { } + +fn client(x1: U, y1: T) { + let x2 = foo(x1); + bar(&x2, &x2, &x2); + + let y2 = foo(y1); + let y3 = y2; + bar(&y2, &y1, &y3); + + let val1 = 10; + let val2 = foo(val1); + let val3 = val1; + bar(&val1, &val3, &val2); +} diff --git a/prusti-viper/src/encoder/encoder.rs b/prusti-viper/src/encoder/encoder.rs index e02da1a5bcc..f1bd1a6fc23 100644 --- a/prusti-viper/src/encoder/encoder.rs +++ b/prusti-viper/src/encoder/encoder.rs @@ -718,8 +718,8 @@ impl<'v, 'tcx> Encoder<'v, 'tcx> { ty::ReEarlyBound(_) => { unimplemented!("ReEarlyBound: {}", format!("{}", region)); }, - ty::ReLateBound(_, _) => { - unimplemented!("ReLateBound: {}", format!("{}", region)); + ty::ReLateBound(debruijn, bound_reg) => { + format!("lft_late_{}_{}", debruijn.index(), bound_reg.var.index()) }, ty::ReFree(_) => { unimplemented!("ReFree: {}", format!("{}", region)); diff --git a/prusti-viper/src/encoder/foldunfold/footprint.rs b/prusti-viper/src/encoder/foldunfold/footprint.rs index b47cf24cc9a..582c9b82656 100644 --- a/prusti-viper/src/encoder/foldunfold/footprint.rs +++ b/prusti-viper/src/encoder/foldunfold/footprint.rs @@ -115,9 +115,6 @@ impl ExprFootprintGetter for vir::Expr { box body, .. }) => { - assert!(variables - .iter() - .all(|var| !var.typ.is_typed_ref_or_type_var())); let vars_places: FxHashSet = variables .iter() .map(|var| Acc(vir::Expr::local(var.clone()), PermAmount::Write)) diff --git a/prusti-viper/src/encoder/high/pure_functions/interface.rs b/prusti-viper/src/encoder/high/pure_functions/interface.rs index 66a2a9e595d..c54da46a10d 100644 --- a/prusti-viper/src/encoder/high/pure_functions/interface.rs +++ b/prusti-viper/src/encoder/high/pure_functions/interface.rs @@ -12,6 +12,7 @@ pub(crate) trait HighPureFunctionEncoderInterface<'tcx> { fn encode_discriminant_call( &self, adt: vir_high::Expression, + return_type: vir_high::Type, ) -> EncodingResult; fn encode_index_call( &self, @@ -54,9 +55,9 @@ impl<'v, 'tcx: 'v> HighPureFunctionEncoderInterface<'tcx> fn encode_discriminant_call( &self, adt: vir_high::Expression, + return_type: vir_high::Type, ) -> EncodingResult { let name = "discriminant"; - let return_type = vir_high::Type::Int(vir_high::ty::Int::Isize); Ok(vir_high::Expression::function_call( name, vec![], // FIXME: This is most likely wrong. diff --git a/prusti-viper/src/encoder/mir/pure/interpreter/mod.rs b/prusti-viper/src/encoder/mir/pure/interpreter/mod.rs index 5d4d402f2e0..852377d9ab8 100644 --- a/prusti-viper/src/encoder/mir/pure/interpreter/mod.rs +++ b/prusti-viper/src/encoder/mir/pure/interpreter/mod.rs @@ -30,7 +30,7 @@ use rustc_span::Span; use vir_crate::{ common::expression::{BinaryOperationHelpers, UnaryOperationHelpers}, - high::{self as vir_high}, + high::{self as vir_high, operations::ty::Typed}, }; // FIXME: Make this explicitly accessible only to spec_encoder and pure @@ -75,10 +75,6 @@ impl<'p, 'v: 'p, 'tcx: 'v> ExpressionBackwardInterpreter<'p, 'v, 'tcx> { } } - pub(super) fn mir_encoder(&self) -> &MirEncoder<'p, 'v, 'tcx> { - &self.mir_encoder - } - fn encode_place(&self, place: mir::Place<'tcx>) -> SpannedEncodingResult { self.encoder.encode_place_high(self.mir, place) } @@ -228,7 +224,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ExpressionBackwardInterpreter<'p, 'v, 'tcx> { } mir::Rvalue::Discriminant(src) => { let arg = self.encoder.encode_place_high(self.mir, *src)?; - let expr = self.encoder.encode_discriminant_call(arg).with_span(span)?; + let expr = self + .encoder + .encode_discriminant_call(arg, encoded_lhs.get_type().clone()) + .with_span(span)?; state.substitute_value(&encoded_lhs, expr); } mir::Rvalue::Ref(_, mir::BorrowKind::Unique, place) diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs index 7048d0587eb..cf8f1564f49 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs @@ -34,26 +34,62 @@ use vir_crate::{ pub(super) struct PureFunctionEncoder<'p, 'v: 'p, 'tcx: 'v> { encoder: &'p Encoder<'v, 'tcx>, + /// The function to be encoded. proc_def_id: DefId, - mir: &'p mir::Body<'tcx>, - interpreter: PureFunctionBackwardInterpreter<'p, 'v, 'tcx>, + /// Where is this being encoded? + pure_encoding_context: PureEncodingContext, parent_def_id: DefId, + /// Type substitutions applied to the MIR (if any) and the signature. substs: SubstsRef<'tcx>, + /// Span of the function declaration. + span: Span, + /// Signature of the function to be encoded. + sig: ty::FnSig<'tcx>, + /// Spans of MIR locals, when encoding a local pure function. + local_spans: Option>, +} + +/// Used to encode expressions in assertions +pub(super) fn encode_body<'p, 'v: 'p, 'tcx: 'v>( + encoder: &'p Encoder<'v, 'tcx>, + proc_def_id: DefId, + pure_encoding_context: PureEncodingContext, + parent_def_id: DefId, + substs: SubstsRef<'tcx>, +) -> SpannedEncodingResult { + let mir = encoder.env().local_mir(proc_def_id.expect_local(), substs); + let interpreter = PureFunctionBackwardInterpreter::new( + encoder, + &mir, + proc_def_id, + pure_encoding_context, + parent_def_id, + ); + + let function_name = encoder.env().get_absolute_item_name(proc_def_id); + debug!("Encode body of pure function {}", function_name); + + let state = run_backward_interpretation(&mir, &interpreter)? + .unwrap_or_else(|| panic!("Procedure {:?} contains a loop", proc_def_id)); + let body_expr = state.into_expr().unwrap(); + debug!( + "Pure function body {} has been encoded with expr: {}", + function_name, body_expr + ); + + Ok(body_expr) } impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { pub fn new( encoder: &'p Encoder<'v, 'tcx>, proc_def_id: DefId, - mir: &'p mir::Body<'tcx>, pure_encoding_context: PureEncodingContext, parent_def_id: DefId, substs: SubstsRef<'tcx>, ) -> Self { trace!("PureFunctionEncoder constructor: {:?}", proc_def_id); - let proc_def_id = encoder.get_wrapper_def_id(proc_def_id); - // should hold for extern specs as well (otherwise there would have // been an error reported earlier) assert_eq!( @@ -61,65 +97,63 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { encoder.env().identity_substs(proc_def_id).len() ); - let interpreter = PureFunctionBackwardInterpreter::new( - encoder, - mir, - proc_def_id, - pure_encoding_context, - parent_def_id, - substs, - ); + let span = encoder.get_spec_span(proc_def_id); + + // TODO: move this to a signatures module + use crate::rustc_middle::ty::subst::Subst; + let sig = encoder + .env() + .tcx() + .fn_sig(proc_def_id) + .subst(encoder.env().tcx(), substs) + .skip_binder(); + PureFunctionEncoder { encoder, proc_def_id, - mir, - interpreter, + pure_encoding_context, parent_def_id, substs, + span, + sig, + local_spans: None, } } - /// Used to encode expressions in assertions - pub fn encode_body(&self) -> SpannedEncodingResult { - let function_name = self.encoder.env().get_absolute_item_name(self.proc_def_id); - debug!("Encode body of pure function {}", function_name); - - let state = run_backward_interpretation(self.mir, &self.interpreter)? - .unwrap_or_else(|| panic!("Procedure {:?} contains a loop", self.proc_def_id)); - let body_expr = state.into_expr().unwrap(); - debug!( - "Pure function body {} has been encoded with expr: {}", - function_name, body_expr + pub fn encode_function(&mut self) -> SpannedEncodingResult { + let mir = self + .encoder + .env() + .local_mir(self.proc_def_id.expect_local(), self.substs); + let interpreter = PureFunctionBackwardInterpreter::new( + self.encoder, + &mir, + self.proc_def_id, + self.pure_encoding_context, + self.parent_def_id, ); - Ok(body_expr) - } + self.local_spans = Some( + (0..=self.sig.inputs().len()) + .map(|idx| { + interpreter + .mir_encoder() + .get_local_span(mir::Local::from_usize(idx)) + }) + .collect(), + ); - pub fn encode_function(&self) -> SpannedEncodingResult { let function_name = self.encode_function_name(); debug!("Encode pure function {}", function_name); - let mut state = run_backward_interpretation(self.mir, &self.interpreter)? + let mut state = run_backward_interpretation(&mir, &interpreter)? .unwrap_or_else(|| panic!("Procedure {:?} contains a loop", self.proc_def_id)); // Fix arguments - for arg in self.mir.args_iter() { - let arg_ty = self.interpreter.mir_encoder().get_local_ty(arg); - let span = self.get_local_span(arg); - let target_place = self - .encoder - .encode_value_expr( - vir::Expr::local(self.interpreter.mir_encoder().encode_local(arg)?), - arg_ty, - ) - .with_span(span)?; - let mut new_place: vir::Expr = self.encode_local(arg)?.into(); - if let ty::TyKind::Ref(_, _, _) = arg_ty.kind() { - // patch references with an explicit snap app - // TODO: this probably needs to be adjusted when snapshots of - // references are implemented - new_place = vir::Expr::snap_app(new_place); - } - state.substitute_value(&target_place, new_place); + if let Some(curr_expr) = state.expr_mut() { + // Replace two times to avoid cloning `expr`, which could be big. + let expr = std::mem::replace(curr_expr, true.into()); + let new_expr = self.fix_arguments(expr)?; + let _ = std::mem::replace(curr_expr, new_expr); } let mut body_expr = state.into_expr().unwrap(); @@ -130,14 +164,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { // if the function returns a snapshot, we take a snapshot of the body if self.encode_function_return_type()?.is_snapshot() { - let ty = self.mir.return_ty(); - let return_span = self.get_local_span(mir::RETURN_PLACE); - + let ty = self.sig.output(); let param_env = self.encoder.env().tcx().param_env(self.proc_def_id); + if !self.encoder.env().type_is_copy(ty, param_env) { return Err(SpannedEncodingError::unsupported( "return type of pure function does not implement Copy", - return_span, + self.get_return_span(), )); } @@ -160,11 +193,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { let function_name = self.encode_function_name(); debug!("Encode predicate function {}", function_name); - let mir_span = self.encoder.env().tcx().def_span(self.proc_def_id); let contract = self .encoder .get_procedure_contract_for_def(self.proc_def_id, self.substs) - .with_span(mir_span)?; + .with_span(self.span)?; let encoded_args = contract .args .iter() @@ -209,7 +241,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { let contract = self .encoder .get_procedure_contract_for_def(self.proc_def_id, self.substs) - .with_span(self.mir.span)?; + .with_span(self.span)?; let (type_precondition, func_precondition) = self.encode_precondition_expr(&contract)?; @@ -220,7 +252,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { let return_type = self.encode_function_return_type()?; let res_value_range_pos = self.encoder.error_manager().register_error( - self.mir.span, + self.span, ErrorCtxt::PureFunctionPostconditionValueRangeOfResult, self.parent_def_id, ); @@ -228,14 +260,14 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { // Add value range of the arguments and return value to the pre/postconditions if config::check_overflows() { debug_assert!(self.encoder.env().type_is_copy( - self.mir.return_ty(), + self.sig.output(), self.encoder.env().tcx().param_env(self.proc_def_id) )); let mut return_bounds: Vec<_> = self .encoder .encode_type_bounds( &vir::Expr::local(pure_fn_return_variable), - self.mir.return_ty(), + self.sig.output(), ) .into_iter() .map(|p| p.set_default_pos(res_value_range_pos)) @@ -243,8 +275,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { return_bounds.extend(postcondition); postcondition = return_bounds; - for (formal_arg, local) in formal_args.iter().zip(self.mir.args_iter()) { - let typ = self.interpreter.mir_encoder().get_local_ty(local); + for (formal_arg, local) in formal_args.iter().zip(self.args_iter()) { + let typ = self.get_local_ty(local); debug_assert!(self .encoder .env() @@ -256,12 +288,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { precondition = bounds; } } else if config::encode_unsigned_num_constraint() { - if let ty::TyKind::Uint(_) = self.mir.return_ty().kind() { + if let ty::TyKind::Uint(_) = self.sig.output().kind() { let expr = vir::Expr::le_cmp(0u32.into(), pure_fn_return_variable.into()); postcondition.push(expr.set_default_pos(res_value_range_pos)); } - for (formal_arg, local) in formal_args.iter().zip(self.mir.args_iter()) { - let typ = self.interpreter.mir_encoder().get_local_ty(local); + for (formal_arg, local) in formal_args.iter().zip(self.args_iter()) { + let typ = self.get_local_ty(local); if let ty::TyKind::Uint(_) = typ.kind() { precondition.push(vir::Expr::le_cmp(0u32.into(), formal_arg.into())); } @@ -297,36 +329,41 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { function = self .encoder .patch_snapshots_function(function) - .with_span(self.mir.span)?; + .with_span(self.span)?; // Fix arguments - if let Some(mut body) = function.body.take() { - for arg in self.mir.args_iter() { - let arg_ty = self.interpreter.mir_encoder().get_local_ty(arg); - let span = self.get_local_span(arg); - let target_place = self - .encoder - .encode_value_expr( - vir::Expr::local(self.interpreter.mir_encoder().encode_local(arg)?), - arg_ty, - ) - .with_span(span)?; - let mut new_place: vir::Expr = self.encode_local(arg)?.into(); - if let ty::TyKind::Ref(_, _, _) = arg_ty.kind() { - // patch references with an explicit snap app - // TODO: this probably needs to be adjusted when snapshots of - // references are implemented - new_place = vir::Expr::snap_app(new_place); - } - body = body.replace_place(&target_place, &new_place); - } - function.body = Some(body) + if let Some(body) = function.body.take() { + function.body = Some(self.fix_arguments(body)?); } // Add folding/unfolding Ok(function) } + fn fix_arguments(&self, mut expr: vir::Expr) -> SpannedEncodingResult { + for arg in self.args_iter() { + let arg_ty = self.get_local_ty(arg); + let span = self.get_local_span(arg); + let target_place = self + .encoder + .encode_value_expr(vir::Expr::local(self.encode_mir_local(arg)?), arg_ty) + .with_span(span)?; + let mut new_place: vir::Expr = self.encode_local(arg)?.into(); + if let ty::TyKind::Ref(_, _, _) = arg_ty.kind() { + // patch references with an explicit snap app + // TODO: this probably needs to be adjusted when snapshots of + // references are implemented + new_place = vir::Expr::snap_app(new_place); + } + expr = expr.replace_place(&target_place, &new_place); + } + Ok(expr) + } + + fn args_iter(&self) -> impl Iterator { + (0..self.sig.inputs().len()).map(|idx| mir::Local::from_usize(1 + idx)) + } + /// Encode the precondition with two expressions: /// - one for the type encoding /// - one for the functional specification. @@ -336,19 +373,14 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { ) -> SpannedEncodingResult<(vir::Expr, vir::Expr)> { let mut type_spec = vec![]; for &local in contract.args.iter() { - let local_ty = self.interpreter.mir_encoder().get_local_ty(local.into()); + let local_ty = self.get_local_ty(local.into()); let fraction = if let ty::TyKind::Ref(_, _, hir::Mutability::Not) = local_ty.kind() { vir::PermAmount::Read } else { vir::PermAmount::Write }; - let opt_pred_perm = self - .interpreter - .mir_encoder() - .encode_place_predicate_permission( - self.encode_local(local.into())?.into(), - fraction, - ); + let opt_pred_perm = + vir::Expr::pred_permission(self.encode_local(local.into())?.into(), fraction); if let Some(spec) = opt_pred_perm { type_spec.push(spec) } @@ -425,7 +457,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { // TODO: use a better span let postcondition_pos = self.encoder.error_manager().register_error( - self.mir.span, + self.span, ErrorCtxt::PureFunctionDefinition, self.parent_def_id, ); @@ -440,19 +472,45 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { Ok(post) } + /// Encodes a VIR local with a snapshot type. fn encode_local(&self, local: mir::Local) -> SpannedEncodingResult { - let mir_encoder = self.interpreter.mir_encoder(); - let var_name = mir_encoder.encode_local_var_name(local); - let var_span = mir_encoder.get_local_span(local); + let var_name = format!("{:?}", local); + let var_span = self.get_local_span(local); + let var_type = self + .encoder + .encode_snapshot_type(self.get_local_ty(local)) + .with_span(var_span)?; + Ok(vir::LocalVar::new(var_name, var_type)) + } + + /// Encodes a VIR local with the original MIR type. + fn encode_mir_local(&self, local: mir::Local) -> SpannedEncodingResult { + let var_name = format!("{:?}", local); + let var_span = self.get_local_span(local); let var_type = self .encoder - .encode_snapshot_type(self.interpreter.mir_encoder().get_local_ty(local)) + .encode_type(self.get_local_ty(local)) .with_span(var_span)?; Ok(vir::LocalVar::new(var_name, var_type)) } + fn get_local_ty(&self, local: mir::Local) -> ty::Ty<'tcx> { + if local.as_usize() == 0 { + self.sig.output() + } else { + self.sig.inputs()[local.as_usize() - 1] + } + } + fn get_local_span(&self, local: mir::Local) -> Span { - self.interpreter.mir_encoder().get_local_span(local) + self.local_spans + .as_ref() + .map(|spans| spans[local.index()]) + .unwrap_or(self.span) + } + + fn get_return_span(&self) -> Span { + self.get_local_span(mir::RETURN_PLACE) } pub fn encode_function_name(&self) -> String { @@ -460,46 +518,46 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> { } pub fn encode_function_return_type(&self) -> SpannedEncodingResult { - let ty = self.mir.return_ty(); - let return_span = self.get_local_span(mir::RETURN_PLACE); + let ty = self.sig.output(); // Return an error for unsupported return types let param_env = self.encoder.env().tcx().param_env(self.proc_def_id); if !self.encoder.env().type_is_copy(ty, param_env) { return Err(SpannedEncodingError::incorrect( "return type of pure function does not implement Copy", - return_span, + self.get_return_span(), )); } - let return_local = mir::Place::return_place().as_local().unwrap(); - let span = self.interpreter.mir_encoder().get_local_span(return_local); - self.encoder.encode_snapshot_type(ty).with_span(span) + self.encoder + .encode_snapshot_type(ty) + .with_span(self.get_return_span()) } fn encode_type_arguments(&self) -> SpannedEncodingResult> { self.encoder .encode_generic_arguments(self.proc_def_id, self.substs) - .with_span(self.mir.span) + .with_span(self.span) } fn encode_formal_args(&self) -> SpannedEncodingResult> { let mut formal_args = vec![]; - for local in self.mir.args_iter() { - let mir_encoder = self.interpreter.mir_encoder(); - let var_name = mir_encoder.encode_local_var_name(local); - let var_span = mir_encoder.get_local_span(local); - let mir_type = mir_encoder.get_local_ty(local); + for (local_idx, local_ty) in self.sig.inputs().iter().enumerate() { + let local = rustc_middle::mir::Local::from_usize(local_idx + 1); + let var_name = format!("{:?}", local); + let var_span = self.get_local_span(local); + let param_env = self.encoder.env().tcx().param_env(self.proc_def_id); - if !self.encoder.env().type_is_copy(mir_type, param_env) { + if !self.encoder.env().type_is_copy(*local_ty, param_env) { return Err(SpannedEncodingError::incorrect( "pure function parameters must be Copy", var_span, )); } + let var_type = self .encoder - .encode_snapshot_type(mir_type) + .encode_snapshot_type(*local_ty) .with_span(var_span)?; formal_args.push(vir::LocalVar::new(var_name, var_type)) } diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs index 314846a5f58..fbc36162ec7 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs @@ -29,7 +29,7 @@ type FunctionConstructor<'v, 'tcx> = Box< /// Depending on the context of the pure encoding, /// panics will be encoded slightly differently. -#[derive(PartialEq, Eq)] +#[derive(PartialEq, Eq, Clone, Copy)] pub(crate) enum PureEncodingContext { /// Panics will be encoded as calls to unreachable functions /// (which have a `requires false` pre-condition). @@ -167,11 +167,9 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx> .borrow() .contains_key(&key) { - let procedure = self.env().get_procedure(proc_def_id); let body = super::new_encoder::encode_pure_expression( self, proc_def_id, - procedure.get_mir(), parent_def_id, substs, )?; @@ -205,11 +203,9 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx> .borrow() .contains_key(&key) { - let mir = self.env().local_mir(proc_def_id.expect_local(), substs); - let pure_function_encoder = PureFunctionEncoder::new( + let body = super::encoder::encode_body( self, proc_def_id, - &mir, if self.is_encoding_trigger.get() { // quantifier triggers might not evaluate to boolean PureEncodingContext::Trigger @@ -218,8 +214,7 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx> }, parent_def_id, substs, - ); - let body = pure_function_encoder.encode_body()?; + )?; self.pure_function_encoder_state .bodies_poly .borrow_mut() @@ -264,14 +259,9 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx> .borrow_mut() .insert(key.clone()); - let wrapper_def_id = self.get_wrapper_def_id(proc_def_id); - - let mir = self.env().local_mir(wrapper_def_id.expect_local(), substs); - let mir_span = mir.span; - let pure_function_encoder = PureFunctionEncoder::new( + let mut pure_function_encoder = PureFunctionEncoder::new( self, proc_def_id, - &mir, PureEncodingContext::Code, proc_def_id, substs, @@ -292,7 +282,6 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx> let _ = super::new_encoder::encode_function_decl( self, proc_def_id, - &mir, proc_def_id, substs, )?; @@ -322,12 +311,10 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx> } Err(error) => { self.register_encoding_error(error); - debug!( - "Error encoding pure function: {:?} wrapper_def_id={:?}", - proc_def_id, wrapper_def_id - ); - let body = self.env().external_mir(wrapper_def_id); - let stub_encoder = StubFunctionEncoder::new(self, proc_def_id, body, substs); + debug!("Error encoding pure function: {:?}", proc_def_id); + let body = self.env().external_mir(proc_def_id, substs); + // TODO(tymap): does stub encoder need substs? + let stub_encoder = StubFunctionEncoder::new(self, proc_def_id, &body, substs); let function = stub_encoder.encode_function()?; self.log_vir_program_before_viper(function.to_string()); let identifier = self.insert_function(function); @@ -391,13 +378,9 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx> if !call_infos.contains_key(&key) { // Compute information necessary to encode the function call and // memoize it. - let wrapper_def_id = self.get_wrapper_def_id(proc_def_id); - - let mir = self.env().local_mir(wrapper_def_id.expect_local(), substs); let pure_function_encoder = PureFunctionEncoder::new( self, proc_def_id, - &mir, PureEncodingContext::Code, parent_def_id, substs, @@ -458,13 +441,9 @@ impl<'v, 'tcx: 'v> PureFunctionEncoderInterface<'v, 'tcx> if !call_infos.contains_key(&key) { // Compute information necessary to encode the function call and // memoize it. - let wrapper_def_id = self.get_wrapper_def_id(proc_def_id); - - let mir = self.env().local_mir(wrapper_def_id.expect_local(), substs); let function_call_info = super::new_encoder::encode_function_call_info( self, proc_def_id, - &mir, parent_def_id, substs, )?; diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs index 57ae94fb062..5ac18459637 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs @@ -25,10 +25,7 @@ use prusti_common::vir_local; use rustc_hash::FxHashMap; use rustc_hir::def_id::DefId; -use rustc_middle::{ - mir, span_bug, ty, - ty::subst::{Subst, SubstsRef}, -}; +use rustc_middle::{mir, span_bug, ty}; use std::{convert::TryInto, mem}; use vir_crate::polymorphic::{self as vir}; @@ -43,7 +40,6 @@ pub(crate) struct PureFunctionBackwardInterpreter<'p, 'v: 'p, 'tcx: 'v> { pure_encoding_context: PureEncodingContext, /// DefId of the caller. Used for error reporting. caller_def_id: DefId, - substs: SubstsRef<'tcx>, def_id: DefId, // TODO(tymap): is this actually caller_def_id? } @@ -57,7 +53,6 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionBackwardInterpreter<'p, 'v, 'tcx> { def_id: DefId, pure_encoding_context: PureEncodingContext, caller_def_id: DefId, - substs: SubstsRef<'tcx>, ) -> Self { PureFunctionBackwardInterpreter { encoder, @@ -65,7 +60,6 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionBackwardInterpreter<'p, 'v, 'tcx> { mir_encoder: MirEncoder::new(encoder, mir, def_id), pure_encoding_context, caller_def_id, - substs, def_id, } } @@ -413,9 +407,6 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> let full_func_proc_name: &str = &tcx.def_path_str(def_id); let func_proc_name = &self.encoder.env().get_item_name(def_id); - // compose substitutions - let composed_substs = call_substs.subst(self.encoder.env().tcx(), self.substs); - let state = if destination.is_some() { let (ref lhs_place, target_block) = destination.as_ref().unwrap(); let (encoded_lhs, ty, _) = self.encode_place(lhs_place).with_span(span)?; @@ -585,7 +576,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> span, encoded_args, self.caller_def_id, - composed_substs, + call_substs, )?; let mut state = states[target_block].clone(); state.substitute_value(&encoded_lhs, expr); @@ -594,10 +585,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> // simple function call _ => { - let (called_def_id, composed_substs) = self + let (called_def_id, call_substs) = self .encoder .env() - .resolve_method_call(self.def_id, def_id, composed_substs); + .resolve_method_call(self.def_id, def_id, call_substs); trace!("Resolved function call: {:?}", called_def_id); let is_pure_function = self.encoder.is_pure(called_def_id); @@ -606,7 +597,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> .encode_pure_function_use( called_def_id, self.caller_def_id, - composed_substs, + call_substs, ) .with_span(term.source_info.span)? } else { @@ -638,7 +629,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> ); let type_arguments = self .encoder - .encode_generic_arguments(called_def_id, composed_substs) + .encode_generic_arguments(called_def_id, call_substs) .with_span(term.source_info.span)?; let encoded_rhs = vir::Expr::func_app( function_name, diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs index 5803ef7f5ab..b78146d1445 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/new_encoder.rs @@ -4,21 +4,21 @@ use crate::encoder::{ errors::{ErrorCtxt, SpannedEncodingError, SpannedEncodingResult, WithSpan}, mir::{ generics::MirGenericsEncoderInterface, - places::PlacesEncoderInterface, pure::{ interpreter::ExpressionBackwardInterpreter, specifications::SpecificationEncoderInterface, }, + specifications::SpecificationsInterface, types::MirTypeEncoderInterface, }, - mir_encoder::{MirEncoder, PlaceEncoder}, mir_interpreter::run_backward_interpretation, Encoder, }; + use log::{debug, trace}; use prusti_common::vir_high_local; use rustc_hir::def_id::DefId; -use rustc_middle::{mir, ty::subst::SubstsRef}; +use rustc_middle::{mir, ty, ty::subst::SubstsRef}; use rustc_span::Span; use vir_crate::{ common::{expression::ExpressionIterator, position::Positioned}, @@ -28,20 +28,10 @@ use vir_crate::{ pub(super) fn encode_function_decl<'p, 'v: 'p, 'tcx: 'v>( encoder: &'p Encoder<'v, 'tcx>, proc_def_id: DefId, - mir: &'p mir::Body<'tcx>, parent_def_id: DefId, substs: SubstsRef<'tcx>, ) -> SpannedEncodingResult { - let interpreter = - ExpressionBackwardInterpreter::new(encoder, mir, proc_def_id, false, parent_def_id, substs); - let pure_encoder = PureEncoder { - encoder, - proc_def_id, - mir, - parent_def_id, - substs, - interpreter, - }; + let pure_encoder = PureEncoder::new(encoder, proc_def_id, parent_def_id, substs); let function_decl = pure_encoder.encode_function_decl()?; if function_decl.body.is_some() { // Check that function does not call itself in its contract. @@ -84,43 +74,46 @@ pub(super) fn encode_function_decl<'p, 'v: 'p, 'tcx: 'v>( pub(super) fn encode_pure_expression<'p, 'v: 'p, 'tcx: 'v>( encoder: &'p Encoder<'v, 'tcx>, proc_def_id: DefId, - mir: &'p mir::Body<'tcx>, parent_def_id: DefId, substs: SubstsRef<'tcx>, ) -> SpannedEncodingResult { - let interpreter = - ExpressionBackwardInterpreter::new(encoder, mir, proc_def_id, false, parent_def_id, substs); - let encoder = PureEncoder { + let mir = encoder.env().local_mir(proc_def_id.expect_local(), substs); + let interpreter = ExpressionBackwardInterpreter::new( encoder, + &mir, proc_def_id, - mir, + false, parent_def_id, substs, - interpreter, - }; - encoder.encode_pure_expression() + ); + let state = run_backward_interpretation(&mir, &interpreter)?.ok_or_else(|| { + SpannedEncodingError::incorrect( + format!("procedure {:?} contains a loop", proc_def_id), + encoder.env().get_def_span(proc_def_id), + ) + })?; + let body = state.into_expr().ok_or_else(|| { + SpannedEncodingError::internal( + format!("failed to encode function's body: {:?}", proc_def_id), + encoder.env().get_def_span(proc_def_id), + ) + })?; + debug!( + "Pure function {:?} has been encoded with expr: {}", + proc_def_id, body + ); // FIXME: Traverse the encoded function and check that all used types are // Copy. Doing this before encoding causes too many false positives. + Ok(body) } pub(super) fn encode_function_call_info<'p, 'v: 'p, 'tcx: 'v>( encoder: &'p Encoder<'v, 'tcx>, proc_def_id: DefId, - mir: &'p mir::Body<'tcx>, parent_def_id: DefId, substs: SubstsRef<'tcx>, ) -> SpannedEncodingResult { - // FIXME: Refactor code to avoid creating the interpreter because it is unnecessary. - let interpreter = - ExpressionBackwardInterpreter::new(encoder, mir, proc_def_id, false, parent_def_id, substs); - let encoder = PureEncoder { - encoder, - proc_def_id, - mir, - parent_def_id, - substs, - interpreter, - }; + let encoder = PureEncoder::new(encoder, proc_def_id, parent_def_id, substs); Ok(FunctionCallInfoHigh { name: encoder.encode_function_name(), _parameters: encoder.encode_parameters()?, @@ -131,16 +124,78 @@ pub(super) fn encode_function_call_info<'p, 'v: 'p, 'tcx: 'v>( /// Encoder of pure things such as pure functions and specification assertions. pub(super) struct PureEncoder<'p, 'v: 'p, 'tcx: 'v> { encoder: &'p Encoder<'v, 'tcx>, + /// The function to be encoded. proc_def_id: DefId, - mir: &'p mir::Body<'tcx>, - interpreter: ExpressionBackwardInterpreter<'p, 'v, 'tcx>, + /// Where is this being encoded? + // TODO: should pure encoding context also exist here? + // pure_encoding_context: PureEncodingContext, parent_def_id: DefId, + /// Type substitutions applied to the MIR (if any) and the signature. substs: SubstsRef<'tcx>, + /// Span of the function declaration. + span: Span, + /// Signature of the function to be encoded. + sig: ty::FnSig<'tcx>, + /// Spans of MIR locals, when encoding a local pure function. + local_spans: Option>, } impl<'p, 'v: 'p, 'tcx: 'v> PureEncoder<'p, 'v, 'tcx> { - fn encode_pure_expression(&self) -> SpannedEncodingResult { - let state = run_backward_interpretation(self.mir, &self.interpreter)?.ok_or_else(|| { + fn new( + encoder: &'p Encoder<'v, 'tcx>, + proc_def_id: DefId, + // pure_encoding_context: PureEncodingContext, + parent_def_id: DefId, + substs: SubstsRef<'tcx>, + ) -> Self { + trace!("PureEncoder constructor: {:?}", proc_def_id); + + // should hold for extern specs as well (otherwise there would have + // been an error reported earlier) + assert_eq!( + substs.len(), + encoder.env().identity_substs(proc_def_id).len() + ); + + let span = encoder.get_spec_span(proc_def_id); + + // TODO: move this to a signatures module + use crate::rustc_middle::ty::subst::Subst; + let sig = encoder + .env() + .tcx() + .fn_sig(proc_def_id) + .subst(encoder.env().tcx(), substs) + .skip_binder(); + + Self { + encoder, + proc_def_id, + // pure_encoding_context, + parent_def_id, + substs, + span, + sig, + local_spans: None, + } + } + + fn encode_function_decl(&self) -> SpannedEncodingResult { + trace!("[enter] encode_function_decl({:?})", self.proc_def_id); + let mir = self + .encoder + .env() + .local_mir(self.proc_def_id.expect_local(), self.substs); + let interpreter = ExpressionBackwardInterpreter::new( + self.encoder, + &mir, + self.proc_def_id, + false, + self.parent_def_id, + self.substs, + ); + + let state = run_backward_interpretation(&mir, &interpreter)?.ok_or_else(|| { SpannedEncodingError::incorrect( format!("procedure {:?} contains a loop", self.proc_def_id), self.encoder.env().get_def_span(self.proc_def_id), @@ -152,19 +207,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureEncoder<'p, 'v, 'tcx> { self.encoder.env().get_def_span(self.proc_def_id), ) })?; - debug!( - "Pure function {:?} has been encoded with expr: {}", - self.proc_def_id, body - ); - // FIXME: Apply type substitutions. - Ok(body) - } - - fn encode_function_decl(&self) -> SpannedEncodingResult { - trace!("[enter] encode_function({:?})", self.proc_def_id); - let body = Some(self.encode_pure_expression()?); - let function = self.encode_function_decl_given_body(body); - trace!("[exit] encode_function({:?})", self.proc_def_id); + let function = self.encode_function_decl_given_body(Some(body)); + trace!("[exit] encode_function_decl({:?})", self.proc_def_id); function } @@ -187,7 +231,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureEncoder<'p, 'v, 'tcx> { let contract = self .encoder .get_mir_procedure_contract_for_def(self.proc_def_id, self.substs) - .with_span(self.mir.span)?; + .with_span(self.span)?; let func_precondition = self.encode_precondition_expr(¶meters, &contract)?; let func_postcondition = self.encode_postcondition_expr(¶meters, &contract)?; let type_arguments = self.encode_type_arguments()?; @@ -211,13 +255,13 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureEncoder<'p, 'v, 'tcx> { fn encode_type_arguments(&self) -> SpannedEncodingResult> { self.encoder .encode_generic_arguments_high(self.proc_def_id, self.substs) - .with_span(self.mir.span) + .with_span(self.span) } fn encode_parameters(&self) -> SpannedEncodingResult> { let mut parameters = Vec::new(); - for local in self.mir.args_iter() { - let ty = self.encoder.get_local_type(self.mir, local)?; + for local in self.args_iter() { + let ty = self.get_local_ty(local); let param_env = self.encoder.env().tcx().param_env(self.proc_def_id); if !self .encoder @@ -226,7 +270,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureEncoder<'p, 'v, 'tcx> { { return Err(SpannedEncodingError::incorrect( "all types used in pure functions must be Copy", - self.encoder.get_local_span(self.mir, local)?, + self.get_local_span(local), )); } let variable_decl = self.encode_mir_local(local)?; @@ -247,8 +291,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureEncoder<'p, 'v, 'tcx> { } fn encode_return_type(&self) -> SpannedEncodingResult { - let ty = self.mir.return_ty(); - let span = self.get_local_span(mir::RETURN_PLACE); + let ty = self.sig.output(); + + let span = self.get_return_span(); let param_env = self.encoder.env().tcx().param_env(self.proc_def_id); if !self .encoder @@ -260,18 +305,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureEncoder<'p, 'v, 'tcx> { span, )); } - self.encoder.encode_type_high(ty) - } - fn encode_mir_local(&self, local: mir::Local) -> SpannedEncodingResult { - let param_env = self.encoder.env().tcx().param_env(self.proc_def_id); - if !self.encoder.is_local_copy(self.mir, local, param_env)? { - return Err(SpannedEncodingError::incorrect( - "pure function parameters must be Copy", - self.encoder.get_local_span(self.mir, local)?, - )); - } - self.encoder.encode_local_high(self.mir, local) + self.encoder.encode_type_high(ty) } fn encode_precondition_expr( @@ -330,7 +365,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureEncoder<'p, 'v, 'tcx> { // TODO: use a better span let postcondition_pos = self.encoder.error_manager().register_error( - self.mir.span, + self.span, ErrorCtxt::PureFunctionDefinition, self.parent_def_id, ); @@ -345,11 +380,48 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureEncoder<'p, 'v, 'tcx> { Ok(post) } + fn args_iter(&self) -> impl Iterator { + (0..self.sig.inputs().len()).map(|idx| mir::Local::from_usize(1 + idx)) + } + + /// Encodes a VIR local with the original MIR type. + fn encode_mir_local(&self, local: mir::Local) -> SpannedEncodingResult { + let ty = self.get_local_ty(local); + let param_env = self.encoder.env().tcx().param_env(self.proc_def_id); + if !self + .encoder + .env() + .type_is_allowed_in_pure_functions(ty, param_env) + { + return Err(SpannedEncodingError::incorrect( + "pure function parameters must be Copy", + self.get_local_span(local), + )); + } + let var_name = format!("{:?}", local); + let var_type = self.encoder.encode_type_high(ty)?; + Ok(vir_high::VariableDecl { + name: var_name, + ty: var_type, + }) + } + + fn get_local_ty(&self, local: mir::Local) -> ty::Ty<'tcx> { + if local.as_usize() == 0 { + self.sig.output() + } else { + self.sig.inputs()[local.as_usize() - 1] + } + } + fn get_local_span(&self, local: mir::Local) -> Span { - self.mir_encoder().get_local_span(local) + self.local_spans + .as_ref() + .map(|spans| spans[local.index()]) + .unwrap_or(self.span) } - fn mir_encoder(&self) -> &MirEncoder<'p, 'v, 'tcx> { - self.interpreter.mir_encoder() + fn get_return_span(&self) -> Span { + self.get_local_span(mir::RETURN_PLACE) } } diff --git a/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs b/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs index 118f6b9a2ed..7de82628262 100644 --- a/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs +++ b/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs @@ -12,6 +12,7 @@ use crate::encoder::{ types::MirTypeEncoderInterface, }, mir_encoder::{MirEncoder, PlaceEncoder}, + snapshot::interface::SnapshotEncoderInterface, Encoder, }; use prusti_common::config; @@ -123,12 +124,12 @@ pub(super) fn encode_quantifier<'tcx>( // ) let cl_type_body = substs.type_at(1); - let (body_def_id, body_substs, _, args, _) = extract_closure_from_ty(tcx, cl_type_body); + let (body_def_id, body_substs, body_span, args, _) = extract_closure_from_ty(tcx, cl_type_body); let mut encoded_qvars = vec![]; let mut bounds = vec![]; for (arg_idx, arg_ty) in args.into_iter().enumerate() { - let qvar_ty = encoder.encode_type(arg_ty).unwrap(); + let qvar_ty = encoder.encode_snapshot_type(arg_ty).with_span(body_span)?; let qvar_name = format!( "_{}_quant_{}", arg_idx, diff --git a/prusti-viper/src/encoder/mir/pure/specifications/interface.rs b/prusti-viper/src/encoder/mir/pure/specifications/interface.rs index fe054868878..c7a05e693dc 100644 --- a/prusti-viper/src/encoder/mir/pure/specifications/interface.rs +++ b/prusti-viper/src/encoder/mir/pure/specifications/interface.rs @@ -241,7 +241,6 @@ impl<'v, 'tcx: 'v> SpecificationEncoderInterface<'tcx> for crate::encoder::Encod parent_def_id, PureEncodingContext::Code, parent_def_id, - substs, ); let invariant = run_backward_interpretation_point_to_point( mir, diff --git a/prusti-viper/src/encoder/mir/pure/specifications/utils.rs b/prusti-viper/src/encoder/mir/pure/specifications/utils.rs index 4788b0cd7a9..c5d559f5152 100644 --- a/prusti-viper/src/encoder/mir/pure/specifications/utils.rs +++ b/prusti-viper/src/encoder/mir/pure/specifications/utils.rs @@ -21,7 +21,7 @@ pub(super) fn extract_closure_from_ty<'tcx>( match ty.kind() { ty::TyKind::Closure(def_id, substs) => { let cl_substs = substs.as_closure(); - let sig = cl_substs.sig().no_bound_vars().unwrap(); + let sig = cl_substs.sig().skip_binder(); ( *def_id, substs, diff --git a/prusti-viper/src/encoder/mir/specifications/interface.rs b/prusti-viper/src/encoder/mir/specifications/interface.rs index d6497c2a5a1..7a0edb40393 100644 --- a/prusti-viper/src/encoder/mir/specifications/interface.rs +++ b/prusti-viper/src/encoder/mir/specifications/interface.rs @@ -5,6 +5,7 @@ use prusti_interface::{ utils::has_spec_only_attr, }; use rustc_hir::def_id::{DefId, LocalDefId}; +use rustc_span::Span; use std::cell::RefCell; pub(crate) struct SpecificationsState { @@ -26,8 +27,6 @@ pub(crate) trait SpecificationsInterface { fn get_predicate_body(&self, def_id: DefId) -> Option; - fn has_extern_spec(&self, def_id: DefId) -> bool; - /// Get the loop invariant attached to a function with a /// `prusti::loop_body_invariant_spec` attribute. fn get_loop_specs(&self, def_id: DefId) -> Option; @@ -35,12 +34,12 @@ pub(crate) trait SpecificationsInterface { /// Get the specifications attached to the `def_id` function. fn get_procedure_specs(&self, def_id: DefId) -> Option; - /// Get a local wrapper `DefId` for functions that have external specs. - /// Return the original `DefId` for everything else. - fn get_wrapper_def_id(&self, def_id: DefId) -> DefId; - - /// Is the closure specified with the `def_id` is spec only? + /// Is the closure specified with the `def_id` spec only? fn is_spec_closure(&self, def_id: DefId) -> bool; + + /// Get the span of the declared specification, if any, or else the span of + /// the method declaration. + fn get_spec_span(&self, def_id: DefId) -> Span; } impl<'v, 'tcx: 'v> SpecificationsInterface for super::super::super::Encoder<'v, 'tcx> { @@ -80,22 +79,6 @@ impl<'v, 'tcx: 'v> SpecificationsInterface for super::super::super::Encoder<'v, result.cloned() } - fn has_extern_spec(&self, def_id: DefId) -> bool { - // FIXME: eventually, procedure specs (the entries in def_spec) should - // have an `is_extern_spec` field. For now, due to the way we handle - // MIR, extern specs create a wrapper function with a different DefId, - // so since we already have this remapping, it is enough to check if - // there is a wrapper present for the given external DefId. - let result = self - .specifications_state - .specs - .borrow() - .get_extern_spec_map() - .contains_key(&def_id); - trace!("has_extern_spec {:?} = {}", def_id, result); - result - } - fn get_loop_specs(&self, def_id: DefId) -> Option { self.specifications_state .specs @@ -110,18 +93,16 @@ impl<'v, 'tcx: 'v> SpecificationsInterface for super::super::super::Encoder<'v, Some(spec.clone()) } - fn get_wrapper_def_id(&self, def_id: DefId) -> DefId { - self.specifications_state - .specs - .borrow() - .get_extern_spec_map() - .get(&def_id) - .map(|local_id| local_id.to_def_id()) - .unwrap_or(def_id) - } - - /// Is the closure specified with the `def_id` is spec only? fn is_spec_closure(&self, def_id: DefId) -> bool { has_spec_only_attr(self.env().tcx().get_attrs(def_id)) } + + fn get_spec_span(&self, def_id: DefId) -> Span { + self.specifications_state + .specs + .borrow_mut() + .get_and_refine_proc_spec(self.env(), def_id) + .and_then(|spec| spec.span) + .unwrap_or_else(|| self.env().get_def_span(def_id)) + } } diff --git a/prusti-viper/src/encoder/mir/specifications/specs.rs b/prusti-viper/src/encoder/mir/specifications/specs.rs index 341f18d2615..2d868ca9621 100644 --- a/prusti-viper/src/encoder/mir/specifications/specs.rs +++ b/prusti-viper/src/encoder/mir/specifications/specs.rs @@ -9,8 +9,7 @@ use prusti_interface::{ PrustiError, }; use rustc_hash::FxHashMap; -use rustc_hir::def_id::{DefId, LocalDefId}; -use std::collections::HashMap; +use rustc_hir::def_id::DefId; /// Provides access to specifications, handling refinement if needed pub(super) struct Specifications { @@ -26,17 +25,9 @@ impl Specifications { } } - pub(super) fn get_user_typed_specs(&self) -> &DefSpecificationMap { - &self.user_typed_specs - } - - pub(super) fn get_extern_spec_map(&self) -> &HashMap { - &self.get_user_typed_specs().extern_specs - } - pub(super) fn get_loop_spec(&self, def_id: DefId) -> Option<&LoopSpecification> { trace!("Get loop specs of {:?}", def_id); - let spec = self.get_user_typed_specs().get(&def_id)?; + let spec = self.user_typed_specs.get(&def_id)?; spec.as_loop() } diff --git a/vir-gen/src/lib.rs b/vir-gen/src/lib.rs index 2fe6eb3e781..c8bc763503b 100644 --- a/vir-gen/src/lib.rs +++ b/vir-gen/src/lib.rs @@ -60,7 +60,7 @@ pub fn define_vir(input: TokenStream, source_file: &std::path::Path) -> TokenStr } if !error_tokens.is_empty() { - unreachable!(); + unreachable!("{:?}", error_tokens); } quote! { #declarations #error_tokens }