@@ -347,183 +347,172 @@ float getALowerBound(Expr expr) {
347
347
* Gets a possible upper bound of SSA definition `def`.
348
348
*/
349
349
float getAnSsaUpperBound ( SsaDefinition def ) {
350
- if recursiveSelfDef ( def )
351
- then none ( )
352
- else (
353
- if def instanceof SsaExplicitDefinition
354
- then
355
- exists ( SsaExplicitDefinition explicitDef | explicitDef = def |
356
- //SSA definition coresponding to a `SimpleAssignStmt`
357
- if explicitDef .getInstruction ( ) instanceof IR:: AssignInstruction
358
- then
359
- exists ( IR:: AssignInstruction assignInstr , SimpleAssignStmt simpleAssign |
360
- assignInstr = explicitDef .getInstruction ( ) and
361
- assignInstr .getRhs ( ) .( IR:: EvalInstruction ) .getExpr ( ) = simpleAssign .getRhs ( ) and
362
- result = getAnUpperBound ( simpleAssign .getRhs ( ) )
363
- )
364
- or
365
- //SSA definition coresponding to a ValueSpec(used in a variable declaration)
366
- exists ( IR:: AssignInstruction declInstr , ValueSpec vs , int i , Expr init |
367
- declInstr = explicitDef .getInstruction ( ) and
368
- declInstr = IR:: initInstruction ( vs , i ) and
369
- init = vs .getInit ( i ) and
370
- result = getAnUpperBound ( init )
371
- )
372
- or
373
- //SSA definition coresponding to an `AddAssignStmt` (x += y) or `SubAssignStmt` (x -= y)
374
- exists (
375
- IR:: AssignInstruction assignInstr , SsaExplicitDefinition prevDef ,
376
- CompoundAssignStmt compoundAssign , float prevBound , float delta
377
- |
378
- assignInstr = explicitDef .getInstruction ( ) and
379
- getAUse ( prevDef ) = compoundAssign .getLhs ( ) and
380
- assignInstr = IR:: assignInstruction ( compoundAssign , 0 ) and
381
- prevBound = getAnSsaUpperBound ( prevDef ) and
382
- if compoundAssign instanceof AddAssignStmt
383
- then
384
- delta = getAnUpperBound ( compoundAssign .getRhs ( ) ) and
385
- result = addRoundingUp ( prevBound , delta )
386
- else
387
- if compoundAssign instanceof SubAssignStmt
388
- then
389
- delta = getALowerBound ( compoundAssign .getRhs ( ) ) and
390
- result = addRoundingUp ( prevBound , - delta )
391
- else none ( )
392
- )
393
- else
394
- //SSA definition coresponding to an `IncDecStmt`
395
- if explicitDef .getInstruction ( ) instanceof IR:: IncDecInstruction
350
+ not recursiveSelfDef ( def ) and
351
+ (
352
+ def instanceof SsaExplicitDefinition and
353
+ exists ( SsaExplicitDefinition explicitDef | explicitDef = def |
354
+ //SSA definition coresponding to a `SimpleAssignStmt`
355
+ if explicitDef .getInstruction ( ) instanceof IR:: AssignInstruction
356
+ then
357
+ exists ( IR:: AssignInstruction assignInstr , SimpleAssignStmt simpleAssign |
358
+ assignInstr = explicitDef .getInstruction ( ) and
359
+ assignInstr .getRhs ( ) .( IR:: EvalInstruction ) .getExpr ( ) = simpleAssign .getRhs ( ) and
360
+ result = getAnUpperBound ( simpleAssign .getRhs ( ) )
361
+ )
362
+ or
363
+ //SSA definition coresponding to a ValueSpec(used in a variable declaration)
364
+ exists ( IR:: AssignInstruction declInstr , ValueSpec vs , int i , Expr init |
365
+ declInstr = explicitDef .getInstruction ( ) and
366
+ declInstr = IR:: initInstruction ( vs , i ) and
367
+ init = vs .getInit ( i ) and
368
+ result = getAnUpperBound ( init )
369
+ )
370
+ or
371
+ //SSA definition coresponding to an `AddAssignStmt` (x += y) or `SubAssignStmt` (x -= y)
372
+ exists (
373
+ IR:: AssignInstruction assignInstr , SsaExplicitDefinition prevDef ,
374
+ CompoundAssignStmt compoundAssign , float prevBound , float delta
375
+ |
376
+ assignInstr = explicitDef .getInstruction ( ) and
377
+ getAUse ( prevDef ) = compoundAssign .getLhs ( ) and
378
+ assignInstr = IR:: assignInstruction ( compoundAssign , 0 ) and
379
+ prevBound = getAnSsaUpperBound ( prevDef ) and
380
+ if compoundAssign instanceof AddAssignStmt
396
381
then
397
- exists ( IncDecStmt incOrDec , IR:: IncDecInstruction instr , float exprLB |
398
- instr = explicitDef .getInstruction ( ) and
399
- exprLB = getAnUpperBound ( incOrDec .getOperand ( ) ) and
400
- instr .getRhs ( ) .( IR:: EvalIncDecRhsInstruction ) .getStmt ( ) = incOrDec and
401
- (
402
- //IncStmt(x++)
403
- exists ( IncStmt inc |
404
- inc = incOrDec and
405
- result = addRoundingUp ( exprLB , 1 )
406
- )
407
- or
408
- //DecStmt(x--)
409
- exists ( DecStmt dec |
410
- dec = incOrDec and
411
- result = addRoundingUp ( exprLB , - 1 )
412
- )
413
- )
414
- )
382
+ delta = getAnUpperBound ( compoundAssign .getRhs ( ) ) and
383
+ result = addRoundingUp ( prevBound , delta )
415
384
else
416
- //SSA definition coreponding to the init of the parameter
417
- if explicitDef .getInstruction ( ) instanceof IR:: InitParameterInstruction
385
+ if compoundAssign instanceof SubAssignStmt
418
386
then
419
- exists ( IR:: InitParameterInstruction instr , Parameter p |
420
- instr = explicitDef .getInstruction ( ) and
421
- IR:: initParamInstruction ( p ) = instr and
422
- result = typeMaxValue ( p .getType ( ) )
423
- )
387
+ delta = getALowerBound ( compoundAssign .getRhs ( ) ) and
388
+ result = addRoundingUp ( prevBound , - delta )
424
389
else none ( )
425
- )
426
- else
427
- //this SSA definition is a phi node.
428
- if def instanceof SsaPhiNode
429
- then
430
- exists ( SsaPhiNode phi |
431
- phi = def and
432
- result = getAnSsaUpperBound ( phi .getAnInput ( ) .getDefinition ( ) )
433
390
)
434
- else none ( )
391
+ else
392
+ //SSA definition coresponding to an `IncDecStmt`
393
+ if explicitDef .getInstruction ( ) instanceof IR:: IncDecInstruction
394
+ then
395
+ exists ( IncDecStmt incOrDec , IR:: IncDecInstruction instr , float exprLB |
396
+ instr = explicitDef .getInstruction ( ) and
397
+ exprLB = getAnUpperBound ( incOrDec .getOperand ( ) ) and
398
+ instr .getRhs ( ) .( IR:: EvalIncDecRhsInstruction ) .getStmt ( ) = incOrDec and
399
+ (
400
+ //IncStmt(x++)
401
+ exists ( IncStmt inc |
402
+ inc = incOrDec and
403
+ result = addRoundingUp ( exprLB , 1 )
404
+ )
405
+ or
406
+ //DecStmt(x--)
407
+ exists ( DecStmt dec |
408
+ dec = incOrDec and
409
+ result = addRoundingUp ( exprLB , - 1 )
410
+ )
411
+ )
412
+ )
413
+ else (
414
+ //SSA definition coreponding to the init of the parameter
415
+ explicitDef .getInstruction ( ) instanceof IR:: InitParameterInstruction and
416
+ exists ( IR:: InitParameterInstruction instr , Parameter p |
417
+ instr = explicitDef .getInstruction ( ) and
418
+ IR:: initParamInstruction ( p ) = instr and
419
+ result = typeMaxValue ( p .getType ( ) )
420
+ )
421
+ )
422
+ )
423
+ or
424
+ //this SSA definition is a phi node.
425
+ def instanceof SsaPhiNode and
426
+ exists ( SsaPhiNode phi |
427
+ phi = def and
428
+ result = getAnSsaUpperBound ( phi .getAnInput ( ) .getDefinition ( ) )
429
+ )
435
430
)
436
431
}
437
432
438
433
/**
439
434
* Gets a possible lower bound of SSA definition `def`.
440
435
*/
441
436
float getAnSsaLowerBound ( SsaDefinition def ) {
442
- if recursiveSelfDef ( def )
443
- then none ( )
444
- else (
445
- if def instanceof SsaExplicitDefinition
446
- then
447
- exists ( SsaExplicitDefinition explicitDef | explicitDef = def |
448
- if explicitDef .getInstruction ( ) instanceof IR:: AssignInstruction
449
- then
450
- //SimpleAssignStmt
451
- exists ( IR:: AssignInstruction assignInstr , SimpleAssignStmt simpleAssign |
452
- assignInstr = explicitDef .getInstruction ( ) and
453
- assignInstr .getRhs ( ) .( IR:: EvalInstruction ) .getExpr ( ) = simpleAssign .getRhs ( ) and
454
- result = getALowerBound ( simpleAssign .getRhs ( ) )
455
- )
456
- or
457
- //ValueSpec
458
- exists ( IR:: AssignInstruction declInstr , ValueSpec vs , int i , Expr init |
459
- declInstr = explicitDef .getInstruction ( ) and
460
- declInstr = IR:: initInstruction ( vs , i ) and
461
- init = vs .getInit ( i ) and
462
- result = getALowerBound ( init )
463
- )
464
- or
465
- //AddAssignStmt(x += y)
466
- exists (
467
- IR:: AssignInstruction assignInstr , SsaExplicitDefinition prevDef ,
468
- CompoundAssignStmt compoundAssign , float prevBound , float delta
469
- |
470
- assignInstr = explicitDef .getInstruction ( ) and
471
- getAUse ( prevDef ) = compoundAssign .getLhs ( ) and
472
- assignInstr = IR:: assignInstruction ( compoundAssign , 0 ) and
473
- prevBound = getAnSsaLowerBound ( prevDef ) and
474
- if compoundAssign instanceof AddAssignStmt
475
- then
476
- delta = getALowerBound ( compoundAssign .getRhs ( ) ) and
477
- result = addRoundingDown ( prevBound , delta )
478
- else
479
- if compoundAssign instanceof SubAssignStmt
480
- then
481
- delta = getAnUpperBound ( compoundAssign .getRhs ( ) ) and
482
- result = addRoundingDown ( prevBound , - delta )
483
- else none ( )
437
+ not recursiveSelfDef ( def ) and
438
+ (
439
+ def instanceof SsaExplicitDefinition and
440
+ exists ( SsaExplicitDefinition explicitDef | explicitDef = def |
441
+ if explicitDef .getInstruction ( ) instanceof IR:: AssignInstruction
442
+ then
443
+ //SimpleAssignStmt
444
+ exists ( IR:: AssignInstruction assignInstr , SimpleAssignStmt simpleAssign |
445
+ assignInstr = explicitDef .getInstruction ( ) and
446
+ assignInstr .getRhs ( ) .( IR:: EvalInstruction ) .getExpr ( ) = simpleAssign .getRhs ( ) and
447
+ result = getALowerBound ( simpleAssign .getRhs ( ) )
448
+ )
449
+ or
450
+ //ValueSpec
451
+ exists ( IR:: AssignInstruction declInstr , ValueSpec vs , int i , Expr init |
452
+ declInstr = explicitDef .getInstruction ( ) and
453
+ declInstr = IR:: initInstruction ( vs , i ) and
454
+ init = vs .getInit ( i ) and
455
+ result = getALowerBound ( init )
456
+ )
457
+ or
458
+ //AddAssignStmt(x += y)
459
+ exists (
460
+ IR:: AssignInstruction assignInstr , SsaExplicitDefinition prevDef ,
461
+ CompoundAssignStmt compoundAssign , float prevBound , float delta
462
+ |
463
+ assignInstr = explicitDef .getInstruction ( ) and
464
+ getAUse ( prevDef ) = compoundAssign .getLhs ( ) and
465
+ assignInstr = IR:: assignInstruction ( compoundAssign , 0 ) and
466
+ prevBound = getAnSsaLowerBound ( prevDef ) and
467
+ (
468
+ compoundAssign instanceof AddAssignStmt and
469
+ delta = getALowerBound ( compoundAssign .getRhs ( ) ) and
470
+ result = addRoundingDown ( prevBound , delta )
471
+ or
472
+ compoundAssign instanceof SubAssignStmt and
473
+ delta = getAnUpperBound ( compoundAssign .getRhs ( ) ) and
474
+ result = addRoundingDown ( prevBound , - delta )
484
475
)
485
- else
486
- //IncDecStmt
487
- if explicitDef .getInstruction ( ) instanceof IR:: IncDecInstruction
488
- then
489
- exists ( IncDecStmt incOrDec , IR:: IncDecInstruction instr , float exprLB |
490
- instr = explicitDef .getInstruction ( ) and
491
- exprLB = getALowerBound ( incOrDec .getOperand ( ) ) and
492
- instr .getRhs ( ) .( IR:: EvalIncDecRhsInstruction ) .getStmt ( ) = incOrDec and
493
- (
494
- //IncStmt(x++)
495
- exists ( IncStmt inc |
496
- inc = incOrDec and
497
- result = addRoundingDown ( exprLB , 1 )
498
- )
499
- or
500
- //DecStmt(x--)
501
- exists ( DecStmt dec |
502
- dec = incOrDec and
503
- result = addRoundingDown ( exprLB , - 1 )
504
- )
476
+ )
477
+ else
478
+ //IncDecStmt
479
+ if explicitDef .getInstruction ( ) instanceof IR:: IncDecInstruction
480
+ then
481
+ exists ( IncDecStmt incOrDec , IR:: IncDecInstruction instr , float exprLB |
482
+ instr = explicitDef .getInstruction ( ) and
483
+ exprLB = getALowerBound ( incOrDec .getOperand ( ) ) and
484
+ instr .getRhs ( ) .( IR:: EvalIncDecRhsInstruction ) .getStmt ( ) = incOrDec and
485
+ (
486
+ //IncStmt(x++)
487
+ exists ( IncStmt inc |
488
+ inc = incOrDec and
489
+ result = addRoundingDown ( exprLB , 1 )
505
490
)
506
- )
507
- else
508
- //init of the function parameter
509
- if explicitDef .getInstruction ( ) instanceof IR:: InitParameterInstruction
510
- then
511
- exists ( IR:: InitParameterInstruction instr , Parameter p |
512
- instr = explicitDef .getInstruction ( ) and
513
- IR:: initParamInstruction ( p ) = instr and
514
- result = typeMinValue ( p .getType ( ) )
491
+ or
492
+ //DecStmt(x--)
493
+ exists ( DecStmt dec |
494
+ dec = incOrDec and
495
+ result = addRoundingDown ( exprLB , - 1 )
515
496
)
516
- else none ( )
517
- )
518
- else
519
- //phi node
520
- if def instanceof SsaPhiNode
521
- then
522
- exists ( SsaPhiNode phi |
523
- phi = def and
524
- result = getAnSsaLowerBound ( phi .getAnInput ( ) .getDefinition ( ) )
497
+ )
498
+ )
499
+ else (
500
+ //init of the function parameter
501
+ explicitDef .getInstruction ( ) instanceof IR:: InitParameterInstruction and
502
+ exists ( IR:: InitParameterInstruction instr , Parameter p |
503
+ instr = explicitDef .getInstruction ( ) and
504
+ IR:: initParamInstruction ( p ) = instr and
505
+ result = typeMinValue ( p .getType ( ) )
506
+ )
525
507
)
526
- else none ( )
508
+ )
509
+ or
510
+ //phi node
511
+ def instanceof SsaPhiNode and
512
+ exists ( SsaPhiNode phi |
513
+ phi = def and
514
+ result = getAnSsaLowerBound ( phi .getAnInput ( ) .getDefinition ( ) )
515
+ )
527
516
)
528
517
}
529
518
0 commit comments