org.checkerframework.checker.initialization

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>

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.

Author:

Stefan Heule

See Also:

InitializationTransfer

Nested Class Summary

Nested classes/interfaces inherited from interface org.checkerframework.dataflow.analysis.Store

Store.FlowRule, Store.Kind

Field Summary

Fields

Modifier and Type	Field and Description
protected Set<VariableElement>	initializedFields The list of fields that are initialized.

Fields inherited from class org.checkerframework.framework.flow.CFAbstractStore

analysis, arrayValues, classValues, fieldValues, localVariableValues, methodValues, sequentialSemantics, thisValue

Constructor Summary

Constructors

Constructor and Description
InitializationStore(CFAbstractAnalysis<V,S,?> analysis, boolean sequentialSemantics)
InitializationStore(S other) A copy constructor.

Method Summary

Modifier and Type	Method and Description
void	addInitializedField(FlowExpressions.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).
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).
CFAbstractAnalysis<V,S,?>	getAnalysis()
Map<FlowExpressions.FieldAccess,V>	getFieldValues()
void	insertValue(FlowExpressions.Receiver r, V value) Add the abstract value value for the expression r (correctly deciding where to store the information depending on the type of the expression r).
protected void	internalDotOutput(StringBuilder result) Adds a DOT representation of the internal information of this store to result.
boolean	isFieldInitialized(Element f) Is the field identified by the element f initialized?
S	leastUpperBound(S other) Compute the least upper bound of two stores.
protected boolean	supersetOf(CFAbstractStore<V,S> o) Returns true iff this CFAbstractStore contains a superset of the map entries of the argument CFAbstractStore.
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.

Methods inherited from class org.checkerframework.framework.flow.CFAbstractStore

canAlias, canInsertReceiver, clearValue, copy, equals, escapeDoubleQuotes, getValue, getValue, getValue, getValue, getValue, getValue, hasDOToutput, initializeMethodParameter, initializeThisValue, insertThisValue, insertValue, isSideEffectFree, removeConflicting, removeConflicting, removeConflicting, replaceValue, toDOToutput, toString, toStringEscapeDoubleQuotes, updateForArrayAssignment, updateForAssignment, updateForFieldAccessAssignment, updateForLocalVariableAssignment

Methods inherited from class java.lang.Object

clone, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

initializedFields

protected final Set<VariableElement> initializedFields

The list of fields that are initialized.

Constructor Detail

InitializationStore

public InitializationStore(CFAbstractAnalysis<V,S,?> analysis,
                           boolean sequentialSemantics)

InitializationStore

public InitializationStore(S other)

A copy constructor.

Method Detail

insertValue

public void insertValue(FlowExpressions.Receiver r,
                        V value)

Add the abstract value value for the expression r (correctly deciding where to store the information depending on the type of the expression r).

This method does not take care of removing other information that might be influenced by changes to certain parts of the state.

If there is already a value v present for r, then the stronger of the new and old value are taken (according to the lattice). Note that this happens per hierarchy, and if the store already contains information about a hierarchy for which value does not contain information, then that information is preserved.

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

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

addInitializedField

public void addInitializedField(FlowExpressions.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).

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

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<S extends InitializationStore<V,S>>

Overrides:

leastUpperBound in class CFAbstractStore<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>>

internalDotOutput

protected void internalDotOutput(StringBuilder result)

Description copied from class: CFAbstractStore

Adds a DOT representation of the internal information of this store to result.

Overrides:

internalDotOutput in class CFAbstractStore<V extends CFAbstractValue<V>,S extends InitializationStore<V,S>>

getFieldValues

public Map<FlowExpressions.FieldAccess,V> getFieldValues()

getAnalysis

public CFAbstractAnalysis<V,S,?> getAnalysis()