1 files changed, 137 insertions, 0 deletions
diff --git a/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/ConditionalTransferResult.java b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/ConditionalTransferResult.java
new file mode 100644
index 0000000000..c49357a3ff
--- /dev/null
+++ b/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/ConditionalTransferResult.java
@@ -0,0 +1,137 @@
+package org.checkerframework.dataflow.analysis;
+
+import java.util.Map;
+
+import javax.lang.model.type.TypeMirror;
+
+/**
+ * Implementation of a {@link TransferResult} with two non-exceptional store;
+ * one for the 'then' edge and one for 'else'. The result of
+ * {@code getRegularStore} will be the least upper bound of the two underlying
+ * stores.
+ *
+ * @author Stefan Heule
+ *
+ * @param <S>
+ *            The {@link Store} used to keep track of intermediate results.
+ */
+public class ConditionalTransferResult<A extends AbstractValue<A>, S extends Store<S>>
+        extends TransferResult<A, S> {
+
+    private final boolean storeChanged;
+
+    /** The 'then' result store. */
+    protected S thenStore;
+
+    /** The 'else' result store. */
+    protected S elseStore;
+
+    /**
+     * 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.
+     *
+     * For the meaning of storeChanged, see
+     * {@link org.checkerframework.dataflow.analysis.TransferResult#storeChanged}.
+     *
+     * <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 transfered to this class.
+     */
+    public ConditionalTransferResult(A value, S thenStore, S elseStore, boolean storeChanged) {
+        super(value);
+        this.thenStore = thenStore;
+        this.elseStore = elseStore;
+        this.storeChanged = storeChanged;
+    }
+
+    public ConditionalTransferResult(A value, S thenStore, S elseStore) {
+        this(value, thenStore, elseStore, 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 transfered to this class.
+     */
+    public ConditionalTransferResult(A value, S thenStore, S elseStore,
+            Map<TypeMirror, S> exceptionalStores, boolean storeChanged) {
+        super(value);
+        this.exceptionalStores = exceptionalStores;
+        this.thenStore = thenStore;
+        this.elseStore = elseStore;
+        this.storeChanged = storeChanged;
+    }
+
+    public ConditionalTransferResult(A value, S thenStore, S elseStore,
+        Map<TypeMirror, S> exceptionalStores) {
+        this(value, thenStore, elseStore, exceptionalStores, false);
+    }
+
+    @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() {
+        StringBuilder result = new StringBuilder();
+        result.append("RegularTransferResult(");
+        result.append(System.getProperty("line.separator"));
+        result.append("resultValue = " + resultValue);
+        result.append(System.getProperty("line.separator"));
+        result.append("thenStore = " + thenStore);
+        result.append("elseStore = " + elseStore);
+        result.append(System.getProperty("line.separator"));
+        result.append(")");
+        return result.toString();
+    }
+
+    /**
+     * @see org.checkerframework.dataflow.analysis.TransferResult#storeChanged()
+     */
+    @Override
+    public boolean storeChanged() {
+      return storeChanged;
+    }
+
+}