From d63dd2088d83140076b11f35d421946daa55750d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aurel=20B=C3=ADl=C3=BD?= Date: Thu, 9 Feb 2023 16:56:35 +0100 Subject: [PATCH] Update dependencies (rustc nightly-2023-02-01, viper v-2023-01-31-0912) --- analysis/src/bin/analysis-driver.rs | 2 +- analysis/src/bin/gen-accessibility-driver.rs | 2 +- .../collect_closure_defs_visitor.rs | 10 ++-- prusti-interface/src/environment/loops.rs | 4 +- prusti-interface/src/environment/name.rs | 2 +- prusti-interface/src/environment/procedure.rs | 16 +++--- prusti-interface/src/environment/query.rs | 13 +++-- prusti-interface/src/specs/checker/common.rs | 8 +-- .../src/specs/checker/predicate_checks.rs | 14 +++-- prusti-interface/src/specs/external.rs | 8 +-- prusti-interface/src/specs/mod.rs | 9 ++-- prusti-rustc-interface/src/lib.rs | 1 + .../parse/ui/predicates-visibility.stdout | 5 +- prusti-tests/tests/parse/ui/predicates.stdout | 20 +++---- prusti-tests/tests/parse/ui/unbalanced.stderr | 4 +- prusti-tests/tests/verify/ui/predicate.stdout | 25 ++++----- .../counterexample_translation_refactored.rs | 8 ++- .../encoder/mir/procedures/encoder/loops.rs | 4 +- .../src/encoder/mir/procedures/encoder/mod.rs | 11 ++-- .../encoder/specification_blocks.rs | 2 +- .../mir/pure/specifications/interface.rs | 4 +- .../src/encoder/mir/types/const_parameters.rs | 3 +- prusti-viper/src/encoder/mir/types/encoder.rs | 1 + .../src/encoder/mir/types/lifetimes.rs | 3 +- prusti-viper/src/encoder/procedure_encoder.rs | 8 +-- prusti-viper/src/utils/mod.rs | 4 +- prusti/src/callbacks.rs | 54 ++++++++++++------- rust-toolchain | 2 +- test-crates/crates.csv | 8 +-- 29 files changed, 142 insertions(+), 113 deletions(-) diff --git a/analysis/src/bin/analysis-driver.rs b/analysis/src/bin/analysis-driver.rs index 9915886b8f2..58e17900f23 100644 --- a/analysis/src/bin/analysis-driver.rs +++ b/analysis/src/bin/analysis-driver.rs @@ -161,7 +161,7 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls { println!( "Analyzing file {} using {}...", - compiler.input().source_name().prefer_local(), + compiler.session().io.input.source_name().prefer_local(), abstract_domain ); diff --git a/analysis/src/bin/gen-accessibility-driver.rs b/analysis/src/bin/gen-accessibility-driver.rs index 3b30241dfc3..66c9ddc548b 100644 --- a/analysis/src/bin/gen-accessibility-driver.rs +++ b/analysis/src/bin/gen-accessibility-driver.rs @@ -155,7 +155,7 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls { // Skip functions that are in an external file. let source_file = session.source_map().lookup_source_file(mir_span.data().lo); if let FileName::Real(filename) = &source_file.name { - if session.local_crate_source_file + if session.local_crate_source_file() != filename.local_path().map(PathBuf::from) { return None; diff --git a/prusti-interface/src/environment/collect_closure_defs_visitor.rs b/prusti-interface/src/environment/collect_closure_defs_visitor.rs index d4e6251f01b..0bb0dd071b1 100644 --- a/prusti-interface/src/environment/collect_closure_defs_visitor.rs +++ b/prusti-interface/src/environment/collect_closure_defs_visitor.rs @@ -39,9 +39,13 @@ impl<'env, 'tcx> Visitor<'tcx> for CollectClosureDefsVisitor<'env, 'tcx> { } fn visit_expr(&mut self, expr: &'tcx hir::Expr<'tcx>) { - if let hir::ExprKind::Closure { .. } = expr.kind { - if !has_spec_only_attr(self.env.query.get_local_attributes(expr.hir_id)) { - let def_id = self.map.local_def_id(expr.hir_id).to_def_id(); + if let hir::ExprKind::Closure(hir::Closure { + def_id: local_def_id, + .. + }) = expr.kind + { + let def_id = local_def_id.to_def_id(); + if !has_spec_only_attr(self.env.query.get_attributes(def_id)) { let item_def_path = self.env.name.get_item_def_path(def_id); trace!("Add {} to result", item_def_path); self.result.push(def_id); diff --git a/prusti-interface/src/environment/loops.rs b/prusti-interface/src/environment/loops.rs index 57cf34b38ba..f7d9277e501 100644 --- a/prusti-interface/src/environment/loops.rs +++ b/prusti-interface/src/environment/loops.rs @@ -259,7 +259,7 @@ impl ProcedureLoops { let mut back_edges: FxHashSet<(_, _)> = FxHashSet::default(); for bb in mir.basic_blocks.indices() { for successor in real_edges.successors(bb) { - if dominators.is_dominated_by(bb, *successor) { + if dominators.dominates(*successor, bb) { back_edges.insert((bb, *successor)); debug!("Loop head: {:?}", successor); } @@ -475,7 +475,7 @@ impl ProcedureLoops { /// Check if ``block`` is inside a given loop. pub fn is_block_in_loop(&self, loop_head: BasicBlockIndex, block: BasicBlockIndex) -> bool { - self.dominators.is_dominated_by(block, loop_head) + self.dominators.dominates(loop_head, block) } /// Compute what paths that are accessed inside the loop. diff --git a/prusti-interface/src/environment/name.rs b/prusti-interface/src/environment/name.rs index 4b3a44b2137..5caeb09f297 100644 --- a/prusti-interface/src/environment/name.rs +++ b/prusti-interface/src/environment/name.rs @@ -16,7 +16,7 @@ impl<'tcx> EnvName<'tcx> { /// Returns the path of the source that is being compiled pub fn source_path(self) -> PathBuf { - self.tcx.sess.local_crate_source_file.clone().unwrap() + self.tcx.sess.local_crate_source_file().unwrap() } /// Returns the file name of the source that is being compiled diff --git a/prusti-interface/src/environment/procedure.rs b/prusti-interface/src/environment/procedure.rs index 4f87ed1a386..6f68fc23759 100644 --- a/prusti-interface/src/environment/procedure.rs +++ b/prusti-interface/src/environment/procedure.rs @@ -236,7 +236,7 @@ pub fn is_marked_specification_block(env_query: EnvQuery, bb_data: &BasicBlockDa Rvalue::Aggregate(box AggregateKind::Closure(def_id, _), _), )) = &stmt.kind { - if is_spec_closure(env_query, def_id.to_def_id()) { + if is_spec_closure(env_query, *def_id) { return true; } } @@ -257,13 +257,13 @@ pub fn get_loop_invariant<'tcx>( Rvalue::Aggregate(box AggregateKind::Closure(def_id, substs), _), )) = &stmt.kind { - if is_spec_closure(env_query, def_id.to_def_id()) + if is_spec_closure(env_query, *def_id) && crate::utils::has_prusti_attr( - env_query.get_attributes(def_id.to_def_id()), + env_query.get_attributes(def_id), "loop_body_invariant_spec", ) { - return Some((def_id.to_def_id(), substs)); + return Some((*def_id, substs)); } } } @@ -293,8 +293,8 @@ fn is_spec_block_kind(env_query: EnvQuery, bb_data: &BasicBlockData, kind: &str) Rvalue::Aggregate(box AggregateKind::Closure(def_id, _), _), )) = &stmt.kind { - if is_spec_closure(env_query, def_id.to_def_id()) - && crate::utils::has_prusti_attr(env_query.get_attributes(def_id.to_def_id()), kind) + if is_spec_closure(env_query, *def_id) + && crate::utils::has_prusti_attr(env_query.get_attributes(def_id), kind) { return true; } @@ -338,7 +338,7 @@ fn blocks_dominated_by(mir: &Body, dominator: BasicBlock) -> FxHashSet EnvQuery<'tcx> { /// Returns true iff `def_id` is an unsafe function. pub fn is_unsafe_function(self, def_id: impl IntoParam) -> bool { - self.tcx.fn_sig(def_id.into_param()).unsafety() + self.tcx + .fn_sig(def_id.into_param()) + .subst_identity() + .unsafety() == prusti_rustc_interface::hir::Unsafety::Unsafe } @@ -152,11 +155,11 @@ impl<'tcx> EnvQuery<'tcx> { ) -> ty::PolyFnSig<'tcx> { let def_id = def_id.into_param(); let sig = if self.tcx.is_closure(def_id) { - substs.as_closure().sig() + ty::EarlyBinder(substs.as_closure().sig()) } else { self.tcx.fn_sig(def_id) }; - ty::EarlyBinder(sig).subst(self.tcx, substs) + sig.subst(self.tcx, substs) } /// Computes the signature of the function with subst applied and associated types resolved. @@ -531,8 +534,8 @@ mod sealed { } impl<'tcx> IntoParamTcx<'tcx, LocalDefId> for HirId { #[inline(always)] - fn into_param(self, tcx: TyCtxt<'tcx>) -> LocalDefId { - tcx.hir().local_def_id(self) + fn into_param(self, _tcx: TyCtxt<'tcx>) -> LocalDefId { + self.owner.def_id } } impl<'tcx> IntoParamTcx<'tcx, ParamEnv<'tcx>> for DefId { diff --git a/prusti-interface/src/specs/checker/common.rs b/prusti-interface/src/specs/checker/common.rs index 891da9fb4ae..6d920e7f147 100644 --- a/prusti-interface/src/specs/checker/common.rs +++ b/prusti-interface/src/specs/checker/common.rs @@ -2,6 +2,7 @@ use crate::{environment::Environment, utils::has_spec_only_attr, PrustiError}; use prusti_rustc_interface::{ hir::{ self as hir, + def_id::LocalDefId, intravisit::{self, Visitor}, }, middle::{hir::map::Map, ty::TyCtxt}, @@ -77,14 +78,15 @@ impl<'tcx, T: NonSpecExprVisitor<'tcx>> Visitor<'tcx> for NonSpecExprVisitorWrap fd: &'tcx hir::FnDecl<'tcx>, b: hir::BodyId, _s: Span, - id: hir::HirId, + local_id: LocalDefId, ) { // Stop checking inside `prusti::spec_only` functions - let attrs = self.wrapped.tcx().hir().attrs(id); + let tcx = self.wrapped.tcx(); + let attrs = tcx.hir().attrs(tcx.local_def_id_to_hir_id(local_id)); if has_spec_only_attr(attrs) { return; } - intravisit::walk_fn(self, fk, fd, b, id); + intravisit::walk_fn(self, fk, fd, b, local_id); } } diff --git a/prusti-interface/src/specs/checker/predicate_checks.rs b/prusti-interface/src/specs/checker/predicate_checks.rs index e97bc0a04cd..6ddaad104b0 100644 --- a/prusti-interface/src/specs/checker/predicate_checks.rs +++ b/prusti-interface/src/specs/checker/predicate_checks.rs @@ -8,7 +8,11 @@ use log::debug; use prusti_rustc_interface::{ data_structures::fx::{FxHashMap, FxHashSet}, errors::MultiSpan, - hir::{self as hir, def_id::DefId, intravisit}, + hir::{ + self as hir, + def_id::{DefId, LocalDefId}, + intravisit, + }, middle::{hir::map::Map, ty::TyCtxt}, span::Span, }; @@ -106,16 +110,16 @@ impl<'tcx> intravisit::Visitor<'tcx> for CollectPredicatesVisitor<'tcx> { fd: &'tcx hir::FnDecl<'tcx>, b: hir::BodyId, s: Span, - id: hir::HirId, + local_id: LocalDefId, ) { // collect this fn's DefId if predicate function - let attrs = self.env_query.get_local_attributes(id); + let attrs = self.env_query.get_local_attributes(local_id); if has_prusti_attr(attrs, "pred_spec_id_ref") { - let def_id = self.env_query.as_local_def_id(id).to_def_id(); + let def_id = local_id.to_def_id(); self.predicates.insert(def_id, s); } - intravisit::walk_fn(self, fk, fd, b, id); + intravisit::walk_fn(self, fk, fd, b, local_id); } fn visit_trait_item(&mut self, ti: &'tcx hir::TraitItem<'tcx>) { diff --git a/prusti-interface/src/specs/external.rs b/prusti-interface/src/specs/external.rs index 6730526c769..dc42ed6aeaf 100644 --- a/prusti-interface/src/specs/external.rs +++ b/prusti-interface/src/specs/external.rs @@ -1,7 +1,7 @@ use prusti_rustc_interface::{ errors::MultiSpan, hir::{ - def_id::DefId, + def_id::{DefId, LocalDefId}, intravisit::{self, Visitor}, }, middle::hir::map::Map, @@ -130,15 +130,15 @@ impl<'tcx> ExternSpecResolver<'tcx> { fn_decl: &'tcx prusti_rustc_interface::hir::FnDecl, body_id: prusti_rustc_interface::hir::BodyId, span: Span, - id: prusti_rustc_interface::hir::hir_id::HirId, + local_id: LocalDefId, extern_spec_kind: ExternSpecKind, ) { let mut visitor = ExternSpecVisitor { env_query: self.env_query, spec_found: None, }; - visitor.visit_fn(fn_kind, fn_decl, body_id, span, id); - let current_def_id = self.env_query.as_local_def_id(id).to_def_id(); + visitor.visit_fn(fn_kind, fn_decl, body_id, span, local_id); + let current_def_id = local_id.to_def_id(); if let Some((target_def_id, substs, span)) = visitor.spec_found { let extern_spec_decl = ExternSpecDeclaration::from_method_call(target_def_id, substs, self.env_query); diff --git a/prusti-interface/src/specs/mod.rs b/prusti-interface/src/specs/mod.rs index a5407ce84be..0950a1e73d5 100644 --- a/prusti-interface/src/specs/mod.rs +++ b/prusti-interface/src/specs/mod.rs @@ -411,13 +411,12 @@ impl<'a, 'tcx> intravisit::Visitor<'tcx> for SpecCollector<'a, 'tcx> { fn_decl: &'tcx prusti_rustc_interface::hir::FnDecl, body_id: prusti_rustc_interface::hir::BodyId, span: Span, - id: prusti_rustc_interface::hir::hir_id::HirId, + local_id: LocalDefId, ) { - intravisit::walk_fn(self, fn_kind, fn_decl, body_id, id); + intravisit::walk_fn(self, fn_kind, fn_decl, body_id, local_id); - let local_id = self.env.query.as_local_def_id(id); let def_id = local_id.to_def_id(); - let attrs = self.env.query.get_local_attributes(id); + let attrs = self.env.query.get_local_attributes(local_id); // Collect spec functions if let Some(raw_spec_id) = read_prusti_attr("spec_id", attrs) { @@ -497,7 +496,7 @@ impl<'a, 'tcx> intravisit::Visitor<'tcx> for SpecCollector<'a, 'tcx> { let attr = read_prusti_attr("extern_spec", attrs).unwrap_or_default(); let kind = prusti_specs::ExternSpecKind::try_from(attr).unwrap(); self.extern_resolver - .add_extern_fn(fn_kind, fn_decl, body_id, span, id, kind); + .add_extern_fn(fn_kind, fn_decl, body_id, span, local_id, kind); } // Collect procedure specifications diff --git a/prusti-rustc-interface/src/lib.rs b/prusti-rustc-interface/src/lib.rs index e5691bd15c2..626308e06f3 100644 --- a/prusti-rustc-interface/src/lib.rs +++ b/prusti-rustc-interface/src/lib.rs @@ -8,6 +8,7 @@ extern crate rustc_smir; pub extern crate polonius_engine as polonius_engine; pub extern crate rustc_ast as ast; +pub extern crate rustc_ast_pretty as ast_pretty; pub extern crate rustc_attr as attr; pub extern crate rustc_data_structures as data_structures; pub extern crate rustc_driver as driver; diff --git a/prusti-tests/tests/parse/ui/predicates-visibility.stdout b/prusti-tests/tests/parse/ui/predicates-visibility.stdout index a99c1e55f91..3ebd48713fd 100644 --- a/prusti-tests/tests/parse/ui/predicates-visibility.stdout +++ b/prusti-tests/tests/parse/ui/predicates-visibility.stdout @@ -35,9 +35,8 @@ mod foo { #[prusti::pred_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] pub fn pred1(a: bool) -> bool { - ::core::panicking::panic_fmt(::core::fmt::Arguments::new_v1(&["not implemented: "], - &[::core::fmt::ArgumentV1::new_display(&::core::fmt::Arguments::new_v1(&["predicate"], - &[]))])) + ::core::panicking::panic_fmt(format_args!("not implemented: {0}", + format_args!("predicate"))) } } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, diff --git a/prusti-tests/tests/parse/ui/predicates.stdout b/prusti-tests/tests/parse/ui/predicates.stdout index ed19a3ca2be..bd47d01ae3c 100644 --- a/prusti-tests/tests/parse/ui/predicates.stdout +++ b/prusti-tests/tests/parse/ui/predicates.stdout @@ -36,9 +36,8 @@ fn prusti_pred_item_pred1_$(NUM_UUID)(a: bool) -> bool { #[prusti::pred_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] fn pred1(a: bool) -> bool { - ::core::panicking::panic_fmt(::core::fmt::Arguments::new_v1(&["not implemented: "], - &[::core::fmt::ArgumentV1::new_display(&::core::fmt::Arguments::new_v1(&["predicate"], - &[]))])) + ::core::panicking::panic_fmt(format_args!("not implemented: {0}", + format_args!("predicate"))) } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -64,9 +63,8 @@ fn prusti_pred_item_pred2_$(NUM_UUID)(a: bool) -> bool { #[prusti::pred_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] fn pred2(a: bool) -> bool { - ::core::panicking::panic_fmt(::core::fmt::Arguments::new_v1(&["not implemented: "], - &[::core::fmt::ArgumentV1::new_display(&::core::fmt::Arguments::new_v1(&["predicate"], - &[]))])) + ::core::panicking::panic_fmt(format_args!("not implemented: {0}", + format_args!("predicate"))) } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -94,9 +92,8 @@ fn prusti_pred_item_forall_implication_$(NUM_UUID)() #[prusti::pred_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] fn forall_implication() -> bool { - ::core::panicking::panic_fmt(::core::fmt::Arguments::new_v1(&["not implemented: "], - &[::core::fmt::ArgumentV1::new_display(&::core::fmt::Arguments::new_v1(&["predicate"], - &[]))])) + ::core::panicking::panic_fmt(format_args!("not implemented: {0}", + format_args!("predicate"))) } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -114,9 +111,8 @@ fn prusti_pred_item_exists_implication_$(NUM_UUID)() #[prusti::pred_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] fn exists_implication() -> bool { - ::core::panicking::panic_fmt(::core::fmt::Arguments::new_v1(&["not implemented: "], - &[::core::fmt::ArgumentV1::new_display(&::core::fmt::Arguments::new_v1(&["predicate"], - &[]))])) + ::core::panicking::panic_fmt(format_args!("not implemented: {0}", + format_args!("predicate"))) } fn main() {} ProcedureSpecification { source: DefId(0:7 ~ predicates[$(CRATE_ID)]::pred1), kind: Inherent(Predicate(Some(DefId(0:5 ~ predicates[$(CRATE_ID)]::prusti_pred_item_pred1_$(NUM_UUID))))), pres: Empty, posts: Empty, pledges: Empty, trusted: Inherent(false), terminates: Inherent(None), purity: Inherent(None) } diff --git a/prusti-tests/tests/parse/ui/unbalanced.stderr b/prusti-tests/tests/parse/ui/unbalanced.stderr index 02463ba7470..69e88a608a5 100644 --- a/prusti-tests/tests/parse/ui/unbalanced.stderr +++ b/prusti-tests/tests/parse/ui/unbalanced.stderr @@ -2,7 +2,9 @@ error: unexpected closing delimiter: `]` --> $DIR/unbalanced.rs:3:18 | 3 | #[requires(true))] - | ^ unexpected closing delimiter + | -^ unexpected closing delimiter + | | + | missing open `(` for this delimiter error: mismatched closing delimiter: `)` --> $DIR/unbalanced.rs:3:2 diff --git a/prusti-tests/tests/verify/ui/predicate.stdout b/prusti-tests/tests/verify/ui/predicate.stdout index 62ff9e9254c..36ab9225986 100644 --- a/prusti-tests/tests/verify/ui/predicate.stdout +++ b/prusti-tests/tests/verify/ui/predicate.stdout @@ -44,9 +44,8 @@ fn prusti_pred_item_true_p1_$(NUM_UUID)() -> bool { #[prusti::pred_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] fn true_p1() -> bool { - ::core::panicking::panic_fmt(::core::fmt::Arguments::new_v1(&["not implemented: "], - &[::core::fmt::ArgumentV1::new_display(&::core::fmt::Arguments::new_v1(&["predicate"], - &[]))])) + ::core::panicking::panic_fmt(format_args!("not implemented: {0}", + format_args!("predicate"))) } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -62,9 +61,8 @@ fn prusti_pred_item_true_p2_$(NUM_UUID)() -> bool { #[prusti::pred_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] fn true_p2() -> bool { - ::core::panicking::panic_fmt(::core::fmt::Arguments::new_v1(&["not implemented: "], - &[::core::fmt::ArgumentV1::new_display(&::core::fmt::Arguments::new_v1(&["predicate"], - &[]))])) + ::core::panicking::panic_fmt(format_args!("not implemented: {0}", + format_args!("predicate"))) } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -82,9 +80,8 @@ fn prusti_pred_item_forall_identity_$(NUM_UUID)() #[prusti::pred_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] fn forall_identity() -> bool { - ::core::panicking::panic_fmt(::core::fmt::Arguments::new_v1(&["not implemented: "], - &[::core::fmt::ArgumentV1::new_display(&::core::fmt::Arguments::new_v1(&["predicate"], - &[]))])) + ::core::panicking::panic_fmt(format_args!("not implemented: {0}", + format_args!("predicate"))) } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -103,9 +100,8 @@ fn prusti_pred_item_exists_identity_$(NUM_UUID)() #[prusti::pred_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] fn exists_identity() -> bool { - ::core::panicking::panic_fmt(::core::fmt::Arguments::new_v1(&["not implemented: "], - &[::core::fmt::ArgumentV1::new_display(&::core::fmt::Arguments::new_v1(&["predicate"], - &[]))])) + ::core::panicking::panic_fmt(format_args!("not implemented: {0}", + format_args!("predicate"))) } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] @@ -158,9 +154,8 @@ fn prusti_pred_item_false_p_$(NUM_UUID)() -> bool { #[prusti::pred_spec_id_ref = "$(NUM_UUID)"] #[prusti::specs_version = $(SPECS_VERSION)] fn false_p() -> bool { - ::core::panicking::panic_fmt(::core::fmt::Arguments::new_v1(&["not implemented: "], - &[::core::fmt::ArgumentV1::new_display(&::core::fmt::Arguments::new_v1(&["predicate"], - &[]))])) + ::core::panicking::panic_fmt(format_args!("not implemented: {0}", + format_args!("predicate"))) } #[allow(unused_must_use, unused_parens, unused_variables, dead_code, non_snake_case)] diff --git a/prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs b/prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs index da6484657e4..45fabf01c14 100644 --- a/prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs +++ b/prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs @@ -193,7 +193,13 @@ impl<'ce, 'tcx, 'v> CounterexampleTranslator<'ce, 'tcx, 'v> { let typ = self .encoder .get_proc_def_id(pure_fn.name.trim_start_matches("caller_for$").to_string()) - .map(|fn_proc_id| self.tcx.fn_sig(fn_proc_id).skip_binder().output()); + .map(|fn_proc_id| { + self.tcx + .fn_sig(fn_proc_id) + .subst_identity() + .skip_binder() + .output() + }); let sil_arguments = pure_fn .args .iter() diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/loops.rs b/prusti-viper/src/encoder/mir/procedures/encoder/loops.rs index 8834f7fb3f6..7af06a785b5 100644 --- a/prusti-viper/src/encoder/mir/procedures/encoder/loops.rs +++ b/prusti-viper/src/encoder/mir/procedures/encoder/loops.rs @@ -35,7 +35,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> super::ProcedureEncoder<'p, 'v, 'tcx> { ), )) = statement.kind { - let specification = self.encoder.get_loop_specs(cl_def_id.to_def_id()).unwrap(); + let specification = self.encoder.get_loop_specs(cl_def_id).unwrap(); let (spec, encoding_vec, err_ctxt) = match specification { LoopSpecification::Invariant(inv) => { (inv, &mut encoded_invariant_specs, ErrorCtxt::LoopInvariant) @@ -65,7 +65,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> super::ProcedureEncoder<'p, 'v, 'tcx> { let dominators = self.mir.basic_blocks.dominators(); predecessors[loop_head] .iter() - .filter(|predecessor| dominators.is_dominated_by(**predecessor, loop_head)) + .filter(|predecessor| dominators.dominates(loop_head, **predecessor)) .map(|back_edge| self.encode_basic_block_label(*back_edge)) .collect() }; diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs b/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs index 6d1bd330662..289010692c4 100644 --- a/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs +++ b/prusti-viper/src/encoder/mir/procedures/encoder/mod.rs @@ -1967,7 +1967,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { mir::Rvalue::Aggregate(box mir::AggregateKind::Closure(cl_def_id, cl_substs), _), )) = stmt.kind { - let assertion = match self.encoder.get_prusti_assertion(cl_def_id.to_def_id()) { + let assertion = match self.encoder.get_prusti_assertion(cl_def_id) { Some(spec) => spec, None => return Ok(false), }; @@ -2016,7 +2016,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { mir::Rvalue::Aggregate(box mir::AggregateKind::Closure(cl_def_id, cl_substs), _), )) = stmt.kind { - let assumption = match self.encoder.get_prusti_assumption(cl_def_id.to_def_id()) { + let assumption = match self.encoder.get_prusti_assumption(cl_def_id) { Some(spec) => spec, None => return Ok(false), }; @@ -2063,11 +2063,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { mir::Rvalue::Aggregate(box mir::AggregateKind::Closure(cl_def_id, _), _), )) = stmt.kind { - let is_begin = self - .encoder - .get_ghost_begin(cl_def_id.to_def_id()) - .is_some(); - let is_end = self.encoder.get_ghost_end(cl_def_id.to_def_id()).is_some(); + let is_begin = self.encoder.get_ghost_begin(cl_def_id).is_some(); + let is_end = self.encoder.get_ghost_end(cl_def_id).is_some(); return Ok(is_begin || is_end); } } diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/specification_blocks.rs b/prusti-viper/src/encoder/mir/procedures/encoder/specification_blocks.rs index eb258f5547a..f3b84ed5886 100644 --- a/prusti-viper/src/encoder/mir/procedures/encoder/specification_blocks.rs +++ b/prusti-viper/src/encoder/mir/procedures/encoder/specification_blocks.rs @@ -49,7 +49,7 @@ impl SpecificationBlocks { let dominators = body.basic_blocks.dominators(); for specification_block in specification_blocks.clone() { for bb in body.basic_blocks.indices() { - if dominators.is_dominated_by(bb, specification_block) { + if dominators.dominates(specification_block, bb) { specification_blocks.insert(bb); } } diff --git a/prusti-viper/src/encoder/mir/pure/specifications/interface.rs b/prusti-viper/src/encoder/mir/pure/specifications/interface.rs index 5d3f3ae69c1..ff05151e2dd 100644 --- a/prusti-viper/src/encoder/mir/pure/specifications/interface.rs +++ b/prusti-viper/src/encoder/mir/pure/specifications/interface.rs @@ -201,7 +201,7 @@ impl<'v, 'tcx: 'v> SpecificationEncoderInterface<'tcx> for crate::encoder::Encod // inline invariant body let encoded_invariant = inline_closure_high( self, - inv_def_id.to_def_id(), + inv_def_id, closure_expression_borrow, vec![], parent_def_id, @@ -341,7 +341,7 @@ impl<'v, 'tcx: 'v> SpecificationEncoderInterface<'tcx> for crate::encoder::Encod // inline invariant body let encoded_invariant = inline_closure( self, - inv_def_id.to_def_id(), + inv_def_id, inv_cl_expr_encoded.try_into_expr().unwrap(), vec![], parent_def_id, diff --git a/prusti-viper/src/encoder/mir/types/const_parameters.rs b/prusti-viper/src/encoder/mir/types/const_parameters.rs index 99b1113570c..5f4dc7b8796 100644 --- a/prusti-viper/src/encoder/mir/types/const_parameters.rs +++ b/prusti-viper/src/encoder/mir/types/const_parameters.rs @@ -75,7 +75,8 @@ pub(super) fn extract_const_parameters_from_type<'tcx>( | ty::TyKind::Placeholder(_) | ty::TyKind::Infer(_) | ty::TyKind::Generator(..) - | ty::TyKind::GeneratorWitness(_) => { + | ty::TyKind::GeneratorWitness(_) + | ty::TyKind::GeneratorWitnessMIR(..) => { return Err(SpannedEncodingError::unsupported( format!( "unsupported type to extract const_parameters: {:?}", diff --git a/prusti-viper/src/encoder/mir/types/encoder.rs b/prusti-viper/src/encoder/mir/types/encoder.rs index 80468ee6aac..9b9d0f3300b 100644 --- a/prusti-viper/src/encoder/mir/types/encoder.rs +++ b/prusti-viper/src/encoder/mir/types/encoder.rs @@ -266,6 +266,7 @@ impl<'p, 'v, 'r: 'v, 'tcx: 'v> TypeEncoder<'p, 'v, 'tcx> { | ty::TyKind::FnPtr(_) | ty::TyKind::Dynamic(..) | ty::TyKind::GeneratorWitness(..) + | ty::TyKind::GeneratorWitnessMIR(..) | ty::TyKind::Never | ty::TyKind::Tuple(_) | ty::TyKind::Alias(ty::AliasKind::Projection, _) diff --git a/prusti-viper/src/encoder/mir/types/lifetimes.rs b/prusti-viper/src/encoder/mir/types/lifetimes.rs index 8c9780b666e..e63f9a7847b 100644 --- a/prusti-viper/src/encoder/mir/types/lifetimes.rs +++ b/prusti-viper/src/encoder/mir/types/lifetimes.rs @@ -86,7 +86,8 @@ pub(super) fn extract_lifetimes_from_type<'tcx>( | ty::TyKind::Placeholder(_) | ty::TyKind::Infer(_) | ty::TyKind::Generator(..) - | ty::TyKind::GeneratorWitness(_) => { + | ty::TyKind::GeneratorWitness(_) + | ty::TyKind::GeneratorWitnessMIR(..) => { return Err(SpannedEncodingError::unsupported( format!("unsupported type to extract lifetimes: {:?}", ty.kind()), type_encoder.get_type_definition_span(ty), diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index cbbd0767652..b4c87b76540 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -237,7 +237,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { mir::Rvalue::Aggregate(box mir::AggregateKind::Closure(cl_def_id, cl_substs), _), )) = stmt.kind { - if self.encoder.get_prusti_assumption(cl_def_id.to_def_id()).is_none() { + if self.encoder.get_prusti_assumption(cl_def_id).is_none() { return Ok(false); } let assume_expr = self.encoder.encode_invariant(self.mir, bb, self.proc_def_id, cl_substs)?; @@ -268,7 +268,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { mir::Rvalue::Aggregate(box mir::AggregateKind::Closure(cl_def_id, cl_substs), _), )) = stmt.kind { - let assertion = match self.encoder.get_prusti_assertion(cl_def_id.to_def_id()) { + let assertion = match self.encoder.get_prusti_assertion(cl_def_id) { Some(spec) => spec, None => return Ok(false), }; @@ -5289,7 +5289,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { _, mir::Rvalue::Aggregate(box mir::AggregateKind::Closure(cl_def_id, cl_substs), _), )) = stmt.kind { - if let Some(spec) = self.encoder.get_loop_specs(cl_def_id.to_def_id()) { + if let Some(spec) = self.encoder.get_loop_specs(cl_def_id) { encoded_specs.push(self.encoder.encode_invariant( self.mir, bbi, @@ -6719,7 +6719,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { mir::AggregateKind::Closure(def_id, substs) => { // TODO: might need to assert history invariants? - assert!(!self.encoder.is_spec_closure(def_id.to_def_id()), "spec closure: {def_id:?}"); + assert!(!self.encoder.is_spec_closure(def_id), "spec closure: {def_id:?}"); let cl_substs = substs.as_closure(); for (field_index, field_ty) in cl_substs.upvar_tys().enumerate() { let operand = &operands[field_index]; diff --git a/prusti-viper/src/utils/mod.rs b/prusti-viper/src/utils/mod.rs index 4d6022e2db8..daa4f02a198 100644 --- a/prusti-viper/src/utils/mod.rs +++ b/prusti-viper/src/utils/mod.rs @@ -28,7 +28,9 @@ pub fn ty_to_string(typ: &ty::TyKind) -> String { &ty::TyKind::FnPtr(_) => "function pointer", &ty::TyKind::Dynamic(..) => "trait object", &ty::TyKind::Closure(_, _) => "closures", - &ty::TyKind::Generator(..) | &ty::TyKind::GeneratorWitness(..) => "generator", + &ty::TyKind::Generator(..) + | &ty::TyKind::GeneratorWitness(..) + | &ty::TyKind::GeneratorWitnessMIR(..) => "generator", &ty::TyKind::Never => "never type", &ty::TyKind::Tuple(_) => "tuple", &ty::TyKind::Alias(ty::AliasKind::Projection, _) => "projection", diff --git a/prusti/src/callbacks.rs b/prusti/src/callbacks.rs index b50d5fbc6c5..69a9c7d7e95 100644 --- a/prusti/src/callbacks.rs +++ b/prusti/src/callbacks.rs @@ -43,16 +43,16 @@ fn mir_borrowck<'tcx>(tcx: TyCtxt<'tcx>, def_id: LocalDefId) -> mir_borrowck<'tc original_mir_borrowck(tcx, def_id) } -fn override_queries(_session: &Session, local: &mut Providers, _external: &mut ExternProviders) { - local.mir_borrowck = mir_borrowck; -} - impl prusti_rustc_interface::driver::Callbacks for PrustiCompilerCalls { fn config(&mut self, config: &mut Config) { // *Don't take MIR bodies with borrowck info if we won't need them* if !config::no_verify() { assert!(config.override_queries.is_none()); - config.override_queries = Some(override_queries); + config.override_queries = Some( + |_session: &Session, providers: &mut Providers, _external: &mut ExternProviders| { + providers.mir_borrowck = mir_borrowck; + }, + ); } } fn after_expansion<'tcx>( @@ -60,29 +60,45 @@ impl prusti_rustc_interface::driver::Callbacks for PrustiCompilerCalls { compiler: &Compiler, queries: &'tcx Queries<'tcx>, ) -> Compilation { - if compiler.session().rust_2015() { + if compiler.session().is_rust_2015() { compiler .session() .struct_warn( "Prusti specifications are supported only from 2018 edition. Please \ - specify the edition with adding a command line argument `--edition=2018` or \ - `--edition=2021`.", + specify the edition with adding a command line argument `--edition=2018` or \ + `--edition=2021`.", ) .emit(); } compiler.session().abort_if_errors(); - let mut expansion_result = queries.expansion().unwrap(); - let (krate, _resolver, _lint_store) = expansion_result.get_mut(); if config::print_desugared_specs() { - prusti_rustc_interface::driver::pretty::print_after_parsing( - compiler.session(), - compiler.input(), - krate, - prusti_rustc_interface::session::config::PpMode::Source( - prusti_rustc_interface::session::config::PpSourceMode::Normal, - ), - None, - ); + // based on the implementation of rustc_driver::pretty::print_after_parsing + queries.global_ctxt().unwrap().enter(|tcx| { + let sess = compiler.session(); + let krate = &tcx.resolver_for_lowering(()).borrow().1; + let src_name = sess.io.input.source_name(); + let src = sess + .source_map() + .get_source_file(&src_name) + .expect("get_source_file") + .src + .as_ref() + .expect("src") + .to_string(); + print!( + "{}", + prusti_rustc_interface::ast_pretty::pprust::print_crate( + sess.source_map(), + krate, + src_name, + src, + &prusti_rustc_interface::ast_pretty::pprust::state::NoAnn, + false, + sess.edition(), + &sess.parse_sess.attr_id_generator, + ) + ); + }); } Compilation::Continue } diff --git a/rust-toolchain b/rust-toolchain index f092488e8e9..1e964bbcc83 100644 --- a/rust-toolchain +++ b/rust-toolchain @@ -1,4 +1,4 @@ [toolchain] -channel = "nightly-2023-01-15" +channel = "nightly-2023-02-09" components = [ "rustc-dev", "llvm-tools-preview", "rust-std", "rustfmt", "clippy" ] profile = "minimal" diff --git a/test-crates/crates.csv b/test-crates/crates.csv index 1387ed89289..de110eb2927 100644 --- a/test-crates/crates.csv +++ b/test-crates/crates.csv @@ -55,7 +55,7 @@ slab,0.4.1,NoCrash cc,1.0.25,Skip term,0.5.1,Skip thread-id,3.3.0,NoErrorsWithUnreachableUnsupportedCode -atty,0.2.11,NoErrorsWithUnreachableUnsupportedCode +atty,0.2.11,Skip openssl,0.10.15,Skip backtrace,0.3.9,Skip tempdir,0.3.7,NoCrash @@ -290,7 +290,7 @@ byte-tools,0.3.0,NoCrash rls-analysis,0.16.1,Skip glutin,0.18.0,Skip rls-vfs,0.6.0,Skip -crypto-hash,0.3.1,NoErrors +crypto-hash,0.3.1,Skip sha2,0.8.0,NoCrash clippy,0.0.302,Skip precomputed-hash,0.1.1,NoErrors @@ -320,7 +320,7 @@ lock_api,0.1.4,Skip rls-rustc,0.5.0,Skip serde_yaml,0.8.6,Skip gleam,0.6.4,Skip -ascii,0.9.1,NoCrash +ascii,0.9.1,Skip zip,0.4.2,Skip rustc-ap-serialize,274.0.0,Skip rustc-ap-syntax_pos,274.0.0,Skip @@ -435,7 +435,7 @@ endian-type,0.1.2,NoErrors rusttype,0.7.2,Skip environment,0.1.1,NoErrors extprim,1.6.0,Skip -libsqlite3-sys,0.10.0,NoErrors +libsqlite3-sys,0.10.0,Skip tiny-keccak,1.4.2,NoCrash cloudabi,0.0.3,NoCrash slog-term,2.4.0,NoCrash