| 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; |
| |
| /** |
| * A method is called <em>deterministic</em> if it returns the same value (according to {@code ==}) |
| * every time it is called with the same parameters and in the same environment. The parameters |
| * 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>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: |
| * |
| * <pre>{@code |
| * if (x.myDeterministicMethod() != null) { |
| * x.myDeterministicMethod().hashCode(); |
| * } |
| * }</pre> |
| * |
| * <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 |
| * erroneous unless the returned value is cached or interned. |
| * |
| * <p>Also see {@link Pure}, which means both deterministic and {@link SideEffectFree}. |
| * |
| * <p><b>Analysis:</b> The Checker Framework performs a conservative analysis to verify a |
| * {@code @Deterministic} annotation. The Checker Framework issues a warning if the method uses any |
| * of the following Java constructs: |
| * |
| * <ol> |
| * <li>Assignment to any expression, except for local variables and method parameters.<br> |
| * (Note that storing into an array element, such a {@code a[i] = x}, is not an assignment to |
| * a variable and is therefore forbidden.) |
| * <li>A method invocation of a method that is not {@link Deterministic}. |
| * <li>Construction of a new object. |
| * <li>Catching any exceptions. This restriction prevents a method from obtaining a reference to a |
| * newly-created exception object and using these objects (or some property thereof) to change |
| * the method's return value. For instance, the following method must be forbidden. |
| * <!-- "<code>" instead of "{@code ...}" because of at-sign at beginning of line --> |
| * <pre><code>@Deterministic |
| * int f() { |
| * try { |
| * int b = 0; |
| * int a = 1/b; |
| * } catch (Throwable t) { |
| * return t.hashCode(); |
| * } |
| * return 0; |
| * } |
| * </code></pre> |
| * </ol> |
| * |
| * When a constructor is annotated as {@code Deterministic} (or {@code @Pure}), that means that all |
| * the fields are deterministic (the same values, if the arguments are the same). The constructed |
| * object itself is different. That is, a constructor <em>invocation</em> is never deterministic |
| * since it returns a different new object each time. |
| * |
| * <p>Note that the rules for checking currently imply that every {@code Deterministic} method is |
| * also {@link SideEffectFree}. This might change in the future; in general, a deterministic method |
| * does not need to be side-effect-free. |
| * |
| * <p>These rules are conservative: any code that passes the checks is deterministic, but the |
| * Checker Framework may issue false positive warnings, for code that uses one of the forbidden |
| * constructs but is deterministic nonetheless. |
| * |
| * <p>In fact, the rules are so conservative that checking is currently disabled by default, but can |
| * be enabled via the {@code -AcheckPurityAnnotations} command-line option. |
| * |
| * <p>This annotation is inherited by subtypes, just as if it were meta-annotated with |
| * {@code @InheritedAnnotation}. |
| * |
| * @checker_framework.manual #type-refinement-purity Side effects, determinism, purity, and |
| * flow-sensitive analysis |
| */ |
| // @InheritedAnnotation cannot be written here, because "dataflow" project cannot depend on |
| // "framework" project. |
| @Documented |
| @Retention(RetentionPolicy.RUNTIME) |
| @Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) |
| public @interface Deterministic {} |