CFAbstractStore

java.lang.Object
- org.checkerframework.framework.flow.CFAbstractStore<V,S>

All Implemented Interfaces:

Store<S>

Direct Known Subclasses:

CFStore, InitializationStore, LockStore
```
public abstract class CFAbstractStore<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>>
extends Object
implements Store<S>
```
A store for the checker framework analysis tracks the annotations of memory locations such as local variables and fields.

Author:

Charlie Garrett, Stefan Heule

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 CFAbstractAnalysis<V,S,?>`	`analysis` The analysis class this store belongs to.
`protected Map<FlowExpressions.ArrayAccess,V>`	`arrayValues` Information collected about arrays, using the internal representation `FlowExpressions.ArrayAccess`.
`protected Map<FlowExpressions.ClassName,V>`	`classValues`
`protected Map<FlowExpressions.FieldAccess,V>`	`fieldValues` Information collected about fields, using the internal representation `FlowExpressions.FieldAccess`.
`protected Map<FlowExpressions.LocalVariable,V>`	`localVariableValues` Information collected about local variables, which are identified by the corresponding element.
`protected Map<FlowExpressions.PureMethodCall,V>`	`methodValues` Information collected about pure method calls, using the internal representation `FlowExpressions.PureMethodCall`.
`protected boolean`	`sequentialSemantics` Should the analysis use sequential Java semantics (i.e., assume that only one thread is running at all times)?
`protected V`	`thisValue` Information collected about the current object.

Constructor Summary

Constructors
Modifier	Constructor and Description
	`CFAbstractStore(CFAbstractAnalysis<V,S,?> analysis, boolean sequentialSemantics)`
`protected`	`CFAbstractStore(CFAbstractStore<V,S> other)` Copy constructor.

Method Summary

All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`boolean`	`canAlias(FlowExpressions.Receiver a, FlowExpressions.Receiver b)` Can the objects `a` and `b` be aliases? Returns a conservative answer (i.e., returns `true` if not enough information is available to determine aliasing).
`static boolean`	`canInsertReceiver(FlowExpressions.Receiver r)` Returns true if the receiver `r` can be stored in this store.
`void`	`clearValue(FlowExpressions.Receiver r)` Remove any knowledge about the expression `r` (correctly deciding where to remove the information depending on the type of the expression `r`).
`S`	`copy()`
`boolean`	`equals(Object o)`
`protected String`	`escapeDoubleQuotes(String str)`
`V`	`getValue(ArrayAccessNode n)`
`V`	`getValue(FieldAccessNode n)`
`V`	`getValue(FlowExpressions.Receiver expr)`
`V`	`getValue(LocalVariableNode n)`
`V`	`getValue(MethodInvocationNode n)`
`V`	`getValue(ThisLiteralNode n)`
`boolean`	`hasDOToutput()`
`void`	`initializeMethodParameter(LocalVariableNode p, V value)` Set the abstract value of a method parameter (only adds the information to the store, does not remove any other knowledge).
`void`	`initializeThisValue(AnnotationMirror a, TypeMirror underlyingType)` Set the value of the current object.
`void`	`insertThisValue(AnnotationMirror a, TypeMirror underlyingType)`
`void`	`insertValue(FlowExpressions.Receiver r, AnnotationMirror a)` Add the annotation `a` for the expression `r` (correctly deciding where to store the information depending on the type of the expression `r`).
`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`.
`protected boolean`	`isSideEffectFree(AnnotatedTypeFactory atypeFactory, ExecutableElement method)`
`S`	`leastUpperBound(S other)` Compute the least upper bound of two stores.
`protected void`	`removeConflicting(FlowExpressions.ArrayAccess arrayAccess, V val)` Remove any information in the store that might not be true any more after `arrayAccess` has been assigned a new value (with the abstract value `val`).
`protected void`	`removeConflicting(FlowExpressions.FieldAccess fieldAccess, V val)` Remove any information in this store that might not be true any more after `fieldAccess` has been assigned a new value (with the abstract value `val`).
`protected void`	`removeConflicting(FlowExpressions.LocalVariable var)` Remove any information in this store that might not be true any more after `localVar` has been assigned a new value.
`void`	`replaceValue(FlowExpressions.Receiver r, V value)` Completely replaces the abstract value `value` for the expression `r` (correctly deciding where to store the information depending on the type of the expression `r`).
`protected boolean`	`supersetOf(CFAbstractStore<V,S> other)` Returns true iff this `CFAbstractStore` contains a superset of the map entries of the argument `CFAbstractStore`.
`String`	`toDOToutput()`
`String`	`toString()`
`protected String`	`toStringEscapeDoubleQuotes(Object obj)`
`protected void`	`updateForArrayAssignment(FlowExpressions.ArrayAccess arrayAccess, V val)` Update the information in the store by considering an assignment with target `n`, where the target is an array access.
`void`	`updateForAssignment(Node n, V val)` Update the information in the store by considering an assignment with target `n`.
`protected void`	`updateForFieldAccessAssignment(FlowExpressions.FieldAccess fieldAccess, V val)` Update the information in the store by considering a field assignment with target `n`, where the right hand side has the abstract value `val`.
`protected void`	`updateForLocalVariableAssignment(FlowExpressions.LocalVariable receiver, V val)` Set the abstract value of a local variable in the store.
`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 java.lang.Object
clone, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

- Field Detail
  - analysis
```
protected final CFAbstractAnalysis<V extends CFAbstractValue<V>,S extends CFAbstractStore<V,S>,?> analysis
```
    The analysis class this store belongs to.
  - localVariableValues
```
protected final Map<FlowExpressions.LocalVariable,V extends CFAbstractValue<V>> localVariableValues
```
    Information collected about local variables, which are identified by the corresponding element.
  - thisValue
```
protected V extends CFAbstractValue<V> thisValue
```
    Information collected about the current object.
  - fieldValues
```
protected Map<FlowExpressions.FieldAccess,V extends CFAbstractValue<V>> fieldValues
```
    Information collected about fields, using the internal representation FlowExpressions.FieldAccess.
  - arrayValues
```
protected Map<FlowExpressions.ArrayAccess,V extends CFAbstractValue<V>> arrayValues
```
    Information collected about arrays, using the internal representation FlowExpressions.ArrayAccess.
  - methodValues
```
protected Map<FlowExpressions.PureMethodCall,V extends CFAbstractValue<V>> methodValues
```
    Information collected about pure method calls, using the internal representation FlowExpressions.PureMethodCall.
  - classValues
```
protected Map<FlowExpressions.ClassName,V extends CFAbstractValue<V>> classValues
```
  - sequentialSemantics
```
protected final boolean sequentialSemantics
```
    Should the analysis use sequential Java semantics (i.e., assume that only one thread is running at all times)?
- Constructor Detail
  - CFAbstractStore
```
public CFAbstractStore(CFAbstractAnalysis<V,S,?> analysis,
                       boolean sequentialSemantics)
```
  - CFAbstractStore
```
protected CFAbstractStore(CFAbstractStore<V,S> other)
```
    Copy constructor.
- Method Detail
  - initializeMethodParameter
```
public void initializeMethodParameter(LocalVariableNode p,
                                      V value)
```
    Set the abstract value of a method parameter (only adds the information to the store, does not remove any other knowledge). Any previous information is erased; this method should only be used to initialize the abstract value.
  - initializeThisValue
```
public void initializeThisValue(AnnotationMirror a,
                                TypeMirror underlyingType)
```
    Set the value of the current object. Any previous information is erased; this method should only be used to initialize the value.
  - isSideEffectFree
```
protected boolean isSideEffectFree(AnnotatedTypeFactory atypeFactory,
                                   ExecutableElement method)
```
  - 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.
  - insertValue
```
public void insertValue(FlowExpressions.Receiver r,
                        AnnotationMirror a)
```
    Add the annotation a 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 other than as hierarchy, that information is preserved.
  - canInsertReceiver
```
public static boolean canInsertReceiver(FlowExpressions.Receiver r)
```
    Returns true if the receiver r can be stored in this store.
  - 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.
  - insertThisValue
```
public void insertThisValue(AnnotationMirror a,
                            TypeMirror underlyingType)
```
  - replaceValue
```
public void replaceValue(FlowExpressions.Receiver r,
                         V value)
```
    Completely replaces the abstract value value for the expression r (correctly deciding where to store the information depending on the type of the expression r). Any previous information is discarded.
    This method does not take care of removing other information that might be influenced by changes to certain parts of the state.
  - clearValue
```
public void clearValue(FlowExpressions.Receiver r)
```
    Remove any knowledge about the expression r (correctly deciding where to remove the information depending on the type of the expression r).
  - getValue
```
public V getValue(FlowExpressions.Receiver expr)
```
    Returns:
    
    Current abstract value of a flow expression, or null if no information is available.
  - getValue
```
public V getValue(FieldAccessNode n)
```
    Returns:
    
    Current abstract value of a field access, or null if no information is available.
  - getValue
```
public V getValue(MethodInvocationNode n)
```
    Returns:
    
    Current abstract value of a method call, or null if no information is available.
  - getValue
```
public V getValue(ArrayAccessNode n)
```
    Returns:
    
    Current abstract value of a field access, or null if no information is available.
  - updateForAssignment
```
public void updateForAssignment(Node n,
                                V val)
```
    Update the information in the store by considering an assignment with target n.
  - updateForFieldAccessAssignment
```
protected void updateForFieldAccessAssignment(FlowExpressions.FieldAccess fieldAccess,
                                              V val)
```
    Update the information in the store by considering a field assignment with target n, where the right hand side has the abstract value val.
    
    Parameters:
    
    val - The abstract value of the value assigned to n (or null if the abstract value is not known).
  - updateForArrayAssignment
```
protected void updateForArrayAssignment(FlowExpressions.ArrayAccess arrayAccess,
                                        V val)
```
    Update the information in the store by considering an assignment with target n, where the target is an array access.
    1. Remove any abstract values for field accesses b.g where n might alias any expression in the receiver b.
    2. Remove any information about pure method calls.
  - updateForLocalVariableAssignment
```
protected void updateForLocalVariableAssignment(FlowExpressions.LocalVariable receiver,
                                                V val)
```
    Set the abstract value of a local variable in the store. Overwrites any value that might have been available previously.
    
    Parameters:
    
    val - The abstract value of the value assigned to n (or null if the abstract value is not known).
  - removeConflicting
```
protected void removeConflicting(FlowExpressions.FieldAccess fieldAccess,
                                 V val)
```
    Remove any information in this store that might not be true any more after fieldAccess has been assigned a new value (with the abstract value val). This includes the following steps (assume that fieldAccess is of the form a.f for some a.
    1. Update the abstract value of other field accesses b.g where the field is equal (that is, f=g), and the receiver b might alias the receiver of fieldAccess, a. This update will raise the abstract value for such field accesses to at least val (or the old value, if that was less precise). However, this is only necessary if the field g is not final.
    2. Remove any abstract values for field accesses b.g where fieldAccess might alias any expression in the receiver b.
    3. Remove any information about pure method calls.
    4. Remove any abstract values an arrary access b[i] where fieldAccess might alias any expression in the receiver a or index i.
    Parameters:
    
    val - The abstract value of the value assigned to n (or null if the abstract value is not known).
  - removeConflicting
```
protected void removeConflicting(FlowExpressions.ArrayAccess arrayAccess,
                                 V val)
```
    Remove any information in the store that might not be true any more after arrayAccess has been assigned a new value (with the abstract value val). This includes the following steps (assume that arrayAccess is of the form a[i] for some a.
    1. Remove any abstract value for other array access b[j] where a and b can be aliases, or where either b or j contains a modifiable alias of a[i].
    2. Remove any abstract values for field accesses b.g where a[i] might alias any expression in the receiver b and there is an array expression somewhere in the receiver.
    3. Remove any information about pure method calls.
    Parameters:
    
    val - The abstract value of the value assigned to n (or null if the abstract value is not known).
  - removeConflicting
```
protected void removeConflicting(FlowExpressions.LocalVariable var)
```
    Remove any information in this store that might not be true any more after localVar has been assigned a new value. This includes the following steps:
    1. Remove any abstract values for field accesses b.g where localVar might alias any expression in the receiver b.
    2. Remove any abstract values for array accesses a[i] where localVar might alias the receiver a.
    3. Remove any information about pure method calls where the receiver or any of the parameters contains localVar.
  - canAlias
```
public boolean canAlias(FlowExpressions.Receiver a,
                        FlowExpressions.Receiver b)
```
    Can the objects a and b be aliases? Returns a conservative answer (i.e., returns true if not enough information is available to determine aliasing).
    
    Specified by:
    
    canAlias in interface Store<S extends CFAbstractStore<V,S>>
  - getValue
```
public V getValue(LocalVariableNode n)
```
    Returns:
    
    Current abstract value of a local variable, or null if no information is available.
  - getValue
```
public V getValue(ThisLiteralNode n)
```
    Returns:
    
    Current abstract value of the current object, or null if no information is available.
  - copy
```
public S copy()
```
    Specified by:
    
    copy in interface Store<S extends CFAbstractStore<V,S>>
    
    Returns:
    
    An exact copy of this store.
  - 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 CFAbstractStore<V,S>>
  - supersetOf
```
protected boolean supersetOf(CFAbstractStore<V,S> other)
```
    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.
  - equals
```
public boolean equals(Object o)
```
    Overrides:
    
    equals in class Object
  - toString
```
@SideEffectFree
public String toString()
```
    Overrides:
    
    toString in class Object
  - hasDOToutput
```
@Pure
public boolean hasDOToutput()
```
    Specified by:
    
    hasDOToutput in interface Store<S extends CFAbstractStore<V,S>>
    
    Returns:
    
    Whether the Store supports DOT graph output.
  - toDOToutput
```
public String toDOToutput()
```
    Specified by:
    
    toDOToutput in interface Store<S extends CFAbstractStore<V,S>>
    
    Returns:
    
    DOT representation of the store (may contain control characters such as "\n").
  - escapeDoubleQuotes
```
protected String escapeDoubleQuotes(String str)
```
  - toStringEscapeDoubleQuotes
```
protected String toStringEscapeDoubleQuotes(Object obj)
```
  - internalDotOutput
```
protected void internalDotOutput(StringBuilder result)
```
    Adds a DOT representation of the internal information of this store to result.

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

Nested Class Summary

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

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

analysis

localVariableValues

thisValue

fieldValues

arrayValues

methodValues

classValues

sequentialSemantics

Constructor Detail

CFAbstractStore

CFAbstractStore

Method Detail

initializeMethodParameter

initializeThisValue

isSideEffectFree

updateForMethodCall

insertValue

canInsertReceiver

insertValue

insertThisValue

replaceValue

clearValue

getValue

getValue

getValue

getValue

updateForAssignment

updateForFieldAccessAssignment

updateForArrayAssignment

updateForLocalVariableAssignment

removeConflicting

removeConflicting

removeConflicting

canAlias

getValue

getValue

copy

leastUpperBound

supersetOf

equals

toString

hasDOToutput

toDOToutput

escapeDoubleQuotes

toStringEscapeDoubleQuotes

internalDotOutput