From 3c745024f3620f7f711e3955cfcf081165910da1 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Fri, 10 Nov 2023 16:37:02 -0800 Subject: [PATCH 01/16] New command-line option `-AassumePureGetters` --- .../test/junit/OptionalPureGettersTest.java | 28 +++++++ .../PureGetterTest.class | Bin 0 -> 780 bytes .../optional-pure-getters/PureGetterTest.java | 77 ++++++++++++++++++ .../cfg/builder/CFGTranslationPhaseOne.java | 5 +- .../dataflow/util/PurityChecker.java | 21 ++++- .../dataflow/util/PurityUtils.java | 8 +- docs/CHANGELOG.md | 3 + docs/manual/introduction.tex | 7 +- docs/manual/purity-checker.tex | 32 ++++++-- .../common/basetype/BaseTypeVisitor.java | 8 +- .../framework/flow/CFAbstractStore.java | 12 ++- .../framework/source/SourceChecker.java | 2 + .../framework/type/AnnotatedTypeFactory.java | 10 ++- .../javacutil/ElementUtils.java | 22 +++++ 14 files changed, 213 insertions(+), 22 deletions(-) create mode 100644 checker/src/test/java/org/checkerframework/checker/test/junit/OptionalPureGettersTest.java create mode 100644 checker/tests/optional-pure-getters/PureGetterTest.class create mode 100644 checker/tests/optional-pure-getters/PureGetterTest.java diff --git a/checker/src/test/java/org/checkerframework/checker/test/junit/OptionalPureGettersTest.java b/checker/src/test/java/org/checkerframework/checker/test/junit/OptionalPureGettersTest.java new file mode 100644 index 00000000000..be95a29a0df --- /dev/null +++ b/checker/src/test/java/org/checkerframework/checker/test/junit/OptionalPureGettersTest.java @@ -0,0 +1,28 @@ +package org.checkerframework.checker.test.junit; + +import java.io.File; +import java.util.List; +import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest; +import org.junit.runners.Parameterized.Parameters; + +/** JUnit tests for the Optional Checker, which has the {@code @Present} annotation. */ +public class OptionalPureGettersTest extends CheckerFrameworkPerDirectoryTest { + + /** + * Create an OptionalPureGettersTest. + * + * @param testFiles the files containing test code, which will be type-checked + */ + public OptionalPureGettersTest(List testFiles) { + super( + testFiles, + org.checkerframework.checker.optional.OptionalChecker.class, + "optional", + "-AassumePureGetters"); + } + + @Parameters + public static String[] getTestDirs() { + return new String[] {"optional-pure-getters"}; + } +} diff --git a/checker/tests/optional-pure-getters/PureGetterTest.class b/checker/tests/optional-pure-getters/PureGetterTest.class new file mode 100644 index 0000000000000000000000000000000000000000..f180ed6469c0ea432f92080a4be61b3d389b6046 GIT binary patch literal 780 zcmah{(M}UV6g{)8E!{4(w6!XNqGAGlaGy;H2{F-^BE%A!_%>aKW$1RM&dzH16#qhB zF!8|;@S}`(mR$nzfrp)Y=j@$x&$%;y{{H$6U>{pPJXGqa2DpbBL;IY6;bFp693D>3 zMPwOjyHZKJ$57ecIq|WCMjd{DCIW_)qs)kR!dhXDMM}lZSlGjbm0IzHp})N|$_XTB@7Lj9vP7eMWodDqdU_Ja36izQxk?>Nq$2uQ7_?PfJaW; zvbJZ!lwBFBZ}ca@&>Bf4-e>bEY39>}kj7ZXid(Y6Feq7XN#4D(k#`zfBUL=y8!~Ks z$dr|HaUxSmOve`sv9FZ2+zlXQcs&4f8Md@jCfGb@2m7lR5vXFLfH_{CHd zo{771sx^5STOQ30_@a>Nk9B4u@m4zB-P_ZD<>rV@nt(@l3smW&O9jIkWg8TkLk2&= zeo(^jm{#{2sL)3jO3{_B6{Q~gPP?0RHLMfj5!n-pZFoIKN1p<{d?kz~e`9^J<=_(aODumw^D663C_cDGDC-e HuYU0liCdZv literal 0 HcmV?d00001 diff --git a/checker/tests/optional-pure-getters/PureGetterTest.java b/checker/tests/optional-pure-getters/PureGetterTest.java new file mode 100644 index 00000000000..5476f150806 --- /dev/null +++ b/checker/tests/optional-pure-getters/PureGetterTest.java @@ -0,0 +1,77 @@ +import java.util.Optional; + +class PureGetterTest { + + @SuppressWarnings("optional.field") + Optional field; + + Optional getOptional() { + return null; + } + + Optional otherOptional() { + return null; + } + + void sideEffect() {} + + void foo() { + if (field.isPresent()) { + field.get(); + } + if (field.isPresent()) { + sideEffect(); + // :: error: method.invocation + field.get(); + } + if (field.isPresent()) { + getOptional(); + field.get(); + } + if (field.isPresent()) { + otherOptional(); + // :: error: method.invocation + field.get(); + } + + if (getOptional().isPresent()) { + getOptional().get(); + } + if (getOptional().isPresent()) { + sideEffect(); + getOptional().get(); + } + if (getOptional().isPresent()) { + getOptional(); + getOptional().get(); + } + if (getOptional().isPresent()) { + otherOptional(); + getOptional().get(); + } + + if (otherOptional().isPresent()) { + // :: error: method.invocation + otherOptional().get(); + } + if (otherOptional().isPresent()) { + sideEffect(); + // :: error: method.invocation + otherOptional().get(); + } + if (otherOptional().isPresent()) { + getOptional(); + // :: error: method.invocation + otherOptional().get(); + } + if (otherOptional().isPresent()) { + otherOptional(); + // :: error: method.invocation + otherOptional().get(); + } + } + + void bar(Optional os) { + os.get(); + } +} diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java index 95e35710ed6..6fee5c1095a 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java @@ -1458,7 +1458,7 @@ public MethodInvocationNode visitMethodInvocation(MethodInvocationTree tree, Voi // First, compute the receiver, if any (15.12.4.1). // Second, evaluate the actual arguments, left to right and possibly some arguments are - // stored into an array for variable arguments calls (15.12.4.2). + // stored into an array for varargs calls (15.12.4.2). // Third, test the receiver, if any, for nullness (15.12.4.4). // Fourth, convert the arguments to the type of the formal parameters (15.12.4.5). // Fifth, if the method is synchronized, lock the receiving object or class (15.12.4.5). @@ -1528,8 +1528,7 @@ public Node visitAssert(AssertTree tree, Void p) { // see JLS 14.10 - // If assertions are enabled, then we can just translate the - // assertion. + // If assertions are enabled, then we can just translate the assertion. if (assumeAssertionsEnabled || assumeAssertionsEnabledFor(tree)) { translateAssertWithAssertionsEnabled(tree); return null; 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 c249e19ca57..e772f6c6a2b 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java @@ -49,6 +49,7 @@ public class PurityChecker { * @param annoProvider the annotation provider * @param assumeSideEffectFree true if all methods should be assumed to be @SideEffectFree * @param assumeDeterministic true if all methods should be assumed to be @Deterministic + * @param assumePureGetters true if all getter methods should be assumed to be @Pure * @return information about whether the given statement is side-effect-free, deterministic, or * both */ @@ -56,9 +57,11 @@ public static PurityResult checkPurity( TreePath statement, AnnotationProvider annoProvider, boolean assumeSideEffectFree, - boolean assumeDeterministic) { + boolean assumeDeterministic, + boolean assumePureGetters) { PurityCheckerHelper helper = - new PurityCheckerHelper(annoProvider, assumeSideEffectFree, assumeDeterministic); + new PurityCheckerHelper( + annoProvider, assumeSideEffectFree, assumeDeterministic, assumePureGetters); helper.scan(statement, null); return helper.purityResult; } @@ -204,20 +207,29 @@ protected static class PurityCheckerHelper extends TreePathScanner { */ private final boolean assumeDeterministic; + /** + * True if all getter methods should be assumed to be @SideEffectFree and @Deterministic, for + * the purposes of org.checkerframework.dataflow analysis. + */ + private final boolean assumePureGetters; + /** * Create a PurityCheckerHelper. * * @param annoProvider the annotation provider * @param assumeSideEffectFree true if all methods should be assumed to be @SideEffectFree * @param assumeDeterministic true if all methods should be assumed to be @Deterministic + * @param assumePureGetters true if getter methods should be assumed to be @Pure */ public PurityCheckerHelper( AnnotationProvider annoProvider, boolean assumeSideEffectFree, - boolean assumeDeterministic) { + boolean assumeDeterministic, + boolean assumePureGetters) { this.annoProvider = annoProvider; this.assumeSideEffectFree = assumeSideEffectFree; this.assumeDeterministic = assumeDeterministic; + this.assumePureGetters = assumePureGetters; } @Override @@ -237,7 +249,8 @@ public Void visitMethodInvocation(MethodInvocationTree tree, Void ignore) { purityResult.addNotBothReason(tree, "call"); } else { EnumSet purityKinds = - (assumeDeterministic && assumeSideEffectFree) + ((assumeDeterministic && assumeSideEffectFree) + || (assumePureGetters && ElementUtils.isGetter(elt))) // Avoid computation if not necessary ? detAndSeFree : PurityUtils.getPurityKinds(annoProvider, elt); 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 62c66915b8e..558b9592b25 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java @@ -22,6 +22,10 @@ */ public class PurityUtils { + /** Represents a method that is both deterministic and side-effect free. */ + private static final EnumSet detAndSeFree = + EnumSet.of(Pure.Kind.DETERMINISTIC, Pure.Kind.SIDE_EFFECT_FREE); + /** * Does the method {@code methodTree} have any purity annotation? * @@ -139,7 +143,7 @@ public static EnumSet getPurityKinds( // Special case for record accessors if (ElementUtils.isRecordAccessor(methodElement) && ElementUtils.isAutoGeneratedRecordMember(methodElement)) { - return EnumSet.of(Pure.Kind.DETERMINISTIC, Pure.Kind.SIDE_EFFECT_FREE); + return detAndSeFree; } AnnotationMirror pureAnnotation = provider.getDeclAnnotation(methodElement, Pure.class); @@ -148,7 +152,7 @@ public static EnumSet getPurityKinds( AnnotationMirror detAnnotation = provider.getDeclAnnotation(methodElement, Deterministic.class); if (pureAnnotation != null) { - return EnumSet.of(Pure.Kind.DETERMINISTIC, Pure.Kind.SIDE_EFFECT_FREE); + return detAndSeFree; } EnumSet result = EnumSet.noneOf(Pure.Kind.class); if (sefAnnotation != null) { diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 056c1c4a4d9..727a176863a 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -3,6 +3,9 @@ Version 3.40.1 (December 1, 2023) **User-visible changes:** +New command-line options: + -AassumePureGetters Unsoundly assume that every getter method is pure + **Implementation details:** **Closed issues:** diff --git a/docs/manual/introduction.tex b/docs/manual/introduction.tex index 819eed2e1c0..0d931cd1221 100644 --- a/docs/manual/introduction.tex +++ b/docs/manual/introduction.tex @@ -578,9 +578,10 @@ Suppress all errors and warnings within the definition of a given class --- or everywhere except within the definition of a given class. See Section~\ref{askipdefs}. -\item \<-AassumeSideEffectFree>, \<-AassumeDeterministic>, \<-AassumePure> +\item \<-AassumeSideEffectFree>, \<-AassumeDeterministic>, \<-AassumePure>, \<-AassumePureGetters> Unsoundly assume that every method is side-effect-free, deterministic, or - both; see + both; or that every getter method is pure. + See Section~\ref{purity-suppress-warnings} and Section~\ref{type-refinement-purity}. \item \<-AassumeAssertionsAreEnabled>, \<-AassumeAssertionsAreDisabled> Whether to assume that assertions are enabled or disabled; see Section~\ref{type-refinement-assertions}. @@ -1687,4 +1688,4 @@ % LocalWords: requireNonNull ApermitUnsupportedJdkVersion AstubWarnNote % LocalWords: AwarnRedundantAnnotations AinferOutputOriginal % LocalWords: AshowPrefixInWarningMessages AstubNoWarnIfNotFound -% LocalWords: AshowWpiFailedInferences +% LocalWords: AshowWpiFailedInferences AassumePureGetters diff --git a/docs/manual/purity-checker.tex b/docs/manual/purity-checker.tex index 0e30c4f4011..6b5c8f87838 100644 --- a/docs/manual/purity-checker.tex +++ b/docs/manual/purity-checker.tex @@ -105,15 +105,33 @@ \sectionAndLabel{Suppressing warnings}{purity-suppress-warnings} The command-line options \<-AassumeSideEffectFree>, -\<-AassumeDeterministic>, \<-AassumePure> make the Checker Framework unsoundly -assume that \emph{every} called method is side-effect-free, is -deterministic, or is both, respectively. This can make +\<-AassumeDeterministic>, and \<-AassumePure> make the Checker Framework +unsoundly assume that \emph{every} called method is side-effect-free, is +deterministic, or is both, respectively. + +The command-line option \<-AassumePureGetters> makes the Checker Framework +unsoundly assume that every getter method is side-effect-free and +deterministic. For the purposes of \<-AassumePureGetters>, a getter method +is defined as an instance method that starts with ``get[A-Z]'' and has no +formal parameters. + +This can make flow-sensitive type refinement much more effective, since method calls will not cause the analysis to discard information that it has learned. -However, this option can mask real errors. It is most appropriate when you -are starting out annotating a project, or if you are using the Checker -Framework to find some bugs but not to give a guarantee that no more errors -exist of the given type. +However, this option can mask real errors. It is most appropriate when one +of the following is true: +\begin{itemize} +\item + You are starting out annotating a project. +\item + You are using the Checker Framework to find bugs but not to give a + guarantee that no more errors exist of the given type. +\item + You are working with an unannotated library that makes the given + assumptions, in which case (say) using \<-AassumePureGetters> is easier + than writing stub files for all the library's getter methods. +\end{itemize} + %% LocalWords: AsuggestPureMethods AcheckPurityAnnotations %% LocalWords: AsuppressWarnings AassumeSideEffectFree 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 5fc7b97b15b..85e55415cdd 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -261,6 +261,9 @@ public class BaseTypeVisitor getFieldValues() { /** True if -AassumeSideEffectFree or -AassumePure was passed on the command line. */ private final boolean assumeSideEffectFree; + /** True if -AassumePureGetters was passed on the command line. */ + private final boolean assumeSideEffectFreeGetters; + /** The unique ID for the next-created object. */ private static final AtomicLong nextUid = new AtomicLong(0); @@ -143,6 +147,7 @@ protected CFAbstractStore(CFAbstractAnalysis analysis, boolean sequenti assumeSideEffectFree = analysis.checker.hasOption("assumeSideEffectFree") || analysis.checker.hasOption("assumePure"); + assumeSideEffectFreeGetters = analysis.checker.hasOption("assumePureGetters"); } /** @@ -160,6 +165,7 @@ protected CFAbstractStore(CFAbstractStore other) { classValues = new HashMap<>(other.classValues); sequentialSemantics = other.sequentialSemantics; assumeSideEffectFree = other.assumeSideEffectFree; + assumeSideEffectFreeGetters = other.assumeSideEffectFreeGetters; } /** @@ -229,7 +235,11 @@ public void updateForMethodCall( ExecutableElement method = methodInvocationNode.getTarget().getMethod(); // case 1: remove information if necessary - if (!(assumeSideEffectFree || atypeFactory.isSideEffectFree(method))) { + boolean hasSideEffect = + !(assumeSideEffectFree + || (assumeSideEffectFreeGetters && ElementUtils.isGetter(method)) + || atypeFactory.isSideEffectFree(method)); + if (hasSideEffect) { boolean sideEffectsUnrefineAliases = ((GenericAnnotatedTypeFactory) atypeFactory).sideEffectsUnrefineAliases; diff --git a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java index f298f44f7ba..180c6d17c68 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -125,6 +125,8 @@ "assumeSideEffectFree", "assumeDeterministic", "assumePure", + // Unsoundly assume getter methods have no side effects and are deterministic. + "assumePureGetters", // Whether to assume that assertions are enabled or disabled // org.checkerframework.framework.flow.CFCFGBuilder.CFCFGBuilder 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 a5d1ba0a7f7..8b6ed7b2e13 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -373,6 +373,12 @@ public class AnnotatedTypeFactory implements AnnotationProvider { */ private final boolean assumeSideEffectFree; + /** + * True if all getter methods should be assumed to be @SideEffectFree, for the purposes of + * org.checkerframework.dataflow analysis. + */ + private final boolean assumeSideEffectFreeGetters; + /** True if -AmergeStubsWithSource was provided on the command line. */ private final boolean mergeStubsWithSource; @@ -563,6 +569,7 @@ public AnnotatedTypeFactory(BaseTypeChecker checker) { this.checker = checker; this.assumeSideEffectFree = checker.hasOption("assumeSideEffectFree") || checker.hasOption("assumePure"); + this.assumeSideEffectFreeGetters = checker.hasOption("assumePureGetters"); this.trees = Trees.instance(processingEnv); this.elements = processingEnv.getElementUtils(); @@ -5792,7 +5799,8 @@ public boolean isImmutable(TypeMirror type) { @Override public boolean isSideEffectFree(ExecutableElement methodElement) { - if (assumeSideEffectFree) { + if (assumeSideEffectFree + || (assumeSideEffectFreeGetters && ElementUtils.isGetter(methodElement))) { return true; } if (ElementUtils.isRecordAccessor(methodElement) diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java index 3c04709bee6..d4832d53b84 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java @@ -1098,4 +1098,26 @@ public static boolean isCompactCanonicalRecordConstructor(Element elt) { public static boolean isResourceVariable(@Nullable Element elt) { return elt != null && elt.getKind() == ElementKind.RESOURCE_VARIABLE; } + + /** + * Returns true if the given element is a getter method. A getter method is an instance method + * whose name starts with "get[A-Z]" and has no formal parameters. + * + * @param methodElt a method + * @return true if the given element is a getter method + */ + public static boolean isGetter(@Nullable ExecutableElement methodElt) { + if (methodElt == null) { + return false; + } + // Constructors and initializers don't have name starting "get[A-Z]". + String name = methodElt.getSimpleName().toString(); + // I expect this code is more efficient than use of a regular expression. + boolean getterName = + name.startsWith("get") && name.length() > 3 && Character.isUpperCase(name.charAt(3)); + return getterName + // Ensure it is an instance method. + && methodElt.getReceiverType().getKind() != TypeKind.NONE + && methodElt.getParameters().isEmpty(); + } } From fd47257273f2975cacaae2ad25e017eafb093bb5 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Fri, 10 Nov 2023 19:30:16 -0800 Subject: [PATCH 02/16] Checkpoint --- .../optional-pure-getters/PureGetterTest.class | Bin 780 -> 0 bytes .../optional-pure-getters/PureGetterTest.java | 10 ++++------ .../framework/flow/CFAbstractStore.java | 6 +++--- .../checkerframework/javacutil/ElementUtils.java | 7 ++----- 4 files changed, 9 insertions(+), 14 deletions(-) delete mode 100644 checker/tests/optional-pure-getters/PureGetterTest.class diff --git a/checker/tests/optional-pure-getters/PureGetterTest.class b/checker/tests/optional-pure-getters/PureGetterTest.class deleted file mode 100644 index f180ed6469c0ea432f92080a4be61b3d389b6046..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 780 zcmah{(M}UV6g{)8E!{4(w6!XNqGAGlaGy;H2{F-^BE%A!_%>aKW$1RM&dzH16#qhB zF!8|;@S}`(mR$nzfrp)Y=j@$x&$%;y{{H$6U>{pPJXGqa2DpbBL;IY6;bFp693D>3 zMPwOjyHZKJ$57ecIq|WCMjd{DCIW_)qs)kR!dhXDMM}lZSlGjbm0IzHp})N|$_XTB@7Lj9vP7eMWodDqdU_Ja36izQxk?>Nq$2uQ7_?PfJaW; zvbJZ!lwBFBZ}ca@&>Bf4-e>bEY39>}kj7ZXid(Y6Feq7XN#4D(k#`zfBUL=y8!~Ks z$dr|HaUxSmOve`sv9FZ2+zlXQcs&4f8Md@jCfGb@2m7lR5vXFLfH_{CHd zo{771sx^5STOQ30_@a>Nk9B4u@m4zB-P_ZD<>rV@nt(@l3smW&O9jIkWg8TkLk2&= zeo(^jm{#{2sL)3jO3{_B6{Q~gPP?0RHLMfj5!n-pZFoIKN1p<{d?kz~e`9^J<=_(aODumw^D663C_cDGDC-e HuYU0liCdZv diff --git a/checker/tests/optional-pure-getters/PureGetterTest.java b/checker/tests/optional-pure-getters/PureGetterTest.java index 5476f150806..342f14266b1 100644 --- a/checker/tests/optional-pure-getters/PureGetterTest.java +++ b/checker/tests/optional-pure-getters/PureGetterTest.java @@ -39,6 +39,7 @@ void foo() { } if (getOptional().isPresent()) { sideEffect(); + // :: error: method.invocation getOptional().get(); } if (getOptional().isPresent()) { @@ -47,11 +48,12 @@ void foo() { } if (getOptional().isPresent()) { otherOptional(); + // :: error: method.invocation getOptional().get(); } if (otherOptional().isPresent()) { - // :: error: method.invocation + // BUG: https://github.com/typetools/checker-framework/issues/6291 error: method.invocation otherOptional().get(); } if (otherOptional().isPresent()) { @@ -61,7 +63,7 @@ void foo() { } if (otherOptional().isPresent()) { getOptional(); - // :: error: method.invocation + // BUG: https://github.com/typetools/checker-framework/issues/6291 error: method.invocation otherOptional().get(); } if (otherOptional().isPresent()) { @@ -70,8 +72,4 @@ void foo() { otherOptional().get(); } } - - void bar(Optional os) { - os.get(); - } } 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 6b18b92541d..4f7695f9234 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -470,9 +470,9 @@ public final void insertValue(JavaExpression expr, @Nullable V value) { * {@code nondet()} is 3, because it might not be 3 the next time {@code nondet()} is executed. * *

However, contracts can mention a nondeterministic JavaExpression. For example, a contract - * might have a postcondition that{@code nondet()} is odd. This means that the next call to{@code - * nondet()} will return odd. Such a postcondition may be evicted from the store by calling a - * side-effecting method. + * might have a postcondition that {@code nondet()} is odd. This means that the next call to + * {@code nondet()} will return odd. Such a postcondition may be evicted from the store by calling + * a side-effecting method. * * @param expr the expression to insert in the store * @param value the value of the expression diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java index d4832d53b84..7833f99b5b2 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java @@ -1113,11 +1113,8 @@ public static boolean isGetter(@Nullable ExecutableElement methodElt) { // Constructors and initializers don't have name starting "get[A-Z]". String name = methodElt.getSimpleName().toString(); // I expect this code is more efficient than use of a regular expression. - boolean getterName = + boolean isGetterName = name.startsWith("get") && name.length() > 3 && Character.isUpperCase(name.charAt(3)); - return getterName - // Ensure it is an instance method. - && methodElt.getReceiverType().getKind() != TypeKind.NONE - && methodElt.getParameters().isEmpty(); + return isGetterName && !isStatic(methodElt) && methodElt.getParameters().isEmpty(); } } From 961336440bb79c600a0dcaa1ce41aaeecac48b54 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Fri, 10 Nov 2023 21:27:31 -0800 Subject: [PATCH 03/16] Minor updates to purity analysis --- .../cfg/builder/CFGTranslationPhaseOne.java | 5 ++-- .../dataflow/util/PurityUtils.java | 8 +++++-- docs/manual/advanced-features.tex | 23 +++++++++++-------- docs/manual/introduction.tex | 8 ++++--- docs/manual/purity-checker.tex | 20 +++++++++++----- .../framework/flow/CFAbstractStore.java | 6 ++--- 6 files changed, 44 insertions(+), 26 deletions(-) diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java index 95e35710ed6..6fee5c1095a 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java @@ -1458,7 +1458,7 @@ public MethodInvocationNode visitMethodInvocation(MethodInvocationTree tree, Voi // First, compute the receiver, if any (15.12.4.1). // Second, evaluate the actual arguments, left to right and possibly some arguments are - // stored into an array for variable arguments calls (15.12.4.2). + // stored into an array for varargs calls (15.12.4.2). // Third, test the receiver, if any, for nullness (15.12.4.4). // Fourth, convert the arguments to the type of the formal parameters (15.12.4.5). // Fifth, if the method is synchronized, lock the receiving object or class (15.12.4.5). @@ -1528,8 +1528,7 @@ public Node visitAssert(AssertTree tree, Void p) { // see JLS 14.10 - // If assertions are enabled, then we can just translate the - // assertion. + // If assertions are enabled, then we can just translate the assertion. if (assumeAssertionsEnabled || assumeAssertionsEnabledFor(tree)) { translateAssertWithAssertionsEnabled(tree); return null; 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 62c66915b8e..558b9592b25 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java @@ -22,6 +22,10 @@ */ public class PurityUtils { + /** Represents a method that is both deterministic and side-effect free. */ + private static final EnumSet detAndSeFree = + EnumSet.of(Pure.Kind.DETERMINISTIC, Pure.Kind.SIDE_EFFECT_FREE); + /** * Does the method {@code methodTree} have any purity annotation? * @@ -139,7 +143,7 @@ public static EnumSet getPurityKinds( // Special case for record accessors if (ElementUtils.isRecordAccessor(methodElement) && ElementUtils.isAutoGeneratedRecordMember(methodElement)) { - return EnumSet.of(Pure.Kind.DETERMINISTIC, Pure.Kind.SIDE_EFFECT_FREE); + return detAndSeFree; } AnnotationMirror pureAnnotation = provider.getDeclAnnotation(methodElement, Pure.class); @@ -148,7 +152,7 @@ public static EnumSet getPurityKinds( AnnotationMirror detAnnotation = provider.getDeclAnnotation(methodElement, Deterministic.class); if (pureAnnotation != null) { - return EnumSet.of(Pure.Kind.DETERMINISTIC, Pure.Kind.SIDE_EFFECT_FREE); + return detAndSeFree; } EnumSet result = EnumSet.noneOf(Pure.Kind.class); if (sefAnnotation != null) { diff --git a/docs/manual/advanced-features.tex b/docs/manual/advanced-features.tex index d2f10b27355..87430d02453 100644 --- a/docs/manual/advanced-features.tex +++ b/docs/manual/advanced-features.tex @@ -1178,17 +1178,20 @@ If your code contains an \ statement, then your code could behave in two different ways at run time, depending on whether assertions are -enabled or disabled -via the \<-ea> or \<-da> command-line options to java. +enabled or disabled via the \<-ea>, \<-enableassertions>, \<-da>, or +<-disableassertions> command-line options to \. By default, the Checker Framework outputs warnings about any error that could happen at run time, whether assertions are enabled or disabled. If you supply the \<-AassumeAssertionsAreEnabled> command-line option, then -the Checker Framework assumes assertions are enabled. If you supply the +the Checker Framework assumes assertions (that is, Java \ +statements) are enabled, as if Java is run with the \<-ea> or +\<-enableassertions> command-line argument. If you supply the \<-AassumeAssertionsAreDisabled> command-line option, then the Checker -Framework assumes assertions are disabled. You may not supply both -command-line options. It is uncommon to supply either one. +Framework assumes assertions are disabled, as if Java is run with the +\<-da> or \<-disableassertions> command-line argument. You may not supply +both command-line options. It is uncommon to supply either one. These command-line arguments have no effect on processing of \ statements whose message contains the text \<@AssumeAssertion>; see @@ -1620,7 +1623,7 @@ % TO DO: give an example where @Dependent is actually needed -% LocalWords: MyClass qual DefaultQualifier subpackages lang +% LocalWords: MyClass qual DefaultQualifier subpackages lang de package1 % LocalWords: actuals toArray CollectionToArrayHeuristics nn RegexBottom % LocalWords: MyList Nullness DefaultLocation nullness PolyNull util TODO % LocalWords: QualifierDefaults nullable lub persistData updatedAt nble KeyFor @@ -1629,7 +1632,7 @@ % LocalWords: getComponentType enum implementers dereferenced superclasses % LocalWords: regex myStrings myVar pouchSize myMammal getter foo MyAnno % LocalWords: getPouchSize TerminatesExecution myvar myField getField m1 -% LocalWords: computeValue arg myInt Anno Im InheritedAnnotation +% LocalWords: computeValue arg myInt Anno Im InheritedAnnotation package2 % LocalWords: AcheckPurityAnnotations AassumeSideEffectFree iMplicit m2 % LocalWords: AassumeAssertionsAreEnabled myArray vals propkey forName % LocalWords: fenum i18n RequiresQualifier EnsuresQualifier ClassName @@ -1642,5 +1645,7 @@ % LocalWords: EnsuresKeyFor EnsuresKeyForIf DivideByZeroException % LocalWords: EnsuresLockHeld EnsuresLockHeldIf FieldInvariant fieldA % LocalWords: fieldB myMethod SomeType runtime typedefs signedness -% LocalWords: Signedness MonotonicNonNull UpperBoundFor -% LocalWords: getTypeDeclarationBounds identityHashCode +% LocalWords: Signedness MonotonicNonNull UpperBoundFor enableassertions +% LocalWords: getTypeDeclarationBounds identityHashCode disableassertions +% LocalWords: AinvocationPreservesArgumentNullness RequiresPresent +% LocalWords: EnsuresPresent EnsuresPresentIf diff --git a/docs/manual/introduction.tex b/docs/manual/introduction.tex index 819eed2e1c0..f26bd8af07a 100644 --- a/docs/manual/introduction.tex +++ b/docs/manual/introduction.tex @@ -580,10 +580,12 @@ Section~\ref{askipdefs}. \item \<-AassumeSideEffectFree>, \<-AassumeDeterministic>, \<-AassumePure> Unsoundly assume that every method is side-effect-free, deterministic, or - both; see + both. + See Section~\ref{purity-suppress-warnings} and Section~\ref{type-refinement-purity}. \item \<-AassumeAssertionsAreEnabled>, \<-AassumeAssertionsAreDisabled> - Whether to assume that assertions are enabled or disabled; see Section~\ref{type-refinement-assertions}. + Whether to assume that assertions (Java \ statements) are enabled + or disabled; see Section~\ref{type-refinement-assertions}. \item \<-AignoreRangeOverflow> Ignore the possibility of overflow for range annotations such as \<@IntRange>; see Section~\ref{value-checker-overflow}. @@ -1687,4 +1689,4 @@ % LocalWords: requireNonNull ApermitUnsupportedJdkVersion AstubWarnNote % LocalWords: AwarnRedundantAnnotations AinferOutputOriginal % LocalWords: AshowPrefixInWarningMessages AstubNoWarnIfNotFound -% LocalWords: AshowWpiFailedInferences +% LocalWords: AshowWpiFailedInferences AassumePureGetters diff --git a/docs/manual/purity-checker.tex b/docs/manual/purity-checker.tex index 0e30c4f4011..f309dbc8efd 100644 --- a/docs/manual/purity-checker.tex +++ b/docs/manual/purity-checker.tex @@ -105,15 +105,23 @@ \sectionAndLabel{Suppressing warnings}{purity-suppress-warnings} The command-line options \<-AassumeSideEffectFree>, -\<-AassumeDeterministic>, \<-AassumePure> make the Checker Framework unsoundly +\<-AassumeDeterministic>, and \<-AassumePure> make the Checker Framework unsoundly assume that \emph{every} called method is side-effect-free, is -deterministic, or is both, respectively. This can make +deterministic, or is both, respectively. + +This can make flow-sensitive type refinement much more effective, since method calls will not cause the analysis to discard information that it has learned. -However, this option can mask real errors. It is most appropriate when you -are starting out annotating a project, or if you are using the Checker -Framework to find some bugs but not to give a guarantee that no more errors -exist of the given type. +However, this option can mask real errors. It is most appropriate when one +of the following is true: +\begin{itemize} +\item + You are starting out annotating a project. +\item + You are using the Checker Framework to find bugs but not to give a + guarantee that no more errors exist of the given type. +\end{itemize} + %% LocalWords: AsuggestPureMethods AcheckPurityAnnotations %% LocalWords: AsuppressWarnings AassumeSideEffectFree 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 4d77a4f0fd6..f2ddee3e7cd 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -460,9 +460,9 @@ public final void insertValue(JavaExpression expr, @Nullable V value) { * {@code nondet()} is 3, because it might not be 3 the next time {@code nondet()} is executed. * *

However, contracts can mention a nondeterministic JavaExpression. For example, a contract - * might have a postcondition that{@code nondet()} is odd. This means that the next call to{@code - * nondet()} will return odd. Such a postcondition may be evicted from the store by calling a - * side-effecting method. + * might have a postcondition that {@code nondet()} is odd. This means that the next call to + * {@code nondet()} will return odd. Such a postcondition may be evicted from the store by calling + * a side-effecting method. * * @param expr the expression to insert in the store * @param value the value of the expression From fb2fd8db20e1db43f719ed0d9727c58afd55818c Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Fri, 10 Nov 2023 21:32:23 -0800 Subject: [PATCH 04/16] Temporary diagnostics --- .../checker/nullness/NullnessTransfer.java | 4 +++- .../optional-pure-getters/PureGetterTest.java | 1 + .../dataflow/util/PurityUtils.java | 8 ++++++++ .../common/basetype/BaseTypeVisitor.java | 2 +- .../framework/flow/CFAbstractStore.java | 16 ++++++++++++++++ .../javacutil/AnnotationProvider.java | 12 ++++++++++++ 6 files changed, 41 insertions(+), 2 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java index 4076149b917..690a93682e9 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java @@ -386,7 +386,9 @@ public TransferResult visitMethodInvocation( MethodInvocationTree tree = n.getTree(); ExecutableElement method = TreeUtils.elementFromUse(tree); - boolean isMethodSideEffectFree = PurityUtils.isSideEffectFree(atypeFactory, method); + boolean isMethodSideEffectFree = + atypeFactory.isSideEffectFree(method) || PurityUtils.isSideEffectFree(atypeFactory, method); + System.out.printf("isMethodSideEffectFree(%s) = %s%n", method, isMethodSideEffectFree); Node receiver = n.getTarget().getReceiver(); if (nonNullAssumptionAfterInvocation || isMethodSideEffectFree diff --git a/checker/tests/optional-pure-getters/PureGetterTest.java b/checker/tests/optional-pure-getters/PureGetterTest.java index 342f14266b1..f66adb62604 100644 --- a/checker/tests/optional-pure-getters/PureGetterTest.java +++ b/checker/tests/optional-pure-getters/PureGetterTest.java @@ -44,6 +44,7 @@ void foo() { } if (getOptional().isPresent()) { getOptional(); + // :: error: method.invocation getOptional().get(); } if (getOptional().isPresent()) { 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 558b9592b25..f658a2763ba 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java @@ -73,6 +73,14 @@ public static boolean isDeterministic(AnnotationProvider provider, MethodTree me */ public static boolean isDeterministic( AnnotationProvider provider, ExecutableElement methodElement) { + if (provider instanceof BaseTypeVisitor) { + BaseTypeVisitor typeVisitor = (BaseTypeVisitor) provider; + // TODO: Maybe add a method in BaseTypeVisitor that this code can call. + if (typeVisitor.assumePureGetters && ElementUtils.isGetter(methodElement)) { + return true; + } + } + EnumSet kinds = getPurityKinds(provider, methodElement); return kinds.contains(Pure.Kind.DETERMINISTIC); } 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 85e55415cdd..dcad39c59ba 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -262,7 +262,7 @@ public class BaseTypeVisitor !e.isUnmodifiableByOtherCode()); } + System.out.printf(" %s%n", this); + // store information about method call if possible JavaExpression methodCall = JavaExpression.fromNode(methodInvocationNode); + System.out.printf("about to replaceValue(%s, %s)%n", methodCall, val); replaceValue(methodCall, val); + + System.out.printf(" %s%n", this); + System.out.printf("exited updateForMethodCall%n"); } /** @@ -555,6 +565,7 @@ protected void computeNewValueAndInsert( BinaryOperator merger, boolean permitNondeterministic) { if (!shouldInsert(expr, value, permitNondeterministic)) { + System.out.printf("shouldInsert(%s, %s, %s) => false%n", expr, value, permitNondeterministic); return; } @@ -681,8 +692,13 @@ public void insertThisValue(AnnotationMirror a, TypeMirror underlyingType) { * changes to certain parts of the state. */ public void replaceValue(JavaExpression expr, @Nullable V value) { + System.out.printf("entered replaceValue(%s, %s)%n", expr, value); + System.out.printf(" %s%n", this); clearValue(expr); + System.out.printf(" %s%n", this); insertValue(expr, value); + System.out.printf(" %s%n", this); + System.out.printf("exited replaceValue(%s, %s)%n", expr, value); } /** diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java index 0cb676a7c01..ff026b753fb 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java @@ -44,4 +44,16 @@ public interface AnnotationProvider { * @return true if a call to the method does not undo flow-sensitive type refinement */ boolean isSideEffectFree(ExecutableElement methodElement); + + /** + * Returns true if the given method is deterministic according to this AnnotationProvider — + * that is, if multiple calls to the given method (with the same arguments) return the same value. + * + *

Note that this method takes account of this AnnotationProvider's semantics, whereas {@code + * org.checkerframework.dataflow.util.PurityUtils#isDeterministic} does not. + * + * @param methodElement a method + * @return true if multiple calls to the method (with the same arguments) return the same value + */ + boolean isDeterministic(ExecutableElement methodElement); } From 9b73c014789b3b6d02e62b8a78625212b3f976a0 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 11 Nov 2023 06:45:10 -0800 Subject: [PATCH 05/16] Added method `isDeterministic()` to the `AnnotationProvider` interface --- .../dataflow/util/PurityChecker.java | 5 ++++- docs/CHANGELOG.md | 2 ++ .../framework/type/AnnotatedTypeFactory.java | 19 +++++++++++++++++ .../javacutil/AnnotationProvider.java | 12 +++++++++++ .../javacutil/BasicAnnotationProvider.java | 21 +++++++++++++++++++ 5 files changed, 58 insertions(+), 1 deletion(-) 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 c249e19ca57..e112c571d20 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java @@ -291,7 +291,10 @@ public Void visitNewClass(NewClassTree tree, Void ignore) { boolean okThrowDeterministic = parent.getKind() == Tree.Kind.THROW; ExecutableElement ctorElement = TreeUtils.elementFromUse(tree); - boolean deterministic = assumeDeterministic || okThrowDeterministic; + boolean deterministic = + assumeDeterministic + || okThrowDeterministic + || PurityUtils.isDeterministic(annoProvider, ctorElement); boolean sideEffectFree = assumeSideEffectFree || PurityUtils.isSideEffectFree(annoProvider, ctorElement); // This does not use "addNotBothReason" because the reasons are different: one is diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 056c1c4a4d9..5f45dd49a8d 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -5,6 +5,8 @@ Version 3.40.1 (December 1, 2023) **Implementation details:** +Added method `isDeterministic()` to the `AnnotationProvider` interface. + **Closed issues:** 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 a5d1ba0a7f7..d69b4bf21fa 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -5809,6 +5809,25 @@ public boolean isSideEffectFree(ExecutableElement methodElement) { return false; } + @Override + public boolean isDeterministic(ExecutableElement methodElement) { + if (assumeDeterministic) { + return true; + } + if (ElementUtils.isRecordAccessor(methodElement) + && ElementUtils.isAutoGeneratedRecordMember(methodElement)) { + return true; + } + for (AnnotationMirror anno : getDeclAnnotations(methodElement)) { + if (areSameByClass(anno, org.checkerframework.dataflow.qual.Deterministic.class) + || areSameByClass(anno, org.checkerframework.dataflow.qual.Pure.class) + || areSameByClass(anno, org.jmlspecs.annotation.Pure.class)) { + return true; + } + } + return false; + } + /** * Output a message about {@link #getAnnotatedType}, if logging is on. * diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java index 0cb676a7c01..ff026b753fb 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java @@ -44,4 +44,16 @@ public interface AnnotationProvider { * @return true if a call to the method does not undo flow-sensitive type refinement */ boolean isSideEffectFree(ExecutableElement methodElement); + + /** + * Returns true if the given method is deterministic according to this AnnotationProvider — + * that is, if multiple calls to the given method (with the same arguments) return the same value. + * + *

Note that this method takes account of this AnnotationProvider's semantics, whereas {@code + * org.checkerframework.dataflow.util.PurityUtils#isDeterministic} does not. + * + * @param methodElement a method + * @return true if multiple calls to the method (with the same arguments) return the same value + */ + boolean isDeterministic(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 928111530d5..a160fd8a800 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java @@ -62,4 +62,25 @@ public boolean isSideEffectFree(ExecutableElement methodElement) { return false; } + + /** + * {@inheritDoc} + * + *

This implementation returns true if the {@code @Deterministic} annotation is present on the + * given method. + */ + @Override + public boolean isDeterministic(ExecutableElement methodElement) { + List annotationMirrors = methodElement.getAnnotationMirrors(); + + for (AnnotationMirror am : annotationMirrors) { + boolean found = + AnnotationUtils.areSameByName(am, "org.checkerframework.dataflow.qual.Deterministic"); + if (found) { + return true; + } + } + + return false; + } } From 48a21c14c212bbf1d95470c635abdefc2699d2c7 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 11 Nov 2023 06:49:11 -0800 Subject: [PATCH 06/16] Do not instantiate PurityUtils --- .../java/org/checkerframework/dataflow/util/PurityUtils.java | 5 +++++ 1 file changed, 5 insertions(+) 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 558b9592b25..0e38d12d4dc 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java @@ -22,6 +22,11 @@ */ public class PurityUtils { + /** Do not instantiate. */ + private PurityUtils() { + throw new Error("Do not instantiate PurityUtils."); + } + /** Represents a method that is both deterministic and side-effect free. */ private static final EnumSet detAndSeFree = EnumSet.of(Pure.Kind.DETERMINISTIC, Pure.Kind.SIDE_EFFECT_FREE); From e58d92a68ad2d4fecfb1efabe1bd43af4f667f9f Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 11 Nov 2023 06:54:03 -0800 Subject: [PATCH 07/16] Add `assumeDeterministic` variable --- .../framework/type/AnnotatedTypeFactory.java | 8 ++++++++ 1 file changed, 8 insertions(+) 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 d69b4bf21fa..e67c814c8fb 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -373,6 +373,12 @@ public class AnnotatedTypeFactory implements AnnotationProvider { */ private final boolean assumeSideEffectFree; + /** + * True if all methods should be assumed to be @Deterministic, for the purposes of + * org.checkerframework.dataflow analysis. + */ + private final boolean assumeDeterministic; + /** True if -AmergeStubsWithSource was provided on the command line. */ private final boolean mergeStubsWithSource; @@ -563,6 +569,8 @@ public AnnotatedTypeFactory(BaseTypeChecker checker) { this.checker = checker; this.assumeSideEffectFree = checker.hasOption("assumeSideEffectFree") || checker.hasOption("assumePure"); + this.assumeDeterministic = + checker.hasOption("assumeDeterministic") || checker.hasOption("assumePure"); this.trees = Trees.instance(processingEnv); this.elements = processingEnv.getElementUtils(); From 9e39c91607d673d0e3970b8fd339f9f2a0be0140 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 11 Nov 2023 07:02:49 -0800 Subject: [PATCH 08/16] Add comment --- .../org/checkerframework/dataflow/util/PurityUtils.java | 6 ++++-- 1 file changed, 4 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 0e38d12d4dc..12fd1fc2516 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java @@ -123,7 +123,8 @@ public static boolean isSideEffectFree( /** * Returns the purity annotations on the method {@code methodTree}. * - * @param provider how to get annotations + * @param provider how to get annotations. Its {@link AnnotationProvider#isSideEffectFree} method + * is not used. * @param methodTree a method to test * @return the types of purity of the method {@code methodTree} */ @@ -139,7 +140,8 @@ public static EnumSet getPurityKinds( /** * Returns the purity annotations on the method {@code methodElement}. * - * @param provider how to get annotations + * @param provider how to get annotations. Its {@link AnnotationProvider#isSideEffectFree} method + * is not used. * @param methodElement a method to test * @return the types of purity of the method {@code methodElement} */ From 8b46918447cc5b3c6958cf168c7d0aa11fb73fd6 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 11 Nov 2023 07:03:11 -0800 Subject: [PATCH 09/16] Add comment --- .../org/checkerframework/dataflow/util/PurityUtils.java | 6 ++++-- 1 file changed, 4 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 0e38d12d4dc..5cbedb7eb12 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityUtils.java @@ -123,7 +123,8 @@ public static boolean isSideEffectFree( /** * Returns the purity annotations on the method {@code methodTree}. * - * @param provider how to get annotations + * @param provider how to get annotations. Its {@link AnnotationProvider#isSideEffectFree} and + * {@link AnnotationProvider#isDeterministic} methods are not used. * @param methodTree a method to test * @return the types of purity of the method {@code methodTree} */ @@ -139,7 +140,8 @@ public static EnumSet getPurityKinds( /** * Returns the purity annotations on the method {@code methodElement}. * - * @param provider how to get annotations + * @param provider how to get annotations. Its {@link AnnotationProvider#isSideEffectFree} and + * {@link AnnotationProvider#isDeterministic} methods are not used. * @param methodElement a method to test * @return the types of purity of the method {@code methodElement} */ From b695bca8774a02ea8637dad13402f946c30c3c6f Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 11 Nov 2023 07:19:50 -0800 Subject: [PATCH 10/16] parameter => argument --- .../java/org/checkerframework/dataflow/qual/Deterministic.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/checker-qual/src/main/java/org/checkerframework/dataflow/qual/Deterministic.java b/checker-qual/src/main/java/org/checkerframework/dataflow/qual/Deterministic.java index 693898c6800..c56484f0dd6 100644 --- a/checker-qual/src/main/java/org/checkerframework/dataflow/qual/Deterministic.java +++ b/checker-qual/src/main/java/org/checkerframework/dataflow/qual/Deterministic.java @@ -8,7 +8,7 @@ /** * A method is called deterministic if it returns the same value (according to {@code ==}) - * every time it is called with the same parameters and in the same environment. The parameters + * every time it is called with the same arguments and in the same environment. The arguments * include the receiver, and the environment includes all of the Java heap (that is, all fields of * all objects and all static variables). * From 3f94cb5877faeff3399b5be83e6ef8ba906f4be0 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 11 Nov 2023 07:25:54 -0800 Subject: [PATCH 11/16] Text in Dataflow Manual --- dataflow/manual/content.tex | 35 +++++++++++++++-------------------- 1 file changed, 15 insertions(+), 20 deletions(-) diff --git a/dataflow/manual/content.tex b/dataflow/manual/content.tex index 9b37d3e8818..3d95eccde14 100644 --- a/dataflow/manual/content.tex +++ b/dataflow/manual/content.tex @@ -961,9 +961,9 @@ \subsection{Formal Definition of the Control-Flow Graph} Other AST constructs are desugared into the above nodes (see \autoref{sec:desugaring}). -\begin{workinprogress} -Can \code{StringConversionNode} be implicit? I think so, but in any event discuss. -\end{workinprogress} +% \begin{workinprogress} +% Can \code{StringConversionNode} be implicit? I think so, but in any event discuss. +% \end{workinprogress} \subsection{Noteworthy Translations and Node Types} @@ -1267,15 +1267,6 @@ \subsection{AST to CFG Translation} nodes. It is used only temporarily during CFG construction. \end{definition} -% I agree, we should keep this in mind in the future. -%\begin{workinprogress} -%I find it useful to never name phases ``one'', ``two'', ``three'', but -%always to give them English names. This makes the meaning clearer to -%readers --- often because it forces the writer to think harder about the -%meaning of each. It can still be useful to number the phases even after -%they have more mnemonic names. -%\end{workinprogress} - The process of translating an AST to a CFG proceeds in three distinct phases. \begin{enumerate} @@ -1841,9 +1832,9 @@ \subsection{Overview} left or right-hand side to the true (resp. false) successor. It also applies type qualifiers from method postconditions after calls. -\begin{workinprogress} -Preconditions are not mentioned at all in this manual. How are they handled? -\end{workinprogress} +% \begin{workinprogress} +% Preconditions are not mentioned at all in this manual. How are they handled? +% \end{workinprogress} \subsection{Interaction of the Checker Framework and the Dataflow Analysis} @@ -1942,11 +1933,15 @@ \subsection{The Checker Framework Store and Dealing with Aliasing} Section~\ref{sec:field-access}) to abstract values, and the subsequent sections describe the operations that keep this mapping up-to-date. -\begin{workinprogress} - There hasn't been a good introduction of pure vs. non-pure methods. - Maybe this is a good location for a discussion? - Introduce the purity annotations somewhere. -\end{workinprogress} +A side-effect-free method has no visible side-effects, such +as setting a field of an object that existed before the method was called. +A deterministic method returns the same value (according to ==) every time it is called with the same parameters and in the same environment. +A pure method is both side-effect-free and deterministic. +The Dataflow Framework respects the +\href{https://checkerframework.org/api/org/checkerframework/dataflow/qual/SideEffectFree.html}{\code{@SideEffectFree}}, +\href{https://checkerframework.org/api/org/checkerframework/dataflow/qual/Deterministic.html}{\code{@Deterministic}},and +\href{https://checkerframework.org/api/org/checkerframework/dataflow/qual/Pure.html}{\code{@Pure}} +annotations of the Checker Framework \subsubsection{Internal Representation of field access} From 90e2ed250f0582bea5b5b56fbb800211c8b73e8d Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 11 Nov 2023 07:40:25 -0800 Subject: [PATCH 12/16] Adjust expected errors --- framework/tests/flow/Purity.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/framework/tests/flow/Purity.java b/framework/tests/flow/Purity.java index 7df8425d4c2..e2a2fc39701 100644 --- a/framework/tests/flow/Purity.java +++ b/framework/tests/flow/Purity.java @@ -125,7 +125,7 @@ String t12(String[] s) { @Pure String t13() { - // :: error: (purity.not.deterministic.object.creation) + // No "purity.not.deterministic.object.creation" error; an error was issued at the constructor. PureClass p = new PureClass(); return ""; } @@ -144,7 +144,7 @@ String t13d() { @Deterministic String t13c() { - // :: error: (purity.not.deterministic.object.creation) + // No "purity.not.deterministic.object.creation" error; an error was issued at the constructor. PureClass p = new PureClass(); return ""; } From 2776bdcc7fefcf590f2b2a511aed05afaaade8c6 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 11 Nov 2023 08:11:18 -0800 Subject: [PATCH 13/16] Rename variable --- .../checkerframework/framework/flow/CFAbstractStore.java | 8 ++++---- .../framework/type/AnnotatedTypeFactory.java | 9 ++++----- 2 files changed, 8 insertions(+), 9 deletions(-) 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 6acd2fe8902..ef7bb26e72d 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -112,7 +112,7 @@ public Map getFieldValues() { private final boolean assumeSideEffectFree; /** True if -AassumePureGetters was passed on the command line. */ - private final boolean assumeSideEffectFreeGetters; + private final boolean assumePureGetters; /** The unique ID for the next-created object. */ private static final AtomicLong nextUid = new AtomicLong(0); @@ -147,7 +147,7 @@ protected CFAbstractStore(CFAbstractAnalysis analysis, boolean sequenti assumeSideEffectFree = analysis.checker.hasOption("assumeSideEffectFree") || analysis.checker.hasOption("assumePure"); - assumeSideEffectFreeGetters = analysis.checker.hasOption("assumePureGetters"); + assumePureGetters = analysis.checker.hasOption("assumePureGetters"); } /** @@ -165,7 +165,7 @@ protected CFAbstractStore(CFAbstractStore other) { classValues = new HashMap<>(other.classValues); sequentialSemantics = other.sequentialSemantics; assumeSideEffectFree = other.assumeSideEffectFree; - assumeSideEffectFreeGetters = other.assumeSideEffectFreeGetters; + assumePureGetters = other.assumePureGetters; } /** @@ -237,7 +237,7 @@ public void updateForMethodCall( // case 1: remove information if necessary boolean hasSideEffect = !(assumeSideEffectFree - || (assumeSideEffectFreeGetters && ElementUtils.isGetter(method)) + || (assumePureGetters && ElementUtils.isGetter(method)) || atypeFactory.isSideEffectFree(method)); System.out.printf( "CFAS.updateForMethodCall(%s, %s, %s): hasSideEffect=%s%n", 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 07c1d99f057..3da632a4952 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -383,7 +383,7 @@ public class AnnotatedTypeFactory implements AnnotationProvider { * True if all getter methods should be assumed to be @SideEffectFree, for the purposes of * org.checkerframework.dataflow analysis. */ - private final boolean assumeSideEffectFreeGetters; + private final boolean assumePureGetters; /** True if -AmergeStubsWithSource was provided on the command line. */ private final boolean mergeStubsWithSource; @@ -577,7 +577,7 @@ public AnnotatedTypeFactory(BaseTypeChecker checker) { checker.hasOption("assumeSideEffectFree") || checker.hasOption("assumePure"); this.assumeDeterministic = checker.hasOption("assumeDeterministic") || checker.hasOption("assumePure"); - this.assumeSideEffectFreeGetters = checker.hasOption("assumePureGetters"); + this.assumePureGetters = checker.hasOption("assumePureGetters"); this.trees = Trees.instance(processingEnv); this.elements = processingEnv.getElementUtils(); @@ -5807,8 +5807,7 @@ public boolean isImmutable(TypeMirror type) { @Override public boolean isSideEffectFree(ExecutableElement methodElement) { - if (assumeSideEffectFree - || (assumeSideEffectFreeGetters && ElementUtils.isGetter(methodElement))) { + if (assumeSideEffectFree || (assumePureGetters && ElementUtils.isGetter(methodElement))) { return true; } if (ElementUtils.isRecordAccessor(methodElement) @@ -5827,7 +5826,7 @@ public boolean isSideEffectFree(ExecutableElement methodElement) { @Override public boolean isDeterministic(ExecutableElement methodElement) { - if (assumeDeterministic) { + if (assumeDeterministic || (assumePureGetters && ElementUtils.isGetter(methodElement))) { return true; } if (ElementUtils.isRecordAccessor(methodElement) From 7e0a50c4d4d7611f3e2172c24dea7d2015313d75 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 11 Nov 2023 16:32:01 -0800 Subject: [PATCH 14/16] Tweaks --- .../java/org/checkerframework/dataflow/util/PurityChecker.java | 1 + .../org/checkerframework/framework/source/SourceChecker.java | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) 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 e25cb5ee8de..a73470178d7 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java @@ -307,6 +307,7 @@ public Void visitNewClass(NewClassTree tree, Void ignore) { boolean deterministic = assumeDeterministic || okThrowDeterministic + // No need to check assumePureGetters because a constructor is never a getter. || PurityUtils.isDeterministic(annoProvider, ctorElement); boolean sideEffectFree = assumeSideEffectFree || PurityUtils.isSideEffectFree(annoProvider, ctorElement); diff --git a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java index 180c6d17c68..7977a004daf 100644 --- a/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java @@ -749,7 +749,7 @@ public Trees getTreeUtils() { */ public AnnotationProvider getAnnotationProvider() { throw new UnsupportedOperationException( - "getAnnotationProvider is not implemented for this class."); + "getAnnotationProvider is not implemented for " + this.getClass().getSimpleName() + "."); } /** From 4fdbbdb1c95cdbb477d7cb4b644a85c6ad648a18 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sat, 11 Nov 2023 17:22:49 -0800 Subject: [PATCH 15/16] Add fix in MethodCall; remove diagnostics --- .../checker/nullness/NullnessTransfer.java | 1 - .../optional-pure-getters/PureGetterTest.java | 2 +- .../dataflow/expression/MethodCall.java | 2 +- .../framework/flow/CFAbstractStore.java | 16 ---------------- 4 files changed, 2 insertions(+), 19 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java index 690a93682e9..fba3a6ef48f 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java @@ -388,7 +388,6 @@ public TransferResult visitMethodInvocation( boolean isMethodSideEffectFree = atypeFactory.isSideEffectFree(method) || PurityUtils.isSideEffectFree(atypeFactory, method); - System.out.printf("isMethodSideEffectFree(%s) = %s%n", method, isMethodSideEffectFree); Node receiver = n.getTarget().getReceiver(); if (nonNullAssumptionAfterInvocation || isMethodSideEffectFree diff --git a/checker/tests/optional-pure-getters/PureGetterTest.java b/checker/tests/optional-pure-getters/PureGetterTest.java index f66adb62604..01c770c2e6b 100644 --- a/checker/tests/optional-pure-getters/PureGetterTest.java +++ b/checker/tests/optional-pure-getters/PureGetterTest.java @@ -5,6 +5,7 @@ class PureGetterTest { @SuppressWarnings("optional.field") Optional field; + // This method will be treated as @Pure because of -AassumePureGetters. Optional getOptional() { return null; } @@ -44,7 +45,6 @@ void foo() { } if (getOptional().isPresent()) { getOptional(); - // :: error: method.invocation getOptional().get(); } if (getOptional().isPresent()) { diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/expression/MethodCall.java b/dataflow/src/main/java/org/checkerframework/dataflow/expression/MethodCall.java index 02052310067..b73adebb9df 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/expression/MethodCall.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/expression/MethodCall.java @@ -88,7 +88,7 @@ public boolean containsOfClass(Class clazz) { @Override public boolean isDeterministic(AnnotationProvider provider) { - return PurityUtils.isDeterministic(provider, method) + return (PurityUtils.isDeterministic(provider, method) || provider.isDeterministic(method)) && listIsDeterministic(arguments, provider); } 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 ef7bb26e72d..37574a52dba 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -239,10 +239,6 @@ public void updateForMethodCall( !(assumeSideEffectFree || (assumePureGetters && ElementUtils.isGetter(method)) || atypeFactory.isSideEffectFree(method)); - System.out.printf( - "CFAS.updateForMethodCall(%s, %s, %s): hasSideEffect=%s%n", - methodInvocationNode, atypeFactory.getClass().getSimpleName(), val, hasSideEffect); - System.out.printf(" %s%n", this); if (hasSideEffect) { boolean sideEffectsUnrefineAliases = @@ -319,15 +315,9 @@ public void updateForMethodCall( methodValues.keySet().removeIf(e -> !e.isUnmodifiableByOtherCode()); } - System.out.printf(" %s%n", this); - // store information about method call if possible JavaExpression methodCall = JavaExpression.fromNode(methodInvocationNode); - System.out.printf("about to replaceValue(%s, %s)%n", methodCall, val); replaceValue(methodCall, val); - - System.out.printf(" %s%n", this); - System.out.printf("exited updateForMethodCall%n"); } /** @@ -565,7 +555,6 @@ protected void computeNewValueAndInsert( BinaryOperator merger, boolean permitNondeterministic) { if (!shouldInsert(expr, value, permitNondeterministic)) { - System.out.printf("shouldInsert(%s, %s, %s) => false%n", expr, value, permitNondeterministic); return; } @@ -692,13 +681,8 @@ public void insertThisValue(AnnotationMirror a, TypeMirror underlyingType) { * changes to certain parts of the state. */ public void replaceValue(JavaExpression expr, @Nullable V value) { - System.out.printf("entered replaceValue(%s, %s)%n", expr, value); - System.out.printf(" %s%n", this); clearValue(expr); - System.out.printf(" %s%n", this); insertValue(expr, value); - System.out.printf(" %s%n", this); - System.out.printf("exited replaceValue(%s, %s)%n", expr, value); } /** From a60aad1d345e1c015b59d79dbfe07479518f3bab Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sun, 12 Nov 2023 19:18:58 -0800 Subject: [PATCH 16/16] Refactor --- docs/manual/purity-checker.tex | 4 +-- .../javacutil/ElementUtils.java | 35 ++++++++++++++++--- 2 files changed, 32 insertions(+), 7 deletions(-) diff --git a/docs/manual/purity-checker.tex b/docs/manual/purity-checker.tex index 6b5c8f87838..3bdbec99784 100644 --- a/docs/manual/purity-checker.tex +++ b/docs/manual/purity-checker.tex @@ -112,8 +112,8 @@ The command-line option \<-AassumePureGetters> makes the Checker Framework unsoundly assume that every getter method is side-effect-free and deterministic. For the purposes of \<-AassumePureGetters>, a getter method -is defined as an instance method that starts with ``get[A-Z]'' and has no -formal parameters. +is defined as an instance method with no formal parameters, whose name +starts with ``get'' followed by an uppercase letter. This can make flow-sensitive type refinement much more effective, since method calls will diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java index 7833f99b5b2..5e14b4fdfb1 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java @@ -1101,7 +1101,7 @@ public static boolean isResourceVariable(@Nullable Element elt) { /** * Returns true if the given element is a getter method. A getter method is an instance method - * whose name starts with "get[A-Z]" and has no formal parameters. + * with no formal parameters, whose name starts with "get" followed by an upper-case letter. * * @param methodElt a method * @return true if the given element is a getter method @@ -1110,11 +1110,36 @@ public static boolean isGetter(@Nullable ExecutableElement methodElt) { if (methodElt == null) { return false; } - // Constructors and initializers don't have name starting "get[A-Z]". + if (isStatic(methodElt)) { + return false; + } + if (!methodElt.getParameters().isEmpty()) { + return false; + } + + // I could check that the method has a non-void return type. + + // Constructors and initializers don't have a name starting with a character. String name = methodElt.getSimpleName().toString(); // I expect this code is more efficient than use of a regular expression. - boolean isGetterName = - name.startsWith("get") && name.length() > 3 && Character.isUpperCase(name.charAt(3)); - return isGetterName && !isStatic(methodElt) && methodElt.getParameters().isEmpty(); + boolean nameOk = nameStartsWith(name, "get"); + if (!nameOk) { + return false; + } + + return true; + } + + /** + * Returns true if the name starts with the given prefix, followed by an upper-case letter. + * + * @param name a name + * @param prefix a prefix + * @return true if the name starts with the given prefix, followed by an upper-case letter + */ + private static boolean nameStartsWith(String name, String prefix) { + return name.startsWith(prefix) + && name.length() > prefix.length() + && Character.isUpperCase(name.charAt(prefix.length())); } }