Class OwnershipPathVerifier

java.lang.Object
org.ek9lang.compiler.phase9.OwnershipPathVerifier
public final class OwnershipPathVerifier extends Object
THE per-path rules of the ownership form (EK9_IR_OWNERSHIP_STAGE4_DESIGN.md): V-A - every OWNED value is consumed exactly once on every path to a normal exit and to every exceptional exit - and V-J - a path that ends in a Panic owes nothing.

It tracks OBLIGATIONS: an OWNED value (ValueKind.madeBy(IRInstr), or OWN v) is one, discharged by exactly one consumer - DROP, DROP_AT_EXIT (handed to a region, which drops it at every exit, unwind included), a [consume] assignment, an owned call argument, THROW, a forwarding CAST (the obligation moves to the cast). Slots are their owners' (V-G), so they carry none.

Paths, compositionally (design §3): every nested list of a composite is CLOSED - what it makes it discharges, and it discharges nothing it was given. Flat branches inside a list are followed label by label, the state compared at every join and required empty at every RETURN. At every call - every call may throw until the effect summary exists - each live obligation must already be covered (handed to a region), or it leaks on that call's unwind edge.

Enforced (design §4, step 3): IR_ANALYSIS fails a compile on any finding, as it does for OwnershipVerifier.

  • Method Details

    • check

      public static List<String> check(IRConstruct construct)
      The per-path findings of every operation of a construct, as "operation: problem"; empty when every path of every operation keeps V-A.

    • check

      static List<String> check(List<IRInstr> body)
      The per-path findings of one operation body.