| package org.checkerframework.dataflow.analysis; |
| |
| import java.util.Map; |
| import javax.lang.model.type.TypeMirror; |
| import org.checkerframework.checker.nullness.qual.Nullable; |
| |
| /** |
| * {@code TransferResult} is used as the result type of the individual transfer functions of a |
| * {@link TransferFunction}. It always belongs to the result of the individual transfer function for |
| * a particular {@link org.checkerframework.dataflow.cfg.node.Node}, even though that {@code |
| * org.checkerframework.dataflow.cfg.node.Node} is not explicitly stored in {@code TransferResult}. |
| * |
| * <p>A {@code TransferResult} consists of a result value, plus one or more stores. It contains one |
| * or two stores (for 'then' and 'else'), and zero or more stores with a cause ({@link TypeMirror}). |
| * |
| * @param <V> type of the abstract value that is tracked |
| * @param <S> the store type used in the analysis |
| */ |
| public abstract class TransferResult<V extends AbstractValue<V>, S extends Store<S>> { |
| |
| /** |
| * The abstract value of the {@link org.checkerframework.dataflow.cfg.node.Node} associated with |
| * this {@link TransferResult}, or {@code null} if no value has been produced. |
| */ |
| protected @Nullable V resultValue; |
| |
| /** |
| * The stores in case the basic block throws an exception (or {@code null} if the corresponding |
| * {@link org.checkerframework.dataflow.cfg.node.Node} does not throw any exceptions). Does not |
| * necessarily contain a store for every exception, in which case the in-store will be used. |
| */ |
| protected final @Nullable Map<TypeMirror, S> exceptionalStores; |
| |
| /** |
| * Create a new TransferResult, given {@link #resultValue} and {@link #exceptionalStores}. |
| * |
| * @param resultValue the abstract value of the {@link |
| * org.checkerframework.dataflow.cfg.node.Node} associated with this {@link TransferResult} |
| * @param exceptionalStores the stores in case the basic block throws an exception (or {@code |
| * null} if the corresponding {@link org.checkerframework.dataflow.cfg.node.Node} does not |
| * throw any exceptions) |
| */ |
| protected TransferResult( |
| @Nullable V resultValue, @Nullable Map<TypeMirror, S> exceptionalStores) { |
| this.resultValue = resultValue; |
| this.exceptionalStores = exceptionalStores; |
| } |
| |
| /** |
| * Returns the abstract value produced by the transfer function, {@code null} otherwise. |
| * |
| * @return the abstract value produced by the transfer function, {@code null} otherwise |
| */ |
| public @Nullable V getResultValue() { |
| return resultValue; |
| } |
| |
| /** |
| * Set the value of {@link #resultValue}. |
| * |
| * @param resultValue the abstract value of the {@link |
| * org.checkerframework.dataflow.cfg.node.Node} associated with this {@link TransferResult} |
| */ |
| public void setResultValue(V resultValue) { |
| this.resultValue = resultValue; |
| } |
| |
| /** |
| * Returns the regular result store produced if no exception is thrown by the {@link |
| * org.checkerframework.dataflow.cfg.node.Node} corresponding to this transfer function result. |
| * |
| * @return the regular result store produced if no exception is thrown by the {@link |
| * org.checkerframework.dataflow.cfg.node.Node} corresponding to this transfer function result |
| */ |
| public abstract S getRegularStore(); |
| |
| /** |
| * Returns the result store produced if the {@link org.checkerframework.dataflow.cfg.node.Node} |
| * this result belongs to evaluates to {@code true}. |
| * |
| * @return the result store produced if the {@link org.checkerframework.dataflow.cfg.node.Node} |
| * this result belongs to evaluates to {@code true} |
| */ |
| public abstract S getThenStore(); |
| |
| /** |
| * Returns the result store produced if the {@link org.checkerframework.dataflow.cfg.node.Node} |
| * this result belongs to evaluates to {@code false}. |
| * |
| * @return the result store produced if the {@link org.checkerframework.dataflow.cfg.node.Node} |
| * this result belongs to evaluates to {@code false} |
| */ |
| public abstract S getElseStore(); |
| |
| /** |
| * Returns the store that flows along the outgoing exceptional edge labeled with {@code exception} |
| * (or {@code null} if no special handling is required for exceptional edges). |
| * |
| * @param exception an exception type |
| * @return the store that flows along the outgoing exceptional edge labeled with {@code exception} |
| * (or {@code null} if no special handling is required for exceptional edges) |
| */ |
| public @Nullable S getExceptionalStore(TypeMirror exception) { |
| if (exceptionalStores == null) { |
| return null; |
| } |
| return exceptionalStores.get(exception); |
| } |
| |
| /** |
| * Returns a Map of {@link TypeMirror} to {@link Store}, {@code null} otherwise. |
| * |
| * @return a Map of {@link TypeMirror} to {@link Store}, {@code null} otherwise |
| * @see TransferResult#getExceptionalStore(TypeMirror) |
| */ |
| public @Nullable Map<TypeMirror, S> getExceptionalStores() { |
| return exceptionalStores; |
| } |
| |
| /** |
| * Returns {@code true} if and only if this transfer result contains two stores that are |
| * potentially not equal. Note that the result {@code true} does not imply that {@code |
| * getRegularStore} cannot be called (or vice versa for {@code false}). Rather, it indicates that |
| * {@code getThenStore} or {@code getElseStore} can be used to give more precise results. |
| * Otherwise, if the result is {@code false}, then all three methods {@code getRegularStore}, |
| * {@code getThenStore}, and {@code getElseStore} return equivalent stores. |
| * |
| * @return {@code true} if and only if this transfer result contains two stores that are |
| * potentially not equal |
| */ |
| public abstract boolean containsTwoStores(); |
| |
| /** |
| * Returns {@code true} if and only if the transfer function returning this transfer result |
| * changed the regularStore, elseStore, or thenStore. |
| * |
| * @return {@code true} if and only if the transfer function returning this transfer result |
| * changed the regularStore, elseStore, or thenStore |
| */ |
| public abstract boolean storeChanged(); |
| } |