Add @SideEffectsOnly annotation

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

docs/manual/advanced-features.tex

@@ -1019,7 +1019,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.
@@ -1059,7 +1060,7 @@
   }
 \end{Verbatim}
 
-There are three ways to express that \<computeValue> does not set
+There are four ways to express that \<computeValue> does not set
 \<myField> to \<null>, and thus to prevent the Nullness Checker from
 issuing a warning about the call \<myField.toString()>.
 
@@ -1073,6 +1074,15 @@
   int computeValue() { ... }
 \end{Verbatim}
 
+\item
+  If \<computeValue> has side effects, but they do not affect \<myField>,
+  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
@@ -1126,6 +1136,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:

docs/manual/called-methods-checker.tex

@@ -218,15 +218,19 @@
   \end{Verbatim}
 
   If \<m()> 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 \<m()>, and therefore assumes
   the worst: that all information it knows about in-scope variables (including
   that \<close()> was called on \<sock>) is stale and must be discarded.
   There are two possible fixes:
 
   \begin{itemize}
-  \item add a \<@SideEffectFree> or \<@Pure> annotation to \<m()>, if \<m()> is
+  \item add a \refqualclass{dataflow/qual}{SideEffectFree},
+  \refqualclass{dataflow/qual}{SideEffectsOnly}, or
+  \refqualclass{dataflow/qual}{Pure} annotation to \<m()>, if \<m()> is
     in fact side-effect free or pure; or
   \item re-order the calls to \<sock.close()> and \<m()> so that the call
     to \<sock.close()> appears last in \<closeSocket()>.

docs/manual/introduction.tex

@@ -608,6 +608,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,
@@ -1554,6 +1555,10 @@
   If your proof includes ``method \<m> has no side effects'',
   then annotate \<m>'s declaration with
   \refqualclass{dataflow/qual}{SideEffectFree}.
+\item
+  If your proof includes ``method \<m> has limited side effects'',
+  then annotate \<m>'s declaration with
+  \refqualclass{dataflow/qual}{SideEffectsOnly}.
 \item
   If your proof includes ``each call to method \<m> returns the same value'',
   then annotate \<m>'s declaration with

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 \<null>. (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}

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.
 

docs/manual/troubleshooting.tex

@@ -367,6 +367,7 @@
 \<isCompleted()> does not set the field \<currentOutgoing> to \<null>, 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 \<isCompleted()>; see Sections~\ref{type-refinement-purity}
 and~\ref{nullness-method-annotations}.

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 BaseTypeVisitor<Factory extends GenericAnnotatedTypeFactory<?, ?, ?
   /** The {@code when} element/field of the @Unused annotation. */
   protected final ExecutableElement unusedWhenElement;
 
+  /** The {@code value} element/field of the @{@link SideEffectsOnly} annotation. */
+  ExecutableElement sideEffectsOnlyValueElement;
+
   /** True if "-Ashowchecks" was passed on the command line. */
   protected final boolean showchecks;
 
@@ -304,6 +309,8 @@ protected BaseTypeVisitor(BaseTypeChecker checker, @Nullable 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;
@@ -1075,24 +1082,29 @@ protected boolean shouldPerformContractInference() {
    * AnnotatedTypeMirror.AnnotatedDeclaredType, AnnotatedTypeMirror.AnnotatedExecutableType,
    * AnnotatedTypeMirror.AnnotatedDeclaredType)}.
    *
+   * <p>If 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;
+    // }
 
     // `body` is lazily assigned.
     TreePath body = null;
     boolean bodyAssigned = false;
 
     if (suggestPureMethods || PurityUtils.hasPurityAnnotation(atypeFactory, tree)) {
-
       // check "no" purity
       EnumSet<Pure.Kind> kinds = PurityUtils.getPurityKinds(atypeFactory, tree);
       // @Deterministic makes no sense for a void method or constructor
@@ -1159,6 +1171,77 @@ 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<String> sideEffectsOnlyExpressionStrings =
+          AnnotationUtils.getElementValueArray(
+              sefOnlyAnnotation, sideEffectsOnlyValueElement, String.class);
+      List<JavaExpression> sideEffectsOnlyExpressions =
+          new ArrayList<>(sideEffectsOnlyExpressionStrings.size());
+      for (String st : sideEffectsOnlyExpressionStrings) {
+        try {
+          JavaExpression exprJe = StringToJavaExpression.atMethodBody(st, tree, checker);
+          sideEffectsOnlyExpressions.add(exprJe);
+        } catch (JavaExpressionParseUtil.JavaExpressionParseException ex) {
+          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<IPair<Tree, JavaExpression>> seOnlyIncorrectExprs = sefOnlyResult.getExprs();
+      // System.out.printf("seOnlyIncorrectExprs = %s%n", seOnlyIncorrectExprs);
+
+      if (!seOnlyIncorrectExprs.isEmpty()) {
+        for (IPair<Tree, JavaExpression> s : seOnlyIncorrectExprs) {
+          if (!sideEffectsOnlyExpressions.contains(s.second)) {
+            // System.out.printf("Error 2%n");
+            checker.reportError(s.first, "purity.incorrect.sideeffectsonly", 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.
     // ...
@@ -1169,6 +1252,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);
+  }
+
   /**
    * Infer a purity annotation for {@code elt} by converting {@code kinds} into a method annotation.
    *