@@ -10,10 +10,22 @@ private import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
1010private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
1111
1212private newtype TBufferWriteEstimationReason =
13- TNoSpecifiedEstimateReason ( ) or
13+ TUnspecifiedEstimateReason ( ) or
1414 TTypeBoundsAnalysis ( ) or
15+ TWidenedValueFlowAnalysis ( ) or
1516 TValueFlowAnalysis ( )
1617
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+
1729/**
1830 * A reason for a specific buffer write size estimate.
1931 */
@@ -32,24 +44,24 @@ abstract class BufferWriteEstimationReason extends TBufferWriteEstimationReason
3244 * Combine estimate reasons. Used to give a reason for the size of a format string
3345 * conversion given reasons coming from its individual specifiers.
3446 */
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+ }
3654}
3755
3856/**
3957 * No particular reason given. This is currently used for backward compatibility so that
4058 * classes derived from BufferWrite and overriding `getMaxData/0` still work with the
4159 * queries as intended.
4260 */
43- class NoSpecifiedEstimateReason extends BufferWriteEstimationReason , TNoSpecifiedEstimateReason {
44- override string toString ( ) { result = "NoSpecifiedEstimateReason " }
61+ class UnspecifiedEstimateReason extends BufferWriteEstimationReason , TUnspecifiedEstimateReason {
62+ override string toString ( ) { result = "UnspecifiedEstimateReason " }
4563
4664 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- }
5365}
5466
5567/**
@@ -60,9 +72,24 @@ class TypeBoundsAnalysis extends BufferWriteEstimationReason, TTypeBoundsAnalysi
6072 override string toString ( ) { result = "TypeBoundsAnalysis" }
6173
6274 override string getDescription ( ) { result = "based on type bounds" }
75+ }
6376
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"
6693 }
6794}
6895
@@ -80,10 +107,6 @@ class ValueFlowAnalysis extends BufferWriteEstimationReason, TValueFlowAnalysis
80107 override string toString ( ) { result = "ValueFlowAnalysis" }
81108
82109 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- }
87110}
88111
89112class PrintfFormatAttribute extends FormatAttribute {
@@ -362,6 +385,23 @@ private int lengthInBase10(float f) {
362385pragma [ nomagic]
363386private predicate isPointerTypeWithBase ( Type base , PointerType pt ) { base = pt .getBaseType ( ) }
364387
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+
365405/**
366406 * A class to represent format strings that occur as arguments to invocations of formatting functions.
367407 */
@@ -1160,12 +1200,10 @@ class FormatLiteral extends Literal {
11601200 1 + lengthInBase10 ( 2 .pow ( this .getIntegralDisplayType ( n ) .getSize ( ) * 8 - 1 ) ) and
11611201 // The second case uses range analysis to deduce a length that's shorter than the length
11621202 // 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 |
11641204 arg = this .getUse ( ) .getConversionArgument ( n ) and
11651205 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 ( ) )
11691207 |
11701208 valueBasedBound =
11711209 max ( int cand |
@@ -1182,11 +1220,9 @@ class FormatLiteral extends Literal {
11821220 else cand = lengthInBase10 ( upper )
11831221 )
11841222 ) 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 )
11901226 ) and
11911227 len = valueBasedBound .minimum ( typeBasedBound )
11921228 )
@@ -1198,12 +1234,10 @@ class FormatLiteral extends Literal {
11981234 typeBasedBound = lengthInBase10 ( 2 .pow ( this .getIntegralDisplayType ( n ) .getSize ( ) * 8 ) - 1 ) and
11991235 // The second case uses range analysis to deduce a length that's shorter than
12001236 // 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 |
12021238 arg = this .getUse ( ) .getConversionArgument ( n ) and
12031239 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 ( ) )
12071241 |
12081242 valueBasedBound =
12091243 lengthInBase10 ( max ( float cand |
@@ -1213,11 +1247,9 @@ class FormatLiteral extends Literal {
12131247 or
12141248 cand = upper
12151249 ) ) 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 )
12211253 ) and
12221254 len = valueBasedBound .minimum ( typeBasedBound )
12231255 )
0 commit comments