From d003765e726a592b7b820200168e98a5b4ede9e3 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sun, 4 Apr 2021 12:09:45 -0700 Subject: [PATCH 01/12] Run WPI on plume-util --- checker/bin-devel/wpi-plumelib/test-wpi-plumelib.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/checker/bin-devel/wpi-plumelib/test-wpi-plumelib.sh b/checker/bin-devel/wpi-plumelib/test-wpi-plumelib.sh index 28f3955c3264..c445cf22e3a4 100755 --- a/checker/bin-devel/wpi-plumelib/test-wpi-plumelib.sh +++ b/checker/bin-devel/wpi-plumelib/test-wpi-plumelib.sh @@ -87,5 +87,6 @@ test_wpi_plume_lib bibtex-clean "formatter,index,interning,lock,nullness,re test_wpi_plume_lib html-pretty-print "formatter,index,interning,lock,nullness,regex,signature" test_wpi_plume_lib icalavailable "formatter,index,interning,lock,nullness,regex,signature,initializedfields" test_wpi_plume_lib lookup "formatter,index,interning,lock,nullness,regex,signature" +test_wpi_plume_lib plume-util "formatter,index,interning,lock,nullness,regex,signature,initializedfields" echo "exiting test-wpi-plumelib.sh" From 5993383342ae3a69294581213d5b8e5521b546a3 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sun, 4 Apr 2021 21:49:03 -0700 Subject: [PATCH 02/12] Use setwise operations --- .../LessThanAnnotatedTypeFactory.java | 14 ++--- .../SearchIndexAnnotatedTypeFactory.java | 6 +-- .../initialization/InitializationStore.java | 7 ++- .../AccumulationAnnotatedTypeFactory.java | 4 +- .../MethodValAnnotatedTypeFactory.java | 4 +- .../value/ValueAnnotatedTypeFactory.java | 5 +- .../common/value/ValueQualifierHierarchy.java | 42 +++++++-------- .../javacutil/SystemUtil.java | 52 +++++++++++++++++++ 8 files changed, 90 insertions(+), 44 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/index/inequality/LessThanAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/index/inequality/LessThanAnnotatedTypeFactory.java index c5bfe2ad7a92..7694cde8f153 100644 --- a/checker/src/main/java/org/checkerframework/checker/index/inequality/LessThanAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/index/inequality/LessThanAnnotatedTypeFactory.java @@ -4,7 +4,6 @@ import com.sun.source.tree.Tree; import com.sun.source.util.TreePath; import java.lang.annotation.Annotation; -import java.util.ArrayList; import java.util.Arrays; import java.util.Collections; import java.util.LinkedHashSet; @@ -37,6 +36,7 @@ import org.checkerframework.framework.util.dependenttypes.DependentTypesHelper; import org.checkerframework.javacutil.AnnotationBuilder; import org.checkerframework.javacutil.AnnotationUtils; +import org.checkerframework.javacutil.SystemUtil; import org.checkerframework.javacutil.TreeUtils; /** The type factory for the Less Than Checker. */ @@ -126,10 +126,8 @@ public AnnotationMirror leastUpperBound(AnnotationMirror a1, AnnotationMirror a2 List a1List = getLessThanExpressions(a1); List a2List = getLessThanExpressions(a2); - List lub = new ArrayList<>(a1List); - lub.retainAll(a2List); - - return createLessThanQualifier(lub); + a1List.retainAll(a2List); // intersection + return createLessThanQualifier(a1List); } @Override @@ -142,10 +140,8 @@ public AnnotationMirror greatestLowerBound(AnnotationMirror a1, AnnotationMirror List a1List = getLessThanExpressions(a1); List a2List = getLessThanExpressions(a2); - List glb = new ArrayList<>(a1List); - glb.addAll(a2List); - - return createLessThanQualifier(glb); + SystemUtil.addWithoutDuplicates(a1List, a2List); // union + return createLessThanQualifier(a1List); } } diff --git a/checker/src/main/java/org/checkerframework/checker/index/searchindex/SearchIndexAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/index/searchindex/SearchIndexAnnotatedTypeFactory.java index 0478357221b4..cc4983cd4bb5 100644 --- a/checker/src/main/java/org/checkerframework/checker/index/searchindex/SearchIndexAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/index/searchindex/SearchIndexAnnotatedTypeFactory.java @@ -171,16 +171,16 @@ public AnnotationMirror leastUpperBound(AnnotationMirror a1, AnnotationMirror a2 // Each annotation is either NegativeIndexFor or SearchIndexFor. List arrayIntersection = getValueElement(a1); - arrayIntersection.retainAll(getValueElement(a2)); + arrayIntersection.retainAll(getValueElement(a2)); // intersection if (arrayIntersection.isEmpty()) { return UNKNOWN; } if (areSameByClass(a1, SearchIndexFor.class) || areSameByClass(a2, SearchIndexFor.class)) { - return createSearchIndexFor(Arrays.asList(arrayIntersection.toArray(new String[0]))); + return createSearchIndexFor(arrayIntersection); } else { - return createNegativeIndexFor(Arrays.asList(arrayIntersection.toArray(new String[0]))); + return createNegativeIndexFor(arrayIntersection); } } diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java index 23757ae2077d..8405e5bedcc2 100644 --- a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java +++ b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationStore.java @@ -208,8 +208,11 @@ public S leastUpperBound(S other) { // Set intersection for invariantFields. for (Map.Entry e : invariantFields.entrySet()) { - if (other.invariantFields.containsKey(e.getKey())) { - result.invariantFields.put(e.getKey(), e.getValue()); + FieldAccess key = e.getKey(); + if (other.invariantFields.containsKey(key)) { + // TODO: Is the value other.invariantFields.get(key) the same as e.getValue()? Should the + // two values be lubbed? + result.invariantFields.put(key, e.getValue()); } } // Add invariant annotation. diff --git a/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationAnnotatedTypeFactory.java index dba297ab6f81..cb43774f9865 100644 --- a/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationAnnotatedTypeFactory.java @@ -412,7 +412,7 @@ public AnnotationMirror greatestLowerBound( if (a2Val.containsAll(a1Val)) { return a2; } - a1Val.addAll(a2Val); + a1Val.addAll(a2Val); // union return createAccumulatorAnnotation(a1Val); } @@ -457,7 +457,7 @@ public AnnotationMirror leastUpperBound(final AnnotationMirror a1, final Annotat if (a2Val.containsAll(a1Val)) { return a1; } - a1Val.retainAll(a2Val); + a1Val.retainAll(a2Val); // intersection return createAccumulatorAnnotation(a1Val); } diff --git a/framework/src/main/java/org/checkerframework/common/reflection/MethodValAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/common/reflection/MethodValAnnotatedTypeFactory.java index 97a9449884bb..850bb0d13282 100644 --- a/framework/src/main/java/org/checkerframework/common/reflection/MethodValAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/common/reflection/MethodValAnnotatedTypeFactory.java @@ -225,7 +225,7 @@ protected MethodValQualifierHierarchy( List a2Sigs = getListOfMethodSignatures(a2); Set lubSigs = new HashSet<>(a1Sigs); - lubSigs.addAll(a2Sigs); + lubSigs.addAll(a2Sigs); // union AnnotationMirror result = createMethodVal(lubSigs); return result; @@ -246,7 +246,7 @@ protected MethodValQualifierHierarchy( List a2Sigs = getListOfMethodSignatures(a2); Set lubSigs = new HashSet<>(a1Sigs); - lubSigs.retainAll(a2Sigs); + lubSigs.retainAll(a2Sigs); // intersection AnnotationMirror result = createMethodVal(lubSigs); return result; diff --git a/framework/src/main/java/org/checkerframework/common/value/ValueAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/common/value/ValueAnnotatedTypeFactory.java index 19980dcef16a..b96c73b7ba1b 100644 --- a/framework/src/main/java/org/checkerframework/common/value/ValueAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/common/value/ValueAnnotatedTypeFactory.java @@ -765,6 +765,7 @@ public AnnotationMirror createDoubleValAnnotation(List values) { if (values.size() > MAX_VALUES) { return UNKNOWNVAL; } else { + Collections.sort(values); AnnotationBuilder builder = new AnnotationBuilder(processingEnv, DoubleVal.class); builder.setValue("value", values); return builder.build(); @@ -917,9 +918,7 @@ public AnnotationMirror createDoubleAnnotation(List values) { if (values.size() > MAX_VALUES) { return UNKNOWNVAL; } else { - List doubleValues = - CollectionsPlume.mapList((Double value) -> (double) value, values); - return createDoubleValAnnotation(doubleValues); + return createDoubleValAnnotation(values); } } diff --git a/framework/src/main/java/org/checkerframework/common/value/ValueQualifierHierarchy.java b/framework/src/main/java/org/checkerframework/common/value/ValueQualifierHierarchy.java index 46433f13d371..d4007c2c4890 100644 --- a/framework/src/main/java/org/checkerframework/common/value/ValueQualifierHierarchy.java +++ b/framework/src/main/java/org/checkerframework/common/value/ValueQualifierHierarchy.java @@ -11,7 +11,7 @@ import org.checkerframework.framework.type.ElementQualifierHierarchy; import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.BugInCF; -import org.plumelib.util.CollectionsPlume; +import org.checkerframework.javacutil.SystemUtil; /** The qualifier hierarchy for the Value type system. */ final class ValueQualifierHierarchy extends ElementQualifierHierarchy { @@ -231,33 +231,29 @@ public AnnotationMirror leastUpperBound(AnnotationMirror a1, AnnotationMirror a2 Range range2 = atypeFactory.getRange(a2); return atypeFactory.createArrayLenRangeAnnotation(range1.union(range2)); case ValueAnnotatedTypeFactory.INTVAL_NAME: - List longs1 = atypeFactory.getIntValues(a1); - List longs2 = atypeFactory.getIntValues(a2); - return atypeFactory.createIntValAnnotation(CollectionsPlume.concatenate(longs1, longs2)); + List longs = atypeFactory.getIntValues(a1); + SystemUtil.addWithoutDuplicates(longs, atypeFactory.getIntValues(a2)); + return atypeFactory.createIntValAnnotation(longs); case ValueAnnotatedTypeFactory.ARRAYLEN_NAME: - List arrayLens1 = atypeFactory.getArrayLength(a1); - List arrayLens2 = atypeFactory.getArrayLength(a2); - return atypeFactory.createArrayLenAnnotation( - CollectionsPlume.concatenate(arrayLens1, arrayLens2)); + List arrayLens = atypeFactory.getArrayLength(a1); + SystemUtil.addWithoutDuplicates(arrayLens, atypeFactory.getArrayLength(a2)); + return atypeFactory.createArrayLenAnnotation(arrayLens); case ValueAnnotatedTypeFactory.STRINGVAL_NAME: - List strings1 = atypeFactory.getStringValues(a1); - List strings2 = atypeFactory.getStringValues(a2); - return atypeFactory.createStringAnnotation( - CollectionsPlume.concatenate(strings1, strings2)); + List strings = atypeFactory.getStringValues(a1); + SystemUtil.addWithoutDuplicates(strings, atypeFactory.getStringValues(a2)); + return atypeFactory.createStringAnnotation(strings); case ValueAnnotatedTypeFactory.BOOLVAL_NAME: - List bools1 = atypeFactory.getBooleanValues(a1); - List bools2 = atypeFactory.getBooleanValues(a2); - return atypeFactory.createBooleanAnnotation(CollectionsPlume.concatenate(bools1, bools2)); + List bools = atypeFactory.getBooleanValues(a1); + SystemUtil.addWithoutDuplicates(bools, atypeFactory.getBooleanValues(a2)); + return atypeFactory.createBooleanAnnotation(bools); case ValueAnnotatedTypeFactory.DOUBLEVAL_NAME: - List doubles1 = atypeFactory.getDoubleValues(a1); - List doubles2 = atypeFactory.getDoubleValues(a2); - return atypeFactory.createDoubleAnnotation( - CollectionsPlume.concatenate(doubles1, doubles2)); + List doubles = atypeFactory.getDoubleValues(a1); + SystemUtil.addWithoutDuplicates(doubles, atypeFactory.getDoubleValues(a2)); + return atypeFactory.createDoubleAnnotation(doubles); case ValueAnnotatedTypeFactory.MATCHES_REGEX_NAME: - List<@Regex String> regexes1 = atypeFactory.getMatchesRegexValues(a1); - List<@Regex String> regexes2 = atypeFactory.getMatchesRegexValues(a2); - return atypeFactory.createMatchesRegexAnnotation( - CollectionsPlume.concatenate(regexes1, regexes2)); + List<@Regex String> regexes = atypeFactory.getMatchesRegexValues(a1); + SystemUtil.addWithoutDuplicates(regexes, atypeFactory.getMatchesRegexValues(a2)); + return atypeFactory.createMatchesRegexAnnotation(regexes); default: throw new BugInCF("default case: %s %s %s%n", qual1, a1, a2); } diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/SystemUtil.java b/javacutil/src/main/java/org/checkerframework/javacutil/SystemUtil.java index f3ebfd4d8879..202e17e84460 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/SystemUtil.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/SystemUtil.java @@ -157,6 +157,58 @@ public static int getJreVersion() { /// Array and collection methods /// + /** + * Returns a list that contains all the distinct elements of the two lists: that is, the union of + * the two arguments. + * + *

For very short lists, this is likely more efficient than creating a set and converting back + * to a list. + * + * @param list1 a list + * @param list2 a list + * @return a list that contains all the distinct elements of the two lists + */ + public static List union(List list1, List list2) { + List result = new ArrayList<>(list1.size() + list2.size()); + addWithoutDuplicates(result, list1); + addWithoutDuplicates(result, list2); + return result; + } + + /** + * Adds, to dest, all the elements of source that are not already in dest. + * + *

For very short lists, this is likely more efficient than creating a set and converting back + * to a list. + * + * @param dest a list to add to + * @param source a list of elements to add + */ + public static void addWithoutDuplicates(List dest, List source) { + for (T elt : source) { + if (!dest.contains(elt)) { + dest.add(elt); + } + } + } + + /** + * Returns a list that contains all the elements that are in both lists: that is, the set + * difference of the two arguments. + * + *

For very short lists, this is likely more efficient than creating a set and converting back + * to a list. + * + * @param list1 a list + * @param list2 a list + * @return a list that contains all the elements of {@code list1} that are not in {@code list2} + */ + public static List intersection(List list1, List list2) { + List result = new ArrayList<>(list1); + result.retainAll(list2); + return result; + } + /** * Concatenates two arrays. Can be invoked varargs-style. * From b13d92aef1463e6d1b89acae8788ce6105cbfb29 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sun, 4 Apr 2021 22:36:31 -0700 Subject: [PATCH 03/12] Add Javadoc --- .../main/java/org/checkerframework/javacutil/SystemUtil.java | 3 +++ 1 file changed, 3 insertions(+) diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/SystemUtil.java b/javacutil/src/main/java/org/checkerframework/javacutil/SystemUtil.java index 202e17e84460..c3933724549a 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/SystemUtil.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/SystemUtil.java @@ -164,6 +164,7 @@ public static int getJreVersion() { *

For very short lists, this is likely more efficient than creating a set and converting back * to a list. * + * @param the type of the list elements * @param list1 a list * @param list2 a list * @return a list that contains all the distinct elements of the two lists @@ -181,6 +182,7 @@ public static List union(List list1, List list2) { *

For very short lists, this is likely more efficient than creating a set and converting back * to a list. * + * @param the type of the list elements * @param dest a list to add to * @param source a list of elements to add */ @@ -199,6 +201,7 @@ public static void addWithoutDuplicates(List dest, List sour *

For very short lists, this is likely more efficient than creating a set and converting back * to a list. * + * @param the type of the list elements * @param list1 a list * @param list2 a list * @return a list that contains all the elements of {@code list1} that are not in {@code list2} From f778735242342ee118b751a6e095727018d6786a Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sun, 4 Apr 2021 22:51:15 -0700 Subject: [PATCH 04/12] Suppress a warning --- .../main/java/org/checkerframework/javacutil/SystemUtil.java | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/SystemUtil.java b/javacutil/src/main/java/org/checkerframework/javacutil/SystemUtil.java index c3933724549a..28970d185b22 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/SystemUtil.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/SystemUtil.java @@ -186,6 +186,10 @@ public static List union(List list1, List list2) { * @param dest a list to add to * @param source a list of elements to add */ + @SuppressWarnings( + "nullness:argument.type.incompatible" // true positive: `dest` might be incompatible with + // null and `source` might contain null. + ) public static void addWithoutDuplicates(List dest, List source) { for (T elt : source) { if (!dest.contains(elt)) { From f7cde82bcf3ad831e66645247cc8ea2be1ee833c Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Mon, 5 Apr 2021 09:14:22 -0700 Subject: [PATCH 05/12] Don't infer from recursive calls --- docs/manual/inference.tex | 8 ++- .../WholeProgramInferenceImplementation.java | 65 +++++++++++++++++-- .../framework/type/AnnotatedTypeFactory.java | 2 +- 3 files changed, 67 insertions(+), 8 deletions(-) diff --git a/docs/manual/inference.tex b/docs/manual/inference.tex index e88108f82581..114becbe1ecb 100644 --- a/docs/manual/inference.tex +++ b/docs/manual/inference.tex @@ -438,6 +438,12 @@ to \ passes \ as the argument. Then the tool will infer that \'s parameter has \<@Nullable> type. +If you run whole-program inference on a library that contains mutually +recursive routines, and there are no non-recursive calls to the routines, +then whole-program inference may run a long time and eventually produce +incorrect results. In this case, write type annotations on the formal +parameters of one of the routines. + Whole-program inference is a ``forward analysis''. % This might change in the future. @@ -478,7 +484,7 @@ \refqualclass{framework/qual}{IgnoreInWholeProgramInference}. Whole-program inference, for a type-checker other than the Nullness Checker, -ignores (pseudo-)assignments where the right-hand-side is the \ literal. +ignores assignments and pseudo-assignments where the right-hand-side is the \ literal. \subsectionAndLabel{Manually checking whole-program inference results}{whole-program-inference-manual-checking} diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java index 1aa1faed7702..3084e31a8014 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java @@ -1,6 +1,8 @@ package org.checkerframework.common.wholeprograminference; import com.sun.source.tree.ClassTree; +import com.sun.source.tree.IdentifierTree; +import com.sun.source.tree.MemberSelectTree; import com.sun.source.tree.MethodTree; import com.sun.source.tree.Tree; import com.sun.tools.javac.code.Symbol.ClassSymbol; @@ -12,6 +14,7 @@ import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.Name; import javax.lang.model.element.TypeElement; import javax.lang.model.element.VariableElement; import javax.lang.model.util.ElementFilter; @@ -42,6 +45,7 @@ import org.checkerframework.framework.util.dependenttypes.DependentTypesHelper; import org.checkerframework.javacutil.BugInCF; import org.checkerframework.javacutil.ElementUtils; +import org.checkerframework.javacutil.TreePathUtil; import org.checkerframework.javacutil.TreeUtils; /** @@ -50,8 +54,8 @@ * {@link WholeProgramInferenceStorage} to store annotations and to create output files. * *

This class does not perform inference for an element if the element has explicit annotations. - * That is, calling an update* method on an explicitly annotated field, method return, or method - * parameter has no effect. + * That is, calling an {@code update*} method on an explicitly annotated field, method return, or + * method parameter has no effect. * *

In addition, whole program inference ignores inferred types in a few scenarios. When * discovering a use, WPI ignores an inferred type if: @@ -152,11 +156,60 @@ public void updateFromMethodInvocation( return; } + // Don't infer formal parameter types from recursive calls. + // + // When performing WPI on a library, if there are no external calls (only recursive calls), then + // each iteration of WPI would make the formal parameter types more restrictive, leading to an + // infinite (or very long) loop. + // + // Consider + // void myMethod(int x) { ... myMethod(x-1) ... }` + // On one iteration, if x has type IntRange(to=100), the recursive call's argument has type + // IntRange(to=99). If that is the only call to `MyMethod`, then the formal parameter type + // would be updated. On the next iteration it would be refined again to @IntRange(to=98), and + // so forth. A recursive call should never restrict a formal parameter type. + if (isRecursiveCall(methodInvNode)) { + return; + } + List arguments = methodInvNode.getArguments(); updateInferredExecutableParameterTypes(methodElt, arguments); updateContracts(Analysis.BeforeOrAfter.BEFORE, methodElt, store); } + /** + * Returns true if the given call is a recursive call. + * + * @param methodInvNode a method invocation + * @return true if the given call is a recursive call + */ + private boolean isRecursiveCall(MethodInvocationNode methodInvNode) { + // TODO: This tests only the name. It should also ensure that the call isn't to an overload or + // a completely unrelated method of the same name. + + MethodTree enclosingMethod = TreePathUtil.enclosingMethod(methodInvNode.getTreePath()); + if (enclosingMethod == null) { + return false; + } + + Tree invoked = methodInvNode.getTree().getMethodSelect(); + Name invokedMethodName; + switch (invoked.getKind()) { + case IDENTIFIER: + invokedMethodName = ((IdentifierTree) invoked).getName(); + break; + case MEMBER_SELECT: + invokedMethodName = ((MemberSelectTree) invoked).getIdentifier(); + break; + default: + throw new BugInCF( + "What invoked method? [%s] %s", + invoked.getKind(), TreeUtils.toStringTruncated(invoked, 65)); + } + + return enclosingMethod.getName().contentEquals(invokedMethodName); + } + /** * Updates inferred parameter types based on a call to a method or constructor. * @@ -501,8 +554,8 @@ public void addMethodDeclarationAnnotation(ExecutableElement methodElt, Annotati * @param defLoc the location where the annotation will be added * @param rhsATM the RHS of the annotated type on the source code * @param lhsATM the LHS of the annotated type on the source code - * @param file path to the annotation file containing the executable; used for marking the scene - * as modified (needing to be written to disk) + * @param file the annotation file containing the executable; used for marking the scene as + * modified (needing to be written to disk) */ protected void updateAnnotationSet( T annotationsToUpdate, @@ -529,8 +582,8 @@ protected void updateAnnotationSet( * @param defLoc the location where the annotation will be added * @param rhsATM the RHS of the annotated type on the source code * @param lhsATM the LHS of the annotated type on the source code - * @param file path to the annotation file containing the executable; used for marking the scene - * as modified (needing to be written to disk) + * @param file annotation file containing the executable; used for marking the scene as modified + * (needing to be written to disk) * @param ignoreIfAnnotated if true, don't update any type that is explicitly annotated in the * source code */ diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java index 147e75e05056..2545c7a527e1 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -1981,7 +1981,7 @@ public AnnotatedNullType getAnnotatedNullType(Set an * @return the innermost enclosing method or class tree of {@code tree}, or {@code null} if {@code * tree} is inside an annotation */ - protected @Nullable Tree getEnclosingClassOrMethod(Tree tree) { + public @Nullable Tree getEnclosingClassOrMethod(Tree tree) { TreePath path = getPath(tree); Tree enclosing = TreePathUtil.enclosingOfKind(path, classMethodAnnotationKinds); if (enclosing != null) { From 29ebb3d8f6beb9b31f51675ea498f34ae9eaccd3 Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Mon, 5 Apr 2021 13:11:15 -0700 Subject: [PATCH 06/12] Check elements and receivers instead of method names. --- .../WholeProgramInferenceImplementation.java | 32 +++++++------------ 1 file changed, 11 insertions(+), 21 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java index 3084e31a8014..db66ac0c70f7 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java @@ -1,8 +1,6 @@ package org.checkerframework.common.wholeprograminference; import com.sun.source.tree.ClassTree; -import com.sun.source.tree.IdentifierTree; -import com.sun.source.tree.MemberSelectTree; import com.sun.source.tree.MethodTree; import com.sun.source.tree.Tree; import com.sun.tools.javac.code.Symbol.ClassSymbol; @@ -14,18 +12,19 @@ import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; import javax.lang.model.element.ExecutableElement; -import javax.lang.model.element.Name; import javax.lang.model.element.TypeElement; import javax.lang.model.element.VariableElement; import javax.lang.model.util.ElementFilter; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.dataflow.analysis.Analysis; +import org.checkerframework.dataflow.cfg.node.ClassNameNode; import org.checkerframework.dataflow.cfg.node.FieldAccessNode; import org.checkerframework.dataflow.cfg.node.LocalVariableNode; import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; import org.checkerframework.dataflow.cfg.node.Node; import org.checkerframework.dataflow.cfg.node.ObjectCreationNode; import org.checkerframework.dataflow.cfg.node.ReturnNode; +import org.checkerframework.dataflow.cfg.node.ThisNode; import org.checkerframework.dataflow.expression.ClassName; import org.checkerframework.dataflow.expression.FieldAccess; import org.checkerframework.dataflow.expression.ThisReference; @@ -184,30 +183,21 @@ public void updateFromMethodInvocation( * @return true if the given call is a recursive call */ private boolean isRecursiveCall(MethodInvocationNode methodInvNode) { - // TODO: This tests only the name. It should also ensure that the call isn't to an overload or - // a completely unrelated method of the same name. - MethodTree enclosingMethod = TreePathUtil.enclosingMethod(methodInvNode.getTreePath()); if (enclosingMethod == null) { return false; } - - Tree invoked = methodInvNode.getTree().getMethodSelect(); - Name invokedMethodName; - switch (invoked.getKind()) { - case IDENTIFIER: - invokedMethodName = ((IdentifierTree) invoked).getName(); - break; - case MEMBER_SELECT: - invokedMethodName = ((MemberSelectTree) invoked).getIdentifier(); - break; - default: - throw new BugInCF( - "What invoked method? [%s] %s", - invoked.getKind(), TreeUtils.toStringTruncated(invoked, 65)); + ExecutableElement methodInvocEle = TreeUtils.elementFromUse(methodInvNode.getTree()); + ExecutableElement methodDeclEle = TreeUtils.elementFromDeclaration(enclosingMethod); + if (!methodDeclEle.equals(methodInvocEle)) { + return false; } - return enclosingMethod.getName().contentEquals(invokedMethodName); + if (ElementUtils.isStatic(methodDeclEle)) { + return methodInvNode.getTarget().getReceiver() instanceof ClassNameNode; + } else { + return methodInvNode.getTarget().getMethod() instanceof ThisNode; + } } /** From 7d70c5cf4b55c6521a6966c9a224719915f6c920 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Mon, 5 Apr 2021 15:07:39 -0700 Subject: [PATCH 07/12] Simplify code --- docs/manual/inference.tex | 1 - .../WholeProgramInferenceImplementation.java | 12 +----------- 2 files changed, 1 insertion(+), 12 deletions(-) diff --git a/docs/manual/inference.tex b/docs/manual/inference.tex index 114becbe1ecb..67a9c77e23ce 100644 --- a/docs/manual/inference.tex +++ b/docs/manual/inference.tex @@ -444,7 +444,6 @@ incorrect results. In this case, write type annotations on the formal parameters of one of the routines. - Whole-program inference is a ``forward analysis''. % This might change in the future. It determines a method parameter's type diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java index db66ac0c70f7..5dabdbca5d15 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java @@ -17,14 +17,12 @@ import javax.lang.model.util.ElementFilter; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.dataflow.analysis.Analysis; -import org.checkerframework.dataflow.cfg.node.ClassNameNode; import org.checkerframework.dataflow.cfg.node.FieldAccessNode; import org.checkerframework.dataflow.cfg.node.LocalVariableNode; import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; import org.checkerframework.dataflow.cfg.node.Node; import org.checkerframework.dataflow.cfg.node.ObjectCreationNode; import org.checkerframework.dataflow.cfg.node.ReturnNode; -import org.checkerframework.dataflow.cfg.node.ThisNode; import org.checkerframework.dataflow.expression.ClassName; import org.checkerframework.dataflow.expression.FieldAccess; import org.checkerframework.dataflow.expression.ThisReference; @@ -189,15 +187,7 @@ private boolean isRecursiveCall(MethodInvocationNode methodInvNode) { } ExecutableElement methodInvocEle = TreeUtils.elementFromUse(methodInvNode.getTree()); ExecutableElement methodDeclEle = TreeUtils.elementFromDeclaration(enclosingMethod); - if (!methodDeclEle.equals(methodInvocEle)) { - return false; - } - - if (ElementUtils.isStatic(methodDeclEle)) { - return methodInvNode.getTarget().getReceiver() instanceof ClassNameNode; - } else { - return methodInvNode.getTarget().getMethod() instanceof ThisNode; - } + return methodDeclEle.equals(methodInvocEle); } /** From eb75223216b00d3a9ef9a0faee3b62825b503be1 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Wed, 18 Jan 2023 16:25:44 -0800 Subject: [PATCH 08/12] Permit more time for inference jobs --- azure-pipelines.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index b8d64f8c1055..c76256ee1483 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -124,6 +124,7 @@ jobs: pool: vmImage: 'ubuntu-latest' container: mdernst/cf-ubuntu-jdk8:latest + timeoutInMinutes: 70 steps: - checkout: self fetchDepth: 25 @@ -136,6 +137,7 @@ jobs: pool: vmImage: 'ubuntu-latest' container: mdernst/cf-ubuntu-jdk11:latest + timeoutInMinutes: 70 steps: - checkout: self fetchDepth: 25 @@ -149,6 +151,7 @@ jobs: pool: vmImage: 'ubuntu-latest' container: mdernst/cf-ubuntu-jdk17:latest + timeoutInMinutes: 70 steps: - checkout: self fetchDepth: 25 @@ -161,6 +164,7 @@ jobs: pool: vmImage: 'ubuntu-latest' container: mdernst/cf-ubuntu-jdk19:latest + timeoutInMinutes: 70 steps: - checkout: self fetchDepth: 25 From de71b4bccf8f3919c7e5898eca44fec36490c188 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Thu, 19 Jan 2023 07:37:01 -0800 Subject: [PATCH 09/12] Give inference job more time --- azure-pipelines.yml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index c76256ee1483..f5d2804353c1 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -124,7 +124,7 @@ jobs: pool: vmImage: 'ubuntu-latest' container: mdernst/cf-ubuntu-jdk8:latest - timeoutInMinutes: 70 + timeoutInMinutes: 80 steps: - checkout: self fetchDepth: 25 @@ -137,7 +137,7 @@ jobs: pool: vmImage: 'ubuntu-latest' container: mdernst/cf-ubuntu-jdk11:latest - timeoutInMinutes: 70 + timeoutInMinutes: 80 steps: - checkout: self fetchDepth: 25 @@ -151,7 +151,7 @@ jobs: pool: vmImage: 'ubuntu-latest' container: mdernst/cf-ubuntu-jdk17:latest - timeoutInMinutes: 70 + timeoutInMinutes: 80 steps: - checkout: self fetchDepth: 25 @@ -164,7 +164,7 @@ jobs: pool: vmImage: 'ubuntu-latest' container: mdernst/cf-ubuntu-jdk19:latest - timeoutInMinutes: 70 + timeoutInMinutes: 80 steps: - checkout: self fetchDepth: 25 From 3e5415ee322b6573d27a72757d29f6b00c50c990 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Thu, 19 Jan 2023 13:45:01 -0800 Subject: [PATCH 10/12] Permit more time in CI --- azure-pipelines.yml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/azure-pipelines.yml b/azure-pipelines.yml index f5d2804353c1..863a32bd4325 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -124,7 +124,7 @@ jobs: pool: vmImage: 'ubuntu-latest' container: mdernst/cf-ubuntu-jdk8:latest - timeoutInMinutes: 80 + timeoutInMinutes: 90 steps: - checkout: self fetchDepth: 25 @@ -137,7 +137,7 @@ jobs: pool: vmImage: 'ubuntu-latest' container: mdernst/cf-ubuntu-jdk11:latest - timeoutInMinutes: 80 + timeoutInMinutes: 90 steps: - checkout: self fetchDepth: 25 @@ -151,7 +151,7 @@ jobs: pool: vmImage: 'ubuntu-latest' container: mdernst/cf-ubuntu-jdk17:latest - timeoutInMinutes: 80 + timeoutInMinutes: 90 steps: - checkout: self fetchDepth: 25 @@ -164,7 +164,7 @@ jobs: pool: vmImage: 'ubuntu-latest' container: mdernst/cf-ubuntu-jdk19:latest - timeoutInMinutes: 80 + timeoutInMinutes: 90 steps: - checkout: self fetchDepth: 25 From 175be2bfb1b600462a5836cc1b70d3f9bb35961c Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Thu, 19 Jan 2023 15:04:03 -0800 Subject: [PATCH 11/12] Try twice in case of network lossage --- checker/bin-devel/test-plume-lib.sh | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/checker/bin-devel/test-plume-lib.sh b/checker/bin-devel/test-plume-lib.sh index b33ee4d60e69..7dbaebca95e7 100755 --- a/checker/bin-devel/test-plume-lib.sh +++ b/checker/bin-devel/test-plume-lib.sh @@ -50,5 +50,6 @@ for PACKAGE in "${PACKAGES[@]}"; do # Uses "compileJava" target instead of "assemble" to avoid the javadoc error "Error fetching URL: # https://docs.oracle.com/en/java/javase/17/docs/api/" due to network problems. echo "About to call ./gradlew --console=plain -PcfLocal compileJava" - (cd "${PACKAGEDIR}" && ./gradlew --console=plain -PcfLocal compileJava) + # Try twice in case of network lossage. + (cd "${PACKAGEDIR}" && (./gradlew --console=plain -PcfLocal compileJava || (sleep 60 && ./gradlew --console=plain -PcfLocal compileJava))) done From 0f74febb678ebb978dee10e5dfabd07d9de1cbeb Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Thu, 19 Jan 2023 19:02:41 -0800 Subject: [PATCH 12/12] Add goal file, add diagnostics --- checker/bin-devel/wpi-plumelib/plume-util.expected | 0 checker/bin-devel/wpi-plumelib/test-wpi-plumelib.sh | 2 ++ 2 files changed, 2 insertions(+) create mode 100644 checker/bin-devel/wpi-plumelib/plume-util.expected diff --git a/checker/bin-devel/wpi-plumelib/plume-util.expected b/checker/bin-devel/wpi-plumelib/plume-util.expected new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/checker/bin-devel/wpi-plumelib/test-wpi-plumelib.sh b/checker/bin-devel/wpi-plumelib/test-wpi-plumelib.sh index 5e3a28f673ea..5425c8a3ab73 100755 --- a/checker/bin-devel/wpi-plumelib/test-wpi-plumelib.sh +++ b/checker/bin-devel/wpi-plumelib/test-wpi-plumelib.sh @@ -72,7 +72,9 @@ test_wpi_plume_lib() { # may become redundant and javac -Xlint:all yields "warning: [cast] redundant cast to ...". "$CHECKERFRAMEWORK"/checker/bin-devel/.plume-scripts/preplace -- "-Xlint:" "-Xlint:-cast," build.gradle + echo "wpi-many.sh about to call wpi.sh at $(date)" "$CHECKERFRAMEWORK/checker/bin/wpi.sh" -b "-PskipCheckerFramework" -- --checker "$checkers" --extraJavacArgs='-AsuppressWarnings=type.checking.not.run' + echo "wpi-many.sh returned from wpi.sh at $(date)" EXPECTED_FILE="$SCRIPTDIR/$project.expected" DLJC_OUT_DIR="$TESTDIR/$project/dljc-out"