diff options
Diffstat (limited to 'third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual')
5 files changed, 125 insertions, 171 deletions
diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/Deterministic.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/Deterministic.java index e79543fbb1..7e7d8b9cdc 100644 --- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/Deterministic.java +++ b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/Deterministic.java @@ -7,88 +7,81 @@ 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: + * 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; - } - </code> -</pre> + * <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 <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> + * 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. * - * 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> + * <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. * - * 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> + * <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. * - * @checker_framework.manual #type-refinement-purity Side effects, determinism, purity, and flow-sensitive analysis + * <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 { -} +@Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) +public @interface Deterministic {} diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/LockingFree.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/LockingFree.java deleted file mode 100644 index a210c1a857..0000000000 --- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/LockingFree.java +++ /dev/null @@ -1,19 +0,0 @@ -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; - -/** - * Behaves identically to @SideEffectFree when running the Lock Checker. - * Ignored by all other checkers. - * - * @see SideEffectFree - */ -@Documented -@Retention(RetentionPolicy.RUNTIME) -@Target({ ElementType.METHOD, ElementType.CONSTRUCTOR }) -public @interface LockingFree { -} diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/Pure.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/Pure.java index a559c1db27..5a00db7a1b 100644 --- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/Pure.java +++ b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/Pure.java @@ -7,31 +7,24 @@ import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; /** - * {@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}. - * - * @checker_framework.manual #type-refinement-purity Side effects, determinism, purity, and flow-sensitive analysis + * {@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}. * + * @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 }) +@Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) public @interface Pure { - /** - * The type of purity. - */ + /** The type of purity. */ public static enum Kind { /** The method has no visible side-effects. */ SIDE_EFFECT_FREE, - /** - * The method returns exactly the same value when called in the same - * environment. - */ + /** The method returns exactly the same value when called in the same environment. */ DETERMINISTIC } } diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/SideEffectFree.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/SideEffectFree.java index 0521113bab..6a969c4364 100644 --- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/SideEffectFree.java +++ b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/SideEffectFree.java @@ -7,57 +7,48 @@ import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; /** - * A method is called <em>side-effect-free</em> if it has no visible - * side-effects, such as setting a field of an object that existed before - * the method was called. - * <p> - * Only the visible side-effects are important. The method is allowed to cache - * the answer to a computationally expensive query, for instance. It is also - * allowed to modify newly-created objects, and a constructor is - * side-effect-free if it does not modify any objects that existed before - * it was called. - * <p> - * This annotation is important to pluggable type-checking because if some - * fact about an object is known before a call to such a method, then the - * fact is still known afterwards, even if the fact is about some non-final - * field. When any non-<tt>@SideEffectFree</tt> method is called, then a - * pluggable type-checker must assume that any field of any accessible - * object might have been 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> - * 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 - * <tt>@SideEffectFree</tt> annotation. - * The Checker Framework issues a warning - * if the method uses any of the following Java constructs: + * A method is called <em>side-effect-free</em> if it has no visible side-effects, such as setting a + * field of an object that existed before the method was called. + * + * <p>Only the visible side-effects are important. The method is allowed to cache the answer to a + * computationally expensive query, for instance. It is also allowed to modify newly-created + * objects, and a constructor is side-effect-free if it does not modify any objects that existed + * before it was called. + * + * <p>This annotation is important to pluggable type-checking because if some fact about an object + * is known before a call to such a method, then the fact is still known afterwards, even if the + * fact is about some non-final field. When any non-{@code @SideEffectFree} method is called, then a + * pluggable type-checker must assume that any field of any accessible object might have been + * 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>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 + * {@code @SideEffectFree} 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 <tt>@SideEffectFree</tt>. - * <li>Construction of a new object where the constructor is not <tt>@SideEffectFree</tt>. + * <li>Assignment to any expression, except for local variables and method parameters. + * <li>A method invocation of a method that is not {@code @SideEffectFree}. + * <li>Construction of a new object where the constructor is not {@code @SideEffectFree}. * </ol> - * These rules are conservative: any code that passes the checks is - * side-effect-free, but the Checker Framework may issue false positive - * warnings, for code that uses one of the forbidden constructs but is - * side-effect-free nonetheless. In particular, a method that caches its - * result will be rejected. - * <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> + * These rules are conservative: any code that passes the checks is side-effect-free, but the + * Checker Framework may issue false positive warnings, for code that uses one of the forbidden + * constructs but is side-effect-free nonetheless. In particular, a method that caches its result + * will be rejected. + * + * <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. * - * @checker_framework.manual #type-refinement-purity Side effects, determinism, purity, and flow-sensitive analysis + * <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 SideEffectFree { -} +@Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) +public @interface SideEffectFree {} diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/TerminatesExecution.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/TerminatesExecution.java index 93ff95c546..4e83dcdb64 100644 --- a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/TerminatesExecution.java +++ b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/qual/TerminatesExecution.java @@ -7,32 +7,28 @@ import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; /** - * {@code TerminatesExecution} is a method annotation that indicates that a - * method terminates the execution of the program. This can be used to - * annotate methods such as {@code System.exit()}. - * <p> - - * The annotation enables flow-sensitive type refinement to be more - * precise. For example, after + * {@code TerminatesExecution} is a method annotation that indicates that a method terminates the + * execution of the program. This can be used to annotate methods such as {@code System.exit()}. + * + * <p>The annotation enables flow-sensitive type refinement to be more precise. For example, after + * * <pre> * if (x == null) { * System.err.println("Bad value supplied"); * System.exit(1); * } * </pre> - * the Nullness Checker can determine that <tt>x</tt> is non-null. - * - * <p> - * The annotation is a <em>trusted</em> annotation, meaning that it is not - * checked whether the annotated method really does terminate the program. - * - * @checker_framework.manual #type-refinement Automatic type refinement (flow-sensitive type qualifier inference) * + * the Nullness Checker can determine that {@code x} is non-null. + * + * <p>The annotation is a <em>trusted</em> annotation, meaning that it is not checked whether the + * annotated method really does terminate the program. + * + * @checker_framework.manual #type-refinement Automatic type refinement (flow-sensitive type + * qualifier inference) * @author Stefan Heule - * */ @Documented @Retention(RetentionPolicy.RUNTIME) -@Target({ ElementType.METHOD, ElementType.CONSTRUCTOR }) -public @interface TerminatesExecution { -} +@Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) +public @interface TerminatesExecution {} |