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.

    • trackedSymbols

      public Set<ISymbol> trackedSymbols()
      Every symbol this state holds anything about (a value or the values it may hold), as a copy.

    • 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.

    • markFreshInLoop

      public void markFreshInLoop(ISymbol symbol)
      Note that symbol was written since the innermost loop body was entered (see freshInLoop).

    • unmarkFreshInLoop

      public void unmarkFreshInLoop(ISymbol symbol)
      symbol was written with something other than a literal: what it holds may be what an earlier pass left in another variable, so it is no longer fresh (see freshInLoop).

    • isFreshInLoop

      public boolean isFreshInLoop(ISymbol symbol)
      True if symbol was written, on every path here, since the innermost loop body was entered.

    • clearFreshInLoop

      public void clearFreshInLoop()
      A loop body is being entered: nothing has been written in it yet.

    • 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 ConstraintState join(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. This state is the first branch's; neither is changed.

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

    • joinRetainingMayOf

      public ConstraintState joinRetainingMayOf(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.

      This state is the one before the guaranteed code ran.

      Parameters:
      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