associate assignment nodes that writes to the same height location with corresponding...

diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
index fd02c24d4f91e3f113318a31cafe22c908b37ac3..c2790bfbd21356a6a1e9af401056262c2ecda561 100644 (file)
--- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
+++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
@@ -449,7 +449,8 @@ public class DefinitelyWrittenCheck {
 
         // computing gen/kill set
         computeKILLSetForWrite(curr, killSet, fieldLocTuple, fldHeapPath);
-        if (!fieldLoc.equals(srcLoc)) {
+
+        if (!ssjava.isSameHeightWrite(fn)) {
           computeGENSetForHigherWrite(curr, genSet, fieldLocTuple, fldHeapPath);
           updateDeleteSetForHigherWrite(currDeleteSet, fieldLocTuple, fldHeapPath);
         } else {
@@ -793,8 +794,13 @@ public class DefinitelyWrittenCheck {
         fld = getArrayField(td);
       }
 
+      NTuple<Location> lhsLocTuple = new NTuple<Location>();
+      lhsLocTuple.addAll(deriveLocationTuple(md, lhs));
+      mapDescriptorToLocationPath.put(lhs, lhsLocTuple);
+
       NTuple<Location> fieldLocTuple = new NTuple<Location>();
-      fieldLocTuple.addAll(deriveLocationTuple(md, lhs));
+      fieldLocTuple.addAll(lhsLocTuple);
+
       if (fn.kind() == FKind.FlatSetFieldNode) {
         fieldLocTuple.add((Location) fld.getType().getExtension());
       }

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 8ff79e398032c8652695b791848a87c93fc22e2b..9cbe54bde105816425298b208b1552548405de42 100644 (file)
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -25,6 +25,7 @@ import IR.SymbolTable;
 import IR.TypeDescriptor;
 import IR.TypeExtension;
 import IR.VarDescriptor;
+import IR.Flat.FlatNode;
 import IR.Tree.ArrayAccessNode;
 import IR.Tree.AssignmentNode;
 import IR.Tree.BlockExpressionNode;
@@ -1527,10 +1528,10 @@ public class FlowDownCheck {
       }
       // }
 
-//      System.out.println("dstLocation=" + destLocation);
-//      System.out.println("rhsLocation=" + rhsLocation);
-//      System.out.println("srcLocation=" + srcLocation);
-//      System.out.println("constraint=" + constraint);
+      // System.out.println("dstLocation=" + destLocation);
+      // System.out.println("rhsLocation=" + rhsLocation);
+      // System.out.println("srcLocation=" + srcLocation);
+      // System.out.println("constraint=" + constraint);
 
       if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, generateErrorMessage(cd, an))) {
 
@@ -1544,6 +1545,16 @@ public class FlowDownCheck {
             + " at " + cd.getSourceFileName() + "::" + an.getNumLine());
       }
 
+      if (srcLocation.equals(destLocation)) {
+        // keep it for definitely written analysis
+        Set<FlatNode> flatNodeSet = ssjava.getBuildFlat().getFlatNodeSet(an);
+        for (Iterator iterator = flatNodeSet.iterator(); iterator.hasNext();) {
+          FlatNode fn = (FlatNode) iterator.next();
+          ssjava.addSameHeightWriteFlatNode(fn);
+        }
+
+      }
+
     } else {
       destLocation =
           rhsLocation =
@@ -1576,6 +1587,15 @@ public class FlowDownCheck {
 
       }
 
+      if (srcLocation.equals(destLocation)) {
+        // keep it for definitely written analysis
+        Set<FlatNode> flatNodeSet = ssjava.getBuildFlat().getFlatNodeSet(an);
+        for (Iterator iterator = flatNodeSet.iterator(); iterator.hasNext();) {
+          FlatNode fn = (FlatNode) iterator.next();
+          ssjava.addSameHeightWriteFlatNode(fn);
+        }
+      }
+
     }
 
     return destLocation;

diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
index 58369f8f6e4c885abe7ad5dd8bd1891b4ee81b3d..7326d7e9b01455c2ba2ca270e7208f4ff1f2814c 100644 (file)
--- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
+++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
@@ -87,6 +87,8 @@ public class SSJavaAnalysis {
   // keep the field ownership from the linear type checking
   Hashtable<MethodDescriptor, Set<FieldDescriptor>> mapMethodToOwnedFieldSet;
 
+  Set<FlatNode> sameHeightWriteFlatNodeSet;
+
   CallGraph callgraph;
 
   LinearTypeCheck checker;
@@ -106,6 +108,7 @@ public class SSJavaAnalysis {
     this.bf = bf;
     this.trustWorthyMDSet = new HashSet<MethodDescriptor>();
     this.mapMethodToOwnedFieldSet = new Hashtable<MethodDescriptor, Set<FieldDescriptor>>();
+    this.sameHeightWriteFlatNodeSet = new HashSet<FlatNode>();
   }
 
   public void doCheck() {
@@ -560,4 +563,12 @@ public class SSJavaAnalysis {
     this.ssjavaLoopEntrance = ssjavaLoopEntrance;
   }
 
+  public void addSameHeightWriteFlatNode(FlatNode fn) {
+    this.sameHeightWriteFlatNodeSet.add(fn);
+  }
+
+  public boolean isSameHeightWrite(FlatNode fn) {
+    return this.sameHeightWriteFlatNodeSet.contains(fn);
+  }
+
 }

diff --git a/Robust/src/IR/Flat/BuildFlat.java b/Robust/src/IR/Flat/BuildFlat.java
index 8eb9ce6a8132d484af47e35a7959352f7f706ab9..bc6c613fbb23061fb9fb5a1ff35af84d7d4d986b 100644 (file)
--- a/Robust/src/IR/Flat/BuildFlat.java
+++ b/Robust/src/IR/Flat/BuildFlat.java
@@ -688,6 +688,7 @@ public class BuildFlat {
 
       FlatSetFieldNode fsfn=new FlatSetFieldNode(dst_tmp, fan.getField(), src_tmp);
       fsfn.setNumLine(en.getNumLine());
+      addMapNode2FlatNodeSet(an,fsfn);
       last.addNext(fsfn);
       last=fsfn;
       if (pre) {
@@ -783,6 +784,7 @@ public class BuildFlat {
         last.addNext(fon2);
         last=fon2;
       }
+      addMapNode2FlatNodeSet(an,last);
       return new NodePair(first, last);
     } else if (an.getDest().kind()==Kind.NameNode) {
       //We could be assigning a field or variable
@@ -849,6 +851,7 @@ public class BuildFlat {
 
         FlatSetFieldNode fsfn=new FlatSetFieldNode(dst_tmp, fan.getField(), src_tmp);
         fsfn.setNumLine(en.getNumLine());
+        addMapNode2FlatNodeSet(an,fsfn);
         last.addNext(fsfn);
         last=fsfn;
         if (pre) {
@@ -921,6 +924,7 @@ public class BuildFlat {
             fsfn=new FlatSetFieldNode(getTempforVar(nn.getVar()), nn.getField(), src_tmp);
             fsfn.setNumLine(nn.getNumLine());
           }
+          addMapNode2FlatNodeSet(an,fsfn);
           if (first==null) {
             first=fsfn;
           } else {
@@ -987,6 +991,7 @@ public class BuildFlat {
 
           FlatOpNode fon=new FlatOpNode(getTempforVar(nn.getVar()), src_tmp, null, new Operation(Operation.ASSIGN));
           fon.setNumLine(an.getNumLine());
+          addMapNode2FlatNodeSet(an,fon);
 
           last.addNext(fon);
           last=fon;