Class InitializationStore<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>>

java.lang.Object
org.checkerframework.framework.flow.CFAbstractStore<V,S>
org.checkerframework.checker.initialization.InitializationStore<V,S>
All Implemented Interfaces:
Store<S>, org.plumelib.util.UniqueId
Direct Known Subclasses:
NullnessStore

public class InitializationStore<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>> extends CFAbstractStore<V,S>
A store that extends CFAbstractStore and additionally tracks which fields of the 'self' reference have been initialized.
See Also:
  • Field Details

    • initializedFields

      protected final Set<VariableElement> initializedFields
      The set of fields that are initialized.
    • invariantFields

      protected final Map<FieldAccess,V extends CFAbstractValue<V>> invariantFields
      The set of fields that have the 'invariant' annotation, and their value.
  • Constructor Details

    • InitializationStore

      public InitializationStore(CFAbstractAnalysis<V,S,?> analysis, boolean sequentialSemantics)
      Creates a new InitializationStore.
      Parameters:
      analysis - the analysis class this store belongs to
      sequentialSemantics - should the analysis use sequential Java semantics?
    • InitializationStore

      public InitializationStore(S other)
      A copy constructor.
  • Method Details

    • insertValue

      public void insertValue(JavaExpression je, V value, boolean permitNondeterministic)
      Helper method for CFAbstractStore.insertValue(JavaExpression, CFAbstractValue) and CFAbstractStore.insertValuePermitNondeterministic(org.checkerframework.dataflow.expression.JavaExpression, javax.lang.model.element.AnnotationMirror).

      Every overriding implementation should start with

      
       if (!shouldInsert) {
         return;
       }
       

      If the receiver is a field, and has an invariant annotation, then it can be considered initialized.

      Overrides:
      insertValue in class CFAbstractStore<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>>
      Parameters:
      je - the expression to insert in the store
      value - the value of the expression
      permitNondeterministic - if false, does nothing if expr is nondeterministic; if true, permits nondeterministic expressions to be placed in the store
    • updateForMethodCall

      public void updateForMethodCall(MethodInvocationNode n, AnnotatedTypeFactory atypeFactory, V val)
      Remove any information that might not be valid any more after a method call, and add information guaranteed by the method.
      1. If the method is side-effect-free (as indicated by SideEffectFree or Pure), then no information needs to be removed.
      2. Otherwise, all information about field accesses a.f needs to be removed, except if the method n cannot modify a.f (e.g., if a is a local variable or this, and f is final).
      3. Furthermore, if the field has a monotonic annotation, then its information can also be kept.
      Furthermore, if the method is deterministic, we store its result val in the store.

      Additionally, the InitializationStore keeps all field values for fields that have the 'invariant' annotation.

      Overrides:
      updateForMethodCall in class CFAbstractStore<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>>
      Parameters:
      n - method whose information is being updated
      atypeFactory - the type factory of the associated checker
      val - abstract value of the method call
    • addInitializedField

      public void addInitializedField(FieldAccess field)
      Mark the field identified by the element field as initialized if it belongs to the current class, or is static (in which case there is no aliasing issue and we can just add all static fields).
      Parameters:
      field - a field that is initialized
    • addInitializedField

      public void addInitializedField(VariableElement f)
      Mark the field identified by the element f as initialized (the caller needs to ensure that the field belongs to the current class, or is a static field).
      Parameters:
      f - a field that is initialized
    • isFieldInitialized

      public boolean isFieldInitialized(Element f)
      Is the field identified by the element f initialized?
    • supersetOf

      protected boolean supersetOf(CFAbstractStore<V,S> o)
      Description copied from class: CFAbstractStore
      Returns true iff this CFAbstractStore contains a superset of the map entries of the argument CFAbstractStore. Note that we test the entry keys and values by Java equality, not by any subtype relationship. This method is used primarily to simplify the equals predicate.
      Overrides:
      supersetOf in class CFAbstractStore<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>>
    • leastUpperBound

      public S leastUpperBound(S other)
      Description copied from interface: Store
      Compute the least upper bound of two stores.

      Important: This method must fulfill the following contract:

      • Does not change this.
      • Does not change other.
      • Returns a fresh object which is not aliased yet.
      • Returns an object of the same (dynamic) type as this, even if the signature is more permissive.
      • Is commutative.
      Specified by:
      leastUpperBound in interface Store<V extends CFAbstractValue<V>>
      Overrides:
      leastUpperBound in class CFAbstractStore<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>>
    • internalVisualize

      protected String internalVisualize(CFGVisualizer<V,S,?> viz)
      Description copied from class: CFAbstractStore
      Adds a representation of the internal information of this Store to visualizer viz.
      Overrides:
      internalVisualize in class CFAbstractStore<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>>
      Parameters:
      viz - the visualizer
      Returns:
      a representation of the internal information of this Store
    • getAnalysis

      public CFAbstractAnalysis<V,S,?> getAnalysis()
      Returns the analysis associated with this store.
      Returns:
      the analysis associated with this store