Take the state at a join as the disjunction of the states behind it

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<rty::Refinement<rty::FunctionParamIdx>>),
 }
 
 #[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<rty::FunctionParamIdx>,
     ) {
-        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<rty::FunctionParamIdx> {
+        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

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<rty::FunctionParamIdx, Var>,
     ) {
-        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<rty::FunctionParamIdx, Var>,
@@ -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<F, T>(&mut self, assumptions: Vec<impl Into<Assumption>>, callback: F) -> T

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<BasicBlock> {
         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,17 +1017,16 @@ 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)
                     .build_basic_block(&self.body, live_locals, ret_ty);
                 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)

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<V> Body<V> {
         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<Formula<V>> {
+        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<F, W>(self, mut f: F) -> Body<W>
     where
         F: FnMut(V) -> W,

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<Item = Self>) -> Option<Self> {
+        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.