@@ -10,10 +10,22 @@ private import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
10
10
private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
11
11
12
12
private newtype TBufferWriteEstimationReason =
13
- TNoSpecifiedEstimateReason ( ) or
13
+ TUnspecifiedEstimateReason ( ) or
14
14
TTypeBoundsAnalysis ( ) or
15
+ TWidenedValueFlowAnalysis ( ) or
15
16
TValueFlowAnalysis ( )
16
17
18
+ private predicate gradeToReason ( int grade , TBufferWriteEstimationReason reason ) {
19
+ // when combining reasons, lower grade takes precedence
20
+ grade = 0 and reason = TUnspecifiedEstimateReason ( )
21
+ or
22
+ grade = 1 and reason = TTypeBoundsAnalysis ( )
23
+ or
24
+ grade = 2 and reason = TWidenedValueFlowAnalysis ( )
25
+ or
26
+ grade = 3 and reason = TValueFlowAnalysis ( )
27
+ }
28
+
17
29
/**
18
30
* A reason for a specific buffer write size estimate.
19
31
*/
@@ -32,24 +44,24 @@ abstract class BufferWriteEstimationReason extends TBufferWriteEstimationReason
32
44
* Combine estimate reasons. Used to give a reason for the size of a format string
33
45
* conversion given reasons coming from its individual specifiers.
34
46
*/
35
- abstract BufferWriteEstimationReason combineWith ( BufferWriteEstimationReason other ) ;
47
+ BufferWriteEstimationReason combineWith ( BufferWriteEstimationReason other ) {
48
+ exists ( int grade , int otherGrade |
49
+ gradeToReason ( grade , this ) and gradeToReason ( otherGrade , other )
50
+ |
51
+ if otherGrade < grade then result = other else result = this
52
+ )
53
+ }
36
54
}
37
55
38
56
/**
39
57
* No particular reason given. This is currently used for backward compatibility so that
40
58
* classes derived from BufferWrite and overriding `getMaxData/0` still work with the
41
59
* queries as intended.
42
60
*/
43
- class NoSpecifiedEstimateReason extends BufferWriteEstimationReason , TNoSpecifiedEstimateReason {
44
- override string toString ( ) { result = "NoSpecifiedEstimateReason " }
61
+ class UnspecifiedEstimateReason extends BufferWriteEstimationReason , TUnspecifiedEstimateReason {
62
+ override string toString ( ) { result = "UnspecifiedEstimateReason " }
45
63
46
64
override string getDescription ( ) { result = "no reason specified" }
47
-
48
- override BufferWriteEstimationReason combineWith ( BufferWriteEstimationReason other ) {
49
- // this reason should not be used in format specifiers, so it should not be combined
50
- // with other reasons
51
- none ( )
52
- }
53
65
}
54
66
55
67
/**
@@ -60,9 +72,24 @@ class TypeBoundsAnalysis extends BufferWriteEstimationReason, TTypeBoundsAnalysi
60
72
override string toString ( ) { result = "TypeBoundsAnalysis" }
61
73
62
74
override string getDescription ( ) { result = "based on type bounds" }
75
+ }
63
76
64
- override BufferWriteEstimationReason combineWith ( BufferWriteEstimationReason other ) {
65
- other != TNoSpecifiedEstimateReason ( ) and result = TTypeBoundsAnalysis ( )
77
+ /**
78
+ * The estimation comes from non trivial bounds found via actual flow analysis,
79
+ * but a widening aproximation might have been used for variables in loops.
80
+ * For example
81
+ * ```
82
+ * for (int i = 0; i < 10; ++i) {
83
+ * int j = i + i;
84
+ * //... <- estimation done here based on j
85
+ * }
86
+ * ```
87
+ */
88
+ class WidenedValueFlowAnalysis extends BufferWriteEstimationReason , TWidenedValueFlowAnalysis {
89
+ override string toString ( ) { result = "WidenedValueFlowAnalysis" }
90
+
91
+ override string getDescription ( ) {
92
+ result = "based on flow analysis of value bounds with a widening approximation"
66
93
}
67
94
}
68
95
@@ -80,10 +107,6 @@ class ValueFlowAnalysis extends BufferWriteEstimationReason, TValueFlowAnalysis
80
107
override string toString ( ) { result = "ValueFlowAnalysis" }
81
108
82
109
override string getDescription ( ) { result = "based on flow analysis of value bounds" }
83
-
84
- override BufferWriteEstimationReason combineWith ( BufferWriteEstimationReason other ) {
85
- other != TNoSpecifiedEstimateReason ( ) and result = other
86
- }
87
110
}
88
111
89
112
class PrintfFormatAttribute extends FormatAttribute {
@@ -362,6 +385,23 @@ private int lengthInBase10(float f) {
362
385
pragma [ nomagic]
363
386
private predicate isPointerTypeWithBase ( Type base , PointerType pt ) { base = pt .getBaseType ( ) }
364
387
388
+ bindingset [ expr]
389
+ private BufferWriteEstimationReason getEstimationReasonForIntegralExpression ( Expr expr ) {
390
+ // we consider the range analysis non trivial if it
391
+ // * constrained non-trivially both sides of a signed value, or
392
+ // * constrained non-trivially the positive side of an unsigned value
393
+ // expr should already be given as getFullyConverted
394
+ if
395
+ upperBound ( expr ) < exprMaxVal ( expr ) and
396
+ ( exprMinVal ( expr ) >= 0 or lowerBound ( expr ) > exprMinVal ( expr ) )
397
+ then
398
+ // next we check whether the estimate may have been widened
399
+ if upperBoundMayBeWidened ( expr )
400
+ then result = TWidenedValueFlowAnalysis ( )
401
+ else result = TValueFlowAnalysis ( )
402
+ else result = TTypeBoundsAnalysis ( )
403
+ }
404
+
365
405
/**
366
406
* A class to represent format strings that occur as arguments to invocations of formatting functions.
367
407
*/
@@ -1160,12 +1200,10 @@ class FormatLiteral extends Literal {
1160
1200
1 + lengthInBase10 ( 2 .pow ( this .getIntegralDisplayType ( n ) .getSize ( ) * 8 - 1 ) ) and
1161
1201
// The second case uses range analysis to deduce a length that's shorter than the length
1162
1202
// of the number -2^31.
1163
- exists ( Expr arg , float lower , float upper , float typeLower , float typeUpper |
1203
+ exists ( Expr arg , float lower , float upper |
1164
1204
arg = this .getUse ( ) .getConversionArgument ( n ) and
1165
1205
lower = lowerBound ( arg .getFullyConverted ( ) ) and
1166
- upper = upperBound ( arg .getFullyConverted ( ) ) and
1167
- typeLower = exprMinVal ( arg .getFullyConverted ( ) ) and
1168
- typeUpper = exprMaxVal ( arg .getFullyConverted ( ) )
1206
+ upper = upperBound ( arg .getFullyConverted ( ) )
1169
1207
|
1170
1208
valueBasedBound =
1171
1209
max ( int cand |
@@ -1182,11 +1220,9 @@ class FormatLiteral extends Literal {
1182
1220
else cand = lengthInBase10 ( upper )
1183
1221
)
1184
1222
) and
1185
- (
1186
- if lower > typeLower or upper < typeUpper
1187
- then reason = TValueFlowAnalysis ( )
1188
- else reason = TTypeBoundsAnalysis ( )
1189
- )
1223
+ // we don't want to call this on `arg.getFullyConverted()` as we want
1224
+ // to detect non-trivial range analysis without taking into account up-casting
1225
+ reason = getEstimationReasonForIntegralExpression ( arg )
1190
1226
) and
1191
1227
len = valueBasedBound .minimum ( typeBasedBound )
1192
1228
)
@@ -1198,12 +1234,10 @@ class FormatLiteral extends Literal {
1198
1234
typeBasedBound = lengthInBase10 ( 2 .pow ( this .getIntegralDisplayType ( n ) .getSize ( ) * 8 ) - 1 ) and
1199
1235
// The second case uses range analysis to deduce a length that's shorter than
1200
1236
// the length of the number 2^31 - 1.
1201
- exists ( Expr arg , float lower , float upper , float typeLower , float typeUpper |
1237
+ exists ( Expr arg , float lower , float upper |
1202
1238
arg = this .getUse ( ) .getConversionArgument ( n ) and
1203
1239
lower = lowerBound ( arg .getFullyConverted ( ) ) and
1204
- upper = upperBound ( arg .getFullyConverted ( ) ) and
1205
- typeLower = exprMinVal ( arg .getFullyConverted ( ) ) and
1206
- typeUpper = exprMaxVal ( arg .getFullyConverted ( ) )
1240
+ upper = upperBound ( arg .getFullyConverted ( ) )
1207
1241
|
1208
1242
valueBasedBound =
1209
1243
lengthInBase10 ( max ( float cand |
@@ -1213,11 +1247,9 @@ class FormatLiteral extends Literal {
1213
1247
or
1214
1248
cand = upper
1215
1249
) ) and
1216
- (
1217
- if lower > typeLower or upper < typeUpper
1218
- then reason = TValueFlowAnalysis ( )
1219
- else reason = TTypeBoundsAnalysis ( )
1220
- )
1250
+ // we don't want to call this on `arg.getFullyConverted()` as we want
1251
+ // to detect non-trivial range analysis without taking into account up-casting
1252
+ reason = getEstimationReasonForIntegralExpression ( arg )
1221
1253
) and
1222
1254
len = valueBasedBound .minimum ( typeBasedBound )
1223
1255
)
0 commit comments