add new compilation flag -ssjavainfer for the location inference.

[IRC.git] / Robust / src / Analysis / SSJava / SSJavaAnalysis.java

diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
index 67b50e543aaac82b114999f7b360cb75cbc6af46..bf1c6f12df1262f7c36be0b67cd2c4538465881a 100644 (file)
--- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
+++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
@@ -28,6 +28,7 @@ import IR.SymbolTable;
 import IR.TypeUtil;
 import IR.Flat.BuildFlat;
 import IR.Flat.FlatMethod;
+import IR.Flat.FlatNode;
 import Util.Pair;
 
 public class SSJavaAnalysis {
@@ -81,9 +82,13 @@ public class SSJavaAnalysis {
   // points to method containing SSJAVA Loop
   private MethodDescriptor methodContainingSSJavaLoop;
 
+  private FlatNode ssjavaLoopEntrance;
+
   // keep the field ownership from the linear type checking
   Hashtable<MethodDescriptor, Set<FieldDescriptor>> mapMethodToOwnedFieldSet;
 
+  Set<FlatNode> sameHeightWriteFlatNodeSet;
+
   CallGraph callgraph;
 
   LinearTypeCheck checker;
@@ -103,6 +108,7 @@ public class SSJavaAnalysis {
     this.bf = bf;
     this.trustWorthyMDSet = new HashSet<MethodDescriptor>();
     this.mapMethodToOwnedFieldSet = new Hashtable<MethodDescriptor, Set<FieldDescriptor>>();
+    this.sameHeightWriteFlatNodeSet = new HashSet<FlatNode>();
   }
 
   public void doCheck() {
@@ -112,13 +118,22 @@ public class SSJavaAnalysis {
     // if (state.SSJAVADEBUG) {
     // debugPrint();
     // }
-    parseLocationAnnotation();
-    doFlowDownCheck();
-    doDefinitelyWrittenCheck();
-    debugDoLoopCheck();
+    if (state.SSJAVAINFER) {
+      inference();
+    } else {
+      parseLocationAnnotation();
+      doFlowDownCheck();
+      doDefinitelyWrittenCheck();
+      doLoopCheck();
+    }
   }
 
-  private void debugDoLoopCheck() {
+  private void inference() {
+    LocationInference inferEngine = new LocationInference(this, state);
+    inferEngine.inference();
+  }
+
+  private void doLoopCheck() {
     GlobalFieldType gft = new GlobalFieldType(callgraph, state, tu.getMain());
     LoopOptimize lo = new LoopOptimize(gft, tu);
 
@@ -358,12 +373,12 @@ public class SSJavaAnalysis {
     // sanity checks
     if (locOrder.getThisLoc() != null && !locOrder.containsKey(locOrder.getThisLoc())) {
       throw new Error("Variable 'this' location '" + locOrder.getThisLoc()
-          + "' is not defined in the default local variable lattice at " + cd.getSourceFileName());
+          + "' is not defined in the local variable lattice at " + cd.getSourceFileName());
     }
 
     if (locOrder.getGlobalLoc() != null && !locOrder.containsKey(locOrder.getGlobalLoc())) {
       throw new Error("Variable global location '" + locOrder.getGlobalLoc()
-          + "' is not defined in the default local variable lattice at " + cd.getSourceFileName());
+          + "' is not defined in the local variable lattice at " + cd.getSourceFileName());
     }
   }
 
@@ -430,7 +445,13 @@ public class SSJavaAnalysis {
     if (md2lattice.containsKey(md)) {
       return md2lattice.get(md);
     } else {
-      return cd2methodDefault.get(md.getClassDesc());
+
+      if (cd2methodDefault.containsKey(md.getClassDesc())) {
+        return cd2methodDefault.get(md.getClassDesc());
+      } else {
+        throw new Error("Method Lattice of " + md + " is not defined.");
+      }
+
     }
   }
 
@@ -537,4 +558,20 @@ public class SSJavaAnalysis {
     return false;
   }
 
+  public FlatNode getSSJavaLoopEntrance() {
+    return ssjavaLoopEntrance;
+  }
+
+  public void setSSJavaLoopEntrance(FlatNode ssjavaLoopEntrance) {
+    this.ssjavaLoopEntrance = ssjavaLoopEntrance;
+  }
+
+  public void addSameHeightWriteFlatNode(FlatNode fn) {
+    this.sameHeightWriteFlatNodeSet.add(fn);
+  }
+
+  public boolean isSameHeightWrite(FlatNode fn) {
+    return this.sameHeightWriteFlatNodeSet.contains(fn);
+  }
+
 }