Clarify roles of @Deterministic, @Pure, and @SideEffectFree annotations

checker-qual/src/main/java/org/checkerframework/dataflow/qual/Deterministic.java

@@ -7,27 +7,50 @@
 import java.lang.annotation.Target;
 
 /**
- * A method is called <em>deterministic</em> if it returns the same value (according to {@code ==})
- * every time it is called with the same arguments and in the same environment. The arguments
- * include the receiver, and the environment includes all of the Java heap (that is, all fields of
- * all objects and all static variables).
+ * A method is called <em>deterministic</em> if, starting from the same arguments and the same
+ * initial environment, every invocation produces the same return value (according to {@code ==})
+ * and the same final environment. The arguments include the receiver, and the environment
+ * includes all of the Java heap (that is, all fields of all objects and all static variables).
  *
- * <p>Determinism refers to the return value during a non-exceptional execution. If a method throws
- * an exception, the Throwable does not have to be exactly the same object on each invocation (and
- * generally should not be, to capture the correct stack trace).
+ * <p>Determinism does <em>not</em> mean that the method leaves the heap unchanged; it means that
+ * any changes the method makes to the heap are the same on every invocation from the same
+ * starting heap. For example, a method whose body always executes {@code this.f = 99; return 5;}
+ * is deterministic, even though it is not {@link SideEffectFree}. (The Checker Framework's
+ * conservative analysis described below is currently stricter than this — see the note in the
+ * Analysis section.)
  *
- * <p>This annotation is important to pluggable type-checking because, after a call to a
- * {@code @Deterministic} method, flow-sensitive type refinement can assume that anything learned
- * about the first invocation is true about subsequent invocations (so long as no
- * non-{@code @}{@link SideEffectFree} method call intervenes). For example, the following code
- * never suffers a null pointer exception, so the Nullness Checker need not issue a warning:
+ * <p>Determinism refers to the return value (and the final environment) during a non-exceptional
+ * execution. If a method throws an exception, the Throwable does not have to be exactly the same
+ * object on each invocation (and generally should not be, to capture the correct stack trace).
+ *
+ * <p><b>Use in flow-sensitive type refinement:</b> By itself, {@code @Deterministic} provides only
+ * a limited guarantee. Two consecutive calls to the same {@code @Deterministic} method are not
+ * guaranteed to return the same value, because the first call may have changed the heap, so the
+ * second call no longer starts from the same environment. For example, the following method is
+ * deterministic:
+ *
+ * <pre>{@code
+ * @Deterministic
+ * Object myDeterministicMethod() {
+ *   Object o = this.f;
+ *   this.f = null;
+ *   return o;
+ * }
+ * }</pre>
+ *
+ * but a type refinement on the result of a first call does not survive a second call:
  *
  * <pre>{@code
  * if (x.myDeterministicMethod() != null) {
- *   x.myDeterministicMethod().hashCode();
+ *   x.myDeterministicMethod().hashCode(); // throws NullPointerException
  * }
  * }</pre>
  *
+ * because the first call sets {@code this.f} to {@code null}, so the second call returns
+ * {@code null}. To get the guarantee that any property inferred from one call also holds at a
+ * subsequent call to the same method, the method must be both {@code @Deterministic} and
+ * {@link SideEffectFree} — that is, {@link Pure}.
+ *
  * <p>Note that {@code @Deterministic} guarantees that the result is identical according to {@code
  * ==}, <b>not</b> just equal according to {@code equals()}. This means that writing
  * {@code @Deterministic} on a method that returns a reference (including a String) is often

checker-qual/src/main/java/org/checkerframework/dataflow/qual/Pure.java

@@ -8,8 +8,24 @@
 
 /**
  * {@code Pure} is a method annotation that means both {@link SideEffectFree} and {@link
- * Deterministic}. The more important of these, when performing pluggable type-checking, is usually
- * {@link SideEffectFree}.
+ * Deterministic}.
+ *
+ * <p>For pluggable type-checking, the two components play complementary roles:
+ *
+ * <ul>
+ *   <li>{@link SideEffectFree} preserves facts <em>about heap</em> across the call: a
+ *       property known about a field before the call is still known afterwards.
+ *   <li>{@link Deterministic} ensures that, from the same starting state, the call always returns
+ *       the same value. By itself this is not enough to assume a property checked on the result of
+ *       one call also holds on the result of a subsequent call to the same method, because a
+ *       deterministic method may make state changes that invalidate its own precondition on the
+ *       second call (see {@link Deterministic} for an example).
+ * </ul>
+ *
+ * Only {@code @Pure} provides both guarantees together: facts inferred from a {@code @Pure} call
+ * survive across the call and across subsequent calls to the same method with the same arguments
+ * and receiver, provided those subsequent calls begin in the same relevant starting state (that
+ * is, with no intervening state changes that affect the method's result).
  *
  * <p>For a discussion of the meaning of {@code Pure} on a constructor, see the documentation of
  * {@link Deterministic}.

checker-qual/src/main/java/org/checkerframework/dataflow/qual/SideEffectFree.java

@@ -22,6 +22,13 @@
  * modified, which annuls the effect of flow-sensitive type refinement and prevents the pluggable
  * type-checker from making conclusions that are obvious to a programmer.
  *
+ * <p>{@code @SideEffectFree} preserves facts <em>about heap</em> across the call. To
+ * additionally guarantee that two calls to the <em>same</em> method return identical values when
+ * they start from the same environment (so a property checked on the result of one call also
+ * holds on the result of a subsequent call), the method must also be {@link Deterministic}; a
+ * method that is both {@code @SideEffectFree} and {@code @Deterministic} is {@link Pure}. See
+ * {@link Deterministic} for an example of why {@code @Deterministic} alone is not sufficient.
+ *
  * <p>Also see {@link Pure}, which means both side-effect-free and {@link Deterministic}.
  *
  * <p><b>Analysis:</b> The Checker Framework performs a conservative analysis to verify a