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 0c0b477a41988ac22950cff8f8058741d1ae2ce0..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,19 +118,22 @@ public class SSJavaAnalysis {
     // if (state.SSJAVADEBUG) {
     // debugPrint();
     // }
-    parseLocationAnnotation();
-    // inference();
-    doFlowDownCheck();
-    doDefinitelyWrittenCheck();
-    debugDoLoopCheck();
+    if (state.SSJAVAINFER) {
+      inference();
+    } else {
+      parseLocationAnnotation();
+      doFlowDownCheck();
+      doDefinitelyWrittenCheck();
+      doLoopCheck();
+    }
   }
 
   private void inference() {
-    SSJavaInferenceEngine inferEngine = new SSJavaInferenceEngine(this, state);
+    LocationInference inferEngine = new LocationInference(this, state);
     inferEngine.inference();
   }
 
-  private void debugDoLoopCheck() {
+  private void doLoopCheck() {
     GlobalFieldType gft = new GlobalFieldType(callgraph, state, tu.getMain());
     LoopOptimize lo = new LoopOptimize(gft, tu);
 
@@ -549,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);
+  }
+
 }