Skip to content

Commit 6dd45b3

Browse files
MathiasVPMathiasVP
authored
Merge pull request github#12696 from MathiasVP/range-analysis-of-mul-expr
C++: IR-based range analysis of multiplication
2 parents d0fa7c7 + 9d5c785 commit 6dd45b3

File tree

2 files changed

+159
-40
lines changed

2 files changed

+159
-40
lines changed

‎cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisStage.qll

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1062,6 +1062,20 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
10621062
or
10631063
upper = false and delta = D::fromFloat(-D::toFloat(d_max).abs() + 1)
10641064
)
1065+
or
1066+
exists(
1067+
D::Delta dLeft, D::Delta dRight, boolean fbeLeft, boolean fbeRight, D::Delta odLeft,
1068+
D::Delta odRight, SemReason rLeft, SemReason rRight
1069+
|
1070+
boundedMulOperand(e, upper, true, dLeft, fbeLeft, odLeft, rLeft) and
1071+
boundedMulOperand(e, upper, false, dRight, fbeRight, odRight, rRight) and
1072+
delta = D::fromFloat(D::toFloat(dLeft) * D::toFloat(dRight)) and
1073+
fromBackEdge = fbeLeft.booleanOr(fbeRight)
1074+
|
1075+
b instanceof SemZeroBound and origdelta = odLeft and reason = rLeft
1076+
or
1077+
b instanceof SemZeroBound and origdelta = odRight and reason = rRight
1078+
)
10651079
)
10661080
}
10671081

@@ -1095,4 +1109,109 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
10951109
) {
10961110
bounded(rem.getRightOperand(), b, delta, upper, fromBackEdge, origdelta, reason)
10971111
}
1112+
1113+
/**
1114+
* Define `cmp(true) = <=` and `cmp(false) = >=`.
1115+
*
1116+
* Holds if `mul = left * right`, and in order to know if `mul cmp(upper) 0 + k` (for
1117+
* some `k`) we need to know that `left cmp(upperLeft) 0 + k1` and
1118+
* `right cmp(upperRight) 0 + k2` (for some `k1` and `k2`).
1119+
*/
1120+
pragma[nomagic]
1121+
private predicate boundedMulOperandCand(
1122+
SemMulExpr mul, SemExpr left, SemExpr right, boolean upper, boolean upperLeft,
1123+
boolean upperRight
1124+
) {
1125+
not boundFlowStepMul(mul, _, _) and
1126+
mul.getLeftOperand() = left and
1127+
mul.getRightOperand() = right and
1128+
(
1129+
semPositive(left) and
1130+
(
1131+
// left, right >= 0
1132+
semPositive(right) and
1133+
(
1134+
// max(left * right) = max(left) * max(right)
1135+
upper = true and
1136+
upperLeft = true and
1137+
upperRight = true
1138+
or
1139+
// min(left * right) = min(left) * min(right)
1140+
upper = false and
1141+
upperLeft = false and
1142+
upperRight = false
1143+
)
1144+
or
1145+
// left >= 0, right <= 0
1146+
semNegative(right) and
1147+
(
1148+
// max(left * right) = min(left) * max(right)
1149+
upper = true and
1150+
upperLeft = false and
1151+
upperRight = true
1152+
or
1153+
// min(left * right) = max(left) * min(right)
1154+
upper = false and
1155+
upperLeft = true and
1156+
upperRight = false
1157+
)
1158+
)
1159+
or
1160+
semNegative(left) and
1161+
(
1162+
// left <= 0, right >= 0
1163+
semPositive(right) and
1164+
(
1165+
// max(left * right) = max(left) * min(right)
1166+
upper = true and
1167+
upperLeft = true and
1168+
upperRight = false
1169+
or
1170+
// min(left * right) = min(left) * max(right)
1171+
upper = false and
1172+
upperLeft = false and
1173+
upperRight = true
1174+
)
1175+
or
1176+
// left, right <= 0
1177+
semNegative(right) and
1178+
(
1179+
// max(left * right) = min(left) * min(right)
1180+
upper = true and
1181+
upperLeft = false and
1182+
upperRight = false
1183+
or
1184+
// min(left * right) = max(left) * max(right)
1185+
upper = false and
1186+
upperLeft = true and
1187+
upperRight = true
1188+
)
1189+
)
1190+
)
1191+
}
1192+
1193+
/**
1194+
* Holds if `isLeft = true` and `mul`'s left operand is bounded by `delta`,
1195+
* or if `isLeft = false` and `mul`'s right operand is bounded by `delta`.
1196+
*
1197+
* If `upper = true` the computed bound contributes to an upper bound of `mul`,
1198+
* and if `upper = false` it contributes to a lower bound.
1199+
* The `fromBackEdge`, `origdelta`, `reason` triple are defined by the recursive
1200+
* call to `bounded`.
1201+
*/
1202+
pragma[nomagic]
1203+
private predicate boundedMulOperand(
1204+
SemMulExpr mul, boolean upper, boolean isLeft, D::Delta delta, boolean fromBackEdge,
1205+
D::Delta origdelta, SemReason reason
1206+
) {
1207+
exists(boolean upperLeft, boolean upperRight, SemExpr left, SemExpr right |
1208+
boundedMulOperandCand(mul, left, right, upper, upperLeft, upperRight)
1209+
|
1210+
isLeft = true and
1211+
bounded(left, any(SemZeroBound zb), delta, upperLeft, fromBackEdge, origdelta, reason)
1212+
or
1213+
isLeft = false and
1214+
bounded(right, any(SemZeroBound zb), delta, upperRight, fromBackEdge, origdelta, reason)
1215+
)
1216+
}
10981217
}

‎cpp/ql/test/library-tests/ir/range-analysis/SimpleRangeAnalysis_tests.cpp

Lines changed: 40 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -300,17 +300,17 @@ int test_mult01(int a, int b) {
300300
range(a); // $ range=<=11 range=>=3
301301
range(b); // $ range=<=23 range=>=5
302302
int r = a*b; // 15 .. 253
303-
range(r);
303+
range(r); // $ range=<=253 range=>=15
304304
total += r;
305-
range(total); // $ MISSING: range=>=1
305+
range(total); // $ range=<=253 range=>=15
306306
}
307307
if (3 <= a && a <= 11 && 0 <= b && b <= 23) {
308308
range(a); // $ range=<=11 range=>=3
309309
range(b); // $ range=<=23 range=>=0
310310
int r = a*b; // 0 .. 253
311-
range(r);
311+
range(r); // $ range=<=253 range=>=0
312312
total += r;
313-
range(total); // $ MISSING: range=>=0 range=>=3+0
313+
range(total); // $ range=<=3+253 range=<=506 range=>=0 range=>=3+0
314314
}
315315
if (3 <= a && a <= 11 && -13 <= b && b <= 23) {
316316
range(a); // $ range=<=11 range=>=3
@@ -324,19 +324,19 @@ int test_mult01(int a, int b) {
324324
range(a); // $ range=<=11 range=>=3
325325
range(b); // $ range=<=0 range=>=-13
326326
int r = a*b; // -143 .. 0
327-
range(r);
327+
range(r); // $ range=<=0 range=>=-143
328328
total += r;
329-
range(total); // $ MISSING: range=<=3+0
329+
range(total); // $ range=<=3+0 range=>=3-143
330330
}
331331
if (3 <= a && a <= 11 && -13 <= b && b <= -7) {
332332
range(a); // $ range=<=11 range=>=3
333333
range(b); // $ range=<=-7 range=>=-13
334334
int r = a*b; // -143 .. -21
335-
range(r);
335+
range(r); // $ range=<=-21 range=>=-143
336336
total += r;
337-
range(total); // $ MISSING: range=<=3-1
337+
range(total); // $ range=<=3-21 range=>=3-143 range=>=3-286
338338
}
339-
range(total); // $ MISSING: range=<=3+0
339+
range(total); // $ range=<=3+0 range=>=3-143 range=>=3-286
340340
return total;
341341
}
342342

@@ -348,17 +348,17 @@ int test_mult02(int a, int b) {
348348
range(a); // $ range=<=11 range=>=0
349349
range(b); // $ range=<=23 range=>=5
350350
int r = a*b; // 0 .. 253
351-
range(r);
351+
range(r); // $ range=<=253 range=>=0
352352
total += r;
353-
range(total); // $ MISSING: range=>=0
353+
range(total); // $ range=>=0 range=<=253
354354
}
355355
if (0 <= a && a <= 11 && 0 <= b && b <= 23) {
356356
range(a); // $ range=<=11 range=>=0
357357
range(b); // $ range=<=23 range=>=0
358358
int r = a*b; // 0 .. 253
359-
range(r);
359+
range(r); // $ range=<=253 range=>=0
360360
total += r;
361-
range(total); // $ MISSING: range=>=0 range=>=0+0
361+
range(total); // $ range=>=0 range=>=0+0 range=<=0+253 range=<=506
362362
}
363363
if (0 <= a && a <= 11 && -13 <= b && b <= 23) {
364364
range(a); // $ range=<=11 range=>=0
@@ -372,19 +372,19 @@ int test_mult02(int a, int b) {
372372
range(a); // $ range=<=11 range=>=0
373373
range(b); // $ range=<=0 range=>=-13
374374
int r = a*b; // -143 .. 0
375-
range(r);
375+
range(r); // $ range=<=0 range=>=-143
376376
total += r;
377-
range(total); // $ MISSING: range=<=0+0
377+
range(total); // $ range=<=0+0 range=>=0-143
378378
}
379379
if (0 <= a && a <= 11 && -13 <= b && b <= -7) {
380380
range(a); // $ range=<=11 range=>=0
381381
range(b); // $ range=<=-7 range=>=-13
382382
int r = a*b; // -143 .. 0
383-
range(r);
383+
range(r); // $ range=<=0 range=>=-143
384384
total += r;
385-
range(total); // $ MISSING: range=<=0+0
385+
range(total); // $ range=<=0+0 range=>=0-143 range=>=0-286
386386
}
387-
range(total); // $ MISSING: range=<=0+0
387+
range(total); // $ range=<=0+0 range=>=0-143 range=>=0-286
388388
return total;
389389
}
390390

@@ -445,15 +445,15 @@ int test_mult04(int a, int b) {
445445
range(b); // $ range=<=23 range=>=5
446446
int r = a*b; // -391 .. 0
447447
total += r;
448-
range(total); // $ MISSING: range=<=0
448+
range(total); // $ range=<=0 range=>=-391
449449
}
450450
if (-17 <= a && a <= 0 && 0 <= b && b <= 23) {
451451
range(a); // $ range=<=0 range=>=-17
452452
range(b); // $ range=<=23 range=>=0
453453
int r = a*b; // -391 .. 0
454-
range(r);
454+
range(r); // $ range=<=0 range=>=-391
455455
total += r;
456-
range(total); // $ MISSING: range="<=- ...+0" range=<=0
456+
range(total); // $ range="<=- ...+0" range=<=0 range=">=- ...-391" range=>=-782
457457
}
458458
if (-17 <= a && a <= 0 && -13 <= b && b <= 23) {
459459
range(a); // $ range=<=0 range=>=-17
@@ -467,19 +467,19 @@ int test_mult04(int a, int b) {
467467
range(a); // $ range=<=0 range=>=-17
468468
range(b); // $ range=<=0 range=>=-13
469469
int r = a*b; // 0 .. 221
470-
range(r);
470+
range(r); // $ range=<=221 range=>=0
471471
total += r;
472-
range(total); // $ MISSING: range=">=- ...+0"
472+
range(total); // $ range="<=- ...+221" range=">=- ...+0"
473473
}
474474
if (-17 <= a && a <= 0 && -13 <= b && b <= -7) {
475475
range(a); // $ range=<=0 range=>=-17
476476
range(b); // $ range=<=-7 range=>=-13
477477
int r = a*b; // 0 .. 221
478-
range(r);
478+
range(r); // $ range=<=221 range=>=0
479479
total += r;
480-
range(total); // $ MISSING: range=">=- ...+0"
480+
range(total); // $ range=">=- ...+0" range="<=- ...+221" range="<=- ...+442"
481481
}
482-
range(total); // $ MISSING: range=">=- ...+0"
482+
range(total); // $ range=">=- ...+0" range="<=- ...+221" range="<=- ...+442"
483483
return total;
484484
}
485485

@@ -491,17 +491,17 @@ int test_mult05(int a, int b) {
491491
range(a); // $ range=<=-2 range=>=-17
492492
range(b); // $ range=<=23 range=>=5
493493
int r = a*b; // -391 .. -10
494-
range(r);
494+
range(r); // $ range=<=-10 range=>=-391
495495
total += r;
496-
range(total); // $ MISSING: range=<=-1
496+
range(total); // $ range=<=-10 range=>=-391
497497
}
498498
if (-17 <= a && a <= -2 && 0 <= b && b <= 23) {
499499
range(a); // $ range=<=-2 range=>=-17
500500
range(b); // $ range=<=23 range=>=0
501501
int r = a*b; // -391 .. 0
502-
range(r);
502+
range(r); // $ range=<=0 range=>=-391
503503
total += r;
504-
range(total); // $ MISSING: range="<=- ...+0" range=<=0
504+
range(total); // $ range="<=- ...+0" range=<=0 range=">=- ...-391" range=>=-782
505505
}
506506
if (-17 <= a && a <= -2 && -13 <= b && b <= 23) {
507507
range(a); // $ range=<=-2 range=>=-17
@@ -515,19 +515,19 @@ int test_mult05(int a, int b) {
515515
range(a); // $ range=<=-2 range=>=-17
516516
range(b); // $ range=<=0 range=>=-13
517517
int r = a*b; // 0 .. 221
518-
range(r);
518+
range(r); // $ range=<=221 range=>=0
519519
total += r;
520-
range(total); // $ MISSING: range=">=- ...+0"
520+
range(total); // $ range="<=- ...+221" range=">=- ...+0"
521521
}
522522
if (-17 <= a && a <= -2 && -13 <= b && b <= -7) {
523523
range(a); // $ range=<=-2 range=>=-17
524524
range(b); // $ range=<=-7 range=>=-13
525525
int r = a*b; // 14 .. 221
526-
range(r);
526+
range(r); // $ range=<=221 range=>=14
527527
total += r;
528-
range(total); // $ MISSING: range=">=- ...+1"
528+
range(total); // $ range="<=- ...+221" range="<=- ...+442" range=">=- ...+14"
529529
}
530-
range(total); // $ MISSING: range=">=- ...+0"
530+
range(total); // $ range=">=- ...+0" range="<=- ...+221" range="<=- ...+442"
531531
return total;
532532
}
533533

@@ -741,7 +741,7 @@ unsigned long mult_rounding() {
741741
range(y); // $ range===1000000003
742742
range(x); // $ range===1000000003
743743
xy = x * y;
744-
range(xy);
744+
range(xy); // $ range===2147483647
745745
return xy; // BUG: upper bound should be >= 1000000006000000009UL
746746
}
747747

@@ -761,13 +761,13 @@ unsigned long mult_lower_bound(unsigned int ui, unsigned long ul) {
761761
range(ui); // $ range=>=10
762762
range((unsigned long)ui); // $ range=>=10
763763
unsigned long result = (unsigned long)ui * ui;
764-
range(result);
764+
range(result); // $ range=>=100 range=>=100
765765
return result; // BUG: upper bound should be >= 18446744065119617025
766766
}
767767
if (ul >= 10) {
768768
range(ul); // $ range=>=10
769769
unsigned long result = ul * ul;
770-
range(result);
770+
range(result); // $ range=>=100
771771
return result; // BUG: lower bound should be 0 (overflow is possible)
772772
}
773773
return 0;
@@ -777,7 +777,7 @@ unsigned long mul_assign(unsigned int ui) {
777777
if (ui <= 10 && ui >= 2) {
778778
range(ui); // $ range=<=10 range=>=2
779779
ui *= ui + 0;
780-
range(ui);
780+
range(ui); // $ range=<=100 range=>=4
781781
return ui; // 4 .. 100
782782
}
783783

@@ -813,7 +813,7 @@ int mul_by_constant(int i, int j) {
813813
range(i); // $ range===-1
814814
range((int)0xffFFffFF); // $ range===-1
815815
i = i * (int)0xffFFffFF; // fully converted literal is -1
816-
range(i); // 1 .. 1
816+
range(i); // $ range===1
817817
}
818818
i = i * -1;
819819
range( i); // -2^31 .. 2^31-1

0 commit comments

Comments
 (0)