| package org.checkerframework.checker.lock; |
| |
| import com.sun.source.tree.ClassTree; |
| import com.sun.source.tree.MethodTree; |
| import java.util.List; |
| import javax.lang.model.element.ElementKind; |
| import javax.lang.model.element.ExecutableElement; |
| import javax.lang.model.element.Modifier; |
| import javax.lang.model.type.TypeMirror; |
| import org.checkerframework.dataflow.analysis.TransferInput; |
| import org.checkerframework.dataflow.analysis.TransferResult; |
| import org.checkerframework.dataflow.cfg.UnderlyingAST; |
| import org.checkerframework.dataflow.cfg.UnderlyingAST.CFGMethod; |
| import org.checkerframework.dataflow.cfg.UnderlyingAST.Kind; |
| import org.checkerframework.dataflow.cfg.node.LocalVariableNode; |
| import org.checkerframework.dataflow.cfg.node.Node; |
| import org.checkerframework.dataflow.cfg.node.SynchronizedNode; |
| import org.checkerframework.dataflow.expression.ClassName; |
| import org.checkerframework.dataflow.expression.JavaExpression; |
| import org.checkerframework.framework.flow.CFAbstractTransfer; |
| import org.checkerframework.framework.flow.CFValue; |
| import org.checkerframework.javacutil.TreeUtils; |
| |
| /** |
| * LockTransfer handles constructors, initializers, synchronized methods, and synchronized blocks. |
| */ |
| public class LockTransfer extends CFAbstractTransfer<CFValue, LockStore, LockTransfer> { |
| /** The type factory associated with this transfer function. */ |
| private final LockAnnotatedTypeFactory atypeFactory; |
| |
| /** |
| * Create a transfer function for the Lock Checker. |
| * |
| * @param analysis the analysis this transfer function belongs to |
| * @param checker the type-checker this transfer function belongs to |
| */ |
| public LockTransfer(LockAnalysis analysis, LockChecker checker) { |
| // Always run the Lock Checker with -AconcurrentSemantics turned on. |
| super(analysis, /*useConcurrentSemantics=*/ true); |
| this.atypeFactory = (LockAnnotatedTypeFactory) analysis.getTypeFactory(); |
| } |
| |
| /** |
| * Sets a given {@link Node} to @LockHeld in the given {@code store}. |
| * |
| * @param store the store to update |
| * @param node the node that should be @LockHeld |
| */ |
| protected void makeLockHeld(LockStore store, Node node) { |
| JavaExpression internalRepr = JavaExpression.fromNode(node); |
| store.insertValue(internalRepr, atypeFactory.LOCKHELD); |
| } |
| |
| /** |
| * Sets a given {@link Node} to @LockPossiblyHeld in the given {@code store}. |
| * |
| * @param store the store to update |
| * @param node the node that should be @LockPossiblyHeld |
| */ |
| protected void makeLockPossiblyHeld(LockStore store, Node node) { |
| JavaExpression internalRepr = JavaExpression.fromNode(node); |
| |
| // insertValue cannot change an annotation to a less specific type (e.g. LockHeld to |
| // LockPossiblyHeld), so insertLockPossiblyHeld is called. |
| store.insertLockPossiblyHeld(internalRepr); |
| } |
| |
| /** Sets a given {@link Node} {@code node} to LockHeld in the given {@link TransferResult}. */ |
| protected void makeLockHeld(TransferResult<CFValue, LockStore> result, Node node) { |
| if (result.containsTwoStores()) { |
| makeLockHeld(result.getThenStore(), node); |
| makeLockHeld(result.getElseStore(), node); |
| } else { |
| makeLockHeld(result.getRegularStore(), node); |
| } |
| } |
| |
| /** |
| * Sets a given {@link Node} {@code node} to LockPossiblyHeld in the given {@link TransferResult}. |
| */ |
| protected void makeLockPossiblyHeld(TransferResult<CFValue, LockStore> result, Node node) { |
| if (result.containsTwoStores()) { |
| makeLockPossiblyHeld(result.getThenStore(), node); |
| makeLockPossiblyHeld(result.getElseStore(), node); |
| } else { |
| makeLockPossiblyHeld(result.getRegularStore(), node); |
| } |
| } |
| |
| @Override |
| public LockStore initialStore(UnderlyingAST underlyingAST, List<LocalVariableNode> parameters) { |
| |
| LockStore store = super.initialStore(underlyingAST, parameters); |
| |
| Kind astKind = underlyingAST.getKind(); |
| |
| // Methods with the 'synchronized' modifier are holding the 'this' lock. |
| |
| // There is a subtle difference between synchronized methods and constructors/initializers. A |
| // synchronized method is only taking the intrinsic lock of the current object. It says nothing |
| // about any fields of the current object. |
| |
| // Furthermore, since the current object already exists, other objects may be guarded by the |
| // current object. So a synchronized method can affect the locking behavior of other objects. |
| |
| // A constructor/initializer behaves as if the current object and all its non-static fields were |
| // held as locks. But in reality no locks are held. |
| |
| // Furthermore, since the current object is being constructed, no other object can be guarded by |
| // it or any of its non-static fields. |
| |
| // Handle synchronized methods and constructors. |
| if (astKind == Kind.METHOD) { |
| CFGMethod method = (CFGMethod) underlyingAST; |
| MethodTree methodTree = method.getMethod(); |
| |
| ExecutableElement methodElement = TreeUtils.elementFromDeclaration(methodTree); |
| |
| if (methodElement.getModifiers().contains(Modifier.SYNCHRONIZED)) { |
| final ClassTree classTree = method.getClassTree(); |
| TypeMirror classType = TreeUtils.typeOf(classTree); |
| |
| if (methodElement.getModifiers().contains(Modifier.STATIC)) { |
| store.insertValue(new ClassName(classType), atypeFactory.LOCKHELD); |
| } else { |
| store.insertThisValue(atypeFactory.LOCKHELD, classType); |
| } |
| } else if (methodElement.getKind() == ElementKind.CONSTRUCTOR) { |
| store.setInConstructorOrInitializer(); |
| } |
| } else if (astKind == Kind.ARBITRARY_CODE) { // Handle initializers |
| store.setInConstructorOrInitializer(); |
| } |
| |
| return store; |
| } |
| |
| @Override |
| public TransferResult<CFValue, LockStore> visitSynchronized( |
| SynchronizedNode n, TransferInput<CFValue, LockStore> p) { |
| |
| TransferResult<CFValue, LockStore> result = super.visitSynchronized(n, p); |
| |
| // Handle the entering and leaving of the synchronized block |
| if (n.getIsStartOfBlock()) { |
| makeLockHeld(result, n.getExpression()); |
| } else { |
| makeLockPossiblyHeld(result, n.getExpression()); |
| } |
| |
| return result; |
| } |
| } |