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 3571704dc817a885e5577f4d8f146de26eea34c2..5b111ca3b7feb46a91012d927be562a0fe31ab51 100644 (file)
--- 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 dc09e23b27cb6694588b9a36161c0999354355aa..3cfbb3d0f1c1c202bb3af75b21aa286c21523526 100644 (file)
--- 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 c017ea4931b6af5012ef29e36dee320f3b1ab712..db16bef941f85e9ca0f32d79638951516fbbff5f 100644 (file)
--- 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 c2a71cba6caa664add9b2c18b25a36e0bc11eb32..ca98c6bed48b363b9451f96800498d8bbb479abe 100644 (file)
--- 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 d800573341ba39c74581c09a405e8cb3010724bb..e8ae399d71ca8d237e10205b0f77d56e34a2b57e 100644 (file)
--- 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) {