Retain type refinements across calls to @SideEffectsOnly methods

checker/src/test/java/org/checkerframework/checker/test/junit/OptionalSideEffectsTest.java

@@ -0,0 +1,28 @@
+package org.checkerframework.checker.test.junit;
+
+import java.io.File;
+import java.util.List;
+import org.checkerframework.checker.optional.OptionalChecker;
+import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest;
+import org.junit.runners.Parameterized.Parameters;
+
+/**
+ * Tests that the Optional Checker retains type refinements across a call to a method that is
+ * annotated with {@code @SideEffectsOnly}.
+ */
+public class OptionalSideEffectsTest extends CheckerFrameworkPerDirectoryTest {
+
+  /**
+   * Create an OptionalSideEffectsTest.
+   *
+   * @param testFiles the files containing test code, which will be type-checked
+   */
+  public OptionalSideEffectsTest(List<File> testFiles) {
+    super(testFiles, OptionalChecker.class, "optional-side-effects", "-AcheckPurityAnnotations");
+  }
+
+  @Parameters
+  public static String[] getTestDirs() {
+    return new String[] {"optional-side-effects"};
+  }
+}

checker/src/test/java/org/checkerframework/checker/test/junit/SideEffectsOnlyTest.java

@@ -0,0 +1,25 @@
+package org.checkerframework.checker.test.junit;
+
+import java.io.File;
+import java.util.List;
+import org.checkerframework.checker.tainting.TaintingChecker;
+import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest;
+import org.junit.runners.Parameterized.Parameters;
+
+/** Tests {@code @SideEffectsOnly} annotations that are written in the code under test. */
+public class SideEffectsOnlyTest extends CheckerFrameworkPerDirectoryTest {
+
+  /**
+   * Create a SideEffectsOnlyTest.
+   *
+   * @param testFiles the files containing test code, which will be type-checked
+   */
+  public SideEffectsOnlyTest(List<File> testFiles) {
+    super(testFiles, TaintingChecker.class, "sideeffectsonly", "-AcheckPurityAnnotations");
+  }
+
+  @Parameters
+  public static String[] getTestDirs() {
+    return new String[] {"sideeffectsonly"};
+  }
+}

checker/tests/nullness/SetIteratorTest.java

@@ -26,7 +26,6 @@ public String listChildren(String parentNode) {
 
     if (edges.get(parentNode) != null) {
       for (String childNode : edges.get(parentNode).keySet()) {
-        // :: error: [dereference.of.nullable]
         edges.get(parentNode).toString();
         for (String childNodeEdgeX : edges.get(parentNode).get(childNode)) {
           childrenString += " " + childNode + "(" + childNodeEdgeX + ")";
@@ -42,7 +41,6 @@ public void listChildren2(String parentNode) {
       Iterator<String> itor = edges.get(parentNode).keySet().iterator();
       edges.get(parentNode).toString();
       String s = itor.next();
-      // :: error: [dereference.of.nullable]
       edges.get(parentNode).toString();
     }
   }

checker/tests/nullness/SideEffectsOnlySuper.java

@@ -0,0 +1,33 @@
+// A `@SideEffectsOnly("this")` method that is called via `super` side-effects the object that the
+// caller denotes as `this`, so refinements of that object's fields must be discarded.
+
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.dataflow.qual.SideEffectsOnly;
+
+public class SideEffectsOnlySuper {
+
+  static class Super {
+    @Nullable Object f;
+
+    @SideEffectsOnly("this")
+    void clear() {
+      f = null;
+    }
+  }
+
+  static class Sub extends Super {
+    void viaSuper() {
+      f = new Object();
+      super.clear();
+      // :: error: (dereference.of.nullable)
+      f.toString();
+    }
+
+    void viaThis() {
+      f = new Object();
+      this.clear();
+      // :: error: (dereference.of.nullable)
+      f.toString();
+    }
+  }
+}

checker/tests/optional-side-effects/OptionalSideEffectsLambda.java

@@ -0,0 +1,44 @@
+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.SideEffectFree;
+
+class OptionalSideEffectsLambda {
+
+  void fooWithEnhancedFor(OptContainer container, List<String> strs) {
+    if (!container.getOptStr().isPresent()) {
+      return;
+    }
+    for (String s : strs) {
+      // This should verify because the call to Iterator.next only side effects the iterator.
+      bar(container);
+    }
+  }
+
+  void fooWithForEach(OptContainer container, List<String> strs) {
+    if (!container.getOptStr().isPresent()) {
+      return;
+    }
+    strs.forEach(s -> bar(container));
+  }
+
+  @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,68 @@
+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) {}
+
+  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;
+    }
+  }
+}

checker/tests/sideeffectsonly/PureMethodCallRefinement.java

@@ -0,0 +1,101 @@
+// A `@SideEffectsOnly` annotation says what the callee writes, but says nothing about what a
+// `@Pure` method reads.  A refinement of a `@Pure` method call must therefore be discarded when
+// a listed expression is reached through the call's receiver or one of its arguments, even though
+// the call is not built out of the listed expression.
+
+import org.checkerframework.checker.tainting.qual.Tainted;
+import org.checkerframework.checker.tainting.qual.Untainted;
+import org.checkerframework.dataflow.qual.Pure;
+import org.checkerframework.dataflow.qual.SideEffectsOnly;
+import org.checkerframework.framework.qual.EnsuresQualifier;
+
+public class PureMethodCallRefinement {
+
+  @Tainted Object f;
+
+  @Pure
+  Object getF() {
+    return f;
+  }
+
+  @EnsuresQualifier(expression = "#1.getF()", qualifier = Untainted.class)
+  // :: error: contracts.postcondition
+  void makeUntainted(PureMethodCallRefinement o) {}
+
+  @SideEffectsOnly("#1.f")
+  void modifyField(PureMethodCallRefinement o) {}
+
+  @SideEffectsOnly("this")
+  void modifyThis() {}
+
+  void test(PureMethodCallRefinement o) {
+    makeUntainted(o);
+    // `modifyField` may write `o.f`, which `getF()` returns.  The annotation does not mention
+    // `o.getF()`, but that expression is not a subexpression of `o.f`, so a rule based only on
+    // subexpressions would wrongly retain the refinement.
+    modifyField(o);
+    // :: error: assignment
+    @Untainted Object y = o.getF();
+  }
+
+  void testNestedCall(PureMethodCallRefinement o) {
+    makeUntaintedNested(o);
+    // The stored expression's receiver is itself a call, so the search for the modified location
+    // must recur through it.
+    modifyField(o);
+    // :: error: assignment
+    @Untainted Object y = o.getSelf().getF();
+  }
+
+  @Pure
+  PureMethodCallRefinement getSelf() {
+    return this;
+  }
+
+  @EnsuresQualifier(expression = "#1.getSelf().getF()", qualifier = Untainted.class)
+  // :: error: contracts.postcondition
+  void makeUntaintedNested(PureMethodCallRefinement o) {}
+
+  @Tainted Object g;
+
+  @Tainted Object @Tainted [] arr = new @Tainted Object[10];
+
+  @Pure
+  Object @Tainted [] getArr() {
+    return arr;
+  }
+
+  @EnsuresQualifier(expression = "#1.getSelf().g", qualifier = Untainted.class)
+  // :: error: contracts.postcondition
+  void makeUntaintedFieldOfCall(PureMethodCallRefinement o) {}
+
+  @EnsuresQualifier(expression = "#1.getArr()[0]", qualifier = Untainted.class)
+  // :: error: contracts.postcondition
+  void makeUntaintedElementOfCall(PureMethodCallRefinement o) {}
+
+  void testFieldOfCall(PureMethodCallRefinement o) {
+    makeUntaintedFieldOfCall(o);
+    // The stored expression is a field access, not a call, but its receiver is a call, so the
+    // search for the modified location must recur through the receiver.
+    modifyField(o);
+    // :: error: assignment
+    @Untainted Object y = o.getSelf().g;
+  }
+
+  void testElementOfCall(PureMethodCallRefinement o) {
+    makeUntaintedElementOfCall(o);
+    // The stored expression is an array access whose array is a call.
+    modifyField(o);
+    // :: error: assignment
+    @Untainted Object y = o.getArr()[0];
+  }
+
+  void testUnrelatedReceiver(PureMethodCallRefinement o) {
+    makeUntainted(o);
+    // `modifyThis` modifies `this`, which is unrelated to `o` and to `o`'s fields.  Like every
+    // other use of `@SideEffectsOnly` for type refinement, this is unsound if `this` and `o` are
+    // aliases, or if `o` is reachable from `this`.
+    modifyThis();
+    @Untainted Object y = o.getF();
+  }
+}

checker/tests/sideeffectsonly/SideEffectsMultiple.java

@@ -0,0 +1,24 @@
+import org.checkerframework.checker.tainting.qual.Tainted;
+import org.checkerframework.checker.tainting.qual.Untainted;
+import org.checkerframework.dataflow.qual.SideEffectsOnly;
+import org.checkerframework.framework.qual.EnsuresQualifier;
+
+public class SideEffectsMultiple {
+  @Tainted Object x;
+
+  void test() {
+    method(x);
+    method1(x);
+    // :: error: [argument]
+    method2(x);
+  }
+
+  @EnsuresQualifier(expression = "#1", qualifier = Untainted.class)
+  // :: error: contracts.postcondition
+  void method(Object x) {}
+
+  @SideEffectsOnly({"this", "#1"})
+  void method1(@Untainted Object y) {}
+
+  void method2(@Untainted Object x) {}
+}

checker/tests/sideeffectsonly/SideEffectsOnlyField.java

@@ -0,0 +1,30 @@
+import org.checkerframework.checker.tainting.qual.Tainted;
+import org.checkerframework.checker.tainting.qual.Untainted;
+import org.checkerframework.dataflow.qual.SideEffectFree;
+import org.checkerframework.dataflow.qual.SideEffectsOnly;
+import org.checkerframework.framework.qual.EnsuresQualifier;
+
+public class SideEffectsOnlyField {
+  @Tainted Object a;
+  @Tainted 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 = Untainted.class)
+  // :: error: contracts.postcondition
+  static void method(SideEffectsOnlyField x) {}
+
+  @SideEffectsOnly("#1.a")
+  static void method3(SideEffectsOnlyField z) {}
+
+  @SideEffectFree
+  static void method2(@Untainted Object x) {}
+}