From 79f6aeed83d9075a6d0723f0e57efa110d8fc267 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Mon, 26 Sep 2022 12:09:29 -0700 Subject: [PATCH 01/29] Infer purity when using the Lock Checker --- .../org/checkerframework/checker/lock/LockVisitor.java | 3 --- .../common/basetype/BaseTypeVisitor.java | 9 ++++++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java b/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java index 32f19b37aa8..0bf15193f7b 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java @@ -90,9 +90,6 @@ public LockVisitor(BaseTypeChecker checker) { if (!(checkerName.equals("lock") || checkerName.equals("LockChecker") || checkerName.equals("org.checkerframework.checker.lock.LockChecker"))) { - // The Lock Checker redefines CFAbstractStore#isSideEffectFree in a way that is incompatible - // with (semantically different than) other checkers. - inferPurity = false; break; } } diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index fb71ff703fd..1488fce1b69 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -231,9 +231,12 @@ public class BaseTypeVisitorSetting to false will break whole-program inference (WPI), because the checker may read + * {@code .ajava} files generated by itself for some classes and {@code .ajava} files generated by + * a different checker for other classes. The failure is nondeterministic: it doesn't always + * occur. */ protected boolean inferPurity = true; From c81cd8a40f4a6ffd964d7cb434a34d17cff807eb Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 07:43:00 -0700 Subject: [PATCH 02/29] Reorder method --- .../lock/LockAnnotatedTypeFactory.java | 56 +++++++++---------- 1 file changed, 28 insertions(+), 28 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java index dcc8166a08e..0ed3425431e 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java @@ -507,41 +507,41 @@ public static SideEffectAnnotation weakest() { // package-private SideEffectAnnotation methodSideEffectAnnotation( Element element, boolean issueErrorIfMoreThanOnePresent) { - if (element != null) { - Set sideEffectAnnotationPresent = - EnumSet.noneOf(SideEffectAnnotation.class); - for (SideEffectAnnotation sea : SideEffectAnnotation.values()) { - if (getDeclAnnotationNoAliases(element, sea.getAnnotationClass()) != null) { - sideEffectAnnotationPresent.add(sea); - } + if (element == null) { + // When there is not enough information to determine the correct side effect annotation, + // return the weakest one. + return SideEffectAnnotation.weakest(); + } + + Set sideEffectAnnotationPresent = + EnumSet.noneOf(SideEffectAnnotation.class); + for (SideEffectAnnotation sea : SideEffectAnnotation.values()) { + if (getDeclAnnotationNoAliases(element, sea.getAnnotationClass()) != null) { + sideEffectAnnotationPresent.add(sea); } + } - int count = sideEffectAnnotationPresent.size(); + int count = sideEffectAnnotationPresent.size(); - if (count == 0) { - return defaults.applyConservativeDefaults(element) - ? SideEffectAnnotation.MAYRELEASELOCKS - : SideEffectAnnotation.RELEASESNOLOCKS; - } + if (count == 0) { + return defaults.applyConservativeDefaults(element) + ? SideEffectAnnotation.MAYRELEASELOCKS + : SideEffectAnnotation.RELEASESNOLOCKS; + } - if (count > 1 && issueErrorIfMoreThanOnePresent) { - // TODO: Turn on after figuring out how this interacts with inherited annotations. - // checker.reportError(element, "multiple.sideeffect.annotations"); - } + if (count > 1 && issueErrorIfMoreThanOnePresent) { + // TODO: Turn on after figuring out how this interacts with inherited annotations. + // checker.reportError(element, "multiple.sideeffect.annotations"); + } - SideEffectAnnotation weakest = null; - // At least one side effect annotation was found. Return the weakest. - for (SideEffectAnnotation sea : sideEffectAnnotationPresent) { - if (weakest == null || sea.isWeakerThan(weakest)) { - weakest = sea; - } + SideEffectAnnotation weakest = null; + // At least one side effect annotation was found. Return the weakest. + for (SideEffectAnnotation sea : sideEffectAnnotationPresent) { + if (weakest == null || sea.isWeakerThan(weakest)) { + weakest = sea; } - return weakest; } - - // When there is not enough information to determine the correct side effect annotation, - // return the weakest one. - return SideEffectAnnotation.weakest(); + return weakest; } /** From 0205a576dfcb4d63f5f4401c007101eec2b26af6 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 07:43:18 -0700 Subject: [PATCH 03/29] Cleanup "infer purity" commit --- .../org/checkerframework/checker/lock/LockVisitor.java | 7 ------- 1 file changed, 7 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java b/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java index 0bf15193f7b..4974452bb3a 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java @@ -86,13 +86,6 @@ public class LockVisitor extends BaseTypeVisitor { */ public LockVisitor(BaseTypeChecker checker) { super(checker); - for (String checkerName : atypeFactory.getCheckerNames()) { - if (!(checkerName.equals("lock") - || checkerName.equals("LockChecker") - || checkerName.equals("org.checkerframework.checker.lock.LockChecker"))) { - break; - } - } } @Override From 82ad20dd123db57034ddf9197aeb2284fcd8df93 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 08:12:20 -0700 Subject: [PATCH 04/29] Reorder method (simplify flow, reduce indentation) --- .../lock/LockAnnotatedTypeFactory.java | 56 +++++++++---------- 1 file changed, 28 insertions(+), 28 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java index dcc8166a08e..0ed3425431e 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java @@ -507,41 +507,41 @@ public static SideEffectAnnotation weakest() { // package-private SideEffectAnnotation methodSideEffectAnnotation( Element element, boolean issueErrorIfMoreThanOnePresent) { - if (element != null) { - Set sideEffectAnnotationPresent = - EnumSet.noneOf(SideEffectAnnotation.class); - for (SideEffectAnnotation sea : SideEffectAnnotation.values()) { - if (getDeclAnnotationNoAliases(element, sea.getAnnotationClass()) != null) { - sideEffectAnnotationPresent.add(sea); - } + if (element == null) { + // When there is not enough information to determine the correct side effect annotation, + // return the weakest one. + return SideEffectAnnotation.weakest(); + } + + Set sideEffectAnnotationPresent = + EnumSet.noneOf(SideEffectAnnotation.class); + for (SideEffectAnnotation sea : SideEffectAnnotation.values()) { + if (getDeclAnnotationNoAliases(element, sea.getAnnotationClass()) != null) { + sideEffectAnnotationPresent.add(sea); } + } - int count = sideEffectAnnotationPresent.size(); + int count = sideEffectAnnotationPresent.size(); - if (count == 0) { - return defaults.applyConservativeDefaults(element) - ? SideEffectAnnotation.MAYRELEASELOCKS - : SideEffectAnnotation.RELEASESNOLOCKS; - } + if (count == 0) { + return defaults.applyConservativeDefaults(element) + ? SideEffectAnnotation.MAYRELEASELOCKS + : SideEffectAnnotation.RELEASESNOLOCKS; + } - if (count > 1 && issueErrorIfMoreThanOnePresent) { - // TODO: Turn on after figuring out how this interacts with inherited annotations. - // checker.reportError(element, "multiple.sideeffect.annotations"); - } + if (count > 1 && issueErrorIfMoreThanOnePresent) { + // TODO: Turn on after figuring out how this interacts with inherited annotations. + // checker.reportError(element, "multiple.sideeffect.annotations"); + } - SideEffectAnnotation weakest = null; - // At least one side effect annotation was found. Return the weakest. - for (SideEffectAnnotation sea : sideEffectAnnotationPresent) { - if (weakest == null || sea.isWeakerThan(weakest)) { - weakest = sea; - } + SideEffectAnnotation weakest = null; + // At least one side effect annotation was found. Return the weakest. + for (SideEffectAnnotation sea : sideEffectAnnotationPresent) { + if (weakest == null || sea.isWeakerThan(weakest)) { + weakest = sea; } - return weakest; } - - // When there is not enough information to determine the correct side effect annotation, - // return the weakest one. - return SideEffectAnnotation.weakest(); + return weakest; } /** From 61f8428c2f028ba550158cde5909e81b432f92dc Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 10:33:03 -0700 Subject: [PATCH 05/29] Checkpoint; parts must be undone --- checker/bin/wpi-many.sh | 11 ++-- .../lock/LockAnnotatedTypeFactory.java | 37 ++++++++++++ checker/tests/wpi-many/testin.txt | 12 ++-- .../dataflow/util/PurityChecker.java | 8 ++- .../dataflow/util/PurityUtils.java | 45 +++++++++++--- docs/CHANGELOG.md | 4 +- .../common/basetype/BaseTypeVisitor.java | 6 +- .../checkerframework/javacutil/FileUtils.java | 59 +++++++++++++++++++ 8 files changed, 158 insertions(+), 24 deletions(-) create mode 100644 javacutil/src/main/java/org/checkerframework/javacutil/FileUtils.java diff --git a/checker/bin/wpi-many.sh b/checker/bin/wpi-many.sh index 1e4ad01e3b7..91ca3889861 100755 --- a/checker/bin/wpi-many.sh +++ b/checker/bin/wpi-many.sh @@ -303,7 +303,7 @@ else # Don't match arguments like "-J--add-opens=jdk.compiler/com.sun.tools.java" # or "--add-opens=jdk.compiler/com.sun.tools.java". # shellcheck disable=SC2046 - grep -oh "\S*\.java" $(cat "${OUTDIR}-results/results_available.txt") | sed "s/'//g" | grep -v '^\-J' | grep -v '^\-\-add\-opens' | sort | uniq > "${listpath}" + grep -oh "^\S*\.java" $(cat "${OUTDIR}-results/results_available.txt") | sed "s/'//g" | grep -v '^\-J' | grep -v '^\-\-add\-opens' | sort | uniq > "${listpath}" if [ ! -s "${listpath}" ] ; then echo "${listpath} has size zero" @@ -321,9 +321,12 @@ else unzip -o "scc-2.13.0-i386-unknown-linux.zip" # shellcheck disable=SC2046 - "${SCRIPTDIR}/.scc/scc" --output "${OUTDIR}-results/loc.txt" \ - $(< "${listpath}") - + if ! "${SCRIPTDIR}/.scc/scc" --output "${OUTDIR}-results/loc.txt" $(< "${listpath}") ; then + echo "Problem in wpi-many.sh while running scc." + echo " listpath = ${listpath}" + echo " generated from ${OUTDIR}-results/results_available.txt" + exit 1 + fi rm -f "${listpath}" else echo "skipping computation of lines of code because the operating system is not linux: ${OSTYPE}}" diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java index 0ed3425431e..45ca1b31f18 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java @@ -4,6 +4,9 @@ import com.sun.source.tree.MethodInvocationTree; import com.sun.source.tree.Tree; import com.sun.source.tree.VariableTree; +import java.io.File; +import java.io.IOException; +import java.io.PrintStream; import java.lang.annotation.Annotation; import java.util.ArrayList; import java.util.Arrays; @@ -61,6 +64,7 @@ import org.checkerframework.javacutil.AnnotationBuilder; import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.ElementUtils; +import org.checkerframework.javacutil.FileUtils; import org.checkerframework.javacutil.TreeUtils; import org.checkerframework.javacutil.TypeSystemError; import org.plumelib.util.CollectionsPlume; @@ -80,6 +84,18 @@ public class LockAnnotatedTypeFactory extends GenericAnnotatedTypeFactory { + static final PrintStream log; + + static { + try { + log = + new PrintStream( + FileUtils.createTempFile(new File(".").toPath(), "latf", ".log").toFile()); + } catch (IOException e) { + throw new Error(e); + } + } + /** dependent type annotation error message for when the expression is not effectively final. */ public static final String NOT_EFFECTIVELY_FINAL = "lock expression is not effectively final"; @@ -513,6 +529,17 @@ SideEffectAnnotation methodSideEffectAnnotation( return SideEffectAnnotation.weakest(); } + boolean doLog = + element.getEnclosingElement().toString().endsWith("InstructionContextQueue") + && element.toString().startsWith("add("); + + if (doLog) { + log.printf( + "methodSideEffectAnnotation(%s . %s, %s)%n", + element.getEnclosingElement(), element, issueErrorIfMoreThanOnePresent); + log.printf(" decl annotations = %s%n", getDeclAnnotations(element)); + } + Set sideEffectAnnotationPresent = EnumSet.noneOf(SideEffectAnnotation.class); for (SideEffectAnnotation sea : SideEffectAnnotation.values()) { @@ -522,6 +549,11 @@ SideEffectAnnotation methodSideEffectAnnotation( } int count = sideEffectAnnotationPresent.size(); + if (doLog) { + log.printf( + " methodSideEffectAnnotation(): present (size %d) = %s%n", + count, sideEffectAnnotationPresent); + } if (count == 0) { return defaults.applyConservativeDefaults(element) @@ -541,6 +573,11 @@ SideEffectAnnotation methodSideEffectAnnotation( weakest = sea; } } + if (doLog) { + log.printf( + " methodSideEffectAnnotation(%s . %s, %s) => %s%n", + element.getEnclosingElement(), element, issueErrorIfMoreThanOnePresent, weakest); + } return weakest; } diff --git a/checker/tests/wpi-many/testin.txt b/checker/tests/wpi-many/testin.txt index 69d5014a200..f9ce34aa437 100644 --- a/checker/tests/wpi-many/testin.txt +++ b/checker/tests/wpi-many/testin.txt @@ -1,7 +1,7 @@ https://github.com/kelloggm/wpi-many-tests-bcel-util 74be0b18f893077223850d5ffb117e496c4b833a -https://github.com/kelloggm/wpi-many-tests-bibtex-clean b7ac872c9323a0944015cd79014e45fb7a5d1c93 -https://github.com/kelloggm/wpi-many-tests-ensures-called-methods db816432c95a3d047a1e3f7966fefb1515cba7c9 -https://github.com/kelloggm/wpi-many-tests-html-pretty-print 1c4f2da82407e21eb89a9196f06d613a64af211a -https://github.com/kelloggm/-wpi-many-tests-bibtex-clean 7a70d58b9fdaedd71c4af4a9dfca7d5fda9268dc -# This comment line tests that the commenting feature works (if it doesn't then, this line will be read and fail, as it's not a URL). -https://github.com/Nargeshdb/wpi-many-tests-owning-field 6accab941bdae0274862ab414d729851851670ea +# https://github.com/kelloggm/wpi-many-tests-bibtex-clean b7ac872c9323a0944015cd79014e45fb7a5d1c93 +# https://github.com/kelloggm/wpi-many-tests-ensures-called-methods db816432c95a3d047a1e3f7966fefb1515cba7c9 +# https://github.com/kelloggm/wpi-many-tests-html-pretty-print 1c4f2da82407e21eb89a9196f06d613a64af211a +# https://github.com/kelloggm/-wpi-many-tests-bibtex-clean 7a70d58b9fdaedd71c4af4a9dfca7d5fda9268dc +# # This comment line tests that the commenting feature works (if it doesn't, then this line will be read and fail, as it's not a URL). +# https://github.com/Nargeshdb/wpi-many-tests-owning-field 6accab941bdae0274862ab414d729851851670ea diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java index ed20a8bb891..aa9fbdd28de 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java @@ -218,6 +218,10 @@ public Void visitCatch(CatchTree node, Void ignore) { return super.visitCatch(node, ignore); } + /** Represents a method that is both deterministic and side-effect free. */ + private static final EnumSet detAndSeFree = + EnumSet.of(Kind.DETERMINISTIC, Kind.SIDE_EFFECT_FREE); + @Override public Void visitMethodInvocation(MethodInvocationTree node, Void ignore) { ExecutableElement elt = TreeUtils.elementFromUse(node); @@ -227,8 +231,8 @@ public Void visitMethodInvocation(MethodInvocationTree node, Void ignore) { EnumSet purityKinds = (assumeDeterministic && assumeSideEffectFree) // Avoid computation if not necessary - ? EnumSet.of(Kind.DETERMINISTIC, Kind.SIDE_EFFECT_FREE) - : PurityUtils.getPurityKinds(annoProvider, elt); + ? detAndSeFree + : PurityUtils.getPurityAnnotations(annoProvider, elt); boolean det = assumeDeterministic || purityKinds.contains(Kind.DETERMINISTIC); boolean seFree = assumeSideEffectFree || purityKinds.contains(Kind.SIDE_EFFECT_FREE); if (!det && !seFree) { diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java index 01b689d2b85..a7ff50d2913 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java @@ -31,7 +31,7 @@ public class PurityUtils { * @return whether the method has any purity annotations */ public static boolean hasPurityAnnotation(AnnotationProvider provider, MethodTree methodTree) { - return !getPurityKinds(provider, methodTree).isEmpty(); + return !getPurityAnnotations(provider, methodTree).isEmpty(); } /** @@ -43,7 +43,7 @@ public static boolean hasPurityAnnotation(AnnotationProvider provider, MethodTre */ public static boolean hasPurityAnnotation( AnnotationProvider provider, ExecutableElement methodElement) { - return !getPurityKinds(provider, methodElement).isEmpty(); + return !getPurityAnnotations(provider, methodElement).isEmpty(); } /** @@ -70,7 +70,7 @@ public static boolean isDeterministic(AnnotationProvider provider, MethodTree me */ public static boolean isDeterministic( AnnotationProvider provider, ExecutableElement methodElement) { - EnumSet kinds = getPurityKinds(provider, methodElement); + EnumSet kinds = getPurityAnnotations(provider, methodElement); return kinds.contains(Kind.DETERMINISTIC); } @@ -98,39 +98,68 @@ public static boolean isSideEffectFree(AnnotationProvider provider, MethodTree m */ public static boolean isSideEffectFree( AnnotationProvider provider, ExecutableElement methodElement) { - EnumSet kinds = getPurityKinds(provider, methodElement); + EnumSet kinds = getPurityAnnotations(provider, methodElement); return kinds.contains(Kind.SIDE_EFFECT_FREE); } /** - * Returns the types of purity of the method {@code methodTree}. + * Returns the purity annotations of the method {@code methodTree}. * * @param provider how to get annotations * @param methodTree a method to test * @return the types of purity of the method {@code methodTree} + * @deprecated use {@code getPurityAnnotations} */ + @Deprecated // 2022-09-27 public static EnumSet getPurityKinds( AnnotationProvider provider, MethodTree methodTree) { + return getPurityAnnotations(provider, methodTree); + } + + /** + * Returns the purity annotations on the method {@code methodTree}. + * + * @param provider how to get annotations + * @param methodTree a method to test + * @return the types of purity of the method {@code methodTree} + */ + public static EnumSet getPurityAnnotations( + AnnotationProvider provider, MethodTree methodTree) { ExecutableElement methodElement = TreeUtils.elementFromDeclaration(methodTree); if (methodElement == null) { throw new BugInCF("Could not find element for tree: " + methodTree); } - return getPurityKinds(provider, methodElement); + return getPurityAnnotations(provider, methodElement); } /** - * Returns the types of purity of the method {@code methodElement}. + * Returns the purity annotations on the method {@code methodElement}. * * @param provider how to get annotations * @param methodElement a method to test * @return the types of purity of the method {@code methodElement} + * @deprecated use {@code getPurityAnnotations} */ - // TODO: should the return type be an EnumSet? + @Deprecated // 2022-09-27 public static EnumSet getPurityKinds( AnnotationProvider provider, ExecutableElement methodElement) { + return getPurityAnnotations(provider, methodElement); + } + + /** + * Returns the types of purity of the method {@code methodElement}. + * + * @param provider how to get annotations + * @param methodElement a method to test + * @return the types of purity of the method {@code methodElement} + */ + public static EnumSet getPurityAnnotations( + AnnotationProvider provider, ExecutableElement methodElement) { + // Special case for record accessors if (ElementUtils.isRecordAccessor(methodElement)) { return EnumSet.of(Kind.DETERMINISTIC, Kind.SIDE_EFFECT_FREE); } + AnnotationMirror pureAnnotation = provider.getDeclAnnotation(methodElement, Pure.class); AnnotationMirror sefAnnotation = provider.getDeclAnnotation(methodElement, SideEffectFree.class); diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 2fc4eb59a78..fbf18c3280b 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -13,7 +13,9 @@ introduced since JDK 11). **Implementation details:** -Deprecated `TreeUtils.constructor()` in favor of `TreeUtils.elementFromUse()`. +Deprecated methods: + * `TreeUtils.constructor()` => `TreeUtils.elementFromUse()` + * `PurityUtils.getPurityKinds()` => `PurityUtils.getPurityAnnotations()` Use `TreeUtils.elementFromDeclaration` and `TreeUtils.elementFromUse` in preference to `TreeUtils.elementFromTree`, when possible. diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 1488fce1b69..9d9e1b16b39 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -980,7 +980,7 @@ protected void checkPurity(MethodTree node) { } // check "no" purity - EnumSet kinds = PurityUtils.getPurityKinds(atypeFactory, node); + EnumSet kinds = PurityUtils.getPurityAnnotations(atypeFactory, node); // @Deterministic makes no sense for a void method or constructor boolean isDeterministic = kinds.contains(Pure.Kind.DETERMINISTIC); if (isDeterministic) { @@ -3710,9 +3710,9 @@ private void checkPurity() { // check purity annotations EnumSet superPurity = - PurityUtils.getPurityKinds(atypeFactory, overridden.getElement()); + PurityUtils.getPurityAnnotations(atypeFactory, overridden.getElement()); EnumSet subPurity = - PurityUtils.getPurityKinds(atypeFactory, overrider.getElement()); + PurityUtils.getPurityAnnotations(atypeFactory, overrider.getElement()); if (!subPurity.containsAll(superPurity)) { checker.reportError( overriderTree, diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/FileUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/FileUtils.java new file mode 100644 index 00000000000..690130c308f --- /dev/null +++ b/javacutil/src/main/java/org/checkerframework/javacutil/FileUtils.java @@ -0,0 +1,59 @@ +// TODO: Move into plume-util, and then delete this class.import +package org.checkerframework.javacutil; + +import java.io.File; +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.attribute.FileAttribute; + +/** File utilities. To be moved into plume-util. */ +public class FileUtils { + + /** Do not instantiate. */ + private FileUtils() { + throw new Error("do not instantiate"); + } + + /** + * Creates a new empty file in the default temporary-file directory, using the given prefix and + * suffix strings to generate its name. This is like {@link File#createTempFile}, but uses + * sequential file names. + * + * @param prefix the prefix string to be used in generating the file's name; may be null + * @param suffix the suffix string to be used in generating the file's name; may be null, in which + * case ".tmp" is used + * @param attrs an optional list of file attributes to set atomically when creating the file + * @return the path to the newly created file that did not exist before this method was invoked + * @throws IllegalArgumentException if there is trouble creating the file + */ + public static Path createTempFile(String prefix, String suffix, FileAttribute... attrs) + throws IOException { + return createTempFile(Path.of(System.getProperty("java.io.tmpdir")), prefix, suffix, attrs); + } + + /** + * Creates a new empty file in the specified directory, using the given prefix and suffix strings + * to generate its name. This is like {@link File#createTempFile}, but uses sequential file names. + * + * @param dir the path to directory in which to create the file + * @param prefix the prefix string to be used in generating the file's name; may be null + * @param suffix the suffix string to be used in generating the file's name; may be null, in which + * case ".tmp" is used + * @param attrs an optional list of file attributes to set atomically when creating the file + * @return the path to the newly created file that did not exist before this method was invoked + * @throws IllegalArgumentException if there is trouble creating the file + */ + public static Path createTempFile( + Path dir, String prefix, String suffix, FileAttribute... attrs) throws IOException { + Path createdDir = Files.createDirectories(dir, attrs); + for (int i = 1; i < Integer.MAX_VALUE; i++) { + File candidate = new File(createdDir.toFile(), prefix + i + suffix); + if (!candidate.exists()) { + System.out.println("Created " + candidate); + return candidate.toPath(); + } + } + throw new Error("every file exists"); + } +} From 5d0009f58324029d637606ef6ad4bd526eaed0e3 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 10:57:32 -0700 Subject: [PATCH 06/29] Tweaks to log file creation --- .../checker/lock/LockAnnotatedTypeFactory.java | 4 +++- .../main/java/org/checkerframework/javacutil/FileUtils.java | 3 ++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java index 45ca1b31f18..c222ffa632e 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java @@ -90,7 +90,9 @@ public class LockAnnotatedTypeFactory try { log = new PrintStream( - FileUtils.createTempFile(new File(".").toPath(), "latf", ".log").toFile()); + FileUtils.createTempFile( + new File(System.getProperty("user.dir")).toPath(), "latf", ".log") + .toFile()); } catch (IOException e) { throw new Error(e); } diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/FileUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/FileUtils.java index 690130c308f..4e648e66161 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/FileUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/FileUtils.java @@ -1,4 +1,5 @@ -// TODO: Move into plume-util, and then delete this class.import +// TODO: When plume-util 1.6.0 is released, deprecate createTempFile in favor of +// FilesPlume.createTempFile(). package org.checkerframework.javacutil; import java.io.File; From 485ea823c6e80a7335eddad6039a25dfb62e8ce2 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 12:34:27 -0700 Subject: [PATCH 07/29] Check purity annotations --- .../org/checkerframework/framework/test/junit/FlowTest.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/framework/src/test/java/org/checkerframework/framework/test/junit/FlowTest.java b/framework/src/test/java/org/checkerframework/framework/test/junit/FlowTest.java index a8235c6b0a2..c88ca95acc6 100644 --- a/framework/src/test/java/org/checkerframework/framework/test/junit/FlowTest.java +++ b/framework/src/test/java/org/checkerframework/framework/test/junit/FlowTest.java @@ -13,7 +13,7 @@ public class FlowTest extends CheckerFrameworkPerDirectoryTest { * @param testFiles the files containing test code, which will be type-checked */ public FlowTest(List testFiles) { - super(testFiles, FlowTestChecker.class, "flow", "-Anomsgtext"); + super(testFiles, FlowTestChecker.class, "flow", "-Anomsgtext", "-AcheckPurityAnnotations"); } @Parameters From 64a52053fb8bfe4caa77ae7725cf365d207ec12c Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 12:37:27 -0700 Subject: [PATCH 08/29] Combine `flow/` and `flow2/` test directories --- framework/tests/{flow2 => flow}/AnnotationAliasing.java | 0 framework/tests/{flow2 => flow}/ArrayFlow.java | 0 framework/tests/{flow2 => flow}/Basic2.java | 0 framework/tests/{flow2 => flow}/ContractsOverriding.java | 0 .../tests/{flow2 => flow}/ContractsOverridingSubtyping.java | 0 framework/tests/{flow2 => flow}/CustomContractWithArgs.java | 0 framework/tests/{flow2 => flow}/Equal.java | 0 framework/tests/{flow2 => flow}/FieldShadowing.java | 0 framework/tests/{flow2 => flow}/Issue4449.java | 0 framework/tests/{flow2 => flow}/Issue951.java | 0 framework/tests/{flow2 => flow}/MetaPostcondition.java | 0 framework/tests/{flow2 => flow}/MetaPrecondition.java | 0 framework/tests/{flow2 => flow}/MethodCallFlowExpr.java | 0 framework/tests/{flow2 => flow}/Monotonic.java | 0 framework/tests/{flow2 => flow}/NonMethodCode.java | 0 framework/tests/{flow2 => flow}/ParamFlowExpr.java | 0 framework/tests/{flow2 => flow}/Postcondition.java | 0 framework/tests/{flow2 => flow}/Precondition.java | 0 framework/tests/{flow2 => flow}/Purity.java | 0 framework/tests/{flow2 => flow}/StorePure.java | 0 framework/tests/{flow2 => flow}/Termination.java | 0 .../tests/{flow2 => flow}/flowexpression-scope/Class1.java | 0 .../tests/{flow2 => flow}/flowexpression-scope/Class2.java | 0 .../tests/{flow2 => flow}/flowexpression-scope/Issue862.java | 0 framework/tests/flow2/README | 5 ----- 25 files changed, 5 deletions(-) rename framework/tests/{flow2 => flow}/AnnotationAliasing.java (100%) rename framework/tests/{flow2 => flow}/ArrayFlow.java (100%) rename framework/tests/{flow2 => flow}/Basic2.java (100%) rename framework/tests/{flow2 => flow}/ContractsOverriding.java (100%) rename framework/tests/{flow2 => flow}/ContractsOverridingSubtyping.java (100%) rename framework/tests/{flow2 => flow}/CustomContractWithArgs.java (100%) rename framework/tests/{flow2 => flow}/Equal.java (100%) rename framework/tests/{flow2 => flow}/FieldShadowing.java (100%) rename framework/tests/{flow2 => flow}/Issue4449.java (100%) rename framework/tests/{flow2 => flow}/Issue951.java (100%) rename framework/tests/{flow2 => flow}/MetaPostcondition.java (100%) rename framework/tests/{flow2 => flow}/MetaPrecondition.java (100%) rename framework/tests/{flow2 => flow}/MethodCallFlowExpr.java (100%) rename framework/tests/{flow2 => flow}/Monotonic.java (100%) rename framework/tests/{flow2 => flow}/NonMethodCode.java (100%) rename framework/tests/{flow2 => flow}/ParamFlowExpr.java (100%) rename framework/tests/{flow2 => flow}/Postcondition.java (100%) rename framework/tests/{flow2 => flow}/Precondition.java (100%) rename framework/tests/{flow2 => flow}/Purity.java (100%) rename framework/tests/{flow2 => flow}/StorePure.java (100%) rename framework/tests/{flow2 => flow}/Termination.java (100%) rename framework/tests/{flow2 => flow}/flowexpression-scope/Class1.java (100%) rename framework/tests/{flow2 => flow}/flowexpression-scope/Class2.java (100%) rename framework/tests/{flow2 => flow}/flowexpression-scope/Issue862.java (100%) delete mode 100644 framework/tests/flow2/README diff --git a/framework/tests/flow2/AnnotationAliasing.java b/framework/tests/flow/AnnotationAliasing.java similarity index 100% rename from framework/tests/flow2/AnnotationAliasing.java rename to framework/tests/flow/AnnotationAliasing.java diff --git a/framework/tests/flow2/ArrayFlow.java b/framework/tests/flow/ArrayFlow.java similarity index 100% rename from framework/tests/flow2/ArrayFlow.java rename to framework/tests/flow/ArrayFlow.java diff --git a/framework/tests/flow2/Basic2.java b/framework/tests/flow/Basic2.java similarity index 100% rename from framework/tests/flow2/Basic2.java rename to framework/tests/flow/Basic2.java diff --git a/framework/tests/flow2/ContractsOverriding.java b/framework/tests/flow/ContractsOverriding.java similarity index 100% rename from framework/tests/flow2/ContractsOverriding.java rename to framework/tests/flow/ContractsOverriding.java diff --git a/framework/tests/flow2/ContractsOverridingSubtyping.java b/framework/tests/flow/ContractsOverridingSubtyping.java similarity index 100% rename from framework/tests/flow2/ContractsOverridingSubtyping.java rename to framework/tests/flow/ContractsOverridingSubtyping.java diff --git a/framework/tests/flow2/CustomContractWithArgs.java b/framework/tests/flow/CustomContractWithArgs.java similarity index 100% rename from framework/tests/flow2/CustomContractWithArgs.java rename to framework/tests/flow/CustomContractWithArgs.java diff --git a/framework/tests/flow2/Equal.java b/framework/tests/flow/Equal.java similarity index 100% rename from framework/tests/flow2/Equal.java rename to framework/tests/flow/Equal.java diff --git a/framework/tests/flow2/FieldShadowing.java b/framework/tests/flow/FieldShadowing.java similarity index 100% rename from framework/tests/flow2/FieldShadowing.java rename to framework/tests/flow/FieldShadowing.java diff --git a/framework/tests/flow2/Issue4449.java b/framework/tests/flow/Issue4449.java similarity index 100% rename from framework/tests/flow2/Issue4449.java rename to framework/tests/flow/Issue4449.java diff --git a/framework/tests/flow2/Issue951.java b/framework/tests/flow/Issue951.java similarity index 100% rename from framework/tests/flow2/Issue951.java rename to framework/tests/flow/Issue951.java diff --git a/framework/tests/flow2/MetaPostcondition.java b/framework/tests/flow/MetaPostcondition.java similarity index 100% rename from framework/tests/flow2/MetaPostcondition.java rename to framework/tests/flow/MetaPostcondition.java diff --git a/framework/tests/flow2/MetaPrecondition.java b/framework/tests/flow/MetaPrecondition.java similarity index 100% rename from framework/tests/flow2/MetaPrecondition.java rename to framework/tests/flow/MetaPrecondition.java diff --git a/framework/tests/flow2/MethodCallFlowExpr.java b/framework/tests/flow/MethodCallFlowExpr.java similarity index 100% rename from framework/tests/flow2/MethodCallFlowExpr.java rename to framework/tests/flow/MethodCallFlowExpr.java diff --git a/framework/tests/flow2/Monotonic.java b/framework/tests/flow/Monotonic.java similarity index 100% rename from framework/tests/flow2/Monotonic.java rename to framework/tests/flow/Monotonic.java diff --git a/framework/tests/flow2/NonMethodCode.java b/framework/tests/flow/NonMethodCode.java similarity index 100% rename from framework/tests/flow2/NonMethodCode.java rename to framework/tests/flow/NonMethodCode.java diff --git a/framework/tests/flow2/ParamFlowExpr.java b/framework/tests/flow/ParamFlowExpr.java similarity index 100% rename from framework/tests/flow2/ParamFlowExpr.java rename to framework/tests/flow/ParamFlowExpr.java diff --git a/framework/tests/flow2/Postcondition.java b/framework/tests/flow/Postcondition.java similarity index 100% rename from framework/tests/flow2/Postcondition.java rename to framework/tests/flow/Postcondition.java diff --git a/framework/tests/flow2/Precondition.java b/framework/tests/flow/Precondition.java similarity index 100% rename from framework/tests/flow2/Precondition.java rename to framework/tests/flow/Precondition.java diff --git a/framework/tests/flow2/Purity.java b/framework/tests/flow/Purity.java similarity index 100% rename from framework/tests/flow2/Purity.java rename to framework/tests/flow/Purity.java diff --git a/framework/tests/flow2/StorePure.java b/framework/tests/flow/StorePure.java similarity index 100% rename from framework/tests/flow2/StorePure.java rename to framework/tests/flow/StorePure.java diff --git a/framework/tests/flow2/Termination.java b/framework/tests/flow/Termination.java similarity index 100% rename from framework/tests/flow2/Termination.java rename to framework/tests/flow/Termination.java diff --git a/framework/tests/flow2/flowexpression-scope/Class1.java b/framework/tests/flow/flowexpression-scope/Class1.java similarity index 100% rename from framework/tests/flow2/flowexpression-scope/Class1.java rename to framework/tests/flow/flowexpression-scope/Class1.java diff --git a/framework/tests/flow2/flowexpression-scope/Class2.java b/framework/tests/flow/flowexpression-scope/Class2.java similarity index 100% rename from framework/tests/flow2/flowexpression-scope/Class2.java rename to framework/tests/flow/flowexpression-scope/Class2.java diff --git a/framework/tests/flow2/flowexpression-scope/Issue862.java b/framework/tests/flow/flowexpression-scope/Issue862.java similarity index 100% rename from framework/tests/flow2/flowexpression-scope/Issue862.java rename to framework/tests/flow/flowexpression-scope/Issue862.java diff --git a/framework/tests/flow2/README b/framework/tests/flow2/README deleted file mode 100644 index d1199887d8e..00000000000 --- a/framework/tests/flow2/README +++ /dev/null @@ -1,5 +0,0 @@ -To add a new file to the test suite, see - ../README - -To run the tests, do - (cd $CHECKERFRAMEWORK && ./gradlew Flow2Test) From 24daa9894bbdcba5c76d2f287e5baaa2ddefb3fa Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 13:04:29 -0700 Subject: [PATCH 09/29] Rename `queue` to `classQueue` --- .../type/GenericAnnotatedTypeFactory.java | 24 +++++++++---------- 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java index 0f031c3de08..d84608d5a5d 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -1289,14 +1289,14 @@ protected void performFlowAnalysis(ClassTree classTree) { return; } - Queue> queue = new ArrayDeque<>(); + Queue> classQueue = new ArrayDeque<>(); List> fieldValues = new ArrayList<>(); // No captured store for top-level classes. - queue.add(Pair.of(classTree, null)); + classQueue.add(Pair.of(classTree, null)); - while (!queue.isEmpty()) { - final Pair qel = queue.remove(); + while (!classQueue.isEmpty()) { + final Pair qel = classQueue.remove(); final ClassTree ct = qel.first; final Store capturedStore = qel.second; scannedClasses.put(ct, ScanState.IN_PROGRESS); @@ -1352,7 +1352,7 @@ protected void performFlowAnalysis(ClassTree classTree) { if (initializer != null) { boolean isStatic = vt.getModifiers().getFlags().contains(Modifier.STATIC); analyze( - queue, + classQueue, lambdaQueue, new CFGStatement(vt, ct), fieldValues, @@ -1376,12 +1376,12 @@ protected void performFlowAnalysis(ClassTree classTree) { case ENUM: // Visit inner and nested class trees. // TODO: Use no store for them? What can be captured? - queue.add(Pair.of((ClassTree) m, capturedStore)); + classQueue.add(Pair.of((ClassTree) m, capturedStore)); break; case BLOCK: BlockTree b = (BlockTree) m; analyze( - queue, + classQueue, lambdaQueue, new CFGStatement(b, ct), fieldValues, @@ -1402,7 +1402,7 @@ protected void performFlowAnalysis(ClassTree classTree) { // fields of superclasses. for (CFGMethod met : methods) { analyze( - queue, + classQueue, lambdaQueue, met, fieldValues, @@ -1419,7 +1419,7 @@ protected void performFlowAnalysis(ClassTree classTree) { (MethodTree) TreePathUtil.enclosingOfKind(getPath(lambdaPair.first), Tree.Kind.METHOD); analyze( - queue, + classQueue, lambdaQueue, new CFGLambda(lambdaPair.first, classTree, mt), fieldValues, @@ -1468,7 +1468,7 @@ public int compare(Tree t1, Tree t2) { * Analyze the AST {@code ast} and store the result. Additional operations that should be * performed after analysis should be implemented in {@link #postAnalyze(ControlFlowGraph)}. * - * @param queue the queue for encountered class trees and their initial stores + * @param queue the classQueue for encountered class trees and their initial stores * @param lambdaQueue the queue for encountered lambda expression trees and their initial stores * @param ast the AST to analyze * @param fieldValues the abstract values for all fields of the same class @@ -1480,7 +1480,7 @@ public int compare(Tree t1, Tree t2) { * @see #postAnalyze(org.checkerframework.dataflow.cfg.ControlFlowGraph) */ protected void analyze( - Queue> queue, + Queue> classQueue, Queue> lambdaQueue, UnderlyingAST ast, List> fieldValues, @@ -1559,7 +1559,7 @@ protected void analyze( // add classes declared in CFG for (ClassTree cls : cfg.getDeclaredClasses()) { - queue.add(Pair.of(cls, getStoreBefore(cls))); + classQueue.add(Pair.of(cls, getStoreBefore(cls))); } // add lambdas declared in CFG for (LambdaExpressionTree lambda : cfg.getDeclaredLambdas()) { From 57a50221a383908ec80cbe2a96f9b4ce00d396fc Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 13:06:02 -0700 Subject: [PATCH 10/29] Tweak comments --- .../type/GenericAnnotatedTypeFactory.java | 29 ++++++++++--------- 1 file changed, 16 insertions(+), 13 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java index d84608d5a5d..4640083e09c 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -1312,6 +1312,8 @@ protected void performFlowAnalysis(ClassTree classTree) { Queue> lambdaQueue = new ArrayDeque<>(); + // Queue up classes (for top-level whire loop) and methods (for within this try construct); + // analyze top-level blocks and variable initializers as they are encountered. try { List methods = new ArrayList<>(); List members = ct.getMembers(); @@ -1323,6 +1325,14 @@ protected void performFlowAnalysis(ClassTree classTree) { } for (Tree m : members) { switch (TreeUtils.getKindRecordAsClass(m)) { + case CLASS: // Including RECORD + case ANNOTATION_TYPE: + case INTERFACE: + case ENUM: + // Visit inner and nested class trees. + // TODO: Use no store for them? What can be captured? + classQueue.add(Pair.of((ClassTree) m, capturedStore)); + break; case METHOD: MethodTree mt = (MethodTree) m; @@ -1370,14 +1380,6 @@ protected void performFlowAnalysis(ClassTree classTree) { } fieldValues.add(new FieldInitialValue<>(fieldExpr, declaredValue, null)); break; - case CLASS: // Including RECORD - case ANNOTATION_TYPE: - case INTERFACE: - case ENUM: - // Visit inner and nested class trees. - // TODO: Use no store for them? What can be captured? - classQueue.add(Pair.of((ClassTree) m, capturedStore)); - break; case BLOCK: BlockTree b = (BlockTree) m; analyze( @@ -1468,7 +1470,7 @@ public int compare(Tree t1, Tree t2) { * Analyze the AST {@code ast} and store the result. Additional operations that should be * performed after analysis should be implemented in {@link #postAnalyze(ControlFlowGraph)}. * - * @param queue the classQueue for encountered class trees and their initial stores + * @param classQueue the queue for encountered class trees and their initial stores * @param lambdaQueue the queue for encountered lambda expression trees and their initial stores * @param ast the AST to analyze * @param fieldValues the abstract values for all fields of the same class @@ -1820,8 +1822,8 @@ protected void addComputedTypeAnnotations(Tree tree, AnnotatedTypeMirror type, b * Flow analysis will be performed if all of the following are true. * *
    - *
  • tree is a {@link ClassTree} - *
  • Flow analysis has not already been performed on tree + *
  • {@code tree} is a {@link ClassTree} + *
  • Flow analysis has not already been performed on {@code tree} *
* * @param tree the tree to check and possibly perform flow analysis on @@ -1831,8 +1833,9 @@ protected void checkAndPerformFlowAnalysis(Tree tree) { // on the ClassTree before it's called on any code contained in the class, // so that we can perform flow analysis on the class. Previously we // used TreePath.getPath to find enclosing classes, but that call - // alone consumed more than 10% of execution time. See BaseTypeVisitor - // .visitClass for the call to getAnnotatedType that triggers analysis. + // alone consumed more than 10% of execution time. See + // BaseTypeVisitor.visitClass for the call to getAnnotatedType that + // triggers analysis. if (tree instanceof ClassTree) { ClassTree classTree = (ClassTree) tree; if (!scannedClasses.containsKey(classTree)) { From 2cf19675b36742b46d7c186cd767b285ed5f7d20 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 13:09:41 -0700 Subject: [PATCH 11/29] Delete unused JUnit test --- .../framework/test/junit/Flow2Test.java | 27 ------------------- 1 file changed, 27 deletions(-) delete mode 100644 framework/src/test/java/org/checkerframework/framework/test/junit/Flow2Test.java diff --git a/framework/src/test/java/org/checkerframework/framework/test/junit/Flow2Test.java b/framework/src/test/java/org/checkerframework/framework/test/junit/Flow2Test.java deleted file mode 100644 index f439bdb2b06..00000000000 --- a/framework/src/test/java/org/checkerframework/framework/test/junit/Flow2Test.java +++ /dev/null @@ -1,27 +0,0 @@ -package org.checkerframework.framework.test.junit; - -import java.io.File; -import java.util.List; -import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest; -import org.checkerframework.framework.testchecker.util.FlowTestChecker; -import org.junit.runners.Parameterized.Parameters; - -/** - * Tests for the flow-sensitive part of the framework. These tests complement the tests of {@link - * FlowTest} and have been written when the org.checkerframework.dataflow analysis has been - * completely rewritten. - */ -public class Flow2Test extends CheckerFrameworkPerDirectoryTest { - - /** - * @param testFiles the files containing test code, which will be type-checked - */ - public Flow2Test(List testFiles) { - super(testFiles, FlowTestChecker.class, "flow", "-Anomsgtext", "-AcheckPurityAnnotations"); - } - - @Parameters - public static String[] getTestDirs() { - return new String[] {"flow2"}; - } -} From 979221e7c3be4fcfa3876daeeb9193f846b520de Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 13:17:53 -0700 Subject: [PATCH 12/29] Fix typo --- .../framework/type/GenericAnnotatedTypeFactory.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java index 4640083e09c..afed1fc2a2c 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -1312,8 +1312,8 @@ protected void performFlowAnalysis(ClassTree classTree) { Queue> lambdaQueue = new ArrayDeque<>(); - // Queue up classes (for top-level whire loop) and methods (for within this try construct); - // analyze top-level blocks and variable initializers as they are encountered. + // Queue up classes (for top-level `while` loop) and methods (for within this `try` + // construct); analyze top-level blocks and variable initializers as they are encountered. try { List methods = new ArrayList<>(); List members = ct.getMembers(); From 8cafd5f3c60d391d3a6c1aabe90e1da7e2065977 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 13:18:27 -0700 Subject: [PATCH 13/29] Refactoring --- .../type/GenericAnnotatedTypeFactory.java | 49 ++++++++++--------- 1 file changed, 26 insertions(+), 23 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java index 9d7d37573ef..cda6f800227 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -1289,14 +1289,14 @@ protected void performFlowAnalysis(ClassTree classTree) { return; } - Queue> queue = new ArrayDeque<>(); + Queue> classQueue = new ArrayDeque<>(); List> fieldValues = new ArrayList<>(); // No captured store for top-level classes. - queue.add(Pair.of(classTree, null)); + classQueue.add(Pair.of(classTree, null)); - while (!queue.isEmpty()) { - final Pair qel = queue.remove(); + while (!classQueue.isEmpty()) { + final Pair qel = classQueue.remove(); final ClassTree ct = qel.first; final Store capturedStore = qel.second; scannedClasses.put(ct, ScanState.IN_PROGRESS); @@ -1312,6 +1312,8 @@ protected void performFlowAnalysis(ClassTree classTree) { Queue> lambdaQueue = new ArrayDeque<>(); + // Queue up classes (for top-level `while` loop) and methods (for within this `try` + // construct); analyze top-level blocks and variable initializers as they are encountered. try { List methods = new ArrayList<>(); List members = ct.getMembers(); @@ -1323,6 +1325,14 @@ protected void performFlowAnalysis(ClassTree classTree) { } for (Tree m : members) { switch (TreeUtils.getKindRecordAsClass(m)) { + case CLASS: // Including RECORD + case ANNOTATION_TYPE: + case INTERFACE: + case ENUM: + // Visit inner and nested class trees. + // TODO: Use no store for them? What can be captured? + classQueue.add(Pair.of((ClassTree) m, capturedStore)); + break; case METHOD: MethodTree mt = (MethodTree) m; @@ -1352,7 +1362,7 @@ protected void performFlowAnalysis(ClassTree classTree) { if (initializer != null) { boolean isStatic = vt.getModifiers().getFlags().contains(Modifier.STATIC); analyze( - queue, + classQueue, lambdaQueue, new CFGStatement(vt, ct), fieldValues, @@ -1370,18 +1380,10 @@ protected void performFlowAnalysis(ClassTree classTree) { } fieldValues.add(new FieldInitialValue<>(fieldExpr, declaredValue, null)); break; - case CLASS: // Including RECORD - case ANNOTATION_TYPE: - case INTERFACE: - case ENUM: - // Visit inner and nested class trees. - // TODO: Use no store for them? What can be captured? - queue.add(Pair.of((ClassTree) m, capturedStore)); - break; case BLOCK: BlockTree b = (BlockTree) m; analyze( - queue, + classQueue, lambdaQueue, new CFGStatement(b, ct), fieldValues, @@ -1402,7 +1404,7 @@ protected void performFlowAnalysis(ClassTree classTree) { // fields of superclasses. for (CFGMethod met : methods) { analyze( - queue, + classQueue, lambdaQueue, met, fieldValues, @@ -1419,7 +1421,7 @@ protected void performFlowAnalysis(ClassTree classTree) { (MethodTree) TreePathUtil.enclosingOfKind(getPath(lambdaPair.first), Tree.Kind.METHOD); analyze( - queue, + classQueue, lambdaQueue, new CFGLambda(lambdaPair.first, classTree, mt), fieldValues, @@ -1468,7 +1470,7 @@ public int compare(Tree t1, Tree t2) { * Analyze the AST {@code ast} and store the result. Additional operations that should be * performed after analysis should be implemented in {@link #postAnalyze(ControlFlowGraph)}. * - * @param queue the queue for encountered class trees and their initial stores + * @param classQueue the queue for encountered class trees and their initial stores * @param lambdaQueue the queue for encountered lambda expression trees and their initial stores * @param ast the AST to analyze * @param fieldValues the abstract values for all fields of the same class @@ -1480,7 +1482,7 @@ public int compare(Tree t1, Tree t2) { * @see #postAnalyze(org.checkerframework.dataflow.cfg.ControlFlowGraph) */ protected void analyze( - Queue> queue, + Queue> classQueue, Queue> lambdaQueue, UnderlyingAST ast, List> fieldValues, @@ -1559,7 +1561,7 @@ protected void analyze( // add classes declared in CFG for (ClassTree cls : cfg.getDeclaredClasses()) { - queue.add(Pair.of(cls, getStoreBefore(cls))); + classQueue.add(Pair.of(cls, getStoreBefore(cls))); } // add lambdas declared in CFG for (LambdaExpressionTree lambda : cfg.getDeclaredLambdas()) { @@ -1820,8 +1822,8 @@ protected void addComputedTypeAnnotations(Tree tree, AnnotatedTypeMirror type, b * Flow analysis will be performed if all of the following are true. * *
    - *
  • tree is a {@link ClassTree} - *
  • Flow analysis has not already been performed on tree + *
  • {@code tree} is a {@link ClassTree} + *
  • Flow analysis has not already been performed on {@code tree} *
* * @param tree the tree to check and possibly perform flow analysis on @@ -1831,8 +1833,9 @@ protected void checkAndPerformFlowAnalysis(Tree tree) { // on the ClassTree before it's called on any code contained in the class, // so that we can perform flow analysis on the class. Previously we // used TreePath.getPath to find enclosing classes, but that call - // alone consumed more than 10% of execution time. See BaseTypeVisitor - // .visitClass for the call to getAnnotatedType that triggers analysis. + // alone consumed more than 10% of execution time. See + // BaseTypeVisitor.visitClass for the call to getAnnotatedType that + // triggers analysis. if (tree instanceof ClassTree) { ClassTree classTree = (ClassTree) tree; if (!scannedClasses.containsKey(classTree)) { From 147c207f84be967b7c9a1ff8fcd2c96069bb5e90 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 13:18:37 -0700 Subject: [PATCH 14/29] Tweak manual --- dataflow/manual/content.tex | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/dataflow/manual/content.tex b/dataflow/manual/content.tex index aa8cd8a4b43..bf6605ea2b9 100644 --- a/dataflow/manual/content.tex +++ b/dataflow/manual/content.tex @@ -1740,10 +1740,11 @@ \subsection{Interaction of the Checker Framework and the Dataflow Analysis} and set the constructor parameter \code{useFlow} to true will automatically run dataflow analysis and use the result of the analysis when creating an \code{AnnotatedTypeMirror}. The first time that a \code{GenericAnnotatedTypeFactory} -instance visits a \code{ClassTree}, the type factory runs the dataflow analysis on all the field initializers of the class first, then the bodies of methods in +instance visits a \code{ClassTree}, the type factory runs the dataflow analysis +on all the field initializers of the class first, then the bodies of methods in the class, and then finally the dataflow analysis is -ran recursively on the members of nested classes. The result of -dataflow analysis are stored in the \code{GenericAnnotatedTypeFactory} instance. +run recursively on the members of nested classes. The result of +dataflow analysis is stored in the \code{GenericAnnotatedTypeFactory} instance. When creating an \code{AnnotatedTypeMirror} for a tree node, the type factory queries the result of the dataflow analysis to determine if a more refined From 95ecff574e1769db195c60f415df331d3b8f5e38 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 13:21:35 -0700 Subject: [PATCH 15/29] Checkpoint --- .../checker/lock/LockAnnotatedTypeFactory.java | 4 ++-- .../framework/type/GenericAnnotatedTypeFactory.java | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java index c222ffa632e..304b0934ebe 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java @@ -150,13 +150,13 @@ public LockAnnotatedTypeFactory(BaseTypeChecker checker) { // This alias is only true for the Lock Checker. All other checkers must // ignore the @LockingFree annotation. - addAliasedDeclAnnotation(LockingFree.class, SideEffectFree.class, SIDEEFFECTFREE); + // addAliasedDeclAnnotation(LockingFree.class, SideEffectFree.class, SIDEEFFECTFREE); // This alias is only true for the Lock Checker. All other checkers must // ignore the @ReleasesNoLocks annotation. Note that ReleasesNoLocks is // not truly side-effect-free even as far as the Lock Checker is concerned, // so there is additional handling of this annotation in the Lock Checker. - addAliasedDeclAnnotation(ReleasesNoLocks.class, SideEffectFree.class, SIDEEFFECTFREE); + // addAliasedDeclAnnotation(ReleasesNoLocks.class, SideEffectFree.class, SIDEEFFECTFREE); jcipGuardedBy = classForNameOrNull("net.jcip.annotations.GuardedBy"); diff --git a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java index cda6f800227..80bf482b542 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -1289,6 +1289,7 @@ protected void performFlowAnalysis(ClassTree classTree) { return; } + // class trees an their initial stores Queue> classQueue = new ArrayDeque<>(); List> fieldValues = new ArrayList<>(); From b6ea009e1aa29f36795b2a636c67e2f1b7c6d77b Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 13:22:28 -0700 Subject: [PATCH 16/29] Add comment --- .../framework/type/GenericAnnotatedTypeFactory.java | 1 + 1 file changed, 1 insertion(+) diff --git a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java index afed1fc2a2c..fb053ce0360 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -1289,6 +1289,7 @@ protected void performFlowAnalysis(ClassTree classTree) { return; } + // class trees and their initial stores Queue> classQueue = new ArrayDeque<>(); List> fieldValues = new ArrayList<>(); From b2f4641a60adbb18afc4b1d9c5808d5f3c21e2a4 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 13:46:28 -0700 Subject: [PATCH 17/29] Undo some changes --- .../checker/lock/LockStore.java | 4 +- .../dataflow/util/PurityChecker.java | 2 +- .../dataflow/util/PurityUtils.java | 40 +++---------------- docs/CHANGELOG.md | 4 +- .../common/basetype/BaseTypeVisitor.java | 6 +-- .../type/GenericAnnotatedTypeFactory.java | 2 +- 6 files changed, 14 insertions(+), 44 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java b/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java index 9f9ac013726..2a15cc333eb 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java @@ -185,8 +185,8 @@ public void updateForMethodCall( super.updateForMethodCall(n, atypeFactory, val); ExecutableElement method = n.getTarget().getMethod(); // The following behavior is similar to setting the sideEffectsUnrefineAliases field of - // Lockannotatedtypefactory, but it affects only one of the two type hierarchies, so it - // cannot use that logic. + // Lockannotatedtypefactory, but it affects only the LockPosssiblyHeld type hierarchy (not the + // @GuardedBy hierarchy), so it cannot use that logic. if (!isSideEffectFree(atypeFactory, method)) { // After the call to super.updateForMethodCall, only final fields are left in fieldValues (if // the method called is side-effecting). For the LockPossiblyHeld hierarchy, even a final diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java index aa9fbdd28de..d66be25f1ab 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java @@ -232,7 +232,7 @@ public Void visitMethodInvocation(MethodInvocationTree node, Void ignore) { (assumeDeterministic && assumeSideEffectFree) // Avoid computation if not necessary ? detAndSeFree - : PurityUtils.getPurityAnnotations(annoProvider, elt); + : PurityUtils.getPurityKinds(annoProvider, elt); boolean det = assumeDeterministic || purityKinds.contains(Kind.DETERMINISTIC); boolean seFree = assumeSideEffectFree || purityKinds.contains(Kind.SIDE_EFFECT_FREE); if (!det && !seFree) { diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java index a7ff50d2913..c77388220e9 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java @@ -31,7 +31,7 @@ public class PurityUtils { * @return whether the method has any purity annotations */ public static boolean hasPurityAnnotation(AnnotationProvider provider, MethodTree methodTree) { - return !getPurityAnnotations(provider, methodTree).isEmpty(); + return !getPurityKinds(provider, methodTree).isEmpty(); } /** @@ -43,7 +43,7 @@ public static boolean hasPurityAnnotation(AnnotationProvider provider, MethodTre */ public static boolean hasPurityAnnotation( AnnotationProvider provider, ExecutableElement methodElement) { - return !getPurityAnnotations(provider, methodElement).isEmpty(); + return !getPurityKinds(provider, methodElement).isEmpty(); } /** @@ -70,7 +70,7 @@ public static boolean isDeterministic(AnnotationProvider provider, MethodTree me */ public static boolean isDeterministic( AnnotationProvider provider, ExecutableElement methodElement) { - EnumSet kinds = getPurityAnnotations(provider, methodElement); + EnumSet kinds = getPurityKinds(provider, methodElement); return kinds.contains(Kind.DETERMINISTIC); } @@ -98,24 +98,10 @@ public static boolean isSideEffectFree(AnnotationProvider provider, MethodTree m */ public static boolean isSideEffectFree( AnnotationProvider provider, ExecutableElement methodElement) { - EnumSet kinds = getPurityAnnotations(provider, methodElement); + EnumSet kinds = getPurityKinds(provider, methodElement); return kinds.contains(Kind.SIDE_EFFECT_FREE); } - /** - * Returns the purity annotations of the method {@code methodTree}. - * - * @param provider how to get annotations - * @param methodTree a method to test - * @return the types of purity of the method {@code methodTree} - * @deprecated use {@code getPurityAnnotations} - */ - @Deprecated // 2022-09-27 - public static EnumSet getPurityKinds( - AnnotationProvider provider, MethodTree methodTree) { - return getPurityAnnotations(provider, methodTree); - } - /** * Returns the purity annotations on the method {@code methodTree}. * @@ -123,13 +109,13 @@ public static EnumSet getPurityKinds( * @param methodTree a method to test * @return the types of purity of the method {@code methodTree} */ - public static EnumSet getPurityAnnotations( + public static EnumSet getPurityKinds( AnnotationProvider provider, MethodTree methodTree) { ExecutableElement methodElement = TreeUtils.elementFromDeclaration(methodTree); if (methodElement == null) { throw new BugInCF("Could not find element for tree: " + methodTree); } - return getPurityAnnotations(provider, methodElement); + return getPurityKinds(provider, methodElement); } /** @@ -138,23 +124,9 @@ public static EnumSet getPurityAnnotations( * @param provider how to get annotations * @param methodElement a method to test * @return the types of purity of the method {@code methodElement} - * @deprecated use {@code getPurityAnnotations} */ - @Deprecated // 2022-09-27 public static EnumSet getPurityKinds( AnnotationProvider provider, ExecutableElement methodElement) { - return getPurityAnnotations(provider, methodElement); - } - - /** - * Returns the types of purity of the method {@code methodElement}. - * - * @param provider how to get annotations - * @param methodElement a method to test - * @return the types of purity of the method {@code methodElement} - */ - public static EnumSet getPurityAnnotations( - AnnotationProvider provider, ExecutableElement methodElement) { // Special case for record accessors if (ElementUtils.isRecordAccessor(methodElement)) { return EnumSet.of(Kind.DETERMINISTIC, Kind.SIDE_EFFECT_FREE); diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index fbf18c3280b..2fc4eb59a78 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -13,9 +13,7 @@ introduced since JDK 11). **Implementation details:** -Deprecated methods: - * `TreeUtils.constructor()` => `TreeUtils.elementFromUse()` - * `PurityUtils.getPurityKinds()` => `PurityUtils.getPurityAnnotations()` +Deprecated `TreeUtils.constructor()` in favor of `TreeUtils.elementFromUse()`. Use `TreeUtils.elementFromDeclaration` and `TreeUtils.elementFromUse` in preference to `TreeUtils.elementFromTree`, when possible. diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 9d9e1b16b39..1488fce1b69 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -980,7 +980,7 @@ protected void checkPurity(MethodTree node) { } // check "no" purity - EnumSet kinds = PurityUtils.getPurityAnnotations(atypeFactory, node); + EnumSet kinds = PurityUtils.getPurityKinds(atypeFactory, node); // @Deterministic makes no sense for a void method or constructor boolean isDeterministic = kinds.contains(Pure.Kind.DETERMINISTIC); if (isDeterministic) { @@ -3710,9 +3710,9 @@ private void checkPurity() { // check purity annotations EnumSet superPurity = - PurityUtils.getPurityAnnotations(atypeFactory, overridden.getElement()); + PurityUtils.getPurityKinds(atypeFactory, overridden.getElement()); EnumSet subPurity = - PurityUtils.getPurityAnnotations(atypeFactory, overrider.getElement()); + PurityUtils.getPurityKinds(atypeFactory, overrider.getElement()); if (!subPurity.containsAll(superPurity)) { checker.reportError( overriderTree, diff --git a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java index 1c6444b32b4..fb053ce0360 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -1289,7 +1289,7 @@ protected void performFlowAnalysis(ClassTree classTree) { return; } - // class trees an their initial stores + // class trees and their initial stores Queue> classQueue = new ArrayDeque<>(); List> fieldValues = new ArrayList<>(); From 389ae02e54b3fc371b71f721ebfc5412fe20b1fe Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 15:19:17 -0700 Subject: [PATCH 18/29] Checkpoint --- .../lock/LockAnnotatedTypeFactory.java | 8 +++++ .../checker/lock/LockStore.java | 15 +--------- .../dataflow/util/PurityUtils.java | 8 +++++ docs/CHANGELOG.md | 8 +++-- .../framework/flow/CFAbstractStore.java | 7 +++-- .../framework/type/AnnotatedTypeFactory.java | 29 +++++++++++++++++-- .../javacutil/AnnotationProvider.java | 10 +++++++ .../javacutil/BasicAnnotationProvider.java | 24 +++++++++++++++ 8 files changed, 88 insertions(+), 21 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java index 304b0934ebe..3cf6057a371 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java @@ -805,4 +805,12 @@ private AnnotationMirror createGuardedByAnnotationMirror(List values) { // Return the resulting AnnotationMirror return builder.build(); } + + @Override + public boolean isSideEffectFree(ExecutableElement method) { + SideEffectAnnotation seAnno = methodSideEffectAnnotation(method, false); + return seAnno == SideEffectAnnotation.RELEASESNOLOCKS + || seAnno == SideEffectAnnotation.LOCKINGFREE + || super.isSideEffectFree(method); + } } diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java b/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java index 2a15cc333eb..a5d21aa35f5 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java @@ -4,7 +4,6 @@ import java.util.Set; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.ExecutableElement; -import org.checkerframework.checker.lock.LockAnnotatedTypeFactory.SideEffectAnnotation; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; import org.checkerframework.dataflow.cfg.visualize.CFGVisualizer; @@ -17,7 +16,6 @@ import org.checkerframework.dataflow.expression.ThisReference; import org.checkerframework.framework.flow.CFAbstractStore; import org.checkerframework.framework.flow.CFValue; -import org.checkerframework.framework.source.SourceChecker; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.QualifierHierarchy; import org.checkerframework.javacutil.AnnotationUtils; @@ -168,17 +166,6 @@ protected String internalVisualize(CFGVisualizer viz) { + super.internalVisualize(viz); } - @Override - protected boolean isSideEffectFree(AnnotatedTypeFactory atypeFactory, ExecutableElement method) { - LockAnnotatedTypeFactory lockAnnotatedTypeFactory = (LockAnnotatedTypeFactory) atypeFactory; - SourceChecker checker = lockAnnotatedTypeFactory.getChecker(); - return checker.hasOption("assumeSideEffectFree") - || checker.hasOption("assumePure") - || lockAnnotatedTypeFactory.methodSideEffectAnnotation(method, false) - == SideEffectAnnotation.RELEASESNOLOCKS - || super.isSideEffectFree(atypeFactory, method); - } - @Override public void updateForMethodCall( MethodInvocationNode n, AnnotatedTypeFactory atypeFactory, CFValue val) { @@ -187,7 +174,7 @@ public void updateForMethodCall( // The following behavior is similar to setting the sideEffectsUnrefineAliases field of // Lockannotatedtypefactory, but it affects only the LockPosssiblyHeld type hierarchy (not the // @GuardedBy hierarchy), so it cannot use that logic. - if (!isSideEffectFree(atypeFactory, method)) { + if (!atypeFactory.isSideEffectFree(method)) { // After the call to super.updateForMethodCall, only final fields are left in fieldValues (if // the method called is side-effecting). For the LockPossiblyHeld hierarchy, even a final // field might be locked or unlocked by a side-effecting method. So, final fields must be set diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java index c77388220e9..d85b05061c8 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java @@ -77,10 +77,15 @@ public static boolean isDeterministic( /** * Is the method {@code methodTree} side-effect-free? * + *

This does not use {@link AnnotationProvider#isSideEffectFree()}, it is concerned only with + * standard purity annotations. + * * @param provider how to get annotations * @param methodTree a method to test * @return whether the method is side-effect-free + * @deprecated use {@link AnnotationProvider.isSideEffectFree} */ + @Deprecated // 2022-09-27 public static boolean isSideEffectFree(AnnotationProvider provider, MethodTree methodTree) { ExecutableElement methodElement = TreeUtils.elementFromDeclaration(methodTree); if (methodElement == null) { @@ -92,6 +97,9 @@ public static boolean isSideEffectFree(AnnotationProvider provider, MethodTree m /** * Is the method {@code methodElement} side-effect-free? * + *

This does not use {@link AnnotationProvider#isSideEffectFree()}, it is concerned only with + * standard purity annotations. + * * @param provider how to get annotations * @param methodElement a method to test * @return whether the method is side-effect-free diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 2fc4eb59a78..fca7b7235fa 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -15,11 +15,15 @@ introduced since JDK 11). Deprecated `TreeUtils.constructor()` in favor of `TreeUtils.elementFromUse()`. +Deprecated `CFAbstractStore.isSideEffectFree()` in favor of new method +`AnnotationProvider.isSideEffectFree()`. Note the different contracts of +`PurityUtils.isSideEffectFree()` and `AnnotationProvider.isSideEffectFree()`. + Use `TreeUtils.elementFromDeclaration` and `TreeUtils.elementFromUse` in preference to `TreeUtils.elementFromTree`, when possible. -Use Spotless for formatting; the relevant commands are `./gradlew spotlessCheck` -and `./gradlew spotlessApply`. +For code formatting, use `./gradlew spotlessCheck` and `./gradlew spotlessApply`. +The `checkFormat` and `reformat` Gradle tasks have been removed. **Closed issues:** diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java index d66bcb6dfab..0ea9445ea76 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -33,7 +33,6 @@ import org.checkerframework.dataflow.expression.MethodCall; import org.checkerframework.dataflow.expression.ThisReference; import org.checkerframework.dataflow.qual.SideEffectFree; -import org.checkerframework.dataflow.util.PurityUtils; import org.checkerframework.framework.qual.MonotonicQualifier; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; @@ -181,9 +180,11 @@ public void initializeThisValue(AnnotationMirror a, TypeMirror underlyingType) { * @param atypeFactory the type factory used to retrieve annotations on the method element * @param method the method element * @return whether the method is side-effect-free + * @deprecated use {@link AnnotatatedTypeFactory#isSideEffectFree} */ + @Deprecated // 2022-09-27 protected boolean isSideEffectFree(AnnotatedTypeFactory atypeFactory, ExecutableElement method) { - return PurityUtils.isSideEffectFree(atypeFactory, method); + return atypeFactory.isSideEffectFree(method); } /* --------------------------------------------------------- */ @@ -214,7 +215,7 @@ public void updateForMethodCall( // case 1: remove information if necessary if (!(analysis.checker.hasOption("assumeSideEffectFree") || analysis.checker.hasOption("assumePure") - || isSideEffectFree(atypeFactory, method))) { + || atypeFactory.isSideEffectFree(method))) { boolean sideEffectsUnrefineAliases = ((GenericAnnotatedTypeFactory) atypeFactory).sideEffectsUnrefineAliases; 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 9eb064ec95e..6d2c7c2902c 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -336,6 +336,12 @@ public class AnnotatedTypeFactory implements AnnotationProvider { private SimpleAnnotatedTypeScanner atmInitializer = new SimpleAnnotatedTypeScanner<>((type1, q) -> null); + /** + * True if all methods should be assumed to be @SideEffectFree, for the purposes of + * org.checkerframework.dataflow analysis. + */ + private final boolean assumeSideEffectFree; + /** * Initializes all fields of {@code type}. * @@ -517,6 +523,9 @@ public AnnotatedTypeFactory(BaseTypeChecker checker) { this.processingEnv = checker.getProcessingEnvironment(); // this.root = root; this.checker = checker; + this.assumeSideEffectFree = + checker.hasOption("assumeSideEffectFree") || checker.hasOption("assumePure"); + this.trees = Trees.instance(processingEnv); this.elements = processingEnv.getElementUtils(); this.types = processingEnv.getTypeUtils(); @@ -5422,8 +5431,8 @@ public boolean areSameByClass(AnnotationMirror am, Class a } /** - * Checks that the collection contains the annotation. Using Collection.contains does not always - * work, because it does not use areSame for comparison. + * Checks that the collection contains the annotation. Using {@code Collection.contains} does not + * always work, because it does not use {@code areSame()} for comparison. * *

This method is faster than {@link AnnotationUtils#containsSameByClass(Collection, Class)} * because is caches the name of the class rather than computing it each time. @@ -5583,4 +5592,20 @@ public boolean isImmutable(TypeMirror type) { } return ImmutableTypes.isImmutable(TypeAnnotationUtils.unannotatedType(type).toString()); } + + @Override + public boolean isSideEffectFree(ExecutableElement methodElement) { + if (assumeSideEffectFree) { + return true; + } + + for (AnnotationMirror anno : getDeclAnnotations(methodElement)) { + if (areSameByClass(anno, org.checkerframework.dataflow.qual.SideEffectFree.class) + || areSameByClass(anno, org.checkerframework.dataflow.qual.Pure.class) + || areSameByClass(anno, org.jmlspecs.annotation.Pure.class)) { + return true; + } + } + return false; + } } diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java index 3452a5b2f6c..74e0f1ef091 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java @@ -4,6 +4,7 @@ import java.lang.annotation.Annotation; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; +import javax.lang.model.element.ExecutableElement; import org.checkerframework.checker.nullness.qual.Nullable; // This class exists to break a circular dependency between the dataflow framework and @@ -31,4 +32,13 @@ public interface AnnotationProvider { * @return the annotation on {@code tree} that has the class {@code target}, or null */ @Nullable AnnotationMirror getAnnotationMirror(Tree tree, Class target); + + /** + * Returns true if the given method is side-effect-free according to this AnnotationProvider + * — that is, if a call to the given method does not undo flow-sensitive type refinement. + * + * @param methodElement a method + * @return true if a call to the method does not undo flow-sensitive type refinement + */ + public boolean isSideEffectFree(ExecutableElement methodElement); } diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java b/javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java index 20e72ec2d5c..7460fd78be5 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java @@ -5,6 +5,7 @@ import java.util.List; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; +import javax.lang.model.element.ExecutableElement; import org.checkerframework.checker.nullness.qual.Nullable; /** An AnnotationProvider that is independent of any type hierarchy. */ @@ -41,4 +42,27 @@ public class BasicAnnotationProvider implements AnnotationProvider { Tree tree, Class target) { return null; } + + /** + * {@inheritDoc} + * + *

This implementation returns true if the {@code @SideEffectFree} annotation is present on the + * given method. + */ + @Override + public boolean isSideEffectFree(ExecutableElement methodElement) { + List annotationMirrors = methodElement.getAnnotationMirrors(); + + // Then look at the real annotations. + for (AnnotationMirror am : annotationMirrors) { + @SuppressWarnings("deprecation") // method intended for use by the hierarchy + boolean found = + AnnotationUtils.areSameByName(am, "org.checkerframework.dataflow.qual.SideEffectFree"); + if (found) { + return true; + } + } + + return false; + } } From d1ae162dbfe87c95a6788513b9a870798900e8a9 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 15:24:54 -0700 Subject: [PATCH 19/29] Update documentation --- .../java/org/checkerframework/dataflow/util/PurityUtils.java | 5 +++-- .../org/checkerframework/javacutil/AnnotationProvider.java | 3 +++ 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java index d85b05061c8..3fe731fad0b 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java @@ -77,8 +77,9 @@ public static boolean isDeterministic( /** * Is the method {@code methodTree} side-effect-free? * - *

This does not use {@link AnnotationProvider#isSideEffectFree()}, it is concerned only with - * standard purity annotations. + *

This method does not use, and has different semantics than, {@link + * AnnotationProvider#isSideEffectFree()}. This method is concerned only with standard purity + * annotations. * * @param provider how to get annotations * @param methodTree a method to test diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java index 74e0f1ef091..da24705a99b 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java @@ -37,6 +37,9 @@ public interface AnnotationProvider { * Returns true if the given method is side-effect-free according to this AnnotationProvider * — that is, if a call to the given method does not undo flow-sensitive type refinement. * + *

Note that this method takes account of this AnnotationProvider's semantics, whereas {@code + * org.checkerframework.dataflow.util.PurityUtils#isSideEffectFree} does not. + * * @param methodElement a method * @return true if a call to the method does not undo flow-sensitive type refinement */ From 666efda3fa759a3d5e5af99a96d66a8422d6dabf Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 15:29:02 -0700 Subject: [PATCH 20/29] Add documentation, refine type --- .../checker/lock/LockAnnotatedTypeFactory.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java index 0ed3425431e..b3444c8a17e 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java @@ -503,10 +503,11 @@ public static SideEffectAnnotation weakest() { * @param element the method element * @param issueErrorIfMoreThanOnePresent whether to issue an error if more than one side effect * annotation is present on the method + * @return the side effect annotation that is present on the given method */ // package-private SideEffectAnnotation methodSideEffectAnnotation( - Element element, boolean issueErrorIfMoreThanOnePresent) { + ExecutableElement element, boolean issueErrorIfMoreThanOnePresent) { if (element == null) { // When there is not enough information to determine the correct side effect annotation, // return the weakest one. From 9bb9b4187105ad80e4c92b47ad3117545183ee29 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 15:30:32 -0700 Subject: [PATCH 21/29] Rename formal parameter --- .../checker/lock/LockAnnotatedTypeFactory.java | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java index b3444c8a17e..12b7d89906b 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java @@ -500,15 +500,15 @@ public static SideEffectAnnotation weakest() { * annotation is present, return RELEASESNOLOCKS as the default, and MAYRELEASELOCKS as the * conservative default. * - * @param element the method element + * @param methodElement the method element * @param issueErrorIfMoreThanOnePresent whether to issue an error if more than one side effect * annotation is present on the method * @return the side effect annotation that is present on the given method */ // package-private SideEffectAnnotation methodSideEffectAnnotation( - ExecutableElement element, boolean issueErrorIfMoreThanOnePresent) { - if (element == null) { + ExecutableElement methodElement, boolean issueErrorIfMoreThanOnePresent) { + if (methodElement == null) { // When there is not enough information to determine the correct side effect annotation, // return the weakest one. return SideEffectAnnotation.weakest(); @@ -517,7 +517,7 @@ SideEffectAnnotation methodSideEffectAnnotation( Set sideEffectAnnotationPresent = EnumSet.noneOf(SideEffectAnnotation.class); for (SideEffectAnnotation sea : SideEffectAnnotation.values()) { - if (getDeclAnnotationNoAliases(element, sea.getAnnotationClass()) != null) { + if (getDeclAnnotationNoAliases(methodElement, sea.getAnnotationClass()) != null) { sideEffectAnnotationPresent.add(sea); } } @@ -525,14 +525,14 @@ SideEffectAnnotation methodSideEffectAnnotation( int count = sideEffectAnnotationPresent.size(); if (count == 0) { - return defaults.applyConservativeDefaults(element) + return defaults.applyConservativeDefaults(methodElement) ? SideEffectAnnotation.MAYRELEASELOCKS : SideEffectAnnotation.RELEASESNOLOCKS; } if (count > 1 && issueErrorIfMoreThanOnePresent) { // TODO: Turn on after figuring out how this interacts with inherited annotations. - // checker.reportError(element, "multiple.sideeffect.annotations"); + // checker.reportError(methodElement, "multiple.sideeffect.annotations"); } SideEffectAnnotation weakest = null; From fd5cb17a270da83b0d44420fc4f437dbe8b13baa Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 15:42:17 -0700 Subject: [PATCH 22/29] Remove diagnostics --- .../lock/LockAnnotatedTypeFactory.java | 50 ---------------- .../common/basetype/BaseTypeVisitor.java | 1 + .../framework/flow/CFAbstractStore.java | 2 +- .../checkerframework/javacutil/FileUtils.java | 60 ------------------- 4 files changed, 2 insertions(+), 111 deletions(-) delete mode 100644 javacutil/src/main/java/org/checkerframework/javacutil/FileUtils.java diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java index 3cf6057a371..0faa0af0097 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java @@ -4,9 +4,6 @@ import com.sun.source.tree.MethodInvocationTree; import com.sun.source.tree.Tree; import com.sun.source.tree.VariableTree; -import java.io.File; -import java.io.IOException; -import java.io.PrintStream; import java.lang.annotation.Annotation; import java.util.ArrayList; import java.util.Arrays; @@ -64,7 +61,6 @@ import org.checkerframework.javacutil.AnnotationBuilder; import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.ElementUtils; -import org.checkerframework.javacutil.FileUtils; import org.checkerframework.javacutil.TreeUtils; import org.checkerframework.javacutil.TypeSystemError; import org.plumelib.util.CollectionsPlume; @@ -84,20 +80,6 @@ public class LockAnnotatedTypeFactory extends GenericAnnotatedTypeFactory { - static final PrintStream log; - - static { - try { - log = - new PrintStream( - FileUtils.createTempFile( - new File(System.getProperty("user.dir")).toPath(), "latf", ".log") - .toFile()); - } catch (IOException e) { - throw new Error(e); - } - } - /** dependent type annotation error message for when the expression is not effectively final. */ public static final String NOT_EFFECTIVELY_FINAL = "lock expression is not effectively final"; @@ -148,16 +130,6 @@ public class LockAnnotatedTypeFactory public LockAnnotatedTypeFactory(BaseTypeChecker checker) { super(checker, true); - // This alias is only true for the Lock Checker. All other checkers must - // ignore the @LockingFree annotation. - // addAliasedDeclAnnotation(LockingFree.class, SideEffectFree.class, SIDEEFFECTFREE); - - // This alias is only true for the Lock Checker. All other checkers must - // ignore the @ReleasesNoLocks annotation. Note that ReleasesNoLocks is - // not truly side-effect-free even as far as the Lock Checker is concerned, - // so there is additional handling of this annotation in the Lock Checker. - // addAliasedDeclAnnotation(ReleasesNoLocks.class, SideEffectFree.class, SIDEEFFECTFREE); - jcipGuardedBy = classForNameOrNull("net.jcip.annotations.GuardedBy"); javaxGuardedBy = classForNameOrNull("javax.annotation.concurrent.GuardedBy"); @@ -531,17 +503,6 @@ SideEffectAnnotation methodSideEffectAnnotation( return SideEffectAnnotation.weakest(); } - boolean doLog = - element.getEnclosingElement().toString().endsWith("InstructionContextQueue") - && element.toString().startsWith("add("); - - if (doLog) { - log.printf( - "methodSideEffectAnnotation(%s . %s, %s)%n", - element.getEnclosingElement(), element, issueErrorIfMoreThanOnePresent); - log.printf(" decl annotations = %s%n", getDeclAnnotations(element)); - } - Set sideEffectAnnotationPresent = EnumSet.noneOf(SideEffectAnnotation.class); for (SideEffectAnnotation sea : SideEffectAnnotation.values()) { @@ -551,12 +512,6 @@ SideEffectAnnotation methodSideEffectAnnotation( } int count = sideEffectAnnotationPresent.size(); - if (doLog) { - log.printf( - " methodSideEffectAnnotation(): present (size %d) = %s%n", - count, sideEffectAnnotationPresent); - } - if (count == 0) { return defaults.applyConservativeDefaults(element) ? SideEffectAnnotation.MAYRELEASELOCKS @@ -575,11 +530,6 @@ SideEffectAnnotation methodSideEffectAnnotation( weakest = sea; } } - if (doLog) { - log.printf( - " methodSideEffectAnnotation(%s . %s, %s) => %s%n", - element.getEnclosingElement(), element, issueErrorIfMoreThanOnePresent, weakest); - } return weakest; } diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 1488fce1b69..2194d1abf66 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -230,6 +230,7 @@ public class BaseTypeVisitor... attrs) - throws IOException { - return createTempFile(Path.of(System.getProperty("java.io.tmpdir")), prefix, suffix, attrs); - } - - /** - * Creates a new empty file in the specified directory, using the given prefix and suffix strings - * to generate its name. This is like {@link File#createTempFile}, but uses sequential file names. - * - * @param dir the path to directory in which to create the file - * @param prefix the prefix string to be used in generating the file's name; may be null - * @param suffix the suffix string to be used in generating the file's name; may be null, in which - * case ".tmp" is used - * @param attrs an optional list of file attributes to set atomically when creating the file - * @return the path to the newly created file that did not exist before this method was invoked - * @throws IllegalArgumentException if there is trouble creating the file - */ - public static Path createTempFile( - Path dir, String prefix, String suffix, FileAttribute... attrs) throws IOException { - Path createdDir = Files.createDirectories(dir, attrs); - for (int i = 1; i < Integer.MAX_VALUE; i++) { - File candidate = new File(createdDir.toFile(), prefix + i + suffix); - if (!candidate.exists()) { - System.out.println("Created " + candidate); - return candidate.toPath(); - } - } - throw new Error("every file exists"); - } -} From 97c27c76c3fccd905124fe34beaee0ff04160ecd Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 15:49:16 -0700 Subject: [PATCH 23/29] Miscellaneous documentation improvements --- .../org/checkerframework/checker/lock/LockStore.java | 4 ++-- dataflow/manual/content.tex | 7 ++++--- .../checkerframework/dataflow/util/PurityChecker.java | 6 +++++- .../org/checkerframework/dataflow/util/PurityUtils.java | 7 ++++--- .../framework/type/AnnotatedTypeFactory.java | 4 ++-- .../framework/type/GenericAnnotatedTypeFactory.java | 9 +++++---- 6 files changed, 22 insertions(+), 15 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java b/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java index 9f9ac013726..2a15cc333eb 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockStore.java @@ -185,8 +185,8 @@ public void updateForMethodCall( super.updateForMethodCall(n, atypeFactory, val); ExecutableElement method = n.getTarget().getMethod(); // The following behavior is similar to setting the sideEffectsUnrefineAliases field of - // Lockannotatedtypefactory, but it affects only one of the two type hierarchies, so it - // cannot use that logic. + // Lockannotatedtypefactory, but it affects only the LockPosssiblyHeld type hierarchy (not the + // @GuardedBy hierarchy), so it cannot use that logic. if (!isSideEffectFree(atypeFactory, method)) { // After the call to super.updateForMethodCall, only final fields are left in fieldValues (if // the method called is side-effecting). For the LockPossiblyHeld hierarchy, even a final diff --git a/dataflow/manual/content.tex b/dataflow/manual/content.tex index aa8cd8a4b43..bf6605ea2b9 100644 --- a/dataflow/manual/content.tex +++ b/dataflow/manual/content.tex @@ -1740,10 +1740,11 @@ \subsection{Interaction of the Checker Framework and the Dataflow Analysis} and set the constructor parameter \code{useFlow} to true will automatically run dataflow analysis and use the result of the analysis when creating an \code{AnnotatedTypeMirror}. The first time that a \code{GenericAnnotatedTypeFactory} -instance visits a \code{ClassTree}, the type factory runs the dataflow analysis on all the field initializers of the class first, then the bodies of methods in +instance visits a \code{ClassTree}, the type factory runs the dataflow analysis +on all the field initializers of the class first, then the bodies of methods in the class, and then finally the dataflow analysis is -ran recursively on the members of nested classes. The result of -dataflow analysis are stored in the \code{GenericAnnotatedTypeFactory} instance. +run recursively on the members of nested classes. The result of +dataflow analysis is stored in the \code{GenericAnnotatedTypeFactory} instance. When creating an \code{AnnotatedTypeMirror} for a tree node, the type factory queries the result of the dataflow analysis to determine if a more refined diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java index ed20a8bb891..d66be25f1ab 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java @@ -218,6 +218,10 @@ public Void visitCatch(CatchTree node, Void ignore) { return super.visitCatch(node, ignore); } + /** Represents a method that is both deterministic and side-effect free. */ + private static final EnumSet detAndSeFree = + EnumSet.of(Kind.DETERMINISTIC, Kind.SIDE_EFFECT_FREE); + @Override public Void visitMethodInvocation(MethodInvocationTree node, Void ignore) { ExecutableElement elt = TreeUtils.elementFromUse(node); @@ -227,7 +231,7 @@ public Void visitMethodInvocation(MethodInvocationTree node, Void ignore) { EnumSet purityKinds = (assumeDeterministic && assumeSideEffectFree) // Avoid computation if not necessary - ? EnumSet.of(Kind.DETERMINISTIC, Kind.SIDE_EFFECT_FREE) + ? detAndSeFree : PurityUtils.getPurityKinds(annoProvider, elt); boolean det = assumeDeterministic || purityKinds.contains(Kind.DETERMINISTIC); boolean seFree = assumeSideEffectFree || purityKinds.contains(Kind.SIDE_EFFECT_FREE); diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java index 01b689d2b85..c77388220e9 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java @@ -103,7 +103,7 @@ public static boolean isSideEffectFree( } /** - * Returns the types of purity of the method {@code methodTree}. + * Returns the purity annotations on the method {@code methodTree}. * * @param provider how to get annotations * @param methodTree a method to test @@ -119,18 +119,19 @@ public static EnumSet getPurityKinds( } /** - * Returns the types of purity of the method {@code methodElement}. + * Returns the purity annotations on the method {@code methodElement}. * * @param provider how to get annotations * @param methodElement a method to test * @return the types of purity of the method {@code methodElement} */ - // TODO: should the return type be an EnumSet? public static EnumSet getPurityKinds( AnnotationProvider provider, ExecutableElement methodElement) { + // Special case for record accessors if (ElementUtils.isRecordAccessor(methodElement)) { return EnumSet.of(Kind.DETERMINISTIC, Kind.SIDE_EFFECT_FREE); } + AnnotationMirror pureAnnotation = provider.getDeclAnnotation(methodElement, Pure.class); AnnotationMirror sefAnnotation = provider.getDeclAnnotation(methodElement, SideEffectFree.class); 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 9eb064ec95e..8aeb2e47905 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -5422,8 +5422,8 @@ public boolean areSameByClass(AnnotationMirror am, Class a } /** - * Checks that the collection contains the annotation. Using Collection.contains does not always - * work, because it does not use areSame for comparison. + * Checks that the collection contains the annotation. Using {@code Collection.contains} does not + * always work, because it does not use {@code areSame()} for comparison. * *

This method is faster than {@link AnnotationUtils#containsSameByClass(Collection, Class)} * because is caches the name of the class rather than computing it each time. diff --git a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java index 0f031c3de08..af6eae49a2c 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -1820,8 +1820,8 @@ protected void addComputedTypeAnnotations(Tree tree, AnnotatedTypeMirror type, b * Flow analysis will be performed if all of the following are true. * *

    - *
  • tree is a {@link ClassTree} - *
  • Flow analysis has not already been performed on tree + *
  • {@code tree} is a {@link ClassTree} + *
  • Flow analysis has not already been performed on {@code tree} *
* * @param tree the tree to check and possibly perform flow analysis on @@ -1831,8 +1831,9 @@ protected void checkAndPerformFlowAnalysis(Tree tree) { // on the ClassTree before it's called on any code contained in the class, // so that we can perform flow analysis on the class. Previously we // used TreePath.getPath to find enclosing classes, but that call - // alone consumed more than 10% of execution time. See BaseTypeVisitor - // .visitClass for the call to getAnnotatedType that triggers analysis. + // alone consumed more than 10% of execution time. See + // BaseTypeVisitor.visitClass for the call to getAnnotatedType that + // triggers analysis. if (tree instanceof ClassTree) { ClassTree classTree = (ClassTree) tree; if (!scannedClasses.containsKey(classTree)) { From 17a31547d0dff7a34d1113784a31b0b5aeebee27 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 15:52:08 -0700 Subject: [PATCH 24/29] Move a comma --- checker/tests/wpi-many/testin.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/checker/tests/wpi-many/testin.txt b/checker/tests/wpi-many/testin.txt index 69d5014a200..b4aacc4b055 100644 --- a/checker/tests/wpi-many/testin.txt +++ b/checker/tests/wpi-many/testin.txt @@ -3,5 +3,5 @@ https://github.com/kelloggm/wpi-many-tests-bibtex-clean b7ac872c9323a0944015cd79 https://github.com/kelloggm/wpi-many-tests-ensures-called-methods db816432c95a3d047a1e3f7966fefb1515cba7c9 https://github.com/kelloggm/wpi-many-tests-html-pretty-print 1c4f2da82407e21eb89a9196f06d613a64af211a https://github.com/kelloggm/-wpi-many-tests-bibtex-clean 7a70d58b9fdaedd71c4af4a9dfca7d5fda9268dc -# This comment line tests that the commenting feature works (if it doesn't then, this line will be read and fail, as it's not a URL). +# This comment line tests that the commenting feature works (if it doesn't, then this line will be read and fail, as it's not a URL). https://github.com/Nargeshdb/wpi-many-tests-owning-field 6accab941bdae0274862ab414d729851851670ea From 8e5c74c29c1b50e3e79075913e320fb1da2a71f9 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 15:54:07 -0700 Subject: [PATCH 25/29] Undo changes --- checker/tests/wpi-many/testin.txt | 12 ++++++------ docs/CHANGELOG.md | 2 ++ 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/checker/tests/wpi-many/testin.txt b/checker/tests/wpi-many/testin.txt index f9ce34aa437..b4aacc4b055 100644 --- a/checker/tests/wpi-many/testin.txt +++ b/checker/tests/wpi-many/testin.txt @@ -1,7 +1,7 @@ https://github.com/kelloggm/wpi-many-tests-bcel-util 74be0b18f893077223850d5ffb117e496c4b833a -# https://github.com/kelloggm/wpi-many-tests-bibtex-clean b7ac872c9323a0944015cd79014e45fb7a5d1c93 -# https://github.com/kelloggm/wpi-many-tests-ensures-called-methods db816432c95a3d047a1e3f7966fefb1515cba7c9 -# https://github.com/kelloggm/wpi-many-tests-html-pretty-print 1c4f2da82407e21eb89a9196f06d613a64af211a -# https://github.com/kelloggm/-wpi-many-tests-bibtex-clean 7a70d58b9fdaedd71c4af4a9dfca7d5fda9268dc -# # This comment line tests that the commenting feature works (if it doesn't, then this line will be read and fail, as it's not a URL). -# https://github.com/Nargeshdb/wpi-many-tests-owning-field 6accab941bdae0274862ab414d729851851670ea +https://github.com/kelloggm/wpi-many-tests-bibtex-clean b7ac872c9323a0944015cd79014e45fb7a5d1c93 +https://github.com/kelloggm/wpi-many-tests-ensures-called-methods db816432c95a3d047a1e3f7966fefb1515cba7c9 +https://github.com/kelloggm/wpi-many-tests-html-pretty-print 1c4f2da82407e21eb89a9196f06d613a64af211a +https://github.com/kelloggm/-wpi-many-tests-bibtex-clean 7a70d58b9fdaedd71c4af4a9dfca7d5fda9268dc +# This comment line tests that the commenting feature works (if it doesn't, then this line will be read and fail, as it's not a URL). +https://github.com/Nargeshdb/wpi-many-tests-owning-field 6accab941bdae0274862ab414d729851851670ea diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index fca7b7235fa..c86cc08b1d1 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -15,6 +15,8 @@ introduced since JDK 11). Deprecated `TreeUtils.constructor()` in favor of `TreeUtils.elementFromUse()`. +Added method `isSideEffectFree()` to the `AnnotationProvider` interface. + Deprecated `CFAbstractStore.isSideEffectFree()` in favor of new method `AnnotationProvider.isSideEffectFree()`. Note the different contracts of `PurityUtils.isSideEffectFree()` and `AnnotationProvider.isSideEffectFree()`. From 2cdfbd3ff052a419e0209fb27e2ee4c457907699 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 27 Sep 2022 16:42:37 -0700 Subject: [PATCH 26/29] Fix Javadoc cross-references --- .../org/checkerframework/dataflow/util/PurityUtils.java | 9 +++++---- .../checkerframework/framework/flow/CFAbstractStore.java | 2 +- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java index 3fe731fad0b..8f8db6c148e 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java @@ -78,13 +78,13 @@ public static boolean isDeterministic( * Is the method {@code methodTree} side-effect-free? * *

This method does not use, and has different semantics than, {@link - * AnnotationProvider#isSideEffectFree()}. This method is concerned only with standard purity + * AnnotationProvider#isSideEffectFree}. This method is concerned only with standard purity * annotations. * * @param provider how to get annotations * @param methodTree a method to test * @return whether the method is side-effect-free - * @deprecated use {@link AnnotationProvider.isSideEffectFree} + * @deprecated use {@link AnnotationProvider#isSideEffectFree} */ @Deprecated // 2022-09-27 public static boolean isSideEffectFree(AnnotationProvider provider, MethodTree methodTree) { @@ -98,8 +98,9 @@ public static boolean isSideEffectFree(AnnotationProvider provider, MethodTree m /** * Is the method {@code methodElement} side-effect-free? * - *

This does not use {@link AnnotationProvider#isSideEffectFree()}, it is concerned only with - * standard purity annotations. + *

This method does not use, and has different semantics than, {@link + * AnnotationProvider#isSideEffectFree}. This method is concerned only with standard purity + * annotations. * * @param provider how to get annotations * @param methodElement a method to test diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java index e319a61cc5a..65dcc4b8416 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -180,7 +180,7 @@ public void initializeThisValue(AnnotationMirror a, TypeMirror underlyingType) { * @param atypeFactory the type factory used to retrieve annotations on the method element * @param method the method element * @return whether the method is side-effect-free - * @deprecated use {@link AnnotationProvider#isSideEffectFree} + * @deprecated use {@link org.checkerframework.javacutil.AnnotationProvider#isSideEffectFree} */ @Deprecated // 2022-09-27 protected boolean isSideEffectFree(AnnotatedTypeFactory atypeFactory, ExecutableElement method) { From 5e9a80b8f059b8f74d14796e805f9906fefffacf Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Wed, 28 Sep 2022 08:08:01 -0700 Subject: [PATCH 27/29] Tweaks. --- .../java/org/checkerframework/javacutil/AnnotationProvider.java | 2 +- .../org/checkerframework/javacutil/BasicAnnotationProvider.java | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java index da24705a99b..0cb676a7c01 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java @@ -43,5 +43,5 @@ public interface AnnotationProvider { * @param methodElement a method * @return true if a call to the method does not undo flow-sensitive type refinement */ - public boolean isSideEffectFree(ExecutableElement methodElement); + boolean isSideEffectFree(ExecutableElement methodElement); } diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java b/javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java index 7460fd78be5..a303edc87ad 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java @@ -55,7 +55,6 @@ public boolean isSideEffectFree(ExecutableElement methodElement) { // Then look at the real annotations. for (AnnotationMirror am : annotationMirrors) { - @SuppressWarnings("deprecation") // method intended for use by the hierarchy boolean found = AnnotationUtils.areSameByName(am, "org.checkerframework.dataflow.qual.SideEffectFree"); if (found) { From 97217b6abf5fb5a3106852703258efcfd4f43a18 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Wed, 28 Sep 2022 08:25:46 -0700 Subject: [PATCH 28/29] Remove stray comment --- .../org/checkerframework/javacutil/BasicAnnotationProvider.java | 2 -- 1 file changed, 2 deletions(-) diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java b/javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java index 7460fd78be5..38fa4575519 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java @@ -20,7 +20,6 @@ public class BasicAnnotationProvider implements AnnotationProvider { Element elt, Class anno) { List annotationMirrors = elt.getAnnotationMirrors(); - // Then look at the real annotations. for (AnnotationMirror am : annotationMirrors) { @SuppressWarnings("deprecation") // method intended for use by the hierarchy boolean found = AnnotationUtils.areSameByClass(am, anno); @@ -53,7 +52,6 @@ public class BasicAnnotationProvider implements AnnotationProvider { public boolean isSideEffectFree(ExecutableElement methodElement) { List annotationMirrors = methodElement.getAnnotationMirrors(); - // Then look at the real annotations. for (AnnotationMirror am : annotationMirrors) { @SuppressWarnings("deprecation") // method intended for use by the hierarchy boolean found = From acddc03061a3ba9aa7a98836da6463c6cf886b28 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Wed, 28 Sep 2022 09:06:46 -0700 Subject: [PATCH 29/29] Remove `inferPurity` variable --- docs/CHANGELOG.md | 2 ++ .../common/basetype/BaseTypeVisitor.java | 34 ++++++------------- 2 files changed, 13 insertions(+), 23 deletions(-) diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index c86cc08b1d1..b49daa7408e 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -27,6 +27,8 @@ preference to `TreeUtils.elementFromTree`, when possible. For code formatting, use `./gradlew spotlessCheck` and `./gradlew spotlessApply`. The `checkFormat` and `reformat` Gradle tasks have been removed. +Removed variable `BaseTypeVisitor.inferPurity`. + **Closed issues:** diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 2194d1abf66..45d3ac63616 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -230,16 +230,6 @@ public class BaseTypeVisitorSetting to false will break whole-program inference (WPI), because the checker may read - * {@code .ajava} files generated by itself for some classes and {@code .ajava} files generated by - * a different checker for other classes. The failure is nondeterministic: it doesn't always - * occur. - */ - protected boolean inferPurity = true; /** The tree of the enclosing method that is currently being visited. */ protected @Nullable MethodTree methodTree = null; @@ -1011,7 +1001,7 @@ protected void checkPurity(MethodTree node) { if (suggestPureMethods && !TreeUtils.isSynthetic(node)) { // Issue a warning if the method is pure, but not annotated as such. EnumSet additionalKinds = r.getKinds().clone(); - if (!(infer && inferPurity)) { + if (!infer) { // During WPI, propagate all purity kinds, even those that are already // present (because they were inferred in a previous WPI round). additionalKinds.removeAll(kinds); @@ -1021,18 +1011,16 @@ protected void checkPurity(MethodTree node) { } if (!additionalKinds.isEmpty()) { if (infer) { - if (inferPurity) { - WholeProgramInference wpi = atypeFactory.getWholeProgramInference(); - ExecutableElement methodElt = TreeUtils.elementFromDeclaration(node); - if (additionalKinds.size() == 2) { - wpi.addMethodDeclarationAnnotation(methodElt, PURE); - } else if (additionalKinds.contains(Pure.Kind.SIDE_EFFECT_FREE)) { - wpi.addMethodDeclarationAnnotation(methodElt, SIDE_EFFECT_FREE); - } else if (additionalKinds.contains(Pure.Kind.DETERMINISTIC)) { - wpi.addMethodDeclarationAnnotation(methodElt, DETERMINISTIC); - } else { - throw new BugInCF("Unexpected purity kind in " + additionalKinds); - } + WholeProgramInference wpi = atypeFactory.getWholeProgramInference(); + ExecutableElement methodElt = TreeUtils.elementFromDeclaration(node); + if (additionalKinds.size() == 2) { + wpi.addMethodDeclarationAnnotation(methodElt, PURE); + } else if (additionalKinds.contains(Pure.Kind.SIDE_EFFECT_FREE)) { + wpi.addMethodDeclarationAnnotation(methodElt, SIDE_EFFECT_FREE); + } else if (additionalKinds.contains(Pure.Kind.DETERMINISTIC)) { + wpi.addMethodDeclarationAnnotation(methodElt, DETERMINISTIC); + } else { + throw new BugInCF("Unexpected purity kind in " + additionalKinds); } } else { if (additionalKinds.size() == 2) {