Purity annotations

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

@@ -510,14 +510,15 @@ public static SideEffectAnnotation weakest() {
   }
 
   /**
-   * Indicates which side effect annotation is present on the given method. If more than one
-   * annotation is present, this method issues an error (if issueErrorIfMoreThanOnePresent is true)
-   * and returns the annotation providing the weakest guarantee. Only call with
-   * issueErrorIfMoreThanOnePresent == true when visiting a method definition. This prevents
-   * multiple errors being issued for the same method (as would occur if
-   * issueErrorIfMoreThanOnePresent were set to true when visiting method invocations). If no
-   * annotation is present, return RELEASESNOLOCKS as the default, and MAYRELEASELOCKS as the
-   * conservative default.
+   * Indicates which side effect annotation is present on the given method. Returns LOCKINGFREE
+   * rather than PURE or SIDEEFFECTFREE. If no annotation is present, returns RELEASESNOLOCKS as the
+   * default, and MAYRELEASELOCKS as the conservative default.
+   *
+   * <p>If more than one annotation is present, this method issues an error (if
+   * issueErrorIfMoreThanOnePresent is true) and returns the annotation providing the weakest
+   * guarantee. Only call with issueErrorIfMoreThanOnePresent == true when visiting a method
+   * definition. This prevents multiple errors being issued for the same method (as would occur if
+   * issueErrorIfMoreThanOnePresent were set to true when visiting method invocations).
    *
    * @param methodElement the method element
    * @param issueErrorIfMoreThanOnePresent if true, issue an error if more than one side effect
@@ -536,6 +537,9 @@ public static SideEffectAnnotation weakest() {
         EnumSet.noneOf(SideEffectAnnotation.class);
     for (SideEffectAnnotation sea : SideEffectAnnotation.values()) {
       if (getDeclAnnotationNoAliases(methodElement, sea.getAnnotationClass()) != null) {
+        if (sea == SideEffectAnnotation.PURE || sea == SideEffectAnnotation.SIDEEFFECTFREE) {
+          sea = SideEffectAnnotation.LOCKINGFREE;
+        }
         sideEffectAnnotationPresent.add(sea);
       }
     }
@@ -548,7 +552,12 @@ public static SideEffectAnnotation weakest() {
           : SideEffectAnnotation.RELEASESNOLOCKS;
     }
 
-    if (count > 1 && issueErrorIfMoreThanOnePresent) {
+    if (count == 1) {
+      return sideEffectAnnotationPresent.iterator().next();
+    }
+    // count > 1
+
+    if (issueErrorIfMoreThanOnePresent) {
       // TODO: Turn on after figuring out how this interacts with inherited annotations.
       // checker.reportError(methodElement, "multiple.sideeffect.annotations");
     }

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

@@ -1447,12 +1447,14 @@ private void reportPurityError(String msgKeyPrefix, IPair<Tree, String> r) {
     @SuppressWarnings("compilermessages")
     @CompilerMessageKey String msgKey = msgKeyPrefix + reason;
     if (reason.equals("call")) {
+      ExecutableElement calleeElement;
       if (r.first instanceof MethodInvocationTree mitree) {
-        checker.reportError(r.first, msgKey, mitree.getMethodSelect());
+        calleeElement = TreeUtils.elementFromUse(mitree);
       } else {
-        NewClassTree nctree = (NewClassTree) r.first;
-        checker.reportError(r.first, msgKey, nctree.getIdentifier());
+        calleeElement = TreeUtils.elementFromUse((NewClassTree) r.first);
       }
+      checker.reportError(
+          r.first, msgKey, calleeElement.getEnclosingElement(), calleeElement.getSimpleName());
     } else {
       checker.reportError(r.first, msgKey);
     }

framework/src/main/java/org/checkerframework/common/basetype/messages.properties

@@ -68,15 +68,15 @@ purity.methodref=Incompatible purity declaration%nMethod in %s%n  %s %s%n  is no
 purity.overriding=Incompatible purity declaration%nMethod in %s%n  %s %s%ncannot override method in %s%n  %s %s
 purity.not.deterministic.assign.array=array assignment not allowed in deterministic method
 purity.not.deterministic.assign.field=field assignment not allowed in deterministic method
-purity.not.deterministic.call=call to non-deterministic method %s not allowed in deterministic method
+purity.not.deterministic.call=call to non-deterministic %s::%s not allowed in deterministic method
 purity.not.deterministic.catch=catch block not allowed in deterministic method
 purity.not.deterministic.object.creation=object creation not allowed in deterministic method
 purity.not.deterministic.not.sideeffectfree.assign.array=array assignment not allowed in deterministic side-effect-free method
 purity.not.deterministic.not.sideeffectfree.assign.field=field assignment not allowed in deterministic side-effect-free method
-purity.not.deterministic.not.sideeffectfree.call=call to non-deterministic side-effecting %s not allowed in deterministic side-effect-free method
+purity.not.deterministic.not.sideeffectfree.call=call to non-deterministic side-effecting %s::%s not allowed in deterministic side-effect-free method
 purity.not.sideeffectfree.assign.array=array assignment not allowed in side-effect-free method
 purity.not.sideeffectfree.assign.field=field assignment not allowed in side-effect-free method
-purity.not.sideeffectfree.call=call to side-effecting %s not allowed in side-effect-free method
+purity.not.sideeffectfree.call=call to side-effecting %s::%s not allowed in side-effect-free method
 purity.more.deterministic=the method %s could be declared as @Deterministic
 purity.more.pure=the method %s could be declared as @Pure
 purity.more.sideeffectfree=the method %s could be declared as @SideEffectFree

framework/src/main/java/org/checkerframework/framework/ajava/InsertAjavaAnnotations.java

@@ -54,6 +54,7 @@
 import org.checkerframework.checker.regex.qual.Regex;
 import org.checkerframework.checker.signature.qual.DotSeparatedIdentifiers;
 import org.checkerframework.checker.signature.qual.FullyQualifiedName;
+import org.checkerframework.dataflow.qual.Pure;
 import org.checkerframework.framework.stub.AnnotationFileParser;
 import org.checkerframework.framework.util.JavaParserUtil;
 import org.checkerframework.framework.util.StaticJavaParserUtil;
@@ -520,6 +521,7 @@ public String insertAnnotations(
    * @return a negative integer, zero, or a positive integer if {@code insertion1} belongs before,
    *     at the same position, or after {@code insertion2} respectively in the above ordering
    */
+  @Pure
   private static int compareInsertions(Insertion insertion1, Insertion insertion2) {
     int cmp = Integer.compare(insertion1.position, insertion2.position);
     if (cmp == 0 && (insertion1.ownLine != insertion2.ownLine)) {

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

@@ -396,6 +396,7 @@ public static boolean containsSameByName(
    * @param a2 the second annotation
    * @return an ordering over AnnotationMirrors based on their name and values
    */
+  @Pure
   public static int compareAnnotationMirrors(AnnotationMirror a1, AnnotationMirror a2) {
     int nameComparison = compareByName(a1, a2);
     if (nameComparison != 0) {