| package org.checkerframework.framework.util; |
| |
| import com.sun.source.tree.Tree; |
| import java.lang.annotation.Annotation; |
| import java.util.Objects; |
| import javax.lang.model.element.AnnotationMirror; |
| import org.checkerframework.checker.nullness.qual.Nullable; |
| import org.checkerframework.dataflow.expression.JavaExpression; |
| import org.checkerframework.framework.qual.ConditionalPostconditionAnnotation; |
| import org.checkerframework.framework.qual.EnsuresQualifier; |
| import org.checkerframework.framework.qual.EnsuresQualifierIf; |
| import org.checkerframework.framework.qual.PostconditionAnnotation; |
| import org.checkerframework.framework.qual.PreconditionAnnotation; |
| import org.checkerframework.framework.qual.RequiresQualifier; |
| import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; |
| import org.checkerframework.framework.util.dependenttypes.DependentTypesHelper; |
| import org.checkerframework.javacutil.BugInCF; |
| |
| /** |
| * A contract represents an annotation on an expression. It is a precondition, postcondition, or |
| * conditional postcondition. |
| * |
| * @see Precondition |
| * @see Postcondition |
| * @see ConditionalPostcondition |
| */ |
| public abstract class Contract { |
| |
| /** |
| * The expression for which the condition must hold, such as {@code "foo"} in |
| * {@code @RequiresNonNull("foo")}. |
| * |
| * <p>An annotation like {@code @RequiresNonNull({"a", "b", "c"})} would be represented by |
| * multiple Contracts. |
| */ |
| public final String expressionString; |
| |
| /** The annotation on the type of expression, according to this contract. */ |
| public final AnnotationMirror annotation; |
| |
| /** The annotation that expressed this contract; used for diagnostic messages. */ |
| public final AnnotationMirror contractAnnotation; |
| |
| // This is redundant with the contract's class and is not used in this file, but the field |
| // is used by clients, for its fields. |
| /** The kind of contract: precondition, postcondition, or conditional postcondition. */ |
| public final Kind kind; |
| |
| /** Enumerates the kinds of contracts. */ |
| public enum Kind { |
| /** A precondition. */ |
| PRECONDITION( |
| "precondition", |
| PreconditionAnnotation.class, |
| RequiresQualifier.class, |
| RequiresQualifier.List.class), |
| /** A postcondition. */ |
| POSTCONDITION( |
| "postcondition", |
| PostconditionAnnotation.class, |
| EnsuresQualifier.class, |
| EnsuresQualifier.List.class), |
| /** A conditional postcondition. */ |
| CONDITIONALPOSTCONDITION( |
| "conditional postcondition", |
| ConditionalPostconditionAnnotation.class, |
| EnsuresQualifierIf.class, |
| EnsuresQualifierIf.List.class); |
| |
| /** Used for constructing error messages. */ |
| public final String errorKey; |
| |
| /** The meta-annotation identifying annotations of this kind. */ |
| public final Class<? extends Annotation> metaAnnotation; |
| /** The built-in framework qualifier for this contract. */ |
| public final Class<? extends Annotation> frameworkContractClass; |
| /** The built-in framework qualifier for repeated occurrences of this contract. */ |
| public final Class<? extends Annotation> frameworkContractListClass; |
| |
| /** |
| * Create a new Kind. |
| * |
| * @param errorKey used for constructing error messages |
| * @param metaAnnotation the meta-annotation identifying annotations of this kind |
| * @param frameworkContractClass the built-in framework qualifier for this contract |
| * @param frameworkContractListClass the built-in framework qualifier for repeated occurrences |
| * of this contract |
| */ |
| Kind( |
| String errorKey, |
| Class<? extends Annotation> metaAnnotation, |
| Class<? extends Annotation> frameworkContractClass, |
| Class<? extends Annotation> frameworkContractListClass) { |
| this.errorKey = errorKey; |
| this.metaAnnotation = metaAnnotation; |
| this.frameworkContractClass = frameworkContractClass; |
| this.frameworkContractListClass = frameworkContractListClass; |
| } |
| } |
| |
| /** |
| * Creates a new Contract. This should be called only by the constructors for {@link |
| * Precondition}, {@link Postcondition}, and {@link ConditionalPostcondition}. |
| * |
| * @param kind precondition, postcondition, or conditional postcondition |
| * @param expressionString the Java expression that should have a type qualifier |
| * @param annotation the type qualifier that {@code expressionString} should have |
| * @param contractAnnotation the pre- or post-condition annotation that the programmer wrote; used |
| * for diagnostic messages |
| */ |
| private Contract( |
| Kind kind, |
| String expressionString, |
| AnnotationMirror annotation, |
| AnnotationMirror contractAnnotation) { |
| this.expressionString = expressionString; |
| this.annotation = annotation; |
| this.contractAnnotation = contractAnnotation; |
| this.kind = kind; |
| } |
| |
| /** |
| * Creates a new Contract. |
| * |
| * @param kind precondition, postcondition, or conditional postcondition |
| * @param expressionString the Java expression that should have a type qualifier |
| * @param annotation the type qualifier that {@code expressionString} should have |
| * @param contractAnnotation the pre- or post-condition annotation that the programmer wrote; used |
| * for diagnostic messages |
| * @param ensuresQualifierIf the ensuresQualifierIf field, for a conditional postcondition |
| * @return a new contract |
| */ |
| public static Contract create( |
| Kind kind, |
| String expressionString, |
| AnnotationMirror annotation, |
| AnnotationMirror contractAnnotation, |
| Boolean ensuresQualifierIf) { |
| if ((ensuresQualifierIf != null) != (kind == Kind.CONDITIONALPOSTCONDITION)) { |
| throw new BugInCF( |
| "Mismatch: Contract.create(%s, %s, %s, %s, %s)", |
| kind, expressionString, annotation, contractAnnotation, ensuresQualifierIf); |
| } |
| switch (kind) { |
| case PRECONDITION: |
| return new Precondition(expressionString, annotation, contractAnnotation); |
| case POSTCONDITION: |
| return new Postcondition(expressionString, annotation, contractAnnotation); |
| case CONDITIONALPOSTCONDITION: |
| return new ConditionalPostcondition( |
| expressionString, annotation, contractAnnotation, ensuresQualifierIf); |
| default: |
| throw new BugInCF("Unrecognized kind: " + kind); |
| } |
| } |
| |
| // Note that equality requires exact match of the run-time class and that it ignores the |
| // `contractAnnotation` field. |
| @Override |
| public boolean equals(@Nullable Object o) { |
| if (this == o) { |
| return true; |
| } |
| if (o == null) { |
| return false; |
| } |
| if (getClass() != o.getClass()) { |
| return false; |
| } |
| |
| Contract otherContract = (Contract) o; |
| |
| return kind == otherContract.kind |
| && Objects.equals(expressionString, otherContract.expressionString) |
| && Objects.equals(annotation, otherContract.annotation); |
| } |
| |
| @Override |
| public int hashCode() { |
| return Objects.hash(kind, expressionString, annotation); |
| } |
| |
| @Override |
| public String toString() { |
| return String.format( |
| "%s{expressionString=%s, annotation=%s, contractAnnotation=%s}", |
| getClass().getSimpleName(), expressionString, annotation, contractAnnotation); |
| } |
| |
| /** |
| * Viewpoint-adapt {@link #annotation} using {@code stringToJavaExpr}. |
| * |
| * <p>For example, if the contract is {@code @EnsuresKeyFor(value = "this.field", map = "map")}, |
| * {@code annotation} is {@code @KeyFor("map")}. This method applies {@code stringToJava} to "map" |
| * and returns a new {@code KeyFor} annotation with the result. |
| * |
| * @param factory used to get {@link DependentTypesHelper} |
| * @param stringToJavaExpr function used to convert strings to {@link JavaExpression}s |
| * @param errorTree if non-null, where to report any errors that occur when parsing the dependent |
| * type annotation; if null, report no errors |
| * @return the viewpoint-adapted annotation, or {@link #annotation} if it is not a dependent type |
| * annotation |
| */ |
| public AnnotationMirror viewpointAdaptDependentTypeAnnotation( |
| GenericAnnotatedTypeFactory<?, ?, ?, ?> factory, |
| StringToJavaExpression stringToJavaExpr, |
| @Nullable Tree errorTree) { |
| DependentTypesHelper dependentTypesHelper = factory.getDependentTypesHelper(); |
| AnnotationMirror standardized = |
| dependentTypesHelper.convertAnnotationMirror(stringToJavaExpr, annotation); |
| if (standardized == null) { |
| return annotation; |
| } |
| if (errorTree != null) { |
| dependentTypesHelper.checkAnnotationForErrorExpressions(standardized, errorTree); |
| } |
| return standardized; |
| } |
| |
| /** A precondition contract. */ |
| public static class Precondition extends Contract { |
| /** |
| * Create a precondition contract. |
| * |
| * @param expressionString the Java expression that should have a type qualifier |
| * @param annotation the type qualifier that {@code expressionString} should have |
| * @param contractAnnotation the precondition annotation that the programmer wrote; used for |
| * diagnostic messages |
| */ |
| public Precondition( |
| String expressionString, AnnotationMirror annotation, AnnotationMirror contractAnnotation) { |
| super(Kind.PRECONDITION, expressionString, annotation, contractAnnotation); |
| } |
| } |
| |
| /** A postcondition contract. */ |
| public static class Postcondition extends Contract { |
| /** |
| * Create a postcondition contract. |
| * |
| * @param expressionString the Java expression that should have a type qualifier |
| * @param annotation the type qualifier that {@code expressionString} should have |
| * @param contractAnnotation the postcondition annotation that the programmer wrote; used for |
| * diagnostic messages |
| */ |
| public Postcondition( |
| String expressionString, AnnotationMirror annotation, AnnotationMirror contractAnnotation) { |
| super(Kind.POSTCONDITION, expressionString, annotation, contractAnnotation); |
| } |
| } |
| |
| /** |
| * Represents a conditional postcondition that must be verified by {@code BaseTypeVisitor} or one |
| * of its subclasses. Automatically extracted from annotations with meta-annotation |
| * {@code @ConditionalPostconditionAnnotation}, such as {@code EnsuresNonNullIf}. |
| */ |
| public static class ConditionalPostcondition extends Contract { |
| |
| /** |
| * The return value for the annotated method that ensures that the conditional postcondition |
| * holds. For example, given |
| * |
| * <pre> |
| * {@code @EnsuresNonNullIf(expression="foo", result=false) boolean method()} |
| * </pre> |
| * |
| * {@code foo} is guaranteed to be {@code @NonNull} after a call to {@code method()} that |
| * returns {@code false}. |
| */ |
| public final boolean resultValue; |
| |
| /** |
| * Create a new conditional postcondition. |
| * |
| * @param expressionString the Java expression that should have a type qualifier |
| * @param annotation the type qualifier that {@code expressionString} should have |
| * @param contractAnnotation the postcondition annotation that the programmer wrote; used for |
| * diagnostic messages |
| * @param resultValue whether the condition is the method returning true or false |
| */ |
| public ConditionalPostcondition( |
| String expressionString, |
| AnnotationMirror annotation, |
| AnnotationMirror contractAnnotation, |
| boolean resultValue) { |
| super(Kind.CONDITIONALPOSTCONDITION, expressionString, annotation, contractAnnotation); |
| this.resultValue = resultValue; |
| } |
| |
| @Override |
| public boolean equals(@Nullable Object o) { |
| return super.equals(o) && resultValue == ((ConditionalPostcondition) o).resultValue; |
| } |
| |
| @Override |
| public int hashCode() { |
| return Objects.hash(super.hashCode(), resultValue); |
| } |
| |
| @Override |
| public String toString() { |
| String superToString = super.toString(); |
| return superToString.substring(0, superToString.length() - 1) |
| + ", annoResult=" |
| + resultValue |
| + "}"; |
| } |
| } |
| } |