2525//! materializer's pending-value register is full. Tracking span *ids* (not just
2626//! a depth) proves every `SpanEnd` closes the span the matching bracket opened,
2727//! so inspection extraction can assert pairing instead of re-validating. The
28- //! walk starts from each entry point wrapper and follows `Match` successors,
29- //! descending through `Call` and resuming at its return address — exactly the
30- //! edge set that orders effects at runtime .
28+ //! walk starts from each entry definition and follows `Match` successors,
29+ //! descending through `Call` and resuming at its return address. Entry-owned
30+ //! record/node effects are modeled around the resulting definition summary .
3131//!
3232//! ## Why state *sets* (collecting semantics)
3333//!
7575//! summary instead of inlining, which both terminates and stays sound. The
7676//! summaries are computed by a monotone fixpoint (a callee that reads its
7777//! caller's top before pushing propagates the constraint up to its own
78- //! callers), then a final pass checks every call site and every entry point
79- //! wrapper against the stabilized summaries.
78+ //! callers), then a final pass checks every call site and every entry boundary
79+ //! against the stabilized summaries.
8080//!
8181//! `record_sets_caller_top` exists because a below-entry `RecordSet` mutates state the
8282//! caller's walk otherwise cannot see: setting a field on the caller's *variant*
8787//! panic past the check.
8888//!
8989//! A successor-less `Match` accepts the *whole run* from any call depth,
90- //! freezing the log with every caller frame still open. Inside an entry point
91- //! wrapper the local stack is the global stack, so the existing exit check is
92- //! exact; inside a body reachable through `Call` the caller's frames are
93- //! invisible here, so such accepts are rejected outright — the compiler ends
94- //! every definition body with `Return` and only accepts at wrapper level.
90+ //! freezing the log with every caller frame still open. Inside a body reachable
91+ //! through `Call` the caller's frames are invisible here, so such accepts are
92+ //! rejected outright — the compiler ends every definition body with `Return`.
9593//!
9694//! Net-neutrality, no popping below entry, and suppression balance are not
9795//! assumed — they are verified, so a malformed body is rejected
@@ -113,7 +111,7 @@ use std::collections::{HashMap, HashSet, VecDeque};
113111
114112use super :: { Instruction , Module , ModuleError } ;
115113use crate :: bytecode:: {
116- CodeAddr , Effect , EffectKind , FrameAction , TypeDefKind , TypeKind , ValueFrameKind ,
114+ CodeAddr , Effect , EffectKind , EntryBoundary , FrameAction , TypeDefKind , TypeKind , ValueFrameKind ,
117115} ;
118116
119117/// Builder frames the materializer pushes. The root/result frame can be a
@@ -328,19 +326,22 @@ pub(crate) fn validate_effect_stack(module: &Module) -> Result<(), ModuleError>
328326 ) ?;
329327 }
330328
331- // ...and every entry point wrapper. A wrapper has no caller, so a residual
332- // caller-top constraint means some effect would read below the frames the
333- // wrapper itself opened and hit the materializer's result root frame.
329+ // Entry boundaries supply the root frame/effect that used to be executable
330+ // wrapper instructions.
334331 for entry_point in entry_points. iter ( ) {
335332 let target = entry_point. target ( ) ;
336- let wrapper = analyze (
337- module,
338- & summaries,
339- target,
340- BodyRole :: from_called ( called. contains ( & target) ) ,
341- VerifyPhase :: Final ,
342- ) ?;
343- if wrapper. entry_tos != KS_ANY {
333+ let summary = summaries[ & target] ;
334+ let boundary = entry_point. boundary ( ) ;
335+ let accepts_caller_top = match boundary {
336+ EntryBoundary :: Record => summary. entry_tos & KS_RECORD != 0 ,
337+ EntryBoundary :: Passthrough | EntryBoundary :: Node => summary. entry_tos == KS_ANY ,
338+ } ;
339+ if !accepts_caller_top {
340+ return Err ( ModuleError :: EffectStackImbalance ( target) ) ;
341+ }
342+ if matches ! ( boundary, EntryBoundary :: Node | EntryBoundary :: Record )
343+ && summary. returns_pending == Some ( true )
344+ {
344345 return Err ( ModuleError :: EffectStackImbalance ( target) ) ;
345346 }
346347 }
@@ -600,10 +601,9 @@ fn analyze(
600601 ) ?;
601602 }
602603 if m. succ_count ( ) == 0 {
603- // A successor-less match accepts the whole run. At wrapper
604- // level the local stack is the global stack, so balance
605- // here is exact; under a `Call` the caller's frames are
606- // still open in the log, so this is never sound.
604+ // A successor-less match accepts the whole run. Under a
605+ // `Call`, caller frames are still open in the log, so this
606+ // is never sound.
607607 if role == BodyRole :: Called {
608608 return Err ( ModuleError :: EffectStackImbalance ( addr) ) ;
609609 }
@@ -651,7 +651,7 @@ impl CallRoute {
651651 fn from_instruction ( instruction : Instruction < ' _ > ) -> Option < Self > {
652652 match instruction {
653653 Instruction :: Call ( call) => Some ( Self {
654- target : CodeAddr :: from ( u16 :: from ( call. target ) ) ,
654+ target : call. target ,
655655 returns : call
656656 . returns ( )
657657 . map ( |addr| CodeAddr :: from ( u16:: from ( addr) ) )
0 commit comments