4444import cpp
4545private import RangeAnalysisUtils
4646import RangeSSA
47+ import SimpleRangeAnalysisCached
4748
4849/**
4950 * This fixed set of lower bounds is used when the lower bounds of an
@@ -406,27 +407,6 @@ deprecated predicate negative_overflow(Expr expr) {
406407 exprMightOverflowNegatively ( expr )
407408}
408409
409- /**
410- * Holds if the expression might overflow negatively. This predicate
411- * does not consider the possibility that the expression might overflow
412- * due to a conversion.
413- */
414- cached
415- predicate exprMightOverflowNegatively ( Expr expr ) {
416- getLowerBoundsImpl ( expr ) < exprMinVal ( expr )
417- }
418-
419- /**
420- * Holds if the expression might overflow negatively. Conversions
421- * are also taken into account. For example the expression
422- * `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than
423- * due to the addition.
424- */
425- cached
426- predicate convertedExprMightOverflowNegatively ( Expr expr ) {
427- exprMightOverflowNegatively ( expr ) or
428- convertedExprMightOverflowNegatively ( expr .getConversion ( ) )
429- }
430410
431411/**
432412 * Holds if the expression might overflow positively. This predicate
@@ -439,39 +419,6 @@ deprecated predicate positive_overflow(Expr expr) {
439419 exprMightOverflowPositively ( expr )
440420}
441421
442- /**
443- * Holds if the expression might overflow positively. This predicate
444- * does not consider the possibility that the expression might overflow
445- * due to a conversion.
446- */
447- cached
448- predicate exprMightOverflowPositively ( Expr expr ) {
449- getUpperBoundsImpl ( expr ) > exprMaxVal ( expr )
450- }
451-
452- /**
453- * Holds if the expression might overflow positively. Conversions
454- * are also taken into account. For example the expression
455- * `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than
456- * due to the addition.
457- */
458- cached
459- predicate convertedExprMightOverflowPositively ( Expr expr ) {
460- exprMightOverflowPositively ( expr ) or
461- convertedExprMightOverflowPositively ( expr .getConversion ( ) )
462- }
463-
464- /**
465- * Holds if the expression might overflow (either positively or
466- * negatively). The possibility that the expression might overflow
467- * due to an implicit or explicit cast is also considered.
468- */
469- cached
470- predicate convertedExprMightOverflow ( Expr expr ) {
471- convertedExprMightOverflowNegatively ( expr ) or
472- convertedExprMightOverflowPositively ( expr )
473- }
474-
475422/** Only to be called by `getTruncatedLowerBounds`. */
476423private
477424float getLowerBoundsImpl ( Expr expr ) {
@@ -921,28 +868,6 @@ float getDefUpperBoundsImpl(RangeSsaDefinition def, LocalScopeVariable v) {
921868 unanalyzableDefBounds ( def , v , _, result )
922869}
923870
924- /** Holds if the definition might overflow negatively. */
925- cached
926- predicate defMightOverflowNegatively ( RangeSsaDefinition def , LocalScopeVariable v ) {
927- getDefLowerBoundsImpl ( def , v ) < varMinVal ( v )
928- }
929-
930- /** Holds if the definition might overflow positively. */
931- cached
932- predicate defMightOverflowPositively ( RangeSsaDefinition def , LocalScopeVariable v ) {
933- getDefUpperBoundsImpl ( def , v ) > varMaxVal ( v )
934- }
935-
936- /**
937- * Holds if the definition might overflow (either positively or
938- * negatively).
939- */
940- cached
941- predicate defMightOverflow ( RangeSsaDefinition def , LocalScopeVariable v ) {
942- defMightOverflowNegatively ( def , v ) or
943- defMightOverflowPositively ( def , v )
944- }
945-
946871/**
947872 * Get the lower bounds for a `RangeSsaDefinition`. Most of the work is
948873 * done by `getDefLowerBoundsImpl`, but this is where widening is applied
@@ -1133,63 +1058,142 @@ predicate exprTypeBounds(Expr expr, float boundValue, boolean isLowerBound) {
11331058 ( isLowerBound = false and boundValue = exprMaxVal ( expr .getFullyConverted ( ) ) )
11341059}
11351060
1136- /**
1137- * Gets the lower bound of the expression.
1138- *
1139- * Note: expressions in C/C++ are often implicitly or explicitly cast to a
1140- * different result type. Such casts can cause the value of the expression
1141- * to overflow or to be truncated. This predicate computes the lower bound
1142- * of the expression without including the effect of the casts. To compute
1143- * the lower bound of the expression after all the casts have been applied,
1144- * call `lowerBound` like this:
1145- *
1146- * `lowerBound(expr.getFullyConverted())`
1147- */
1148- cached
1149- float lowerBound ( Expr expr ) {
1150- // Combine the lower bounds returned by getTruncatedLowerBounds into a
1151- // single minimum value.
1152- result = min ( float lb | lb = getTruncatedLowerBounds ( expr ) | lb )
1153- }
1154-
1155- /**
1156- * Gets the upper bound of the expression.
1157- *
1158- * Note: expressions in C/C++ are often implicitly or explicitly cast to a
1159- * different result type. Such casts can cause the value of the expression
1160- * to overflow or to be truncated. This predicate computes the upper bound
1161- * of the expression without including the effect of the casts. To compute
1162- * the upper bound of the expression after all the casts have been applied,
1163- * call `upperBound` like this:
1164- *
1165- * `upperBound(expr.getFullyConverted())`
1166- */
1167- cached
1168- float upperBound ( Expr expr ) {
1169- // Combine the upper bounds returned by getTruncatedUpperBounds into a
1170- // single maximum value.
1171- result = max ( float ub | ub = getTruncatedUpperBounds ( expr ) | ub )
1172- }
1061+ private cached module SimpleRangeAnalysisCached {
1062+ /**
1063+ * Gets the lower bound of the expression.
1064+ *
1065+ * Note: expressions in C/C++ are often implicitly or explicitly cast to a
1066+ * different result type. Such casts can cause the value of the expression
1067+ * to overflow or to be truncated. This predicate computes the lower bound
1068+ * of the expression without including the effect of the casts. To compute
1069+ * the lower bound of the expression after all the casts have been applied,
1070+ * call `lowerBound` like this:
1071+ *
1072+ * `lowerBound(expr.getFullyConverted())`
1073+ */
1074+ cached
1075+ float lowerBound ( Expr expr ) {
1076+ // Combine the lower bounds returned by getTruncatedLowerBounds into a
1077+ // single minimum value.
1078+ result = min ( float lb | lb = getTruncatedLowerBounds ( expr ) | lb )
1079+ }
1080+
1081+ /**
1082+ * Gets the upper bound of the expression.
1083+ *
1084+ * Note: expressions in C/C++ are often implicitly or explicitly cast to a
1085+ * different result type. Such casts can cause the value of the expression
1086+ * to overflow or to be truncated. This predicate computes the upper bound
1087+ * of the expression without including the effect of the casts. To compute
1088+ * the upper bound of the expression after all the casts have been applied,
1089+ * call `upperBound` like this:
1090+ *
1091+ * `upperBound(expr.getFullyConverted())`
1092+ */
1093+ cached
1094+ float upperBound ( Expr expr ) {
1095+ // Combine the upper bounds returned by getTruncatedUpperBounds into a
1096+ // single maximum value.
1097+ result = max ( float ub | ub = getTruncatedUpperBounds ( expr ) | ub )
1098+ }
1099+
1100+ /**
1101+ * Holds if `expr` has a provably empty range. For example:
1102+ *
1103+ * 10 < expr and expr < 5
1104+ *
1105+ * The range of an expression can only be empty if it can never be
1106+ * executed. For example:
1107+ *
1108+ * if (10 < x) {
1109+ * if (x < 5) {
1110+ * // Unreachable code
1111+ * return x; // x has an empty range: 10 < x && x < 5
1112+ * }
1113+ * }
1114+ */
1115+ cached
1116+ predicate exprWithEmptyRange ( Expr expr ) {
1117+ analyzableExpr ( expr ) and
1118+ ( not exists ( lowerBound ( expr ) ) or
1119+ not exists ( upperBound ( expr ) ) or
1120+ lowerBound ( expr ) > upperBound ( expr ) )
1121+ }
11731122
1174- /**
1175- * Holds if `expr` has a provably empty range. For example:
1176- *
1177- * 10 < expr and expr < 5
1178- *
1179- * The range of an expression can only be empty if it can never be
1180- * executed. For example:
1181- *
1182- * if (10 < x) {
1183- * if (x < 5) {
1184- * // Unreachable code
1185- * return x; // x has an empty range: 10 < x && x < 5
1186- * }
1187- * }
1188- */
1189- cached
1190- predicate exprWithEmptyRange ( Expr expr ) {
1191- analyzableExpr ( expr ) and
1192- ( not exists ( lowerBound ( expr ) ) or
1193- not exists ( upperBound ( expr ) ) or
1194- lowerBound ( expr ) > upperBound ( expr ) )
1123+ /** Holds if the definition might overflow negatively. */
1124+ cached
1125+ predicate defMightOverflowNegatively ( RangeSsaDefinition def , LocalScopeVariable v ) {
1126+ getDefLowerBoundsImpl ( def , v ) < varMinVal ( v )
1127+ }
1128+
1129+ /** Holds if the definition might overflow positively. */
1130+ cached
1131+ predicate defMightOverflowPositively ( RangeSsaDefinition def , LocalScopeVariable v ) {
1132+ getDefUpperBoundsImpl ( def , v ) > varMaxVal ( v )
1133+ }
1134+
1135+ /**
1136+ * Holds if the definition might overflow (either positively or
1137+ * negatively).
1138+ */
1139+ cached
1140+ predicate defMightOverflow ( RangeSsaDefinition def , LocalScopeVariable v ) {
1141+ defMightOverflowNegatively ( def , v ) or
1142+ defMightOverflowPositively ( def , v )
1143+ }
1144+
1145+ /**
1146+ * Holds if the expression might overflow negatively. This predicate
1147+ * does not consider the possibility that the expression might overflow
1148+ * due to a conversion.
1149+ */
1150+ cached
1151+ predicate exprMightOverflowNegatively ( Expr expr ) {
1152+ getLowerBoundsImpl ( expr ) < exprMinVal ( expr )
1153+ }
1154+
1155+ /**
1156+ * Holds if the expression might overflow negatively. Conversions
1157+ * are also taken into account. For example the expression
1158+ * `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than
1159+ * due to the addition.
1160+ */
1161+ cached
1162+ predicate convertedExprMightOverflowNegatively ( Expr expr ) {
1163+ exprMightOverflowNegatively ( expr ) or
1164+ convertedExprMightOverflowNegatively ( expr .getConversion ( ) )
1165+ }
1166+
1167+ /**
1168+ * Holds if the expression might overflow positively. This predicate
1169+ * does not consider the possibility that the expression might overflow
1170+ * due to a conversion.
1171+ */
1172+ cached
1173+ predicate exprMightOverflowPositively ( Expr expr ) {
1174+ getUpperBoundsImpl ( expr ) > exprMaxVal ( expr )
1175+ }
1176+
1177+ /**
1178+ * Holds if the expression might overflow positively. Conversions
1179+ * are also taken into account. For example the expression
1180+ * `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than
1181+ * due to the addition.
1182+ */
1183+ cached
1184+ predicate convertedExprMightOverflowPositively ( Expr expr ) {
1185+ exprMightOverflowPositively ( expr ) or
1186+ convertedExprMightOverflowPositively ( expr .getConversion ( ) )
1187+ }
1188+
1189+ /**
1190+ * Holds if the expression might overflow (either positively or
1191+ * negatively). The possibility that the expression might overflow
1192+ * due to an implicit or explicit cast is also considered.
1193+ */
1194+ cached
1195+ predicate convertedExprMightOverflow ( Expr expr ) {
1196+ convertedExprMightOverflowNegatively ( expr ) or
1197+ convertedExprMightOverflowPositively ( expr )
1198+ }
11951199}
0 commit comments