From: yeom <yeom>
Date: Wed, 22 Jun 2011 00:27:05 +0000 (+0000)
Subject: bug fixes + integrate loop termination analysis into ssjava checking
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=1eb46e8f7edc3dc014777a951b27b71d85d396ba;p=IRC.git

bug fixes + integrate loop termination analysis into ssjava checking
- add an interface to access loop invariant from LoopOptimize
- add "TERMINATE" annotation for method method declaration when developer wants to skip the loop termination analysis for an annotated method. There is no way to have direct annotations on the loop since Java only allows to have annotations on declaration nodes
---

diff --git a/Robust/src/Analysis/Loops/LoopOptimize.java b/Robust/src/Analysis/Loops/LoopOptimize.java
index 3571704d..5b111ca3 100644
--- a/Robust/src/Analysis/Loops/LoopOptimize.java
+++ b/Robust/src/Analysis/Loops/LoopOptimize.java
@@ -1,26 +1,41 @@
 package Analysis.Loops;
 
-import IR.Flat.*;
-import IR.TypeUtil;
-import IR.MethodDescriptor;
-import IR.Operation;
-import java.util.HashSet;
+import java.util.HashMap;
+import java.util.Hashtable;
+import java.util.Iterator;
+import java.util.Map;
 import java.util.Set;
 import java.util.Vector;
-import java.util.Iterator;
-import java.util.Hashtable;
+
+import IR.Operation;
+import IR.TypeUtil;
+import IR.Flat.FlatMethod;
+import IR.Flat.FlatNode;
+import IR.Flat.FlatOpNode;
+import IR.Flat.TempDescriptor;
+import IR.Flat.TempMap;
 
 public class LoopOptimize {
-  LoopInvariant loopinv;
+  private LoopInvariant loopinv;
+  private GlobalFieldType gft;
+  private TypeUtil typeutil;
+  private Map<FlatMethod, LoopInvariant> fm2loopinv;
+  
+  private Hashtable<FlatNode, FlatNode> ntoomap;
+  private Hashtable<FlatNode, FlatNode> clonemap;
+  private Hashtable<FlatNode, FlatNode> map;
+  
   public LoopOptimize(GlobalFieldType gft, TypeUtil typeutil) {
-    loopinv=new LoopInvariant(typeutil,gft);
+    this.gft = gft;
+    this.typeutil = typeutil;
+    fm2loopinv = new HashMap<FlatMethod, LoopInvariant>();
   }
-  Hashtable<FlatNode, FlatNode> ntoomap;
-  Hashtable<FlatNode, FlatNode> clonemap;
-  Hashtable<FlatNode, FlatNode> map;
 
   public void optimize(FlatMethod fm) {
+    loopinv = new LoopInvariant(typeutil, gft);
     loopinv.analyze(fm);
+    fm2loopinv.put(fm, loopinv);
+    
     ntoomap=new Hashtable<FlatNode, FlatNode>();
     map=new Hashtable<FlatNode, FlatNode>();
     clonemap=new Hashtable<FlatNode, FlatNode>();
@@ -240,4 +255,8 @@ public class LoopOptimize {
       }
     }
   }
+  
+  public LoopInvariant getLoopInvariant(FlatMethod fm){
+    return fm2loopinv.get(fm);
+  }
 }
diff --git a/Robust/src/Analysis/Loops/LoopTerminate.java b/Robust/src/Analysis/Loops/LoopTerminate.java
index dc09e23b..3cfbb3d0 100644
--- a/Robust/src/Analysis/Loops/LoopTerminate.java
+++ b/Robust/src/Analysis/Loops/LoopTerminate.java
@@ -30,15 +30,8 @@ public class LoopTerminate {
 
   /**
    * Constructor for Loop Termination Analysis
-   * 
-   * @param fm
-   *          FlatMethod for termination analysis
-   * @param loopInv
-   *          LoopInvariants for given method
    */
-  public LoopTerminate(FlatMethod fm, LoopInvariant loopInv) {
-    this.fm = fm;
-    this.loopInv = loopInv;
+  public LoopTerminate() {
     this.inductionSet = new HashSet<TempDescriptor>();
     this.inductionVar2DefNode = new HashMap<TempDescriptor, FlatNode>();
     this.derivedVar2basicInduction = new HashMap<TempDescriptor, TempDescriptor>();
@@ -47,8 +40,15 @@ public class LoopTerminate {
 
   /**
    * starts loop termination analysis
+   * 
+   * @param fm
+   *          FlatMethod for termination analysis
+   * @param loopInv
+   *          LoopInvariants for given method
    */
-  public void terminateAnalysis() {
+  public void terminateAnalysis(FlatMethod fm, LoopInvariant loopInv) {
+    this.fm = fm;
+    this.loopInv = loopInv;
     Loops loopFinder = loopInv.root;
     recurse(fm, loopFinder);
   }
diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index c017ea49..db16bef9 100644
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -293,6 +293,11 @@ public class FlowDownCheck {
       }
 
     }
+
+    if (lowestLoc == null) {
+      lowestLoc = new CompositeLocation(Location.createBottomLocation(md));
+    }
+
     return lowestLoc;
   }
 
@@ -325,10 +330,10 @@ public class FlowDownCheck {
       compLoc = checkLocationFromSubBlockNode(md, nametable, (SubBlockNode) bsn);
       break;
 
-    // case Kind.ContinueBreakNode:
-    // checkLocationFromContinueBreakNode(md, nametable,(ContinueBreakNode)
-    // bsn);
-    // return null;
+    case Kind.ContinueBreakNode:
+      compLoc = new CompositeLocation();
+      break;
+
     }
     return compLoc;
   }
diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
index c2a71cba..ca98c6be 100644
--- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
+++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
@@ -6,11 +6,14 @@ import java.util.Set;
 import java.util.StringTokenizer;
 import java.util.Vector;
 
+import Analysis.Loops.LoopOptimize;
+import Analysis.Loops.LoopTerminate;
 import IR.AnnotationDescriptor;
 import IR.ClassDescriptor;
 import IR.MethodDescriptor;
 import IR.State;
 import IR.TypeUtil;
+import IR.Flat.FlatMethod;
 
 public class SSJavaAnalysis {
 
@@ -22,6 +25,8 @@ public class SSJavaAnalysis {
   public static final String RETURNLOC = "RETURNLOC";
   public static final String LOC = "LOC";
   public static final String DELTA = "DELTA";
+  public static final String TERMINATE = "TERMINATE";
+
   State state;
   TypeUtil tu;
   FlowDownCheck flowDownChecker;
@@ -39,6 +44,9 @@ public class SSJavaAnalysis {
   // method -> local variable lattice
   Hashtable<MethodDescriptor, MethodLattice<String>> md2lattice;
 
+  // method set that does not have loop termination analysis
+  Hashtable<MethodDescriptor, Integer> skipLoopTerminate;
+
   public SSJavaAnalysis(State state, TypeUtil tu) {
     this.state = state;
     this.tu = tu;
@@ -46,13 +54,14 @@ public class SSJavaAnalysis {
     this.cd2methodDefault = new Hashtable<ClassDescriptor, MethodLattice<String>>();
     this.md2lattice = new Hashtable<MethodDescriptor, MethodLattice<String>>();
     this.md2needAnnotation = new Hashtable<MethodDescriptor, Boolean>();
+    this.skipLoopTerminate = new Hashtable<MethodDescriptor, Integer>();
   }
 
   public void doCheck() {
     doMethodAnnotationCheck();
     parseLocationAnnotation();
     doFlowDownCheck();
-    doLoopCheck();
+    doDefinitelyWrittenCheck();
     doSingleReferenceCheck();
   }
 
@@ -67,7 +76,7 @@ public class SSJavaAnalysis {
     flowDownChecker.flowDownCheck();
   }
 
-  public void doLoopCheck() {
+  public void doDefinitelyWrittenCheck() {
     DefinitelyWrittenCheck checker = new DefinitelyWrittenCheck(state);
     checker.definitelyWrittenCheck();
   }
@@ -114,6 +123,14 @@ public class SSJavaAnalysis {
                     new MethodLattice<String>(SSJavaLattice.TOP, SSJavaLattice.BOTTOM);
                 md2lattice.put(md, locOrder);
                 parseMethodLatticeDefinition(cd, an.getValue(), locOrder);
+              } else if (an.getMarker().equals(TERMINATE)) {
+                // developer explicitly wants to skip loop termination analysis
+                String value = an.getValue();
+                int maxIteration = 0;
+                if (value != null) {
+                  maxIteration = Integer.parseInt(value);
+                }
+                skipLoopTerminate.put(md, new Integer(maxIteration));
               }
             }
           }
@@ -244,4 +261,17 @@ public class SSJavaAnalysis {
     return md2needAnnotation;
   }
 
+  public void doLoopTerminationCheck(LoopOptimize lo) {
+    LoopTerminate lt = new LoopTerminate();
+    Set<MethodDescriptor> mdSet = md2needAnnotation.keySet();
+    for (Iterator iterator = mdSet.iterator(); iterator.hasNext();) {
+      MethodDescriptor md = (MethodDescriptor) iterator.next();
+      if (!skipLoopTerminate.containsKey(md)) {
+        FlatMethod fm = state.getMethodFlat(md);
+        lt.terminateAnalysis(fm, lo.getLoopInvariant(fm));
+      }
+    }
+
+  }
+
 }
diff --git a/Robust/src/Main/Main.java b/Robust/src/Main/Main.java
index d8005733..e8ae399d 100644
--- a/Robust/src/Main/Main.java
+++ b/Robust/src/Main/Main.java
@@ -479,8 +479,8 @@ public class Main {
     CallGraph callgraph=jb!=null?jb:(state.TASK?new BaseCallGraph(state, tu):new JavaCallGraph(state, tu));
 
     // SSJava
+    SSJavaAnalysis ssjava=new SSJavaAnalysis(state,tu);
     if(state.SSJAVA) {
-      SSJavaAnalysis ssjava=new SSJavaAnalysis(state,tu);
       ssjava.doCheck();
       State.logEvent("Done SSJava Checking");
     }
@@ -519,6 +519,10 @@ public class Main {
         }
       }
       State.logEvent("Done Optimizing");
+      
+      if(state.SSJAVA) {
+        ssjava.doLoopTerminationCheck(lo);
+      }
     }
 
     if (state.FLATIRGRAPH) {