changes toward intraprocedural analysis

diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
index 39c5ee268176f9fcf50cf370408716d9338bab2e..7cc86f16fda8875a34d6fe8914889b069babe45f 100644 (file)
--- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
+++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
@@ -63,14 +63,14 @@ public class DefinitelyWrittenCheck {
   // maps a method descriptor to its current summary during the analysis
   // then analysis reaches fixed-point, this mapping will have the final summary
   // for each method descriptor
-  private Hashtable<MethodDescriptor, Hashtable<Location, Vector<Object>>> mapMethodDescriptorToCompleteClearingSummary;
+  private Hashtable<MethodDescriptor, Hashtable<NTuple<Descriptor>, Set<SharedLocState>>> mapMethodDescriptorToCompleteClearingSummary;
 
   // maps a method descriptor to the merged incoming caller's current
   // overwritten status
-  private Hashtable<MethodDescriptor, Hashtable<Location, Vector<Object>>> mapMethodDescriptorToInitialClearingSummary;
+  private Hashtable<MethodDescriptor, Hashtable<NTuple<Descriptor>, Set<SharedLocState>>> mapMethodDescriptorToInitialClearingSummary;
 
   // maps a flat node to current partial results
-  private Hashtable<FlatNode, Hashtable<Location, Vector<Object>>> mapFlatNodeToClearingSummary;
+  private Hashtable<FlatNode, Hashtable<NTuple<Descriptor>, Set<SharedLocState>>> mapFlatNodeToClearingSummary;
 
   private FlatNode ssjavaLoopEntrance;
   private LoopFinder ssjavaLoop;
@@ -79,6 +79,8 @@ public class DefinitelyWrittenCheck {
   private Set<NTuple<Descriptor>> calleeUnionBoundReadSet;
   private Set<NTuple<Descriptor>> calleeIntersectBoundOverWriteSet;
 
+  private TempDescriptor LOCAL;
+
   public DefinitelyWrittenCheck(SSJavaAnalysis ssjava, State state) {
     this.state = state;
     this.ssjava = ssjava;
@@ -92,19 +94,21 @@ public class DefinitelyWrittenCheck {
         new Hashtable<FlatNode, Hashtable<NTuple<Descriptor>, Hashtable<FlatNode, Boolean>>>();
     this.calleeUnionBoundReadSet = new HashSet<NTuple<Descriptor>>();
     this.calleeIntersectBoundOverWriteSet = new HashSet<NTuple<Descriptor>>();
+
     this.mapMethodDescriptorToCompleteClearingSummary =
-        new Hashtable<MethodDescriptor, Hashtable<Location, Vector<Object>>>();
+        new Hashtable<MethodDescriptor, Hashtable<NTuple<Descriptor>, Set<SharedLocState>>>();
     this.mapMethodDescriptorToInitialClearingSummary =
-        new Hashtable<MethodDescriptor, Hashtable<Location, Vector<Object>>>();
+        new Hashtable<MethodDescriptor, Hashtable<NTuple<Descriptor>, Set<SharedLocState>>>();
     this.mapFlatNodeToClearingSummary =
-        new Hashtable<FlatNode, Hashtable<Location, Vector<Object>>>();
+        new Hashtable<FlatNode, Hashtable<NTuple<Descriptor>, Set<SharedLocState>>>();
+    this.LOCAL = new TempDescriptor("LOCAL");
   }
 
   public void definitelyWrittenCheck() {
     if (!ssjava.getAnnotationRequireSet().isEmpty()) {
       methodReadOverWriteAnalysis();
       writtenAnalyis();
-//      sharedLocationAnalysis();
+      sharedLocationAnalysis();
     }
   }
 
@@ -131,7 +135,7 @@ public class DefinitelyWrittenCheck {
       MethodDescriptor md = methodDescriptorsToVisitStack.pop();
       FlatMethod fm = state.getMethodFlat(md);
 
-      sharedLocation_analyzeMethod(fm, (fm.equals(methodContainingSSJavaLoop)));
+      sharedLocation_analyzeMethod(fm, (md.equals(methodContainingSSJavaLoop)));
 
       if (true) {
 
@@ -159,7 +163,8 @@ public class DefinitelyWrittenCheck {
   private void sharedLocation_analyzeMethod(FlatMethod fm, boolean onlyVisitSSJavaLoop) {
 
     if (state.SSJAVADEBUG) {
-      System.out.println("Definitely written for shared locations Analyzing: " + fm);
+      System.out.println("Definitely written for shared locations Analyzing: " + fm + " "
+          + onlyVisitSSJavaLoop);
     }
 
     // intraprocedural analysis
@@ -176,19 +181,22 @@ public class DefinitelyWrittenCheck {
       FlatNode fn = flatNodesToVisit.iterator().next();
       flatNodesToVisit.remove(fn);
 
-      Hashtable<Location, Vector<Object>> curr = new Hashtable<Location, Vector<Object>>();
+      Hashtable<NTuple<Descriptor>, Set<SharedLocState>> curr =
+          new Hashtable<NTuple<Descriptor>, Set<SharedLocState>>();
 
       for (int i = 0; i < fn.numPrev(); i++) {
         FlatNode prevFn = fn.getPrev(i);
-        Hashtable<Location, Vector<Object>> in = mapFlatNodeToClearingSummary.get(prevFn);
+        Hashtable<NTuple<Descriptor>, Set<SharedLocState>> in =
+            mapFlatNodeToClearingSummary.get(prevFn);
         if (in != null) {
           mergeSharedAnaylsis(curr, in);
         }
       }
 
-      sharedLocation_nodeActions(fn, curr);
+      sharedLocation_nodeActions(fn, curr, onlyVisitSSJavaLoop);
 
-      Hashtable<Location, Vector<Object>> clearingPrev = mapFlatNodeToClearingSummary.get(fn);
+      Hashtable<NTuple<Descriptor>, Set<SharedLocState>> clearingPrev =
+          mapFlatNodeToClearingSummary.get(fn);
 
       if (!curr.equals(clearingPrev)) {
         mapFlatNodeToClearingSummary.put(fn, curr);
@@ -207,14 +215,34 @@ public class DefinitelyWrittenCheck {
 
   }
 
-  private void sharedLocation_nodeActions(FlatNode fn, Hashtable<Location, Vector<Object>> curr) {
+  private void sharedLocation_nodeActions(FlatNode fn,
+      Hashtable<NTuple<Descriptor>, Set<SharedLocState>> curr, boolean isSSJavaLoop) {
 
     TempDescriptor lhs;
     TempDescriptor rhs;
     FieldDescriptor fld;
-
-    System.out.println("fn="+fn);
     switch (fn.kind()) {
+
+    case FKind.FlatOpNode: {
+      FlatOpNode fon = (FlatOpNode) fn;
+      lhs = fon.getDest();
+      rhs = fon.getLeft();
+
+      if (fon.getOp().getOp() == Operation.ASSIGN) {
+        if (rhs.getType().isImmutable() && isSSJavaLoop) {
+          // in ssjavaloop, we need to take care about reading local variables!
+          NTuple<Descriptor> rhsHeapPath = new NTuple<Descriptor>();
+          NTuple<Descriptor> lhsHeapPath = new NTuple<Descriptor>();
+          rhsHeapPath.add(LOCAL);
+          lhsHeapPath.add(LOCAL);
+          readLocation(curr, rhsHeapPath, rhs);
+          writeLocation(curr, lhsHeapPath, lhs);
+        }
+      }
+
+    }
+      break;
+
     case FKind.FlatFieldNode:
     case FKind.FlatElementNode: {
 
@@ -229,7 +257,7 @@ public class DefinitelyWrittenCheck {
       fldHeapPath.add(fld);
 
       if (fld.getType().isImmutable()) {
-        readLocation(fn, fldHeapPath, curr);
+        // readLocation(f curr);
       }
 
       // propagate rhs's heap path to the lhs
@@ -248,7 +276,7 @@ public class DefinitelyWrittenCheck {
       // write(field)
       NTuple<Descriptor> lhsHeapPath = computePath(lhs);
       NTuple<Descriptor> fldHeapPath = new NTuple<Descriptor>(lhsHeapPath.getList());
-      writeLocation(curr, fldHeapPath, fld);
+      // writeLocation(curr, fldHeapPath, fld, getLocation(fld));
 
     }
       break;
@@ -261,28 +289,63 @@ public class DefinitelyWrittenCheck {
 
   }
 
-  private void writeLocation(Hashtable<Location, Vector<Object>> curr,
-      NTuple<Descriptor> fldHeapPath, FieldDescriptor fld) {
+  private Location getLocation(Descriptor d) {
+
+    if (d instanceof FieldDescriptor) {
+      return (Location) ((FieldDescriptor) d).getType().getExtension();
+    } else {
+      assert d instanceof TempDescriptor;
+      CompositeLocation comp = (CompositeLocation) ((TempDescriptor) d).getType().getExtension();
+      return comp.get(comp.getSize() - 1);
+    }
+
+  }
+
+  private SharedLocState getSharedLocState(Hashtable<NTuple<Descriptor>, Set<SharedLocState>> curr,
+      NTuple<Descriptor> hp, Location loc) {
 
-    Location fieldLoc = (Location) fld.getType().getExtension();
-    if (ssjava.isSharedLocation(fieldLoc)) {
+    Set<SharedLocState> set = curr.get(hp);
+    if (set == null) {
+      set = new HashSet<SharedLocState>();
+      curr.put(hp, set);
+    }
 
-      Vector<Object> v = curr.get(fieldLoc);
-      if (v == null) {
-        v = new Vector<Object>();
-        curr.put(fieldLoc, v);
-        v.add(0, fldHeapPath);
-        v.add(1, new HashSet());
-        v.add(2, new Boolean(false));
+    SharedLocState state = null;
+    for (Iterator iterator = set.iterator(); iterator.hasNext();) {
+      SharedLocState e = (SharedLocState) iterator.next();
+      if (e.getLoc().equals(loc)) {
+        state = e;
+        break;
       }
-      ((Set) v.get(1)).add(fld);
     }
+
+    if (state == null) {
+      state = new SharedLocState(loc);
+      set.add(state);
+    }
+
+    return state;
   }
 
-  private void readLocation(FlatNode fn, NTuple<Descriptor> fldHeapPath,
-      Hashtable<Location, Vector<Object>> curr) {
-    // TODO Auto-generated method stub
+  private void writeLocation(Hashtable<NTuple<Descriptor>, Set<SharedLocState>> curr,
+      NTuple<Descriptor> hp, Descriptor d) {
 
+    Location loc = getLocation(d);
+    if (ssjava.isSharedLocation(loc)) {
+      SharedLocState state = getSharedLocState(curr, hp, loc);
+      state.addVar(d);
+    }
+  }
+
+  private void readLocation(Hashtable<NTuple<Descriptor>, Set<SharedLocState>> curr,
+      NTuple<Descriptor> hp, Descriptor d) {
+    // remove reading var x from written set
+
+    Location loc = getLocation(d);
+    if (ssjava.isSharedLocation(loc)) {
+      SharedLocState state = getSharedLocState(curr, hp, loc);
+      state.removeVar(d);
+    }
   }
 
   private void writtenAnalyis() {
@@ -890,8 +953,8 @@ public class DefinitelyWrittenCheck {
 
   }
 
-  private void mergeSharedAnaylsis(Hashtable<Location, Vector<Object>> curr,
-      Hashtable<Location, Vector<Object>> in) {
+  private void mergeSharedAnaylsis(Hashtable<NTuple<Descriptor>, Set<SharedLocState>> curr,
+      Hashtable<NTuple<Descriptor>, Set<SharedLocState>> in) {
 
   }
 

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 7978daa1bb84f2c44af12427a94bd7c41a3dec23..108ad0dc8d0c5eda947ad7ec8dc181e1b869e927 100644 (file)
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -405,7 +405,7 @@ public class FlowDownCheck {
 
       Set<CompositeLocation> glbInputSet = new HashSet<CompositeLocation>();
       glbInputSet.add(condLoc);
-//      glbInputSet.add(updateLoc);
+      // glbInputSet.add(updateLoc);
 
       CompositeLocation glbLocOfForLoopCond = CompositeLattice.calculateGLB(glbInputSet);
 
@@ -414,21 +414,21 @@ public class FlowDownCheck {
 
       // compute glb of body including loop body and update statement
       glbInputSet.clear();
-      
+
       if (blockLoc == null) {
         // when there is no statement in the loop body
-        
-        if(updateLoc==null){
+
+        if (updateLoc == null) {
           // also there is no update statement in the loop body
           return glbLocOfForLoopCond;
         }
         glbInputSet.add(updateLoc);
-        
-      }else{
+
+      } else {
         glbInputSet.add(blockLoc);
         glbInputSet.add(updateLoc);
       }
-      
+
       CompositeLocation loopBodyLoc = CompositeLattice.calculateGLB(glbInputSet);
 
       if (!CompositeLattice.isGreaterThan(glbLocOfForLoopCond, loopBodyLoc)) {
@@ -1036,6 +1036,12 @@ public class FlowDownCheck {
           addLocationType(vd.getType(), deltaLoc);
         } else {
           CompositeLocation compLoc = parseLocationDeclaration(md, n, locDec);
+
+          Location lastElement = compLoc.get(compLoc.getSize() - 1);
+          if (ssjava.isSharedLocation(lastElement)) {
+            ssjava.mapSharedLocation2Descriptor(lastElement, vd);
+          }
+
           d2loc.put(vd, compLoc);
           addLocationType(vd.getType(), compLoc);
         }
@@ -1183,6 +1189,11 @@ public class FlowDownCheck {
               + cd.getSourceFileName() + ".");
         }
         Location loc = new Location(cd, locationID);
+
+        if (ssjava.isSharedLocation(loc)) {
+          ssjava.mapSharedLocation2Descriptor(loc, fd);
+        }
+
         addLocationType(fd.getType(), loc);
 
       }

diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
index 80a81e9c3ba1776a67f86ecbdcc56899de0ba19b..1402a41f13e6b45e0c5f37413ade659790d1a482 100644 (file)
--- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
+++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
@@ -16,7 +16,9 @@ import IR.Descriptor;
 import IR.MethodDescriptor;
 import IR.State;
 import IR.TypeUtil;
+import IR.Flat.BuildFlat;
 import IR.Flat.FlatMethod;
+import IR.Flat.TempDescriptor;
 
 public class SSJavaAnalysis {
 
@@ -50,6 +52,9 @@ public class SSJavaAnalysis {
   // method set that does not have loop termination analysis
   Hashtable<MethodDescriptor, Integer> skipLoopTerminate;
 
+  // map shared location to its descriptors
+  Hashtable<Location, Set<Descriptor>> mapSharedLocation2DescriptorSet;
+
   CallGraph callgraph;
 
   public SSJavaAnalysis(State state, TypeUtil tu, CallGraph callgraph) {
@@ -61,6 +66,7 @@ public class SSJavaAnalysis {
     this.md2lattice = new Hashtable<MethodDescriptor, MethodLattice<String>>();
     this.annotationRequireSet = new HashSet<MethodDescriptor>();
     this.skipLoopTerminate = new Hashtable<MethodDescriptor, Integer>();
+    this.mapSharedLocation2DescriptorSet = new Hashtable<Location, Set<Descriptor>>();
   }
 
   public void doCheck() {
@@ -310,9 +316,17 @@ public class SSJavaAnalysis {
   }
 
   public boolean isSharedLocation(Location loc) {
-
     SSJavaLattice<String> lattice = getLattice(loc.getDescriptor());
     return lattice.getSpinLocSet().contains(loc.getLocIdentifier());
+  }
 
+  public void mapSharedLocation2Descriptor(Location loc, Descriptor d) {
+    Set<Descriptor> set = mapSharedLocation2DescriptorSet.get(loc);
+    if (set == null) {
+      set = new HashSet<Descriptor>();
+      mapSharedLocation2DescriptorSet.put(loc, set);
+    }
+    set.add(d);
   }
+
 }

diff --git a/Robust/src/Analysis/SSJava/SharedLocState.java b/Robust/src/Analysis/SSJava/SharedLocState.java
new file mode 100644 (file)
index 0000000..d55bd57
--- /dev/null
+++ b/Robust/src/Analysis/SSJava/SharedLocState.java
@@ -0,0 +1,56 @@
+package Analysis.SSJava;
+
+import java.util.HashSet;
+import java.util.Set;
+
+import IR.Descriptor;
+
+public class SharedLocState {
+
+  Location loc;
+  Set<Descriptor> varSet;
+  boolean flag;
+
+  public SharedLocState(Location loc) {
+    this.loc = loc;
+    this.varSet = new HashSet<Descriptor>();
+    this.flag = false;
+  }
+
+  public void addVar(Descriptor d) {
+    varSet.add(d);
+  }
+
+  public void removeVar(Descriptor d) {
+    varSet.remove(d);
+  }
+
+  public Location getLoc() {
+    return loc;
+  }
+
+  public String toString() {
+    return "<" + loc + "," + varSet + "," + flag + ">";
+  }
+
+  public void setLoc(Location loc) {
+    this.loc = loc;
+  }
+
+  public Set<Descriptor> getVarSet() {
+    return varSet;
+  }
+
+  public void setVarSet(Set<Descriptor> varSet) {
+    this.varSet = varSet;
+  }
+
+  public boolean isFlag() {
+    return flag;
+  }
+
+  public void setFlag(boolean flag) {
+    this.flag = flag;
+  }
+
+}