Conversation
An expression that modifies an LValue is said to be invertible w.r.t. the LValue if we can write an expression in terms of the original value of the LValue before the modification. For example, the expression x + 1 is invertible w.r.t x because we can write this expression in terms of the original value of x which is (x - 1) + 1. In this PR, we use invertibility of statements to support bounds widening in loops. More specifically, if a statement modifies a variable that occurs in the bounds expression of a null-terminated array then instead of killing its bounds at that statement we use invertibility of the statement to try to write the widened bounds in terms of the original value of the variable.
| // set InOfLastStmt to StmtOut. | ||
| // InOfCurrStmt contains the Out set of the second last statement of the | ||
| // block. This is equal to the In set for the last statement of this | ||
| // block. So we set InOfLastStmt to StmtOut. |
There was a problem hiding this comment.
Nit: The comment on lines 100 - 102 can now be further simplified.
| // a bounds expression which is strictly wider than the declared upper | ||
| // bound. | ||
| // So we will proceed only if AdjustedRangeBounds is wider than | ||
| // StmtOut[V] which contains the delcared bounds of V at this point. For |
There was a problem hiding this comment.
Typo: delcared -> declared
| // statement. If the statement is invertible then store the statement, the | ||
| // modified LValue, the original LValue and the set of null-terminated arrays | ||
| // whose bounds are affected by the statement. We will use this info in the | ||
| // computation of the Out sets of blocks. |
There was a problem hiding this comment.
Nit: ...computation of the Out sets of blocks -> ...computation of the Out sets of statements.
| void assign2( | ||
| array_ptr<int> a : count(len - 1), // expected-note {{(expanded) declared bounds are 'bounds(a, a + len - 1)'}} | ||
| char b nt_checked[0] : count(len), // expected-note {{(expanded) declared bounds are 'bounds(b, b + len)'}} | ||
| char b nt_checked[0] : count(len), |
There was a problem hiding this comment.
This change on line 303 and lines 311 and 312 do not seem to be caused by the implementation of invertibility. It will be great if you could give some context for this change.
There was a problem hiding this comment.
These changes are a direct result of invertibility. b is a null-terminated array which uses len in its bounds and len is modified. Without invertibility we would have killed the bounds of b and issued the warning/note messages. But with invertibility we can "adjust" the bounds of b to bounds(b, b + len - 3).
There was a problem hiding this comment.
Filed #1138 to track the invalid declaration of nt_checked array of size 0.
2 participants
An expression that modifies an LValue is said to be invertible w.r.t. the
LValue if we can write an expression in terms of the original value of the
LValue before the modification. For example, the expression x + 1 is invertible
w.r.t x because we can write this expression in terms of the original value of
x which is (x - 1) + 1.
In this PR, we use invertibility of statements to support bounds widening in
loops. More specifically, if a statement modifies a variable that occurs in the
bounds expression of a null-terminated array then instead of killing its bounds
at that statement we use invertibility of the statement to try to write the
widened bounds in terms of the original value of the variable.