@@ -149,17 +149,45 @@ module ValidState {
149
149
* ```
150
150
*/
151
151
private predicate validStateImpl ( PathNode n , int value ) {
152
+ // If the dataflow node depends recursively on itself we restrict the range.
152
153
( inLoop ( n ) implies value = [ - 2 .. 2 ] ) and
153
154
(
155
+ // For the dataflow source we have an allocation such as `malloc(size + k)`,
156
+ // and the value of the flow-state is then `k`.
154
157
hasSize ( _, n .getNode ( ) , value )
155
158
or
159
+ // For a dataflow sink any `value` that is strictly smaller than the delta
160
+ // needs to be a valid flow-state. That is, for a snippet like:
161
+ // ```
162
+ // p = new char[size];
163
+ // memset(p, 0, size + 2);
164
+ // ```
165
+ // the valid flow-states at the `memset` must include `0` since the flow-state
166
+ // at the source is `0`. Similarly, for an example such as:
167
+ // ```
168
+ // p = new char[size + 1];
169
+ // memset(p, 0, size + 2);
170
+ // ```
171
+ // the flow-state at the `memset` must include `1` since `1` is the flow-state
172
+ // after the source.
173
+ //
174
+ // So we find a valid flow-state at the sink's predecessor, and use the definition
175
+ // of our sink predicate to compute the valid flow-states at the sink.
156
176
exists ( int delta , PathNode n0 |
157
177
n0 .getASuccessor ( ) = n and
158
178
validStateImpl ( n0 , value ) and
159
179
isSinkPairImpl ( _, _, n .getNode ( ) , delta , _) and
160
180
delta > value
161
181
)
162
182
or
183
+ // For a non-source and non-sink node there is two cases to consider.
184
+ // 1. A node where we have to update the flow-state, or
185
+ // 2. A node that doesn't update the flow-state.
186
+ //
187
+ // For case 1, we compute the new flow-state by adding the constant operand of the
188
+ // `AddInstruction` to the flow-state of any predecessor node.
189
+ // For case 2 we simply propagate the valid flow-states from the predecessor node to
190
+ // the next one.
163
191
exists ( PathNode n0 , DataFlow:: Node node , int value0 |
164
192
n0 .getASuccessor ( ) = n and
165
193
validStateImpl ( n0 , value0 ) and
0 commit comments