| package org.checkerframework.dataflow.analysis; |
| |
| import java.util.Map; |
| import java.util.StringJoiner; |
| import javax.lang.model.type.TypeMirror; |
| import org.checkerframework.checker.nullness.qual.Nullable; |
| import org.plumelib.util.StringsPlume; |
| |
| /** |
| * Implementation of a {@link TransferResult} with two non-exceptional stores. The 'then' store |
| * contains information valid when the previous boolean-valued expression was true, and the 'else' |
| * store contains information valid when the expression was false. |
| * |
| * <p>The result of {@code getRegularStore} will be the least upper bound of the two underlying |
| * stores. |
| * |
| * @param <V> type of the abstract value that is tracked |
| * @param <S> the store type used in the analysis |
| */ |
| public class ConditionalTransferResult<V extends AbstractValue<V>, S extends Store<S>> |
| extends TransferResult<V, S> { |
| |
| /** Whether the store changed. */ |
| private final boolean storeChanged; |
| |
| /** The 'then' result store. */ |
| protected final S thenStore; |
| |
| /** The 'else' result store. */ |
| protected final S elseStore; |
| |
| /** |
| * Create a new {@link #ConditionalTransferResult(AbstractValue, Store, Store, Map, boolean)}, |
| * using {@code null} for {@link #exceptionalStores}. |
| * |
| * <p><em>Exceptions</em>: If the corresponding {@link |
| * org.checkerframework.dataflow.cfg.node.Node} throws an exception, then it is assumed that no |
| * special handling is necessary and the store before the corresponding {@link |
| * org.checkerframework.dataflow.cfg.node.Node} will be passed along any exceptional edge. |
| * |
| * <p><em>Aliasing</em>: {@code thenStore} and {@code elseStore} are not allowed to be used |
| * anywhere outside of this class (including use through aliases). Complete control over the |
| * objects is transferred to this class. |
| * |
| * @param value the abstract value produced by the transfer function |
| * @param thenStore 'then' result store |
| * @param elseStore 'else' result store |
| * @param storeChanged whether the store changed |
| * @see #ConditionalTransferResult(AbstractValue, Store, Store, Map, boolean) |
| */ |
| public ConditionalTransferResult( |
| @Nullable V value, S thenStore, S elseStore, boolean storeChanged) { |
| this(value, thenStore, elseStore, null, storeChanged); |
| } |
| |
| /** |
| * Create a new {@link #ConditionalTransferResult(AbstractValue, Store, Store, Map, boolean)}, |
| * using {@code false} for whether the store changed and {@code null} for {@link |
| * #exceptionalStores}. |
| * |
| * @param value the abstract value produced by the transfer function |
| * @param thenStore {@link #thenStore} |
| * @param elseStore {@link #elseStore} |
| * @see #ConditionalTransferResult(AbstractValue, Store, Store, Map, boolean) |
| */ |
| public ConditionalTransferResult(@Nullable V value, S thenStore, S elseStore) { |
| this(value, thenStore, elseStore, false); |
| } |
| |
| /** |
| * Create a new {@link #ConditionalTransferResult(AbstractValue, Store, Store, Map, boolean)}, |
| * using {@code false} for the {@code storeChanged} formal parameter. |
| * |
| * @param value the abstract value produced by the transfer function |
| * @param thenStore {@link #thenStore} |
| * @param elseStore {@link #elseStore} |
| * @param exceptionalStores {@link #exceptionalStores} |
| * @see #ConditionalTransferResult(AbstractValue, Store, Store, Map, boolean) |
| */ |
| public ConditionalTransferResult( |
| V value, S thenStore, S elseStore, Map<TypeMirror, S> exceptionalStores) { |
| this(value, thenStore, elseStore, exceptionalStores, false); |
| } |
| |
| /** |
| * Create a {@code ConditionalTransferResult} with {@code thenStore} as the resulting store if the |
| * corresponding {@link org.checkerframework.dataflow.cfg.node.Node} evaluates to {@code true} and |
| * {@code elseStore} otherwise. |
| * |
| * <p><em>Exceptions</em>: If the corresponding {@link |
| * org.checkerframework.dataflow.cfg.node.Node} throws an exception, then the corresponding store |
| * in {@code exceptionalStores} is used. If no exception is found in {@code exceptionalStores}, |
| * then it is assumed that no special handling is necessary and the store before the corresponding |
| * {@link org.checkerframework.dataflow.cfg.node.Node} will be passed along any exceptional edge. |
| * |
| * <p><em>Aliasing</em>: {@code thenStore}, {@code elseStore}, and any store in {@code |
| * exceptionalStores} are not allowed to be used anywhere outside of this class (including use |
| * through aliases). Complete control over the objects is transferred to this class. |
| * |
| * @param value the abstract value produced by the transfer function |
| * @param thenStore {@link #thenStore} |
| * @param elseStore {@link #elseStore} |
| * @param exceptionalStores {@link #exceptionalStores} |
| * @param storeChanged whether the store changed; see {@link |
| * org.checkerframework.dataflow.analysis.TransferResult#storeChanged}. |
| */ |
| public ConditionalTransferResult( |
| @Nullable V value, |
| S thenStore, |
| S elseStore, |
| @Nullable Map<TypeMirror, S> exceptionalStores, |
| boolean storeChanged) { |
| super(value, exceptionalStores); |
| this.thenStore = thenStore; |
| this.elseStore = elseStore; |
| this.storeChanged = storeChanged; |
| } |
| |
| /** The regular result store. */ |
| @Override |
| public S getRegularStore() { |
| return thenStore.leastUpperBound(elseStore); |
| } |
| |
| @Override |
| public S getThenStore() { |
| return thenStore; |
| } |
| |
| @Override |
| public S getElseStore() { |
| return elseStore; |
| } |
| |
| @Override |
| public boolean containsTwoStores() { |
| return true; |
| } |
| |
| @Override |
| public String toString() { |
| StringJoiner result = new StringJoiner(System.lineSeparator()); |
| result.add("RegularTransferResult("); |
| result.add(" resultValue = " + StringsPlume.indentLinesExceptFirst(2, resultValue)); |
| result.add(" thenStore = " + StringsPlume.indentLinesExceptFirst(2, thenStore)); |
| result.add(" elseStore = " + StringsPlume.indentLinesExceptFirst(2, elseStore)); |
| result.add(")"); |
| return result.toString(); |
| } |
| |
| @Override |
| public boolean storeChanged() { |
| return storeChanged; |
| } |
| } |