bug fixes

diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
index d99f44f4ee978c9c21fde04bfea999c5f1cb909c..2a0d0c93b79f13363c0fc3a9b33f375636e3bf01 100644 (file)
--- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
+++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
@@ -187,30 +187,15 @@ public class DefinitelyWrittenCheck {
         NTuple<Descriptor> rhsHeapPath = computePath(rhs);
         if (!rhs.getType().isImmutable()) {
           mapHeapPath.put(lhs, rhsHeapPath);
-        }
-
-        if (fon.getOp().getOp() == Operation.ASSIGN) {
-          // read(rhs)
-          Hashtable<FlatNode, Boolean> gen = curr.get(rhsHeapPath);
-
-          if (gen == null) {
-            gen = new Hashtable<FlatNode, Boolean>();
-            curr.put(rhsHeapPath, gen);
-          }
-          Boolean currentStatus = gen.get(fn);
-          if (currentStatus == null) {
-            gen.put(fn, Boolean.FALSE);
-          } else {
-            if (!rhs.getType().isClass()) {
-              checkFlag(currentStatus.booleanValue(), fn);
-            }
+        } else {
+          if (fon.getOp().getOp() == Operation.ASSIGN) {
+            // read(rhs)
+            readValue(fn, rhsHeapPath, curr);
           }
-
+          // write(lhs)
+          NTuple<Descriptor> lhsHeapPath = computePath(lhs);
+          removeHeapPath(curr, lhsHeapPath);
         }
-        // write(lhs)
-        NTuple<Descriptor> lhsHeapPath = computePath(lhs);
-        removeHeapPath(curr, lhsHeapPath);
-        // curr.put(lhsHeapPath, new Hashtable<FlatNode, Boolean>());
       }
         break;
 
@@ -229,26 +214,21 @@ public class DefinitelyWrittenCheck {
       case FKind.FlatElementNode: {
 
         FlatFieldNode ffn = (FlatFieldNode) fn;
-        lhs = ffn.getSrc();
+        lhs = ffn.getDst();
+        rhs = ffn.getSrc();
         fld = ffn.getField();
 
         // read field
-        NTuple<Descriptor> srcHeapPath = mapHeapPath.get(lhs);
+        NTuple<Descriptor> srcHeapPath = mapHeapPath.get(rhs);
         NTuple<Descriptor> fldHeapPath = new NTuple<Descriptor>(srcHeapPath.getList());
         fldHeapPath.add(fld);
-        Hashtable<FlatNode, Boolean> gen = curr.get(fldHeapPath);
 
-        if (gen == null) {
-          gen = new Hashtable<FlatNode, Boolean>();
-          curr.put(fldHeapPath, gen);
+        if (fld.getType().isImmutable()) {
+          readValue(fn, fldHeapPath, curr);
         }
 
-        Boolean currentStatus = gen.get(fn);
-        if (currentStatus == null) {
-          gen.put(fn, Boolean.FALSE);
-        } else {
-          checkFlag(currentStatus.booleanValue(), fn);
-        }
+        // propagate rhs's heap path to the lhs
+        mapHeapPath.put(lhs, fldHeapPath);
 
       }
         break;
@@ -261,11 +241,10 @@ public class DefinitelyWrittenCheck {
         fld = fsfn.getField();
 
         // write(field)
-        NTuple<Descriptor> lhsHeapPath = mapHeapPath.get(lhs);
+        NTuple<Descriptor> lhsHeapPath = computePath(lhs);
         NTuple<Descriptor> fldHeapPath = new NTuple<Descriptor>(lhsHeapPath.getList());
         fldHeapPath.add(fld);
         removeHeapPath(curr, fldHeapPath);
-        // curr.put(fldHeapPath, new Hashtable<FlatNode, Boolean>());
 
       }
         break;
@@ -273,7 +252,6 @@ public class DefinitelyWrittenCheck {
       case FKind.FlatCall: {
 
         FlatCall fc = (FlatCall) fn;
-
         bindHeapPathCallerArgWithCaleeParam(fc);
 
         // add <hp,statement,false> in which hp is an element of
@@ -301,13 +279,27 @@ public class DefinitelyWrittenCheck {
         for (Iterator iterator = calleeIntersectBoundOverWriteSet.iterator(); iterator.hasNext();) {
           NTuple<Descriptor> write = (NTuple<Descriptor>) iterator.next();
           removeHeapPath(curr, write);
-          // curr.put(write, new Hashtable<FlatNode, Boolean>());
         }
       }
         break;
 
       }
+    }
 
+  }
+
+  private void readValue(FlatNode fn, NTuple<Descriptor> hp,
+      Hashtable<NTuple<Descriptor>, Hashtable<FlatNode, Boolean>> curr) {
+    Hashtable<FlatNode, Boolean> gen = curr.get(hp);
+    if (gen == null) {
+      gen = new Hashtable<FlatNode, Boolean>();
+      curr.put(hp, gen);
+    }
+    Boolean currentStatus = gen.get(fn);
+    if (currentStatus == null) {
+      gen.put(fn, Boolean.FALSE);
+    } else {
+      checkFlag(currentStatus.booleanValue(), fn);
     }
 
   }
@@ -334,6 +326,10 @@ public class DefinitelyWrittenCheck {
     // transform all READ/OVERWRITE set from the any possible
     // callees to the
     // caller
+
+    calleeUnionBoundReadSet.clear();
+    calleeIntersectBoundOverWriteSet.clear();
+
     MethodDescriptor mdCallee = fc.getMethod();
     FlatMethod fmCallee = state.getMethodFlat(mdCallee);
     Set<MethodDescriptor> setPossibleCallees = new HashSet<MethodDescriptor>();
@@ -360,6 +356,7 @@ public class DefinitelyWrittenCheck {
       FlatMethod calleeFlatMethod = state.getMethodFlat(callee);
 
       // binding caller's args and callee's params
+
       Set<NTuple<Descriptor>> calleeReadSet = mapFlatMethodToRead.get(calleeFlatMethod);
       if (calleeReadSet == null) {
         calleeReadSet = new HashSet<NTuple<Descriptor>>();
@@ -396,8 +393,9 @@ public class DefinitelyWrittenCheck {
   private void checkFlag(boolean booleanValue, FlatNode fn) {
     if (booleanValue) {
       throw new Error(
-          "There is a variable who comes back to the same read statement at the out-most iteration at "
-              + methodContainingSSJavaLoop.getClassDesc().getSourceFileName() + "::"
+          "There is a variable who comes back to the same read statement without being overwritten at the out-most iteration at "
+              + methodContainingSSJavaLoop.getClassDesc().getSourceFileName()
+              + "::"
               + fn.getNumLine());
     }
   }
@@ -502,11 +500,13 @@ public class DefinitelyWrittenCheck {
 
     // intraprocedural analysis
     Set<FlatNode> flatNodesToVisit = new HashSet<FlatNode>();
+    Set<FlatNode> visited = new HashSet<FlatNode>();
     flatNodesToVisit.add(fm);
 
     while (!flatNodesToVisit.isEmpty()) {
       FlatNode fn = flatNodesToVisit.iterator().next();
       flatNodesToVisit.remove(fn);
+      visited.add(fn);
 
       Set<NTuple<Descriptor>> curr = new HashSet<NTuple<Descriptor>>();
 
@@ -524,7 +524,9 @@ public class DefinitelyWrittenCheck {
 
       for (int i = 0; i < fn.numNext(); i++) {
         FlatNode nn = fn.getNext(i);
-        flatNodesToVisit.add(nn);
+        if (!visited.contains(nn)) {
+          flatNodesToVisit.add(nn);
+        }
       }
 
     }
@@ -585,9 +587,11 @@ public class DefinitelyWrittenCheck {
       mapHeapPath.put(lhs, readingHeapPath);
 
       // read (x.f)
-      // if WT doesnot have hp(x.f), add hp(x.f) to READ
-      if (!writtenSet.contains(readingHeapPath)) {
-        readSet.add(readingHeapPath);
+      if (fld.getType().isImmutable()) {
+        // if WT doesnot have hp(x.f), add hp(x.f) to READ
+        if (!writtenSet.contains(readingHeapPath)) {
+          readSet.add(readingHeapPath);
+        }
       }
 
       // need to kill hp(x.f) from WT
@@ -656,7 +660,6 @@ public class DefinitelyWrittenCheck {
   }
 
   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

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 970b19291cee8f407658cef897ef4e9539be2cc5..b14fecfc30ac38912e96e0fd7ccc5fbbdb1464de 100644 (file)
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -713,10 +713,10 @@ public class FlowDownCheck {
               VarDescriptor calleevd2 = (VarDescriptor) min.getMethod().getParameter(currentIdx);
               CompositeLocation calleeLoc2 = d2loc.get(calleevd2);
 
-              boolean callerResult = CompositeLattice.isGreaterThan(callerArg1, callerArg2);
-              boolean calleeResult = CompositeLattice.isGreaterThan(calleeLoc1, calleeLoc2);
-
-              if (calleeResult && !callerResult) {
+              int callerResult = CompositeLattice.compare(callerArg1, callerArg2);
+              int calleeResult = CompositeLattice.compare(calleeLoc1, calleeLoc2);
+              if (calleeResult == ComparisonResult.GREATER
+                  && callerResult != ComparisonResult.GREATER) {
                 // If calleeLoc1 is higher than calleeLoc2
                 // then, caller should have same ordering relation in-bet
                 // callerLoc1 & callerLoc2
@@ -1194,9 +1194,7 @@ public class FlowDownCheck {
 
     public static boolean isGreaterThan(CompositeLocation loc1, CompositeLocation loc2) {
 
-      // System.out.println("isGreaterThan= " + loc1 + " " + loc2);
-
-      int baseCompareResult = compareBaseLocationSet(loc1, loc2);
+      int baseCompareResult = compareBaseLocationSet(loc1, loc2, true);
       if (baseCompareResult == ComparisonResult.EQUAL) {
         if (compareDelta(loc1, loc2) == ComparisonResult.GREATER) {
           return true;
@@ -1214,7 +1212,7 @@ public class FlowDownCheck {
     public static int compare(CompositeLocation loc1, CompositeLocation loc2) {
 
       // System.out.println("compare=" + loc1 + " " + loc2);
-      int baseCompareResult = compareBaseLocationSet(loc1, loc2);
+      int baseCompareResult = compareBaseLocationSet(loc1, loc2, false);
 
       if (baseCompareResult == ComparisonResult.EQUAL) {
         return compareDelta(loc1, loc2);
@@ -1245,7 +1243,8 @@ public class FlowDownCheck {
 
     }
 
-    private static int compareBaseLocationSet(CompositeLocation compLoc1, CompositeLocation compLoc2) {
+    private static int compareBaseLocationSet(CompositeLocation compLoc1,
+        CompositeLocation compLoc2, boolean awareSharedLoc) {
 
       // if compLoc1 is greater than compLoc2, return true
       // else return false;
@@ -1297,7 +1296,7 @@ public class FlowDownCheck {
           // check if the current location is the spinning location
           // note that the spinning location only can be appeared in the last
           // part of the composite location
-          if (numOfTie == compLoc1.getSize()
+          if (awareSharedLoc && numOfTie == compLoc1.getSize()
               && lattice1.getSpinLocSet().contains(loc1.getLocIdentifier())) {
             return ComparisonResult.GREATER;
           }

diff --git a/Robust/src/Analysis/SSJava/NTuple.java b/Robust/src/Analysis/SSJava/NTuple.java
index d69708deb42220cc3e6268da00f9f952e7c24eec..800c36529aac183f32858d3482d79a5e9d602dde 100644 (file)
--- a/Robust/src/Analysis/SSJava/NTuple.java
+++ b/Robust/src/Analysis/SSJava/NTuple.java
@@ -77,12 +77,14 @@ public class NTuple<T> {
     }
 
     for (int i = 0; i < prefix.size(); i++) {
-      if (prefix.get(i).equals(get(i))) {
+      if (!prefix.get(i).equals(get(i))) {
         return false;
       }
     }
     return true;
 
   }
+  
+  
 
 }