|
44 | 44 | import cpp |
45 | 45 | private import RangeAnalysisUtils |
46 | 46 | import RangeSSA |
| 47 | +import SimpleRangeAnalysisCached |
47 | 48 |
|
48 | 49 | /** |
49 | 50 | * This fixed set of lower bounds is used when the lower bounds of an |
@@ -921,28 +922,6 @@ float getDefUpperBoundsImpl(RangeSsaDefinition def, LocalScopeVariable v) { |
921 | 922 | unanalyzableDefBounds(def, v, _, result) |
922 | 923 | } |
923 | 924 |
|
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 | | - |
946 | 925 | /** |
947 | 926 | * Get the lower bounds for a `RangeSsaDefinition`. Most of the work is |
948 | 927 | * done by `getDefLowerBoundsImpl`, but this is where widening is applied |
@@ -1133,63 +1112,87 @@ predicate exprTypeBounds(Expr expr, float boundValue, boolean isLowerBound) { |
1133 | 1112 | (isLowerBound = false and boundValue = exprMaxVal(expr.getFullyConverted())) |
1134 | 1113 | } |
1135 | 1114 |
|
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 | | -} |
| 1115 | +private cached module SimpleRangeAnalysisCached { |
| 1116 | + /** |
| 1117 | + * Gets the lower bound of the expression. |
| 1118 | + * |
| 1119 | + * Note: expressions in C/C++ are often implicitly or explicitly cast to a |
| 1120 | + * different result type. Such casts can cause the value of the expression |
| 1121 | + * to overflow or to be truncated. This predicate computes the lower bound |
| 1122 | + * of the expression without including the effect of the casts. To compute |
| 1123 | + * the lower bound of the expression after all the casts have been applied, |
| 1124 | + * call `lowerBound` like this: |
| 1125 | + * |
| 1126 | + * `lowerBound(expr.getFullyConverted())` |
| 1127 | + */ |
| 1128 | + cached |
| 1129 | + float lowerBound(Expr expr) { |
| 1130 | + // Combine the lower bounds returned by getTruncatedLowerBounds into a |
| 1131 | + // single minimum value. |
| 1132 | + result = min(float lb | lb = getTruncatedLowerBounds(expr) | lb) |
| 1133 | + } |
| 1134 | + |
| 1135 | + /** |
| 1136 | + * Gets the upper bound of the expression. |
| 1137 | + * |
| 1138 | + * Note: expressions in C/C++ are often implicitly or explicitly cast to a |
| 1139 | + * different result type. Such casts can cause the value of the expression |
| 1140 | + * to overflow or to be truncated. This predicate computes the upper bound |
| 1141 | + * of the expression without including the effect of the casts. To compute |
| 1142 | + * the upper bound of the expression after all the casts have been applied, |
| 1143 | + * call `upperBound` like this: |
| 1144 | + * |
| 1145 | + * `upperBound(expr.getFullyConverted())` |
| 1146 | + */ |
| 1147 | + cached |
| 1148 | + float upperBound(Expr expr) { |
| 1149 | + // Combine the upper bounds returned by getTruncatedUpperBounds into a |
| 1150 | + // single maximum value. |
| 1151 | + result = max(float ub | ub = getTruncatedUpperBounds(expr) | ub) |
| 1152 | + } |
| 1153 | + |
| 1154 | + /** |
| 1155 | + * Holds if `expr` has a provably empty range. For example: |
| 1156 | + * |
| 1157 | + * 10 < expr and expr < 5 |
| 1158 | + * |
| 1159 | + * The range of an expression can only be empty if it can never be |
| 1160 | + * executed. For example: |
| 1161 | + * |
| 1162 | + * if (10 < x) { |
| 1163 | + * if (x < 5) { |
| 1164 | + * // Unreachable code |
| 1165 | + * return x; // x has an empty range: 10 < x && x < 5 |
| 1166 | + * } |
| 1167 | + * } |
| 1168 | + */ |
| 1169 | + cached |
| 1170 | + predicate exprWithEmptyRange(Expr expr) { |
| 1171 | + analyzableExpr(expr) and |
| 1172 | + (not exists(lowerBound(expr)) or |
| 1173 | + not exists(upperBound(expr)) or |
| 1174 | + lowerBound(expr) > upperBound(expr)) |
| 1175 | + } |
1173 | 1176 |
|
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)) |
| 1177 | + /** Holds if the definition might overflow negatively. */ |
| 1178 | + cached |
| 1179 | + predicate defMightOverflowNegatively(RangeSsaDefinition def, LocalScopeVariable v) { |
| 1180 | + getDefLowerBoundsImpl(def, v) < varMinVal(v) |
| 1181 | + } |
| 1182 | + |
| 1183 | + /** Holds if the definition might overflow positively. */ |
| 1184 | + cached |
| 1185 | + predicate defMightOverflowPositively(RangeSsaDefinition def, LocalScopeVariable v) { |
| 1186 | + getDefUpperBoundsImpl(def, v) > varMaxVal(v) |
| 1187 | + } |
| 1188 | + |
| 1189 | + /** |
| 1190 | + * Holds if the definition might overflow (either positively or |
| 1191 | + * negatively). |
| 1192 | + */ |
| 1193 | + cached |
| 1194 | + predicate defMightOverflow(RangeSsaDefinition def, LocalScopeVariable v) { |
| 1195 | + defMightOverflowNegatively(def, v) or |
| 1196 | + defMightOverflowPositively(def, v) |
| 1197 | + } |
1195 | 1198 | } |
0 commit comments