From 55e2d7244f8de57ad01e2510001b9c890ed0bde2 Mon Sep 17 00:00:00 2001 From: Martin Kellogg Date: Thu, 30 Jun 2022 12:21:11 -0700 Subject: [PATCH 1/6] ajava-based inference should not print invisible qualifiers, and make top annotations invisible --- .../checker/index/qual/LessThanUnknown.java | 2 + .../checker/index/qual/LowerBoundUnknown.java | 2 + .../checker/index/qual/SameLenUnknown.java | 2 + .../index/qual/SearchIndexUnknown.java | 2 + .../index/qual/SubstringIndexUnknown.java | 2 + .../checker/index/qual/UpperBoundUnknown.java | 2 + .../returnsreceiver/qual/UnknownThis.java | 2 + .../common/value/qual/UnknownVal.java | 2 + ...holeProgramInferenceJavaParserStorage.java | 54 ++++++++++++++++++- 9 files changed, 69 insertions(+), 1 deletion(-) diff --git a/checker-qual/src/main/java/org/checkerframework/checker/index/qual/LessThanUnknown.java b/checker-qual/src/main/java/org/checkerframework/checker/index/qual/LessThanUnknown.java index 3b456c3469d..d75a0a4aafa 100644 --- a/checker-qual/src/main/java/org/checkerframework/checker/index/qual/LessThanUnknown.java +++ b/checker-qual/src/main/java/org/checkerframework/checker/index/qual/LessThanUnknown.java @@ -6,6 +6,7 @@ import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; import org.checkerframework.framework.qual.DefaultQualifierInHierarchy; +import org.checkerframework.framework.qual.InvisibleQualifier; import org.checkerframework.framework.qual.SubtypeOf; /** @@ -19,4 +20,5 @@ @Target({ElementType.TYPE_PARAMETER, ElementType.TYPE_USE}) @SubtypeOf({}) @DefaultQualifierInHierarchy +@InvisibleQualifier public @interface LessThanUnknown {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/index/qual/LowerBoundUnknown.java b/checker-qual/src/main/java/org/checkerframework/checker/index/qual/LowerBoundUnknown.java index f9c9031d5e8..9025c8efa06 100644 --- a/checker-qual/src/main/java/org/checkerframework/checker/index/qual/LowerBoundUnknown.java +++ b/checker-qual/src/main/java/org/checkerframework/checker/index/qual/LowerBoundUnknown.java @@ -6,6 +6,7 @@ import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; import org.checkerframework.framework.qual.DefaultQualifierInHierarchy; +import org.checkerframework.framework.qual.InvisibleQualifier; import org.checkerframework.framework.qual.SubtypeOf; /** @@ -19,4 +20,5 @@ @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) @SubtypeOf({}) @DefaultQualifierInHierarchy +@InvisibleQualifier public @interface LowerBoundUnknown {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/index/qual/SameLenUnknown.java b/checker-qual/src/main/java/org/checkerframework/checker/index/qual/SameLenUnknown.java index f090c956e1b..08b1616a466 100644 --- a/checker-qual/src/main/java/org/checkerframework/checker/index/qual/SameLenUnknown.java +++ b/checker-qual/src/main/java/org/checkerframework/checker/index/qual/SameLenUnknown.java @@ -6,6 +6,7 @@ import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; import org.checkerframework.framework.qual.DefaultQualifierInHierarchy; +import org.checkerframework.framework.qual.InvisibleQualifier; import org.checkerframework.framework.qual.SubtypeOf; /** @@ -20,4 +21,5 @@ @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) @SubtypeOf({}) @DefaultQualifierInHierarchy +@InvisibleQualifier public @interface SameLenUnknown {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/index/qual/SearchIndexUnknown.java b/checker-qual/src/main/java/org/checkerframework/checker/index/qual/SearchIndexUnknown.java index 75bc3432bf3..065f800d56f 100644 --- a/checker-qual/src/main/java/org/checkerframework/checker/index/qual/SearchIndexUnknown.java +++ b/checker-qual/src/main/java/org/checkerframework/checker/index/qual/SearchIndexUnknown.java @@ -6,6 +6,7 @@ import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; import org.checkerframework.framework.qual.DefaultQualifierInHierarchy; +import org.checkerframework.framework.qual.InvisibleQualifier; import org.checkerframework.framework.qual.SubtypeOf; /** @@ -19,4 +20,5 @@ @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) @SubtypeOf({}) @DefaultQualifierInHierarchy +@InvisibleQualifier public @interface SearchIndexUnknown {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/index/qual/SubstringIndexUnknown.java b/checker-qual/src/main/java/org/checkerframework/checker/index/qual/SubstringIndexUnknown.java index 94c4480d38a..6cc1921eefc 100644 --- a/checker-qual/src/main/java/org/checkerframework/checker/index/qual/SubstringIndexUnknown.java +++ b/checker-qual/src/main/java/org/checkerframework/checker/index/qual/SubstringIndexUnknown.java @@ -6,6 +6,7 @@ import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; import org.checkerframework.framework.qual.DefaultQualifierInHierarchy; +import org.checkerframework.framework.qual.InvisibleQualifier; import org.checkerframework.framework.qual.SubtypeOf; /** @@ -19,4 +20,5 @@ @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) @SubtypeOf({}) @DefaultQualifierInHierarchy +@InvisibleQualifier public @interface SubstringIndexUnknown {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/index/qual/UpperBoundUnknown.java b/checker-qual/src/main/java/org/checkerframework/checker/index/qual/UpperBoundUnknown.java index 8548028b56e..87dff96d2b1 100644 --- a/checker-qual/src/main/java/org/checkerframework/checker/index/qual/UpperBoundUnknown.java +++ b/checker-qual/src/main/java/org/checkerframework/checker/index/qual/UpperBoundUnknown.java @@ -6,6 +6,7 @@ import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; import org.checkerframework.framework.qual.DefaultQualifierInHierarchy; +import org.checkerframework.framework.qual.InvisibleQualifier; import org.checkerframework.framework.qual.SubtypeOf; /** @@ -19,4 +20,5 @@ @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) @SubtypeOf({}) @DefaultQualifierInHierarchy +@InvisibleQualifier public @interface UpperBoundUnknown {} diff --git a/checker-qual/src/main/java/org/checkerframework/common/returnsreceiver/qual/UnknownThis.java b/checker-qual/src/main/java/org/checkerframework/common/returnsreceiver/qual/UnknownThis.java index 6d1d282ac9c..5c22729f753 100644 --- a/checker-qual/src/main/java/org/checkerframework/common/returnsreceiver/qual/UnknownThis.java +++ b/checker-qual/src/main/java/org/checkerframework/common/returnsreceiver/qual/UnknownThis.java @@ -6,6 +6,7 @@ import java.lang.annotation.Target; import org.checkerframework.framework.qual.DefaultFor; import org.checkerframework.framework.qual.DefaultQualifierInHierarchy; +import org.checkerframework.framework.qual.InvisibleQualifier; import org.checkerframework.framework.qual.LiteralKind; import org.checkerframework.framework.qual.QualifierForLiterals; import org.checkerframework.framework.qual.SubtypeOf; @@ -23,4 +24,5 @@ @SubtypeOf({}) @QualifierForLiterals(LiteralKind.NULL) @DefaultFor(value = TypeUseLocation.LOWER_BOUND) +@InvisibleQualifier public @interface UnknownThis {} diff --git a/checker-qual/src/main/java/org/checkerframework/common/value/qual/UnknownVal.java b/checker-qual/src/main/java/org/checkerframework/common/value/qual/UnknownVal.java index bcc6b9d1186..1ae28c0f75b 100644 --- a/checker-qual/src/main/java/org/checkerframework/common/value/qual/UnknownVal.java +++ b/checker-qual/src/main/java/org/checkerframework/common/value/qual/UnknownVal.java @@ -6,6 +6,7 @@ import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; import org.checkerframework.framework.qual.DefaultQualifierInHierarchy; +import org.checkerframework.framework.qual.InvisibleQualifier; import org.checkerframework.framework.qual.SubtypeOf; /** @@ -19,4 +20,5 @@ @Target({ElementType.TYPE_PARAMETER, ElementType.TYPE_USE}) @SubtypeOf({}) @DefaultQualifierInHierarchy +@InvisibleQualifier public @interface UnknownVal {} diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java index dc4ff0f8d74..a4f4e2a01b7 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java @@ -1,6 +1,7 @@ package org.checkerframework.common.wholeprograminference; import com.github.javaparser.ast.CompilationUnit; +import com.github.javaparser.ast.Node; import com.github.javaparser.ast.NodeList; import com.github.javaparser.ast.body.CallableDeclaration; import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration; @@ -14,12 +15,17 @@ import com.github.javaparser.ast.body.TypeDeclaration; import com.github.javaparser.ast.body.VariableDeclarator; import com.github.javaparser.ast.expr.AnnotationExpr; +import com.github.javaparser.ast.expr.MarkerAnnotationExpr; +import com.github.javaparser.ast.expr.NormalAnnotationExpr; import com.github.javaparser.ast.expr.ObjectCreationExpr; +import com.github.javaparser.ast.expr.SingleMemberAnnotationExpr; import com.github.javaparser.ast.type.ClassOrInterfaceType; import com.github.javaparser.ast.type.Type; import com.github.javaparser.ast.type.TypeParameter; import com.github.javaparser.ast.visitor.CloneVisitor; +import com.github.javaparser.ast.visitor.VoidVisitor; import com.github.javaparser.printer.DefaultPrettyPrinter; +import com.github.javaparser.printer.DefaultPrettyPrinterVisitor; import com.sun.source.tree.ClassTree; import com.sun.source.tree.MethodTree; import com.sun.source.tree.NewClassTree; @@ -33,12 +39,14 @@ import java.nio.file.Files; import java.nio.file.Paths; import java.util.ArrayList; +import java.util.Arrays; import java.util.Collections; import java.util.HashMap; import java.util.HashSet; import java.util.List; import java.util.Map; import java.util.Set; +import java.util.stream.Collectors; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; import javax.lang.model.element.ExecutableElement; @@ -56,6 +64,7 @@ import org.checkerframework.framework.ajava.AnnotationTransferVisitor; import org.checkerframework.framework.ajava.DefaultJointVisitor; import org.checkerframework.framework.ajava.JointJavacJavaParserVisitor; +import org.checkerframework.framework.qual.InvisibleQualifier; import org.checkerframework.framework.qual.TypeUseLocation; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; @@ -782,7 +791,50 @@ private void writeAjavaFile(String outputPath, CompilationUnitAnnos root) { // certain locations. This implementation could be used instead if it's fixed in JavaParser. // LexicalPreservingPrinter.print(root.declaration, writer); - DefaultPrettyPrinter prettyPrinter = new DefaultPrettyPrinter(); + // Do not print invisible qualifiers, to avoid cluttering the output. + Set invisibleQualifierNames = + atypeFactory.getSupportedTypeQualifiers().stream() + .filter( + qual -> + Arrays.stream(qual.getAnnotations()) + .anyMatch(anno -> anno.annotationType() == InvisibleQualifier.class)) + .map(Class::getCanonicalName) + .collect(Collectors.toSet()); + DefaultPrettyPrinter prettyPrinter = + new DefaultPrettyPrinter() { + @Override + public String print(Node node) { + VoidVisitor visitor = + new DefaultPrettyPrinterVisitor(getConfiguration()) { + @Override + public void visit(final MarkerAnnotationExpr n, final Void arg) { + if (invisibleQualifierNames.contains(n.getName().toString())) { + return; + } + super.visit(n, arg); + } + + @Override + public void visit(final SingleMemberAnnotationExpr n, final Void arg) { + if (invisibleQualifierNames.contains(n.getName().toString())) { + return; + } + super.visit(n, arg); + } + + @Override + public void visit(final NormalAnnotationExpr n, final Void arg) { + if (invisibleQualifierNames.contains(n.getName().toString())) { + return; + } + super.visit(n, arg); + } + }; + node.accept(visitor, null); + return visitor.toString(); + } + }; + writer.write(prettyPrinter.print(root.compilationUnit)); writer.close(); } catch (IOException e) { From b80ddd1728af15a9ffc9566ecd4db61c73da2ed1 Mon Sep 17 00:00:00 2001 From: Martin Kellogg Date: Thu, 30 Jun 2022 14:47:21 -0700 Subject: [PATCH 2/6] remove invisible qualifiers from JTREG test --- checker/jtreg/sortwarnings/ErrorOrders.out | 94 +++++++++++----------- 1 file changed, 47 insertions(+), 47 deletions(-) diff --git a/checker/jtreg/sortwarnings/ErrorOrders.out b/checker/jtreg/sortwarnings/ErrorOrders.out index 143ba4a6f6a..db5fe8c207f 100644 --- a/checker/jtreg/sortwarnings/ErrorOrders.out +++ b/checker/jtreg/sortwarnings/ErrorOrders.out @@ -1,23 +1,23 @@ OrderOfCheckers.java:12:95: compiler.err.proc.messager: [assignment] incompatible types in assignment. found : @UnknownVal int @UnknownVal [] -required: @UnknownVal int [] +required: @UnknownVal int @BottomVal [] OrderOfCheckers.java:12:95: compiler.err.proc.messager: [assignment] incompatible types in assignment. -found : @SearchIndexUnknown int @SearchIndexUnknown [] -required: @SearchIndexBottom int @SearchIndexUnknown [] +found : int [] +required: @SearchIndexBottom int [] OrderOfCheckers.java:12:95: compiler.err.proc.messager: [assignment] incompatible types in assignment. -found : @SameLenUnknown int @SameLen("y") [] -required: @SameLenUnknown int @SameLenBottom [] +found : int @SameLen("y") [] +required: int @SameLenBottom [] OrderOfCheckers.java:12:95: compiler.err.proc.messager: [assignment] incompatible types in assignment. -found : @LowerBoundUnknown int @LowerBoundUnknown [] -required: @GTENegativeOne int @LowerBoundUnknown [] +found : int [] +required: @GTENegativeOne int [] OrderOfCheckers.java:12:95: compiler.err.proc.messager: [assignment] incompatible types in assignment. -found : @UpperBoundUnknown int @UpperBoundUnknown [] -required: @UpperBoundBottom int @UpperBoundUnknown [] +found : int [] +required: @UpperBoundBottom int [] ErrorOrders.java:13:7: compiler.err.proc.messager: [array.access.unsafe.low] Potentially unsafe array access: the index could be negative. -found : @LowerBoundUnknown int +found : int required: an integer >= 0 (@NonNegative or @Positive) ErrorOrders.java:13:7: compiler.err.proc.messager: [array.access.unsafe.high] Potentially unsafe array access: the index could be larger than the array's bound -found : @UpperBoundUnknown int +found : int required: @IndexFor("a") or @LTLengthOf("a") -- an integer less than a's length ErrorOrders.java:23:29: compiler.err.proc.messager: [assignment] incompatible types in assignment. found : @UpperBoundLiteral(0) int @@ -27,66 +27,66 @@ ErrorOrders.java:24:51: compiler.err.proc.messager: [assignment] incompatible ty found : @LTLengthOf("p2") int required: @LTLengthOf("[error for expression: This isn't an expression; error: Invalid 'This isn't an expression' because the expression did not parse. Error message: Encountered unexpected token: "isn" ]") int ErrorOrders.java:29:11: compiler.err.proc.messager: [argument] incompatible argument for parameter p1 of test4. -found : @LowerBoundUnknown int +found : int required: @GTENegativeOne int ErrorOrders.java:29:11: compiler.err.proc.messager: [argument] incompatible argument for parameter p1 of test4. -found : @UpperBoundUnknown int +found : int required: @UpperBoundBottom int ErrorOrders.java:29:20: compiler.err.proc.messager: [argument] incompatible argument for parameter p2 of test4. -found : @LowerBoundUnknown int +found : int required: @GTENegativeOne int ErrorOrders.java:29:20: compiler.err.proc.messager: [argument] incompatible argument for parameter p2 of test4. -found : @UpperBoundUnknown int +found : int required: @UpperBoundBottom int ErrorOrders.java:29:21: compiler.err.proc.messager: [argument] incompatible argument for parameter p1 of test4. -found : @LowerBoundUnknown int +found : int required: @GTENegativeOne int ErrorOrders.java:29:21: compiler.err.proc.messager: [argument] incompatible argument for parameter p1 of test4. -found : @UpperBoundUnknown int +found : int required: @UpperBoundBottom int ErrorOrders.java:29:25: compiler.err.proc.messager: [argument] incompatible argument for parameter p2 of test4. -found : @LowerBoundUnknown int +found : int required: @GTENegativeOne int ErrorOrders.java:29:25: compiler.err.proc.messager: [argument] incompatible argument for parameter p2 of test4. -found : @UpperBoundUnknown int +found : int required: @UpperBoundBottom int ErrorOrders.java:29:29: compiler.err.proc.messager: [argument] incompatible argument for parameter p3 of test4. found : @UnknownVal int @UnknownVal [] -required: @UnknownVal int [] +required: @UnknownVal int @BottomVal [] ErrorOrders.java:29:33: compiler.err.proc.messager: [argument] incompatible argument for parameter p4 of test4. -found : @SameLenUnknown int @SameLen("p4") [] -required: @SameLenUnknown int @SameLenBottom [] +found : int @SameLen("p4") [] +required: int @SameLenBottom [] ErrorOrders.java:29:37: compiler.err.proc.messager: [argument] incompatible argument for parameter p5 of test4. found : @UnknownVal int -required: int +required: @BottomVal int ErrorOrders.java:29:42: compiler.err.proc.messager: [argument] incompatible argument for parameter p3 of test4. found : @UnknownVal int @UnknownVal [] -required: @UnknownVal int [] +required: @UnknownVal int @BottomVal [] ErrorOrders.java:29:46: compiler.err.proc.messager: [argument] incompatible argument for parameter p4 of test4. -found : @SameLenUnknown int @SameLen("p4") [] -required: @SameLenUnknown int @SameLenBottom [] +found : int @SameLen("p4") [] +required: int @SameLenBottom [] ErrorOrders.java:29:50: compiler.err.proc.messager: [argument] incompatible argument for parameter p5 of test4. found : @UnknownVal int -required: int +required: @BottomVal int ErrorOrders.java:33:43: compiler.err.proc.messager: [expression.unparsable] Expression invalid in dependent type annotation: [error for expression: This isn't an expression; error: Invalid 'This isn't an expression' because the expression did not parse. Error message: Encountered unexpected token: "isn" ] ErrorOrders.java:33:51: compiler.err.proc.messager: [assignment] incompatible types in assignment. found : @UpperBoundLiteral(0) int required: @LTLengthOf("[error for expression: This isn't an expression; error: Invalid 'This isn't an expression' because the expression did not parse. Error message: Encountered unexpected token: "isn" ]") int ErrorOrders.java:36:9: compiler.err.proc.messager: [array.access.unsafe.low] Potentially unsafe array access: the index could be negative. -found : @LowerBoundUnknown int +found : int required: an integer >= 0 (@NonNegative or @Positive) ErrorOrders.java:36:9: compiler.err.proc.messager: [array.access.unsafe.high] Potentially unsafe array access: the index could be larger than the array's bound -found : @UpperBoundUnknown int +found : int required: @IndexFor("a") or @LTLengthOf("a") -- an integer less than a's length ErrorOrders.java:42:41: compiler.err.proc.messager: [expression.unparsable] Expression invalid in dependent type annotation: [error for expression: This isn't an expression; error: Invalid 'This isn't an expression' because the expression did not parse. Error message: Encountered unexpected token: "isn" ] ErrorOrders.java:42:49: compiler.err.proc.messager: [assignment] incompatible types in assignment. found : @UpperBoundLiteral(0) int required: @LTLengthOf("[error for expression: This isn't an expression; error: Invalid 'This isn't an expression' because the expression did not parse. Error message: Encountered unexpected token: "isn" ]") int ErrorOrders.java:45:7: compiler.err.proc.messager: [array.access.unsafe.low] Potentially unsafe array access: the index could be negative. -found : @LowerBoundUnknown int +found : int required: an integer >= 0 (@NonNegative or @Positive) ErrorOrders.java:45:7: compiler.err.proc.messager: [array.access.unsafe.high] Potentially unsafe array access: the index could be larger than the array's bound -found : @UpperBoundUnknown int +found : int required: @IndexFor("a") or @LTLengthOf("a") -- an integer less than a's length ErrorOrders.java:55:29: compiler.err.proc.messager: [assignment] incompatible types in assignment. found : @UpperBoundLiteral(0) int @@ -96,45 +96,45 @@ ErrorOrders.java:56:51: compiler.err.proc.messager: [assignment] incompatible ty found : @LTLengthOf("p2") int required: @LTLengthOf("[error for expression: This isn't an expression; error: Invalid 'This isn't an expression' because the expression did not parse. Error message: Encountered unexpected token: "isn" ]") int ErrorOrders.java:61:11: compiler.err.proc.messager: [argument] incompatible argument for parameter p1 of test4. -found : @LowerBoundUnknown int +found : int required: @GTENegativeOne int ErrorOrders.java:61:11: compiler.err.proc.messager: [argument] incompatible argument for parameter p1 of test4. -found : @UpperBoundUnknown int +found : int required: @UpperBoundBottom int ErrorOrders.java:61:20: compiler.err.proc.messager: [argument] incompatible argument for parameter p2 of test4. -found : @LowerBoundUnknown int +found : int required: @GTENegativeOne int ErrorOrders.java:61:20: compiler.err.proc.messager: [argument] incompatible argument for parameter p2 of test4. -found : @UpperBoundUnknown int +found : int required: @UpperBoundBottom int ErrorOrders.java:61:21: compiler.err.proc.messager: [argument] incompatible argument for parameter p1 of test4. -found : @LowerBoundUnknown int +found : int required: @GTENegativeOne int ErrorOrders.java:61:21: compiler.err.proc.messager: [argument] incompatible argument for parameter p1 of test4. -found : @UpperBoundUnknown int +found : int required: @UpperBoundBottom int ErrorOrders.java:61:25: compiler.err.proc.messager: [argument] incompatible argument for parameter p2 of test4. -found : @LowerBoundUnknown int +found : int required: @GTENegativeOne int ErrorOrders.java:61:25: compiler.err.proc.messager: [argument] incompatible argument for parameter p2 of test4. -found : @UpperBoundUnknown int +found : int required: @UpperBoundBottom int ErrorOrders.java:61:29: compiler.err.proc.messager: [argument] incompatible argument for parameter p3 of test4. found : @UnknownVal int @UnknownVal [] -required: @UnknownVal int [] +required: @UnknownVal int @BottomVal [] ErrorOrders.java:61:33: compiler.err.proc.messager: [argument] incompatible argument for parameter p4 of test4. -found : @SameLenUnknown int @SameLen("p4") [] -required: @SameLenUnknown int @SameLenBottom [] +found : int @SameLen("p4") [] +required: int @SameLenBottom [] ErrorOrders.java:61:37: compiler.err.proc.messager: [argument] incompatible argument for parameter p5 of test4. found : @UnknownVal int -required: int +required: @BottomVal int ErrorOrders.java:61:42: compiler.err.proc.messager: [argument] incompatible argument for parameter p3 of test4. found : @UnknownVal int @UnknownVal [] -required: @UnknownVal int [] +required: @UnknownVal int @BottomVal [] ErrorOrders.java:61:46: compiler.err.proc.messager: [argument] incompatible argument for parameter p4 of test4. -found : @SameLenUnknown int @SameLen("p4") [] -required: @SameLenUnknown int @SameLenBottom [] +found : int @SameLen("p4") [] +required: int @SameLenBottom [] ErrorOrders.java:61:50: compiler.err.proc.messager: [argument] incompatible argument for parameter p5 of test4. found : @UnknownVal int -required: int +required: @BottomVal int 49 errors From a850ee94f197000609341ccea330482cc0a6abb7 Mon Sep 17 00:00:00 2001 From: Martin Kellogg Date: Thu, 30 Jun 2022 15:13:37 -0700 Subject: [PATCH 3/6] fix another jtreg test --- checker/jtreg/sortwarnings/OrderOfCheckers.out | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/checker/jtreg/sortwarnings/OrderOfCheckers.out b/checker/jtreg/sortwarnings/OrderOfCheckers.out index 186ba72a7ca..bde21c38c5b 100644 --- a/checker/jtreg/sortwarnings/OrderOfCheckers.out +++ b/checker/jtreg/sortwarnings/OrderOfCheckers.out @@ -1,16 +1,16 @@ OrderOfCheckers.java:12:95: compiler.err.proc.messager: [[value, allcheckers]:assignment] incompatible types in assignment. found : @UnknownVal int @UnknownVal [] -required: @UnknownVal int [] +required: @UnknownVal int @BottomVal [] OrderOfCheckers.java:12:95: compiler.err.proc.messager: [[index, searchindex, allcheckers]:assignment] incompatible types in assignment. -found : @SearchIndexUnknown int @SearchIndexUnknown [] -required: @SearchIndexBottom int @SearchIndexUnknown [] +found : int [] +required: @SearchIndexBottom int [] OrderOfCheckers.java:12:95: compiler.err.proc.messager: [[index, samelen, allcheckers]:assignment] incompatible types in assignment. -found : @SameLenUnknown int @SameLen("y") [] -required: @SameLenUnknown int @SameLenBottom [] +found : int @SameLen("y") [] +required: int @SameLenBottom [] OrderOfCheckers.java:12:95: compiler.err.proc.messager: [[index, lowerbound, allcheckers]:assignment] incompatible types in assignment. -found : @LowerBoundUnknown int @LowerBoundUnknown [] -required: @GTENegativeOne int @LowerBoundUnknown [] +found : int [] +required: @GTENegativeOne int [] OrderOfCheckers.java:12:95: compiler.err.proc.messager: [[index, upperbound, allcheckers]:assignment] incompatible types in assignment. -found : @UpperBoundUnknown int @UpperBoundUnknown [] -required: @UpperBoundBottom int @UpperBoundUnknown [] +found : int [] +required: @UpperBoundBottom int [] 5 errors From 9f9bc53d7eb5562d9126638dceaaf724b5ee26d5 Mon Sep 17 00:00:00 2001 From: Martin Kellogg Date: Wed, 6 Jul 2022 15:14:27 -0400 Subject: [PATCH 4/6] factor out getting the invisible qualifier names into a static method --- ...holeProgramInferenceJavaParserStorage.java | 26 +++++++++++++------ 1 file changed, 18 insertions(+), 8 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java index a4f4e2a01b7..ee3f6334af5 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java @@ -114,6 +114,23 @@ public class WholeProgramInferenceJavaParserStorage /** Whether the {@code -AinferOutputOriginal} option was supplied to the checker. */ private final boolean inferOutputOriginal; + /** + * Returns the names of all qualifiers supported by the type factory passed as input that are + * marked with {@link InvisibleQualifier}. + * + * @param atypeFactory a type factory + * @return the names of every invisible qualifier supported by {@code atypeFactory} + */ + public static Set getInvisibleQualifierNames(AnnotatedTypeFactory atypeFactory) { + return atypeFactory.getSupportedTypeQualifiers().stream() + .filter( + qual -> + Arrays.stream(qual.getAnnotations()) + .anyMatch(anno -> anno.annotationType() == InvisibleQualifier.class)) + .map(Class::getCanonicalName) + .collect(Collectors.toSet()); + } + /** * Constructs a new {@code WholeProgramInferenceJavaParser} that has not yet inferred any * annotations. @@ -792,14 +809,7 @@ private void writeAjavaFile(String outputPath, CompilationUnitAnnos root) { // LexicalPreservingPrinter.print(root.declaration, writer); // Do not print invisible qualifiers, to avoid cluttering the output. - Set invisibleQualifierNames = - atypeFactory.getSupportedTypeQualifiers().stream() - .filter( - qual -> - Arrays.stream(qual.getAnnotations()) - .anyMatch(anno -> anno.annotationType() == InvisibleQualifier.class)) - .map(Class::getCanonicalName) - .collect(Collectors.toSet()); + Set invisibleQualifierNames = getInvisibleQualifierNames(); DefaultPrettyPrinter prettyPrinter = new DefaultPrettyPrinter() { @Override From 566045b3190b9cba14f8f8dd171ac708ef3ee946 Mon Sep 17 00:00:00 2001 From: Martin Kellogg Date: Wed, 6 Jul 2022 15:47:48 -0400 Subject: [PATCH 5/6] fix typo --- .../WholeProgramInferenceJavaParserStorage.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java index ee3f6334af5..b10a1377648 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java @@ -809,7 +809,7 @@ private void writeAjavaFile(String outputPath, CompilationUnitAnnos root) { // LexicalPreservingPrinter.print(root.declaration, writer); // Do not print invisible qualifiers, to avoid cluttering the output. - Set invisibleQualifierNames = getInvisibleQualifierNames(); + Set invisibleQualifierNames = getInvisibleQualifierNames(this.atypeFactory); DefaultPrettyPrinter prettyPrinter = new DefaultPrettyPrinter() { @Override From f474b5b7ac314d691e514f18c6bbacdb3531f5b2 Mon Sep 17 00:00:00 2001 From: Martin Kellogg Date: Thu, 7 Jul 2022 10:27:47 -0400 Subject: [PATCH 6/6] factor out isInvisible, too --- .../WholeProgramInferenceJavaParserStorage.java | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java index b10a1377648..922f568c5a7 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java @@ -36,6 +36,7 @@ import java.io.FileNotFoundException; import java.io.FileWriter; import java.io.IOException; +import java.lang.annotation.Annotation; import java.nio.file.Files; import java.nio.file.Paths; import java.util.ArrayList; @@ -123,14 +124,22 @@ public class WholeProgramInferenceJavaParserStorage */ public static Set getInvisibleQualifierNames(AnnotatedTypeFactory atypeFactory) { return atypeFactory.getSupportedTypeQualifiers().stream() - .filter( - qual -> - Arrays.stream(qual.getAnnotations()) - .anyMatch(anno -> anno.annotationType() == InvisibleQualifier.class)) + .filter(WholeProgramInferenceJavaParserStorage::isInvisible) .map(Class::getCanonicalName) .collect(Collectors.toSet()); } + /** + * Is the definition of the given annotation class annotated with {@link InvisibleQualifier}? + * + * @param qual an annotation class + * @return true iff {@code qual} is meta-annotated with {@link InvisibleQualifier} + */ + public static boolean isInvisible(Class qual) { + return Arrays.stream(qual.getAnnotations()) + .anyMatch(anno -> anno.annotationType() == InvisibleQualifier.class); + } + /** * Constructs a new {@code WholeProgramInferenceJavaParser} that has not yet inferred any * annotations.