Add support for suggesting Lock Checker annotations in the Purity Checker

In addition to @Pure and @SideEffectFree, the Lock Checker also makes use of three additional side effect annotations. In order of increasing strength of guarantee, these are the side effect annotations supported by the Lock Checker (this list is defined in LockAnnotatedTypeFactory.SideEffectAnnotation):

@MayReleaseLocks
@ReleasesNoLocks
@LockingFree
@SideEffectFree
@Pure

Purity suggestions

The Purity Checker (see org.checkerframework.dataflow.util.PurityChecker and BaseTypeVisitor.visitMethod) could be enhanced by suggesting these additional annotations.

• If a method is not synchronized, contains no synchronized blocks, and does not call any methods annotated with @ReleasesNoLocks, @MayReleaseLocks, @EnsuresLockHeld or @EnsuresLockHeldIf, it can be annotated with @LockingFree.

Note: methods that directly acquire explicit locks (such as ReentrantLock.lock()) must always be annotated with @EnsuresLockHeld or @EnsuresLockHeldIf. Methods that indirectly call such methods will not be annotated with @LockingFree (or a stronger annotation). Methods that directly release explicit locks, such as ReentrantLock.unlock(), must always be annotated with @MayReleaseLocks.

• If a method is not @LockingFree, but it does not call any methods annotated with @MayReleaseLocks, it is considered to be annotated with @ReleaseNoLocks. Note that in this case the Purity Checker does not need to issue a suggestion, since the Lock Checker considers an unannotated method as being annotated with @ReleasesNoLocks.
• If a method calls a method annotated with @MayReleaseLocks, the Purity Checker can suggest a @MayReleaseLocks annotation for it.

Purity checking

As for purity checking of existing Lock Checker annotations, it could be done by the Purity Checker as well, but this would result in overlap with the Lock Checker's existing behavior:

• In LockVisitor.visitMethodInvocation, a method.guarantee.violated warning is issued when a method is called that has a weaker side effect annotation than the method being visited.
• In LockVisitor.visitMethod, a lockingfree.synchronized.method warning is issued if a method annotated with @LockingFree (or a stronger annotation) is synchronized.
• In LockingVisitor.visitSynchronized, a synchronized.block.in.lockingfree.method warning is issued if a method annotated with @LockingFree (or a stronger annotation) contains a synchronized block.

A better approach might be to complete the Lock Checker's purity verification by issuing warnings when a method annotated with @EnsuresLockHeld or @EnsuresLockHeldIf is annotated with @LockingFree (or a stronger annotation).

Start with org.checkerframework.dataflow.util.PurityChecker and BaseTypeVisitor.visitMethod, then inspect LockAnnotatedTypeFactory.SideEffectAnnotation and the existing LockVisitor and LockingVisitor checks. Trace how method invocations, synchronized methods, and synchronized blocks are currently handled. Done means the Purity Checker suggests the applicable Lock Checker annotations and covers the proposed EnsuresLockHeld or EnsuresLockHeldIf purity warning without duplicating existing checks.