@@ -261,6 +261,10 @@ module KindPredicatesLog {
261
261
float getCompletionTime ( ) { result = stringToTimestamp ( this .getCompletionTimeString ( ) ) }
262
262
263
263
float getResultSize ( ) { result = this .getFloat ( "resultSize" ) }
264
+
265
+ Array getRA ( string ordering ) { result = this .getObject ( "ra" ) .getArray ( ordering ) }
266
+
267
+ string getAnOrdering ( ) { exists ( this .getRA ( result ) ) }
264
268
}
265
269
266
270
class SentinelEmpty extends SummaryEvent {
@@ -317,12 +321,162 @@ module KindPredicatesLog {
317
321
Predicate getPredicate ( ) { result = getPredicateFromPosition ( this .getPosition ( ) ) }
318
322
}
319
323
324
+ /** Gets the `index`'th event that's evaluated by `recursive`. */
325
+ private InLayer layerEventRank ( ComputeRecursive recursive , int index ) {
326
+ result =
327
+ rank [ index + 1 ] ( InLayer cand , int startline , string filepath |
328
+ cand .getComputeRecursiveEvent ( ) = recursive and
329
+ cand .hasLocationInfo ( filepath , startline , _, _, _)
330
+ |
331
+ cand order by filepath , startline
332
+ )
333
+ }
334
+
335
+ /**
336
+ * Gets the first predicate that's evaluated in an iteration
337
+ * of the SCC computation rooted at `recursive`.
338
+ */
339
+ private InLayer firstPredicate ( ComputeRecursive recursive ) {
340
+ result = layerEventRank ( recursive , 0 )
341
+ }
342
+
343
+ /**
344
+ * Gets the last predicate that's evaluated in an iteration
345
+ * of the SCC computation rooted at `recursive`.
346
+ */
347
+ private InLayer lastPredicate ( ComputeRecursive recursive ) {
348
+ exists ( int n |
349
+ result = layerEventRank ( recursive , n ) and
350
+ not exists ( layerEventRank ( recursive , n + 1 ) )
351
+ )
352
+ }
353
+
354
+ /**
355
+ * Holds if the predicate represented by `next` was evaluated after the
356
+ * predicate represented by `prev` in the SCC computation rooted at `recursive`.
357
+ */
358
+ predicate successor ( ComputeRecursive recursive , InLayer prev , InLayer next ) {
359
+ exists ( int index |
360
+ layerEventRank ( recursive , index ) = prev and
361
+ layerEventRank ( recursive , index + 1 ) = next
362
+ )
363
+ }
364
+
365
+ /**
366
+ * Holds if the predicate represented by `inLayer` was run in the `iteration`'iteration
367
+ * of the SCC computation rooted at `recursive`.
368
+ */
369
+ private predicate ran ( ComputeRecursive recursive , int iteration , InLayer inLayer ) {
370
+ exists ( int index |
371
+ inLayer = layerEventRank ( recursive , index ) and
372
+ inLayer .getPredicateIterationMillis ( ) .getNumber ( iteration ) >= 0
373
+ )
374
+ }
375
+
376
+ /**
377
+ * Gets the next iteration in which the predicate `pred` in the `iteration`'th iteration
378
+ * of a recursive SCC rooted at `recursive` should be evaluated.
379
+ */
380
+ int nextPipeline ( ComputeRecursive recursive , int iteration , InLayer inLayer ) {
381
+ iteration = 0 and
382
+ if ran ( recursive , iteration , inLayer ) then result = 1 else result = 0
383
+ or
384
+ iteration > 1 and
385
+ exists ( int n | n = nextPipeline ( recursive , iteration - 1 , inLayer ) |
386
+ if ran ( recursive , iteration , inLayer ) then result = n + 1 else result = n
387
+ )
388
+ }
389
+
390
+ bindingset [ this ]
391
+ signature class ResultSig ;
392
+
393
+ /**
394
+ * A signature for generically traversing a SCC computation.
395
+ */
396
+ signature module Fold< ResultSig R> {
397
+ /**
398
+ * Gets the base case for the fold. That is, the initial value that
399
+ * is produced from the first evaluation of the first IN_LAYER event
400
+ * in the recursive evaluation.
401
+ */
402
+ bindingset [ run]
403
+ R base ( PipeLineRun run ) ;
404
+
405
+ /**
406
+ * Gets the recursive case for the fold. That is, `r` is the accumulation
407
+ * of the previous evaluations, and `run` is the pipeline of the next IN_LAYER
408
+ * event that is evaluated.
409
+ */
410
+ bindingset [ run, r]
411
+ R fold ( PipeLineRun run , R r ) ;
412
+ }
413
+
414
+ module Iterate< ResultSig R, Fold< R > F> {
415
+ private R iterate ( ComputeRecursive recursive , int iteration , InLayer pred ) {
416
+ // Case: The first iteration
417
+ iteration = 0 and
418
+ (
419
+ // Subcase: The first predicate in the first iteration
420
+ pred = firstPredicate ( recursive ) and
421
+ result = F:: base ( pred .getPipelineRuns ( ) .getRun ( 0 ) )
422
+ or
423
+ // Subcase: The predicate has a predecessor
424
+ exists ( InLayer pred0 , R r |
425
+ successor ( recursive , pred0 , pred ) and
426
+ r = iterate ( recursive , 0 , pred0 ) and
427
+ result = F:: fold ( pred .getPipelineRuns ( ) .getRun ( 0 ) , r )
428
+ )
429
+ )
430
+ or
431
+ // Case: Not the first iteration
432
+ iteration > 0 and
433
+ (
434
+ // Subcase: The first predicate in the iteration
435
+ pred = firstPredicate ( recursive ) and
436
+ exists ( InLayer last , R r |
437
+ last = lastPredicate ( recursive ) and
438
+ r = iterate ( recursive , iteration - 1 , last ) and
439
+ result = F:: fold ( pred .getPipelineRuns ( ) .getRun ( iteration ) , r )
440
+ )
441
+ or
442
+ // Subcase: The predicate has a predecessor in the same iteration
443
+ exists ( InLayer pred0 , R r |
444
+ successor ( recursive , pred0 , pred ) and
445
+ r = iterate ( recursive , iteration , pred0 ) and
446
+ result = F:: fold ( pred .getPipelineRuns ( ) .getRun ( iteration ) , r )
447
+ )
448
+ )
449
+ }
450
+
451
+ R iterate ( ComputeRecursive recursive ) {
452
+ exists ( int iteration , InLayer pred |
453
+ pred = lastPredicate ( recursive ) and
454
+ result = iterate ( recursive , iteration , pred ) and
455
+ not exists ( iterate ( recursive , iteration + 1 , pred ) )
456
+ )
457
+ }
458
+ }
459
+
320
460
class ComputeRecursive extends SummaryEvent {
321
461
ComputeRecursive ( ) { evaluationStrategy = "COMPUTE_RECURSIVE" }
322
462
}
323
463
324
464
class InLayer extends SummaryEvent {
325
465
InLayer ( ) { evaluationStrategy = "IN_LAYER" }
466
+
467
+ string getMainHash ( ) { result = this .getString ( "mainHash" ) }
468
+
469
+ ComputeRecursive getComputeRecursiveEvent ( ) { result .getRAHash ( ) = this .getMainHash ( ) }
470
+
471
+ Array getPredicateIterationMillis ( ) { result = this .getArray ( "predicateIterationMillis" ) }
472
+
473
+ float getPredicateIterationMillis ( int i ) {
474
+ result = getRanked ( this .getArray ( "predicateIterationMillis" ) , i )
475
+ }
476
+
477
+ PipeLineRuns getPipelineRuns ( ) { result = this .getArray ( "pipelineRuns" ) }
478
+
479
+ float getDeltaSize ( int i ) { result = getRanked ( this .getArray ( "deltaSizes" ) , i ) }
326
480
}
327
481
328
482
class ComputedExtensional extends SummaryEvent {
0 commit comments