From 8a03fd7ab26b1ae5d2364e973b2b386f8ca38cd9 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 15 Aug 2026 10:02:48 +0000 Subject: [PATCH] Take the state at a join as the disjunction of the states behind it A block reached by more than one edge took a predicate variable for its precondition, inferred from a clause per incoming edge. The states its predecessors leave say exactly what it is entered in, so their disjunction is its precondition, and only a loop header still has one to infer: the state carried by its back edge is not yet known when it is analyzed. A disjunction is no conjunct of a Horn clause body, so this holds only as long as no predicate variable appears in the states. Where one does, the disjunction is named by a predicate variable of its own, bounded from below by each state, which is what the block had all along. `needs_own_precondition` becomes `is_loop_header` accordingly. The states are collected as the predecessors are analyzed and installed once they all have been, so a block that inherits its precondition now holds the states until then rather than a flag. Over the pass tests this drops the predicate variables from 734 to 676 and the constraints from 917 KiB to 832 KiB: naming a state costs an argument list at every use, which the disjunction rarely exceeds. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01P7MyQbvfkfNy1h7yeN553N --- src/analyze.rs | 100 +++++++++++++++++++++++++++++++------ src/analyze/basic_block.rs | 45 +++++++---------- src/analyze/local_def.rs | 21 ++++---- src/chc.rs | 19 +++++++ src/rty.rs | 33 +++++++++++- src/rty/subtyping.rs | 31 +++++++++++- 6 files changed, 192 insertions(+), 57 deletions(-) diff --git a/src/analyze.rs b/src/analyze.rs index fce97595..ed544293 100644 --- a/src/analyze.rs +++ b/src/analyze.rs @@ -188,7 +188,18 @@ enum DefTy<'tcx> { #[derive(Debug, Clone)] struct BasicBlockDef { ty: BasicBlockType, - has_precondition: bool, + precondition: BasicBlockPrecondition, +} + +/// How a basic block comes by its precondition. +#[derive(Debug, Clone)] +enum BasicBlockPrecondition { + /// Already installed, be it from an annotation, the signature of the function, or a predicate + /// variable left to be inferred. + Installed, + /// The disjunction of the states its predecessors leave, collected as they are analyzed and + /// installed once they all have been. + Inherited(Vec>), } #[derive(Debug, Clone, Default)] @@ -553,7 +564,7 @@ impl<'tcx> Analyzer<'tcx> { bb, BasicBlockDef { ty: rty, - has_precondition: true, + precondition: BasicBlockPrecondition::Installed, }, ); } @@ -569,7 +580,7 @@ impl<'tcx> Analyzer<'tcx> { bb, BasicBlockDef { ty: rty, - has_precondition: false, + precondition: BasicBlockPrecondition::Inherited(Vec::new()), }, ); } @@ -579,30 +590,89 @@ impl<'tcx> Analyzer<'tcx> { def_id = ?def_id, ?bb, rty = %def.ty.display(), - has_precondition = def.has_precondition, "register_basic_block_def", ); self.basic_blocks.entry(def_id).or_default().insert(bb, def); } - pub fn register_basic_block_precondition( + /// Records the state a predecessor leaves as one of the states the block is entered in. + pub fn push_basic_block_precondition( &mut self, def_id: LocalDefId, bb: BasicBlock, precondition: rty::Refinement, ) { - let bb_def = &mut self - .basic_blocks + let bb_def = self.basic_block_def_mut(def_id, bb); + match &mut bb_def.precondition { + BasicBlockPrecondition::Inherited(states) => states.push(precondition), + BasicBlockPrecondition::Installed => { + panic!("precondition of {bb:?} is already installed") + } + } + } + + /// Installs the precondition of a block that inherits it, once every predecessor has been + /// analyzed. + /// + /// The states its predecessors leave are the states it is entered in, so their disjunction is + /// its precondition. A disjunction is no conjunct of a Horn clause body, so when a predicate + /// variable appears in one of the states, the disjunction has to be named by a predicate + /// variable of its own, bounded from below by every state. + pub fn install_inherited_basic_block_precondition( + &mut self, + def_id: LocalDefId, + bb: BasicBlock, + ) { + let bb_def = self.basic_block_def_mut(def_id, bb); + let states = + match std::mem::replace(&mut bb_def.precondition, BasicBlockPrecondition::Installed) { + BasicBlockPrecondition::Inherited(states) => states, + BasicBlockPrecondition::Installed => return, + }; + let ty = bb_def.ty.clone(); + + let precondition = match rty::Refinement::disjunction(states.iter().cloned()) { + Some(disjunction) => disjunction, + None => { + let template = self.precondition_template(&ty); + for state in states { + let clauses = + rty::relate_sub_precondition(&ty.as_ref().params, state, template.clone()); + self.extend_clauses(clauses); + } + template + } + }; + self.basic_block_def_mut(def_id, bb) + .ty + .set_precondition(precondition); + } + + /// A predicate variable standing for the precondition of a basic block, over its parameters. + fn precondition_template( + &mut self, + ty: &BasicBlockType, + ) -> rty::Refinement { + use crate::refine::TemplateRegistry as _; + + let params = &ty.as_ref().params; + let last_param_idx = params.last_index().expect("basic block has a parameter"); + let mut builder = rty::TemplateBuilder::default(); + for (param_idx, param) in params.iter_enumerated() { + if param_idx != last_param_idx { + builder.add_dependency(param_idx, param.ty.to_sort()); + } + } + let template = builder.build(params[last_param_idx].ty.clone()); + self.register_template(template).refinement + } + + fn basic_block_def_mut(&mut self, def_id: LocalDefId, bb: BasicBlock) -> &mut BasicBlockDef { + self.basic_blocks .get_mut(&def_id) .unwrap() .get_mut(&bb) - .unwrap(); - assert!( - !bb_def.has_precondition, - "precondition is already registered for basic block" - ); - bb_def.has_precondition = true; - bb_def.ty.set_precondition(precondition); + .unwrap() } pub fn basic_block_ty(&self, def_id: LocalDefId, bb: BasicBlock) -> &BasicBlockType { @@ -616,7 +686,7 @@ impl<'tcx> Analyzer<'tcx> { ) -> &BasicBlockType { let def = &self.basic_blocks[&def_id][&bb]; assert!( - def.has_precondition, + matches!(def.precondition, BasicBlockPrecondition::Installed), "basic block does not have precondition" ); &def.ty diff --git a/src/analyze/basic_block.rs b/src/analyze/basic_block.rs index 6a7f4a1c..50329bdc 100644 --- a/src/analyze/basic_block.rs +++ b/src/analyze/basic_block.rs @@ -24,29 +24,19 @@ mod drop_point; mod visitor; pub use drop_point::DropPoints; -/// Whether a basic block needs a precondition of its own, rather than -/// inheriting its predecessor's outgoing env state. +/// Whether `bb` is a loop header, i.e. it is reached by an edge that closes a cycle. /// -/// This holds for `START_BLOCK` (whose precondition comes from the function -/// signature, not a predecessor) and for every block reached by more than one -/// CFG edge — i.e. join points with multiple predecessors, or multiple edges -/// from a single predecessor (e.g. `SwitchInt` arms that share a target). +/// Basic blocks are analyzed in reverse postorder, under which every predecessor of a block comes +/// before it unless the edge back to it closes a cycle. A block reached only from blocks analyzed +/// before it inherits the states they leave as its precondition; a loop header cannot, as the +/// state carried around the loop is not yet known when it is analyzed, and has to be inferred. /// -/// A block with a unique incoming edge can inherit that edge's env state, so it -/// needs no precondition of its own. A block that does need one currently models -/// it with a fresh predicate variable; this is also the set of CFG cutpoints, so -/// it cuts every cycle (a loop header always has in-degree >= 2). -pub fn needs_own_precondition(body: &Body<'_>, bb: BasicBlock) -> bool { - if bb == mir::START_BLOCK { - return true; - } - let preds = &body.basic_blocks.predecessors()[bb]; - if preds.len() != 1 { - return true; - } - let pred = preds[0]; - let pred_term = body.basic_blocks[pred].terminator(); - pred_term.successors().filter(|s| *s == bb).count() > 1 +/// These blocks are the cutpoints of the CFG, so a precondition inferred here cuts every cycle. +pub fn is_loop_header(body: &Body<'_>, bb: BasicBlock) -> bool { + let doms = body.basic_blocks.dominators(); + body.basic_blocks.predecessors()[bb] + .iter() + .any(|&pred| doms.dominates(bb, pred)) } /// Adapts the actual arguments of a call to the parameter list of the callee's function type. @@ -755,8 +745,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { bb: BasicBlock, outer_fn_param_vars: &HashMap, ) { - if !needs_own_precondition(&self.body, bb) { - self.install_inherited_bb_ty(bb, outer_fn_param_vars); + if !is_loop_header(&self.body, bb) { + self.push_inherited_precondition(bb, outer_fn_param_vars); return; } let bty = self.basic_block_ty_with_precondition(bb); @@ -793,10 +783,9 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { self.ctx.extend_clauses(clauses); } - /// Materializes the `BasicBlockType` for a target that inherits its - /// precondition by building its (pvar-free) layout and overwriting the last - /// param's refinement with the current env state. - fn install_inherited_bb_ty( + /// Records the env state this block leaves as one of the states `bb` is entered in, which its + /// precondition is the disjunction of. + fn push_inherited_precondition( &mut self, bb: BasicBlock, outer_fn_param_vars: &HashMap, @@ -825,7 +814,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let precondition = capture.finish(&self.env); self.ctx - .register_basic_block_precondition(self.local_def_id, bb, precondition); + .push_basic_block_precondition(self.local_def_id, bb, precondition); } fn with_assumptions(&mut self, assumptions: Vec>, callback: F) -> T diff --git a/src/analyze/local_def.rs b/src/analyze/local_def.rs index 50a587fe..7f5d476f 100644 --- a/src/analyze/local_def.rs +++ b/src/analyze/local_def.rs @@ -744,16 +744,12 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { } /// Walks up the dominator tree from the marker block to the innermost - /// enclosing loop header: the first dominator that needs its own - /// precondition (in-degree >= 2) and has a back edge. + /// enclosing loop header. fn loop_header_of(body: &Body<'_>, marker_bb: BasicBlock) -> Option { let doms = body.basic_blocks.dominators(); - let preds = body.basic_blocks.predecessors(); let mut cur = Some(marker_bb); while let Some(bb) = cur { - if analyze::basic_block::needs_own_precondition(body, bb) - && preds[bb].iter().any(|&p| doms.dominates(bb, p)) - { + if analyze::basic_block::is_loop_header(body, bb) { return Some(bb); } cur = doms.immediate_dominator(bb); @@ -1021,7 +1017,7 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { let bty = self.entry_block_ty(expected, live_locals, ret_ty); self.ctx .register_basic_block_ty_with_precondition(self.local_def_id, bb, bty); - } else if analyze::basic_block::needs_own_precondition(&self.body, bb) { + } else if analyze::basic_block::is_loop_header(&self.body, bb) { let bty = self .type_builder .for_template(&mut self.ctx) @@ -1029,9 +1025,8 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { self.ctx .register_basic_block_ty_with_precondition(self.local_def_id, bb, bty); } else { - // The block inherits its predecessor's outgoing env state as its - // precondition, materialized lazily during the predecessor's - // analysis. Record only unrefined type here. + // The block inherits the states its predecessors leave as its precondition, + // which is only known once they have all been analyzed. Record the type alone. let bty = self .type_builder .build_basic_block(&self.body, live_locals, ret_ty); @@ -1043,12 +1038,14 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> { fn analyze_basic_blocks(&mut self, expected_fn_ty: &rty::RefinedType) { let expected_fn_ty = expected_fn_ty.ty.as_function().unwrap(); - // Reverse postorder guarantees each block that inherits its precondition - // is visited after the predecessor that lazily materialized its type. + // Reverse postorder guarantees each block that inherits its precondition is visited + // after every predecessor that leaves a state for it. for (bb, data) in mir::traversal::reverse_postorder(&self.body) { if data.is_cleanup { continue; } + self.ctx + .install_inherited_basic_block_precondition(self.local_def_id, bb); let rty = self .ctx .basic_block_ty_with_precondition(self.local_def_id, bb) diff --git a/src/chc.rs b/src/chc.rs index b70112c0..e145f7fd 100644 --- a/src/chc.rs +++ b/src/chc.rs @@ -1225,6 +1225,10 @@ impl Pred { } } + pub fn is_var(&self) -> bool { + matches!(self, Pred::Var(_)) + } + pub fn is_top(&self) -> bool { match self { Pred::Known(p) => p.is_top(), @@ -1787,6 +1791,21 @@ impl Body { self.formula.push_conj(formula); } + /// The body stated as a single formula, unless a predicate variable appears in it. + /// + /// A formula holds no predicate variable, because the only place a Horn clause has for one is + /// a conjunct of its body or its head (see [`Formula`]). + pub fn into_formula(self) -> Option> { + if self.atoms.iter().any(|atom| atom.pred.is_var()) { + return None; + } + let mut formula = self.formula; + for atom in self.atoms { + formula.push_conj(Formula::Atom(atom)); + } + Some(formula) + } + pub fn map_var(self, mut f: F) -> Body where F: FnMut(V) -> W, diff --git a/src/rty.rs b/src/rty.rs index c0c068bc..c2b43771 100644 --- a/src/rty.rs +++ b/src/rty.rs @@ -52,7 +52,7 @@ mod clause_builder; pub use clause_builder::ClauseBuilderExt; mod subtyping; -pub use subtyping::{ClauseScope, Subtyping}; +pub use subtyping::{relate_sub_precondition, ClauseScope, Subtyping}; mod params; pub use params::{RefinedTypeArgs, TypeParamIdx, TypeParamSubst}; @@ -1522,6 +1522,37 @@ where self.existentials.extend(existentials); self.body.simplify(); } + + /// The disjunction of the formulas, unless a predicate variable appears in one of them. + /// + /// The existential variables of every disjunct are hoisted in front of the disjunction, which + /// they may be as long as every sort is inhabited. A disjunct that holds a predicate variable + /// has no such form, as a disjunction is no conjunct of a Horn clause body. A single formula + /// stands for itself, and is under no such restriction. + pub fn disjunction(formulas: impl IntoIterator) -> Option { + let mut formulas: Vec<_> = formulas.into_iter().collect(); + if formulas.len() == 1 { + return formulas.pop(); + } + + let mut existentials = IndexVec::new(); + let mut disjuncts = Vec::new(); + for Formula { + existentials: disjunct_existentials, + body, + } in formulas + { + let base = existentials.len(); + existentials.extend(disjunct_existentials); + disjuncts.push(body.map_var(|v| v.shift_existential(base)).into_formula()?); + } + let body = match disjuncts.len() { + 0 => chc::Body::bottom(), + 1 => disjuncts.pop().unwrap().into(), + _ => chc::Formula::Or(disjuncts).into(), + }; + Some(Formula::new(existentials, body)) + } } /// A refinement predicate in a refinement type. diff --git a/src/rty/subtyping.rs b/src/rty/subtyping.rs index 4125d794..d2dd00d8 100644 --- a/src/rty/subtyping.rs +++ b/src/rty/subtyping.rs @@ -1,9 +1,13 @@ //! Translation of subtyping relations into CHC constraints. +use rustc_index::IndexVec; + use crate::chc; use crate::pretty::PrettyDisplayExt; -use super::{ClauseBuilderExt as _, PointerKind, RefKind, RefinedType, Type}; +use super::{ + ClauseBuilderExt as _, FunctionParamIdx, PointerKind, RefKind, RefinedType, Refinement, Type, +}; /// A scope for building clauses. /// @@ -168,3 +172,28 @@ where clauses } } + +/// Produces the constraint that a state a basic block is entered in satisfies its precondition. +/// +/// A precondition is a refinement of the last parameter of the block, over the other parameters +/// (see [`crate::refine::BasicBlockType::set_precondition`]), and both refinements are stated in +/// terms of the given parameters. +#[must_use] +pub fn relate_sub_precondition( + params: &IndexVec>, + got: Refinement, + expected: Refinement, +) -> Vec { + let mut builder = chc::ClauseBuilder::default(); + for (param_idx, param) in params.iter_enumerated() { + let param_sort = param.ty.to_sort(); + if !param_sort.is_singleton() { + builder.add_mapped_var(param_idx, param_sort); + } + } + let last_param_idx = params.last_index().expect("basic block has a parameter"); + builder + .with_mapped_value_var(last_param_idx) + .add_body(got) + .head(expected) +}