Skip to content
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.

Sign up for GitHub

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

C++: Fix original delta calculation for subtraction in new range analysis #13981

Merged
merged 2 commits into from
Aug 16, 2023
Merged

C++: Fix original delta calculation for subtraction in new range analysis #13981

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
5e14b5c
C++: 'origDelta' should always be 'odLeft' when deriving subtraction …
MathiasVP Aug 16, 2023
20df63f
C++: Respond to review comments.
MathiasVP Aug 16, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 6 additions & 14 deletions ...l/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1106,12 +1106,9 @@ module RangeStage<
b = bRight and origdelta = odRight and reason = rRight and bLeft instanceof SemZeroBound
)
or
exists(
D::Delta dLeft, D::Delta dRight, boolean fbeLeft, boolean fbeRight, D::Delta odLeft,
D::Delta odRight, SemReason rLeft, SemReason rRight
|
boundedSubOperandLeft(e, upper, b, dLeft, fbeLeft, odLeft, rLeft) and
boundedSubOperandRight(e, upper, dRight, fbeRight, odRight, rRight) and
exists(D::Delta dLeft, D::Delta dRight, boolean fbeLeft, boolean fbeRight |
boundedSubOperandLeft(e, upper, b, dLeft, fbeLeft, origdelta, reason) and
boundedSubOperandRight(e, upper, dRight, fbeRight) and
// when `upper` is `true` we have:
// left <= b + dLeft
// right >= 0 + dRight
Expand All @@ -1124,10 +1121,6 @@ module RangeStage<
// = b + (dLeft - dRight)
delta = D::fromFloat(D::toFloat(dLeft) - D::toFloat(dRight)) and
fromBackEdge = fbeLeft.booleanOr(fbeRight)
|
origdelta = odLeft and reason = rLeft
or
origdelta = odRight and reason = rRight
)
or
exists(
Expand Down Expand Up @@ -1217,13 +1210,12 @@ module RangeStage<
*/
pragma[nomagic]
private predicate boundedSubOperandRight(
SemSubExpr sub, boolean upper, D::Delta delta, boolean fromBackEdge, D::Delta origdelta,
SemReason reason
SemSubExpr sub, boolean upper, D::Delta delta, boolean fromBackEdge
) {
// `semValueFlowStep` already handles the case where one of the operands is a constant.
not semValueFlowStep(sub, _, _) and
bounded(sub.getRightOperand(), any(SemZeroBound zb), delta, upper.booleanNot(), fromBackEdge,
origdelta, reason)
bounded(sub.getRightOperand(), any(SemZeroBound zb), delta, upper.booleanNot(), fromBackEdge, _,
_)
}

pragma[nomagic]
Expand Down