aboutsummaryrefslogtreecommitdiffhomepage
path: root/third_party/checker_framework_dataflow/java/org/checkerframework/dataflow/analysis/Store.java
blob: 7d1b8f9259ef8aec2edf4289b1d95688a3c3ebaf (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
package org.checkerframework.dataflow.analysis;

import org.checkerframework.dataflow.cfg.CFGVisualizer;

/**
 * A store is used to keep track of the information that the org.checkerframework.dataflow analysis
 * has accumulated at any given point in time.
 *
 * @author Stefan Heule
 *
 * @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 {
        EACH_TO_EACH,       // The normal case, then store flows to the then store
                            // and else store flows to the else store.
        THEN_TO_BOTH,       // Then store flows to both then and else of successor.
        ELSE_TO_BOTH,       // Else store flows to both then and else of successor.
        THEN_TO_THEN,       // Then store flows to the then of successor.  Else store is ignored.
        ELSE_TO_ELSE,       // Else store flows to the else of successor.  Then store is ignored.
    }

    /** @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>
     * <li>Does not change {@code other}.</li>
     * <li>Returns a fresh object which is not aliased yet.</li>
     * <li>Returns an object of the same (dynamic) type as {@code this}, even if
     * the signature is more permissive.</li>
     * <li>Is commutative.</li>
     * </ul>
     */
    S leastUpperBound(S other);

    /**
     * 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(FlowExpressions.Receiver a,
                     FlowExpressions.Receiver b);

    /**
     * Delegate visualization responsibility to a visualizer.
     *
     * @param viz the visualizer to visualize this store
     */
    void visualize(CFGVisualizer<?, S, ?> viz);
}