Package org.checkerframework.checker.nullness

Class NullnessNoInitStore

java.lang.Object

org.checkerframework.framework.flow.CFAbstractStore<NullnessNoInitValue,NullnessNoInitStore>

org.checkerframework.checker.nullness.NullnessNoInitStore

All Implemented Interfaces:

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

public class NullnessNoInitStore
extends CFAbstractStore<NullnessNoInitValue,NullnessNoInitStore>

In addition to the base class behavior, tracks whether PolyNull is known to be NonNull or Nullable (or not known to be either).

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 Map<FieldAccess,NullnessNoInitValue>	initializedFields	Initialized fields and their values.
protected boolean	isPolyNullNonNull	True if, at this point, PolyNull is known to be NonNull.
protected boolean	isPolyNullNull	True if, at this point, PolyNull is known to be Nullable.

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

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

Constructor Summary

Constructors

Constructor	Description
NullnessNoInitStore(NullnessNoInitStore s)	Create a NullnessStore (copy constructor).
NullnessNoInitStore(CFAbstractAnalysis<NullnessNoInitValue,NullnessNoInitStore,?> analysis, boolean sequentialSemantics)	Create a NullnessStore.

Method Summary

Modifier and Type	Method	Description
protected String	internalVisualize(CFGVisualizer<NullnessNoInitValue,NullnessNoInitStore,?> viz)	Adds a representation of the internal information of this Store to visualizer viz.
boolean	isPolyNullNonNull()	Returns true if, at this point, PolyNull is known to be NonNull.
boolean	isPolyNullNull()	Returns true if, at this point, PolyNull is known to be Nullable.
NullnessNoInitStore	leastUpperBound(NullnessNoInitStore other)	Compute the least upper bound of two stores.
protected NullnessNoInitValue	newFieldValueAfterMethodCall(FieldAccess fieldAccess, GenericAnnotatedTypeFactory<NullnessNoInitValue,NullnessNoInitStore,?,?> atypeFactory, NullnessNoInitValue value)	Returns the new value of a field after a method call, or null if the field should be removed from the store.
void	setPolyNullNonNull(boolean isPolyNullNonNull)	Set the value of whether, at this point, PolyNull is known to be NonNull.
void	setPolyNullNull(boolean isPolyNullNull)	Set the value of whether, at this point, PolyNull is known to be Nullable.
protected boolean	supersetOf(CFAbstractStore<NullnessNoInitValue,NullnessNoInitStore> 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, insertValue, insertValuePermitNondeterministic, insertValuePermitNondeterministic, isMonotonicUpdate, 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 Details

isPolyNullNonNull

protected boolean isPolyNullNonNull

True if, at this point, PolyNull is known to be NonNull.

isPolyNullNull

protected boolean isPolyNullNull

True if, at this point, PolyNull is known to be Nullable.

initializedFields

protected Map<FieldAccess,NullnessNoInitValue> initializedFields

Initialized fields and their values.

This is used by newFieldValueAfterMethodCall(FieldAccess, GenericAnnotatedTypeFactory, NullnessNoInitValue) as cache to avoid performance issue in #1438.

See Also:

• InitializationAnnotatedTypeFactory.isInitialized(org.checkerframework.framework.type.GenericAnnotatedTypeFactory, org.checkerframework.framework.flow.CFAbstractValue, javax.lang.model.element.VariableElement)

Constructor Details

NullnessNoInitStore

public NullnessNoInitStore(CFAbstractAnalysis<NullnessNoInitValue,NullnessNoInitStore,?> analysis,
 boolean sequentialSemantics)

Create a NullnessStore.

Parameters:

analysis - the analysis class this store belongs to

sequentialSemantics - should the analysis use sequential Java semantics (i.e., assume that only one thread is running at all times)?

NullnessNoInitStore

public NullnessNoInitStore(NullnessNoInitStore s)

Create a NullnessStore (copy constructor).

Parameters:

s - a store to copy

Method Details

newFieldValueAfterMethodCall

protected NullnessNoInitValue newFieldValueAfterMethodCall(FieldAccess fieldAccess,
 GenericAnnotatedTypeFactory<NullnessNoInitValue,NullnessNoInitStore,?,?> atypeFactory,
 NullnessNoInitValue 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<NullnessNoInitValue,NullnessNoInitStore>

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

leastUpperBound

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

Overrides:

leastUpperBound in class CFAbstractStore<NullnessNoInitValue,NullnessNoInitStore>

supersetOf

protected boolean supersetOf(CFAbstractStore<NullnessNoInitValue,NullnessNoInitStore> 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<NullnessNoInitValue,NullnessNoInitStore>

internalVisualize

protected String internalVisualize(CFGVisualizer<NullnessNoInitValue,NullnessNoInitStore,?> viz)

Description copied from class: CFAbstractStore

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

Overrides:

internalVisualize in class CFAbstractStore<NullnessNoInitValue,NullnessNoInitStore>

Parameters:

viz - the visualizer

Returns:

a representation of the internal information of this Store

isPolyNullNonNull

public boolean isPolyNullNonNull()

Returns true if, at this point, PolyNull is known to be NonNull.

Returns:

true if, at this point, PolyNull is known to be NonNull

setPolyNullNonNull

public void setPolyNullNonNull(boolean isPolyNullNonNull)

Set the value of whether, at this point, PolyNull is known to be NonNull.

Parameters:

isPolyNullNonNull - whether, at this point, PolyNull is known to be NonNull

isPolyNullNull

public boolean isPolyNullNull()

Returns true if, at this point, PolyNull is known to be Nullable.

Returns:

true if, at this point, PolyNull is known to be Nullable

setPolyNullNull

public void setPolyNullNull(boolean isPolyNullNull)

Set the value of whether, at this point, PolyNull is known to be Nullable.

Parameters:

isPolyNullNull - whether, at this point, PolyNull is known to be Nullable