@@ -347,183 +347,172 @@ float getALowerBound(Expr expr) {
347347 * Gets a possible upper bound of SSA definition `def`.
348348 */
349349float 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
396381 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 )
415384 else
416- //SSA definition coreponding to the init of the parameter
417- if explicitDef .getInstruction ( ) instanceof IR:: InitParameterInstruction
385+ if compoundAssign instanceof SubAssignStmt
418386 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 )
424389 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 ( ) )
433390 )
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+ )
435430 )
436431}
437432
438433/**
439434 * Gets a possible lower bound of SSA definition `def`.
440435 */
441436float 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 )
484475 )
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 )
505490 )
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 )
515496 )
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+ )
525507 )
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+ )
527516 )
528517}
529518
0 commit comments