Add document for lvalue bounds checking generalization #970
Conversation
|
|
||
| 1. The widened bounds for `v`, if `v` has widened bounds within the current CFG | ||
| block `B`, or: | ||
| 2. The declared bounds for `v`, if `v` has declared bounds, or: |
There was a problem hiding this comment.
It might perhaps be more clear to reword this sentence as "The declared bounds for v, if v is declared in S" (as is stated in line 116 above).
There was a problem hiding this comment.
v here could be a variable that was declared prior to S. For example:
void f() {
_Array_ptr<int> a : count(1) = 0;
// Statement S
// Before checking S, the ObservedBounds context is { a => bounds(a, a + 1), b => bounds(b, b + 2) }
_Array_ptr<int> b : count(2) = 0;
}
I moved this description of the initial ObservedBounds to the end of the section describing ResetKilledBounds, since at that point all the methods that are involved in setting the initial ObservedBounds have been described.
There was a problem hiding this comment.
Ok, thanks for the clarification!
|
|
||
| After checking a statement `S`, this method checks that, for each variable | ||
| declaration `v` in `ObservedBounds`, the inferred bounds `ObservedBounds[v]` | ||
| `ObservedBounds[v]` imply the declared bounds of `v` (`v->getBoundsExpr()`). |
There was a problem hiding this comment.
Typo: ObservedBounds[v] is repeated.
| occurs immediately after checking an assignment to the expression. The goal | ||
| is to generalize the work that was previously done for variables so that the | ||
| bounds checking behavior is the same for all lvalue expressions. | ||
|
|
There was a problem hiding this comment.
General question: Are bounds on global/static/extern variables declared in the compilation unit, being checked?
There was a problem hiding this comment.
These are checked in TraverseTopLevelVarDecl. This method itself doesn't do anything to the CheckingState members, including ObservedBounds and EquivExprs - it just initializes an empty CheckingState and checks the bounds immediately after traversing its VarDecl * argument.
How much detail on bounds checking do you think would be helpful in this document? Initially I didn't include TraverseTopLevelVarDecl here since it doesn't directly interact with ObservedBounds (or EquivExprs). I have another document in progress in #945 that describes bounds checking in general. I would propose that I move most of the detail in this "Bounds Checking for Variables" section into that document so that this document can focus more on lvalue generalization. The "Bounds Checking for Variables" section in this document can then just briefly list the places where ObservedBounds is updated or used since this is relevant to changing the ObservedBounds keys, and reference the other bounds checking document for more detail. What are your thoughts on this?
There was a problem hiding this comment.
Yes, I agree that most of the detail on bounds checking can be in the other document (#945) and this document can focus on lvalue generalization.
There was a problem hiding this comment.
Thanks. I've moved most of this section into the #945 document and just included a list of methods where it will be necessary to change the keys of ObservedBounds in this section
|
|
||
| In general, for lvalue expressions `e1` and `e2`, updating the inferred bounds | ||
| of `e1` should also update the bounds of `e2` if and only if `e1` and `e2` | ||
| are guranteed to be **identical lvalue expressions**. That is, if: |
There was a problem hiding this comment.
Typo: guranteed -> guaranteed.
|
|
||
| This definition does not account for aliasing concerns. It is possible for | ||
| lvalue expressions to partially or completely overlap (for example, struct | ||
| variables `a` and `b` may share some or all of their fields). For the initial |
There was a problem hiding this comment.
I think these two sentences must be removed from here. The definition, as it is stated above in lines 178 and 179, does not ignore aliasing concerns - we are ignoring aliasing concerns while determining identical lvalue expressions. Also see my comment below.
| lvalue expressions to partially or completely overlap (for example, struct | ||
| variables `a` and `b` may share some or all of their fields). For the initial | ||
| planned work for lvalue generalization, we will only consider lvalue identity | ||
| as defined above. We may consider aliasing issues in future work. |
There was a problem hiding this comment.
I think that the last-but-one sentence above must be reworded along the lines of:
"For the initial planned work for lvalue generalization, we will only generalize across lvalue expressions that the we are able to determine as identical based on the definition stated above. Further, while determining identical lvalue expressions, we will initially ignore aliasing concerns and ignore lvalue expressions that do not fully overlap in memory."
| ### ObservedBounds Keys | ||
|
|
||
| Currently, the `ObservedBounds` map uses `VarDecl *` as its keys. This ensures | ||
| that updating the inferred bounds for a `DeclExpr *` `x` updates the inferred |
There was a problem hiding this comment.
Typo: DeclExpr * -> DeclRefExpr *.
…ledBounds section
…of relevant methods The details have been moved into the bounds checking doc in PR #945.
|
LGTM. |
This document summarizes the proposed work necessary to generalize bounds checking from variables to lvalue expressions.