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 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(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 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) Indicates whether the given method is side-effect-free as far as the current store is concerned.
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, 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, 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)

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

isSideEffectFree

protected boolean isSideEffectFree(AnnotatedTypeFactory atypeFactory,
                                   ExecutableElement method)

Description copied from class: CFAbstractStore

Indicates whether the given method is side-effect-free as far as the current store is concerned. In some cases, a store for a checker allows for other mechanisms to specify whether a method is side-effect-free. For example, unannotated methods may be considered side-effect-free by default.

Overrides:

isSideEffectFree in class CFAbstractStore<CFValue,LockStore>

Parameters:

atypeFactory - the type factory used to retrieve annotations on the method element

method - the method element

Returns:

whether the method is side-effect-free

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(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