-
Notifications
You must be signed in to change notification settings - Fork 5.2k
[Bounds Checks] Make union/intersect operations more precise #113862
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 all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -510,10 +510,15 @@ struct RangeOps | |
| { | ||
| result.lLimit = r1lo; | ||
| } | ||
| // Widen Upper Limit => Max(k, (a.len + n)) yields (a.len + n), | ||
| // This is correct if k >= 0 and n >= k, since a.len always >= 0 | ||
|
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.
NOTE: we've been already relying on this fact in RangeOps::Merge before my change |
||
| // (a.len + n) could overflow, but the result (a.len + n) also | ||
|
|
||
| // NOTE: in some of the calculations below, we assume that $bnd is never negative | ||
| // and we have to be careful by not masking possible overflows. | ||
|
|
||
| // Widen Upper Limit => Max(k, ($bnd + n)) yields ($bnd + n), | ||
| // This is correct if k >= 0 and n >= k, since $bnd always >= 0 | ||
| // ($bnd + n) could overflow, but the result ($bnd + n) also | ||
| // preserves the overflow. | ||
| // | ||
| if (r1hi.IsConstant() && r1hi.GetConstant() >= 0 && r2hi.IsBinOpArray() && | ||
| r2hi.GetConstant() >= r1hi.GetConstant()) | ||
| { | ||
|
|
@@ -524,14 +529,38 @@ struct RangeOps | |
| { | ||
| result.uLimit = r1hi; | ||
| } | ||
|
|
||
| // Rule: <$bnd + cns1, ...> U <cns2, ...> = <min(cns1, cns2), ...> when cns1 <= 0 | ||
| // | ||
| // Example: <$bnd - 3, ...> U <0, ...> = <-3, ...> | ||
| // | ||
| if (r1lo.IsBinOpArray() && r2lo.IsConstant() && (r1lo.cns <= 0)) | ||
| { | ||
| result.lLimit = Limit(Limit::keConstant, min(r1lo.cns, r2lo.cns)); | ||
| } | ||
| if (r2lo.IsBinOpArray() && r1lo.IsConstant() && (r2lo.cns <= 0)) | ||
| { | ||
| result.lLimit = Limit(Limit::keConstant, min(r2lo.cns, r1lo.cns)); | ||
| } | ||
|
Comment on lines
+537
to
+544
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 is adding more reliance on the unsound limits created based on 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. Yep, but we either shouldn't do it at all (depends on the bound actually, if it's VNF_ArrLen then it's always fine to rely on) or keep using it. I hope the "is montonic"/overflow analysis make it safe |
||
|
|
||
| // Rule: <..., $bnd + cns1> U <..., $bnd + cns2> = <..., $bnd + max(cns1, cns2)> | ||
| // | ||
| // Example: <..., $bnd + 10> U <..., $bnd + 20> = <..., $bnd + 20> | ||
| // | ||
| if (r1hi.IsBinOpArray() && r2hi.IsBinOpArray() && r1hi.vn == r2hi.vn) | ||
| { | ||
| result.uLimit = r1hi; | ||
| // Widen the upper bound if the other constant is greater. | ||
| if (r2hi.GetConstant() > r1hi.GetConstant()) | ||
| { | ||
| result.uLimit = r2hi; | ||
| } | ||
| result.uLimit = r1hi; // copy $bnd and kind info | ||
| result.uLimit.cns = max(r1hi.cns, r2hi.cns); | ||
| } | ||
|
|
||
| // Rule: <$bnd + cns1, ...> U <$bnd + cns2, ...> = <$bnd + min(cns1, cns2), ...> | ||
| // | ||
| // Example: <$bnd + 10, ...> U <$bnd + 20, ...> = <$bnd + 10, ...> | ||
| // | ||
| if (r1lo.IsBinOpArray() && r2lo.IsBinOpArray() && r1lo.vn == r2lo.vn) | ||
| { | ||
| result.lLimit = r1lo; // copy $bnd and kind info | ||
| result.lLimit.cns = min(r1lo.cns, r2lo.cns); | ||
| } | ||
| return result; | ||
| } | ||
|
|
||
Uh oh!
There was an error while loading. Please reload this page.
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.
In this case we just tighten the range (from multiple facts), it's fine to be liberal here. Seems like for lower bound it's always better to report a constant than trying to be smart with adjusted "bnd + offset"