1 package Analysis.Loops;
3 import java.util.HashMap;
4 import java.util.HashSet;
5 import java.util.Iterator;
8 import Analysis.SSJava.SSJavaAnalysis;
12 import IR.Flat.FlatCondBranch;
13 import IR.Flat.FlatMethod;
14 import IR.Flat.FlatNode;
15 import IR.Flat.FlatOpNode;
16 import IR.Flat.TempDescriptor;
18 public class LoopTerminate {
20 private FlatMethod fm;
21 private LoopInvariant loopInv;
22 private Set<TempDescriptor> inductionSet;
23 // mapping from Induction Variable TempDescriptor to Flat Node that defines
25 private HashMap<TempDescriptor, FlatNode> inductionVar2DefNode;
27 // mapping from Derived Induction Variable TempDescriptor to its root
28 // induction variable TempDescriptor
29 private HashMap<TempDescriptor, TempDescriptor> derivedVar2basicInduction;
31 Set<FlatNode> computed;
34 SSJavaAnalysis ssjava;
37 * Constructor for Loop Termination Analysis
39 public LoopTerminate(SSJavaAnalysis ssjava, State state) {
42 this.inductionSet = new HashSet<TempDescriptor>();
43 this.inductionVar2DefNode = new HashMap<TempDescriptor, FlatNode>();
44 this.derivedVar2basicInduction = new HashMap<TempDescriptor, TempDescriptor>();
45 this.computed = new HashSet<FlatNode>();
49 * starts loop termination analysis
52 * FlatMethod for termination analysis
54 * LoopInvariants for given method
56 public void terminateAnalysis(FlatMethod fm, LoopInvariant loopInv) {
58 this.loopInv = loopInv;
59 Loops loopFinder = loopInv.root;
60 recurse(fm, loopFinder);
64 * iterate over the current level of loops and spawn analysis for its child
67 * FlatMethod for loop analysis
69 * the current level of loop
71 private void recurse(FlatMethod fm, Loops parent) {
72 for (Iterator lpit = parent.nestedLoops().iterator(); lpit.hasNext();) {
73 Loops child = (Loops) lpit.next();
74 processLoop(fm, child);
80 * initialize internal data structure
84 inductionVar2DefNode.clear();
85 derivedVar2basicInduction.clear();
89 * analysis loop for termination property
92 * FlatMethod that contains loop l
94 * analysis target loop l
96 private void processLoop(FlatMethod fm, Loops l) {
98 Set loopElements = l.loopIncElements(); // loop body elements
99 Set loopEntrances = l.loopEntrances(); // loop entrance
100 assert loopEntrances.size() == 1;
101 FlatNode loopEntrance = (FlatNode) loopEntrances.iterator().next();
103 String loopLabel = (String) state.fn2labelMap.get(loopEntrance);
105 if (loopLabel == null || !loopLabel.startsWith(ssjava.TERMINATE)) {
107 detectBasicInductionVar(loopElements);
108 detectDerivedInductionVar(loopElements);
109 checkConditionBranch(loopEntrance, loopElements);
115 * check if condition branch node satisfies loop condition
117 * @param loopEntrance
118 * loop entrance flat node
119 * @param loopElements
120 * elements of current loop and all nested loop
122 private void checkConditionBranch(FlatNode loopEntrance, Set loopElements) {
123 // In the loop, every guard condition of the loop must be composed by
124 // induction & invariants
125 // every guard condition of the if-statement that leads it to the exit must
126 // be composed by induction&invariants
128 Set<FlatNode> tovisit = new HashSet<FlatNode>();
129 Set<FlatNode> visited = new HashSet<FlatNode>();
130 tovisit.add(loopEntrance);
132 int numMustTerminateGuardCondtion = 0;
134 while (!tovisit.isEmpty()) {
135 FlatNode fnvisit = tovisit.iterator().next();
136 tovisit.remove(fnvisit);
137 visited.add(fnvisit);
139 if (fnvisit.kind() == FKind.FlatCondBranch) {
140 FlatCondBranch fcb = (FlatCondBranch) fnvisit;
142 if (fcb.isLoopBranch()) {
146 if (fcb.isLoopBranch() || hasLoopExitNode(fcb, true, loopEntrance, loopElements)) {
147 // current FlatCondBranch can introduce loop exits
148 // in this case, guard condition of it should be composed only by loop
149 // invariants and induction variables
150 Set<FlatNode> condSet = getDefinitionInLoop(fnvisit, fcb.getTest(), loopElements);
151 assert condSet.size() == 1;
152 FlatNode condFn = condSet.iterator().next();
153 // assume that guard condition node is always a conditional inequality
154 if (condFn instanceof FlatOpNode) {
155 FlatOpNode condOp = (FlatOpNode) condFn;
156 // check if guard condition is composed only with induction
158 if (checkConditionNode(condOp, fcb.isLoopBranch(), loopElements)) {
159 numMustTerminateGuardCondtion++;
161 if (!fcb.isLoopBranch()) {
162 // if it is if-condition and it leads us to loop exit,
163 // corresponding guard condition should be composed by induction
165 throw new Error("Loop may never terminate at "
166 + fm.getMethod().getClassDesc().getSourceFileName() + "::"
167 + loopEntrance.numLine);
174 for (int i = 0; i < fnvisit.numNext(); i++) {
175 FlatNode next = fnvisit.getNext(i);
176 if (loopElements.contains(next) && !visited.contains(next)) {
183 // # of must-terminate loop condition must be equal to or larger than # of
185 if (numMustTerminateGuardCondtion < numLoop) {
186 throw new Error("Loop may never terminate at "
187 + fm.getMethod().getClassDesc().getSourceFileName() + "::" + loopEntrance.numLine);
193 * detect derived induction variable
195 * @param loopElements
196 * elements of current loop and all nested loop
198 private void detectDerivedInductionVar(Set loopElements) {
199 // 2) detect derived induction variables
200 // variable k is a derived induction variable if
201 // 1) there is only one definition of k within the loop, of the form k=j*c
202 // or k=j+d where j is induction variable, c, d are loop-invariant
203 // 2) and if j is a derived induction variable in the family of i, then:
204 // (a) the only definition of j that reaches k is the one in the loop
205 // (b) and there is no definition of i on any path between the definition of
206 // j and the definition of k
208 boolean changed = true;
209 Set<TempDescriptor> basicInductionSet = new HashSet<TempDescriptor>();
210 basicInductionSet.addAll(inductionSet);
214 nextfn: for (Iterator elit = loopElements.iterator(); elit.hasNext();) {
215 FlatNode fn = (FlatNode) elit.next();
216 if (!computed.contains(fn)) {
217 if (fn.kind() == FKind.FlatOpNode) {
218 FlatOpNode fon = (FlatOpNode) fn;
219 int op = fon.getOp().getOp();
220 if (op == Operation.ADD || op == Operation.MULT) {
221 TempDescriptor tdLeft = fon.getLeft();
222 TempDescriptor tdRight = fon.getRight();
223 TempDescriptor tdDest = fon.getDest();
225 boolean isLeftLoopInvariant = isLoopInvariantVar(fn, tdLeft, loopElements);
226 boolean isRightLoopInvariant = isLoopInvariantVar(fn, tdRight, loopElements);
228 if (isLeftLoopInvariant ^ isRightLoopInvariant) {
229 TempDescriptor inductionOp;
230 if (isLeftLoopInvariant) {
231 inductionOp = tdRight;
233 inductionOp = tdLeft;
236 if (inductionSet.contains(inductionOp)) {
237 // find new derived one k
239 if (!basicInductionSet.contains(inductionOp)) {
240 // in this case, induction variable 'j' is derived from
241 // basic induction var
243 // check if only definition of j that reaches k is the one
246 Set<FlatNode> defSet = getDefinitionInLoop(fn, inductionOp, loopElements);
247 if (defSet.size() == 1) {
248 // check if there is no def of i on any path bet' def of j
251 TempDescriptor originInduc = derivedVar2basicInduction.get(inductionOp);
252 FlatNode defI = inductionVar2DefNode.get(originInduc);
253 FlatNode defJ = inductionVar2DefNode.get(inductionOp);
256 if (!checkPath(defI, defJ, defk)) {
262 // add new induction var
264 // when tdDest has the form of srctmp(tdDest) = inductionOp +
266 // want to have the definition of srctmp
267 Set<FlatNode> setUseNode = loopInv.usedef.useMap(fn, tdDest);
268 assert setUseNode.size() == 1;
269 assert setUseNode.iterator().next().writesTemps().length == 1;
271 FlatNode srcDefNode = setUseNode.iterator().next();
272 if (srcDefNode instanceof FlatOpNode) {
273 if (((FlatOpNode) srcDefNode).getOp().getOp() == Operation.ASSIGN) {
274 TempDescriptor derivedIndVar = setUseNode.iterator().next().writesTemps()[0];
275 FlatNode defNode = setUseNode.iterator().next();
278 computed.add(defNode);
279 inductionSet.add(derivedIndVar);
280 inductionVar2DefNode.put(derivedIndVar, defNode);
281 derivedVar2basicInduction.put(derivedIndVar, inductionOp);
301 * detect basic induction variable
303 * @param loopElements
304 * elements of current loop and all nested loop
306 private void detectBasicInductionVar(Set loopElements) {
307 // 1) find out basic induction variable
308 // variable i is a basic induction variable in loop if the only definitions
309 // of i within L are of the form i=i+c where c is loop invariant
310 for (Iterator elit = loopElements.iterator(); elit.hasNext();) {
311 FlatNode fn = (FlatNode) elit.next();
312 if (fn.kind() == FKind.FlatOpNode) {
313 FlatOpNode fon = (FlatOpNode) fn;
314 int op = fon.getOp().getOp();
315 if (op == Operation.ADD) {
316 TempDescriptor tdLeft = fon.getLeft();
317 TempDescriptor tdRight = fon.getRight();
319 boolean isLeftLoopInvariant = isLoopInvariantVar(fn, tdLeft, loopElements);
320 boolean isRightLoopInvariant = isLoopInvariantVar(fn, tdRight, loopElements);
322 if (isLeftLoopInvariant ^ isRightLoopInvariant) {
324 TempDescriptor candidateTemp;
326 if (isLeftLoopInvariant) {
327 candidateTemp = tdRight;
329 candidateTemp = tdLeft;
332 Set<FlatNode> defSetOfLoop = getDefinitionInLoop(fn, candidateTemp, loopElements);
333 // basic induction variable must have only one definition within the
335 if (defSetOfLoop.size() == 1) {
336 // find out definition of induction var, form of Flat
337 // Assign:inductionVar = candidateTemp
338 FlatNode indNode = defSetOfLoop.iterator().next();
339 assert indNode.readsTemps().length == 1;
340 TempDescriptor readTemp = indNode.readsTemps()[0];
341 if (readTemp.equals(fon.getDest())) {
342 inductionVar2DefNode.put(candidateTemp, defSetOfLoop.iterator().next());
343 inductionVar2DefNode.put(readTemp, defSetOfLoop.iterator().next());
344 inductionSet.add(fon.getDest());
345 inductionSet.add(candidateTemp);
360 * check whether there is no definition node 'def' on any path between 'start'
361 * node and 'end' node
366 * @return true if there is no def in-bet start and end
368 private boolean checkPath(FlatNode def, FlatNode start, FlatNode end) {
369 Set<FlatNode> endSet = new HashSet<FlatNode>();
371 return !(start.getReachableSet(endSet)).contains(def);
375 * check condition node satisfies termination condition
378 * condition node FlatOpNode
379 * @param isLoopCondition
380 * true if condition is loop condition
381 * @param loopElements
382 * elements of current loop and all nested loop
383 * @return true if it satisfies termination condition
385 private boolean checkConditionNode(FlatOpNode fon, boolean isLoopCondition, Set loopElements) {
386 // check flatOpNode that computes loop guard condition
387 // currently we assume that induction variable is always getting bigger
388 // and guard variable is constant
389 // so need to check (1) one of operand should be induction variable
390 // (2) another operand should be constant or loop invariant
392 TempDescriptor induction = null;
393 TempDescriptor guard = null;
395 int op = fon.getOp().getOp();
396 if (op == Operation.LT || op == Operation.LTE) {
397 if (isLoopCondition) {
398 // loop condition is inductionVar <= loop invariant
399 induction = fon.getLeft();
400 guard = fon.getRight();
402 // if-statement condition is loop invariant <= inductionVar since
403 // inductionVar is getting biggier each iteration
404 induction = fon.getRight();
405 guard = fon.getLeft();
407 } else if (op == Operation.GT || op == Operation.GTE) {
408 if (isLoopCondition) {
409 // condition is loop invariant >= inductionVar
410 induction = fon.getRight();
411 guard = fon.getLeft();
413 // if-statement condition is loop inductionVar >= invariant
414 induction = fon.getLeft();
415 guard = fon.getRight();
421 // here, verify that guard operand is an induction variable
422 if (!hasInductionVar(fon, induction, loopElements)) {
427 Set guardDefSet = getDefinitionInLoop(fon, guard, loopElements);
428 for (Iterator iterator = guardDefSet.iterator(); iterator.hasNext();) {
429 FlatNode guardDef = (FlatNode) iterator.next();
430 if (!(guardDef.kind() == FKind.FlatLiteralNode) && !loopInv.hoisted.contains(guardDef)) {
440 * check if TempDescriptor td has at least one induction variable and is
441 * composed only by induction vars +loop invariants
444 * FlatNode that contains TempDescriptor 'td'
446 * TempDescriptor representing target variable
447 * @param loopElements
448 * elements of current loop and all nested loop
449 * @return true if 'td' is induction variable
451 private boolean hasInductionVar(FlatNode fn, TempDescriptor td, Set loopElements) {
453 if (inductionSet.contains(td)) {
456 // check if td is composed by induction variables or loop invariants
457 Set<FlatNode> defSet = getDefinitionInLoop(fn, td, loopElements);
458 for (Iterator iterator = defSet.iterator(); iterator.hasNext();) {
459 FlatNode defNode = (FlatNode) iterator.next();
461 int inductionVarCount = 0;
462 TempDescriptor[] readTemps = defNode.readsTemps();
463 for (int i = 0; i < readTemps.length; i++) {
464 if (!hasInductionVar(defNode, readTemps[i], loopElements)) {
465 if (!isLoopInvariantVar(defNode, readTemps[i], loopElements)) {
473 // check definition of td has at least one induction var
474 if (inductionVarCount > 0) {
486 * check if TempDescriptor td is loop invariant variable or constant value wrt
490 * FlatNode that contains TempDescriptor 'td'
492 * TempDescriptor representing target variable
493 * @param loopElements
494 * elements of current loop and all nested loop
495 * @return true if 'td' is loop invariant variable
497 private boolean isLoopInvariantVar(FlatNode fn, TempDescriptor td, Set loopElements) {
499 Set<FlatNode> defset = loopInv.usedef.defMap(fn, td);
501 Set<FlatNode> defSetOfLoop = new HashSet<FlatNode>();
502 for (Iterator<FlatNode> defit = defset.iterator(); defit.hasNext();) {
503 FlatNode def = defit.next();
504 if (loopElements.contains(def)) {
505 defSetOfLoop.add(def);
509 if (defSetOfLoop.size() == 0) {
510 // all definition comes from outside the loop
511 // so it is loop invariant
513 } else if (defSetOfLoop.size() == 1) {
514 // check if def is 1) constant node or 2) loop invariant
515 FlatNode defFlatNode = defSetOfLoop.iterator().next();
516 if (defFlatNode.kind() == FKind.FlatLiteralNode || loopInv.hoisted.contains(defFlatNode)) {
526 * compute the set of definitions of variable 'td' inside of the loop
529 * FlatNode that uses 'td'
531 * target node that we want to have the set of definitions
532 * @param loopElements
533 * elements of current loop and all nested loop
534 * @return the set of definition nodes for 'td' in the current loop
536 private Set<FlatNode> getDefinitionInLoop(FlatNode fn, TempDescriptor td, Set loopElements) {
538 Set<FlatNode> defSetOfLoop = new HashSet<FlatNode>();
540 Set defSet = loopInv.usedef.defMap(fn, td);
541 for (Iterator iterator = defSet.iterator(); iterator.hasNext();) {
542 FlatNode defFlatNode = (FlatNode) iterator.next();
543 if (loopElements.contains(defFlatNode)) {
544 defSetOfLoop.add(defFlatNode);
553 * check whether FlatCondBranch introduces loop exit
557 * @param fromTrueBlock
558 * specify which block is possible to have loop exit
560 * loop header of current loop
561 * @param loopElements
562 * elements of current loop and all nested loop
563 * @return true if input 'fcb' intrroduces loop exit
565 private boolean hasLoopExitNode(FlatCondBranch fcb, boolean fromTrueBlock, FlatNode loopHeader,
567 // return true if fcb possibly introduces loop exit
571 next = fcb.getNext(0);
573 next = fcb.getNext(1);
576 return hasLoopExitNode(loopHeader, next, loopElements);
581 * check whether start node reaches loop exit
585 * @param loopElements
586 * @return true if a path exist from start to loop exit
588 private boolean hasLoopExitNode(FlatNode loopHeader, FlatNode start, Set loopElements) {
590 Set<FlatNode> tovisit = new HashSet<FlatNode>();
591 Set<FlatNode> visited = new HashSet<FlatNode>();
594 while (!tovisit.isEmpty()) {
596 FlatNode fn = tovisit.iterator().next();
600 for (int i = 0; i < fn.numNext(); i++) {
601 FlatNode next = fn.getNext(i);
602 if (!visited.contains(next)) {
603 // check that if-body statment introduces loop exit.
604 if (!loopElements.contains(next)) {
608 if (loopInv.domtree.idom(next).equals(fn)) {
609 // add next node only if current node is immediate dominator of the