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
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
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;
}
}
|
