| package org.checkerframework.common.wholeprograminference; |
| |
| import com.sun.source.tree.ClassTree; |
| import javax.lang.model.element.AnnotationMirror; |
| import javax.lang.model.element.Element; |
| import javax.lang.model.element.ExecutableElement; |
| import javax.lang.model.element.VariableElement; |
| import javax.lang.model.type.TypeMirror; |
| import org.checkerframework.common.basetype.BaseTypeChecker; |
| import org.checkerframework.dataflow.analysis.Analysis; |
| import org.checkerframework.framework.qual.TypeUseLocation; |
| import org.checkerframework.framework.type.AnnotatedTypeFactory; |
| import org.checkerframework.framework.type.AnnotatedTypeMirror; |
| |
| /** |
| * Stores annotations from whole-program inference. For a given location such as a field or method, |
| * an object can be obtained containing the inferred annotations for that object. |
| * |
| * <p>Also writes stored annotations to storage files. The specific format depends on the |
| * implementation. |
| * |
| * @param <T> the type used by the storage to store annotations. The methods {@link |
| * #atmFromStorageLocation} and {@link #updateStorageLocationFromAtm} can be used to manipulate |
| * a storage location. |
| */ |
| public interface WholeProgramInferenceStorage<T> { |
| /** |
| * Returns the file corresponding to the given element. This may side-effect the storage to load |
| * the file if it hasn't been read yet. |
| * |
| * @param elt an element |
| * @return the path to the file where inference results for the element will be written |
| */ |
| public String getFileForElement(Element elt); |
| |
| /** |
| * Given an ExecutableElement in a compilation unit that has already been read into storage, |
| * returns whether there exists a stored method matching {@code elt}. |
| * |
| * <p>An implementation is permitted to return false if {@code elt} represents a method that was |
| * synthetically added by javac, such as zero-argument constructors or valueOf(String) methods for |
| * enum types. |
| * |
| * @param methodElt a method or constructor Element |
| * @return true if the storage has a method corresponding to {@code elt} |
| */ |
| public boolean hasStorageLocationForMethod(ExecutableElement methodElt); |
| |
| /** |
| * Get the annotations for a formal parameter type. |
| * |
| * @param methodElt the method or constructor Element |
| * @param i the parameter index (0-based) |
| * @param paramATM the parameter type |
| * @param ve the parameter variable |
| * @param atypeFactory the type factory |
| * @return the annotations for a formal parameter type |
| */ |
| public T getParameterAnnotations( |
| ExecutableElement methodElt, |
| int i, |
| AnnotatedTypeMirror paramATM, |
| VariableElement ve, |
| AnnotatedTypeFactory atypeFactory); |
| |
| /** |
| * Get the annotations for the receiver type. |
| * |
| * @param methodElt the method or constructor Element |
| * @param paramATM the receiver type |
| * @param atypeFactory the type factory |
| * @return the annotations for the receiver type |
| */ |
| public T getReceiverAnnotations( |
| ExecutableElement methodElt, AnnotatedTypeMirror paramATM, AnnotatedTypeFactory atypeFactory); |
| |
| /** |
| * Get the annotations for the return type. |
| * |
| * @param methodElt the method or constructor Element |
| * @param atm the return type |
| * @param atypeFactory the type factory |
| * @return the annotations for the return type |
| */ |
| public T getReturnAnnotations( |
| ExecutableElement methodElt, AnnotatedTypeMirror atm, AnnotatedTypeFactory atypeFactory); |
| |
| /** |
| * Get the annotations for a field type. |
| * |
| * @param element the element for the field |
| * @param fieldName the simple field name |
| * @param lhsATM the field type |
| * @param atypeFactory the annotated type factory |
| * @return the annotations for a field type |
| */ |
| public T getFieldAnnotations( |
| Element element, |
| String fieldName, |
| AnnotatedTypeMirror lhsATM, |
| AnnotatedTypeFactory atypeFactory); |
| |
| // Fields are special because currently WPI computes preconditions for fields only, not for |
| // other expressions. |
| /** |
| * Returns the pre- or postcondition annotations for a field. |
| * |
| * @param preOrPost whether to get the precondition or postcondition |
| * @param methodElement the method |
| * @param fieldElement the field |
| * @param atypeFactory the type factory |
| * @return the pre- or postcondition annotations for a field |
| */ |
| public T getPreOrPostconditionsForField( |
| Analysis.BeforeOrAfter preOrPost, |
| ExecutableElement methodElement, |
| VariableElement fieldElement, |
| AnnotatedTypeFactory atypeFactory); |
| |
| /** |
| * Updates a method to add a declaration annotation. |
| * |
| * @param methodElt the method to annotate |
| * @param anno the declaration annotation to add to the method |
| * @return true if {@code anno} is a new declaration annotation for {@code methodElt}, false |
| * otherwise |
| */ |
| public boolean addMethodDeclarationAnnotation(ExecutableElement methodElt, AnnotationMirror anno); |
| |
| /** |
| * Obtain the type from a storage location. |
| * |
| * @param typeMirror the underlying type for the result |
| * @param storageLocation the storage location from which to obtain annotations |
| * @return an annotated type mirror with underlying type {@code typeMirror} and annotations from |
| * {@code storageLocation} |
| */ |
| public AnnotatedTypeMirror atmFromStorageLocation(TypeMirror typeMirror, T storageLocation); |
| |
| /** |
| * Updates a storage location to have the annotations of the given {@code AnnotatedTypeMirror}. |
| * Annotations in the original set that should be ignored are not added to the resulting set. If |
| * {@code ignoreIfAnnotated} is true, doesn't add annotations for locations with explicit |
| * annotations in source code. |
| * |
| * <p>This method removes from the storage location all annotations supported by the |
| * AnnotatedTypeFactory before inserting new ones. It is assumed that every time this method is |
| * called, the new {@code AnnotatedTypeMirror} has a better type estimate for the given location. |
| * Therefore, it is not a problem to remove all annotations before inserting the new annotations. |
| * |
| * <p>The {@code update*} methods in {@link WholeProgramInference} perform LUB. This one just does |
| * replacement. (Thus, the naming may be a bit confusing.) |
| * |
| * @param newATM the type whose annotations will be added to the {@code AnnotatedTypeMirror} |
| * @param curATM the annotations currently stored at the location, used to check if the element |
| * that will be updated has explicit annotations in source code |
| * @param storageLocationToUpdate the storage location that will be updated |
| * @param defLoc the location where the annotation will be added |
| * @param ignoreIfAnnotated if true, don't update any type that is explicitly annotated in the |
| * source code |
| */ |
| public void updateStorageLocationFromAtm( |
| AnnotatedTypeMirror newATM, |
| AnnotatedTypeMirror curATM, |
| T storageLocationToUpdate, |
| TypeUseLocation defLoc, |
| boolean ignoreIfAnnotated); |
| |
| /** |
| * Writes the inferred results to a file. Ideally, it should be called at the end of the |
| * type-checking process. In practice, it is called after each class, because we don't know which |
| * class will be the last one in the type-checking process. |
| * |
| * @param outputFormat the file format in which to write the results |
| * @param checker the checker from which this method is called, for naming stub files |
| */ |
| public void writeResultsToFile( |
| WholeProgramInference.OutputFormat outputFormat, BaseTypeChecker checker); |
| |
| /** |
| * Indicates that inferred annotations for the file at {@code path} have changed since last |
| * written. This causes output files for {@code path} to be written out next time {@link |
| * #writeResultsToFile} is called. |
| * |
| * @param path path to the file with annotations that have been modified |
| */ |
| public void setFileModified(String path); |
| |
| /** |
| * Performs any preparation required for inference on the elements of a class. Should be called on |
| * each top-level class declaration in a compilation unit before processing it. |
| * |
| * @param classTree the class to preprocess |
| */ |
| void preprocessClassTree(ClassTree classTree); |
| } |