org.checkerframework.checker.lock

Class LockStore

java.lang.Object

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

org.checkerframework.checker.lock.LockStore

All Implemented Interfaces:

Store<LockStore>

public class LockStore
extends CFAbstractStore<CFValue,LockStore>

The Lock Store behaves like CFAbstractStore but requires the ability to insert exact annotations. This is because we want to be able to insert @LockPossiblyHeld to replace @LockHeld, which normally is not possible in CFAbstractStore since @LockHeld is more specific.

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 boolean	inConstructorOrInitializer If true, indicates that the store refers to a point in the code inside a constructor or initializer.

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

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

Constructor Summary

Constructors

Constructor and Description
LockStore(LockAnalysis analysis, boolean sequentialSemantics)
LockStore(LockAnalysis analysis, CFAbstractStore<CFValue,LockStore> other) Copy constructor.

Method Summary

Modifier and Type	Method and Description
@Nullable CFValue	getValue(FlowExpressions.Receiver expr) Returns current abstract value of a flow expression, or null if no information is available.
void	insertLockPossiblyHeld(FlowExpressions.Receiver r)
void	insertValue(FlowExpressions.Receiver r, @Nullable CFValue 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 String	internalVisualize(CFGVisualizer<CFValue,LockStore,?> viz) Adds a representation of the internal information of this Store to visualizer viz.
protected boolean	isSideEffectFree(AnnotatedTypeFactory atypeFactory, ExecutableElement method)
LockStore	leastUpperBound(LockStore other) Compute the least upper bound of two stores.
void	setInConstructorOrInitializer()
void	updateForMethodCall(MethodInvocationNode n, AnnotatedTypeFactory atypeFactory, CFValue 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, getValue, getValue, getValue, getValue, getValue, hashCode, initializeMethodParameter, initializeThisValue, insertOrRefine, insertThisValue, insertValue, isMonotonicUpdate, removeConflicting, removeConflicting, removeConflicting, replaceValue, supersetOf, toString, updateForArrayAssignment, updateForAssignment, updateForFieldAccessAssignment, updateForLocalVariableAssignment, visualize, widenedUpperBound

Methods inherited from class java.lang.Object

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

Field Detail

inConstructorOrInitializer

protected boolean inConstructorOrInitializer

If true, indicates that the store refers to a point in the code inside a constructor or initializer. This is useful because constructors and initializers are special with regard to the set of locks that is considered to be held. For example, 'this' is considered to be held inside a constructor.

Constructor Detail

LockStore

public LockStore(LockAnalysis analysis,
                 boolean sequentialSemantics)

LockStore

public LockStore(LockAnalysis analysis,
                 CFAbstractStore<CFValue,LockStore> other)

Copy constructor.

Method Detail

leastUpperBound

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

Overrides:

leastUpperBound in class CFAbstractStore<CFValue,LockStore>

insertLockPossiblyHeld

public void insertLockPossiblyHeld(FlowExpressions.Receiver r)

setInConstructorOrInitializer

public void setInConstructorOrInitializer()

getValue

public @Nullable CFValue getValue(FlowExpressions.Receiver expr)

Description copied from class: CFAbstractStore

Returns current abstract value of a flow expression, or null if no information is available.

Overrides:

getValue in class CFAbstractStore<CFValue,LockStore>

Returns:

current abstract value of a flow expression, or null if no information is available

internalVisualize

protected String internalVisualize(CFGVisualizer<CFValue,LockStore,?> 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,LockStore>

Returns:

a representation of the internal information of this Store

isSideEffectFree

protected boolean isSideEffectFree(AnnotatedTypeFactory atypeFactory,
                                   ExecutableElement method)

Overrides:

isSideEffectFree in class CFAbstractStore<CFValue,LockStore>

updateForMethodCall

public void updateForMethodCall(MethodInvocationNode n,
                                AnnotatedTypeFactory atypeFactory,
                                CFValue val)

Description copied from class: CFAbstractStore

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.

Overrides:

updateForMethodCall in class CFAbstractStore<CFValue,LockStore>

insertValue

public void insertValue(FlowExpressions.Receiver r,
                        @Nullable CFValue value)

Description copied from class: CFAbstractStore

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.

Overrides:

insertValue in class CFAbstractStore<CFValue,LockStore>