Consider the following method: * @@ -61,10 +64,10 @@ String[] methods(); /** - * A wrapper annotation that makes the {@link EnsuresCalledMethods} annotation repeatable. - * - *
Programmers generally do not need to write this. It is created by Java when a programmer - * writes more than one {@link EnsuresCalledMethods} annotation at the same location. + * A wrapper annotation that makes the {@link EnsuresCalledMethods} annotation repeatable. This + * annotation is an implementation detail: programmers generally do not need to write this. It + * is created automatically by Java when a programmer writes more than one {@link + * EnsuresCalledMethods} annotation at the same location. */ @Documented @Retention(RetentionPolicy.RUNTIME) diff --git a/checker-qual/src/main/java/org/checkerframework/checker/signedness/qual/SignedPositive.java b/checker-qual/src/main/java/org/checkerframework/checker/signedness/qual/SignedPositive.java index f91e659378d..52416f01445 100644 --- a/checker-qual/src/main/java/org/checkerframework/checker/signedness/qual/SignedPositive.java +++ b/checker-qual/src/main/java/org/checkerframework/checker/signedness/qual/SignedPositive.java @@ -1,5 +1,7 @@ package org.checkerframework.checker.signedness.qual; +import org.checkerframework.framework.qual.SubtypeOf; + import java.lang.annotation.Documented; import java.lang.annotation.ElementType; import java.lang.annotation.Retention; @@ -7,17 +9,14 @@ import java.lang.annotation.Target; /** - * 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. * *
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. * - *
Internally, this is translated to the {@code @}{@link SignednessGlb} annotation. This means - * that programmers do not see this annotation in error messages. - * *
{@code @SignedPositive} corresponds to {@code @}{@link * org.checkerframework.checker.index.qual.NonNegative NonNegative} in the Index Checker's type * system. @@ -28,4 +27,5 @@ @Documented @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) +@SubtypeOf(SignednessGlb.class) public @interface SignedPositive {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/signedness/qual/SignedPositiveFromUnsigned.java b/checker-qual/src/main/java/org/checkerframework/checker/signedness/qual/SignedPositiveFromUnsigned.java deleted file mode 100644 index 2aee2fb5f18..00000000000 --- a/checker-qual/src/main/java/org/checkerframework/checker/signedness/qual/SignedPositiveFromUnsigned.java +++ /dev/null @@ -1,24 +0,0 @@ -package org.checkerframework.checker.signedness.qual; - -import org.checkerframework.framework.qual.SubtypeOf; - -import java.lang.annotation.Documented; -import java.lang.annotation.ElementType; -import java.lang.annotation.Retention; -import java.lang.annotation.RetentionPolicy; -import java.lang.annotation.Target; - -/** - * The expression is {@code @}{@link SignedPositive}, and its value came from widening a value that - * is allowed to be interpreted as unsigned. - * - *
Programmers should rarely write this annotation.
- *
- * @see SignednessGlb
- * @checker_framework.manual #signedness-checker Signedness Checker
- */
-@Documented
-@Retention(RetentionPolicy.RUNTIME)
-@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
-@SubtypeOf({SignednessGlb.class})
-public @interface SignedPositiveFromUnsigned {}
diff --git a/checker-qual/src/main/java/org/checkerframework/checker/signedness/qual/SignednessBottom.java b/checker-qual/src/main/java/org/checkerframework/checker/signedness/qual/SignednessBottom.java
index 33ec7578e0e..2cb269fbf62 100644
--- a/checker-qual/src/main/java/org/checkerframework/checker/signedness/qual/SignednessBottom.java
+++ b/checker-qual/src/main/java/org/checkerframework/checker/signedness/qual/SignednessBottom.java
@@ -25,5 +25,5 @@
TypeUseLocation.LOWER_BOUND,
TypeUseLocation.UPPER_BOUND,
})
-@SubtypeOf({SignedPositiveFromUnsigned.class})
+@SubtypeOf({SignedPositive.class})
public @interface SignednessBottom {}
diff --git a/checker-qual/src/main/java/org/checkerframework/checker/signedness/qual/SignednessGlb.java b/checker-qual/src/main/java/org/checkerframework/checker/signedness/qual/SignednessGlb.java
index 33a33869fb8..36f8e10c7ee 100644
--- a/checker-qual/src/main/java/org/checkerframework/checker/signedness/qual/SignednessGlb.java
+++ b/checker-qual/src/main/java/org/checkerframework/checker/signedness/qual/SignednessGlb.java
@@ -1,7 +1,5 @@
package org.checkerframework.checker.signedness.qual;
-import org.checkerframework.framework.qual.LiteralKind;
-import org.checkerframework.framework.qual.QualifierForLiterals;
import org.checkerframework.framework.qual.SubtypeOf;
import java.lang.annotation.Documented;
@@ -39,5 +37,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 {}
diff --git a/checker/bin-devel/count-suppressions b/checker/bin-devel/count-suppression-reasons
similarity index 91%
rename from checker/bin-devel/count-suppressions
rename to checker/bin-devel/count-suppression-reasons
index 1ca1e143740..f4326b591a9 100755
--- a/checker/bin-devel/count-suppressions
+++ b/checker/bin-devel/count-suppression-reasons
@@ -3,7 +3,7 @@
# This command counts the approximate frequency of each distinct reason for
# warning suppressions, in all files under the current directory.
# To invoke it, pass a type system name; for example:
-# count-suppressions nullness
+# count-suppression-reasons nullness
# The argument to this script is actually a regular expression.
# The "reason" for a warning suppression is the Java line comment after it:
@@ -62,8 +62,8 @@ fi
# Diagnostics
# echo "regex=${regex}"
-greplines=$(mktemp /tmp/count-suppressions."$(date +%Y%m%d-%H%M%S)"-XXX)
-countedreasons=$(mktemp /tmp/count-suppressions."$(date +%Y%m%d-%H%M%S)"-XXX)
+greplines=$(mktemp /tmp/count-suppression-reasons."$(date +%Y%m%d-%H%M%S)"-XXX)
+countedreasons=$(mktemp /tmp/count-suppression-reasons."$(date +%Y%m%d-%H%M%S)"-XXX)
# These are the two types of matching lines:
# * "checkername" or "chekername:..."
@@ -71,10 +71,10 @@ countedreasons=$(mktemp /tmp/count-suppressions."$(date +%Y%m%d-%H%M%S)"-XXX)
# include "@SuppressWarnings" because it might appear on the previous line.
# * @AssumeAssertion(checkername)
# This grep command captures a few stray lines; users should ignore them.
-# This grep command assumes that tests are not annotated, and it hard-codes ignoring "annotated-jdk", "jdk", "true positive", "// TP" (as an alias for "true positive"), and "count-suppressions-ignore".
+# This grep command assumes that tests are not annotated, and it hard-codes ignoring "annotated-jdk", "jdk", "true positive", "// TP" (as an alias for "true positive"), and "count-suppression-reasons-ignore".
${GREP} -n --recursive --include='*.java' "\"${regex}[:\"]\(.*[^;]\)\?\(\$\|//\)\|@AssumeAssertion(${regex})" \
| grep -v "@AnnotatedFor" | grep -v "/tests/" \
- | grep -v "/annotated-jdk/" | grep -v "/jdk/" | grep -v "^jdk/" | grep -v "true positive" | grep -v "// TP" | grep -v "count-suppressions-ignore" > "${greplines}"
+ | grep -v "/annotated-jdk/" | grep -v "/jdk/" | grep -v "^jdk/" | grep -v "true positive" | grep -v "// TP" | grep -v "count-suppression-reasons-ignore" > "${greplines}"
total=$(wc -l < "${greplines}")
## Don't output a total, to avoid people using this approximate count.
@@ -87,7 +87,7 @@ cat "${greplines}" \
| ${SED} 's/ \+$//' \
| sort | uniq -c | sort -rg > "${countedreasons}"
-# Add leading percentages to `uniq -c` output. Note that it rounds down to the nearest integer.
+# Add leading percentages to `uniq -c` output. Note that it rounds *down* to the nearest integer.
# (Digits afert the decimal don't make a practical difference.)
while read -r line; do
count=$(echo "$line" | cut -f1 -d " ");
diff --git a/checker/bin/query-github.sh b/checker/bin/query-github.sh
index 49d5d5906b2..752d789a508 100755
--- a/checker/bin/query-github.sh
+++ b/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
diff --git a/checker/src/main/java/org/checkerframework/checker/calledmethods/builder/BuilderFrameworkSupport.java b/checker/src/main/java/org/checkerframework/checker/calledmethods/builder/BuilderFrameworkSupport.java
index 555677ed745..40aa4a06202 100644
--- a/checker/src/main/java/org/checkerframework/checker/calledmethods/builder/BuilderFrameworkSupport.java
+++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/builder/BuilderFrameworkSupport.java
@@ -20,7 +20,7 @@
public interface BuilderFrameworkSupport {
/**
- * Determines if a method is a {@code toBuilder} method on a type generated by the builder
+ * Returns true if a method is a {@code toBuilder} method on a type generated by the builder
* framework.
*
* @param candidateToBuilderElement a method
@@ -42,7 +42,7 @@ public interface BuilderFrameworkSupport {
void handleToBuilderMethod(AnnotatedExecutableType toBuilderType);
/**
- * Determines if a method is a {@code build} method on a {@code Builder} type for the builder
+ * Returns true if a method is a {@code build} method on a {@code Builder} type for the builder
* framework.
*
* @param candidateBuildElement a method
diff --git a/checker/src/main/java/org/checkerframework/checker/index/IndexUtil.java b/checker/src/main/java/org/checkerframework/checker/index/IndexUtil.java
index 80c7c7370a6..9f86692a4e4 100644
--- a/checker/src/main/java/org/checkerframework/checker/index/IndexUtil.java
+++ b/checker/src/main/java/org/checkerframework/checker/index/IndexUtil.java
@@ -15,7 +15,18 @@
/** A collection of utility functions used by several Index Checker subcheckers. */
public class IndexUtil {
- /** Determines whether the type is a sequence supported by this checker. */
+
+ /** Do not instantiate IndexUtil. */
+ private IndexUtil() {
+ throw new Error("Do not instantiate IndexUtil.");
+ }
+
+ /**
+ * Returns true if the type is a sequence supported by this checker.
+ *
+ * @param type a type
+ * @return true if the type is a sequence supported by this checker
+ */
public static boolean isSequenceType(TypeMirror type) {
return type.getKind() == TypeKind.ARRAY || TypesUtils.isString(type);
}
diff --git a/checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java b/checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java
index 0982bcb6140..dc72963e72c 100644
--- a/checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java
+++ b/checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java
@@ -937,7 +937,7 @@ private boolean classIsAnnotated(AnnotatedTypeMirror type) {
}
/**
- * Determines whether or not the given element overrides the named method in the named class.
+ * Returns true if the given element overrides the named method in the named class.
*
* @param e an element for a method
* @param clazz the class
diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java
index c53290aa00b..52557668104 100644
--- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java
+++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java
@@ -863,9 +863,9 @@ private void updateObligationsWithInvocationResult(Set Specifically, an invocation result does NOT need to be tracked if any of the following is
@@ -1505,12 +1505,17 @@ && varTrackedInObligations(obligations, (LocalVariableNode) receiver))
AccumulationStore cmStoreBefore = typeFactory.getStoreBefore(rhs);
AccumulationValue cmValue = cmStoreBefore == null ? null : cmStoreBefore.getValue(lhs);
AnnotationMirror cmAnno = null;
- if (cmValue != null) {
- for (AnnotationMirror anno : cmValue.getAnnotations()) {
- if (AnnotationUtils.areSameByName(
- anno, "org.checkerframework.checker.calledmethods.qual.CalledMethods")) {
- cmAnno = anno;
- break;
+ if (cmValue != null) { // When store contains the lhs
+ Set {@code expr & 0x0[anything] == 0x0[something] ;}
- *
- * {@code expr | 0xF[anything] == 0xF[something] ;}
- *
- * @param maskKind the kind of mask (AND or OR)
- * @param shiftAmountLit the LiteralTree whose value is shiftAmount
- * @param maskLit the LiteralTree whose value is mask
- * @param shiftedTypeKind the type of shift operation; int or long
- * @return true iff the shiftAmount most significant bits of mask are 0 for AND, and 1 for OR
- */
- private boolean maskIgnoresMSB(
- Tree.Kind maskKind,
- LiteralTree shiftAmountLit,
- LiteralTree maskLit,
- TypeKind shiftedTypeKind) {
- long shiftAmount = getLong(shiftAmountLit.getValue());
-
- // Shift of zero is a nop
- if (shiftAmount == 0) {
- return true;
- }
-
- long mask = getLong(maskLit.getValue());
- // Shift the shiftAmount most significant bits to become the shiftAmount least significant
- // bits, zeroing out the rest.
- if (shiftedTypeKind == TypeKind.INT) {
- mask <<= 32;
- }
- mask >>>= (64 - shiftAmount);
-
- if (maskKind == Tree.Kind.AND) {
- // Check that the shiftAmount most significant bits of the mask were 0.
- return mask == 0;
- } else if (maskKind == Tree.Kind.OR) {
- // Check that the shiftAmount most significant bits of the mask were 1.
- return mask == (1 << shiftAmount) - 1;
- } else {
- throw new TypeSystemError("Invalid Masking Operation");
- }
- }
-
- /**
- * Given a casted right shift of the form {@code (type) (baseExpr >> shiftAmount)} or {@code
- * (type) (baseExpr >>> shiftAmount)}, return true iff the expression's value is the same
- * regardless of the type of right shift (signed or unsigned). This is true if the cast ignores
- * the shiftAmount most significant bits of the shift result -- that is, if the cast ignores all
- * the new bits that the right shift introduced on the left.
- *
- * For example, the function returns true for
- *
- * {@code (b >> 4) & 0x0F == (b >>> 4) & 0x0F;}
- *
- * {@code (b >> 4) | 0xF0 == (b >>> 4) | 0xF0;}
- *
- * @param shiftExpr a right shift expression: {@code expr1 >> expr2} or {@code expr1 >>> expr2}
- * @param path the path to {@code shiftExpr}
- * @return true iff the right shift is masked such that a signed or unsigned right shift has the
- * same effect
- */
- /*package-private*/ boolean isMaskedShiftEitherSignedness(BinaryTree shiftExpr, TreePath path) {
- IPair {@code (byte)(s >> 8) == (byte)(b >>> 8);}
- *
- * @param shiftExpr a right shift expression: {@code expr1 >> expr2} or {@code expr1 >>> expr2}
- * @param path the path to {@code shiftExpr}
- * @return true iff the right shift is type casted such that a signed or unsigned right shift
- * has the same effect
- */
- /*package-private*/ boolean isCastedShiftEitherSignedness(BinaryTree shiftExpr, TreePath path) {
- // enclosing immediately contains shiftExpr or a parenthesized version of shiftExpr
- Tree enclosing = TreePathUtil.enclosingNonParen(path).first;
-
- PrimitiveTypeTree castPrimitiveType = primitiveTypeCast(enclosing);
- if (castPrimitiveType == null) {
- return false;
- }
- TypeKind castTypeKind = castPrimitiveType.getPrimitiveTypeKind();
-
- // Determine the type of the shift result
- TypeKind shiftTypeKind = TreeUtils.typeOf(shiftExpr).getKind();
-
- // Determine shift literal
- ExpressionTree shiftAmountExpr = shiftExpr.getRightOperand();
- if (!isLiteral(shiftAmountExpr)) {
- return false;
- }
- LiteralTree shiftLit = (LiteralTree) shiftAmountExpr;
-
- boolean result = castIgnoresMSB(shiftTypeKind, castTypeKind, shiftLit);
- return result;
- }
-
- // End of special-case code for shifts that do not depend on the MSB of the first argument.
-
/**
* Requires that, when two formal parameter types are annotated with {@code @PolySigned}, the
* two arguments must have the same signedness type annotation.
diff --git a/checker/src/main/java/org/checkerframework/checker/signedness/SignednessShifts.java b/checker/src/main/java/org/checkerframework/checker/signedness/SignednessShifts.java
new file mode 100644
index 00000000000..69758906971
--- /dev/null
+++ b/checker/src/main/java/org/checkerframework/checker/signedness/SignednessShifts.java
@@ -0,0 +1,304 @@
+package org.checkerframework.checker.signedness;
+
+import com.sun.source.tree.AnnotatedTypeTree;
+import com.sun.source.tree.BinaryTree;
+import com.sun.source.tree.ExpressionTree;
+import com.sun.source.tree.LiteralTree;
+import com.sun.source.tree.PrimitiveTypeTree;
+import com.sun.source.tree.Tree;
+import com.sun.source.tree.TypeCastTree;
+import com.sun.source.util.TreePath;
+
+import org.checkerframework.checker.interning.qual.InternedDistinct;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.javacutil.TreePathUtil;
+import org.checkerframework.javacutil.TreeUtils;
+import org.checkerframework.javacutil.TypeSystemError;
+import org.plumelib.util.IPair;
+
+import javax.lang.model.type.TypeKind;
+
+/**
+ * This file contains code to special-case shifts whose result does not depend on the MSB of the
+ * first argument, due to subsequent masking or casts.
+ *
+ * @checker_framework.manual #signedness-checker Signedness Checker
+ */
+public class SignednessShifts {
+
+ /** Do not instantiate SignednessShifts. */
+ private SignednessShifts() {
+ throw new Error("Do not instantiate SignednessShifts");
+ }
+
+ /**
+ * Returns true iff the given tree node is a mask operation (& or |).
+ *
+ * @param tree a tree to test
+ * @return true iff node is a mask operation (& or |)
+ */
+ private static boolean isMask(Tree tree) {
+ Tree.Kind kind = tree.getKind();
+
+ return kind == Tree.Kind.AND || kind == Tree.Kind.OR;
+ }
+
+ // TODO: Return a TypeKind rather than a PrimitiveTypeTree?
+ /**
+ * Returns the type of a primitive cast, or null if the argument is not a cast to a primitive.
+ *
+ * @param tree a tree that might be a cast to a primitive
+ * @return type of a primitive cast, or null if not a cast to a primitive
+ */
+ private static @Nullable PrimitiveTypeTree primitiveTypeCast(Tree tree) {
+ if (tree.getKind() != Tree.Kind.TYPE_CAST) {
+ return null;
+ }
+
+ TypeCastTree cast = (TypeCastTree) tree;
+ Tree castType = cast.getType();
+
+ Tree underlyingType;
+ if (castType.getKind() == Tree.Kind.ANNOTATED_TYPE) {
+ underlyingType = ((AnnotatedTypeTree) castType).getUnderlyingType();
+ } else {
+ underlyingType = castType;
+ }
+
+ if (underlyingType.getKind() != Tree.Kind.PRIMITIVE_TYPE) {
+ return null;
+ }
+
+ return (PrimitiveTypeTree) underlyingType;
+ }
+
+ /**
+ * Returns true iff the given tree is a literal.
+ *
+ * @param expr a tree to test
+ * @return true iff expr is a literal
+ */
+ private static boolean isLiteral(ExpressionTree expr) {
+ return expr instanceof LiteralTree;
+ }
+
+ /**
+ * Returns the long value of an Integer or a Long
+ *
+ * @param obj either an Integer or a Long
+ * @return the long value of obj
+ */
+ private static long getLong(Object obj) {
+ return ((Number) obj).longValue();
+ }
+
+ /**
+ * Given a masking operation of the form {@code expr & maskLit} or {@code expr | maskLit},
+ * return true iff the masking operation results in the same output regardless of the value of
+ * the shiftAmount most significant bits of expr. This is if the shiftAmount most significant
+ * bits of mask are 0 for AND, and 1 for OR. For example, assuming that shiftAmount is 4, the
+ * following is true about AND and OR masks:
+ *
+ * {@code expr & 0x0[anything] == 0x0[something] ;}
+ *
+ * {@code expr | 0xF[anything] == 0xF[something] ;}
+ *
+ * @param maskKind the kind of mask (AND or OR)
+ * @param shiftAmountLit the LiteralTree whose value is shiftAmount
+ * @param maskLit the LiteralTree whose value is mask
+ * @param shiftedTypeKind the type of shift operation; int or long
+ * @return true iff the shiftAmount most significant bits of mask are 0 for AND, and 1 for OR
+ */
+ private static boolean maskIgnoresMSB(
+ Tree.Kind maskKind,
+ LiteralTree shiftAmountLit,
+ LiteralTree maskLit,
+ TypeKind shiftedTypeKind) {
+ long shiftAmount = getLong(shiftAmountLit.getValue());
+
+ // Shift of zero is a nop
+ if (shiftAmount == 0) {
+ return true;
+ }
+
+ long mask = getLong(maskLit.getValue());
+ // Shift the shiftAmount most significant bits to become the shiftAmount least significant
+ // bits, zeroing out the rest.
+ if (shiftedTypeKind == TypeKind.INT) {
+ mask <<= 32;
+ }
+ mask >>>= (64 - shiftAmount);
+
+ if (maskKind == Tree.Kind.AND) {
+ // Check that the shiftAmount most significant bits of the mask were 0.
+ return mask == 0;
+ } else if (maskKind == Tree.Kind.OR) {
+ // Check that the shiftAmount most significant bits of the mask were 1.
+ return mask == (1 << shiftAmount) - 1;
+ } else {
+ throw new TypeSystemError("Invalid Masking Operation");
+ }
+ }
+
+ /**
+ * Given a casted right shift of the form {@code (type) (baseExpr >> shiftAmount)} or {@code
+ * (type) (baseExpr >>> shiftAmount)}, return true iff the expression's value is the same
+ * regardless of the type of right shift (signed or unsigned). This is true if the cast ignores
+ * the shiftAmount most significant bits of the shift result -- that is, if the cast ignores all
+ * the new bits that the right shift introduced on the left.
+ *
+ * For example, the function returns true for
+ *
+ * {@code (b >> 4) & 0x0F == (b >>> 4) & 0x0F;}
+ *
+ * {@code (b >> 4) | 0xF0 == (b >>> 4) | 0xF0;}
+ *
+ * @param shiftExpr a right shift expression: {@code expr1 >> expr2} or {@code expr1 >>> expr2}
+ * @param path the path to {@code shiftExpr}
+ * @return true iff the right shift is masked such that a signed or unsigned right shift has the
+ * same effect
+ */
+ /*package-private*/ static boolean isMaskedShiftEitherSignedness(
+ BinaryTree shiftExpr, TreePath path) {
+ IPair {@code (byte)(s >> 8) == (byte)(b >>> 8);}
+ *
+ * @param shiftExpr a right shift expression: {@code expr1 >> expr2} or {@code expr1 >>> expr2}
+ * @param path the path to {@code shiftExpr}
+ * @return true iff the right shift is type casted such that a signed or unsigned right shift
+ * has the same effect
+ */
+ /*package-private*/ static boolean isCastedShiftEitherSignedness(
+ BinaryTree shiftExpr, TreePath path) {
+ // enclosing immediately contains shiftExpr or a parenthesized version of shiftExpr
+ Tree enclosing = TreePathUtil.enclosingNonParen(path).first;
+
+ PrimitiveTypeTree castPrimitiveType = primitiveTypeCast(enclosing);
+ if (castPrimitiveType == null) {
+ return false;
+ }
+ TypeKind castTypeKind = castPrimitiveType.getPrimitiveTypeKind();
+
+ // Determine the type of the shift result
+ TypeKind shiftTypeKind = TreeUtils.typeOf(shiftExpr).getKind();
+
+ // Determine shift literal
+ ExpressionTree shiftAmountExpr = shiftExpr.getRightOperand();
+ if (!isLiteral(shiftAmountExpr)) {
+ return false;
+ }
+ LiteralTree shiftLit = (LiteralTree) shiftAmountExpr;
+
+ boolean result = castIgnoresMSB(shiftTypeKind, castTypeKind, shiftLit);
+ return result;
+ }
+}
diff --git a/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java b/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java
index 740d4580afc..dc0f41b6624 100644
--- a/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java
+++ b/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java
@@ -39,7 +39,7 @@ public SignednessVisitor(BaseTypeChecker checker) {
}
/**
- * Determines if an annotated type is annotated as {@link Unsigned} or {@link PolySigned}
+ * Returns true if an annotated type is annotated as {@link Unsigned} or {@link PolySigned}
*
* @param type the annotated type to be checked
* @return true if the annotated type is annotated as {@link Unsigned} or {@link PolySigned}
@@ -49,7 +49,7 @@ private boolean hasUnsignedAnnotation(AnnotatedTypeMirror type) {
}
/**
- * Determines if an annotated type is annotated as {@link Signed} or {@link PolySigned}
+ * Returns true if an annotated type is annotated as {@link Signed} or {@link PolySigned}
*
* @param type the annotated type to be checked
* @return true if the annotated type is annotated as {@link Signed} or {@link PolySigned}
@@ -100,16 +100,18 @@ public Void visitBinary(BinaryTree tree, Void p) {
case RIGHT_SHIFT:
if (hasUnsignedAnnotation(leftOpType)
- && !atypeFactory.isMaskedShiftEitherSignedness(tree, getCurrentPath())
- && !atypeFactory.isCastedShiftEitherSignedness(tree, getCurrentPath())) {
+ && !SignednessShifts.isMaskedShiftEitherSignedness(tree, getCurrentPath())
+ && !SignednessShifts.isCastedShiftEitherSignedness(
+ tree, getCurrentPath())) {
checker.reportError(leftOp, "shift.signed", kind, leftOpType, rightOpType);
}
break;
case UNSIGNED_RIGHT_SHIFT:
if (hasSignedAnnotation(leftOpType)
- && !atypeFactory.isMaskedShiftEitherSignedness(tree, getCurrentPath())
- && !atypeFactory.isCastedShiftEitherSignedness(tree, getCurrentPath())) {
+ && !SignednessShifts.isMaskedShiftEitherSignedness(tree, getCurrentPath())
+ && !SignednessShifts.isCastedShiftEitherSignedness(
+ tree, getCurrentPath())) {
checker.reportError(leftOp, "shift.unsigned", kind, leftOpType, rightOpType);
}
break;
diff --git a/checker/src/main/java/org/checkerframework/checker/tainting/TaintingAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/tainting/TaintingAnnotatedTypeFactory.java
new file mode 100644
index 00000000000..a92ec7a5f4f
--- /dev/null
+++ b/checker/src/main/java/org/checkerframework/checker/tainting/TaintingAnnotatedTypeFactory.java
@@ -0,0 +1,38 @@
+package org.checkerframework.checker.tainting;
+
+import org.checkerframework.checker.tainting.qual.Untainted;
+import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
+import org.checkerframework.common.basetype.BaseTypeChecker;
+import org.checkerframework.javacutil.AnnotationBuilder;
+import org.checkerframework.javacutil.AnnotationMirrorSet;
+
+import java.util.Set;
+
+import javax.lang.model.element.AnnotationMirror;
+
+/** Annotated type factory for the Tainting Checker. */
+public class TaintingAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {
+
+ /** The {@code @}{@link Untainted} annotation mirror. */
+ private final AnnotationMirror UNTAINTED;
+
+ /** A singleton set containing the {@code @}{@link Untainted} annotation mirror. */
+ private final AnnotationMirrorSet setOfUntainted;
+
+ /**
+ * Creates a {@link TaintingAnnotatedTypeFactory}.
+ *
+ * @param checker the tainting checker
+ */
+ public TaintingAnnotatedTypeFactory(BaseTypeChecker checker) {
+ super(checker);
+ this.UNTAINTED = AnnotationBuilder.fromClass(getElementUtils(), Untainted.class);
+ this.setOfUntainted = AnnotationMirrorSet.singleton(UNTAINTED);
+ postInit();
+ }
+
+ @Override
+ protected Set Note that this class is deliberately public, to enable users of the dataflow library to
+ * customize CFG construction.
*/
public class Label {
diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md
index c3a25dca343..34a7e9ba80a 100644
--- a/docs/CHANGELOG.md
+++ b/docs/CHANGELOG.md
@@ -1,4 +1,4 @@
-Version 3.37.0-eisop1 (October ?, 2023)
+Version 3.38.0-eisop1 (October ?, 2023)
---------------------------------------
**User-visible changes:**
@@ -48,6 +48,23 @@ Changed the return types of
eisop#297, eisop#376, eisop#400, eisop#519, eisop#532, eisop#533, typetools#1590, typetools#1919.
+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()`.
+
+**Closed issues:**
+
+#2156, #5672, #6110, #6111, #6116, #6125, #6129, #6136.
+
+
Version 3.37.0 (August 1, 2023)
-------------------------------
diff --git a/docs/checker-framework-webpage.html b/docs/checker-framework-webpage.html
index 5c5d4d21a80..af9e37e1265 100644
--- a/docs/checker-framework-webpage.html
+++ b/docs/checker-framework-webpage.html
@@ -30,8 +30,8 @@
-Last updated: 1 Aug 2023
+Last updated: 1 Sep 2023
{@code (short) (myInt >> 16)}
- *
- * and for
- *
- * {@code (short) (myInt >>> 16)}
- *
- * because these two expressions are guaranteed to have the same result.
- *
- * @param shiftTypeKind the kind of the type of the shift literal (BYTE, CHAR, SHORT, INT, or
- * LONG)
- * @param castTypeKind the kind of the cast target type (BYTE, CHAR, SHORT, INT, or LONG)
- * @param shiftAmountLit the LiteralTree whose value is shiftAmount
- * @return true iff introduced bits are discarded
- */
- private boolean castIgnoresMSB(
- TypeKind shiftTypeKind, TypeKind castTypeKind, LiteralTree shiftAmountLit) {
-
- // Determine number of bits in the shift type, note shifts upcast to int.
- // Also determine the shift amount as it is dependent on the shift type.
- long shiftBits;
- long shiftAmount;
- switch (shiftTypeKind) {
- case INT:
- shiftBits = 32;
- // When the LHS of the shift is an int, the 5 lower order bits of the RHS are used.
- shiftAmount = 0x1F & getLong(shiftAmountLit.getValue());
- break;
- case LONG:
- shiftBits = 64;
- // When the LHS of the shift is a long, the 6 lower order bits of the RHS are used.
- shiftAmount = 0x3F & getLong(shiftAmountLit.getValue());
- break;
- default:
- throw new TypeSystemError("Invalid shift type");
- }
-
- // Determine number of bits in the cast type
- long castBits;
- switch (castTypeKind) {
- case BYTE:
- castBits = 8;
- break;
- case CHAR:
- castBits = 8;
- break;
- case SHORT:
- castBits = 16;
- break;
- case INT:
- castBits = 32;
- break;
- case LONG:
- castBits = 64;
- break;
- default:
- throw new TypeSystemError("Invalid cast target");
- }
-
- long bitsDiscarded = shiftBits - castBits;
-
- return shiftAmount <= bitsDiscarded || shiftAmount == 0;
- }
-
- /**
- * Determines if a right shift operation, {@code >>} or {@code >>>}, is masked with a masking
- * operation of the form {@code shiftExpr & maskLit} or {@code shiftExpr | maskLit} such that
- * the mask renders the shift signedness ({@code >>} vs {@code >>>}) irrelevant by destroying
- * the bits duplicated into the shift result. For example, the following pairs of right shifts
- * on {@code byte b} both produce the same results under any input, because of their masks:
- *
- * {@code (short) (myInt >> 16)}
+ *
+ * and for
+ *
+ * {@code (short) (myInt >>> 16)}
+ *
+ * because these two expressions are guaranteed to have the same result.
+ *
+ * @param shiftTypeKind the kind of the type of the shift literal (BYTE, CHAR, SHORT, INT, or
+ * LONG)
+ * @param castTypeKind the kind of the cast target type (BYTE, CHAR, SHORT, INT, or LONG)
+ * @param shiftAmountLit the LiteralTree whose value is shiftAmount
+ * @return true iff introduced bits are discarded
+ */
+ private static boolean castIgnoresMSB(
+ TypeKind shiftTypeKind, TypeKind castTypeKind, LiteralTree shiftAmountLit) {
+
+ // Determine number of bits in the shift type, note shifts upcast to int.
+ // Also determine the shift amount as it is dependent on the shift type.
+ long shiftBits;
+ long shiftAmount;
+ switch (shiftTypeKind) {
+ case INT:
+ shiftBits = 32;
+ // When the LHS of the shift is an int, the 5 lower order bits of the RHS are used.
+ shiftAmount = 0x1F & getLong(shiftAmountLit.getValue());
+ break;
+ case LONG:
+ shiftBits = 64;
+ // When the LHS of the shift is a long, the 6 lower order bits of the RHS are used.
+ shiftAmount = 0x3F & getLong(shiftAmountLit.getValue());
+ break;
+ default:
+ throw new TypeSystemError("Invalid shift type");
+ }
+
+ // Determine number of bits in the cast type
+ long castBits;
+ switch (castTypeKind) {
+ case BYTE:
+ castBits = 8;
+ break;
+ case CHAR:
+ castBits = 8;
+ break;
+ case SHORT:
+ castBits = 16;
+ break;
+ case INT:
+ castBits = 32;
+ break;
+ case LONG:
+ castBits = 64;
+ break;
+ default:
+ throw new TypeSystemError("Invalid cast target");
+ }
+
+ long bitsDiscarded = shiftBits - castBits;
+
+ return shiftAmount <= bitsDiscarded || shiftAmount == 0;
+ }
+
+ /**
+ * Returns true if a right shift operation, {@code >>} or {@code >>>}, is masked with a masking
+ * operation of the form {@code shiftExpr & maskLit} or {@code shiftExpr | maskLit} such that
+ * the mask renders the shift signedness ({@code >>} vs {@code >>>}) irrelevant by destroying
+ * the bits duplicated into the shift result. For example, the following pairs of right shifts
+ * on {@code byte b} both produce the same results under any input, because of their masks:
+ *
+ * The Checker Framework
Installation instructions and tutorial.
Then, see the installation
@@ -93,7 +93,7 @@ The Checker Framework
the .class file. The tools support both Java 5
declaration annotations and Java 8 type annotations.
-
Mailing lists