Inherited @SideEffectsOnly annotations

checker/tests/sideeffectsonly/SideEffectsOnlyInherit.java

@@ -0,0 +1,71 @@
+// A method that overrides methods in two supertypes inherits the union of their
+// `@SideEffectsOnly` expressions, not just the first supertype's.  The `value` element of
+// `@SideEffectsOnly` is significant, unlike that of the other inherited declaration annotations.
+
+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 SideEffectsOnlyInherit {
+
+  static class Cell {
+    @Tainted Object f;
+    @Tainted Object g;
+  }
+
+  interface I {
+    @SideEffectsOnly("#1.f")
+    void m(Cell c);
+  }
+
+  static class Base {
+    @SideEffectsOnly("#1.g")
+    public void m(Cell c) {}
+  }
+
+  // `C.m` cannot satisfy both supertype specifications; the override errors are suppressed in
+  // order to test what `C.m` inherits.  Whichever supertype `AnnotatedTypes.overriddenMethods`
+  // yields first, `C.m` is treated as side-effecting both `#1.f` and `#1.g`.
+  @SuppressWarnings("purity.sideeffectsonly.overriding")
+  static class C extends Base implements I {
+    @Override
+    public void m(Cell c) {}
+  }
+
+  @EnsuresQualifier(expression = "#1.f", qualifier = Untainted.class)
+  // :: error: contracts.postcondition
+  static void makeFUntainted(Cell c) {}
+
+  @EnsuresQualifier(expression = "#1.g", qualifier = Untainted.class)
+  // :: error: contracts.postcondition
+  static void makeGUntainted(Cell c) {}
+
+  static void testF(C receiver, Cell c) {
+    makeFUntainted(c);
+    receiver.m(c);
+    // :: error: assignment
+    @Untainted Object y = c.f;
+  }
+
+  static void testG(C receiver, Cell c) {
+    makeGUntainted(c);
+    receiver.m(c);
+    // :: error: assignment
+    @Untainted Object y = c.g;
+  }
+
+  // A `@SideEffectsOnly` written on the method itself is authoritative: nothing is inherited.
+  @SuppressWarnings("purity.sideeffectsonly.overriding")
+  static class D extends Base implements I {
+    @SideEffectsOnly("#1.f")
+    @Override
+    public void m(Cell c) {}
+  }
+
+  static void testOwnAnnotationWins(D receiver, Cell c) {
+    makeGUntainted(c);
+    receiver.m(c);
+    @Untainted Object y = c.g;
+  }
+}

checker/tests/sideeffectsonly/SideEffectsOnlyInheritScope.java

@@ -0,0 +1,47 @@
+// The expressions of an inherited `@SideEffectsOnly` annotation are resolved in the scope of the
+// supertype method that declares them, not in the scope of the method that inherits them.
+
+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 SideEffectsOnlyInheritScope {
+
+  static class Sup {
+    @Tainted Object f;
+
+    @SideEffectsOnly("this.f")
+    void m() {}
+  }
+
+  static class Sub extends Sup {
+    // Shadows `Sup.f`.  `Sub.m` inherits a specification about `Sup.f`, not about `Sub.f`.
+    @Tainted Object f;
+
+    @Override
+    void m() {}
+  }
+
+  @EnsuresQualifier(expression = "#1.f", qualifier = Untainted.class)
+  // :: error: contracts.postcondition
+  static void makeSupFUntainted(Sup s) {}
+
+  @EnsuresQualifier(expression = "#1.f", qualifier = Untainted.class)
+  // :: error: contracts.postcondition
+  static void makeSubFUntainted(Sub s) {}
+
+  static void testShadowingFieldIsRetained(Sub s) {
+    makeSubFUntainted(s);
+    s.m();
+    // `Sub.f` is not side-effected, so its refinement is retained.
+    @Untainted Object y = s.f;
+  }
+
+  static void testShadowedFieldIsDiscarded(Sub s) {
+    makeSupFUntainted(s);
+    s.m();
+    // :: error: assignment
+    @Untainted Object y = ((Sup) s).f;
+  }
+}

checker/tests/sideeffectsonly/SideEffectsOnlyOverride.java

@@ -0,0 +1,85 @@
+// An overriding method must not side-effect more than the overridden method's
+// `@SideEffectsOnly` annotation permits.  Otherwise a call whose receiver is statically of the
+// supertype would retain a refinement that the override invalidates.
+
+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 SideEffectsOnlyOverride {
+
+  static class Cell {
+    @Tainted Object g;
+    @Tainted Cell inner;
+  }
+
+  static class Super {
+    @SideEffectsOnly("#1.inner")
+    void m(Cell c) {}
+  }
+
+  /** Side-effects exactly what the supertype permits. */
+  static class SubSame extends Super {
+    @SideEffectsOnly("#1.inner")
+    @Override
+    void m(Cell c) {}
+  }
+
+  /** Side-effects less than the supertype permits: `#1.inner.g` is reached through `#1.inner`. */
+  static class SubDeeper extends Super {
+    @SideEffectsOnly("#1.inner.g")
+    @Override
+    void m(Cell c) {}
+  }
+
+  /** Side-effects nothing at all. */
+  static class SubSideEffectFree extends Super {
+    @SideEffectFree
+    @Override
+    void m(Cell c) {}
+  }
+
+  /** Side-effects more than the supertype permits. */
+  static class SubMore extends Super {
+    @SideEffectsOnly({"#1.inner", "#1.g"})
+    @Override
+    // TODO :: error: purity.sideeffectsonly.overriding
+    void m(Cell c) {}
+  }
+
+  /** `#1` is not reached through `#1.inner`, so side-effecting it is more than permitted. */
+  static class SubWhole extends Super {
+    @SideEffectsOnly("#1")
+    @Override
+    // TODO :: error: purity.sideeffectsonly.overriding
+    void m(Cell c) {}
+  }
+
+  /** A supertype without `@SideEffectsOnly` constrains nothing. */
+  static class Unconstrained {
+    void m(Cell c) {}
+  }
+
+  static class SubOfUnconstrained extends Unconstrained {
+    @SideEffectsOnly("#1.inner")
+    @Override
+    void m(Cell c) {}
+  }
+
+  @EnsuresQualifier(expression = "#1.g", qualifier = Untainted.class)
+  // :: error: contracts.postcondition
+  static void makeUntainted(Cell c) {}
+
+  /**
+   * Without the override check, this refinement would be wrongly retained: the call resolves
+   * statically to {@code Super.m}, which does not permit side-effecting {@code c.g}, but it may
+   * execute {@code SubMore.m}, which does.
+   */
+  static void testDynamicDispatch(Super s, Cell c) {
+    makeUntainted(c);
+    s.m(c);
+    @Untainted Object y = c.g;
+  }
+}

framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java

@@ -198,39 +198,49 @@ public void performAnalysis(ControlFlowGraph cfg, List<FieldInitialValue<V>> fie
    */
   private @Nullable List<JavaExpression> computeSideEffectsOnlyExpressions(
       ExecutableElement method, MethodInvocationNode methodInvocationNode) {
-    List<String> seOnlyExpressionStrings = atypeFactory.getSideEffectsOnlyExpressionStrings(method);
+    Map<ExecutableElement, List<String>> seOnlyExpressionStrings =
+        atypeFactory.getSideEffectsOnlyExpressionStrings(method);
     if (seOnlyExpressionStrings == null) {
       return null;
     }
 
     List<JavaExpression> seOnlyExpressions = new ArrayList<>();
 
-    for (String seOnlyExpr : seOnlyExpressionStrings) {
-      try {
-        // Do not use `StringToJavaExpression.atMethodInvocation(seOnlyExpr,
-        // methodInvocationNode, checker)`, which obtains the invoked method from
-        // `methodInvocationNode.getTree()`; that tree is null for a call that corresponds to no
-        // AST tree, such as the `Iterator.next()` that an enhanced for loop is desugared to.
-        JavaExpression exprJe =
-            StringToJavaExpression.atMethodDecl(seOnlyExpr, method, checker)
-                .atMethodInvocation(methodInvocationNode);
-
-        if (exprJe.containsUnknown()) {
-          // Nothing in the store can match an `Unknown`, so returning the expression would discard
-          // no refinement at all.  Returning null makes the caller discard every refinement.
+    for (Map.Entry<ExecutableElement, List<String>> entry : seOnlyExpressionStrings.entrySet()) {
+      // The method whose `@SideEffectsOnly` annotation contains the expressions.  It is `method`
+      // itself, unless `method` inherits the annotation.
+      ExecutableElement declaringMethod = entry.getKey();
+      for (String seOnlyExpr : entry.getValue()) {
+        try {
+          // An expression is parsed in the scope of the method that declares it, which is not
+          // necessarily the scope of `method`:  a field that the declaring method's class declares
+          // might be shadowed or inaccessible in `method`'s class.
+          // Do not use `StringToJavaExpression.atMethodInvocation(seOnlyExpr,
+          // methodInvocationNode, checker)`, which obtains the invoked method from
+          // `methodInvocationNode.getTree()`; that tree is null for a call that corresponds to no
+          // AST tree, such as the `Iterator.next()` that an enhanced for loop is desugared to.
+          JavaExpression exprJe =
+              StringToJavaExpression.atMethodDecl(seOnlyExpr, declaringMethod, checker)
+                  .atMethodInvocation(methodInvocationNode);
+
+          if (exprJe.containsUnknown()) {
+            // Nothing in the store can match an `Unknown`, so returning the expression would
+            // discard no refinement at all.  Returning null makes the caller discard every
+            // refinement.
+            return null;
+          }
+
+          // At a call of the form `super.m()`, viewpoint-adapting the callee's `this` yields
+          // `super`.
+          // The caller refers to that same object as `this`, so rewrite it that way; otherwise
+          // the refinements of `this` and of its fields would not be discarded.
+          exprJe = JavaExpression.superToThis(exprJe);
+          seOnlyExpressions.add(exprJe);
+        } catch (JavaExpressionParseException ex) {
+          // The expression cannot be represented at the call site, so the caller must assume that
+          // the call might side-effect anything.  A future change will report the parse error.
           return null;
         }
-
-        // At a call of the form `super.m()`, viewpoint-adapting the callee's `this` yields
-        // `super`.
-        // The caller refers to that same object as `this`, so rewrite it that way; otherwise
-        // the refinements of `this` and of its fields would not be discarded.
-        exprJe = JavaExpression.superToThis(exprJe);
-        seOnlyExpressions.add(exprJe);
-      } catch (JavaExpressionParseException ex) {
-        // The expression cannot be represented at the call site, so the caller must assume that
-        // the call might side-effect anything.  A future change will report the parse error.
-        return null;
       }
     }