Skip to content

Commit 61f30c9

Browse files
paldepindpaldepind
committed
C++: Improve bounds from inequalities on integers
1 parent 5dacbec commit 61f30c9

File tree

5 files changed

+52
-28
lines changed

5 files changed

+52
-28
lines changed

‎cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll‎

Lines changed: 38 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1397,6 +1397,20 @@ predicate nonNanGuardedVariable(Expr guard, VariableAccess v, boolean branch) {
13971397
nanExcludingComparison(guard, branch)
13981398
}
13991399

1400+
/**
1401+
* Adjusts a lower bound to its meaning for integral types.
1402+
*
1403+
* Examples:
1404+
* `>= 3.0` becomes `3.0`
1405+
* ` > 3.0` becomes `4.0`
1406+
* `>= 3.5` becomes `4.0`
1407+
* ` > 3.5` becomes `4.0`
1408+
*/
1409+
bindingset[strictness, lb]
1410+
private float adjustLowerBoundIntegral(RelationStrictness strictness, float lb) {
1411+
if strictness = Nonstrict() and lb.floor() = lb then result = lb else result = safeFloor(lb) + 1
1412+
}
1413+
14001414
/**
14011415
* If the guard is a comparison of the form `p*v + q <CMP> r`, then this
14021416
* predicate uses the bounds information for `r` to compute a lower bound
@@ -1408,15 +1422,27 @@ private predicate lowerBoundFromGuard(Expr guard, VariableAccess v, float lb, bo
14081422
|
14091423
if nonNanGuardedVariable(guard, v, branch)
14101424
then
1411-
if
1412-
strictness = Nonstrict() or
1413-
not getVariableRangeType(v.getTarget()) instanceof IntegralType
1414-
then lb = childLB
1415-
else lb = childLB + 1
1425+
if getVariableRangeType(v.getTarget()) instanceof IntegralType
1426+
then lb = adjustLowerBoundIntegral(strictness, childLB)
1427+
else lb = childLB
14161428
else lb = varMinVal(v.getTarget())
14171429
)
14181430
}
14191431

1432+
/**
1433+
* Adjusts an upper bound to its meaning for integral types.
1434+
*
1435+
* Examples:
1436+
* `<= 3.0` becomes `3.0`
1437+
* ` < 3.0` becomes `2.0`
1438+
* `<= 3.5` becomes `3.0`
1439+
* ` < 3.5` becomes `3.0`
1440+
*/
1441+
bindingset[strictness, ub]
1442+
private float adjustUpperBoundIntegral(RelationStrictness strictness, float ub) {
1443+
if strictness = Strict() and ub.floor() = ub then result = ub - 1 else result = safeFloor(ub)
1444+
}
1445+
14201446
/**
14211447
* If the guard is a comparison of the form `p*v + q <CMP> r`, then this
14221448
* predicate uses the bounds information for `r` to compute a upper bound
@@ -1428,11 +1454,9 @@ private predicate upperBoundFromGuard(Expr guard, VariableAccess v, float ub, bo
14281454
|
14291455
if nonNanGuardedVariable(guard, v, branch)
14301456
then
1431-
if
1432-
strictness = Nonstrict() or
1433-
not getVariableRangeType(v.getTarget()) instanceof IntegralType
1434-
then ub = childUB
1435-
else ub = childUB - 1
1457+
if getVariableRangeType(v.getTarget()) instanceof IntegralType
1458+
then ub = adjustUpperBoundIntegral(strictness, childUB)
1459+
else ub = childUB
14361460
else ub = varMaxVal(v.getTarget())
14371461
)
14381462
}
@@ -1472,7 +1496,7 @@ private predicate boundFromGuard(
14721496
* lower or upper bound for `v`.
14731497
*/
14741498
private predicate linearBoundFromGuard(
1475-
ComparisonOperation guard, VariableAccess v, float p, float q, float boundValue,
1499+
ComparisonOperation guard, VariableAccess v, float p, float q, float r,
14761500
boolean isLowerBound, // Is this a lower or an upper bound?
14771501
RelationStrictness strictness, boolean branch // Which control-flow branch is this bound valid on?
14781502
) {
@@ -1487,11 +1511,11 @@ private predicate linearBoundFromGuard(
14871511
|
14881512
isLowerBound = directionIsGreater(dir) and
14891513
strictness = st and
1490-
getBounds(rhs, boundValue, isLowerBound)
1514+
getBounds(rhs, r, isLowerBound)
14911515
or
14921516
isLowerBound = directionIsLesser(dir) and
14931517
strictness = Nonstrict() and
1494-
exprTypeBounds(rhs, boundValue, isLowerBound)
1518+
exprTypeBounds(rhs, r, isLowerBound)
14951519
)
14961520
or
14971521
// For x == RHS, we create the following bounds:
@@ -1502,7 +1526,7 @@ private predicate linearBoundFromGuard(
15021526
exists(Expr lhs, Expr rhs |
15031527
linearAccess(lhs, v, p, q) and
15041528
eqOpWithSwapAndNegate(guard, lhs, rhs, true, branch) and
1505-
getBounds(rhs, boundValue, isLowerBound) and
1529+
getBounds(rhs, r, isLowerBound) and
15061530
strictness = Nonstrict()
15071531
)
15081532
// x != RHS and !x are handled elsewhere

‎cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/lowerBound.expected‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -351,19 +351,19 @@
351351
| test.c:330:14:330:14 | r | -2147483648 |
352352
| test.c:333:10:333:14 | total | -2147483648 |
353353
| test.c:338:27:338:27 | e | 0 |
354-
| test.c:338:40:338:40 | e | 0.5 |
354+
| test.c:338:40:338:40 | e | 0 |
355355
| test.c:339:25:339:25 | e | 0 |
356356
| test.c:339:39:339:39 | e | 0 |
357357
| test.c:340:27:340:27 | e | 0 |
358-
| test.c:340:40:340:40 | e | 0.333333 |
358+
| test.c:340:40:340:40 | e | 0 |
359359
| test.c:341:27:341:27 | e | 0 |
360-
| test.c:341:40:341:40 | e | 0.5 |
360+
| test.c:341:40:341:40 | e | 0 |
361361
| test.c:342:27:342:27 | e | 0 |
362-
| test.c:342:41:342:41 | e | 8.5 |
363-
| test.c:344:10:344:12 | bi1 | 0.5 |
362+
| test.c:342:41:342:41 | e | 8 |
363+
| test.c:344:10:344:12 | bi1 | 0 |
364364
| test.c:344:16:344:18 | bi2 | 0 |
365-
| test.c:344:22:344:24 | bi3 | 0.333333 |
366-
| test.c:344:28:344:30 | bi4 | 0.5 |
365+
| test.c:344:22:344:24 | bi3 | 0 |
366+
| test.c:344:28:344:30 | bi4 | 0 |
367367
| test.c:344:34:344:36 | bi5 | 2 |
368368
| test.c:349:7:349:7 | x | -2147483648 |
369369
| test.c:353:10:353:10 | i | 0 |

‎cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryLower.expected‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
| test.c:154:10:154:40 | ... ? ... : ... | -1.0 | 1.0 | -1.0 |
2-
| test.c:338:22:338:44 | ... ? ... : ... | 0.5 | 0.5 | 2.0 |
2+
| test.c:338:22:338:44 | ... ? ... : ... | 0.0 | 0.0 | 2.0 |
33
| test.c:339:20:339:43 | ... ? ... : ... | 0.0 | 0.0 | 2.0 |
4-
| test.c:340:22:340:44 | ... ? ... : ... | 0.33333333333333337 | 0.33333333333333337 | 2.0 |
5-
| test.c:341:22:341:44 | ... ? ... : ... | 0.5 | 0.5 | 2.0 |
6-
| test.c:342:22:342:45 | ... ? ... : ... | 2.0 | 8.5 | 2.0 |
4+
| test.c:340:22:340:44 | ... ? ... : ... | 0.0 | 0.0 | 2.0 |
5+
| test.c:341:22:341:44 | ... ? ... : ... | 0.0 | 0.0 | 2.0 |
6+
| test.c:342:22:342:45 | ... ? ... : ... | 2.0 | 8.0 | 2.0 |
77
| test.c:368:8:368:23 | ... ? ... : ... | 0.0 | 0.0 | 10.0 |
88
| test.c:369:8:369:24 | ... ? ... : ... | 0.0 | 10.0 | 0.0 |
99
| test.c:377:10:377:15 | ... ? ... : ... | 0.0 | 0.0 | 5.0 |

‎cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryUpper.expected‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
| test.c:154:10:154:40 | ... ? ... : ... | 2.147483647E9 | 2.147483647E9 | -1.0 |
22
| test.c:338:22:338:44 | ... ? ... : ... | 2.147483647E9 | 2.147483647E9 | 2.0 |
33
| test.c:339:20:339:43 | ... ? ... : ... | 2.147483647E9 | 2.147483647E9 | 2.0 |
4-
| test.c:340:22:340:44 | ... ? ... : ... | 1.4316557643333333E9 | 1.4316557643333333E9 | 2.0 |
4+
| test.c:340:22:340:44 | ... ? ... : ... | 1.431655764E9 | 1.431655764E9 | 2.0 |
55
| test.c:341:22:341:44 | ... ? ... : ... | 2.147483647E9 | 2.147483647E9 | 2.0 |
66
| test.c:342:22:342:45 | ... ? ... : ... | 2.147483647E9 | 2.147483647E9 | 2.0 |
77
| test.c:368:8:368:23 | ... ? ... : ... | 99.0 | 99.0 | 10.0 |

‎cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/upperBound.expected‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -355,14 +355,14 @@
355355
| test.c:339:25:339:25 | e | 4294967295 |
356356
| test.c:339:39:339:39 | e | 2147483647 |
357357
| test.c:340:27:340:27 | e | 4294967295 |
358-
| test.c:340:40:340:40 | e | 1431655764.333333 |
358+
| test.c:340:40:340:40 | e | 1431655764 |
359359
| test.c:341:27:341:27 | e | 4294967295 |
360360
| test.c:341:40:341:40 | e | 2147483647 |
361361
| test.c:342:27:342:27 | e | 4294967295 |
362362
| test.c:342:41:342:41 | e | 2147483647 |
363363
| test.c:344:10:344:12 | bi1 | 2147483647 |
364364
| test.c:344:16:344:18 | bi2 | 2147483647 |
365-
| test.c:344:22:344:24 | bi3 | 1431655764.333333 |
365+
| test.c:344:22:344:24 | bi3 | 1431655764 |
366366
| test.c:344:28:344:30 | bi4 | 2147483647 |
367367
| test.c:344:34:344:36 | bi5 | 2147483647 |
368368
| test.c:349:7:349:7 | x | 2147483647 |

0 commit comments

Comments
 (0)