@@ -149,17 +149,45 @@ module ValidState {
149149 * ```
150150 */
151151 private predicate validStateImpl ( PathNode n , int value ) {
152+ // If the dataflow node depends recursively on itself we restrict the range.
152153 ( inLoop ( n ) implies value = [ - 2 .. 2 ] ) and
153154 (
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`.
154157 hasSize ( _, n .getNode ( ) , value )
155158 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.
156176 exists ( int delta , PathNode n0 |
157177 n0 .getASuccessor ( ) = n and
158178 validStateImpl ( n0 , value ) and
159179 isSinkPairImpl ( _, _, n .getNode ( ) , delta , _) and
160180 delta > value
161181 )
162182 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.
163191 exists ( PathNode n0 , DataFlow:: Node node , int value0 |
164192 n0 .getASuccessor ( ) = n and
165193 validStateImpl ( n0 , value0 ) and
0 commit comments