diff --git a/checker-qual/src/main/java/org/checkerframework/dataflow/qual/SideEffectsOnly.java b/checker-qual/src/main/java/org/checkerframework/dataflow/qual/SideEffectsOnly.java new file mode 100644 index 000000000000..3b6b3b507083 --- /dev/null +++ b/checker-qual/src/main/java/org/checkerframework/dataflow/qual/SideEffectsOnly.java @@ -0,0 +1,29 @@ +package org.checkerframework.dataflow.qual; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; +import org.checkerframework.framework.qual.JavaExpression; + +/** + * A method annotated with the declaration annotation {@code @SideEffectsOnly(A, B)} performs + * side-effects on at most the expressions A and B. All other expressions have the same value before + * and after a call. + * + * @checker_framework.manual #type-refinement-purity Specifying side effects + */ +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) +public @interface SideEffectsOnly { + /** + * An upper bound on the expressions that this method side effects. + * + * @return Java expressions that the annotated method might side-effect + * @checker_framework.manual #java-expressions-as-arguments Syntax of Java expressions + */ + @JavaExpression + public String[] value(); +} diff --git a/docs/manual/advanced-features.tex b/docs/manual/advanced-features.tex index 27256193483b..570a85f06ed7 100644 --- a/docs/manual/advanced-features.tex +++ b/docs/manual/advanced-features.tex @@ -1015,7 +1015,8 @@ the refined type, because the method might assign a field. The \refqualclass{dataflow/qual}{SideEffectFree} annotation indicates that the method has no side effects, so calling it does not invalidate any -dataflow facts. +dataflow facts. Alternately, the \refqualclass{dataflow/qual}{SideEffectsOnly} +annotation specifies all the expressions that the method might side-effect. Calling a method twice might have different results, so facts known about one call cannot be relied upon at another call. @@ -1105,6 +1106,16 @@ \end{enumerate} +\subsubsectionAndLabel{Relationship between \<@SideEffectFree> and \<@SideEffectsOnly>}{side-effects-relationship} + +A method cannot be annotated with both \refqualclass{dataflow/qual}{SideEffectFree} +and \refqualclass{dataflow/qual}{SideEffectsOnly}. +The annotation \<@SideEffectsOnly(\{\})> is equivalent to \<@SideEffectFree>. +If a method has no \refqualclass{dataflow/qual}{SideEffectsOnly} +or \refqualclass{dataflow/qual}{SideEffectFree} annotation, then the Checker Framework +assumes that the method may side-effect any expressions (including fields and arguments). + + \subsubsectionAndLabel{Deterministic methods}{type-refinement-determinism} Consider the following declaration and uses: 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 7f13507430bb..07bfb20bc4c0 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -92,6 +92,7 @@ import org.checkerframework.dataflow.qual.Deterministic; import org.checkerframework.dataflow.qual.Pure; import org.checkerframework.dataflow.qual.SideEffectFree; +import org.checkerframework.dataflow.qual.SideEffectsOnly; import org.checkerframework.dataflow.util.PurityChecker; import org.checkerframework.dataflow.util.PurityChecker.PurityResult; import org.checkerframework.dataflow.util.PurityUtils; @@ -129,6 +130,7 @@ import org.checkerframework.framework.util.Contract.Precondition; import org.checkerframework.framework.util.ContractsFromMethod; import org.checkerframework.framework.util.FieldInvariants; +import org.checkerframework.framework.util.JavaExpressionParseUtil; import org.checkerframework.framework.util.JavaExpressionParseUtil.JavaExpressionParseException; import org.checkerframework.framework.util.JavaParserUtil; import org.checkerframework.framework.util.StringToJavaExpression; @@ -218,6 +220,9 @@ public class BaseTypeVisitorIf the method {@code node} is annotated with {@link SideEffectsOnly}, check that the method + * side-effects a subset of the expressions specified as annotation arguments/elements to {@link + * SideEffectsOnly}. + * * @param node the method tree to check */ protected void checkPurity(MethodTree node) { @@ -966,70 +980,121 @@ protected void checkPurity(MethodTree node) { return; } - if (!suggestPureMethods && !PurityUtils.hasPurityAnnotation(atypeFactory, node)) { - // There is nothing to check. - return; - } + TreePath body = atypeFactory.getPath(node.getBody()); - // check "no" purity - 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) { - if (TreeUtils.isConstructor(node)) { - checker.reportWarning(node, "purity.deterministic.constructor"); - } else if (TreeUtils.typeOf(node.getReturnType()).getKind() == TypeKind.VOID) { - checker.reportWarning(node, "purity.deterministic.void.method"); + // if (!suggestPureMethods && !PurityUtils.hasPurityAnnotation(atypeFactory, node) && + // !checkSideEffectsOnly) { + // // There is nothing to check. + // return; + // } + + if (suggestPureMethods || PurityUtils.hasPurityAnnotation(atypeFactory, node)) { + // check "no" purity + 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) { + if (TreeUtils.isConstructor(node)) { + checker.reportWarning(node, "purity.deterministic.constructor"); + } else if (TreeUtils.typeOf(node.getReturnType()).getKind() == TypeKind.VOID) { + checker.reportWarning(node, "purity.deterministic.void.method"); + } } - } - TreePath body = atypeFactory.getPath(node.getBody()); - PurityResult r; - if (body == null) { - r = new PurityResult(); - } else { - r = - PurityChecker.checkPurity( - body, - atypeFactory, - checker.hasOption("assumeSideEffectFree") || checker.hasOption("assumePure"), - checker.hasOption("assumeDeterministic") || checker.hasOption("assumePure")); - } - if (!r.isPure(kinds)) { - reportPurityErrors(r, node, kinds); - } - - if (suggestPureMethods && !TreeUtils.isSynthetic(node)) { - // Issue a warning if the method is pure, but not annotated as such. - EnumSet additionalKinds = r.getKinds().clone(); - additionalKinds.removeAll(kinds); - if (TreeUtils.isConstructor(node)) { - additionalKinds.remove(Pure.Kind.DETERMINISTIC); + PurityResult r; + if (body == null) { + r = new PurityResult(); + } else { + r = + PurityChecker.checkPurity( + body, + atypeFactory, + checker.hasOption("assumeSideEffectFree") || checker.hasOption("assumePure"), + checker.hasOption("assumeDeterministic") || checker.hasOption("assumePure")); } - if (!additionalKinds.isEmpty()) { - if (infer) { - if (inferPurity) { - WholeProgramInference wpi = atypeFactory.getWholeProgramInference(); - ExecutableElement methodElt = TreeUtils.elementFromDeclaration(node); + if (!r.isPure(kinds)) { + reportPurityErrors(r, node, kinds); + } + + if (suggestPureMethods && !TreeUtils.isSynthetic(node)) { + // Issue a warning if the method is pure, but not annotated as such. + EnumSet additionalKinds = r.getKinds().clone(); + additionalKinds.removeAll(kinds); + if (TreeUtils.isConstructor(node)) { + additionalKinds.remove(Pure.Kind.DETERMINISTIC); + } + 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); + } + } + } else { if (additionalKinds.size() == 2) { - wpi.addMethodDeclarationAnnotation(methodElt, PURE); + checker.reportWarning(node, "purity.more.pure", node.getName()); } else if (additionalKinds.contains(Pure.Kind.SIDE_EFFECT_FREE)) { - wpi.addMethodDeclarationAnnotation(methodElt, SIDE_EFFECT_FREE); + checker.reportWarning(node, "purity.more.sideeffectfree", node.getName()); } else if (additionalKinds.contains(Pure.Kind.DETERMINISTIC)) { - wpi.addMethodDeclarationAnnotation(methodElt, DETERMINISTIC); + checker.reportWarning(node, "purity.more.deterministic", node.getName()); } 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)) { - checker.reportWarning(node, "purity.more.sideeffectfree", node.getName()); - } else if (additionalKinds.contains(Pure.Kind.DETERMINISTIC)) { - checker.reportWarning(node, "purity.more.deterministic", node.getName()); - } else { - throw new BugInCF("Unexpected purity kind in " + additionalKinds); + } + } + } + + if (checkSideEffectsOnly) { + if (body == null) { + return; + } else { + @Nullable Element methodDeclElem = TreeUtils.elementFromTree(node); + AnnotationMirror sefOnlyAnnotation = + atypeFactory.getDeclAnnotation(methodDeclElem, SideEffectsOnly.class); + if (sefOnlyAnnotation == null) { + return; + } + List sideEffectsOnlyExpressionStrings = + AnnotationUtils.getElementValueArray( + sefOnlyAnnotation, sideEffectsOnlyValueElement, String.class); + List sideEffectsOnlyExpressions = new ArrayList<>(); + for (String st : sideEffectsOnlyExpressionStrings) { + try { + JavaExpression exprJe = StringToJavaExpression.atMethodBody(st, node, checker); + sideEffectsOnlyExpressions.add(exprJe); + } catch (JavaExpressionParseUtil.JavaExpressionParseException ex) { + checker.report(st, ex.getDiagMessage()); + return; + } + } + + if (sideEffectsOnlyExpressions.isEmpty()) { + return; + } + + SideEffectsOnlyAnnoChecker.SideEffectsOnlyResult sefOnlyResult = + SideEffectsOnlyAnnoChecker.checkSideEffectsOnly( + body, + atypeFactory, + sideEffectsOnlyExpressions, + atypeFactory.getProcessingEnv(), + checker); + + List> seOnlyIncorrectExprs = sefOnlyResult.getSeOnlyResult(); + if (!seOnlyIncorrectExprs.isEmpty()) { + for (Pair s : seOnlyIncorrectExprs) { + if (!sideEffectsOnlyExpressions.contains(s.second)) { + checker.reportError(s.first, "purity.incorrect.sideeffectsonly", s.second.toString()); + } } } } diff --git a/framework/src/main/java/org/checkerframework/common/basetype/SideEffectsOnlyAnnoChecker.java b/framework/src/main/java/org/checkerframework/common/basetype/SideEffectsOnlyAnnoChecker.java new file mode 100644 index 000000000000..d7c2e098292d --- /dev/null +++ b/framework/src/main/java/org/checkerframework/common/basetype/SideEffectsOnlyAnnoChecker.java @@ -0,0 +1,201 @@ +package org.checkerframework.common.basetype; + +import com.sun.source.tree.AssignmentTree; +import com.sun.source.tree.CatchTree; +import com.sun.source.tree.CompoundAssignmentTree; +import com.sun.source.tree.MethodInvocationTree; +import com.sun.source.tree.NewClassTree; +import com.sun.source.tree.Tree; +import com.sun.source.tree.UnaryTree; +import com.sun.source.util.TreePath; +import com.sun.source.util.TreePathScanner; +import java.util.ArrayList; +import java.util.List; +import javax.annotation.processing.ProcessingEnvironment; +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +import javax.lang.model.element.ExecutableElement; +import org.checkerframework.dataflow.expression.JavaExpression; +import org.checkerframework.dataflow.qual.Pure; +import org.checkerframework.dataflow.qual.SideEffectFree; +import org.checkerframework.dataflow.qual.SideEffectsOnly; +import org.checkerframework.framework.util.JavaExpressionParseUtil; +import org.checkerframework.framework.util.StringToJavaExpression; +import org.checkerframework.javacutil.AnnotationProvider; +import org.checkerframework.javacutil.AnnotationUtils; +import org.checkerframework.javacutil.Pair; +import org.checkerframework.javacutil.TreeUtils; + +/** + * For methods annotated with {@link SideEffectsOnly}, computes expressions that are side-effected + * but not permitted by the annotation. + */ +public class SideEffectsOnlyAnnoChecker { + /** + * Returns the computed {@code SideEffectsOnlyResult}. + * + * @param statement The statement to check + * @param annoProvider The annotation provider + * @param sideEffectsOnlyExpressions List of JavaExpressions that are provided as annotation + * values to {@link SideEffectsOnly} + * @param processingEnv The processing environment + * @param checker The checker to use + * @return SideEffectsOnlyResult returns the result of {@link SideEffectsOnlyAnnoChecker} + */ + public static SideEffectsOnlyResult checkSideEffectsOnly( + TreePath statement, + AnnotationProvider annoProvider, + List sideEffectsOnlyExpressions, + ProcessingEnvironment processingEnv, + BaseTypeChecker checker) { + SideEffectsOnlyCheckerHelper helper = + new SideEffectsOnlyCheckerHelper( + annoProvider, sideEffectsOnlyExpressions, processingEnv, checker); + helper.scan(statement, null); + return helper.sideEffectsOnlyResult; + } + + /** + * Result of the {@link SideEffectsOnlyAnnoChecker}. Can be queried to get the list of mutated + * expressions. + */ + public static class SideEffectsOnlyResult { + /** + * List of expressions a method side-effects that are not specified in the list of arguments to + * {@link SideEffectsOnly}. + */ + protected final List> mutatedExprs = new ArrayList<>(1); + + /** + * Adds {@code t} and {@code javaExpr} as a Pair to mutatedExprs. + * + * @param t The expression that is mutated + * @param javaExpr The corresponding Java expression that is mutated + */ + public void addMutatedExpr(Tree t, JavaExpression javaExpr) { + mutatedExprs.add(Pair.of(t, javaExpr)); + } + + /** + * Returns {@code mutatedExprs}. + * + * @return mutatedExprs + */ + public List> getSeOnlyResult() { + return mutatedExprs; + } + } + + /** + * Class that visits that visits various nodes and computes mutated expressions that are not + * specified as annotation values to {@link SideEffectsOnly}. + */ + protected static class SideEffectsOnlyCheckerHelper extends TreePathScanner { + /** Result computed by SideEffectsOnlyCheckerHelper. */ + SideEffectsOnlyResult sideEffectsOnlyResult = new SideEffectsOnlyResult(); + /** + * List of expressions specified as annotation arguments in {@link SideEffectsOnly} annotation. + */ + List sideEffectsOnlyExpressions; + + /** The annotation provider. */ + protected final AnnotationProvider annoProvider; + /** The processing environment. */ + ProcessingEnvironment processingEnv; + /** The checker to use. */ + BaseTypeChecker checker; + + /** + * Constructor for SideEffectsOnlyCheckerHelper. + * + * @param annoProvider The annotation provider + * @param sideEffectsOnlyExpressions List of JavaExpressions that are provided as annotation + * values to {@link SideEffectsOnly} + * @param processingEnv The processing environment + * @param checker The checker to use + */ + public SideEffectsOnlyCheckerHelper( + AnnotationProvider annoProvider, + List sideEffectsOnlyExpressions, + ProcessingEnvironment processingEnv, + BaseTypeChecker checker) { + this.annoProvider = annoProvider; + this.sideEffectsOnlyExpressions = sideEffectsOnlyExpressions; + this.processingEnv = processingEnv; + this.checker = checker; + } + + @Override + public Void visitCatch(CatchTree node, Void aVoid) { + return super.visitCatch(node, aVoid); + } + + @Override + public Void visitMethodInvocation(MethodInvocationTree node, Void aVoid) { + Element treeElem = TreeUtils.elementFromTree(node); + AnnotationMirror pureAnno = annoProvider.getDeclAnnotation(treeElem, Pure.class); + AnnotationMirror sideEffectFreeAnno = + annoProvider.getDeclAnnotation(treeElem, SideEffectFree.class); + // If the invoked method is annotated as @Pure or @SideEffectFree, nothing to do. + if (pureAnno != null || sideEffectFreeAnno != null) { + return super.visitMethodInvocation(node, aVoid); + } + + AnnotationMirror sideEffectsOnlyAnno = + annoProvider.getDeclAnnotation(treeElem, SideEffectsOnly.class); + // The invoked method is not annotated with @SideEffectsOnly; Report an error. + if (sideEffectsOnlyAnno == null) { + checker.reportError(node, "purity.incorrect.sideeffectsonly", node); + } else { + // The invoked method is annotated with @SideEffectsOnly. + // Add annotation values to seOnlyIncorrectExprs + // that are not present in sideEffectsOnlyExpressions. + ExecutableElement sideEffectsOnlyValueElement = + TreeUtils.getMethod(SideEffectsOnly.class, "value", 0, processingEnv); + List sideEffectsOnlyExpressionStrings = + AnnotationUtils.getElementValueArray( + sideEffectsOnlyAnno, sideEffectsOnlyValueElement, String.class); + List sideEffectsOnlyExprInv = new ArrayList<>(); + for (String st : sideEffectsOnlyExpressionStrings) { + try { + JavaExpression exprJe = StringToJavaExpression.atMethodInvocation(st, node, checker); + sideEffectsOnlyExprInv.add(exprJe); + } catch (JavaExpressionParseUtil.JavaExpressionParseException ex) { + checker.report(st, ex.getDiagMessage()); + } + } + + for (JavaExpression expr : sideEffectsOnlyExprInv) { + if (!sideEffectsOnlyExpressions.contains(expr)) { + sideEffectsOnlyResult.addMutatedExpr(node, expr); + } + } + } + return super.visitMethodInvocation(node, aVoid); + } + + @Override + public Void visitNewClass(NewClassTree node, Void aVoid) { + return super.visitNewClass(node, aVoid); + } + + @Override + public Void visitAssignment(AssignmentTree node, Void aVoid) { + JavaExpression javaExpr = JavaExpression.fromTree(node.getVariable()); + if (!sideEffectsOnlyExpressions.contains(javaExpr)) { + sideEffectsOnlyResult.addMutatedExpr(node, javaExpr); + } + return super.visitAssignment(node, aVoid); + } + + @Override + public Void visitUnary(UnaryTree node, Void aVoid) { + return super.visitUnary(node, aVoid); + } + + @Override + public Void visitCompoundAssignment(CompoundAssignmentTree node, Void aVoid) { + return super.visitCompoundAssignment(node, aVoid); + } + } +} diff --git a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties index 8c726b6acd8d..b5277ab64afb 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties +++ b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties @@ -75,6 +75,7 @@ purity.not.sideeffectfree.call=call to side-effecting %s not allowed in side-eff purity.more.deterministic=the method %s could be declared as @Deterministic purity.more.pure=the method %s could be declared as @Pure purity.more.sideeffectfree=the method %s could be declared as @SideEffectFree +purity.incorrect.sideeffectsonly=the method side-effects %s flowexpr.parse.index.too.big=the method does not have a parameter %s flowexpr.parse.error=cannot parse the expression %s 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 6e619dc90ff5..21b13c62ef0a 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -1,5 +1,6 @@ package org.checkerframework.framework.flow; +import java.util.ArrayList; import java.util.HashMap; import java.util.Iterator; import java.util.List; @@ -33,14 +34,19 @@ import org.checkerframework.dataflow.expression.MethodCall; import org.checkerframework.dataflow.expression.ThisReference; import org.checkerframework.dataflow.qual.SideEffectFree; +import org.checkerframework.dataflow.qual.SideEffectsOnly; import org.checkerframework.dataflow.util.PurityUtils; import org.checkerframework.framework.qual.MonotonicQualifier; +import org.checkerframework.framework.source.SourceChecker; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; +import org.checkerframework.framework.util.JavaExpressionParseUtil; +import org.checkerframework.framework.util.StringToJavaExpression; import org.checkerframework.javacutil.AnnotationBuilder; import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.BugInCF; import org.checkerframework.javacutil.Pair; +import org.checkerframework.javacutil.TreeUtils; import org.plumelib.util.CollectionsPlume; import org.plumelib.util.ToStringComparator; import org.plumelib.util.UniqueId; @@ -75,6 +81,9 @@ public abstract class CFAbstractStore, S extends CF /** Information collected about fields, using the internal representation {@link FieldAccess}. */ protected Map fieldValues; + /** The SideEffectsOnly.value argument/element. */ + public ExecutableElement sideEffectsOnlyValueElement; + /** * Returns information about fields. Clients should not side-effect the returned value, which is * aliased to internal state. @@ -137,6 +146,8 @@ protected CFAbstractStore(CFAbstractAnalysis analysis, boolean sequenti arrayValues = new HashMap<>(); classValues = new HashMap<>(); this.sequentialSemantics = sequentialSemantics; + sideEffectsOnlyValueElement = + TreeUtils.getMethod(SideEffectsOnly.class, "value", 0, analysis.env); } /** Copy constructor. */ @@ -149,6 +160,7 @@ protected CFAbstractStore(CFAbstractStore other) { arrayValues = new HashMap<>(other.arrayValues); classValues = new HashMap<>(other.classValues); sequentialSemantics = other.sequentialSemantics; + sideEffectsOnlyValueElement = other.sideEffectsOnlyValueElement; } /** @@ -206,10 +218,39 @@ protected boolean isSideEffectFree(AnnotatedTypeFactory atypeFactory, Executable * * * Furthermore, if the method is deterministic, we store its result {@code val} in the store. + * + * @param methodInvocationNode method whose information is being updated + * @param atypeFactory AnnotatedTypeFactory of the associated checker + * @param val abstract value of the method call */ public void updateForMethodCall( - MethodInvocationNode n, AnnotatedTypeFactory atypeFactory, V val) { - ExecutableElement method = n.getTarget().getMethod(); + MethodInvocationNode methodInvocationNode, AnnotatedTypeFactory atypeFactory, V val) { + ExecutableElement method = methodInvocationNode.getTarget().getMethod(); + + // List of expressions that this method side-effects (specified as arguments/elements of + // @SideEffectsOnly). If the list is empty, then either there is no @SideEffectsOnly annotation + // or the @SideEffectsOnly is written without any annotation argument. + List sideEffectsOnlyExpressions = new ArrayList<>(); + AnnotationMirror sefOnlyAnnotation = + atypeFactory.getDeclAnnotation(method, SideEffectsOnly.class); + if (sefOnlyAnnotation != null) { + SourceChecker checker = analysis.checker; + + List sideEffectsOnlyExpressionStrings = + AnnotationUtils.getElementValueArray( + sefOnlyAnnotation, sideEffectsOnlyValueElement, String.class); + + for (String st : sideEffectsOnlyExpressionStrings) { + try { + JavaExpression exprJe = + StringToJavaExpression.atMethodInvocation(st, methodInvocationNode, checker); + sideEffectsOnlyExpressions.add(exprJe); + } catch (JavaExpressionParseUtil.JavaExpressionParseException ex) { + checker.report(st, ex.getDiagMessage()); + return; + } + } + } // case 1: remove information if necessary if (!(analysis.checker.hasOption("assumeSideEffectFree") @@ -219,21 +260,23 @@ public void updateForMethodCall( boolean sideEffectsUnrefineAliases = ((GenericAnnotatedTypeFactory) atypeFactory).sideEffectsUnrefineAliases; - // update local variables // TODO: Also remove if any element/argument to the annotation is not // isUnmodifiableByOtherCode. Example: @KeyFor("valueThatCanBeMutated"). if (sideEffectsUnrefineAliases) { - localVariableValues.entrySet().removeIf(e -> !e.getKey().isUnmodifiableByOtherCode()); - } - - // update this value - if (sideEffectsUnrefineAliases) { - thisValue = null; - } - - // update field values - if (sideEffectsUnrefineAliases) { - fieldValues.entrySet().removeIf(e -> !e.getKey().isUnmodifiableByOtherCode()); + if (!sideEffectsOnlyExpressions.isEmpty()) { + for (JavaExpression e : sideEffectsOnlyExpressions) { + if (!e.isUnmodifiableByOtherCode()) { + // update local variables + localVariableValues.keySet().remove(e); + // update field values + fieldValues.keySet().remove(e); + } + } + } else { + localVariableValues.keySet().removeIf(e -> !e.isUnmodifiableByOtherCode()); + thisValue = null; + fieldValues.keySet().removeIf(e -> !e.isUnmodifiableByOtherCode()); + } } else { Map newFieldValues = new HashMap<>(CollectionsPlume.mapCapacity(fieldValues)); @@ -291,7 +334,7 @@ public void updateForMethodCall( } // store information about method call if possible - JavaExpression methodCall = JavaExpression.fromNode(n); + JavaExpression methodCall = JavaExpression.fromNode(methodInvocationNode); replaceValue(methodCall, val); } diff --git a/framework/src/test/java/org/checkerframework/framework/test/junit/SideEffectsOnlyTest.java b/framework/src/test/java/org/checkerframework/framework/test/junit/SideEffectsOnlyTest.java new file mode 100644 index 000000000000..fdd97ba8b923 --- /dev/null +++ b/framework/src/test/java/org/checkerframework/framework/test/junit/SideEffectsOnlyTest.java @@ -0,0 +1,24 @@ +package org.checkerframework.framework.test.junit; + +import java.io.File; +import java.util.List; +import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest; +import org.junit.runners.Parameterized.Parameters; + +public class SideEffectsOnlyTest extends CheckerFrameworkPerDirectoryTest { + + /** @param testFiles the files containing test code, which will be type-checked */ + public SideEffectsOnlyTest(List testFiles) { + super( + testFiles, + org.checkerframework.framework.testchecker.sideeffectsonly.SideEffectsOnlyToyChecker.class, + "sideeffectsonly", + "-Anomsgtext", + "-AcheckPurityAnnotations"); + } + + @Parameters + public static String[] getTestDirs() { + return new String[] {"sideeffectsonly"}; + } +} diff --git a/framework/src/test/java/org/checkerframework/framework/testchecker/sideeffectsonly/SideEffectsOnlyToyChecker.java b/framework/src/test/java/org/checkerframework/framework/testchecker/sideeffectsonly/SideEffectsOnlyToyChecker.java new file mode 100644 index 000000000000..7d77d057f6f3 --- /dev/null +++ b/framework/src/test/java/org/checkerframework/framework/testchecker/sideeffectsonly/SideEffectsOnlyToyChecker.java @@ -0,0 +1,23 @@ +package org.checkerframework.framework.testchecker.sideeffectsonly; + +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; + +/** + * Toy checker used to test whether dataflow analysis correctly type-refines methods annotated with + * {@link org.checkerframework.dataflow.qual.SideEffectsOnly}. + */ +public class SideEffectsOnlyToyChecker extends BaseTypeChecker { + /** + * Sets {@code sideEffectsUnrefineAliases} to true as {@code @SideEffectsOnly} annotation has + * effect only on methods that unrefine types. + * + * @return GenericAnnotatedTypeFactory + */ + @Override + public GenericAnnotatedTypeFactory getTypeFactory() { + GenericAnnotatedTypeFactory result = super.getTypeFactory(); + result.sideEffectsUnrefineAliases = true; + return result; + } +} diff --git a/framework/src/test/java/org/checkerframework/framework/testchecker/sideeffectsonly/qual/SideEffectsOnlyToyBottom.java b/framework/src/test/java/org/checkerframework/framework/testchecker/sideeffectsonly/qual/SideEffectsOnlyToyBottom.java new file mode 100644 index 000000000000..fb5e2dabd786 --- /dev/null +++ b/framework/src/test/java/org/checkerframework/framework/testchecker/sideeffectsonly/qual/SideEffectsOnlyToyBottom.java @@ -0,0 +1,19 @@ +package org.checkerframework.framework.testchecker.sideeffectsonly.qual; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; +import org.checkerframework.framework.qual.SubtypeOf; + +/** + * Bottom qualifier of a toy type system. The toy type system is used to test whether dataflow + * analysis correctly type-refines methods annotated with {@link + * org.checkerframework.dataflow.qual.SideEffectsOnly}. + */ +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) +@SubtypeOf({SideEffectsOnlyToyTop.class}) +public @interface SideEffectsOnlyToyBottom {} diff --git a/framework/src/test/java/org/checkerframework/framework/testchecker/sideeffectsonly/qual/SideEffectsOnlyToyTop.java b/framework/src/test/java/org/checkerframework/framework/testchecker/sideeffectsonly/qual/SideEffectsOnlyToyTop.java new file mode 100644 index 000000000000..d24fde75e72f --- /dev/null +++ b/framework/src/test/java/org/checkerframework/framework/testchecker/sideeffectsonly/qual/SideEffectsOnlyToyTop.java @@ -0,0 +1,21 @@ +package org.checkerframework.framework.testchecker.sideeffectsonly.qual; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; +import org.checkerframework.framework.qual.DefaultQualifierInHierarchy; +import org.checkerframework.framework.qual.SubtypeOf; + +/** + * Top qualifier of a toy type system. The toy type system is used to test whether dataflow analysis + * correctly type-refines methods annotated with {@link + * org.checkerframework.dataflow.qual.SideEffectsOnly}. + */ +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) +@DefaultQualifierInHierarchy +@SubtypeOf({}) +public @interface SideEffectsOnlyToyTop {} diff --git a/framework/tests/sideeffectsonly/CheckSideEffectsOnly.java b/framework/tests/sideeffectsonly/CheckSideEffectsOnly.java new file mode 100644 index 000000000000..2afe05c4b65a --- /dev/null +++ b/framework/tests/sideeffectsonly/CheckSideEffectsOnly.java @@ -0,0 +1,19 @@ +package sideeffectsonly; + +import java.util.Collection; +import org.checkerframework.dataflow.qual.SideEffectsOnly; + +public class CheckSideEffectsOnly { + + @SideEffectsOnly({"#2"}) + void test(Collection cl, Collection cl2) { + // :: error: purity.incorrect.sideeffectsonly + cl.add(9); + cl2.add(10); + } + + @SideEffectsOnly({"#2"}) + static void test1(Collection cl, Collection cl2) { + cl2.add(10); + } +} diff --git a/framework/tests/sideeffectsonly/EmptySideEffectsOnly.java b/framework/tests/sideeffectsonly/EmptySideEffectsOnly.java new file mode 100644 index 000000000000..3eddf6ac1e9a --- /dev/null +++ b/framework/tests/sideeffectsonly/EmptySideEffectsOnly.java @@ -0,0 +1,24 @@ +package sideeffectsonly; + +import org.checkerframework.dataflow.qual.SideEffectsOnly; +import org.checkerframework.framework.qual.EnsuresQualifier; +import org.checkerframework.framework.testchecker.sideeffectsonly.qual.SideEffectsOnlyToyBottom; + +public class EmptySideEffectsOnly { + void test(Object x) { + method(x); + method1(x); + // :: error: argument + method2(x); + } + + @EnsuresQualifier(expression = "#1", qualifier = SideEffectsOnlyToyBottom.class) + // :: error: contracts.postcondition + void method(Object x) {} + + @SideEffectsOnly({}) + void method1(@SideEffectsOnlyToyBottom Object x) {} + + @SideEffectsOnly({}) + void method2(@SideEffectsOnlyToyBottom Object x) {} +} diff --git a/framework/tests/sideeffectsonly/IncorrectSideEffectsOnly.java b/framework/tests/sideeffectsonly/IncorrectSideEffectsOnly.java new file mode 100644 index 000000000000..4f4237b53724 --- /dev/null +++ b/framework/tests/sideeffectsonly/IncorrectSideEffectsOnly.java @@ -0,0 +1,20 @@ +package sideeffectsonly; + +import java.util.Collection; +import org.checkerframework.dataflow.qual.SideEffectsOnly; + +public class IncorrectSideEffectsOnly { + Collection coll; + + @SideEffectsOnly({"#2"}) + void test(Collection cl, Collection cl2) { + // :: error: purity.incorrect.sideeffectsonly + cl.add(9); + } + + @SideEffectsOnly({"#2"}) + void test1(Collection cl, Collection cl2) { + // :: error: purity.incorrect.sideeffectsonly + coll = cl; + } +} diff --git a/framework/tests/sideeffectsonly/SideEffectsMultiple.java b/framework/tests/sideeffectsonly/SideEffectsMultiple.java new file mode 100644 index 000000000000..22e4c21ac9ef --- /dev/null +++ b/framework/tests/sideeffectsonly/SideEffectsMultiple.java @@ -0,0 +1,23 @@ +package sideeffectsonly; + +import org.checkerframework.dataflow.qual.SideEffectsOnly; +import org.checkerframework.framework.qual.EnsuresQualifier; +import org.checkerframework.framework.testchecker.sideeffectsonly.qual.SideEffectsOnlyToyBottom; + +public class SideEffectsMultiple { + void test(Object x) { + method(x); + method1(x); + // :: error: argument + method2(x); + } + + @EnsuresQualifier(expression = "#1", qualifier = SideEffectsOnlyToyBottom.class) + // :: error: contracts.postcondition + void method(Object x) {} + + @SideEffectsOnly({"this", "#1"}) + void method1(@SideEffectsOnlyToyBottom Object y) {} + + void method2(@SideEffectsOnlyToyBottom Object x) {} +} diff --git a/framework/tests/sideeffectsonly/SideEffectsOnlyEmpty.java b/framework/tests/sideeffectsonly/SideEffectsOnlyEmpty.java new file mode 100644 index 000000000000..ffcb9430d89c --- /dev/null +++ b/framework/tests/sideeffectsonly/SideEffectsOnlyEmpty.java @@ -0,0 +1,23 @@ +package sideeffectsonly; + +import org.checkerframework.dataflow.qual.SideEffectsOnly; +import org.checkerframework.framework.qual.EnsuresQualifier; +import org.checkerframework.framework.testchecker.sideeffectsonly.qual.SideEffectsOnlyToyBottom; + +public class SideEffectsOnlyEmpty { + void test(Object x) { + method(x); + method1(x); + // :: error: argument + method2(x); + } + + @EnsuresQualifier(expression = "#1", qualifier = SideEffectsOnlyToyBottom.class) + // :: error: contracts.postcondition + void method(Object x) {} + + @SideEffectsOnly({}) + void method1(@SideEffectsOnlyToyBottom Object x) {} + + void method2(@SideEffectsOnlyToyBottom Object x) {} +} diff --git a/framework/tests/sideeffectsonly/SideEffectsOnlyField.java b/framework/tests/sideeffectsonly/SideEffectsOnlyField.java new file mode 100644 index 000000000000..cefaac751848 --- /dev/null +++ b/framework/tests/sideeffectsonly/SideEffectsOnlyField.java @@ -0,0 +1,31 @@ +package sideeffectsonly; + +import org.checkerframework.dataflow.qual.SideEffectFree; +import org.checkerframework.dataflow.qual.SideEffectsOnly; +import org.checkerframework.framework.qual.EnsuresQualifier; +import org.checkerframework.framework.testchecker.sideeffectsonly.qual.SideEffectsOnlyToyBottom; + +public class SideEffectsOnlyField { + Object a; + Object b; + + static void test(SideEffectsOnlyField arg) { + method(arg); + method3(arg); + // :: error: argument + method2(arg.a); + method2(arg.b); + } + + @EnsuresQualifier( + expression = {"#1.a", "#1.b"}, + qualifier = SideEffectsOnlyToyBottom.class) + // :: error: contracts.postcondition + static void method(SideEffectsOnlyField x) {} + + @SideEffectsOnly("#1.a") + static void method3(SideEffectsOnlyField z) {} + + @SideEffectFree + static void method2(@SideEffectsOnlyToyBottom Object x) {} +} diff --git a/framework/tests/sideeffectsonly/SideEffectsOnlyTest.java b/framework/tests/sideeffectsonly/SideEffectsOnlyTest.java new file mode 100644 index 000000000000..64e6c3f45a2c --- /dev/null +++ b/framework/tests/sideeffectsonly/SideEffectsOnlyTest.java @@ -0,0 +1,29 @@ +package sideeffectsonly; + +import org.checkerframework.dataflow.qual.SideEffectsOnly; +import org.checkerframework.framework.qual.EnsuresQualifier; +import org.checkerframework.framework.testchecker.sideeffectsonly.qual.SideEffectsOnlyToyBottom; + +public class SideEffectsOnlyTest { + void test(Object x) { + method(x); + method1(x); + method3(x); + method2(x); + // :: error: argument + method3(x); + } + + @EnsuresQualifier(expression = "#1", qualifier = SideEffectsOnlyToyBottom.class) + // :: error: contracts.postcondition + void method(Object x) {} + + @SideEffectsOnly({"this"}) + void method1(@SideEffectsOnlyToyBottom Object x) {} + + @SideEffectsOnly({"#1"}) + void method2(@SideEffectsOnlyToyBottom Object x) {} + + @SideEffectsOnly({"this"}) + void method3(@SideEffectsOnlyToyBottom Object z) {} +} diff --git a/framework/tests/sideeffectsonly/SideEffectsTest.java b/framework/tests/sideeffectsonly/SideEffectsTest.java new file mode 100644 index 000000000000..fc9742eaaf35 --- /dev/null +++ b/framework/tests/sideeffectsonly/SideEffectsTest.java @@ -0,0 +1,21 @@ +package sideeffectsonly; + +import org.checkerframework.framework.qual.EnsuresQualifier; +import org.checkerframework.framework.testchecker.sideeffectsonly.qual.SideEffectsOnlyToyBottom; + +public class SideEffectsTest { + void test(Object x) { + method(x); + method1(x); + // :: error: argument + method2(x); + } + + @EnsuresQualifier(expression = "#1", qualifier = SideEffectsOnlyToyBottom.class) + // :: error: contracts.postcondition + void method(Object x) {} + + void method1(@SideEffectsOnlyToyBottom Object x) {} + + void method2(@SideEffectsOnlyToyBottom Object x) {} +} diff --git a/framework/tests/sideeffectsonly/TestMethodInvocation.java b/framework/tests/sideeffectsonly/TestMethodInvocation.java new file mode 100644 index 000000000000..79e5ff808d9e --- /dev/null +++ b/framework/tests/sideeffectsonly/TestMethodInvocation.java @@ -0,0 +1,17 @@ +package sideeffectsonly; + +import org.checkerframework.dataflow.qual.SideEffectsOnly; + +public class TestMethodInvocation { + @SideEffectsOnly("#1") + void method1(Object o) { + // :: error: purity.incorrect.sideeffectsonly + method2(); + method3(o); + } + + void method2() {} + + @SideEffectsOnly("#1") + void method3(Object o) {} +}