-
Notifications
You must be signed in to change notification settings - Fork 79
Explain bounds proof failure caused by free variables in inferred/declared bounds #903
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Changes from 1 commit
5722d2d
021e928
354a859
2a82843
af5f9c3
f6f3af5
7296d8b
70aa057
3abacfd
b22bd1a
29926f2
3317bce
ff01d32
d321731
6b84507
729e959
a22825d
edb3309
3df3205
62c2af8
13ecbba
5c5729f
aba5112
84781f7
69c8870
a1e0ebb
f5be4c2
cfa45ef
07f9d30
caf29d3
3960544
cf5c27d
2476209
1362645
7199da9
65476a1
9682a24
c425694
7a65d59
97b4556
842cc89
389e118
7a0c884
b20f1e4
6dba79a
867cf58
555a93c
7db553c
c934e70
7352252
d46fc90
323e8ee
ab80d34
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
* Fix issue #909 and #911 by ignoring casts in EquivExprs * Replace IgnoreCasts with IgnoreParenCasts and add test cases
- Loading branch information
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -571,12 +571,12 @@ namespace { | |
// EqualExprsContainsExpr returns true if the set Exprs contains E. | ||
bool EqualExprsContainsExpr(Sema &S, const EqualExprTy Exprs, Expr *E, | ||
EquivExprSets *EquivExprs) { | ||
for (auto I = Exprs.begin(); I != Exprs.end(); ++I) { | ||
for (auto I = Exprs.begin(); I != Exprs.end(); ++I) { | ||
if (Lexicographic(S.Context, EquivExprs).CompareExpr(*I, E) == | ||
Lexicographic::Result::Equal) | ||
return true; | ||
} | ||
return false; | ||
Lexicographic::Result::Equal) | ||
return true; | ||
} | ||
return false; | ||
} | ||
|
||
// Helper class for collecting a vector of unique variables as rvalues from an | ||
|
@@ -595,12 +595,8 @@ namespace { | |
const EqualExprTy &GetVariableList() const { return VariableList; } | ||
|
||
bool VisitDeclRefExpr(DeclRefExpr *E) { | ||
// We cast variables to rvalues so they can be compared with rvalues in EquivExprSet. | ||
// TODO(checkedc-clang#909): avoid constructing these ImplicitCastExprs. | ||
ImplicitCastExpr *CastExpr = ExprCreatorUtil::CreateImplicitCast( | ||
SemaRef, E, CK_LValueToRValue, E->getType()); | ||
if (!EqualExprsContainsExpr(SemaRef, VariableList, CastExpr, nullptr)) { | ||
VariableList.push_back(CastExpr); | ||
if (!EqualExprsContainsExpr(SemaRef, VariableList, E, nullptr)) { | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This has asymptotic behavior that is quadratic in the number of variables occurring in E. A better algorithm would be to use a hashtable to filter values and then append them the list of they aren't in the hash table. You could use the canonical declaration of the declaration referenced by E. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. @kkjeer, is my comment still accurate? If so, could you leave a comment in the code about the algorithm being quadratic. I don't like to leave quadratic algorithms around in a compiler without calling them out. |
||
VariableList.push_back(E); | ||
} | ||
|
||
return true; | ||
|
@@ -1465,8 +1461,7 @@ namespace { | |
break; | ||
} | ||
|
||
// We searched all declared variables and found neither a constant nor | ||
// a match for SrcV. | ||
// Find no constant or no match for SrcV in EquivExprs. | ||
if (It == DstVars.end()) { | ||
HasFreeVariables = true; | ||
FreeVariables.push_back(SrcV); | ||
|
@@ -1492,10 +1487,24 @@ namespace { | |
EqualExprTy Vars1 = CollectVariableSet(S, E1); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This algorithm isn't correct because of its handling of equivalent expression sets. With equivalent expression sets, you may have two expressions that are known to be equal, such as "a.f == b.f", even though there is no equality of the variables used in the expressions. We don't know that a == b, for example. We may need to generalize the notion of a variable v having relational information to another variable y. We need to check that there no expressions constructed from v or y that have relational information either. |
||
EqualExprTy Vars2 = CollectVariableSet(S, E2); | ||
|
||
if (AddFreeVariables(S, Vars1, Vars2, EquivExprs, Pos1, FreeVars)) | ||
// EquivVars holds sets of DeclRefExpr and IntegerLiteral filtered from | ||
// EquivExprs. | ||
EquivExprSets EquivVars; | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. An implication of my comment is that we shouldn't be filtering EquivVars. We could be removing expressions that have equality relationships and that use variables. |
||
for (auto ExprSet : *EquivExprs) { | ||
EqualExprTy Vars; | ||
auto It = ExprSet.begin(); | ||
for (; It != ExprSet.end(); It++) { | ||
*It = (*It)->IgnoreParenCasts(); | ||
if (isa<IntegerLiteral>(*It) || (isa<DeclRefExpr>(*It))) | ||
Vars.push_back(*It); | ||
} | ||
EquivVars.push_back(Vars); | ||
} | ||
|
||
if (AddFreeVariables(S, Vars1, Vars2, &EquivVars, Pos1, FreeVars)) | ||
HasFreeVariables = true; | ||
|
||
if (AddFreeVariables(S, Vars2, Vars1, EquivExprs, Pos2, FreeVars)) | ||
if (AddFreeVariables(S, Vars2, Vars1, &EquivVars, Pos2, FreeVars)) | ||
HasFreeVariables = true; | ||
|
||
return HasFreeVariables; | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This comment isn't quite accurate. It returns true if Exprs contains an expression that is equivalent to E.