Eliminate @SignedPositiveFromUnsigned annotation (#6146)

checker-qual/src/main/java/org/checkerframework/checker/signedness/qual/SignedPositive.java

@@ -5,19 +5,17 @@
 import java.lang.annotation.Retention;
 import java.lang.annotation.RetentionPolicy;
 import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.SubtypeOf;
 
 /**
- * The expression's value is in the signed positive range; that is, its most significant bit is not
- * set. The value has the same interpretation as {@code @}{@link Signed} and {@code @}{@link
+ * The expression's value is in the signed positive range; that is, its most significant bit is
+ * zero. The value has the same interpretation as {@code @}{@link Signed} and {@code @}{@link
  * Unsigned} — both interpretations are equivalent.
  *
  * <p>Programmers should rarely write {@code @SignedPositive}. Instead, the programmer should write
  * {@code @}{@link Signed} or {@code @}{@link Unsigned} to indicate how the programmer intends the
  * value to be interpreted.
  *
- * <p>Internally, this is translated to the {@code @}{@link SignednessGlb} annotation. This means
- * that programmers do not see this annotation in error messages.
- *
  * <p>{@code @SignedPositive} corresponds to {@code @}{@link
  * org.checkerframework.checker.index.qual.NonNegative NonNegative} in the Index Checker's type
  * system.
@@ -28,4 +26,5 @@
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf(SignednessGlb.class)
 public @interface SignedPositive {}

checker-qual/src/main/java/org/checkerframework/checker/signedness/qual/SignednessBottom.java

@@ -21,5 +21,5 @@
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @TargetLocations({TypeUseLocation.EXPLICIT_LOWER_BOUND, TypeUseLocation.EXPLICIT_UPPER_BOUND})
-@SubtypeOf({SignedPositiveFromUnsigned.class})
+@SubtypeOf({SignedPositive.class})
 public @interface SignednessBottom {}

checker-qual/src/main/java/org/checkerframework/checker/signedness/qual/SignednessGlb.java

@@ -5,8 +5,6 @@
 import java.lang.annotation.Retention;
 import java.lang.annotation.RetentionPolicy;
 import java.lang.annotation.Target;
-import org.checkerframework.framework.qual.LiteralKind;
-import org.checkerframework.framework.qual.QualifierForLiterals;
 import org.checkerframework.framework.qual.SubtypeOf;
 
 /**
@@ -38,5 +36,4 @@
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 @SubtypeOf({Unsigned.class, Signed.class})
-@QualifierForLiterals({LiteralKind.INT, LiteralKind.LONG, LiteralKind.CHAR})
 public @interface SignednessGlb {}

checker/bin/query-github.sh

@@ -11,8 +11,8 @@
 # $1 is the query file, which should contain the literal string to use
 # as the github search. REQUIRED, no default.
 #
-# $2 is the number of GitHub search pages.  Default 1. Each page contains 10 results.  GitHub only returns
-# the first 1000 results, so 100 is the maximum useful number of search pages.
+# $2 is the number of GitHub search pages.  Default 1. Each page contains 10 results.  GitHub only
+# returns the first 1000 results, so 100 is the maximum useful number of search pages.
 #
 # This script outputs a list of projects. The underlying GitHub search is for code snippets, and this
 # script eliminates duplicates (i.e. different code snippets from the same project are combined into

checker/src/main/java/org/checkerframework/checker/signedness/SignednessAnnotatedTypeFactory.java

@@ -3,13 +3,12 @@
 import com.sun.source.tree.BinaryTree;
 import com.sun.source.tree.CompoundAssignmentTree;
 import com.sun.source.tree.ExpressionTree;
+import com.sun.source.tree.LiteralTree;
 import com.sun.source.tree.Tree;
 import com.sun.source.tree.TypeCastTree;
 import com.sun.source.util.TreePath;
 import java.io.Serializable;
-import java.lang.annotation.Annotation;
 import java.util.List;
-import java.util.Set;
 import javax.annotation.processing.ProcessingEnvironment;
 import javax.lang.model.element.AnnotationMirror;
 import javax.lang.model.element.Element;
@@ -19,7 +18,6 @@
 import org.checkerframework.checker.signedness.qual.PolySigned;
 import org.checkerframework.checker.signedness.qual.Signed;
 import org.checkerframework.checker.signedness.qual.SignedPositive;
-import org.checkerframework.checker.signedness.qual.SignedPositiveFromUnsigned;
 import org.checkerframework.checker.signedness.qual.SignednessBottom;
 import org.checkerframework.checker.signedness.qual.SignednessGlb;
 import org.checkerframework.checker.signedness.qual.Unsigned;
@@ -65,9 +63,9 @@ public class SignednessAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {
   private final AnnotationMirror SIGNEDNESS_GLB =
       AnnotationBuilder.fromClass(elements, SignednessGlb.class);
 
-  /** The @SignedPositiveFromUnsigned annotation. */
-  protected final AnnotationMirror SIGNED_POSITIVE_FROM_UNSIGNED =
-      AnnotationBuilder.fromClass(elements, SignedPositiveFromUnsigned.class);
+  /** The @SignedPositive annotation. */
+  protected final AnnotationMirror SIGNED_POSITIVE =
+      AnnotationBuilder.fromClass(elements, SignedPositive.class);
 
   /** The @SignednessBottom annotation. */
   protected final AnnotationMirror SIGNEDNESS_BOTTOM =
@@ -111,24 +109,30 @@ public class SignednessAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {
   public SignednessAnnotatedTypeFactory(BaseTypeChecker checker) {
     super(checker);
 
-    addAliasedTypeAnnotation(SignedPositive.class, SIGNEDNESS_GLB);
-
     addAliasedTypeAnnotation("jdk.jfr.Unsigned", UNSIGNED);
 
     postInit();
   }
 
-  @Override
-  protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
-    Set<Class<? extends Annotation>> result = getBundledTypeQualifiers();
-    result.remove(SignedPositive.class); // this method should not return aliases
-    return result;
-  }
-
   @Override
   protected void addComputedTypeAnnotations(Tree tree, AnnotatedTypeMirror type, boolean iUseFlow) {
-    if (!computingAnnotatedTypeMirrorOfLHS) {
-      addSignednessGlbAnnotation(tree, type);
+    Tree.Kind treeKind = tree.getKind();
+    if (treeKind == Tree.Kind.INT_LITERAL) {
+      int literalValue = (int) ((LiteralTree) tree).getValue();
+      if (literalValue >= 0) {
+        type.replaceAnnotation(SIGNED_POSITIVE);
+      } else {
+        type.replaceAnnotation(SIGNEDNESS_GLB);
+      }
+    } else if (treeKind == Tree.Kind.LONG_LITERAL) {
+      long literalValue = (long) ((LiteralTree) tree).getValue();
+      if (literalValue >= 0) {
+        type.replaceAnnotation(SIGNED_POSITIVE);
+      } else {
+        type.replaceAnnotation(SIGNEDNESS_GLB);
+      }
+    } else if (!computingAnnotatedTypeMirrorOfLHS) {
+      addSignedPositiveAnnotation(tree, type);
     }
 
     super.addComputedTypeAnnotations(tree, type, iUseFlow);
@@ -153,13 +157,13 @@ public AnnotatedTypeMirror getAnnotatedTypeLhs(Tree lhsTree) {
   }
 
   /**
-   * Refines an integer expression to @SignednessGlb if its value is within the signed positive
+   * Refines an integer expression to @SignedPositive if its value is within the signed positive
    * range (i.e. its MSB is zero). Does not refine the type of cast expressions.
    *
    * @param tree an AST node, whose type may be refined
    * @param type the type of the tree
    */
-  private void addSignednessGlbAnnotation(Tree tree, AnnotatedTypeMirror type) {
+  private void addSignedPositiveAnnotation(Tree tree, AnnotatedTypeMirror type) {
     if (tree.getKind() == Tree.Kind.TYPE_CAST) {
       return;
     }
@@ -182,7 +186,7 @@ private void addSignednessGlbAnnotation(Tree tree, AnnotatedTypeMirror type) {
     if ((valueATM.hasPrimaryAnnotation(INT_RANGE_FROM_NON_NEGATIVE)
             || valueATM.hasPrimaryAnnotation(INT_RANGE_FROM_POSITIVE))
         && type.hasPrimaryAnnotation(SIGNED)) {
-      type.replaceAnnotation(SIGNEDNESS_GLB);
+      type.replaceAnnotation(SIGNED_POSITIVE);
     } else {
       Range treeRange = ValueCheckerUtils.getPossibleValues(valueATM, valueFactory);
 
@@ -191,22 +195,22 @@ private void addSignednessGlbAnnotation(Tree tree, AnnotatedTypeMirror type) {
           case BYTE:
           case CHAR:
             if (treeRange.isWithin(0, Byte.MAX_VALUE)) {
-              type.replaceAnnotation(SIGNEDNESS_GLB);
+              type.replaceAnnotation(SIGNED_POSITIVE);
             }
             break;
           case SHORT:
             if (treeRange.isWithin(0, Short.MAX_VALUE)) {
-              type.replaceAnnotation(SIGNEDNESS_GLB);
+              type.replaceAnnotation(SIGNED_POSITIVE);
             }
             break;
           case INT:
             if (treeRange.isWithin(0, Integer.MAX_VALUE)) {
-              type.replaceAnnotation(SIGNEDNESS_GLB);
+              type.replaceAnnotation(SIGNED_POSITIVE);
             }
             break;
           case LONG:
             if (treeRange.isWithin(0, Long.MAX_VALUE)) {
-              type.replaceAnnotation(SIGNEDNESS_GLB);
+              type.replaceAnnotation(SIGNED_POSITIVE);
             }
             break;
           default:
@@ -232,7 +236,7 @@ public AnnotationMirrorSet getWidenedAnnotations(
     }
     if ((widenedTypeKind == TypeKind.INT || widenedTypeKind == TypeKind.LONG)
         && typeKind == TypeKind.CHAR) {
-      result.add(SIGNED_POSITIVE_FROM_UNSIGNED);
+      result.add(SIGNED_POSITIVE);
       return result;
     }
     return annos;
@@ -294,7 +298,7 @@ public Void visitBinary(BinaryTree tree, AnnotatedTypeMirror type) {
           if (path != null
               && (SignednessShifts.isMaskedShiftEitherSignedness(tree, path)
                   || SignednessShifts.isCastedShiftEitherSignedness(tree, path))) {
-            type.replaceAnnotation(SIGNEDNESS_GLB);
+            type.replaceAnnotation(SIGNED_POSITIVE);
           } else {
             AnnotatedTypeMirror lht = getAnnotatedType(tree.getLeftOperand());
             type.replaceAnnotations(lht.getPrimaryAnnotations());

docs/CHANGELOG.md

@@ -3,6 +3,9 @@ Version 3.38.0 (September 1, 2023)
 
 **User-visible changes:**
 
+Eliminated the `@SignedPositiveFromUnsigned` annotation, which users were
+advised against using.
+
 **Implementation details:**
 
 Renamed `SourceChecker.processArg()' to `processErrorMessageArg()`.