Interface AbstractValue

All Known Implementing Classes:
BottomValue, CollectionStateValue, ConstantValue, ExcludesConstantValue, LockIdentityValue, RangeValue, SetStateValue, SymbolicTermValue, TopValue
public sealed interface AbstractValue permits TopValue, BottomValue, ConstantValue, RangeValue, SetStateValue, ExcludesConstantValue, CollectionStateValue, LockIdentityValue, SymbolicTermValue
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.
    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. Every implementation delegates to LatticeJoin, THE join, so the result never depends on which of the two values is the receiver.

      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