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 00000000000..ab6a7dd1718 --- /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")} changes the + * value of at most the expressions A and B. All other expressions have the same value before and + * after a call to the method. + * + * @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 might change the value of. + * + * @return the 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/checker/src/test/java/org/checkerframework/checker/test/junit/ainferrunners/OptionalSideEffectsTest.java b/checker/src/test/java/org/checkerframework/checker/test/junit/ainferrunners/OptionalSideEffectsTest.java new file mode 100644 index 00000000000..cfb1768a4f9 --- /dev/null +++ b/checker/src/test/java/org/checkerframework/checker/test/junit/ainferrunners/OptionalSideEffectsTest.java @@ -0,0 +1,22 @@ +package org.checkerframework.checker.test.junit.ainferrunners; + +import java.io.File; +import java.util.List; +import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest; +import org.junit.runners.Parameterized.Parameters; + +public class OptionalSideEffectsTest extends CheckerFrameworkPerDirectoryTest { + + public OptionalSideEffectsTest(List testFiles) { + super( + testFiles, + org.checkerframework.checker.optional.OptionalChecker.class, + "optional", + "-AcheckPurityAnnotations"); + } + + @Parameters + public static String[] getTestDirs() { + return new String[] {"optional-side-effects"}; + } +} diff --git a/checker/tests/optional-side-effects/OptionalSideEffectsLambda.java b/checker/tests/optional-side-effects/OptionalSideEffectsLambda.java new file mode 100644 index 00000000000..79a1f93795a --- /dev/null +++ b/checker/tests/optional-side-effects/OptionalSideEffectsLambda.java @@ -0,0 +1,42 @@ +import java.util.List; +import java.util.Optional; +import org.checkerframework.checker.optional.qual.*; +import org.checkerframework.dataflow.qual.*; + +class OptionalSideEffectsLambda { + + void fooWithEnhancedFor(OptContainer container, List strs) { + if (!container.getOptStr().isPresent()) { + return; + } + for (String s : strs) { + bar(container); // OK + } + } + + void fooWithForEach(OptContainer container, List strs) { + if (!container.getOptStr().isPresent()) { + return; + } + strs.forEach(s -> bar(container)); // OK + } + + @RequiresPresent("#1.getOptStr()") + @SideEffectFree + void bar(OptContainer container) {} + + class OptContainer { + + @SuppressWarnings("optional:field") + private Optional optStr; + + OptContainer(String s) { + this.optStr = Optional.ofNullable(s); + } + + @Pure + public Optional getOptStr() { + return this.optStr; + } + } +} diff --git a/checker/tests/optional-side-effects/OptionalSideEffectsPrecondition.java b/checker/tests/optional-side-effects/OptionalSideEffectsPrecondition.java new file mode 100644 index 00000000000..b83474d15eb --- /dev/null +++ b/checker/tests/optional-side-effects/OptionalSideEffectsPrecondition.java @@ -0,0 +1,72 @@ +import java.util.ArrayList; +import java.util.List; +import java.util.Optional; +import org.checkerframework.checker.optional.qual.RequiresPresent; +import org.checkerframework.dataflow.qual.Pure; +import org.checkerframework.dataflow.qual.SideEffectsOnly; + +class OptionalSideEffectsPrecondition { + + void test1(OptionalContainer optContainer) { + if (!optContainer.getOpt().isPresent()) { + return; + } + List strs = new ArrayList<>(); + methodA(optContainer, strs); + optContainer.getOpt().get(); // OK + bar(optContainer); // OK + } + + void test2(OptionalContainer optContainer) { + if (!optContainer.getOpt().isPresent()) { + return; + } + List strs = new ArrayList<>(); + methodB(optContainer, strs); + + // :: error: (contracts.precondition) + bar(optContainer); + } + + void test3(OptionalContainer optContainer) { + if (!optContainer.getOpt().isPresent()) { + return; + } + List strs = new ArrayList<>(); + havoc(optContainer, strs); + + // :: error: (contracts.precondition) + bar(optContainer); + } + + @RequiresPresent("#1.getOpt()") + void bar(OptionalContainer optContainer) {} + + @SideEffectsOnly("#2") + void methodA(OptionalContainer optContainer, Object param) {} + + @SideEffectsOnly({"#1", "#2"}) + void methodB(OptionalContainer optContainer, Object param) {} + + @SideEffectsOnly({"#1.getOptional()"}) + // :: error: (flowexpr.parse.error) + void methodC(OptionalContainer optContainer, Object param) {} + + void havoc(OptionalContainer optContainer, Object param) {} + + class OptionalContainer { + + @SuppressWarnings("optional:field") + private Optional opt; + + @SuppressWarnings("optional:parameter") + OptionalContainer(Optional opt) { + this.opt = opt; + } + + @Pure // Not required if running under -AassumePureGetters + public Optional getOpt() { + return this.opt; + } + } +} diff --git a/docs/manual/advanced-features.tex b/docs/manual/advanced-features.tex index 7c3e175ab47..db44a09a11e 100644 --- a/docs/manual/advanced-features.tex +++ b/docs/manual/advanced-features.tex @@ -1023,7 +1023,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. @@ -1063,7 +1064,7 @@ } \end{Verbatim} -There are three ways to express that \ does not set +There are four ways to express that \ does not set \ to \, and thus to prevent the Nullness Checker from issuing a warning about the call \. @@ -1077,6 +1078,15 @@ int computeValue() { ... } \end{Verbatim} +\item + If \ has side effects, but they do not affect \, + declare the method as \refqualclass{dataflow/qual}{SideEffectsOnly}: + +\begin{Verbatim} + @SideEffectsOnly({"someOtherVariable1", "someOtherVariable1"}) + int computeValue() { ... } +\end{Verbatim} + \noindent The Nullness Checker issues no warnings, because it can reason that the second occurrence of \code{myField} has the same (non-null) value as @@ -1130,6 +1140,18 @@ \end{itemize} +\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(\{\})> (i.e., a \<@SideEffectsOnly> annotation +with an empty list of expressions) is equivalent to \<@SideEffectFree>. +Programmers should favor writing \<@SideEffectFree> in this case for clarity. +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/docs/manual/called-methods-checker.tex b/docs/manual/called-methods-checker.tex index 15050b50f9f..108a80b4de8 100644 --- a/docs/manual/called-methods-checker.tex +++ b/docs/manual/called-methods-checker.tex @@ -218,7 +218,9 @@ \end{Verbatim} If \ might have side-effects (i.e., it is not annotated as - \refqualclass{dataflow/qual}{SideEffectFree} or \refqualclass{dataflow/qual}{Pure}), + \refqualclass{dataflow/qual}{SideEffectFree}, + \refqualclass{dataflow/qual}{SideEffectsOnly}, or + \refqualclass{dataflow/qual}{Pure}), then the Called Methods Checker issues an error because it cannot make any assumptions about the call to \, and therefore assumes the worst: that all information it knows about in-scope variables (including @@ -226,7 +228,9 @@ There are two possible fixes: \begin{itemize} - \item add a \<@SideEffectFree> or \<@Pure> annotation to \, if \ is + \item add a \refqualclass{dataflow/qual}{SideEffectFree}, + \refqualclass{dataflow/qual}{SideEffectsOnly}, or + \refqualclass{dataflow/qual}{Pure} annotation to \, if \ is in fact side-effect free or pure; or \item re-order the calls to \ and \ so that the call to \ appears last in \. diff --git a/docs/manual/introduction.tex b/docs/manual/introduction.tex index e4bd9281e4c..a3bdae3d636 100644 --- a/docs/manual/introduction.tex +++ b/docs/manual/introduction.tex @@ -613,6 +613,7 @@ \item \<-AcheckPurityAnnotations> Check the bodies of methods marked \refqualclass{dataflow/qual}{SideEffectFree}, + \refqualclass{dataflow/qual}{SideEffectsOnly}, \refqualclass{dataflow/qual}{Deterministic}, and \refqualclass{dataflow/qual}{Pure} to ensure the method satisfies the annotation. By default, @@ -1559,6 +1560,10 @@ If your proof includes ``method \ has no side effects'', then annotate \'s declaration with \refqualclass{dataflow/qual}{SideEffectFree}. +\item + If your proof includes ``method \ has limited side effects'', + then annotate \'s declaration with + \refqualclass{dataflow/qual}{SideEffectsOnly}. \item If your proof includes ``each call to method \ returns the same value'', then annotate \'s declaration with diff --git a/docs/manual/nullness-checker.tex b/docs/manual/nullness-checker.tex index 8d75f922df0..a605f03bbb9 100644 --- a/docs/manual/nullness-checker.tex +++ b/docs/manual/nullness-checker.tex @@ -239,7 +239,8 @@ arbitrary external method calls that have access to the given field. By contrast, for a \<@Nullable> field, the Nullness Checker assumes that most method calls might set it to \. (Exceptions are calls to - methods that are \refqualclass{dataflow/qual}{SideEffectFree} or that + methods that are \refqualclass{dataflow/qual}{SideEffectFree} or + \refqualclass{dataflow/qual}{SideEffectsOnly}, or that have an \refqualclass{checker/nullness/qual}{EnsuresNonNull} or \refqualclass{checker/nullness/qual}{EnsuresNonNullIf} annotation.) \end{sloppypar} diff --git a/docs/manual/purity-checker.tex b/docs/manual/purity-checker.tex index 1fe3adb4ce3..c684df88d77 100644 --- a/docs/manual/purity-checker.tex +++ b/docs/manual/purity-checker.tex @@ -27,6 +27,9 @@ \item[\refqualclass{dataflow/qual}{SideEffectFree}] indicates that the method has no externally-visible side effects. +\item[\refqualclass{dataflow/qual}{SideEffectsOnly}] + indicates that the method has limited externally-visible side effects. + \item[\refqualclass{dataflow/qual}{Deterministic}] indicates that if the method is called multiple times with identical arguments, then it returns the identical result according to \<==> @@ -42,7 +45,8 @@ By default, purity annotations are trusted. Purity annotations on called methods affect type-checking of client code. However, you can make a -mistake by writing \<@SideEffectFree> on the declaration of a method that +mistake by writing \<@SideEffectFree> or \<@SideEffectsOnly> on the +declaration of a method that is not actually side-effect-free or by writing \<@Deterministic> on the declaration of a method that is not actually deterministic. diff --git a/docs/manual/troubleshooting.tex b/docs/manual/troubleshooting.tex index a1c7add01e7..0894d005a76 100644 --- a/docs/manual/troubleshooting.tex +++ b/docs/manual/troubleshooting.tex @@ -367,6 +367,7 @@ \ does not set the field \ to \, you can use \<\refqualclass{dataflow/qual}{Pure}>, \<\refqualclass{dataflow/qual}{SideEffectFree}>, +\<\refqualclass{dataflow/qual}{SideEffectsOnly}>, or \<\refqualclass{checker/nullness/qual}{EnsuresNonNull}> on the declaration of \; see Sections~\ref{type-refinement-purity} and~\ref{nullness-method-annotations}. 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 d835609da53..c94014d1b5d 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -91,6 +91,7 @@ import org.checkerframework.dataflow.qual.Impure; 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; @@ -128,6 +129,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; @@ -240,6 +242,9 @@ public class BaseTypeVisitorIf the method {@code tree} 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 tree the method tree to check */ + @SuppressWarnings("AlreadyChecked") // TEMPORARY, must fix protected void checkPurityAnnotations(MethodTree tree) { if (!checkPurityAnnotations) { return; } - if (!suggestPureMethods && !PurityUtils.hasPurityAnnotation(atypeFactory, tree)) { - // There is nothing to check. - return; - } + // if (!suggestPureMethods && !PurityUtils.hasPurityAnnotation(atypeFactory, tree) && + // !checkPurityAnnotations) { + // // There is nothing to check. + // return; + // } if (isExplicitlySideEffectFreeAndDeterministic(tree)) { checker.reportWarning(tree, "purity.effectively.pure", tree.getName()); @@ -1109,7 +1122,6 @@ protected void checkPurityAnnotations(MethodTree tree) { boolean bodyAssigned = false; if (suggestPureMethods || PurityUtils.hasPurityAnnotation(atypeFactory, tree)) { - // check "no" purity EnumSet kinds = PurityUtils.getPurityKinds(atypeFactory, tree); // @Deterministic makes no sense for a void method or constructor @@ -1176,6 +1188,83 @@ protected void checkPurityAnnotations(MethodTree tree) { } } + if (checkPurityAnnotations) { + if (bodyAssigned == false) { + body = atypeFactory.getPath(tree.getBody()); + bodyAssigned = true; + } + if (body == null) { + return; + } + @Nullable Element methodDeclElem = TreeUtils.elementFromDeclaration(tree); + AnnotationMirror sefOnlyAnnotation = + atypeFactory.getDeclAnnotation(methodDeclElem, SideEffectsOnly.class); + if (sefOnlyAnnotation == null) { + return; + } + AnnotationMirror pureOrSideEffectFreeAnnotation = + getPureOrSideEffectFreeAnnotation(methodDeclElem); + if (pureOrSideEffectFreeAnnotation != null) { + // It is an error if a @SideEffectsOnly annotation appears with a @Pure or @SideEffectFree + // annotation + checker.reportError( + tree, + "purity.incorrect.annotation.conflict", + tree.getName(), + pureOrSideEffectFreeAnnotation); + return; + } + List sideEffectsOnlyExpressionStrings = + AnnotationUtils.getElementValueArray( + sefOnlyAnnotation, sideEffectsOnlyValueElement, String.class); + List sideEffectsOnlyExpressions = + new ArrayList<>(sideEffectsOnlyExpressionStrings.size()); + for (String st : sideEffectsOnlyExpressionStrings) { + try { + JavaExpression exprJe = StringToJavaExpression.atMethodBody(st, tree, checker); + sideEffectsOnlyExpressions.add(exprJe); + } catch (JavaExpressionParseUtil.JavaExpressionParseException ex) { + DiagMessage diagMessage = ex.getDiagMessage(); + if (diagMessage.getMessageKey().equals("flowexpr.parse.error")) { + checker.reportError(methodTree, "flowexpr.parse.error", st); + } else { + checker.report(st, ex.getDiagMessage()); + } + return; + } + } + + if (sideEffectsOnlyExpressions.isEmpty()) { + // A @SideEffectsOnly annotation with an empty expression array is equivalent to + // a @SideEffectFree annotation. + checker.reportWarning(tree, "purity.more.sideeffectfree", tree.getName()); + return; + } + + SideEffectsOnlyChecker.ExtraSideEffects sefOnlyResult = + SideEffectsOnlyChecker.checkSideEffectsOnly( + body, + atypeFactory, + sideEffectsOnlyExpressions, + atypeFactory.getProcessingEnv(), + checker); + + // System.out.printf("sefOnlyResult = %s%n", sefOnlyResult); + + List> seOnlyIncorrectExprs = sefOnlyResult.getExprs(); + // System.out.printf("seOnlyIncorrectExprs = %s%n", seOnlyIncorrectExprs); + + if (!seOnlyIncorrectExprs.isEmpty()) { + for (IPair s : seOnlyIncorrectExprs) { + if (!sideEffectsOnlyExpressions.contains(s.second)) { + // System.out.printf("Error 2%n"); + checker.reportError( + s.first, "purity.incorrect.sideeffectsonly", tree.getName(), s.second.toString()); + } + } + } + } + // There will be code here that *may* use `body` (and may set `body` before using it). // The below is just a placeholder so `bodyAssigned` is not a dead variable. // ... @@ -1186,6 +1275,22 @@ protected void checkPurityAnnotations(MethodTree tree) { // ... } + /** + * Return either the {@link Pure} or {@link SideEffectFree} annotation (in that order) if either + * appears on a method declaration. + * + * @param methodDeclaration the method declaration + * @return either the {@link Pure} or {@link SideEffectFree} annotation (in that order) if either + * appears on a method declaration + */ + private @Nullable AnnotationMirror getPureOrSideEffectFreeAnnotation(Element methodDeclaration) { + AnnotationMirror pureAnnotation = atypeFactory.getDeclAnnotation(methodDeclaration, Pure.class); + if (pureAnnotation != null) { + return pureAnnotation; + } + return atypeFactory.getDeclAnnotation(methodDeclaration, SideEffectFree.class); + } + /** * Returns true if the given method is explicitly annotated with both @{@link SideEffectFree} * and @{@link Deterministic}. diff --git a/framework/src/main/java/org/checkerframework/common/basetype/SideEffectsOnlyChecker.java b/framework/src/main/java/org/checkerframework/common/basetype/SideEffectsOnlyChecker.java new file mode 100644 index 00000000000..cf1d53d5f5d --- /dev/null +++ b/framework/src/main/java/org/checkerframework/common/basetype/SideEffectsOnlyChecker.java @@ -0,0 +1,285 @@ +package org.checkerframework.common.basetype; + +import com.sun.source.tree.AssignmentTree; +import com.sun.source.tree.CompoundAssignmentTree; +import com.sun.source.tree.ExpressionTree; +import com.sun.source.tree.MethodInvocationTree; +import com.sun.source.tree.MethodTree; +import com.sun.source.tree.NewClassTree; +import com.sun.source.tree.Tree; +import com.sun.source.tree.UnaryTree; +import com.sun.source.tree.VariableTree; +import com.sun.source.util.TreePath; +import com.sun.source.util.TreePathScanner; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.stream.Collectors; +import javax.annotation.processing.ProcessingEnvironment; +import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.Element; +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.javacutil.AnnotationProvider; +import org.checkerframework.javacutil.TreePathUtil; +import org.checkerframework.javacutil.TreeUtils; +import org.plumelib.util.IPair; + +/** + * For methods annotated with {@link SideEffectsOnly}, computes expressions that are side-effected + * but not permitted by the annotation. + */ +public class SideEffectsOnlyChecker { + + /** Do not instantiate. */ + private SideEffectsOnlyChecker() { + throw new Error("Do not instantiate"); + } + + /** + * Returns the computed {@code ExtraSideEffects}. + * + * @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 a ExtraSideEffects + */ + public static ExtraSideEffects 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.extraSideEffects; + } + + /** + * The set of expressions a method side-effects, beyond those specified its {@link + * SideEffectsOnly} annotation. + */ + public static class ExtraSideEffects { + + /** Creates an empty ExtraSideEffects. */ + public ExtraSideEffects() {} + + /** + * List of expressions a method side-effects that are not specified in the list of arguments to + * {@link SideEffectsOnly}. + */ + protected final List> exprs = new ArrayList<>(1); + + /** + * Adds {@code t} and {@code javaExpr} as a pair to this. + * + * @param t the expression that is mutated + * @param javaExpr the corresponding Java expression + */ + public void addExpr(Tree t, JavaExpression javaExpr) { + exprs.add(IPair.of(t, javaExpr)); + } + + /** + * Returns a list of expressions a method side-effects that are not specified in the list of + * arguments to {@link SideEffectsOnly}. + * + * @return side-effected expressions, beyond what is in {@code @SideEffectsOnly}. + */ + public List> getExprs() { + return exprs; + } + } + + /** + * Class 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. */ + ExtraSideEffects extraSideEffects = new ExtraSideEffects(); + + /** + * List of expressions specified as annotation arguments in {@link SideEffectsOnly} annotation. + */ + List sideEffectsOnlyExpressionsFromAnnotation; + + /** Map of expressions that are aliased to other expressions. */ + Map aliasedExpressions; + + /** 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.aliasedExpressions = new HashMap<>(); + this.annoProvider = annoProvider; + this.sideEffectsOnlyExpressionsFromAnnotation = sideEffectsOnlyExpressions; + this.processingEnv = processingEnv; + this.checker = checker; + } + + @Override + public Void visitMethodInvocation(MethodInvocationTree node, Void aVoid) { + Element invokedElem = TreeUtils.elementFromUse(node); + boolean isMarkedPure = annoProvider.getDeclAnnotation(invokedElem, Pure.class) != null; + boolean isMarkedSideEffectFree = + annoProvider.getDeclAnnotation(invokedElem, SideEffectFree.class) != null; + if (isMarkedPure || isMarkedSideEffectFree) { + return super.visitMethodInvocation(node, aVoid); + } + + AnnotationMirror sideEffectsOnlyAnnotationOnEnclosingMethod = + getSideEffectsOnlyAnnotationOnEnclosingMethod(node); + assert sideEffectsOnlyAnnotationOnEnclosingMethod != null + : "This method should only be invoked when the @SideEffectsOnly annotation is not null"; + + boolean isInvokedMethodMarkedWithSideEffectsOnly = + annoProvider.getDeclAnnotation(invokedElem, SideEffectsOnly.class) != null; + + List actualSideEffectedExprs = + this.getJavaExpressionsFromMethodInvocation(node); + + // If the invoked method is NOT marked with @SideEffectsOnly, it may modify anything + if (!isInvokedMethodMarkedWithSideEffectsOnly) { + // What does it modify? Check the arguments for the method invocation + if (actualSideEffectedExprs.isEmpty()) { + // If the args are empty, it might be modifying anything + checker.reportError( + node, + "purity.incorrect.sideeffectsonly", + invokedElem.getSimpleName(), + sideEffectsOnlyExpressionsFromAnnotation); + } + } + actualSideEffectedExprs.stream() + .filter(this::isAdditionalSideEffectedExpression) + .forEach(expr -> extraSideEffects.addExpr(node, expr)); + return super.visitMethodInvocation(node, aVoid); + } + + /** + * Returns the {@link SideEffectsOnly} annotation (if it exists, else null) on the enclosing + * method of a given method invocation. + * + * @param tree the method invocation + * @return the {@link SideEffectsOnly} annotation on the enclosing method of a given method + * invocation + */ + private AnnotationMirror getSideEffectsOnlyAnnotationOnEnclosingMethod( + MethodInvocationTree tree) { + MethodTree enclosingMethod = + TreePathUtil.enclosingMethod(checker.getTypeFactory().getPath(tree)); + if (enclosingMethod == null) { + return null; + } + return annoProvider.getDeclAnnotation( + TreeUtils.elementFromDeclaration(enclosingMethod), SideEffectsOnly.class); + } + + /** + * Returns the arguments to a method invocation, including the receiver. + * + * @param methodInvok a method invocation + * @return the arguments to a method invocation, including the receiver + */ + private List getJavaExpressionsFromMethodInvocation( + MethodInvocationTree methodInvok) { + // TODO: collect all subexpressions of the given expression. For now it just considers the + // actual arguments, which is incomplete. + List args = methodInvok.getArguments(); + ExpressionTree receiver = TreeUtils.getReceiverTree(methodInvok); + List exprs; + if (receiver == null) { + exprs = new ArrayList<>(args); + } else { + exprs = new ArrayList<>(args.size() + 1); + exprs.add(receiver); + exprs.addAll(args); + } + return exprs.stream().map(JavaExpression::fromTree).collect(Collectors.toList()); + } + + /** + * Returns true if the given expression is a side-effected expression beyond what is described + * in the {@link SideEffectsOnly} annotation. + * + *

The following criteria must be met in determining whether a given expression is + * side-effected beyond the expressions provided in the annotation: + * + *

    + *
  • The expression does not appear in the expressions passed as arguments to the + * {@link SideEffectsOnly} annotation + *
  • The expression is modifiable by other code + *
  • The expression is not aliased by other variables in the method body + *
+ * + * @param expr the expression to check for side-effecting + * @return true if the given expression is a side-effected expressio beyond what is described in + * the {@link SideEffectsOnly} annotation + */ + private boolean isAdditionalSideEffectedExpression(JavaExpression expr) { + return !sideEffectsOnlyExpressionsFromAnnotation.contains(expr) + && expr.isModifiableByOtherCode() + && !aliasedExpressions.containsKey(expr); + } + + @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 (!sideEffectsOnlyExpressionsFromAnnotation.contains(javaExpr)) { + extraSideEffects.addExpr(node, javaExpr); + } + return super.visitAssignment(node, aVoid); + } + + @Override + public Void visitVariable(VariableTree node, Void aVoid) { + JavaExpression name = JavaExpression.fromVariableTree(node); + JavaExpression expr = JavaExpression.fromTree(node.getInitializer()); + aliasedExpressions.put(name, expr); + return super.visitVariable(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 4c592045e9b..6dfa0ce0917 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/messages.properties +++ b/framework/src/main/java/org/checkerframework/common/basetype/messages.properties @@ -80,6 +80,8 @@ 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 %s may side-effect %s +purity.incorrect.annotation.conflict=the method %s cannot be annotated with both @SideEffectsOnly and %s purity.effectively.pure=a method declared both @SideEffectFree and @Deterministic can instead be declared @Pure flowexpr.parse.index.too.big=the method does not have a parameter %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 607faae3787..ea253206db2 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java @@ -35,13 +35,18 @@ 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.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.ElementUtils; +import org.checkerframework.javacutil.TreeUtils; import org.plumelib.util.CollectionsPlume; import org.plumelib.util.IPair; import org.plumelib.util.ToStringComparator; @@ -77,6 +82,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. @@ -147,6 +155,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); assumeSideEffectFree = analysis.checker.hasOption("assumeSideEffectFree") || analysis.checker.hasOption("assumePure"); @@ -167,6 +177,7 @@ protected CFAbstractStore(CFAbstractStore other) { arrayValues = new HashMap<>(other.arrayValues); classValues = new HashMap<>(other.classValues); sequentialSemantics = other.sequentialSemantics; + sideEffectsOnlyValueElement = other.sideEffectsOnlyValueElement; assumeSideEffectFree = other.assumeSideEffectFree; assumePureGetters = other.assumePureGetters; } @@ -243,6 +254,31 @@ public void updateForMethodCall( GenericAnnotatedTypeFactory gatypeFactory = (GenericAnnotatedTypeFactory) atypeFactory; + // 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: The method is side-effect-free. boolean hasSideEffect = !(assumeSideEffectFree @@ -250,40 +286,62 @@ public void updateForMethodCall( || atypeFactory.isSideEffectFree(method)); if (hasSideEffect) { - boolean sideEffectsUnrefineAliases = gatypeFactory.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().isModifiableByOtherCode()); - } - - // update this value - if (sideEffectsUnrefineAliases) { - thisValue = null; - } - - // update field values - if (sideEffectsUnrefineAliases) { - fieldValues.entrySet().removeIf(e -> e.getKey().isModifiableByOtherCode()); - } else { - // Case 2 (unassignable fields) and case 3 (monotonic fields) - updateFieldValuesForMethodCall(gatypeFactory); - } + updateFieldValuesForMethodCall(gatypeFactory, sideEffectsOnlyExpressions); - // update array values + // Update array values arrayValues.clear(); - // update method values - methodCallExpressions.keySet().removeIf(MethodCall::isModifiableByOtherCode); + // Update information about method calls + updateMethodCallValues(sideEffectsOnlyExpressions); } - // store information about method call if possible + // store information about method calls if possible JavaExpression methodCall = JavaExpression.fromNode(methodInvocationNode); replaceValue(methodCall, val); } + /** + * Update information about method calls given the list of side-effected expressions. + * + * @param sideEffectsOnlyExpressions the list of side-effected expressions + */ + private void updateMethodCallValues(List sideEffectsOnlyExpressions) { + if (sideEffectsOnlyExpressions.isEmpty()) { + methodCallExpressions + .keySet() + .removeIf(methodCallValue -> methodCallValue.isModifiableByOtherCode()); + } else { + methodCallExpressions + .keySet() + .removeIf( + methodCallValue -> + hasMethodCallInformationChanged(methodCallValue, sideEffectsOnlyExpressions)); + } + } + + /** + * Returns true if information about a method call might have changed. + * + *

Information about a method call might have changed if: + * + *

    + *
  • It is modifiable by other code + *
  • It contains expressions that appear in the list of expressions that are provided to a + * {@code @SideEffectsOnly} annotation + *
+ * + * @param methodCallValue the method call value + * @param sideEffectsOnlyExpressions the list of expressions provided to a + * {@code @SideEffectsOnly} annotation + * @return true if information about a method call might have changed + */ + private boolean hasMethodCallInformationChanged( + JavaExpression methodCallValue, List sideEffectsOnlyExpressions) { + return methodCallValue.isModifiableByOtherCode() + && sideEffectsOnlyExpressions.stream() + .anyMatch(methodCallValue::containsSyntacticEqualJavaExpression); + } + /** * Returns the new value of a field after a method call, or {@code null} if the field should be * removed from the store. @@ -366,19 +424,31 @@ protected V newMonotonicFieldValueAfterMethodCall( *

More specifically, remove all information about fields except for unassignable fields and * fields that have a monotonic annotation. * + *

A non-empty {@code sideEffectsOnlyExpressions} is indicative that the invoked method has + * side effects. In this case, remove information for fields that actually appear in the list of + * side-effected expressions. + * * @param atypeFactory AnnotatedTypeFactory of the associated checker + * @param sideEffectsOnlyExpressions the expressions that are side-effected by a method call */ private void updateFieldValuesForMethodCall( - GenericAnnotatedTypeFactory atypeFactory) { + GenericAnnotatedTypeFactory atypeFactory, + List sideEffectsOnlyExpressions) { Map newFieldValues = new HashMap<>(CollectionsPlume.mapCapacity(fieldValues)); for (Map.Entry e : fieldValues.entrySet()) { FieldAccess fieldAccess = e.getKey(); - V value = e.getValue(); + V previousValue = e.getValue(); - V newValue = newFieldValueAfterMethodCall(fieldAccess, atypeFactory, value); - if (newValue != null) { - // Keep information for all hierarchies where we had a monotonic annotation. - newFieldValues.put(fieldAccess, newValue); + if (!sideEffectsOnlyExpressions.isEmpty() + && !sideEffectsOnlyExpressions.contains(fieldAccess)) { + // If the field hasn't been side-effected, there is no need to compute a new value for it + newFieldValues.put(fieldAccess, previousValue); + } else { + V newValue = newFieldValueAfterMethodCall(fieldAccess, atypeFactory, previousValue); + if (newValue != null) { + // Keep information for all hierarchies where we had a monotonic annotation. + newFieldValues.put(fieldAccess, newValue); + } } } fieldValues = newFieldValues; @@ -1091,14 +1161,14 @@ protected void removeConflicting(LocalVariable var) { } } - Iterator> methodCallValuesIterator = + Iterator> methodCallExpressionsIterator = methodCallExpressions.entrySet().iterator(); - while (methodCallValuesIterator.hasNext()) { - Map.Entry entry = methodCallValuesIterator.next(); + while (methodCallExpressionsIterator.hasNext()) { + Map.Entry entry = methodCallExpressionsIterator.next(); MethodCall otherMethodAccess = entry.getKey(); // case 3: if (otherMethodAccess.containsSyntacticEqualJavaExpression(var)) { - methodCallValuesIterator.remove(); + methodCallExpressionsIterator.remove(); } } } diff --git a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java index d9cb6cf1827..1e663095411 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -255,7 +255,7 @@ public abstract class GenericAnnotatedTypeFactory< * effect to the value could change them; set this field to true. */ // Not final so that subclasses can set it. - public boolean sideEffectsUnrefineAliases = false; + public boolean sideEffectsUnrefineAliases = false; // TODO: maybe remove it /** * True if this checker either has one or more subcheckers, or if this checker is a subchecker. 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 00000000000..8e0e9c37fb2 --- /dev/null +++ b/framework/src/test/java/org/checkerframework/framework/test/junit/SideEffectsOnlyTest.java @@ -0,0 +1,25 @@ +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", + "-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 00000000000..969277d8708 --- /dev/null +++ b/framework/src/test/java/org/checkerframework/framework/testchecker/sideeffectsonly/SideEffectsOnlyToyChecker.java @@ -0,0 +1,9 @@ +package org.checkerframework.framework.testchecker.sideeffectsonly; + +import org.checkerframework.common.basetype.BaseTypeChecker; + +/** + * 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 {} 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 00000000000..fb5e2dabd78 --- /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 00000000000..d24fde75e72 --- /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/purity-suggestions/PuritySuggestionsClass.java b/framework/tests/purity-suggestions/PuritySuggestionsClass.java index fff0f8b6208..937043eeb0b 100644 --- a/framework/tests/purity-suggestions/PuritySuggestionsClass.java +++ b/framework/tests/purity-suggestions/PuritySuggestionsClass.java @@ -1,6 +1,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; // various tests for the checker to automatically suggest pure methods (most methods have been // copied from Purity.java) @@ -173,6 +174,14 @@ String t12() { return ""; } + // Class with a method annotated with @SideEffectsOnly({}) + private static class EmptySideEffectsOnly { + + @SideEffectsOnly({}) + // :: warning: (purity.more.sideeffectfree) + void foo() {} + } + @SideEffectFree @Deterministic // :: warning: (purity.effectively.pure) diff --git a/framework/tests/sideeffectsonly/CheckSideEffectsOnly.java b/framework/tests/sideeffectsonly/CheckSideEffectsOnly.java new file mode 100644 index 00000000000..2afe05c4b65 --- /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 00000000000..4d537c9104c --- /dev/null +++ b/framework/tests/sideeffectsonly/EmptySideEffectsOnly.java @@ -0,0 +1,26 @@ +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({}) + // :: warning: (purity.more.sideeffectfree) + void method1(@SideEffectsOnlyToyBottom Object x) {} + + @SideEffectsOnly({}) + // :: warning: (purity.more.sideeffectfree) + void method2(@SideEffectsOnlyToyBottom Object x) {} +} diff --git a/framework/tests/sideeffectsonly/IncorrectSideEffectsOnly.java b/framework/tests/sideeffectsonly/IncorrectSideEffectsOnly.java new file mode 100644 index 00000000000..4f4237b5372 --- /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/NestedSideEffectsNoAliasing.java b/framework/tests/sideeffectsonly/NestedSideEffectsNoAliasing.java new file mode 100644 index 00000000000..3e4c10a3e24 --- /dev/null +++ b/framework/tests/sideeffectsonly/NestedSideEffectsNoAliasing.java @@ -0,0 +1,22 @@ +import java.util.ArrayList; +import java.util.List; +import org.checkerframework.dataflow.qual.SideEffectsOnly; + +public class NestedSideEffectsNoAliasing { + + @SideEffectsOnly("#1.inner.nestedList") + void test1(OuterWrapper first) { + first.inner.nestedList.add(1); // OK + // :: error: (purity.incorrect.sideeffectsonly) + first.arrB.add(2); + } + + class OuterWrapper { + InnerWrapper inner = new InnerWrapper(); + List arrB = new ArrayList<>(); + } + + class InnerWrapper { + List nestedList = new ArrayList<>(); + } +} diff --git a/framework/tests/sideeffectsonly/NestedSideEffectsWithAliasing.java b/framework/tests/sideeffectsonly/NestedSideEffectsWithAliasing.java new file mode 100644 index 00000000000..106afc221cf --- /dev/null +++ b/framework/tests/sideeffectsonly/NestedSideEffectsWithAliasing.java @@ -0,0 +1,22 @@ +import java.util.ArrayList; +import java.util.List; +import org.checkerframework.dataflow.qual.SideEffectsOnly; + +public class NestedSideEffectsWithAliasing { + + @SideEffectsOnly({"#1.inner.nestedList", "#1.inner"}) + void test1(OuterWrapper first) { + List aliasOfNestedList = first.inner.nestedList; + List aliasOfAlias = aliasOfNestedList; + aliasOfAlias.add(1); // Should be OK + } + + class OuterWrapper { + InnerWrapper inner = new InnerWrapper(); + List arrB = new ArrayList<>(); + } + + class InnerWrapper { + List nestedList = new ArrayList<>(); + } +} diff --git a/framework/tests/sideeffectsonly/SideEffectsMultiple.java b/framework/tests/sideeffectsonly/SideEffectsMultiple.java new file mode 100644 index 00000000000..22e4c21ac9e --- /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/SideEffectsOnlyConflictingAnnotations.java b/framework/tests/sideeffectsonly/SideEffectsOnlyConflictingAnnotations.java new file mode 100644 index 00000000000..8384d2b8fbc --- /dev/null +++ b/framework/tests/sideeffectsonly/SideEffectsOnlyConflictingAnnotations.java @@ -0,0 +1,22 @@ +import java.util.Collection; +import org.checkerframework.dataflow.qual.Pure; +import org.checkerframework.dataflow.qual.SideEffectFree; +import org.checkerframework.dataflow.qual.SideEffectsOnly; + +public class SideEffectsOnlyConflictingAnnotations { + + @SideEffectsOnly("#1") + @SideEffectFree + // :: error: (purity.incorrect.annotation.conflict) + void test1(Collection first) { + // :: error: (purity.not.sideeffectfree.call) + first.add(1); + } + + @SideEffectsOnly("#2") + @Pure + // :: error: (purity.incorrect.annotation.conflict) + int test2(Collection first, Collection second) { + return 1; + } +} diff --git a/framework/tests/sideeffectsonly/SideEffectsOnlyEmpty.java b/framework/tests/sideeffectsonly/SideEffectsOnlyEmpty.java new file mode 100644 index 00000000000..cfbcf661920 --- /dev/null +++ b/framework/tests/sideeffectsonly/SideEffectsOnlyEmpty.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 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({}) + // :: warning: (purity.more.sideeffectfree) + 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 00000000000..cefaac75184 --- /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 00000000000..64e6c3f45a2 --- /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 00000000000..fc9742eaaf3 --- /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 00000000000..79e5ff808d9 --- /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) {} +} diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java index bf246a66b64..3f413ed3a3c 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java @@ -1041,10 +1041,10 @@ public static boolean isCompileTimeString(ExpressionTree tree) { // Trying to handle receiver calls to trees of the form // ((m).getArray()) // returns the type of 'm' in this case - receiver = ((MethodInvocationTree) expression).getMethodSelect(); + ExpressionTree methodSelect = ((MethodInvocationTree) expression).getMethodSelect(); - if (receiver.getKind() == Tree.Kind.MEMBER_SELECT) { - receiver = ((MemberSelectTree) receiver).getExpression(); + if (methodSelect.getKind() == Tree.Kind.MEMBER_SELECT) { + receiver = ((MemberSelectTree) methodSelect).getExpression(); } else { // It's a method call "m(foo)" without an explicit receiver return null;