Robust/src/Analysis/Loops/LoopTerminate.java

   1 package Analysis.Loops;
   2
   3 import java.util.HashMap;
   4 import java.util.HashSet;
   5 import java.util.Iterator;
   6 import java.util.Set;
   7
   8 import Analysis.SSJava.SSJavaAnalysis;
   9 import IR.FieldDescriptor;
  10 import IR.Operation;
  11 import IR.State;
  12 import IR.Flat.FKind;
  13 import IR.Flat.FlatCondBranch;
  14 import IR.Flat.FlatFieldNode;
  15 import IR.Flat.FlatMethod;
  16 import IR.Flat.FlatNode;
  17 import IR.Flat.FlatOpNode;
  18 import IR.Flat.FlatSetFieldNode;
  19 import IR.Flat.TempDescriptor;
  20
  21 public class LoopTerminate {
  22
  23   private FlatMethod fm;
  24   private LoopInvariant loopInv;
  25   private Set<TempDescriptor> inductionSet;
  26   // mapping from Induction Variable TempDescriptor to Flat Node that defines
  27   // it
  28   private HashMap<TempDescriptor, FlatNode> inductionVar2DefNode;
  29
  30   // mapping from Derived Induction Variable TempDescriptor to its root
  31   // induction variable TempDescriptor
  32   private HashMap<TempDescriptor, TempDescriptor> derivedVar2basicInduction;
  33
  34   // maps a loop entrance to the result of termination analysis
  35   private HashMap<FlatNode, Boolean> loopEntranceToTermination;
  36
  37   Set<FlatNode> computed;
  38
  39   State state;
  40   SSJavaAnalysis ssjava;
  41
  42   /**
  43    * Constructor for Loop Termination Analysis
  44    */
  45   public LoopTerminate(SSJavaAnalysis ssjava, State state) {
  46     this.ssjava = ssjava;
  47     this.state = state;
  48     this.inductionSet = new HashSet<TempDescriptor>();
  49     this.inductionVar2DefNode = new HashMap<TempDescriptor, FlatNode>();
  50     this.derivedVar2basicInduction = new HashMap<TempDescriptor, TempDescriptor>();
  51     this.computed = new HashSet<FlatNode>();
  52     this.loopEntranceToTermination = new HashMap<FlatNode, Boolean>();
  53   }
  54
  55   /**
  56    * starts loop termination analysis
  57    *
  58    * @param fm
  59    *          FlatMethod for termination analysis
  60    * @param loopInv
  61    *          LoopInvariants for given method
  62    */
  63   public void terminateAnalysis(FlatMethod fm, LoopInvariant loopInv) {
  64     this.fm = fm;
  65     this.loopInv = loopInv;
  66     Loops loopFinder = loopInv.root;
  67     recurse(fm, loopFinder);
  68   }
  69
  70   /**
  71    *
  72    * spawn analysis for its child and then iterate over the current level of
  73    * loops
  74    *
  75    * @param fm
  76    *          FlatMethod for loop analysis
  77    * @param parent
  78    *          the current level of loop
  79    */
  80   private void recurse(FlatMethod fm, Loops parent) {
  81     for (Iterator lpit = parent.nestedLoops().iterator(); lpit.hasNext();) {
  82       Loops child = (Loops) lpit.next();
  83       recurse(fm, child);
  84       processLoop(fm, child);
  85     }
  86   }
  87
  88   /**
  89    * initialize internal data structure
  90    */
  91   private void init() {
  92     inductionSet.clear();
  93     inductionVar2DefNode.clear();
  94     derivedVar2basicInduction.clear();
  95   }
  96
  97   /**
  98    * analysis loop for termination property
  99    *
 100    * @param fm
 101    *          FlatMethod that contains loop l
 102    * @param l
 103    *          analysis target loop l
 104    */
 105   private void processLoop(FlatMethod fm, Loops l) {
 106
 107     Set loopElements = l.loopIncElements(); // loop body elements
 108     Set loopEntrances = l.loopEntrances(); // loop entrance
 109     assert loopEntrances.size() == 1;
 110     FlatNode loopEntrance = (FlatNode) loopEntrances.iterator().next();
 111
 112     String loopLabel = (String) state.fn2labelMap.get(loopEntrance);
 113
 114     if (loopLabel == null || !loopLabel.startsWith(ssjava.TERMINATE)) {
 115       init();
 116       detectBasicInductionVar(loopElements);
 117       detectDerivedInductionVar(loopElements);
 118
 119       if (!ssjava.getSSJavaLoopEntrance().equals(loopEntrance)) {
 120         checkConditionBranch(loopEntrance, loopElements);
 121       }
 122
 123     }
 124
 125   }
 126
 127   /**
 128    * check if condition branch node satisfies loop condition
 129    *
 130    * @param loopEntrance
 131    *          loop entrance flat node
 132    * @param loopElements
 133    *          elements of current loop and all nested loop
 134    */
 135   private void checkConditionBranch(FlatNode loopEntrance, Set loopElements) {
 136     // In the loop, every guard condition of the loop must be composed by
 137     // induction & invariants
 138     // every guard condition of the if-statement that leads it to the exit must
 139     // be composed by induction&invariants
 140
 141     Set<FlatNode> tovisit = new HashSet<FlatNode>();
 142     Set<FlatNode> visited = new HashSet<FlatNode>();
 143     tovisit.add(loopEntrance);
 144
 145     int numMustTerminateGuardCondtion = 0;
 146     while (!tovisit.isEmpty()) {
 147       FlatNode fnvisit = tovisit.iterator().next();
 148       tovisit.remove(fnvisit);
 149       visited.add(fnvisit);
 150
 151       if (fnvisit.kind() == FKind.FlatCondBranch) {
 152         FlatCondBranch fcb = (FlatCondBranch) fnvisit;
 153
 154         if ((fcb.isLoopBranch() && fcb.getLoopEntrance().equals(loopEntrance))
 155             || hasLoopExitNode(fcb, true, loopEntrance, loopElements)) {
 156           // current FlatCondBranch can introduce loop exits
 157           // in this case, guard condition of it should be composed only by loop
 158           // invariants and induction variables
 159           Set<FlatNode> condSet = getDefinitionInLoop(fnvisit, fcb.getTest(), loopElements);
 160           assert condSet.size() == 1;
 161           FlatNode condFn = condSet.iterator().next();
 162           // assume that guard condition node is always a conditional inequality
 163           if (condFn instanceof FlatOpNode) {
 164             FlatOpNode condOp = (FlatOpNode) condFn;
 165             // check if guard condition is composed only with induction
 166             // variables
 167             if (checkConditionNode(condOp, fcb.isLoopBranch(), loopElements)) {
 168               numMustTerminateGuardCondtion++;
 169             } else {
 170               if (!fcb.isLoopBranch()) {
 171                 // I DON'T THIINK WE NEED TO CARE ABOUT THIS CASE!!!
 172                 // if it is if-condition and it leads us to loop exit,
 173                 // corresponding guard condition should be composed by induction
 174                 // and invariants
 175                 // throw new Error("Loop may never terminate at "
 176                 // + fm.getMethod().getClassDesc().getSourceFileName() + "::"
 177                 // + loopEntrance.numLine);
 178               }
 179             }
 180           }
 181         }
 182       }
 183
 184       for (int i = 0; i < fnvisit.numNext(); i++) {
 185         FlatNode next = fnvisit.getNext(i);
 186         if (loopElements.contains(next) && !visited.contains(next)) {
 187           tovisit.add(next);
 188         }
 189       }
 190
 191     }
 192
 193     // # of must-terminate loop condition must be equal to or larger than # of
 194     // loop
 195     if (numMustTerminateGuardCondtion == 0) {
 196       throw new Error("Loop may never terminate at "
 197           + fm.getMethod().getClassDesc().getSourceFileName() + "::" + loopEntrance.numLine);
 198     }
 199   }
 200
 201   /**
 202    * detect derived induction variable
 203    *
 204    * @param loopElements
 205    *          elements of current loop and all nested loop
 206    */
 207   private void detectDerivedInductionVar(Set loopElements) {
 208     // 2) detect derived induction variables
 209     // variable k is a derived induction variable if
 210     // 1) there is only one definition of k within the loop, of the form k=j*c
 211     // or k=j+d where j is induction variable, c, d are loop-invariant
 212     // 2) and if j is a derived induction variable in the family of i, then:
 213     // (a) the only definition of j that reaches k is the one in the loop
 214     // (b) and there is no definition of i on any path between the definition of
 215     // j and the definition of k
 216
 217     boolean changed = true;
 218     Set<TempDescriptor> basicInductionSet = new HashSet<TempDescriptor>();
 219     basicInductionSet.addAll(inductionSet);
 220
 221     while (changed) {
 222       changed = false;
 223       nextfn: for (Iterator elit = loopElements.iterator(); elit.hasNext();) {
 224         FlatNode fn = (FlatNode) elit.next();
 225         if (!computed.contains(fn)) {
 226           if (fn.kind() == FKind.FlatOpNode) {
 227             FlatOpNode fon = (FlatOpNode) fn;
 228             int op = fon.getOp().getOp();
 229             if (op == Operation.ADD || op == Operation.MULT) {
 230               TempDescriptor tdLeft = fon.getLeft();
 231               TempDescriptor tdRight = fon.getRight();
 232               TempDescriptor tdDest = fon.getDest();
 233
 234               boolean isLeftLoopInvariant = isLoopInvariantVar(fn, tdLeft, loopElements);
 235               boolean isRightLoopInvariant = isLoopInvariantVar(fn, tdRight, loopElements);
 236
 237               if (isLeftLoopInvariant ^ isRightLoopInvariant) {
 238                 TempDescriptor inductionOp;
 239                 if (isLeftLoopInvariant) {
 240                   inductionOp = tdRight;
 241                 } else {
 242                   inductionOp = tdLeft;
 243                 }
 244
 245                 if (inductionSet.contains(inductionOp)) {
 246                   // find new derived one k
 247
 248                   if (!basicInductionSet.contains(inductionOp)) {
 249                     // in this case, induction variable 'j' is derived from
 250                     // basic induction var
 251
 252                     // check if only definition of j that reaches k is the one
 253                     // in the loop
 254
 255                     Set<FlatNode> defSet = getDefinitionInLoop(fn, inductionOp, loopElements);
 256                     if (defSet.size() == 1) {
 257                       // check if there is no def of i on any path bet' def of j
 258                       // and def of k
 259
 260                       TempDescriptor originInduc = derivedVar2basicInduction.get(inductionOp);
 261                       FlatNode defI = inductionVar2DefNode.get(originInduc);
 262                       FlatNode defJ = inductionVar2DefNode.get(inductionOp);
 263                       FlatNode defk = fn;
 264
 265                       if (!checkPath(defI, defJ, defk)) {
 266                         continue nextfn;
 267                       }
 268
 269                     }
 270                   }
 271                   // add new induction var
 272
 273                   // when tdDest has the form of srctmp(tdDest) = inductionOp +
 274                   // loopInvariant
 275                   // want to have the definition of srctmp
 276                   Set<FlatNode> setUseNode = loopInv.usedef.useMap(fn, tdDest);
 277                   assert setUseNode.size() == 1;
 278                   assert setUseNode.iterator().next().writesTemps().length == 1;
 279
 280                   FlatNode srcDefNode = setUseNode.iterator().next();
 281                   if (srcDefNode instanceof FlatOpNode) {
 282                     if (((FlatOpNode) srcDefNode).getOp().getOp() == Operation.ASSIGN) {
 283                       TempDescriptor derivedIndVar = setUseNode.iterator().next().writesTemps()[0];
 284                       FlatNode defNode = setUseNode.iterator().next();
 285
 286                       computed.add(fn);
 287                       computed.add(defNode);
 288                       inductionSet.add(derivedIndVar);
 289                       inductionVar2DefNode.put(derivedIndVar, defNode);
 290                       derivedVar2basicInduction.put(derivedIndVar, inductionOp);
 291                       changed = true;
 292                     }
 293                   }
 294
 295                 }
 296
 297               }
 298
 299             }
 300
 301           }
 302         }
 303
 304       }
 305     }
 306
 307   }
 308
 309   /**
 310    * detect basic induction variable
 311    *
 312    * @param loopElements
 313    *          elements of current loop and all nested loop
 314    */
 315   private void detectBasicInductionVar(Set loopElements) {
 316     // 1) find out basic induction variable
 317     // variable i is a basic induction variable in loop if the only definitions
 318     // of i within L are of the form i=i+c where c is loop invariant
 319
 320     for (Iterator elit = loopElements.iterator(); elit.hasNext();) {
 321       FlatNode fn = (FlatNode) elit.next();
 322       if (fn.kind() == FKind.FlatOpNode) {
 323         FlatOpNode fon = (FlatOpNode) fn;
 324         int op = fon.getOp().getOp();
 325         if (op == Operation.ADD) {
 326           TempDescriptor tdLeft = fon.getLeft();
 327           TempDescriptor tdRight = fon.getRight();
 328
 329           boolean isLeftLoopInvariant = isLoopInvariantVar(fn, tdLeft, loopElements);
 330           boolean isRightLoopInvariant = isLoopInvariantVar(fn, tdRight, loopElements);
 331
 332           if (isLeftLoopInvariant ^ isRightLoopInvariant) {
 333
 334             TempDescriptor candidateTemp;
 335
 336             if (isLeftLoopInvariant) {
 337               candidateTemp = tdRight;
 338             } else {
 339               candidateTemp = tdLeft;
 340             }
 341
 342             Set<FlatNode> defSetOfLoop = getDefinitionInLoop(fn, candidateTemp, loopElements);
 343             // basic induction variable must have only one definition within the
 344             // loop
 345             if (defSetOfLoop.size() == 1) {
 346               // find out definition of induction var, form of Flat
 347               // Assign:inductionVar = candidateTemp
 348               FlatNode indNode = defSetOfLoop.iterator().next();
 349               assert indNode.readsTemps().length == 1;
 350               TempDescriptor readTemp = indNode.readsTemps()[0];
 351               if (readTemp.equals(fon.getDest())) {
 352                 inductionVar2DefNode.put(candidateTemp, defSetOfLoop.iterator().next());
 353                 inductionVar2DefNode.put(readTemp, defSetOfLoop.iterator().next());
 354                 inductionSet.add(fon.getDest());
 355                 inductionSet.add(candidateTemp);
 356                 computed.add(fn);
 357               }
 358
 359             }
 360
 361           }
 362
 363         }
 364       }
 365     }
 366
 367   }
 368
 369   /**
 370    * check whether there is no definition node 'def' on any path between 'start'
 371    * node and 'end' node
 372    *
 373    * @param def
 374    * @param start
 375    * @param end
 376    * @return true if there is no def in-bet start and end
 377    */
 378   private boolean checkPath(FlatNode def, FlatNode start, FlatNode end) {
 379     Set<FlatNode> endSet = new HashSet<FlatNode>();
 380     endSet.add(end);
 381     return !(start.getReachableSet(endSet)).contains(def);
 382   }
 383
 384   /**
 385    * check condition node satisfies termination condition
 386    *
 387    * @param fon
 388    *          condition node FlatOpNode
 389    * @param isLoopCondition
 390    *          true if condition is loop condition
 391    * @param loopElements
 392    *          elements of current loop and all nested loop
 393    * @return true if it satisfies termination condition
 394    */
 395   private boolean checkConditionNode(FlatOpNode fon, boolean isLoopCondition, Set loopElements) {
 396     // check flatOpNode that computes loop guard condition
 397     // currently we assume that induction variable is always getting bigger
 398     // and guard variable is constant
 399     // so need to check (1) one of operand should be induction variable
 400     // (2) another operand should be constant or loop invariant
 401
 402     TempDescriptor induction = null;
 403     TempDescriptor guard = null;
 404
 405     int op = fon.getOp().getOp();
 406     if (op == Operation.LT || op == Operation.LTE) {
 407       if (isLoopCondition) {
 408         // loop condition is inductionVar <= loop invariant
 409         induction = fon.getLeft();
 410         guard = fon.getRight();
 411       } else {
 412         // if-statement condition is loop invariant <= inductionVar since
 413         // inductionVar is getting biggier each iteration
 414         induction = fon.getRight();
 415         guard = fon.getLeft();
 416       }
 417     } else if (op == Operation.GT || op == Operation.GTE) {
 418       if (isLoopCondition) {
 419         // condition is loop invariant >= inductionVar
 420         induction = fon.getRight();
 421         guard = fon.getLeft();
 422       } else {
 423         // if-statement condition is loop inductionVar >= invariant
 424         induction = fon.getLeft();
 425         guard = fon.getRight();
 426       }
 427     } else {
 428       return false;
 429     }
 430
 431     // here, verify that guard operand is an induction variable
 432     if (!hasInductionVar(fon, induction, loopElements, new HashSet<TempDescriptor>())) {
 433       return false;
 434     }
 435
 436     if (guard != null) {
 437       Set guardDefSet = getDefinitionInLoop(fon, guard, loopElements);
 438       for (Iterator iterator = guardDefSet.iterator(); iterator.hasNext();) {
 439         FlatNode guardDef = (FlatNode) iterator.next();
 440         if (guardDef.kind() == FKind.FlatFieldNode) {
 441           FlatFieldNode ffn = (FlatFieldNode) guardDef;
 442           if ((ffn.getField().isStatic() && ffn.getField().isFinal())
 443               || (!hasFieldAccessInLoopElements(ffn, loopElements))) {
 444             // if field is STATIC FINAL field or field is not appeared inside
 445             // the current loop, allow it to be the guard
 446             // condition
 447             return true;
 448           } else {
 449             return false;
 450           }
 451         } else if (!(guardDef.kind() == FKind.FlatLiteralNode)
 452             && !loopInv.hoisted.contains(guardDef)) {
 453           return false;
 454         }
 455       }
 456     }
 457     return true;
 458   }
 459
 460   private boolean hasFieldAccessInLoopElements(FlatFieldNode guardNode, Set loopElements) {
 461     for (Iterator iterator = loopElements.iterator(); iterator.hasNext();) {
 462       FlatNode fn = (FlatNode) iterator.next();
 463       if (fn.kind() == FKind.FlatSetFieldNode) {
 464         FlatSetFieldNode ffn = (FlatSetFieldNode) fn;
 465         if (!ffn.equals(guardNode) && ffn.getField().equals(guardNode.getField())) {
 466           return true;
 467         }
 468       }
 469     }
 470     return false;
 471   }
 472
 473   /**
 474    * check if TempDescriptor td has at least one induction variable and is
 475    * composed only by induction vars +loop invariants
 476    *
 477    * @param fn
 478    *          FlatNode that contains TempDescriptor 'td'
 479    * @param td
 480    *          TempDescriptor representing target variable
 481    * @param loopElements
 482    *          elements of current loop and all nested loop
 483    * @return true if 'td' is induction variable
 484    */
 485   private boolean hasInductionVar(FlatNode fn, TempDescriptor td, Set loopElements,
 486       Set<TempDescriptor> visited) {
 487
 488     visited.add(td);
 489     if (inductionSet.contains(td)) {
 490       return true;
 491     } else {
 492       // check if td is composed by induction variables or loop invariants
 493       Set<FlatNode> defSet = getDefinitionInLoop(fn, td, loopElements);
 494       for (Iterator iterator = defSet.iterator(); iterator.hasNext();) {
 495         FlatNode defNode = (FlatNode) iterator.next();
 496
 497         int inductionVarCount = 0;
 498         TempDescriptor[] readTemps = defNode.readsTemps();
 499         for (int i = 0; i < readTemps.length; i++) {
 500           if (!visited.contains(readTemps[i])) {
 501             if (!hasInductionVar(defNode, readTemps[i], loopElements, visited)) {
 502               if (!isLoopInvariantVar(defNode, readTemps[i], loopElements)) {
 503                 return false;
 504               }
 505             } else {
 506               inductionVarCount++;
 507             }
 508           }
 509         }
 510         // check definition of td has at least one induction var
 511         if (inductionVarCount > 0) {
 512           return true;
 513         }
 514
 515       }
 516
 517       return false;
 518     }
 519
 520   }
 521
 522   /**
 523    * check if TempDescriptor td is loop invariant variable or constant value wrt
 524    * the current loop
 525    *
 526    * @param fn
 527    *          FlatNode that contains TempDescriptor 'td'
 528    * @param td
 529    *          TempDescriptor representing target variable
 530    * @param loopElements
 531    *          elements of current loop and all nested loop
 532    * @return true if 'td' is loop invariant variable
 533    */
 534   private boolean isLoopInvariantVar(FlatNode fn, TempDescriptor td, Set loopElements) {
 535
 536     Set<FlatNode> defset = loopInv.usedef.defMap(fn, td);
 537
 538     Set<FlatNode> defSetOfLoop = new HashSet<FlatNode>();
 539     for (Iterator<FlatNode> defit = defset.iterator(); defit.hasNext();) {
 540       FlatNode def = defit.next();
 541       if (loopElements.contains(def)) {
 542         defSetOfLoop.add(def);
 543       }
 544     }
 545
 546     if (defSetOfLoop.size() == 0) {
 547       // all definition comes from outside the loop
 548       // so it is loop invariant
 549       return true;
 550     } else if (defSetOfLoop.size() == 1) {
 551       // check if def is 1) constant node or 2) loop invariant
 552       FlatNode defFlatNode = defSetOfLoop.iterator().next();
 553       if (defFlatNode.kind() == FKind.FlatLiteralNode || loopInv.hoisted.contains(defFlatNode)) {
 554         return true;
 555       }
 556     }
 557
 558     return false;
 559
 560   }
 561
 562   /**
 563    * compute the set of definitions of variable 'td' inside of the loop
 564    *
 565    * @param fn
 566    *          FlatNode that uses 'td'
 567    * @param td
 568    *          target node that we want to have the set of definitions
 569    * @param loopElements
 570    *          elements of current loop and all nested loop
 571    * @return the set of definition nodes for 'td' in the current loop
 572    */
 573   private Set<FlatNode> getDefinitionInLoop(FlatNode fn, TempDescriptor td, Set loopElements) {
 574
 575     Set<FlatNode> defSetOfLoop = new HashSet<FlatNode>();
 576
 577     Set defSet = loopInv.usedef.defMap(fn, td);
 578     for (Iterator iterator = defSet.iterator(); iterator.hasNext();) {
 579       FlatNode defFlatNode = (FlatNode) iterator.next();
 580       if (loopElements.contains(defFlatNode)) {
 581         defSetOfLoop.add(defFlatNode);
 582       }
 583     }
 584
 585     return defSetOfLoop;
 586
 587   }
 588
 589   /**
 590    * check whether FlatCondBranch introduces loop exit
 591    *
 592    * @param fcb
 593    *          target node
 594    * @param fromTrueBlock
 595    *          specify which block is possible to have loop exit
 596    * @param loopHeader
 597    *          loop header of current loop
 598    * @param loopElements
 599    *          elements of current loop and all nested loop
 600    * @return true if input 'fcb' intrroduces loop exit
 601    */
 602   private boolean hasLoopExitNode(FlatCondBranch fcb, boolean fromTrueBlock, FlatNode loopHeader,
 603       Set loopElements) {
 604     // return true if fcb possibly introduces loop exit
 605
 606     FlatNode next;
 607     if (fromTrueBlock) {
 608       next = fcb.getNext(0);
 609     } else {
 610       next = fcb.getNext(1);
 611     }
 612
 613     return hasLoopExitNode(loopHeader, next, loopElements);
 614
 615   }
 616
 617   /**
 618    * check whether start node reaches loop exit
 619    *
 620    * @param loopHeader
 621    * @param start
 622    * @param loopElements
 623    * @return true if a path exist from start to loop exit
 624    */
 625   private boolean hasLoopExitNode(FlatNode loopHeader, FlatNode start, Set loopElements) {
 626
 627     Set<FlatNode> tovisit = new HashSet<FlatNode>();
 628     Set<FlatNode> visited = new HashSet<FlatNode>();
 629     tovisit.add(start);
 630
 631     while (!tovisit.isEmpty()) {
 632
 633       FlatNode fn = tovisit.iterator().next();
 634       tovisit.remove(fn);
 635       visited.add(fn);
 636
 637       for (int i = 0; i < fn.numNext(); i++) {
 638         FlatNode next = fn.getNext(i);
 639         if (!visited.contains(next)) {
 640           // check that if-body statment introduces loop exit.
 641           if (!loopElements.contains(next)) {
 642             return true;
 643           }
 644
 645           if (loopInv.domtree.idom(next).equals(fn)) {
 646             // add next node only if current node is immediate dominator of the
 647             // next node
 648             tovisit.add(next);
 649           }
 650         }
 651       }
 652
 653     }
 654
 655     return false;
 656
 657   }
 658 }