Skip to content

Commit 8a6ee0a

Browse files
committed
Update dependencies (rustc nightly-2022-07-15, viper v-2022-07-01-0736)
1 parent 9d59188 commit 8a6ee0a

File tree

28 files changed

+155
-214
lines changed

28 files changed

+155
-214
lines changed

Diff for: analysis/src/abstract_interpretation/fixpoint_engine.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,7 @@ pub trait FixpointEngine<'mir, 'tcx: 'mir> {
8282
self.new_bottom()
8383
};
8484

85-
for &pred_bb in &mir.predecessors()[bb] {
85+
for &pred_bb in &mir.basic_blocks.predecessors()[bb] {
8686
if let Some(map) = p_state.lookup_after_block(pred_bb) {
8787
// map should contain bb, because we ensure that we have a state for every
8888
// successor

Diff for: analysis/src/domains/reaching_definitions/state.rs

+6-8
Original file line numberDiff line numberDiff line change
@@ -55,18 +55,16 @@ impl<'mir, 'tcx: 'mir> PartialEq for ReachingDefsState<'mir, 'tcx> {
5555
debug_assert_eq!(
5656
{
5757
let mut stable_hasher = StableHasher::new();
58-
self.mir.hash_stable(
59-
&mut self.tcx.create_stable_hashing_context(),
60-
&mut stable_hasher,
61-
);
58+
self.tcx.with_stable_hashing_context(|mut ctx| {
59+
self.mir.hash_stable(&mut ctx, &mut stable_hasher)
60+
});
6261
stable_hasher.finish::<Fingerprint>()
6362
},
6463
{
6564
let mut stable_hasher = StableHasher::new();
66-
other.mir.hash_stable(
67-
&mut other.tcx.create_stable_hashing_context(),
68-
&mut stable_hasher,
69-
);
65+
other.tcx.with_stable_hashing_context(|mut ctx| {
66+
other.mir.hash_stable(&mut ctx, &mut stable_hasher)
67+
});
7068
stable_hasher.finish::<Fingerprint>()
7169
},
7270
);

Diff for: prusti-interface/src/environment/loops.rs

+3-6
Original file line numberDiff line numberDiff line change
@@ -227,7 +227,7 @@ pub struct ProcedureLoops {
227227

228228
impl ProcedureLoops {
229229
pub fn new<'a, 'tcx: 'a>(mir: &'a mir::Body<'tcx>, real_edges: &RealEdges) -> ProcedureLoops {
230-
let dominators = mir.dominators();
230+
let dominators = mir.basic_blocks.dominators();
231231

232232
let mut back_edges: FxHashSet<(_, _)> = FxHashSet::default();
233233
for bb in mir.basic_blocks().indices() {
@@ -496,9 +496,7 @@ impl ProcedureLoops {
496496
debug!("accesses_pairs = {:?}", accesses_pairs);
497497
if let Some(paths) = definitely_initalised_paths {
498498
debug!("definitely_initalised_paths = {:?}", paths);
499-
accesses_pairs = accesses_pairs
500-
.into_iter()
501-
.filter(|(place, kind)| {
499+
accesses_pairs.retain(|(place, kind)| {
502500
paths.iter().any(|initialised_place|
503501
// If the prefix is definitely initialised, then this place is a potential
504502
// loop invariant.
@@ -512,8 +510,7 @@ impl ProcedureLoops {
512510
*kind == PlaceAccessKind::Store &&
513511
utils::is_prefix(*initialised_place, *place)
514512
))
515-
})
516-
.collect();
513+
});
517514
}
518515
debug!("accesses_pairs = {:?}", accesses_pairs);
519516
// Paths to whose leaves we need write permissions.

Diff for: prusti-interface/src/environment/mir_body/borrowck/facts/patch.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,7 @@ pub fn apply_patch_to_borrowck<'tcx>(
7474
}
7575

7676
// Patch cfg_edge facts for the inserted statements.
77-
let predecessors = patched_body.predecessors();
77+
let predecessors = patched_body.basic_blocks.predecessors();
7878
let mut new_statements: Vec<_> = patch
7979
.new_statements
8080
.iter()

Diff for: prusti-interface/src/environment/mir_body/borrowck/facts/validation.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ pub fn validate<'tcx>(
4545
let mid_point = location_table.location_to_point(RichLocation::Mid(location));
4646
assert_eq!(cfg_edges[&start_point], [mid_point]);
4747
let successor_points = &cfg_edges[&mid_point];
48-
let successors: Vec<_> = body.successors(block).collect();
48+
let successors: Vec<_> = body.basic_blocks.successors(block).collect();
4949
assert_eq!(
5050
successors.len(),
5151
successor_points.len(),

Diff for: prusti-interface/src/environment/mod.rs

+2-3
Original file line numberDiff line numberDiff line change
@@ -203,15 +203,14 @@ impl<'tcx> Environment<'tcx> {
203203
pub fn has_errors(&self) -> bool {
204204
self.tcx.sess.has_errors().is_some()
205205
}
206-
207206
/// Get ids of Rust procedures that are annotated with a Prusti specification
208207
pub fn get_annotated_procedures(&self) -> Vec<ProcedureDefId> {
209208
let tcx = self.tcx;
210209
let mut visitor = CollectPrustiSpecVisitor::new(self);
211210
visitor.visit_all_item_likes();
212211

213212
let mut cl_visitor = CollectClosureDefsVisitor::new(self);
214-
tcx.hir().deep_visit_all_item_likes(&mut cl_visitor);
213+
tcx.hir().visit_all_item_likes_in_crate(&mut cl_visitor);
215214

216215
let mut result: Vec<_> = visitor.get_annotated_procedures();
217216
result.extend(cl_visitor.get_closure_defs());
@@ -496,7 +495,7 @@ impl<'tcx> Environment<'tcx> {
496495
called_def_id: ProcedureDefId, // what are we calling?
497496
call_substs: SubstsRef<'tcx>,
498497
) -> (ProcedureDefId, SubstsRef<'tcx>) {
499-
use prusti_rustc_interface::middle::ty::TypeFoldable;
498+
use prusti_rustc_interface::middle::ty::TypeVisitable;
500499

501500
// avoids a compiler-internal panic
502501
if call_substs.needs_infer() {

Diff for: prusti-interface/src/environment/polonius_info.rs

+2-5
Original file line numberDiff line numberDiff line change
@@ -1421,14 +1421,11 @@ impl<'a, 'tcx: 'a> PoloniusInfo<'a, 'tcx> {
14211421
if representative_loan.is_none() {
14221422
return Err(PoloniusInfoError::MagicWandHasNoRepresentativeLoan(location));
14231423
}
1424-
loans = loans
1425-
.into_iter()
1426-
.filter(|loan| {
1424+
loans.retain(|loan| {
14271425
!loan_loops.iter().any(|(loop_loan, _)| {
14281426
loop_loan == loan && Some(*loan) != representative_loan
14291427
})
1430-
})
1431-
.collect();
1428+
});
14321429
}
14331430
}
14341431

Diff for: prusti-interface/src/environment/procedure.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -294,7 +294,7 @@ fn blocks_definitely_leading_to(bb_graph: &HashMap<BasicBlock, BasicBlockNode>,
294294
}
295295

296296
fn blocks_dominated_by(mir: &Mir, dominator: BasicBlock) -> HashSet<BasicBlock> {
297-
let dominators = mir.dominators();
297+
let dominators = mir.basic_blocks.dominators();
298298
let mut blocks = HashSet::new();
299299
for bb in mir.basic_blocks().indices() {
300300
if dominators.is_dominated_by(bb, dominator) {
@@ -321,7 +321,7 @@ fn get_nonspec_basic_blocks(bb_graph: HashMap<BasicBlock, BasicBlockNode>, mir:
321321

322322
/// Returns the set of basic blocks that are not used as part of the typechecking of Prusti specifications
323323
fn build_nonspec_basic_blocks(mir: &Mir, real_edges: &RealEdges, tcx: &TyCtxt) -> HashSet<BasicBlock> {
324-
let dominators = mir.dominators();
324+
let dominators = mir.basic_blocks.dominators();
325325
let mut loop_heads: HashSet<BasicBlock> = HashSet::new();
326326

327327
for source in mir.basic_blocks().indices() {
+23-80
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,15 @@
11
// This file was taken from the compiler:
2-
// https://raw.githubusercontent.com/rust-lang/rust/949b98cab8a186b98bf87e64374b8d0848c55271/compiler/rustc_trait_selection/src/traits/codegen.rs
2+
// https://raw.githubusercontent.com/rust-lang/rust/03d488b48af9f66b91e9400387f781b82411fa82/compiler/rustc_trait_selection/src/traits/codegen.rs
33
// This file is licensed under Apache 2.0
4-
// (https://github.com/rust-lang/rust/blob/949b98cab8a186b98bf87e64374b8d0848c55271/LICENSE-APACHE)
4+
// (https://github.com/rust-lang/rust/blob/03d488b48af9f66b91e9400387f781b82411fa82/LICENSE-APACHE)
55
// and MIT
6-
// (https://github.com/rust-lang/rust/blob/949b98cab8a186b98bf87e64374b8d0848c55271/LICENSE-MIT).
6+
// (https://github.com/rust-lang/rust/blob/03d488b48af9f66b91e9400387f781b82411fa82/LICENSE-MIT).
77

88
// Changes:
99
// + Fix compilation errors.
1010
// + Remove all diagnostics (this is the main motivation for duplication).
11-
// + `ErrorGuaranteed` changed to `()` (private constructor).
11+
// + Remove all `instrument`ation.
12+
// + Replace `crate::*` imports with `prusti_rustc_interface::*` imports.
1213

1314

1415
// This file contains various trait resolution methods used by codegen.
@@ -17,12 +18,12 @@
1718
// general routines.
1819

1920
use log::debug;
20-
use prusti_rustc_interface::trait_selection::infer::{InferCtxt, TyCtxtInferExt};
21+
use prusti_rustc_interface::trait_selection::infer::{TyCtxtInferExt};
2122
use prusti_rustc_interface::trait_selection::traits::{
2223
FulfillmentContext, ImplSource, Obligation, ObligationCause, SelectionContext, TraitEngine,
2324
Unimplemented,
2425
};
25-
use prusti_rustc_interface::middle::ty::fold::TypeFoldable;
26+
use prusti_rustc_interface::middle::traits::CodegenObligationError;
2627
use prusti_rustc_interface::middle::ty::{self, TyCtxt};
2728

2829
/// Attempts to resolve an obligation to an `ImplSource`. The result is
@@ -32,10 +33,10 @@ use prusti_rustc_interface::middle::ty::{self, TyCtxt};
3233
/// obligations *could be* resolved if we wanted to.
3334
///
3435
/// This also expects that `trait_ref` is fully normalized.
35-
pub fn codegen_fulfill_obligation<'tcx>(
36+
pub(super) fn codegen_fulfill_obligation<'tcx>(
3637
tcx: TyCtxt<'tcx>,
3738
(param_env, trait_ref): (ty::ParamEnv<'tcx>, ty::PolyTraitRef<'tcx>),
38-
) -> Result<&'tcx ImplSource<'tcx, ()>, ()> {
39+
) -> Result<&'tcx ImplSource<'tcx, ()>, CodegenObligationError> {
3940
// Remove any references to regions; this helps improve caching.
4041
let trait_ref = tcx.erase_regions(trait_ref);
4142
// We expect the input to be fully normalized.
@@ -57,37 +58,8 @@ pub fn codegen_fulfill_obligation<'tcx>(
5758

5859
let selection = match selcx.select(&obligation) {
5960
Ok(Some(selection)) => selection,
60-
Ok(None) => {
61-
// // Ambiguity can happen when monomorphizing during trans
62-
// // expands to some humongo type that never occurred
63-
// // statically -- this humongo type can then overflow,
64-
// // leading to an ambiguous result. So report this as an
65-
// // overflow bug, since I believe this is the only case
66-
// // where ambiguity can result.
67-
// let reported = infcx.tcx.sess.delay_span_bug(
68-
// prusti_rustc_interface::span::DUMMY_SP,
69-
// &format!(
70-
// "encountered ambiguity selecting `{:?}` during codegen, presuming due to \
71-
// overflow or prior type error",
72-
// trait_ref
73-
// ),
74-
// );
75-
return Err(());
76-
}
77-
Err(Unimplemented) => {
78-
// // This can trigger when we probe for the source of a `'static` lifetime requirement
79-
// // on a trait object: `impl Foo for dyn Trait {}` has an implicit `'static` bound.
80-
// // This can also trigger when we have a global bound that is not actually satisfied,
81-
// // but was included during typeck due to the trivial_bounds feature.
82-
// let guar = infcx.tcx.sess.delay_span_bug(
83-
// prusti_rustc_interface::span::DUMMY_SP,
84-
// &format!(
85-
// "Encountered error `Unimplemented` selecting `{:?}` during codegen",
86-
// trait_ref
87-
// ),
88-
// );
89-
return Err(());
90-
}
61+
Ok(None) => return Err(CodegenObligationError::Ambiguity),
62+
Err(Unimplemented) => return Err(CodegenObligationError::Unimplemented),
9163
Err(e) => {
9264
panic!("Encountered error `{:?}` selecting `{:?}` during codegen", e, trait_ref)
9365
}
@@ -103,52 +75,23 @@ pub fn codegen_fulfill_obligation<'tcx>(
10375
debug!("fulfill_obligation: register_predicate_obligation {:?}", predicate);
10476
fulfill_cx.register_predicate_obligation(&infcx, predicate);
10577
});
106-
let impl_source = drain_fulfillment_cx_or_panic(&infcx, &mut fulfill_cx, impl_source);
78+
79+
// In principle, we only need to do this so long as `impl_source`
80+
// contains unbound type parameters. It could be a slight
81+
// optimization to stop iterating early.
82+
let errors = fulfill_cx.select_all_or_error(&infcx);
83+
if !errors.is_empty() {
84+
return Err(CodegenObligationError::FulfillmentError);
85+
}
86+
87+
let impl_source = infcx.resolve_vars_if_possible(impl_source);
88+
let impl_source = infcx.tcx.erase_regions(impl_source);
10789

10890
// Opaque types may have gotten their hidden types constrained, but we can ignore them safely
10991
// as they will get constrained elsewhere, too.
11092
let _opaque_types = infcx.inner.borrow_mut().opaque_type_storage.take_opaque_types();
11193

112-
debug!("Cache miss: {:?} => {:?}", trait_ref, impl_source);
94+
debug!("Cache miss: {trait_ref:?} => {impl_source:?}");
11395
Ok(&*tcx.arena.alloc(impl_source))
11496
})
11597
}
116-
117-
// # Global Cache
118-
119-
/// Finishes processes any obligations that remain in the
120-
/// fulfillment context, and then returns the result with all type
121-
/// variables removed and regions erased. Because this is intended
122-
/// for use outside of type inference, if any errors occur,
123-
/// it will panic. It is used during normalization and other cases
124-
/// where processing the obligations in `fulfill_cx` may cause
125-
/// type inference variables that appear in `result` to be
126-
/// unified, and hence we need to process those obligations to get
127-
/// the complete picture of the type.
128-
fn drain_fulfillment_cx_or_panic<'tcx, T>(
129-
infcx: &InferCtxt<'_, 'tcx>,
130-
fulfill_cx: &mut FulfillmentContext<'tcx>,
131-
result: T,
132-
) -> T
133-
where
134-
T: TypeFoldable<'tcx>,
135-
{
136-
debug!("drain_fulfillment_cx_or_panic()");
137-
138-
// In principle, we only need to do this so long as `result`
139-
// contains unbound type parameters. It could be a slight
140-
// optimization to stop iterating early.
141-
let errors = fulfill_cx.select_all_or_error(infcx);
142-
if !errors.is_empty() {
143-
// infcx.tcx.sess.delay_span_bug(
144-
// prusti_rustc_interface::span::DUMMY_SP,
145-
// &format!(
146-
// "Encountered errors `{:?}` resolving bounds outside of type inference",
147-
// errors
148-
// ),
149-
// );
150-
}
151-
152-
let result = infcx.resolve_vars_if_possible(result);
153-
infcx.tcx.erase_regions(result)
154-
}

0 commit comments

Comments
 (0)