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

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<File> testFiles) {
+    super(
+        testFiles,
+        org.checkerframework.checker.optional.OptionalChecker.class,
+        "optional",
+        "-AcheckPurityAnnotations");
+  }
+
+  @Parameters
+  public static String[] getTestDirs() {
+    return new String[] {"optional-side-effects"};
+  }
+}

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<String> strs) {
+    if (!container.getOptStr().isPresent()) {
+      return;
+    }
+    for (String s : strs) {
+      bar(container); // OK
+    }
+  }
+
+  void fooWithForEach(OptContainer container, List<String> 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<String> optStr;
+
+    OptContainer(String s) {
+      this.optStr = Optional.ofNullable(s);
+    }
+
+    @Pure
+    public Optional<String> getOptStr() {
+      return this.optStr;
+    }
+  }
+}

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<String> strs = new ArrayList<>();
+    methodA(optContainer, strs);
+    optContainer.getOpt().get(); // OK
+    bar(optContainer); // OK
+  }
+
+  void test2(OptionalContainer optContainer) {
+    if (!optContainer.getOpt().isPresent()) {
+      return;
+    }
+    List<String> strs = new ArrayList<>();
+    methodB(optContainer, strs);
+
+    // :: error: (contracts.precondition)
+    bar(optContainer);
+  }
+
+  void test3(OptionalContainer optContainer) {
+    if (!optContainer.getOpt().isPresent()) {
+      return;
+    }
+    List<String> 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<String> opt;
+
+    @SuppressWarnings("optional:parameter")
+    OptionalContainer(Optional<String> opt) {
+      this.opt = opt;
+    }
+
+    @Pure // Not required if running under -AassumePureGetters
+    public Optional<String> getOpt() {
+      return this.opt;
+    }
+  }
+}

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 \<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()>.
 
@@ -1077,6 +1078,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
@@ -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:

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

@@ -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 \<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}.