Skip to content

Commit 66d13dc

Browse files
authored
Merge pull request github#13981 from MathiasVP/fix-orig-delta-for-subtraction
C++: Fix original delta calculation for subtraction in new range analysis
2 parents 591565a + 20df63f commit 66d13dc

File tree

1 file changed

+6
-14
lines changed

1 file changed

+6
-14
lines changed

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll

Lines changed: 6 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1106,12 +1106,9 @@ module RangeStage<
11061106
b = bRight and origdelta = odRight and reason = rRight and bLeft instanceof SemZeroBound
11071107
)
11081108
or
1109-
exists(
1110-
D::Delta dLeft, D::Delta dRight, boolean fbeLeft, boolean fbeRight, D::Delta odLeft,
1111-
D::Delta odRight, SemReason rLeft, SemReason rRight
1112-
|
1113-
boundedSubOperandLeft(e, upper, b, dLeft, fbeLeft, odLeft, rLeft) and
1114-
boundedSubOperandRight(e, upper, dRight, fbeRight, odRight, rRight) and
1109+
exists(D::Delta dLeft, D::Delta dRight, boolean fbeLeft, boolean fbeRight |
1110+
boundedSubOperandLeft(e, upper, b, dLeft, fbeLeft, origdelta, reason) and
1111+
boundedSubOperandRight(e, upper, dRight, fbeRight) and
11151112
// when `upper` is `true` we have:
11161113
// left <= b + dLeft
11171114
// right >= 0 + dRight
@@ -1124,10 +1121,6 @@ module RangeStage<
11241121
// = b + (dLeft - dRight)
11251122
delta = D::fromFloat(D::toFloat(dLeft) - D::toFloat(dRight)) and
11261123
fromBackEdge = fbeLeft.booleanOr(fbeRight)
1127-
|
1128-
origdelta = odLeft and reason = rLeft
1129-
or
1130-
origdelta = odRight and reason = rRight
11311124
)
11321125
or
11331126
exists(
@@ -1217,13 +1210,12 @@ module RangeStage<
12171210
*/
12181211
pragma[nomagic]
12191212
private predicate boundedSubOperandRight(
1220-
SemSubExpr sub, boolean upper, D::Delta delta, boolean fromBackEdge, D::Delta origdelta,
1221-
SemReason reason
1213+
SemSubExpr sub, boolean upper, D::Delta delta, boolean fromBackEdge
12221214
) {
12231215
// `semValueFlowStep` already handles the case where one of the operands is a constant.
12241216
not semValueFlowStep(sub, _, _) and
1225-
bounded(sub.getRightOperand(), any(SemZeroBound zb), delta, upper.booleanNot(), fromBackEdge,
1226-
origdelta, reason)
1217+
bounded(sub.getRightOperand(), any(SemZeroBound zb), delta, upper.booleanNot(), fromBackEdge, _,
1218+
_)
12271219
}
12281220

12291221
pragma[nomagic]

0 commit comments

Comments
 (0)