@@ -37,6 +37,8 @@ signature module InputSig<LocationSig Location> {
37
37
string toString ( ) ;
38
38
}
39
39
40
+ class ExceptionSuccessor extends SuccessorType ;
41
+
40
42
class ConditionalSuccessor extends SuccessorType {
41
43
/** Gets the Boolean value of this successor. */
42
44
boolean getValue ( ) ;
@@ -187,7 +189,8 @@ module Make<LocationSig Location, InputSig<Location> Input> {
187
189
188
190
private newtype TGuardValue =
189
191
TValue ( TAbstractSingleValue val , Boolean isVal ) or
190
- TCaseMatch ( Case c , Boolean match )
192
+ TCaseMatch ( Case c , Boolean match ) or
193
+ TException ( Boolean throws )
191
194
192
195
private class AbstractSingleValue extends TAbstractSingleValue {
193
196
/** Gets a textual representation of this value. */
@@ -221,6 +224,11 @@ module Make<LocationSig Location, InputSig<Location> Input> {
221
224
this = TCaseMatch ( c , match ) and
222
225
result = TCaseMatch ( c , match .booleanNot ( ) )
223
226
)
227
+ or
228
+ exists ( boolean throws |
229
+ this = TException ( throws ) and
230
+ result = TException ( throws .booleanNot ( ) )
231
+ )
224
232
}
225
233
226
234
/** Holds if this value represents `null`. */
@@ -235,6 +243,9 @@ module Make<LocationSig Location, InputSig<Location> Input> {
235
243
/** Gets the constant that this value represents, if any. */
236
244
ConstantValue asConstantValue ( ) { this = TValue ( TValueConstant ( result ) , true ) }
237
245
246
+ /** Holds if this value represents throwing an exception. */
247
+ predicate isThrowsException ( ) { this = TException ( true ) }
248
+
238
249
/** Gets a textual representation of this value. */
239
250
string toString ( ) {
240
251
result = this .asBooleanValue ( ) .toString ( )
@@ -257,6 +268,12 @@ module Make<LocationSig Location, InputSig<Location> Input> {
257
268
match = false and result = "non-match " + s
258
269
)
259
270
)
271
+ or
272
+ exists ( boolean throws | this = TException ( throws ) |
273
+ throws = true and result = "exception"
274
+ or
275
+ throws = false and result = "no exception"
276
+ )
260
277
}
261
278
}
262
279
@@ -288,6 +305,15 @@ module Make<LocationSig Location, InputSig<Location> Input> {
288
305
e instanceof NonNullExpr and v = TValue ( TValueNull ( ) , false )
289
306
}
290
307
308
+ private predicate exceptionBranchPoint ( BasicBlock bb1 , BasicBlock normalSucc , BasicBlock excSucc ) {
309
+ exists ( SuccessorType norm , ExceptionSuccessor exc |
310
+ bb1 .getASuccessor ( norm ) = normalSucc and
311
+ bb1 .getASuccessor ( exc ) = excSucc and
312
+ normalSucc != excSucc and
313
+ not norm instanceof ExceptionSuccessor
314
+ )
315
+ }
316
+
291
317
private predicate branchEdge ( BasicBlock bb1 , BasicBlock bb2 , GuardValue v ) {
292
318
exists ( ConditionalSuccessor s |
293
319
bb1 .getASuccessor ( s ) = bb2 and
@@ -307,6 +333,10 @@ module Make<LocationSig Location, InputSig<Location> Input> {
307
333
v = TCaseMatch ( c , false ) and
308
334
c .nonMatchEdge ( bb1 , bb2 )
309
335
)
336
+ or
337
+ exceptionBranchPoint ( bb1 , bb2 , _) and v = TException ( false )
338
+ or
339
+ exceptionBranchPoint ( bb1 , _, bb2 ) and v = TException ( true )
310
340
}
311
341
312
342
pragma [ nomagic]
@@ -399,7 +429,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
399
429
bindingset [ g1, v1]
400
430
pragma [ inline_late]
401
431
private predicate unboundBaseImpliesStep ( PreGuard g1 , GuardValue v1 , PreGuard g2 , GuardValue v2 ) {
402
- g1 .( IdExpr ) .getEqualChildExpr ( ) = g2 and v1 = v2
432
+ g1 .( IdExpr ) .getEqualChildExpr ( ) = g2 and v1 = v2 and not v1 instanceof TException
403
433
or
404
434
exists ( ConditionalExpr cond , boolean branch , Expr e , GuardValue ev |
405
435
cond = g1 and
0 commit comments