Package 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>, org.plumelib.util.UniqueId

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	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	Description
LockStore(LockAnalysis analysis, boolean sequentialSemantics)	Create a LockStore.
LockStore(LockAnalysis analysis, CFAbstractStore<CFValue,LockStore> other)	Copy constructor.

Method Summary

Modifier and Type	Method	Description
@Nullable CFValue	getValue(JavaExpression expr)	Returns the current abstract value of a Java expression, or null if no information is available.
void	insertLockPossiblyHeld(JavaExpression je)
void	insertValue(JavaExpression je, @Nullable 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,LockStore,?> viz)	Adds a representation of the internal information of this Store to visualizer viz.
LockStore	leastUpperBound(LockStore other)	Compute the least upper bound of two stores.
void	setInConstructorOrInitializer()
void	updateForMethodCall(MethodInvocationNode n, GenericAnnotatedTypeFactory<CFValue,LockStore,?,?> 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, canInsertJavaExpression, clearValue, computeNewValueAndInsert, copy, equals, getFieldValue, getFieldValues, getUid, getValue, getValue, getValue, getValue, getValue, hashCode, initializeMethodParameter, initializeThisValue, insertOrRefine, insertOrRefine, insertOrRefinePermitNondeterministic, insertThisValue, insertValue, insertValue, insertValuePermitNondeterministic, insertValuePermitNondeterministic, isMonotonicUpdate, isSideEffectFree, newFieldValueAfterMethodCall, newMonotonicFieldValueAfterMethodCall, removeConflicting, removeConflicting, removeConflicting, replaceValue, shouldInsert, supersetOf, toString, updateForArrayAssignment, updateForAssignment, updateForFieldAccessAssignment, updateForLocalVariableAssignment, 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

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)

Create a LockStore.

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

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(JavaExpression je)

setInConstructorOrInitializer

public void setInConstructorOrInitializer()

getValue

public @Nullable CFValue getValue(JavaExpression expr)

Description copied from class: CFAbstractStore

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

Overrides:

getValue in class CFAbstractStore<CFValue,LockStore>

Returns:

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

internalVisualize

protected java.lang.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>

Parameters:

viz - the visualizer

Returns:

a representation of the internal information of this Store

updateForMethodCall

public void updateForMethodCall(MethodInvocationNode n,
                                GenericAnnotatedTypeFactory<CFValue,LockStore,?,?> 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. This holds if a is a local variable or this, and f is final, or if a.f has a MonotonicQualifier in the current store. Subclasses can change this behavior by overriding CFAbstractStore.newFieldValueAfterMethodCall(FieldAccess, GenericAnnotatedTypeFactory, CFAbstractValue).
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>

Parameters:

n - method whose information is being updated

atypeFactory - the type factory of the associated checker

val - abstract value of the method call

insertValue

public void insertValue(JavaExpression je,
                        @Nullable CFValue value,
                        boolean permitNondeterministic)

Description copied from class: CFAbstractStore

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

Overrides:

insertValue in class CFAbstractStore<CFValue,LockStore>

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