| package org.checkerframework.dataflow.analysis; |
| |
| /*>>> |
| import org.checkerframework.checker.nullness.qual.Nullable; |
| */ |
| |
| import java.util.Map; |
| import javax.lang.model.type.TypeMirror; |
| |
| /** |
| * {@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 store in {@code TransferResult}. |
| * |
| * <p>A {@code TransferResult} contains one or two stores (for 'then' and 'else'), and zero or more |
| * stores with a cause ({@link TypeMirror}). |
| * |
| * @author Stefan Heule |
| * @param <S> the {@link Store} used to keep track of intermediate results |
| */ |
| public abstract class TransferResult<A extends AbstractValue<A>, S extends Store<S>> { |
| |
| /** |
| * 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 /*@Nullable*/ Map<TypeMirror, S> exceptionalStores; |
| |
| /** |
| * 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*/ A resultValue; |
| |
| public TransferResult(/*@Nullable*/ A resultValue) { |
| this.resultValue = resultValue; |
| } |
| |
| /** @return the abstract value produced by the transfer function */ |
| public A getResultValue() { |
| return resultValue; |
| } |
| |
| public void setResultValue(A resultValue) { |
| this.resultValue = resultValue; |
| } |
| |
| /** |
| * @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(); |
| |
| /** |
| * @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(); |
| |
| /** |
| * @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(); |
| |
| /** |
| * @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); |
| } |
| |
| /** |
| * @return a Map of {@link TypeMirror} to {@link Store} |
| * @see TransferResult#getExceptionalStore(TypeMirror) |
| */ |
| public Map<TypeMirror, S> getExceptionalStores() { |
| return exceptionalStores; |
| } |
| |
| /** |
| * @return {@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. |
| */ |
| public abstract boolean containsTwoStores(); |
| |
| /** |
| * @return {@code true} if and only if the transfer function returning this transfer result |
| * changed the regularStore, elseStore, or thenStore. |
| */ |
| public abstract boolean storeChanged(); |
| } |