now it works fine with three benchmarks

[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 b18edaf4152f4120b13496f0cd8ea027eba4e300..04aecf9a3ff698faa25a0f6a7f6e8305c9154251 100644 (file)
--- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
+++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
@@ -110,6 +110,8 @@ public class SSJavaAnalysis {
 
   private LinkedList<MethodDescriptor> sortedDescriptors;
 
+  private Map<Location, Set<Descriptor>> mapSharedLocToDescSet;
+
   public SSJavaAnalysis(State state, TypeUtil tu, BuildFlat bf, CallGraph callgraph) {
     this.state = state;
     this.tu = tu;
@@ -129,29 +131,41 @@ public class SSJavaAnalysis {
     this.mapDescriptorToSetDependents = new Hashtable<Descriptor, Set<MethodDescriptor>>();
     this.sortedDescriptors = new LinkedList<MethodDescriptor>();
     this.md2pcLoc = new HashMap<MethodDescriptor, CompositeLocation>();
+    this.mapSharedLocToDescSet = new HashMap<Location, Set<Descriptor>>();
   }
 
   public void doCheck() {
     doMethodAnnotationCheck();
-    computeLinearTypeCheckMethodSet();
-    doLinearTypeCheck();
 
-    init();
+    if (state.SSJAVA && !state.SSJAVAINFER) {
+      init();
+      computeLinearTypeCheckMethodSet();
+      doLinearTypeCheck();
+    }
 
     if (state.SSJAVADEBUG) {
-      debug_printAnnotationRequiredSet();
+      // debug_printAnnotationRequiredSet();
     }
     if (state.SSJAVAINFER) {
       inference();
+      System.exit(0);
     } else {
       parseLocationAnnotation();
       doFlowDownCheck();
       doDefinitelyWrittenCheck();
       doLoopCheck();
     }
+
+    for (Iterator iterator = annotationRequireSet.iterator(); iterator.hasNext();) {
+      MethodDescriptor md = (MethodDescriptor) iterator.next();
+      MethodLattice<String> locOrder = getMethodLattice(md);
+      writeLatticeDotFile(md.getClassDesc(), md, getMethodLattice(md));
+      // System.out.println("~~~\t" + md.getClassDesc() + "_" + md + "\t"
+      // + locOrder.getKeySet().size());
+    }
   }
 
-  private void init() {
+  public void init() {
     // perform topological sort over the set of methods accessed by the main
     // event loop
     Set<MethodDescriptor> methodDescriptorsToAnalyze = new HashSet<MethodDescriptor>();
@@ -163,8 +177,19 @@ public class SSJavaAnalysis {
     return (LinkedList<MethodDescriptor>) sortedDescriptors.clone();
   }
 
+  public void addSharedDesc(Location loc, Descriptor fd) {
+    if (!mapSharedLocToDescSet.containsKey(loc)) {
+      mapSharedLocToDescSet.put(loc, new HashSet<Descriptor>());
+    }
+    mapSharedLocToDescSet.get(loc).add(fd);
+  }
+
+  public Set<Descriptor> getSharedDescSet(Location loc) {
+    return mapSharedLocToDescSet.get(loc);
+  }
+
   private void inference() {
-    LocationInference inferEngine = new LocationInference(this, state);
+    LocationInference inferEngine = new LocationInference(this, state, tu);
     inferEngine.inference();
   }
 
@@ -241,6 +266,8 @@ public class SSJavaAnalysis {
         linearTypeCheckMethodSet.add(md);
       }
     }
+    
+    linearTypeCheckMethodSet.addAll(sortedDescriptors);
 
   }
 
@@ -262,6 +289,10 @@ public class SSJavaAnalysis {
     methodAnnotationChecker = new MethodAnnotationCheck(this, state, tu);
     methodAnnotationChecker.methodAnnoatationCheck();
     methodAnnotationChecker.methodAnnoataionInheritanceCheck();
+    if (state.SSJAVAINFER) {
+      annotationRequireClassSet.add(methodContainingSSJavaLoop.getClassDesc());
+      annotationRequireSet.add(methodContainingSSJavaLoop);
+    }
     state.setAnnotationRequireSet(annotationRequireSet);
   }
 
@@ -293,6 +324,7 @@ public class SSJavaAnalysis {
           if (state.SSJAVADEBUG) {
             // generate lattice dot file
             writeLatticeDotFile(cd, null, locOrder);
+            System.out.println("~~~\t" + cd + "\t" + locOrder.getKeySet().size());
           }
 
         } else if (marker.equals(METHODDEFAULT)) {
@@ -300,6 +332,7 @@ public class SSJavaAnalysis {
               new MethodLattice<String>(SSJavaAnalysis.TOP, SSJavaAnalysis.BOTTOM);
           cd2methodDefault.put(cd, locOrder);
           parseMethodDefaultLatticeDefinition(cd, an.getValue(), locOrder);
+          // writeLatticeDotFile(cd, null, locOrder, "METHOD_DEFAULT");
         }
       }
 
@@ -318,6 +351,7 @@ public class SSJavaAnalysis {
                     new MethodLattice<String>(SSJavaAnalysis.TOP, SSJavaAnalysis.BOTTOM);
                 md2lattice.put(md, locOrder);
                 parseMethodDefaultLatticeDefinition(cd, an.getValue(), locOrder);
+                writeLatticeDotFile(cd, md, locOrder, "");
               } else if (an.getMarker().equals(TERMINATE)) {
                 // developer explicitly wants to skip loop termination analysis
                 String value = an.getValue();
@@ -338,15 +372,23 @@ public class SSJavaAnalysis {
 
   public <T> void writeLatticeDotFile(ClassDescriptor cd, MethodDescriptor md,
       SSJavaLattice<T> locOrder) {
+    writeLatticeDotFile(cd, md, locOrder, "");
+
+  }
+
+  public <T> void writeLatticeDotFile(ClassDescriptor cd, MethodDescriptor md,
+      SSJavaLattice<T> locOrder, String nameSuffix) {
 
     String fileName = "lattice_";
     if (md != null) {
       fileName +=
-          cd.getSymbol().replaceAll("[\\W_]", "") + "_" + md.getSymbol().replaceAll("[\\W_]", "");
+          cd.getSymbol().replaceAll("[\\W_]", "") + "_" + md.toString().replaceAll("[\\W_]", "");
     } else {
       fileName += cd.getSymbol().replaceAll("[\\W_]", "");
     }
 
+    fileName += nameSuffix;
+
     Set<Pair<T, T>> pairSet = locOrder.getOrderingPairSet();
 
     if (pairSet.size() > 0) {
@@ -372,7 +414,7 @@ public class SSJavaAnalysis {
           } else {
             lowLocStr = lowLocId.toString();
           }
-          bw.write(highLocId + " -> " + lowLocId + ";\n");
+          bw.write(highLocStr + " -> " + lowLocStr + ";\n");
         }
         bw.write("}\n");
         bw.close();
@@ -450,7 +492,7 @@ public class SSJavaAnalysis {
         locOrder.put(higherLoc, lowerLoc);
         if (locOrder.isIntroducingCycle(higherLoc)) {
           throw new Error("Error: the order relation " + lowerLoc + " < " + higherLoc
-              + " introduces a cycle.");
+              + " introduces a cycle in the class lattice " + cd);
         }
       } else if (orderElement.contains("*")) {
         // spin loc definition