bring recent changes before starting to implement definitely written analysis for...

diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
index 2a0d0c93b79f13363c0fc3a9b33f375636e3bf01..65027b5bdab38825415e59af2a99d169faa0058c 100644 (file)
--- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
+++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
@@ -159,6 +159,7 @@ public class DefinitelyWrittenCheck {
 
   private void writtenAnalysis_nodeAction(FlatNode fn,
       Hashtable<NTuple<Descriptor>, Hashtable<FlatNode, Boolean>> curr, FlatNode loopEntrance) {
+
     if (fn.equals(loopEntrance)) {
       // it reaches loop entrance: changes all flag to true
       Set<NTuple<Descriptor>> keySet = curr.keySet();
@@ -250,7 +251,6 @@ public class DefinitelyWrittenCheck {
         break;
 
       case FKind.FlatCall: {
-
         FlatCall fc = (FlatCall) fn;
         bindHeapPathCallerArgWithCaleeParam(fc);
 
@@ -269,7 +269,7 @@ public class DefinitelyWrittenCheck {
           if (currentStatus == null) {
             gen.put(fn, Boolean.FALSE);
           } else {
-            checkFlag(currentStatus.booleanValue(), fn);
+            checkFlag(currentStatus.booleanValue(), fn, read);
           }
         }
 
@@ -299,7 +299,7 @@ public class DefinitelyWrittenCheck {
     if (currentStatus == null) {
       gen.put(fn, Boolean.FALSE);
     } else {
-      checkFlag(currentStatus.booleanValue(), fn);
+      checkFlag(currentStatus.booleanValue(), fn, hp);
     }
 
   }
@@ -341,8 +341,13 @@ public class DefinitelyWrittenCheck {
         new Hashtable<Integer, NTuple<Descriptor>>();
 
     // arg idx is starting from 'this' arg
-    NTuple<Descriptor> thisHeapPath = new NTuple<Descriptor>();
-    thisHeapPath.add(fc.getThis());
+    NTuple<Descriptor> thisHeapPath = mapHeapPath.get(fc.getThis());
+    if (thisHeapPath == null) {
+      // method is called without creating new flat node representing 'this'
+      thisHeapPath = new NTuple<Descriptor>();
+      thisHeapPath.add(fc.getThis());
+    }
+
     mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath);
 
     for (int i = 0; i < fc.numArgs(); i++) {
@@ -390,12 +395,13 @@ public class DefinitelyWrittenCheck {
 
   }
 
-  private void checkFlag(boolean booleanValue, FlatNode fn) {
+  private void checkFlag(boolean booleanValue, FlatNode fn, NTuple<Descriptor> hp) {
     if (booleanValue) {
       throw new Error(
-          "There is a variable who comes back to the same read statement without being overwritten at the out-most iteration at "
-              + methodContainingSSJavaLoop.getClassDesc().getSourceFileName()
-              + "::"
+          "There is a variable, which is reachable through references "
+              + hp
+              + ", who comes back to the same read statement without being overwritten at the out-most iteration at "
+              + methodContainingSSJavaLoop.getClassDesc().getSourceFileName() + "::"
               + fn.getNumLine());
     }
   }
@@ -582,20 +588,25 @@ public class DefinitelyWrittenCheck {
 
       // 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);
-
-      // read (x.f)
-      if (fld.getType().isImmutable()) {
-        // if WT doesnot have hp(x.f), add hp(x.f) to READ
-        if (!writtenSet.contains(readingHeapPath)) {
-          readSet.add(readingHeapPath);
+      if (srcHeapPath != null) {
+        // if lhs srcHeapPath is null, it means that it is not reachable from
+        // callee's parameters. so just ignore it
+
+        NTuple<Descriptor> readingHeapPath = new NTuple<Descriptor>(srcHeapPath.getList());
+        readingHeapPath.add(fld);
+        mapHeapPath.put(lhs, readingHeapPath);
+
+        // read (x.f)
+        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
-      writtenSet.remove(readingHeapPath);
+        // need to kill hp(x.f) from WT
+        writtenSet.remove(readingHeapPath);
+      }
 
     }
       break;
@@ -611,13 +622,17 @@ public class DefinitelyWrittenCheck {
 
       // 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);
+      if (lhsHeapPath != null) {
+        // if lhs heap path is null, it means that it is not reachable from
+        // callee's parameters. so just ignore it
+        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;

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index b14fecfc30ac38912e96e0fd7ccc5fbbdb1464de..7978daa1bb84f2c44af12427a94bd7c41a3dec23 100644 (file)
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -376,7 +376,7 @@ public class FlowDownCheck {
 
       CompositeLocation condLoc =
           checkLocationFromExpressionNode(md, nametable, ln.getCondition(), new CompositeLocation());
-      addTypeLocation(ln.getCondition().getType(), (condLoc));
+      addLocationType(ln.getCondition().getType(), (condLoc));
 
       CompositeLocation bodyLoc = checkLocationFromBlockNode(md, nametable, ln.getBody());
 
@@ -398,26 +398,40 @@ public class FlowDownCheck {
       CompositeLocation condLoc =
           checkLocationFromExpressionNode(md, bn.getVarTable(), ln.getCondition(),
               new CompositeLocation());
-      addTypeLocation(ln.getCondition().getType(), condLoc);
+      addLocationType(ln.getCondition().getType(), condLoc);
 
       CompositeLocation updateLoc =
           checkLocationFromBlockNode(md, bn.getVarTable(), ln.getUpdate());
 
       Set<CompositeLocation> glbInputSet = new HashSet<CompositeLocation>();
       glbInputSet.add(condLoc);
-      glbInputSet.add(updateLoc);
+//      glbInputSet.add(updateLoc);
 
       CompositeLocation glbLocOfForLoopCond = CompositeLattice.calculateGLB(glbInputSet);
 
       // check location of 'forloop' body
       CompositeLocation blockLoc = checkLocationFromBlockNode(md, bn.getVarTable(), ln.getBody());
 
+      // compute glb of body including loop body and update statement
+      glbInputSet.clear();
+      
       if (blockLoc == null) {
         // when there is no statement in the loop body
-        return glbLocOfForLoopCond;
+        
+        if(updateLoc==null){
+          // also there is no update statement in the loop body
+          return glbLocOfForLoopCond;
+        }
+        glbInputSet.add(updateLoc);
+        
+      }else{
+        glbInputSet.add(blockLoc);
+        glbInputSet.add(updateLoc);
       }
+      
+      CompositeLocation loopBodyLoc = CompositeLattice.calculateGLB(glbInputSet);
 
-      if (!CompositeLattice.isGreaterThan(glbLocOfForLoopCond, blockLoc)) {
+      if (!CompositeLattice.isGreaterThan(glbLocOfForLoopCond, loopBodyLoc)) {
         throw new Error(
             "The location of the for-condition statement is lower than the for-loop body at "
                 + cd.getSourceFileName() + ":" + ln.getCondition().getNumLine());
@@ -442,7 +456,7 @@ public class FlowDownCheck {
     CompositeLocation condLoc =
         checkLocationFromExpressionNode(md, nametable, isn.getCondition(), new CompositeLocation());
 
-    addTypeLocation(isn.getCondition().getType(), condLoc);
+    addLocationType(isn.getCondition().getType(), condLoc);
     glbInputSet.add(condLoc);
 
     CompositeLocation locTrueBlock = checkLocationFromBlockNode(md, nametable, isn.getTrueBlock());
@@ -611,13 +625,13 @@ public class FlowDownCheck {
 
     CompositeLocation condLoc =
         checkLocationFromExpressionNode(md, nametable, tn.getCond(), new CompositeLocation());
-    addTypeLocation(tn.getCond().getType(), condLoc);
+    addLocationType(tn.getCond().getType(), condLoc);
     CompositeLocation trueLoc =
         checkLocationFromExpressionNode(md, nametable, tn.getTrueExpr(), new CompositeLocation());
-    addTypeLocation(tn.getTrueExpr().getType(), trueLoc);
+    addLocationType(tn.getTrueExpr().getType(), trueLoc);
     CompositeLocation falseLoc =
         checkLocationFromExpressionNode(md, nametable, tn.getFalseExpr(), new CompositeLocation());
-    addTypeLocation(tn.getFalseExpr().getType(), falseLoc);
+    addLocationType(tn.getFalseExpr().getType(), falseLoc);
 
     // check if condLoc is higher than trueLoc & falseLoc
     if (!CompositeLattice.isGreaterThan(condLoc, trueLoc)) {
@@ -769,7 +783,7 @@ public class FlowDownCheck {
       CompositeLocation argLoc =
           checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation());
       glbInputSet.add(argLoc);
-      addTypeLocation(en.getType(), argLoc);
+      addLocationType(en.getType(), argLoc);
     }
 
     // check array initializers
@@ -934,7 +948,6 @@ public class FlowDownCheck {
 
     ExpressionNode left = fan.getExpression();
     loc = checkLocationFromExpressionNode(md, nametable, left, loc);
-    // addTypeLocation(left.getType(), loc);
 
     if (!left.getType().isPrimitive()) {
       FieldDescriptor fd = fan.getField();
@@ -1020,11 +1033,11 @@ public class FlowDownCheck {
         if (locDec.startsWith(SSJavaAnalysis.DELTA)) {
           DeltaLocation deltaLoc = parseDeltaDeclaration(md, n, locDec);
           d2loc.put(vd, deltaLoc);
-          addTypeLocation(vd.getType(), deltaLoc);
+          addLocationType(vd.getType(), deltaLoc);
         } else {
           CompositeLocation compLoc = parseLocationDeclaration(md, n, locDec);
           d2loc.put(vd, compLoc);
-          addTypeLocation(vd.getType(), compLoc);
+          addLocationType(vd.getType(), compLoc);
         }
 
       }
@@ -1170,21 +1183,20 @@ public class FlowDownCheck {
               + cd.getSourceFileName() + ".");
         }
         Location loc = new Location(cd, locationID);
-        // d2loc.put(fd, loc);
-        addTypeLocation(fd.getType(), loc);
+        addLocationType(fd.getType(), loc);
 
       }
     }
 
   }
 
-  private void addTypeLocation(TypeDescriptor type, CompositeLocation loc) {
+  private void addLocationType(TypeDescriptor type, CompositeLocation loc) {
     if (type != null) {
       type.setExtension(loc);
     }
   }
 
-  private void addTypeLocation(TypeDescriptor type, Location loc) {
+  private void addLocationType(TypeDescriptor type, Location loc) {
     if (type != null) {
       type.setExtension(loc);
     }