Infer purity when using the Lock Checker (typetools#5343)

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");
@@ -768,4 +758,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,12 +174,11 @@ 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)) {
-      // 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 to @LockPossiblyHeld, but the annotation in the
-      // GuardedBy hierarchy should not be changed.
+    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
+      // to @LockPossiblyHeld, but the annotation in the GuardedBy hierarchy should not be changed.
       for (FieldAccess field : new ArrayList<>(fieldValues.keySet())) {
         CFValue newValue = changeLockAnnoToTop(field, fieldValues.get(field));
         if (newValue != null) {

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

@@ -18,12 +18,20 @@ performance; please increase max heap size" message from a warning to a note.
 
 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

@@ -236,12 +236,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;
@@ -1010,35 +1004,18 @@ protected void checkPurity(MethodTree node) {
       // Issue a warning if the method is pure, but not annotated as such.
       EnumSet<Pure.Kind> additionalKinds = r.getKinds().clone();
       /* NO-AFU
-             if (!(infer && inferPurity)) {
-                 // During WPI, propagate all purity kinds, even those that are already
-                 // present (because they were inferred in a previous WPI round).
+      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);
       /* NO-AFU
-             }
+      }
       */
       if (TreeUtils.isConstructor(node)) {
         additionalKinds.remove(Pure.Kind.DETERMINISTIC);
       }
       if (!additionalKinds.isEmpty()) {
-        /* NO-AFU
-                      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);
-                              }
-                          }
-                      } else {
-        */
         if (additionalKinds.size() == 2) {
           checker.reportWarning(node, "purity.more.pure", node.getName());
         } else if (additionalKinds.contains(Pure.Kind.SIDE_EFFECT_FREE)) {
@@ -1048,7 +1025,21 @@ protected void checkPurity(MethodTree node) {
         } else {
           throw new BugInCF("Unexpected purity kind in " + additionalKinds);
         }
-        // NO-AFU }
+        /* NO-AFU
+        if (infer) {
+          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);
+          }
+        }
+        */
       }
     }
   }

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

@@ -333,6 +333,12 @@ public class AnnotatedTypeFactory implements AnnotationProvider {
   private final 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}.
    *
@@ -523,6 +529,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();
@@ -5781,4 +5790,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;
+  }
 }