Interface AbstractValue

All Known Implementing Classes:
BottomValue, CollectionStateValue, ConstantValue, ExcludesConstantValue, LockIdentityValue, RangeValue, SetStateValue, TopValue
public sealed interface AbstractValue permits TopValue, BottomValue, ConstantValue, RangeValue, SetStateValue, ExcludesConstantValue, CollectionStateValue, LockIdentityValue
Represents an abstract value in the value-tracking lattice for flow analysis.

The lattice has the following structure:

        TOP (unknown / no information)
       / | \
  Constant  Range  SetState
       \ | /
       BOTTOM (unreachable / contradiction)

Phase 1 implements: TOP, BOTTOM, and ConstantValue (Integer, Boolean, String). Phase 2 adds RangeValue for integer range constraints from condition narrowing. Phase 3 adds SetStateValue for isSet/unset tracking from guards and literals. Slice-2 deadlock detection adds LockIdentityValue tracking which MutexLock object a variable refers to.

  • Method Summary

    Modifier and Type
    Method
    Description
    ConditionResult
    evaluateCondition(String operator, AbstractValue operand)
    Evaluate whether this abstract value satisfies a comparison condition.
    boolean
    isBottom()
    Check if this value represents an unreachable program point.
    static boolean
    isImplicitlySetMorePrecise(AbstractValue value)
    True if the value is both implicitly SET and strictly more precise than a bare SET state, so that SET join <value> should keep this more precise value at a branch convergence.
    boolean
    isKnown()
    Check if this value represents a known state (not TOP and not BOTTOM).
    default boolean
    isKnownSet()
    Check if this value is known to represent a SET variable.
    AbstractValue
    join(AbstractValue other)
    Join this value with another at a branch convergence point.

  • Method Details

    • join

      AbstractValue join(AbstractValue other)
      Join this value with another at a branch convergence point. Returns the least upper bound of the two values.

      Key rules:

      • BOTTOM join X = X (unreachable path is ignored)
      • X join BOTTOM = X
      • TOP join X = TOP
      • Constant(a) join Constant(a) = Constant(a) (both agree)
      • Constant(a) join Constant(b) = TOP (disagreement)

    • evaluateCondition

      ConditionResult evaluateCondition(String operator, AbstractValue operand)
      Evaluate whether this abstract value satisfies a comparison condition.
      Parameters:
      operator - the comparison operator (==, <>, <, >, etc.)
      operand - the right-hand side value to compare against
      Returns:
      TRUE if condition is always satisfied, FALSE if never satisfied, UNKNOWN if indeterminate

    • isKnown

      boolean isKnown()
      Check if this value represents a known state (not TOP and not BOTTOM).

    • isBottom

      boolean isBottom()
      Check if this value represents an unreachable program point.

    • isKnownSet

      default boolean isKnownSet()
      Check if this value is known to represent a SET variable. Constants and range-constrained values are implicitly SET.
      Returns:
      true if the variable is provably SET, false otherwise

    • isImplicitlySetMorePrecise

      static boolean isImplicitlySetMorePrecise(AbstractValue value)
      True if the value is both implicitly SET and strictly more precise than a bare SET state, so that SET join <value> should keep this more precise value at a branch convergence.

      This is DELIBERATELY a narrower set than isKnownSet(): a LockIdentityValue is implicitly set, but a SET branch must NOT collapse to a specific lock identity at a join - that would claim the variable refers to that lock on a path where it may not, which would be unsound for deadlock detection. So lock identities resolve to TOP at such a join, not to the lock value. Single source for the rule that SetStateValue.join(AbstractValue) and CollectionStateValue.join(AbstractValue) previously hand-rolled (and could drift) independently.