Package org.checkerframework.checker.initialization

Class InitializationStore

java.lang.Object

org.checkerframework.framework.flow.CFAbstractStore<CFValue,InitializationStore>

org.checkerframework.checker.initialization.InitializationStore

All Implemented Interfaces:

Store<InitializationStore>, org.plumelib.util.UniqueId

public class InitializationStore
extends CFAbstractStore<CFValue,InitializationStore>

A store that extends CFAbstractStore and additionally tracks which fields of the 'self' reference have been initialized.

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	Description
protected java.util.Set<javax.lang.model.element.VariableElement>	initializedFields	The set 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	Description
InitializationStore(InitializationAnalysis analysis, boolean sequentialSemantics)	Creates a new InitializationStore.
InitializationStore(InitializationStore other)	A copy constructor.

Method Summary

Modifier and Type	Method	Description
void	addInitializedField(javax.lang.model.element.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).
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).
InitializationAnalysis	getAnalysis()	Returns the analysis associated with this store.
void	insertValue(JavaExpression je, CFValue value, boolean permitNondeterministic)	Helper method for CFAbstractStore.insertValue(JavaExpression, CFAbstractValue) and CFAbstractStore.insertValuePermitNondeterministic(org.checkerframework.dataflow.expression.JavaExpression, javax.lang.model.element.AnnotationMirror).
protected java.lang.String	internalVisualize(CFGVisualizer<CFValue,InitializationStore,?> viz)	Adds a representation of the internal information of this Store to visualizer viz.
protected boolean	isDeclaredInitialized(FieldAccess fieldAccess)	Determine whether the given field is declared as Initialized (taking into account viewpoint adaption for NotOnlyInitialized).
boolean	isFieldInitialized(javax.lang.model.element.Element f)	Is the field identified by the element f initialized?
InitializationStore	leastUpperBound(InitializationStore other)	Compute the least upper bound of two stores.
protected CFValue	newFieldValueAfterMethodCall(FieldAccess fieldAccess, GenericAnnotatedTypeFactory<CFValue,InitializationStore,?,?> atypeFactory, CFValue value)	Returns the new value of a field after a method call, or null if the field should be removed from the store.
protected boolean	supersetOf(CFAbstractStore<CFValue,InitializationStore> o)	Returns true iff this CFAbstractStore contains a superset of the map entries of the argument CFAbstractStore.

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

canAlias, canInsertJavaExpression, clearValue, computeNewValueAndInsert, copy, equals, getFieldValue, getFieldValues, getUid, getValue, getValue, getValue, getValue, getValue, getValue, hashCode, initializeMethodParameter, initializeThisValue, insertOrRefine, insertOrRefine, insertOrRefinePermitNondeterministic, insertThisValue, insertValue, insertValue, insertValuePermitNondeterministic, insertValuePermitNondeterministic, isMonotonicUpdate, isSideEffectFree, newMonotonicFieldValueAfterMethodCall, removeConflicting, removeConflicting, removeConflicting, replaceValue, shouldInsert, toString, updateForArrayAssignment, updateForAssignment, updateForFieldAccessAssignment, updateForLocalVariableAssignment, updateForMethodCall, visualize, widenedUpperBound

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.plumelib.util.UniqueId

getClassAndUid

Field Detail

initializedFields

protected final java.util.Set<javax.lang.model.element.VariableElement> initializedFields

The set of fields that are initialized.

Constructor Detail

InitializationStore

public InitializationStore(InitializationAnalysis 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(InitializationStore other)

A copy constructor.

Parameters:

other - the store to copy

Method Detail

insertValue

public void insertValue(JavaExpression je,
                        CFValue 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<CFValue,InitializationStore>

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

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(javax.lang.model.element.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(javax.lang.model.element.Element f)

Is the field identified by the element f initialized?

supersetOf

protected boolean supersetOf(CFAbstractStore<CFValue,InitializationStore> 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<CFValue,InitializationStore>

leastUpperBound

public InitializationStore leastUpperBound(InitializationStore 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<InitializationStore>

Overrides:

leastUpperBound in class CFAbstractStore<CFValue,InitializationStore>

newFieldValueAfterMethodCall

protected CFValue newFieldValueAfterMethodCall(FieldAccess fieldAccess,
                                               GenericAnnotatedTypeFactory<CFValue,InitializationStore,?,?> atypeFactory,
                                               CFValue value)

Description copied from class: CFAbstractStore

Returns the new value of a field after a method call, or null if the field should be removed from the store.

In this default implementation, the field's value is preserved if it is either unassignable (see FieldAccess.isUnassignableByOtherCode()) or has a monotonic qualifier (see CFAbstractStore.newMonotonicFieldValueAfterMethodCall(FieldAccess, GenericAnnotatedTypeFactory, CFAbstractValue)). Otherwise, it is removed from the store.

Overrides:

newFieldValueAfterMethodCall in class CFAbstractStore<CFValue,InitializationStore>

Parameters:

fieldAccess - the field whose value to update

atypeFactory - AnnotatedTypeFactory of the associated checker

value - the field's value before the method call

Returns:

the field's value after the method call, or null if the field should be removed from the store

isDeclaredInitialized

protected boolean isDeclaredInitialized(FieldAccess fieldAccess)

Determine whether the given field is declared as Initialized (taking into account viewpoint adaption for NotOnlyInitialized).

Parameters:

fieldAccess - the field to check

Returns:

whether the given field is declared as Initialized (taking into account viewpoint adaption for NotOnlyInitialized)

internalVisualize

protected java.lang.String internalVisualize(CFGVisualizer<CFValue,InitializationStore,?> viz)

Description copied from class: CFAbstractStore

Adds a representation of the internal information of this Store to visualizer viz.

Overrides:

internalVisualize in class CFAbstractStore<CFValue,InitializationStore>

Parameters:

viz - the visualizer

Returns:

a representation of the internal information of this Store

getAnalysis

public InitializationAnalysis getAnalysis()

Returns the analysis associated with this store.

Returns:

the analysis associated with this store