@@ -236,6 +236,164 @@ module Trees {
236
236
}
237
237
}
238
238
239
+ abstract class LoopStmtTree extends ControlFlowTree instanceof LoopStmt {
240
+ final AstNode getBody ( ) { result = super .getBody ( ) }
241
+
242
+ override predicate last ( AstNode last , Completion c ) {
243
+ // Exit the loop body when we encounter a break
244
+ last ( this .getBody ( ) , last , c ) and
245
+ c instanceof BreakCompletion
246
+ or
247
+ // Body exits abnormally
248
+ last ( this .getBody ( ) , last , c ) and
249
+ not c instanceof BreakCompletion and
250
+ not c .continuesLoop ( )
251
+ }
252
+ }
253
+
254
+ abstract class ConditionalLoopStmtTree extends PreOrderTree , LoopStmtTree {
255
+ abstract AstNode getCondition ( ) ;
256
+
257
+ abstract predicate entersLoopWhenConditionIs ( boolean value ) ;
258
+
259
+ final override predicate propagatesAbnormal ( AstNode child ) { child = this .getCondition ( ) }
260
+
261
+ override predicate last ( AstNode last , Completion c ) {
262
+ // Exit the loop body when the condition is false
263
+ last ( this .getCondition ( ) , last , c ) and
264
+ this .entersLoopWhenConditionIs ( c .( BooleanCompletion ) .getValue ( ) .booleanNot ( ) )
265
+ or
266
+ super .last ( last , c )
267
+ }
268
+
269
+ override predicate succ ( AstNode pred , AstNode succ , Completion c ) {
270
+ // Condition -> body
271
+ last ( this .getCondition ( ) , pred , c ) and
272
+ this .entersLoopWhenConditionIs ( c .( BooleanCompletion ) .getValue ( ) ) and
273
+ first ( this .getBody ( ) , succ )
274
+ or
275
+ // Body -> condition
276
+ last ( this .getBody ( ) , pred , c ) and
277
+ c .continuesLoop ( ) and
278
+ first ( this .getCondition ( ) , succ )
279
+ }
280
+ }
281
+
282
+ class WhileStmtTree extends ConditionalLoopStmtTree instanceof WhileStmt {
283
+ override predicate entersLoopWhenConditionIs ( boolean value ) { value = true }
284
+
285
+ override AstNode getCondition ( ) { result = WhileStmt .super .getCondition ( ) }
286
+
287
+ final override predicate succ ( AstNode pred , AstNode succ , Completion c ) {
288
+ // Start with the condition
289
+ this = pred and
290
+ first ( this .getCondition ( ) , succ ) and
291
+ completionIsSimple ( c )
292
+ or
293
+ super .succ ( pred , succ , c )
294
+ }
295
+ }
296
+
297
+ abstract class DoBasedLoopStmtTree extends ConditionalLoopStmtTree {
298
+ final override predicate succ ( AstNode pred , AstNode succ , Completion c ) {
299
+ // Start with the body
300
+ this = pred and
301
+ first ( this .getBody ( ) , succ ) and
302
+ completionIsSimple ( c )
303
+ or
304
+ super .succ ( pred , succ , c )
305
+ }
306
+ }
307
+
308
+ class DoWhileStmtTree extends DoBasedLoopStmtTree instanceof DoWhileStmt {
309
+ override AstNode getCondition ( ) { result = DoWhileStmt .super .getCondition ( ) }
310
+
311
+ override predicate entersLoopWhenConditionIs ( boolean value ) { value = true }
312
+ }
313
+
314
+ class DoUntilStmtTree extends DoBasedLoopStmtTree instanceof DoUntilStmt {
315
+ override AstNode getCondition ( ) { result = DoUntilStmt .super .getCondition ( ) }
316
+
317
+ override predicate entersLoopWhenConditionIs ( boolean value ) { value = false }
318
+ }
319
+
320
+ class ForStmtTree extends PreOrderTree , LoopStmtTree instanceof ForStmt {
321
+ final override predicate propagatesAbnormal ( AstNode child ) {
322
+ child = [ super .getInitializer ( ) , super .getIterator ( ) ]
323
+ }
324
+
325
+ override predicate last ( AstNode last , Completion c ) {
326
+ // Condition returns false
327
+ last ( super .getCondition ( ) , last , c ) and
328
+ c instanceof FalseCompletion
329
+ or
330
+ super .last ( last , c )
331
+ }
332
+
333
+ final override predicate succ ( AstNode pred , AstNode succ , Completion c ) {
334
+ // Start with initialization
335
+ this = pred and
336
+ first ( super .getInitializer ( ) , succ ) and
337
+ completionIsSimple ( c )
338
+ or
339
+ // Initialization -> condition
340
+ last ( super .getInitializer ( ) , pred , c ) and
341
+ completionIsNormal ( c ) and
342
+ first ( super .getCondition ( ) , succ )
343
+ or
344
+ // Condition -> body
345
+ last ( super .getCondition ( ) , pred , c ) and
346
+ c instanceof TrueCompletion and
347
+ first ( this .getBody ( ) , succ )
348
+ or
349
+ // Body -> iterator
350
+ last ( this .getBody ( ) , pred , c ) and
351
+ completionIsNormal ( c ) and
352
+ first ( super .getIterator ( ) , succ )
353
+ }
354
+ }
355
+
356
+ class ForEachStmtTree extends LoopStmtTree instanceof ForEachStmt {
357
+ final override predicate propagatesAbnormal ( AstNode child ) { child = super .getIterableExpr ( ) }
358
+
359
+ final override predicate first ( AstNode first ) {
360
+ // Unlike most other statements, `foreach` statements are not modeled in
361
+ // pre-order, because we use the `foreach` node itself to represent the
362
+ // emptiness test that determines whether to execute the loop body
363
+ first ( super .getIterableExpr ( ) , first )
364
+ }
365
+
366
+ final override predicate last ( AstNode last , Completion c ) {
367
+ // Emptiness test exits with no more elements
368
+ last = this and
369
+ completionIsSimple ( c )
370
+ or
371
+ super .last ( last , c )
372
+ }
373
+
374
+ final override predicate succ ( AstNode pred , AstNode succ , Completion c ) {
375
+ // Emptiness test
376
+ last ( super .getIterableExpr ( ) , pred , c ) and
377
+ completionIsNormal ( c ) and
378
+ succ = this
379
+ or
380
+ // Emptiness test to variable declaration
381
+ pred = this and
382
+ first ( super .getVariable ( ) , succ ) and
383
+ completionIsSimple ( c )
384
+ or
385
+ // Variable declaration to body
386
+ last ( super .getVariable ( ) , succ , c ) and
387
+ completionIsNormal ( c ) and
388
+ first ( this .getBody ( ) , succ )
389
+ or
390
+ // Body to emptiness test
391
+ last ( this .getBody ( ) , pred , c ) and
392
+ c .continuesLoop ( ) and
393
+ succ = this
394
+ }
395
+ }
396
+
239
397
class StmtBlockTree extends PreOrderTree instanceof StmtBlock {
240
398
final override predicate propagatesAbnormal ( AstNode child ) { child = super .getAStmt ( ) }
241
399
0 commit comments