Class ConstraintState

java.lang.Object
org.ek9lang.compiler.phase5.flow.ConstraintState
public final class ConstraintState extends Object
Immutable constraint state mapping variables to their abstract values.

At each program point, a ConstraintState maps each tracked variable to its abstract value. Untracked variables are implicitly TopValue.INSTANCE.

Supports copy-on-write semantics for branch splitting — creating a new state from an existing one is cheap (shallow copy of the internal map).

  • Constructor Details

    • ConstraintState

      public ConstraintState()
      Create an empty constraint state.

  • Method Details

    • snapshot

      public ConstraintState snapshot()
      Create a snapshot (copy) of this state for branch splitting.

    • get

      public AbstractValue get(ISymbol symbol)
      Get the abstract value for a symbol. Returns TOP if not tracked.

    • set

      public void set(ISymbol symbol, AbstractValue abstractValue)
      Set the abstract value for a symbol (mutates this state).

    • setMay

      public void setMay(ISymbol symbol, Object value)
      Record that symbol definitely holds value here, REPLACING anything it may have held before — a later write kills an earlier value on this path.

    • setMayAll

      public void setMayAll(ISymbol symbol, Set<Object> values)
      Record the full set of values that may reach symbol here, REPLACING what came before. Used where a value arrives from an expression with several arms (a ternary, a switch expression) rather than from a single assignment.

    • clearMay

      public void clearMay(ISymbol symbol)
      Record that nothing is provable about symbol here. Clears rather than keeps, so a value that has been overwritten by something unknowable can never be reported as still arriving.

    • getMay

      public Set<Object> getMay(ISymbol symbol)
      The constant values that reach this point on SOME path; empty when nothing is provable.

    • markUnreachable

      public void markUnreachable()
      Mark this state as unreachable (BOTTOM). Used after throw statements or contradictory conditions.

    • isUnreachable

      public boolean isUnreachable()
      Check if this state represents an unreachable program point.

    • join

      public static ConstraintState join(ConstraintState first, ConstraintState second)
      Join this state with another at a branch convergence point.

      If either state is unreachable (BOTTOM), the other state is used. Otherwise, for each variable, the joined value is the lattice join of both branch values.

      Parameters:
      first - the state from the first branch
      second - the state from the second branch
      Returns:
      a new joined state

    • joinRetainingMayOf

      public static ConstraintState joinRetainingMayOf(ConstraintState first, ConstraintState second)
      Join for a construct whose second state is GUARANTEED to have executed - the body of a do ... while loop, or a finally block.

      The MUST side still joins with the first state: a body such as n: n + 1 produces a different constant on every iteration, so only TOP is sound there. The MAY side takes the second state ALONE - because that code definitely ran, a definition it overwrote can no longer reach the exit. Unioning the MAY sets here is precisely what makes an unconditional repair inside a do body fail to kill the breach it repairs.

      A body that assigns only CONDITIONALLY needs no special handling: the branch join inside that body has already unioned the surviving earlier value into its own MAY set.

      Parameters:
      first - the state before the guaranteed code ran
      second - the state after it ran - the sole source of the MAY side
      Returns:
      joined MUST side, second's MAY side

    • evaluateCondition

      public ConditionResult evaluateCondition(AbstractValue left, String operator, AbstractValue right)
      Evaluate a condition given the current state of two symbols/values.
      Parameters:
      left - the abstract value of the left operand
      operator - the comparison operator
      right - the abstract value of the right operand
      Returns:
      the condition evaluation result

    • toString

      public String toString()
      Overrides:
      toString in class Object