Document wf constraints on control flow in cleanup blocks

Also fixes a bug in dominator computation
This commit is contained in:
Jakob Degen 2023-01-08 18:23:13 -08:00
parent 4781233a77
commit f49126e3d6
3 changed files with 68 additions and 6 deletions

View File

@ -1,6 +1,8 @@
//! Validates the MIR to ensure that invariants are upheld.
use rustc_data_structures::fx::FxHashSet;
use std::collections::hash_map::Entry;
use rustc_data_structures::fx::{FxHashMap, FxHashSet};
use rustc_index::bit_set::BitSet;
use rustc_infer::traits::Reveal;
use rustc_middle::mir::interpret::Scalar;
@ -18,7 +20,7 @@ use rustc_mir_dataflow::storage::always_storage_live_locals;
use rustc_mir_dataflow::{Analysis, ResultsCursor};
use rustc_target::abi::{Size, VariantIdx};
#[derive(Copy, Clone, Debug)]
#[derive(Copy, Clone, Debug, PartialEq, Eq)]
enum EdgeKind {
Unwind,
Normal,
@ -57,7 +59,7 @@ impl<'tcx> MirPass<'tcx> for Validator {
.iterate_to_fixpoint()
.into_results_cursor(body);
TypeChecker {
let mut checker = TypeChecker {
when: &self.when,
body,
tcx,
@ -67,8 +69,9 @@ impl<'tcx> MirPass<'tcx> for Validator {
storage_liveness,
place_cache: Vec::new(),
value_cache: Vec::new(),
}
.visit_body(body);
};
checker.visit_body(body);
checker.check_cleanup_control_flow();
}
}
@ -134,6 +137,55 @@ impl<'a, 'tcx> TypeChecker<'a, 'tcx> {
}
}
fn check_cleanup_control_flow(&self) {
let doms = self.body.basic_blocks.dominators();
let mut post_contract_node = FxHashMap::default();
let mut get_post_contract_node = |mut bb| {
if let Some(res) = post_contract_node.get(&bb) {
return *res;
}
let mut dom_path = vec![];
while self.body.basic_blocks[bb].is_cleanup {
dom_path.push(bb);
bb = doms.immediate_dominator(bb);
}
let root = *dom_path.last().unwrap();
for bb in dom_path {
post_contract_node.insert(bb, root);
}
root
};
let mut parent = FxHashMap::default();
for (bb, bb_data) in self.body.basic_blocks.iter_enumerated() {
if !bb_data.is_cleanup || !self.reachable_blocks.contains(bb) {
continue;
}
let bb = get_post_contract_node(bb);
for s in bb_data.terminator().successors() {
let s = get_post_contract_node(s);
if s == bb {
continue;
}
match parent.entry(bb) {
Entry::Vacant(e) => {
e.insert(s);
}
Entry::Occupied(e) if s != *e.get() => self.fail(
Location { block: bb, statement_index: 0 },
format!(
"Cleanup control flow violation: The blocks dominated by {:?} have edges to both {:?} and {:?}",
bb,
s,
*e.get()
)
),
Entry::Occupied(_) => (),
}
}
}
}
/// Check if src can be assigned into dest.
/// This is not precise, it will accept some incorrect assignments.
fn mir_assign_valid_types(&self, src: Ty<'tcx>, dest: Ty<'tcx>) -> bool {

View File

@ -135,7 +135,10 @@ pub fn dominators<G: ControlFlowGraph>(graph: G) -> Dominators<G::Node> {
// This loop computes the semi[w] for w.
semi[w] = w;
for v in graph.predecessors(pre_order_to_real[w]) {
let v = real_to_pre_order[v].unwrap();
// Reachable vertices may have unreachable predecessors, so ignore any of them
let Some(v) = real_to_pre_order[v] else {
continue
};
// eval returns a vertex x from which semi[x] is minimum among
// vertices semi[v] +> x *> v.

View File

@ -512,6 +512,13 @@ pub struct CopyNonOverlapping<'tcx> {
/// must also be `cleanup`. This is a part of the type system and checked statically, so it is
/// still an error to have such an edge in the CFG even if it's known that it won't be taken at
/// runtime.
/// 4. The induced subgraph on cleanup blocks must look roughly like an upside down tree. This is
/// necessary to ensure that landing pad information can be correctly codegened. More precisely:
///
/// Begin with the standard control flow graph `G`. Modify `G` as follows: for any two cleanup
/// vertices `u` and `v` such that `u` dominates `v`, contract `u` and `v` into a single vertex,
/// deleting self edges and duplicate edges in the process. The cleanup blocks of the resulting
/// graph must form an inverted forest.
#[derive(Clone, TyEncodable, TyDecodable, Hash, HashStable, PartialEq, TypeFoldable, TypeVisitable)]
pub enum TerminatorKind<'tcx> {
/// Block has one successor; we continue execution there.