@@ -221,13 +221,7 @@ module Trees {
221221 or
222222 last ( super .getProcessBlock ( ) , pred , c ) and
223223 completionIsNormal ( c ) and
224- (
225- // If we process multiple items we will loop back to the process block
226- first ( super .getProcessBlock ( ) , succ )
227- or
228- // Once we're done process all items we will go to the end block
229- first ( super .getEndBlock ( ) , succ )
230- )
224+ first ( super .getEndBlock ( ) , succ )
231225 }
232226
233227 final override predicate propagatesAbnormal ( AstNode child ) {
@@ -292,25 +286,17 @@ module Trees {
292286 final override predicate succEntry ( Ast n , Completion c ) { n = this and completionIsSimple ( c ) }
293287 }
294288
295- abstract class NamedBlockTreeBase extends ControlFlowTree instanceof NamedBlock {
296- final override predicate last ( Ast last , Completion c ) {
289+ abstract class NamedBlockTreeBase extends PreOrderTree instanceof NamedBlock {
290+ override predicate last ( Ast last , Completion c ) {
297291 exists ( int i | last ( super .getStmt ( i ) , last , c ) |
298292 completionIsNormal ( c ) and
299293 not exists ( super .getStmt ( i + 1 ) )
300294 or
301295 not completionIsNormal ( c )
302296 )
303- or
304- not exists ( super .getAStmt ( ) ) and
305- completionIsSimple ( c ) and
306- last = this
307297 }
308298
309299 override predicate succ ( Ast pred , Ast succ , Completion c ) {
310- pred = this and
311- completionIsSimple ( c ) and
312- first ( super .getStmt ( 0 ) , succ )
313- or
314300 exists ( int i |
315301 last ( super .getStmt ( i ) , pred , c ) and
316302 completionIsNormal ( c ) and
@@ -324,20 +310,85 @@ module Trees {
324310 class NamedBlockTree extends NamedBlockTreeBase instanceof NamedBlock {
325311 NamedBlockTree ( ) { not this instanceof ProcessBlock }
326312
327- final override predicate first ( Ast first ) { first = this }
313+ final override predicate last ( Ast last , Completion c ) {
314+ super .last ( last , c )
315+ or
316+ not exists ( super .getAStmt ( ) ) and
317+ completionIsSimple ( c ) and
318+ last = this
319+ }
320+
321+ final override predicate succ ( Ast pred , Ast succ , Completion c ) {
322+ pred = this and
323+ completionIsSimple ( c ) and
324+ first ( super .getStmt ( 0 ) , succ )
325+ or
326+ super .succ ( pred , succ , c )
327+ }
328328
329329 final override predicate propagatesAbnormal ( Ast child ) { super .propagatesAbnormal ( child ) }
330330 }
331331
332+ private VarAccess getRankedPipelineByPropertyNameVariable ( ProcessBlock pb , int i ) {
333+ result =
334+ rank [ i + 1 ] ( string name | | pb .getPipelineByPropertyNameParameterAccess ( name ) order by name )
335+ }
336+
332337 class ProcessBlockTree extends NamedBlockTreeBase instanceof ProcessBlock {
333- final override predicate first ( Ast first ) { first = super .getPipelineParameterAccess ( ) }
338+ predicate lastEmptinessCheck ( AstNode last ) {
339+ last = super .getPipelineParameterAccess ( ) and
340+ not exists ( super .getAPipelineByPropertyNameParameterAccess ( ) )
341+ or
342+ exists ( int i |
343+ last = getRankedPipelineByPropertyNameVariable ( this , i ) and
344+ not exists ( getRankedPipelineByPropertyNameVariable ( this , i + 1 ) )
345+ )
346+ }
347+
348+ private predicate succEmptinessCheck ( AstNode pred , AstNode succ , Completion c ) {
349+ last ( super .getPipelineParameterAccess ( ) , pred , c ) and
350+ first ( getRankedPipelineByPropertyNameVariable ( this , 0 ) , succ )
351+ or
352+ exists ( int i |
353+ last ( getRankedPipelineByPropertyNameVariable ( this , i ) , pred , c ) and
354+ first ( getRankedPipelineByPropertyNameVariable ( this , i + 1 ) , succ )
355+ )
356+ }
357+
358+ private predicate firstEmptinessCheck ( AstNode first ) {
359+ first ( super .getPipelineParameterAccess ( ) , first )
360+ }
361+
362+ final override predicate last ( AstNode last , Completion c ) {
363+ // Emptiness test exits with no more elements
364+ this .lastEmptinessCheck ( last ) and
365+ c .( EmptinessCompletion ) .isEmpty ( )
366+ or
367+ super .last ( last , c )
368+ }
334369
335370 final override predicate succ ( Ast pred , Ast succ , Completion c ) {
336- this .first ( pred ) and
337- completionIsSimple ( c ) and
338- succ = this
371+ // Evaluate the pipeline access
372+ pred = this and
373+ this .firstEmptinessCheck ( succ ) and
374+ completionIsSimple ( c )
375+ or
376+ this .succEmptinessCheck ( pred , succ , c )
377+ or
378+ this .lastEmptinessCheck ( pred ) and
379+ c = any ( EmptinessCompletion ec | not ec .isEmpty ( ) ) and
380+ first ( super .getStmt ( 0 ) , succ )
339381 or
340382 super .succ ( pred , succ , c )
383+ or
384+ // Body to emptiness test
385+ exists ( Ast last0 |
386+ super .last ( last0 , _) and
387+ last ( last0 , pred , c ) and
388+ // TODO: I don't think this correctly models the semantics inside process blocks
389+ c .continuesLoop ( )
390+ ) and
391+ this .firstEmptinessCheck ( succ )
341392 }
342393
343394 final override predicate propagatesAbnormal ( Ast child ) { super .propagatesAbnormal ( child ) }
0 commit comments