| 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 <tt>==</tt>) 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> |
| * This annotation is important to pluggable type-checking because, after a |
| * call to a <tt>@Deterministic</tt> method, flow-sensitive type refinement |
| * can assume that anything learned about the first invocation is true |
| * about subsequent invocations (so long as no non-<tt>@</tt>{@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(); |
| }</code></pre> |
| * <p> |
| * Note that <tt>@Deterministic</tt> guarantees that the result is |
| * identical according to <tt>==</tt>, <b>not</b> equal according to |
| * <tt>equals</tt>. This means that writing <tt>@Deterministic</tt> on a |
| * method that returns a reference 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 |
| * <tt>@Deterministic</tt> 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; |
| } |
| </code> |
| </pre> |
| * </ol> |
| * A constructor can be <tt>@Pure</tt>, 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 |
| * <tt>-AcheckPurityAnnotations</tt> 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 { |
| } |