Implements SideEffectsOnly checking.

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();
+}

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:

docs/manual/introduction.tex

@@ -609,6 +609,11 @@
   to ensure the method satisfies the annotation.  By default,
   the Checker Framework unsoundly trusts the method annotation.  See
   Section~\ref{type-refinement-purity}.
+\item \<-AcheckSideEffectsOnlyAnnotation>
+  Check the bodies of methods marked
+  \refqualclass{dataflow/qual}{SideEffectsOnly} to ensure the method
+  side-effects at most the annotation's arguments/elements. See
+  Section~\ref{type-refinement-purity}.
 \item \<-AinvariantArrays>
   Make array subtyping invariant; that is, two arrays are subtypes of one
   another only if they have exactly the same element type.  By default,

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 BaseTypeVisitor<Factory extends GenericAnnotatedTypeFactory<?, ?, ?
   /** The {@code when} element/field of the @Unused annotation. */
   protected final ExecutableElement unusedWhenElement;
 
+  /** The {@code value} element/field of @{@link SideEffectsOnly} annotation. */
+  ExecutableElement sideEffectsOnlyValueElement;
+
   /** True if "-Ashowchecks" was passed on the command line. */
   private final boolean showchecks;
   /** True if "-Ainfer" was passed on the command line. */
@@ -265,6 +270,8 @@ protected BaseTypeVisitor(BaseTypeChecker checker, Factory typeFactory) {
         atypeFactory.fromElement(elements.getTypeElement(Vector.class.getCanonicalName()));
     targetValueElement = TreeUtils.getMethod(Target.class, "value", 0, env);
     unusedWhenElement = TreeUtils.getMethod(Unused.class, "when", 0, env);
+    sideEffectsOnlyValueElement =
+        TreeUtils.getMethod(SideEffectsOnly.class, "value", 0, checker.getProcessingEnvironment());
     showchecks = checker.hasOption("showchecks");
     infer = checker.hasOption("infer");
     suggestPureMethods = checker.hasOption("suggestPureMethods") || infer;
@@ -887,6 +894,7 @@ public Void visitMethod(MethodTree node, Void p) {
       }
 
       checkPurity(node);
+      checkSideEffectsOnly(node);
 
       // Passing the whole method/constructor validates the return type
       validateTypeOf(node);
@@ -1036,6 +1044,65 @@ protected void checkPurity(MethodTree node) {
     }
   }
 
+  /**
+   * If the method {@code node} is annotated with {@link SideEffectsOnly}, checks 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 checkSideEffectsOnly(MethodTree node) {
+    if (!checker.hasOption("checkSideEffectsOnlyAnnotation")) {
+      return;
+    }
+
+    TreePath body = atypeFactory.getPath(node.getBody());
+    if (body == null) {
+      return;
+    } else {
+      @Nullable Element methodDeclElem = TreeUtils.elementFromTree(node);
+      AnnotationMirror sefOnlyAnnotation =
+          atypeFactory.getDeclAnnotation(methodDeclElem, SideEffectsOnly.class);
+      if (sefOnlyAnnotation == null) {
+        return;
+      }
+      List<String> sideEffectsOnlyExpressionStrings =
+          AnnotationUtils.getElementValueArray(
+              sefOnlyAnnotation, sideEffectsOnlyValueElement, String.class);
+      List<JavaExpression> 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<Pair<Tree, JavaExpression>> seOnlyIncorrectExprs = sefOnlyResult.getSeOnlyResult();
+      if (!seOnlyIncorrectExprs.isEmpty()) {
+        for (Pair<Tree, JavaExpression> s : seOnlyIncorrectExprs) {
+          if (!sideEffectsOnlyExpressions.contains(s.second)) {
+            checker.reportError(s.first, "incorrect.sideeffectsonly", s.second.toString());
+          }
+        }
+      }
+    }
+  }
+
   /**
    * Issue a warning if the result type of the constructor is not top. If it is a supertype of the
    * class, then a conflicting.annos error will also be issued by {@link

framework/src/main/java/org/checkerframework/common/basetype/SideEffectsOnlyAnnoChecker.java

@@ -0,0 +1,198 @@
+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 TreePath
+   * @param annoProvider AnnotationProvider
+   * @param sideEffectsOnlyExpressions List of JavaExpression
+   * @param processingEnv ProcessingEnvironment
+   * @param checker BaseTypeChecker
+   * @return SideEffectsOnlyResult
+   */
+  public static SideEffectsOnlyResult checkSideEffectsOnly(
+      TreePath statement,
+      AnnotationProvider annoProvider,
+      List<JavaExpression> sideEffectsOnlyExpressions,
+      ProcessingEnvironment processingEnv,
+      BaseTypeChecker checker) {
+    SideEffectsOnlyCheckerHelper helper =
+        new SideEffectsOnlyCheckerHelper(
+            annoProvider, sideEffectsOnlyExpressions, processingEnv, checker);
+    helper.scan(statement, null);
+    return helper.sideEffectsOnlyResult;
+  }
+
+  /** SideEffectsOnlyResult. */
+  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<Pair<Tree, JavaExpression>> seOnlyIncorrectExprs = new ArrayList<>(1);
+
+    /**
+     * Adds {@code t} and {@code javaExpr} as a Pair to seOnlyIncorrectExprs.
+     *
+     * @param t Tree
+     * @param javaExpr JavaExpression
+     */
+    public void addNotSEOnlyExpr(Tree t, JavaExpression javaExpr) {
+      seOnlyIncorrectExprs.add(Pair.of(t, javaExpr));
+    }
+
+    /**
+     * Returns {@code seOnlyIncorrectExprs}.
+     *
+     * @return seOnlyIncorrectExprs
+     */
+    public List<Pair<Tree, JavaExpression>> getSeOnlyResult() {
+      return seOnlyIncorrectExprs;
+    }
+  }
+
+  /** SideEffectsOnlyCheckerHelper. */
+  protected static class SideEffectsOnlyCheckerHelper extends TreePathScanner<Void, Void> {
+    /** Result computed by SideEffectsOnlyCheckerHelper. */
+    SideEffectsOnlyResult sideEffectsOnlyResult = new SideEffectsOnlyResult();
+    /**
+     * List of expressions specified as annotation arguments in {@link SideEffectsOnly} annotation.
+     */
+    List<JavaExpression> sideEffectsOnlyExpressions;
+
+    /** AnnotationProvider. */
+    protected final AnnotationProvider annoProvider;
+    /** Processing Environment. */
+    ProcessingEnvironment processingEnv;
+    /** BaseTypeChecker. */
+    BaseTypeChecker checker;
+
+    /**
+     * Constructor for SideEffectsOnlyCheckerHelper.
+     *
+     * @param annoProvider AnnotationProvider
+     * @param sideEffectsOnlyExpressions List of JavaExpressions
+     * @param processingEnv ProcessingEnvironment
+     * @param checker BaseTypeChecker
+     */
+    public SideEffectsOnlyCheckerHelper(
+        AnnotationProvider annoProvider,
+        List<JavaExpression> 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);
+      // If the invoked method is not annotated with @SideEffectsOnly,
+      // add those arguments to seOnlyIncorrectExprs
+      // that are not present in sideEffectsOnlyExpressions.
+      if (sideEffectsOnlyAnno == null) {
+        JavaExpression receiverExpr = JavaExpression.getReceiver(node);
+        if (!sideEffectsOnlyExpressions.contains(receiverExpr)) {
+          sideEffectsOnlyResult.addNotSEOnlyExpr(node, receiverExpr);
+        }
+      } else {
+        // If 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<String> sideEffectsOnlyExpressionStrings =
+            AnnotationUtils.getElementValueArray(
+                sideEffectsOnlyAnno, sideEffectsOnlyValueElement, String.class);
+        List<JavaExpression> 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.addNotSEOnlyExpr(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.addNotSEOnlyExpr(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);
+    }
+  }
+}

framework/src/main/java/org/checkerframework/common/basetype/messages.properties

@@ -76,6 +76,8 @@ 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
 
+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
 flowexpr.parse.error.postcondition=error parsing the postcondition expression for %s%ncannot parse the expression %s