From 69904b92fd8c4d6a065756c13e71360c8dd7f731 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Wed, 28 Sep 2022 13:51:38 -0700 Subject: [PATCH] Infer purity when using the Lock Checker (#5343) --- .../lock/LockAnnotatedTypeFactory.java | 18 ++++--- .../checker/lock/LockStore.java | 24 ++-------- .../checker/lock/LockVisitor.java | 10 ---- .../dataflow/util/PurityUtils.java | 10 ++++ docs/CHANGELOG.md | 8 ++++ .../common/basetype/BaseTypeVisitor.java | 47 ++++++++----------- .../framework/flow/CFAbstractStore.java | 7 +-- .../framework/type/AnnotatedTypeFactory.java | 25 ++++++++++ .../javacutil/AnnotationProvider.java | 13 +++++ .../javacutil/BasicAnnotationProvider.java | 23 ++++++++- 10 files changed, 114 insertions(+), 71 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 5ff5490ba0e..ed885b73437 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java @@ -130,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"); @@ -768,4 +758,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 50cfe5b47b5..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,12 +174,11 @@ 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)) { - // 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 to @LockPossiblyHeld, but the annotation in the - // GuardedBy hierarchy should not be changed. + 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 + // to @LockPossiblyHeld, but the annotation in the GuardedBy hierarchy should not be changed. for (FieldAccess field : new ArrayList<>(fieldValues.keySet())) { CFValue newValue = changeLockAnnoToTop(field, fieldValues.get(field)); if (newValue != null) { 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 53f00ef0255..6612721cf19 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java @@ -86,16 +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"))) { - // The Lock Checker redefines CFAbstractStore#isSideEffectFree in a way that is - // incompatible with (semantically different than) other checkers. - inferPurity = false; - break; - } - } } @Override 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..8f8db6c148e 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,16 @@ 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 + * 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 +98,10 @@ public static boolean isSideEffectFree(AnnotationProvider provider, MethodTree m /** * Is the method {@code methodElement} side-effect-free? * + *

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 * @return whether the method is side-effect-free diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 2995923405e..30c5781c83b 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -18,12 +18,20 @@ performance; please increase max heap size" message from a warning to a note. 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()`. + Use `TreeUtils.elementFromDeclaration` and `TreeUtils.elementFromUse` in 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 8e149484e57..53031fa52dc 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -236,12 +236,6 @@ public class BaseTypeVisitor additionalKinds = r.getKinds().clone(); /* NO-AFU - if (!(infer && inferPurity)) { - // During WPI, propagate all purity kinds, even those that are already - // present (because they were inferred in a previous WPI round). + 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); /* NO-AFU - } + } */ if (TreeUtils.isConstructor(node)) { additionalKinds.remove(Pure.Kind.DETERMINISTIC); } if (!additionalKinds.isEmpty()) { - /* NO-AFU - 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); - } - } - } else { - */ if (additionalKinds.size() == 2) { checker.reportWarning(node, "purity.more.pure", node.getName()); } else if (additionalKinds.contains(Pure.Kind.SIDE_EFFECT_FREE)) { @@ -1048,7 +1025,21 @@ protected void checkPurity(MethodTree node) { } else { throw new BugInCF("Unexpected purity kind in " + additionalKinds); } - // NO-AFU } + /* NO-AFU + if (infer) { + 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); + } + } + */ } } } 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 69458a07e68..52d68b57c44 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 org.checkerframework.javacutil.AnnotationProvider#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 b356d12608a..255c3761d18 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -333,6 +333,12 @@ public class AnnotatedTypeFactory implements AnnotationProvider { private final 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}. * @@ -523,6 +529,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(); @@ -5781,4 +5790,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..0cb676a7c01 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,16 @@ 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. + * + *

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 + */ + 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..928111530d5 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. */ @@ -19,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); @@ -41,4 +41,25 @@ 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(); + + for (AnnotationMirror am : annotationMirrors) { + boolean found = + AnnotationUtils.areSameByName(am, "org.checkerframework.dataflow.qual.SideEffectFree"); + if (found) { + return true; + } + } + + return false; + } }