| package org.checkerframework.dataflow.analysis; |
| |
| import org.checkerframework.dataflow.cfg.visualize.CFGVisualizer; |
| import org.checkerframework.dataflow.expression.JavaExpression; |
| |
| /** |
| * A store is used to keep track of the information that the org.checkerframework.dataflow analysis |
| * has accumulated at any given point in time. |
| * |
| * @param <S> the type of the store returned by {@code copy} and that is used in {@code |
| * leastUpperBound}. Usually it is the implementing class itself, e.g. in {@code T extends |
| * Store<T>}. |
| */ |
| public interface Store<S extends Store<S>> { |
| |
| // We maintain a then store and an else store before each basic block. |
| // When they are identical (by reference equality), they can be treated |
| // as a regular unconditional store. |
| // Once we have some information for both the then and else store, we |
| // create a TransferInput for the block and allow it to be analyzed. |
| public static enum Kind { |
| THEN, |
| ELSE, |
| BOTH |
| } |
| |
| /** A flow rule describes how stores flow along one edge between basic blocks. */ |
| public static enum FlowRule { |
| /** |
| * The normal case: then store flows to the then store, and else store flows to the else store. |
| */ |
| EACH_TO_EACH, |
| /** Then store flows to both then and else of successor. */ |
| THEN_TO_BOTH, |
| /** Else store flows to both then and else of successor. */ |
| ELSE_TO_BOTH, |
| /** Then store flows to the then of successor. Else store is ignored. */ |
| THEN_TO_THEN, |
| /** Else store flows to the else of successor. Then store is ignored. */ |
| ELSE_TO_ELSE, |
| /** Both stores flow to the then of successor. */ |
| BOTH_TO_THEN, |
| /** Both stores flow to the else of successor. */ |
| BOTH_TO_ELSE, |
| } |
| |
| /** |
| * Returns an exact copy of this store. |
| * |
| * @return an exact copy of this store |
| */ |
| S copy(); |
| |
| /** |
| * Compute the least upper bound of two stores. |
| * |
| * <p><em>Important</em>: This method must fulfill the following contract: |
| * |
| * <ul> |
| * <li>Does not change {@code this}. |
| * <li>Does not change {@code other}. |
| * <li>Returns a fresh object which is not aliased yet. |
| * <li>Returns an object of the same (dynamic) type as {@code this}, even if the signature is |
| * more permissive. |
| * <li>Is commutative. |
| * </ul> |
| */ |
| S leastUpperBound(S other); |
| |
| /** |
| * Compute an upper bound of two stores that is wider than the least upper bound of the two |
| * stores. Used to jump to a higher abstraction to allow faster termination of the fixed point |
| * computations in {@link Analysis}. {@code previous} must be the previous store. |
| * |
| * <p>A particular analysis might not require widening and should implement this method by calling |
| * leastUpperBound. |
| * |
| * <p><em>Important</em>: This method must fulfill the following contract: |
| * |
| * <ul> |
| * <li>Does not change {@code this}. |
| * <li>Does not change {@code previous}. |
| * <li>Returns a fresh object which is not aliased yet. |
| * <li>Returns an object of the same (dynamic) type as {@code this}, even if the signature is |
| * more permissive. |
| * <li>Is commutative. |
| * </ul> |
| * |
| * @param previous must be the previous store |
| */ |
| S widenedUpperBound(S previous); |
| |
| /** |
| * Can the objects {@code a} and {@code b} be aliases? Returns a conservative answer (i.e., |
| * returns {@code true} if not enough information is available to determine aliasing). |
| */ |
| boolean canAlias(JavaExpression a, JavaExpression b); |
| |
| /** |
| * Delegate visualization responsibility to a visualizer. |
| * |
| * @param viz the visualizer to visualize this store |
| * @return the String representation of this store |
| */ |
| String visualize(CFGVisualizer<?, S, ?> viz); |
| } |