From: yeom <yeom>
Date: Thu, 30 Jun 2011 00:51:12 +0000 (+0000)
Subject: start to revise definitely written analysis implementation
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=8776b8acbdf09ed6e57244670c13afed5c64f93d;p=IRC.git

start to revise definitely written analysis implementation
---

diff --git a/Robust/src/Analysis/SSJava/CompositeLocation.java b/Robust/src/Analysis/SSJava/CompositeLocation.java
index 7baf552d..23982187 100644
--- a/Robust/src/Analysis/SSJava/CompositeLocation.java
+++ b/Robust/src/Analysis/SSJava/CompositeLocation.java
@@ -12,7 +12,7 @@ public class CompositeLocation implements TypeExtension {
 
   public CompositeLocation(Location loc) {
     locTuple = new NTuple<Location>();
-    locTuple.addElement(loc);
+    locTuple.add(loc);
   }
 
   public NTuple<Location> getTuple() {
@@ -24,7 +24,7 @@ public class CompositeLocation implements TypeExtension {
   }
 
   public void addLocation(Location loc) {
-    locTuple.addElement(loc);
+    locTuple.add(loc);
   }
 
   public Location get(int idx) {
diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
index 480957ad..5487b4b6 100644
--- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
+++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
@@ -3,18 +3,15 @@ package Analysis.SSJava;
 import java.util.HashSet;
 import java.util.Hashtable;
 import java.util.Iterator;
+import java.util.LinkedList;
 import java.util.Set;
 
-import Analysis.Loops.LoopFinder;
-import Analysis.Loops.Loops;
-import IR.ClassDescriptor;
+import Analysis.CallGraph.CallGraph;
 import IR.Descriptor;
 import IR.FieldDescriptor;
 import IR.MethodDescriptor;
 import IR.Operation;
 import IR.State;
-import IR.SymbolTable;
-import IR.VarDescriptor;
 import IR.Flat.FKind;
 import IR.Flat.FlatFieldNode;
 import IR.Flat.FlatLiteralNode;
@@ -26,196 +23,300 @@ import IR.Flat.TempDescriptor;
 
 public class DefinitelyWrittenCheck {
 
-  static State state;
-  HashSet toanalyze;
+  SSJavaAnalysis ssjava;
+  State state;
+  CallGraph callGraph;
+
+  // maps a descriptor to its known dependents: namely
+  // methods or tasks that call the descriptor's method
+  // AND are part of this analysis (reachable from main)
+  private Hashtable<Descriptor, Set<MethodDescriptor>> mapDescriptorToSetDependents;
+
+  // maps a flat node to its WrittenSet: this keeps all heap path overwritten
+  // previously.
+  private Hashtable<FlatNode, Set<NTuple<Descriptor>>> mapFlatNodeToWrittenSet;
+
+  // maps a temp descriptor to its heap path
+  // each temp descriptor has a unique heap path since we do not allow any
+  // alias.
+  private Hashtable<Descriptor, NTuple<Descriptor>> mapHeapPath;
+
+  // maps a flat method to the READ that is the set of heap path that is
+  // expected to be written before method invocation
+  private Hashtable<FlatMethod, Set<NTuple<Descriptor>>> mapFlatMethodToRead;
+
+  // maps a flat method to the OVERWRITE that is the set of heap path that is
+  // overwritten on every possible path during method invocation
+  private Hashtable<FlatMethod, Set<NTuple<Descriptor>>> mapFlatMethodToOverWrite;
 
   private Hashtable<FlatNode, Hashtable<Descriptor, Hashtable<FlatNode, Boolean>>> definitelyWrittenResults;
 
-  public DefinitelyWrittenCheck(State state) {
+  public DefinitelyWrittenCheck(SSJavaAnalysis ssjava, State state) {
     this.state = state;
-    this.toanalyze = new HashSet();
-    this.definitelyWrittenResults =
-      new Hashtable<FlatNode, Hashtable<Descriptor, Hashtable<FlatNode, Boolean>>>();
+    this.ssjava = ssjava;
+    this.callGraph = ssjava.getCallGraph();
+    this.mapFlatNodeToWrittenSet = new Hashtable<FlatNode, Set<NTuple<Descriptor>>>();
+    this.mapDescriptorToSetDependents = new Hashtable<Descriptor, Set<MethodDescriptor>>();
+    this.mapHeapPath = new Hashtable<Descriptor, NTuple<Descriptor>>();
+    this.mapFlatMethodToRead = new Hashtable<FlatMethod, Set<NTuple<Descriptor>>>();
+    this.mapFlatMethodToOverWrite = new Hashtable<FlatMethod, Set<NTuple<Descriptor>>>();
   }
 
   public void definitelyWrittenCheck() {
 
-    SymbolTable classtable = state.getClassSymbolTable();
-    toanalyze.addAll(classtable.getValueSet());
-    toanalyze.addAll(state.getTaskSymbolTable().getValueSet());
-    while (!toanalyze.isEmpty()) {
-      Object obj = toanalyze.iterator().next();
-      ClassDescriptor cd = (ClassDescriptor) obj;
-      toanalyze.remove(cd);
-
-//      if (cd.isClassLibrary()) {
-      // doesn't care about class libraries now
-//        continue;
-//      }
-      for (Iterator method_it = cd.getMethods(); method_it.hasNext(); ) {
-        MethodDescriptor md = (MethodDescriptor) method_it.next();
-        FlatMethod fm = state.getMethodFlat(md);
-        if (fm != null) {
-
-        }
+    analyzeMethods();
+  }
 
-      }
-    }
+  private void analyzeMethods() {
+    // perform method READ/OVERWRITE analysis
 
+    Set<MethodDescriptor> methodDescriptorsToAnalyze = new HashSet<MethodDescriptor>();
+    methodDescriptorsToAnalyze.addAll(ssjava.getAnnotationRequireSet());
 
+    LinkedList<MethodDescriptor> sortedDescriptors = topologicalSort(methodDescriptorsToAnalyze);
 
-    /*
-       // creating map
-       SymbolTable classtable = state.getClassSymbolTable();
-       toanalyze.addAll(classtable.getValueSet());
-       toanalyze.addAll(state.getTaskSymbolTable().getValueSet());
-       while (!toanalyze.isEmpty()) {
-       Object obj = toanalyze.iterator().next();
-       ClassDescriptor cd = (ClassDescriptor) obj;
-       toanalyze.remove(cd);
+    // no need to analyze method having ssjava loop
+    sortedDescriptors.removeFirst();
 
-       if (cd.isClassLibrary()) {
-        // doesn't care about class libraries now
-        continue;
-       }
-       for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
-        MethodDescriptor md = (MethodDescriptor) method_it.next();
-        FlatMethod fm = state.getMethodFlat(md);
-        if (fm != null) {
-          LoopFinder loopFinder = new LoopFinder(fm);
-          Loops loops = loopFinder.getRootloop(fm);
-          Set loopSet = loops.nestedLoops();
-
-          for (Iterator iterator = loopSet.iterator(); iterator.hasNext();) {
-            Loops rootLoops = (Loops) iterator.next();
-            Set loopEntranceSet = rootLoops.loopEntrances();
-            for (Iterator iterator2 = loopEntranceSet.iterator(); iterator2.hasNext();) {
-              FlatNode loopEnter = (FlatNode) iterator2.next();
-              String flatNodeLabel = (String) state.fn2labelMap.get(loopEnter);
-              if (flatNodeLabel != null && flatNodeLabel.equals("ssjava")) {
-                System.out.println("encounting ss loop:" + loopEnter);
-                definitelyWrittenForward(loopEnter);
-              }
-            }
-          }
-        }
-
-       }
-       }
-
-       // check if there is a read statement with flag=TRUE
-       toanalyze.addAll(classtable.getValueSet());
-       toanalyze.addAll(state.getTaskSymbolTable().getValueSet());
-       while (!toanalyze.isEmpty()) {
-       Object obj = toanalyze.iterator().next();
-       ClassDescriptor cd = (ClassDescriptor) obj;
-       toanalyze.remove(cd);
-       if (cd.isClassLibrary()) {
-        // doesn't care about class libraries now
-        continue;
-       }
-       for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
-        MethodDescriptor md = (MethodDescriptor) method_it.next();
-        FlatMethod fm = state.getMethodFlat(md);
-        try {
-          checkMethodBody(fm);
-        } catch (Error e) {
-          System.out.println("Error in " + md);
-          throw e;
-        }
-       }
-       }
-     */
+    // analyze scheduled methods until there are no more to visit
+    while (!sortedDescriptors.isEmpty()) {
+      // start to analyze leaf node
+      MethodDescriptor md = sortedDescriptors.removeLast();
+      analyzeMethod(md);
+    }
 
   }
 
+  private void analyzeMethod(MethodDescriptor md) {
+    if (state.SSJAVADEBUG) {
+      System.out.println("Definitely written Analyzing: " + md);
+    }
 
+    FlatMethod fm = state.getMethodFlat(md);
 
+    Set<NTuple<Descriptor>> readSet = mapFlatMethodToRead.get(fm);
+    if (readSet == null) {
+      readSet = new HashSet<NTuple<Descriptor>>();
+      mapFlatMethodToRead.put(fm, readSet);
+    }
 
-  private void checkMethodBody(FlatMethod fm) {
+    Set<NTuple<Descriptor>> overWriteSet = mapFlatMethodToOverWrite.get(fm);
+    if (overWriteSet == null) {
+      overWriteSet = new HashSet<NTuple<Descriptor>>();
+      mapFlatMethodToOverWrite.put(fm, overWriteSet);
+    }
 
+    // intraprocedural analysis
     Set<FlatNode> flatNodesToVisit = new HashSet<FlatNode>();
-    Set<FlatNode> visited = new HashSet<FlatNode>();
     flatNodesToVisit.add(fm);
 
     while (!flatNodesToVisit.isEmpty()) {
-      FlatNode fn = (FlatNode) flatNodesToVisit.iterator().next();
-      visited.add(fn);
+      FlatNode fn = flatNodesToVisit.iterator().next();
       flatNodesToVisit.remove(fn);
 
-      checkMethodBody_nodeAction(fn);
+      Set<NTuple<Descriptor>> prev = mapFlatNodeToWrittenSet.get(fn);
+      Set<NTuple<Descriptor>> curr = new HashSet<NTuple<Descriptor>>();
+
+      for (int i = 0; i < fn.numPrev(); i++) {
+        FlatNode prevFn = fn.getPrev(i);
+        Set<NTuple<Descriptor>> in = mapFlatNodeToWrittenSet.get(prevFn);
+        if (in != null) {
+          merge(curr, in);
+        }
+      }
+
+      analyzeFlatNode(fn, curr, readSet, overWriteSet);
 
       // if a new result, schedule forward nodes for analysis
-      for (int i = 0; i < fn.numNext(); i++) {
-        FlatNode nn = fn.getNext(i);
-        if (!visited.contains(nn)) {
+      if (!curr.equals(prev)) {
+        mapFlatNodeToWrittenSet.put(fn, curr);
+
+        for (int i = 0; i < fn.numNext(); i++) {
+          FlatNode nn = fn.getNext(i);
           flatNodesToVisit.add(nn);
         }
       }
+
     }
 
+    System.out.println("READSET=" + mapFlatMethodToRead.get(fm));
+    System.out.println("OVERWRITESET=" + mapFlatMethodToOverWrite.get(fm));
+
   }
 
-  private void checkMethodBody_nodeAction(FlatNode fn) {
+  private void merge(Set<NTuple<Descriptor>> curr, Set<NTuple<Descriptor>> in) {
 
+    if (curr.isEmpty()) {
+      // WrittenSet has a special initial value which covers all possible
+      // elements
+      // For the first time of intersection, we can take all previous set
+      curr.addAll(in);
+    } else {
+      // otherwise, current set is the intersection of the two sets
+      curr.retainAll(in);
+    }
+
+  }
+
+  private void analyzeFlatNode(FlatNode fn, Set<NTuple<Descriptor>> writtenSet,
+      Set<NTuple<Descriptor>> readSet, Set<NTuple<Descriptor>> overWriteSet) {
     TempDescriptor lhs;
     TempDescriptor rhs;
     FieldDescriptor fld;
 
     switch (fn.kind()) {
+    case FKind.FlatMethod: {
+
+      // set up initial heap paths for method parameters
+      FlatMethod fm = (FlatMethod) fn;
+      for (int i = 0; i < fm.numParameters(); i++) {
+        TempDescriptor param = fm.getParameter(i);
+        NTuple<Descriptor> heapPath = new NTuple<Descriptor>();
+        heapPath.add(param);
+        mapHeapPath.put(param, heapPath);
+      }
+    }
+      break;
 
     case FKind.FlatOpNode: {
-
       FlatOpNode fon = (FlatOpNode) fn;
+      // for a normal assign node, need to propagate lhs's heap path to rhs
       if (fon.getOp().getOp() == Operation.ASSIGN) {
-        lhs = fon.getDest();
         rhs = fon.getLeft();
-        // read(rhs)
-        Hashtable<Descriptor, Hashtable<FlatNode, Boolean>> map = definitelyWrittenResults.get(fn);
-        if (map != null) {
-          if (map.get(rhs).get(fn).booleanValue()) {
-            // throw new Error("variable " + rhs
-            // +
-            // " was not overwritten in-between the same read statement by the out-most loop.");
-          }
+        lhs = fon.getDest();
+
+        NTuple<Descriptor> rhsHeapPath = mapHeapPath.get(rhs);
+        if (rhsHeapPath != null) {
+          mapHeapPath.put(lhs, mapHeapPath.get(rhs));
         }
 
       }
-
     }
-    break;
+      break;
 
-    case FKind.FlatFieldNode: {
+    case FKind.FlatFieldNode:
+    case FKind.FlatElementNode: {
+
+      // y=x.f;
 
       FlatFieldNode ffn = (FlatFieldNode) fn;
       lhs = ffn.getDst();
       rhs = ffn.getSrc();
       fld = ffn.getField();
 
-    }
-    break;
+      // set up heap path
+      NTuple<Descriptor> srcHeapPath = mapHeapPath.get(rhs);
+      NTuple<Descriptor> readingHeapPath = new NTuple<Descriptor>(srcHeapPath.getList());
+      readingHeapPath.add(fld);
+      mapHeapPath.put(lhs, readingHeapPath);
 
-    case FKind.FlatElementNode: {
+      // read (x.f)
+      // if WT doesnot have hp(x.f), add hp(x.f) to READ
+      if (!writtenSet.contains(readingHeapPath)) {
+        readSet.add(readingHeapPath);
+      }
 
-    }
-    break;
+      // need to kill hp(x.f) from WT
+      writtenSet.remove(readingHeapPath);
 
-    case FKind.FlatSetFieldNode: {
     }
-    break;
+      break;
 
+    case FKind.FlatSetFieldNode:
     case FKind.FlatSetElementNode: {
 
+      // x.f=y;
+      FlatSetFieldNode fsfn = (FlatSetFieldNode) fn;
+      lhs = fsfn.getDst();
+      fld = fsfn.getField();
+      rhs = fsfn.getSrc();
+
+      // set up heap path
+      NTuple<Descriptor> lhsHeapPath = mapHeapPath.get(lhs);
+      NTuple<Descriptor> newHeapPath = new NTuple<Descriptor>(lhsHeapPath.getList());
+      newHeapPath.add(fld);
+      mapHeapPath.put(fld, newHeapPath);
+
+      // write(x.f)
+      // need to add hp(y) to WT
+      writtenSet.add(newHeapPath);
+
     }
-    break;
+      break;
 
-    case FKind.FlatCall: {
+    case FKind.FlatExit: {
+      // merge the current written set with OVERWRITE set
+      merge(overWriteSet, writtenSet);
+    }
+      break;
 
     }
-    break;
+  }
+
+  // Borrowed it from disjoint analysis
+  protected LinkedList<MethodDescriptor> topologicalSort(Set<MethodDescriptor> toSort) {
+
+    Set<MethodDescriptor> discovered = new HashSet<MethodDescriptor>();
 
+    LinkedList<MethodDescriptor> sorted = new LinkedList<MethodDescriptor>();
+
+    Iterator<MethodDescriptor> itr = toSort.iterator();
+    while (itr.hasNext()) {
+      MethodDescriptor d = itr.next();
+
+      if (!discovered.contains(d)) {
+        dfsVisit(d, toSort, sorted, discovered);
+      }
+    }
+
+    return sorted;
+  }
+
+  // While we're doing DFS on call graph, remember
+  // dependencies for efficient queuing of methods
+  // during interprocedural analysis:
+  //
+  // a dependent of a method decriptor d for this analysis is:
+  // 1) a method or task that invokes d
+  // 2) in the descriptorsToAnalyze set
+  protected void dfsVisit(MethodDescriptor md, Set<MethodDescriptor> toSort,
+      LinkedList<MethodDescriptor> sorted, Set<MethodDescriptor> discovered) {
+
+    discovered.add(md);
+
+    // otherwise call graph guides DFS
+    Iterator itr = callGraph.getCallerSet(md).iterator();
+    while (itr.hasNext()) {
+      MethodDescriptor dCaller = (MethodDescriptor) itr.next();
+
+      // only consider callers in the original set to analyze
+      if (!toSort.contains(dCaller)) {
+        continue;
+      }
+
+      if (!discovered.contains(dCaller)) {
+        addDependent(md, // callee
+            dCaller // caller
+        );
+
+        dfsVisit(dCaller, toSort, sorted, discovered);
+      }
     }
 
+    // for leaf-nodes last now!
+    sorted.addLast(md);
+  }
+
+  // a dependent of a method decriptor d for this analysis is:
+  // 1) a method or task that invokes d
+  // 2) in the descriptorsToAnalyze set
+  protected void addDependent(MethodDescriptor callee, MethodDescriptor caller) {
+    Set<MethodDescriptor> deps = mapDescriptorToSetDependents.get(callee);
+    if (deps == null) {
+      deps = new HashSet<MethodDescriptor>();
+    }
+    deps.add(caller);
+    mapDescriptorToSetDependents.put(callee, deps);
   }
 
   private void definitelyWrittenForward(FlatNode entrance) {
@@ -230,7 +331,7 @@ public class DefinitelyWrittenCheck {
       Hashtable<Descriptor, Hashtable<FlatNode, Boolean>> prev = definitelyWrittenResults.get(fn);
 
       Hashtable<Descriptor, Hashtable<FlatNode, Boolean>> curr =
-        new Hashtable<Descriptor, Hashtable<FlatNode, Boolean>>();
+          new Hashtable<Descriptor, Hashtable<FlatNode, Boolean>>();
       for (int i = 0; i < fn.numPrev(); i++) {
         FlatNode nn = fn.getPrev(i);
         Hashtable<Descriptor, Hashtable<FlatNode, Boolean>> dwIn = definitelyWrittenResults.get(nn);
@@ -254,15 +355,15 @@ public class DefinitelyWrittenCheck {
   }
 
   private void mergeResults(Hashtable<Descriptor, Hashtable<FlatNode, Boolean>> curr,
-                            Hashtable<Descriptor, Hashtable<FlatNode, Boolean>> in) {
+      Hashtable<Descriptor, Hashtable<FlatNode, Boolean>> in) {
 
     Set<Descriptor> inKeySet = in.keySet();
-    for (Iterator iterator = inKeySet.iterator(); iterator.hasNext(); ) {
+    for (Iterator iterator = inKeySet.iterator(); iterator.hasNext();) {
       Descriptor inKey = (Descriptor) iterator.next();
       Hashtable<FlatNode, Boolean> inPair = in.get(inKey);
 
       Set<FlatNode> pairKeySet = inPair.keySet();
-      for (Iterator iterator2 = pairKeySet.iterator(); iterator2.hasNext(); ) {
+      for (Iterator iterator2 = pairKeySet.iterator(); iterator2.hasNext();) {
         FlatNode pairKey = (FlatNode) iterator2.next();
         Boolean inFlag = inPair.get(pairKey);
 
@@ -286,17 +387,17 @@ public class DefinitelyWrittenCheck {
   }
 
   private void definitelyWritten_nodeActions(FlatNode fn,
-                                             Hashtable<Descriptor, Hashtable<FlatNode, Boolean>> curr, FlatNode entrance) {
+      Hashtable<Descriptor, Hashtable<FlatNode, Boolean>> curr, FlatNode entrance) {
 
     if (fn == entrance) {
 
       Set<Descriptor> keySet = curr.keySet();
-      for (Iterator iterator = keySet.iterator(); iterator.hasNext(); ) {
+      for (Iterator iterator = keySet.iterator(); iterator.hasNext();) {
         Descriptor key = (Descriptor) iterator.next();
         Hashtable<FlatNode, Boolean> pair = curr.get(key);
         if (pair != null) {
           Set<FlatNode> pairKeySet = pair.keySet();
-          for (Iterator iterator2 = pairKeySet.iterator(); iterator2.hasNext(); ) {
+          for (Iterator iterator2 = pairKeySet.iterator(); iterator2.hasNext();) {
             FlatNode pairKey = (FlatNode) iterator2.next();
             pair.put(pairKey, Boolean.TRUE);
           }
@@ -337,7 +438,7 @@ public class DefinitelyWrittenCheck {
         System.out.println("WRITING LOC=" + lhs.getType().getExtension());
 
       }
-      break;
+        break;
 
       case FKind.FlatLiteralNode: {
         FlatLiteralNode fln = (FlatLiteralNode) fn;
@@ -349,7 +450,7 @@ public class DefinitelyWrittenCheck {
         System.out.println("WRITING LOC=" + lhs.getType().getExtension());
 
       }
-      break;
+        break;
 
       case FKind.FlatFieldNode:
       case FKind.FlatElementNode: {
@@ -374,7 +475,7 @@ public class DefinitelyWrittenCheck {
         System.out.println("READ LOClhs=" + lhs.getType().getExtension());
 
       }
-      break;
+        break;
 
       case FKind.FlatSetFieldNode:
       case FKind.FlatSetElementNode: {
@@ -389,12 +490,12 @@ public class DefinitelyWrittenCheck {
         System.out.println("WRITELOC LOC=" + fld.getType().getExtension());
 
       }
-      break;
+        break;
 
       case FKind.FlatCall: {
 
       }
-      break;
+        break;
 
       }
     }
diff --git a/Robust/src/Analysis/SSJava/NTuple.java b/Robust/src/Analysis/SSJava/NTuple.java
index 85f8759a..30dfd39b 100644
--- a/Robust/src/Analysis/SSJava/NTuple.java
+++ b/Robust/src/Analysis/SSJava/NTuple.java
@@ -1,7 +1,6 @@
 package Analysis.SSJava;
 
 import java.util.ArrayList;
-import java.util.Arrays;
 import java.util.Collection;
 import java.util.List;
 
@@ -9,8 +8,9 @@ public class NTuple<T> {
 
   private List<T> elements;
 
-  public NTuple(T... elements) {
-    this.elements = Arrays.asList(elements);
+  public NTuple(List<T> l) {
+    this.elements = new ArrayList<T>();
+    this.elements.addAll(l);
   }
 
   public NTuple() {
@@ -29,7 +29,7 @@ public class NTuple<T> {
     return elements.size();
   }
 
-  public void addElement(T newElement) {
+  public void add(T newElement) {
     this.elements.add(newElement);
   }
 
diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
index c9e0e900..f5357f35 100644
--- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
+++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
@@ -7,6 +7,7 @@ import java.util.Set;
 import java.util.StringTokenizer;
 import java.util.Vector;
 
+import Analysis.CallGraph.CallGraph;
 import Analysis.Loops.LoopOptimize;
 import Analysis.Loops.LoopTerminate;
 import IR.AnnotationDescriptor;
@@ -48,9 +49,12 @@ public class SSJavaAnalysis {
   // method set that does not have loop termination analysis
   Hashtable<MethodDescriptor, Integer> skipLoopTerminate;
 
-  public SSJavaAnalysis(State state, TypeUtil tu) {
+  CallGraph callgraph;
+
+  public SSJavaAnalysis(State state, TypeUtil tu, CallGraph callgraph) {
     this.state = state;
     this.tu = tu;
+    this.callgraph = callgraph;
     this.cd2lattice = new Hashtable<ClassDescriptor, SSJavaLattice<String>>();
     this.cd2methodDefault = new Hashtable<ClassDescriptor, MethodLattice<String>>();
     this.md2lattice = new Hashtable<MethodDescriptor, MethodLattice<String>>();
@@ -89,7 +93,7 @@ public class SSJavaAnalysis {
   }
 
   public void doDefinitelyWrittenCheck() {
-    DefinitelyWrittenCheck checker = new DefinitelyWrittenCheck(state);
+    DefinitelyWrittenCheck checker = new DefinitelyWrittenCheck(this, state);
     checker.definitelyWrittenCheck();
   }
 
@@ -285,4 +289,8 @@ public class SSJavaAnalysis {
 
   }
 
+  public CallGraph getCallGraph() {
+    return callgraph;
+  }
+
 }
diff --git a/Robust/src/Analysis/SSJava/SingleReferenceCheck.java b/Robust/src/Analysis/SSJava/SingleReferenceCheck.java
index baae40db..8bc6a8c8 100644
--- a/Robust/src/Analysis/SSJava/SingleReferenceCheck.java
+++ b/Robust/src/Analysis/SSJava/SingleReferenceCheck.java
@@ -18,7 +18,7 @@ import IR.Tree.SubBlockNode;
 
 public class SingleReferenceCheck {
 
-  static State state;
+  State state;
   SSJavaAnalysis ssjava;
   String needToNullify = null;
 
diff --git a/Robust/src/Main/Main.java b/Robust/src/Main/Main.java
index d7d3c7ec..c2bc4eb0 100644
--- a/Robust/src/Main/Main.java
+++ b/Robust/src/Main/Main.java
@@ -481,7 +481,7 @@ 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);
+    SSJavaAnalysis ssjava=new SSJavaAnalysis(state,tu,callgraph);
     if(state.SSJAVA) {
       ssjava.doCheck();
       State.logEvent("Done SSJava Checking");