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). + *
Determinism does not 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.) * - *
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: + *
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). + * + *
Use in flow-sensitive type refinement: 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: + * + *
{@code
+ * @Deterministic
+ * Object myDeterministicMethod() {
+ * Object o = this.f;
+ * this.f = null;
+ * return o;
+ * }
+ * }
+ *
+ * but a type refinement on the result of a first call does not survive a second call:
*
* {@code
* if (x.myDeterministicMethod() != null) {
- * x.myDeterministicMethod().hashCode();
+ * x.myDeterministicMethod().hashCode(); // throws NullPointerException
* }
* }
*
+ * 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}.
+ *
* Note that {@code @Deterministic} guarantees that the result is identical according to {@code * ==}, not just equal according to {@code equals()}. This means that writing * {@code @Deterministic} on a method that returns a reference (including a String) is often diff --git a/checker-qual/src/main/java/org/checkerframework/dataflow/qual/Pure.java b/checker-qual/src/main/java/org/checkerframework/dataflow/qual/Pure.java index 1b57e655fd99..e992fa51f294 100644 --- a/checker-qual/src/main/java/org/checkerframework/dataflow/qual/Pure.java +++ b/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}. + * + *
For pluggable type-checking, the two components play complementary roles: + * + *
For a discussion of the meaning of {@code Pure} on a constructor, see the documentation of * {@link Deterministic}. diff --git a/checker-qual/src/main/java/org/checkerframework/dataflow/qual/SideEffectFree.java b/checker-qual/src/main/java/org/checkerframework/dataflow/qual/SideEffectFree.java index da33d80443e7..d763147a6a56 100644 --- a/checker-qual/src/main/java/org/checkerframework/dataflow/qual/SideEffectFree.java +++ b/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. * + *
{@code @SideEffectFree} preserves facts about heap across the call. To + * additionally guarantee that two calls to the same 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. + * *
Also see {@link Pure}, which means both side-effect-free and {@link Deterministic}. * *
Analysis: The Checker Framework performs a conservative analysis to verify a