Infer purity when using the Lock Checker

checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java

@@ -130,16 +130,6 @@ public class LockAnnotatedTypeFactory
   public LockAnnotatedTypeFactory(BaseTypeChecker checker) {
     super(checker, true);
 
-    // This alias is only true for the Lock Checker. All other checkers must
-    // ignore the @LockingFree annotation.
-    addAliasedDeclAnnotation(LockingFree.class, SideEffectFree.class, SIDEEFFECTFREE);
-
-    // This alias is only true for the Lock Checker. All other checkers must
-    // ignore the @ReleasesNoLocks annotation.  Note that ReleasesNoLocks is
-    // not truly side-effect-free even as far as the Lock Checker is concerned,
-    // so there is additional handling of this annotation in the Lock Checker.
-    addAliasedDeclAnnotation(ReleasesNoLocks.class, SideEffectFree.class, SIDEEFFECTFREE);
-
     jcipGuardedBy = classForNameOrNull("net.jcip.annotations.GuardedBy");
 
     javaxGuardedBy = classForNameOrNull("javax.annotation.concurrent.GuardedBy");
@@ -767,4 +757,12 @@ private AnnotationMirror createGuardedByAnnotationMirror(List<String> values) {
     // Return the resulting AnnotationMirror
     return builder.build();
   }
+
+  @Override
+  public boolean isSideEffectFree(ExecutableElement method) {
+    SideEffectAnnotation seAnno = methodSideEffectAnnotation(method, false);
+    return seAnno == SideEffectAnnotation.RELEASESNOLOCKS
+        || seAnno == SideEffectAnnotation.LOCKINGFREE
+        || super.isSideEffectFree(method);
+  }
 }

checker/src/main/java/org/checkerframework/checker/lock/LockStore.java

@@ -4,7 +4,6 @@
 import java.util.Set;
 import javax.lang.model.element.AnnotationMirror;
 import javax.lang.model.element.ExecutableElement;
-import org.checkerframework.checker.lock.LockAnnotatedTypeFactory.SideEffectAnnotation;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.dataflow.cfg.node.MethodInvocationNode;
 import org.checkerframework.dataflow.cfg.visualize.CFGVisualizer;
@@ -17,7 +16,6 @@
 import org.checkerframework.dataflow.expression.ThisReference;
 import org.checkerframework.framework.flow.CFAbstractStore;
 import org.checkerframework.framework.flow.CFValue;
-import org.checkerframework.framework.source.SourceChecker;
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.QualifierHierarchy;
 import org.checkerframework.javacutil.AnnotationUtils;
@@ -168,17 +166,6 @@ protected String internalVisualize(CFGVisualizer<CFValue, LockStore, ?> viz) {
         + super.internalVisualize(viz);
   }
 
-  @Override
-  protected boolean isSideEffectFree(AnnotatedTypeFactory atypeFactory, ExecutableElement method) {
-    LockAnnotatedTypeFactory lockAnnotatedTypeFactory = (LockAnnotatedTypeFactory) atypeFactory;
-    SourceChecker checker = lockAnnotatedTypeFactory.getChecker();
-    return checker.hasOption("assumeSideEffectFree")
-        || checker.hasOption("assumePure")
-        || lockAnnotatedTypeFactory.methodSideEffectAnnotation(method, false)
-            == SideEffectAnnotation.RELEASESNOLOCKS
-        || super.isSideEffectFree(atypeFactory, method);
-  }
-
   @Override
   public void updateForMethodCall(
       MethodInvocationNode n, AnnotatedTypeFactory atypeFactory, CFValue val) {
@@ -187,7 +174,7 @@ public void updateForMethodCall(
     // The following behavior is similar to setting the sideEffectsUnrefineAliases field of
     // Lockannotatedtypefactory, but it affects only the LockPosssiblyHeld type hierarchy (not the
     // @GuardedBy hierarchy), so it cannot use that logic.
-    if (!isSideEffectFree(atypeFactory, method)) {
+    if (!atypeFactory.isSideEffectFree(method)) {
       // After the call to super.updateForMethodCall, only final fields are left in fieldValues (if
       // the method called is side-effecting). For the LockPossiblyHeld hierarchy, even a final
       // field might be locked or unlocked by a side-effecting method.  So, final fields must be set

checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java

@@ -86,16 +86,6 @@ public class LockVisitor extends BaseTypeVisitor<LockAnnotatedTypeFactory> {
    */
   public LockVisitor(BaseTypeChecker checker) {
     super(checker);
-    for (String checkerName : atypeFactory.getCheckerNames()) {
-      if (!(checkerName.equals("lock")
-          || checkerName.equals("LockChecker")
-          || checkerName.equals("org.checkerframework.checker.lock.LockChecker"))) {
-        // The Lock Checker redefines CFAbstractStore#isSideEffectFree in a way that is incompatible
-        // with (semantically different than) other checkers.
-        inferPurity = false;
-        break;
-      }
-    }
   }
 
   @Override

dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java

@@ -77,10 +77,16 @@ public static boolean isDeterministic(
   /**
    * Is the method {@code methodTree} side-effect-free?
    *
+   * <p>This method does not use, and has different semantics than, {@link
+   * AnnotationProvider#isSideEffectFree}. This method is concerned only with standard purity
+   * annotations.
+   *
    * @param provider how to get annotations
    * @param methodTree a method to test
    * @return whether the method is side-effect-free
+   * @deprecated use {@link AnnotationProvider#isSideEffectFree}
    */
+  @Deprecated // 2022-09-27
   public static boolean isSideEffectFree(AnnotationProvider provider, MethodTree methodTree) {
     ExecutableElement methodElement = TreeUtils.elementFromDeclaration(methodTree);
     if (methodElement == null) {
@@ -92,6 +98,10 @@ public static boolean isSideEffectFree(AnnotationProvider provider, MethodTree m
   /**
    * Is the method {@code methodElement} side-effect-free?
    *
+   * <p>This method does not use, and has different semantics than, {@link
+   * AnnotationProvider#isSideEffectFree}. This method is concerned only with standard purity
+   * annotations.
+   *
    * @param provider how to get annotations
    * @param methodElement a method to test
    * @return whether the method is side-effect-free

docs/CHANGELOG.md

@@ -15,12 +15,20 @@ introduced since JDK 11).
 
 Deprecated `TreeUtils.constructor()` in favor of `TreeUtils.elementFromUse()`.
 
+Added method `isSideEffectFree()` to the `AnnotationProvider` interface.
+
+Deprecated `CFAbstractStore.isSideEffectFree()` in favor of new method
+`AnnotationProvider.isSideEffectFree()`.  Note the different contracts of
+`PurityUtils.isSideEffectFree()` and `AnnotationProvider.isSideEffectFree()`.
+
 Use `TreeUtils.elementFromDeclaration` and `TreeUtils.elementFromUse` in
 preference to `TreeUtils.elementFromTree`, when possible.
 
 For code formatting, use `./gradlew spotlessCheck` and `./gradlew spotlessApply`.
 The `checkFormat` and `reformat` Gradle tasks have been removed.
 
+Removed variable `BaseTypeVisitor.inferPurity`.
+
 **Closed issues:**
 
 

framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java

@@ -230,12 +230,6 @@ public class BaseTypeVisitor<Factory extends GenericAnnotatedTypeFactory<?, ?, ?
    * command line.
    */
   private final boolean checkPurity;
-  /**
-   * True if purity annotations should be inferred. Should be set to false if both the Lock Checker
-   * (or some other checker that overrides {@link CFAbstractStore#isSideEffectFree} in a
-   * non-standard way) and some other checker is being run.
-   */
-  protected boolean inferPurity = true;
 
   /** The tree of the enclosing method that is currently being visited. */
   protected @Nullable MethodTree methodTree = null;
@@ -1007,7 +1001,7 @@ protected void checkPurity(MethodTree node) {
     if (suggestPureMethods && !TreeUtils.isSynthetic(node)) {
       // Issue a warning if the method is pure, but not annotated as such.
       EnumSet<Pure.Kind> additionalKinds = r.getKinds().clone();
-      if (!(infer && inferPurity)) {
+      if (!infer) {
         // During WPI, propagate all purity kinds, even those that are already
         // present (because they were inferred in a previous WPI round).
         additionalKinds.removeAll(kinds);
@@ -1017,18 +1011,16 @@ protected void checkPurity(MethodTree node) {
       }
       if (!additionalKinds.isEmpty()) {
         if (infer) {
-          if (inferPurity) {
-            WholeProgramInference wpi = atypeFactory.getWholeProgramInference();
-            ExecutableElement methodElt = TreeUtils.elementFromDeclaration(node);
-            if (additionalKinds.size() == 2) {
-              wpi.addMethodDeclarationAnnotation(methodElt, PURE);
-            } else if (additionalKinds.contains(Pure.Kind.SIDE_EFFECT_FREE)) {
-              wpi.addMethodDeclarationAnnotation(methodElt, SIDE_EFFECT_FREE);
-            } else if (additionalKinds.contains(Pure.Kind.DETERMINISTIC)) {
-              wpi.addMethodDeclarationAnnotation(methodElt, DETERMINISTIC);
-            } else {
-              throw new BugInCF("Unexpected purity kind in " + additionalKinds);
-            }
+          WholeProgramInference wpi = atypeFactory.getWholeProgramInference();
+          ExecutableElement methodElt = TreeUtils.elementFromDeclaration(node);
+          if (additionalKinds.size() == 2) {
+            wpi.addMethodDeclarationAnnotation(methodElt, PURE);
+          } else if (additionalKinds.contains(Pure.Kind.SIDE_EFFECT_FREE)) {
+            wpi.addMethodDeclarationAnnotation(methodElt, SIDE_EFFECT_FREE);
+          } else if (additionalKinds.contains(Pure.Kind.DETERMINISTIC)) {
+            wpi.addMethodDeclarationAnnotation(methodElt, DETERMINISTIC);
+          } else {
+            throw new BugInCF("Unexpected purity kind in " + additionalKinds);
           }
         } else {
           if (additionalKinds.size() == 2) {

framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java

@@ -33,7 +33,6 @@
 import org.checkerframework.dataflow.expression.MethodCall;
 import org.checkerframework.dataflow.expression.ThisReference;
 import org.checkerframework.dataflow.qual.SideEffectFree;
-import org.checkerframework.dataflow.util.PurityUtils;
 import org.checkerframework.framework.qual.MonotonicQualifier;
 import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.GenericAnnotatedTypeFactory;
@@ -181,9 +180,11 @@ public void initializeThisValue(AnnotationMirror a, TypeMirror underlyingType) {
    * @param atypeFactory the type factory used to retrieve annotations on the method element
    * @param method the method element
    * @return whether the method is side-effect-free
+   * @deprecated use {@link org.checkerframework.javacutil.AnnotationProvider#isSideEffectFree}
    */
+  @Deprecated // 2022-09-27
   protected boolean isSideEffectFree(AnnotatedTypeFactory atypeFactory, ExecutableElement method) {
-    return PurityUtils.isSideEffectFree(atypeFactory, method);
+    return atypeFactory.isSideEffectFree(method);
   }
 
   /* --------------------------------------------------------- */
@@ -214,7 +215,7 @@ public void updateForMethodCall(
     // case 1: remove information if necessary
     if (!(analysis.checker.hasOption("assumeSideEffectFree")
         || analysis.checker.hasOption("assumePure")
-        || isSideEffectFree(atypeFactory, method))) {
+        || atypeFactory.isSideEffectFree(method))) {
 
       boolean sideEffectsUnrefineAliases =
           ((GenericAnnotatedTypeFactory) atypeFactory).sideEffectsUnrefineAliases;

framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java

@@ -336,6 +336,12 @@ public class AnnotatedTypeFactory implements AnnotationProvider {
   private SimpleAnnotatedTypeScanner<Void, Void> atmInitializer =
       new SimpleAnnotatedTypeScanner<>((type1, q) -> null);
 
+  /**
+   * True if all methods should be assumed to be @SideEffectFree, for the purposes of
+   * org.checkerframework.dataflow analysis.
+   */
+  private final boolean assumeSideEffectFree;
+
   /**
    * Initializes all fields of {@code type}.
    *
@@ -517,6 +523,9 @@ public AnnotatedTypeFactory(BaseTypeChecker checker) {
     this.processingEnv = checker.getProcessingEnvironment();
     // this.root = root;
     this.checker = checker;
+    this.assumeSideEffectFree =
+        checker.hasOption("assumeSideEffectFree") || checker.hasOption("assumePure");
+
     this.trees = Trees.instance(processingEnv);
     this.elements = processingEnv.getElementUtils();
     this.types = processingEnv.getTypeUtils();
@@ -5583,4 +5592,20 @@ public boolean isImmutable(TypeMirror type) {
     }
     return ImmutableTypes.isImmutable(TypeAnnotationUtils.unannotatedType(type).toString());
   }
+
+  @Override
+  public boolean isSideEffectFree(ExecutableElement methodElement) {
+    if (assumeSideEffectFree) {
+      return true;
+    }
+
+    for (AnnotationMirror anno : getDeclAnnotations(methodElement)) {
+      if (areSameByClass(anno, org.checkerframework.dataflow.qual.SideEffectFree.class)
+          || areSameByClass(anno, org.checkerframework.dataflow.qual.Pure.class)
+          || areSameByClass(anno, org.jmlspecs.annotation.Pure.class)) {
+        return true;
+      }
+    }
+    return false;
+  }
 }

javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java

@@ -4,6 +4,7 @@
 import java.lang.annotation.Annotation;
 import javax.lang.model.element.AnnotationMirror;
 import javax.lang.model.element.Element;
+import javax.lang.model.element.ExecutableElement;
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 // This class exists to break a circular dependency between the dataflow framework and
@@ -31,4 +32,16 @@ public interface AnnotationProvider {
    * @return the annotation on {@code tree} that has the class {@code target}, or null
    */
   @Nullable AnnotationMirror getAnnotationMirror(Tree tree, Class<? extends Annotation> target);
+
+  /**
+   * Returns true if the given method is side-effect-free according to this AnnotationProvider
+   * &mdash; that is, if a call to the given method does not undo flow-sensitive type refinement.
+   *
+   * <p>Note that this method takes account of this AnnotationProvider's semantics, whereas {@code
+   * org.checkerframework.dataflow.util.PurityUtils#isSideEffectFree} does not.
+   *
+   * @param methodElement a method
+   * @return true if a call to the method does not undo flow-sensitive type refinement
+   */
+  boolean isSideEffectFree(ExecutableElement methodElement);
 }

javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java

@@ -5,6 +5,7 @@
 import java.util.List;
 import javax.lang.model.element.AnnotationMirror;
 import javax.lang.model.element.Element;
+import javax.lang.model.element.ExecutableElement;
 import org.checkerframework.checker.nullness.qual.Nullable;
 
 /** An AnnotationProvider that is independent of any type hierarchy. */
@@ -19,7 +20,6 @@ public class BasicAnnotationProvider implements AnnotationProvider {
       Element elt, Class<? extends Annotation> anno) {
     List<? extends AnnotationMirror> annotationMirrors = elt.getAnnotationMirrors();
 
-    // Then look at the real annotations.
     for (AnnotationMirror am : annotationMirrors) {
       @SuppressWarnings("deprecation") // method intended for use by the hierarchy
       boolean found = AnnotationUtils.areSameByClass(am, anno);
@@ -41,4 +41,25 @@ public class BasicAnnotationProvider implements AnnotationProvider {
       Tree tree, Class<? extends Annotation> target) {
     return null;
   }
+
+  /**
+   * {@inheritDoc}
+   *
+   * <p>This implementation returns true if the {@code @SideEffectFree} annotation is present on the
+   * given method.
+   */
+  @Override
+  public boolean isSideEffectFree(ExecutableElement methodElement) {
+    List<? extends AnnotationMirror> annotationMirrors = methodElement.getAnnotationMirrors();
+
+    for (AnnotationMirror am : annotationMirrors) {
+      boolean found =
+          AnnotationUtils.areSameByName(am, "org.checkerframework.dataflow.qual.SideEffectFree");
+      if (found) {
+        return true;
+      }
+    }
+
+    return false;
+  }
 }