| 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> |
| * {@literal @}Deterministic</code> 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). |
| * <li>A method invocation of a method that is not {@link Deterministic}. |
| * <li>Construction of a new object. |
| * <li>Catching any exceptions. This is to prevent a method to get a hold of newly created objects |
| * and using these objects (or some property thereof) to change their return value. For |
| * instance, the following method must be forbidden. |
| * <pre> |
| * {@code @Deterministic |
| * int f() { |
| * try { |
| * int b = 0; |
| * int a = 1/b; |
| * } catch (Throwable t) { |
| * return t.hashCode(); |
| * } |
| * return 0; |
| * } |
| * }</pre> |
| * </ol> |
| * |
| * A constructor can be {@code @Pure}, but a constructor <em>invocation</em> is not deterministic |
| * since it returns a different new object each time. TODO: Side-effect-free constructors could be |
| * allowed to set their own fields. |
| * |
| * <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> |
| * |
| * @checker_framework.manual #type-refinement-purity Side effects, determinism, purity, and |
| * flow-sensitive analysis |
| * @author Stefan Heule |
| */ |
| @Documented |
| @Retention(RetentionPolicy.RUNTIME) |
| @Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) |
| public @interface Deterministic {} |