fix.

[IRC.git] / Robust / src / Analysis / SSJava / FlowDownCheck.java

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 8ff79e398032c8652695b791848a87c93fc22e2b..86766e40154db8e3b2f6f76676a651c7765044c2 100644 (file)
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -6,6 +6,7 @@ import java.util.Comparator;
 import java.util.HashSet;
 import java.util.Hashtable;
 import java.util.Iterator;
+import java.util.LinkedList;
 import java.util.List;
 import java.util.Set;
 import java.util.StringTokenizer;
@@ -25,6 +26,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;
@@ -305,23 +307,26 @@ public class FlowDownCheck {
     }
     Vector<AnnotationDescriptor> methodAnnotations = md.getModifiers().getAnnotations();
 
-    // second, check return location annotation
-    if (!md.getReturnType().isVoid()) {
-      CompositeLocation returnLocComp = null;
-
-      boolean hasReturnLocDeclaration = false;
-      if (methodAnnotations != null) {
-        for (int i = 0; i < methodAnnotations.size(); i++) {
-          AnnotationDescriptor an = methodAnnotations.elementAt(i);
-          if (an.getMarker().equals(ssjava.RETURNLOC)) {
-            // this case, developer explicitly defines method lattice
-            String returnLocDeclaration = an.getValue();
-            returnLocComp = parseLocationDeclaration(md, null, returnLocDeclaration);
-            hasReturnLocDeclaration = true;
-          }
+    CompositeLocation returnLocComp = null;
+
+    boolean hasReturnLocDeclaration = false;
+    if (methodAnnotations != null) {
+      for (int i = 0; i < methodAnnotations.size(); i++) {
+        AnnotationDescriptor an = methodAnnotations.elementAt(i);
+        if (an.getMarker().equals(ssjava.RETURNLOC)) {
+          // this case, developer explicitly defines method lattice
+          String returnLocDeclaration = an.getValue();
+          returnLocComp = parseLocationDeclaration(md, null, returnLocDeclaration);
+          hasReturnLocDeclaration = true;
+        } else if (an.getMarker().equals(ssjava.THISLOC)) {
+          String thisLoc = an.getValue();
+          ssjava.getMethodLattice(md).setThisLoc(thisLoc);
         }
       }
+    }
 
+    // second, check return location annotation
+    if (!md.getReturnType().isVoid()) {
       if (!hasReturnLocDeclaration) {
         // if developer does not define method lattice
         // search return location in the method default lattice
@@ -338,19 +343,17 @@ public class FlowDownCheck {
 
       md2ReturnLoc.put(md, returnLocComp);
 
-      // check this location
+    }
+
+    if (!md.getReturnType().isVoid()) {
       MethodLattice<String> methodLattice = ssjava.getMethodLattice(md);
       String thisLocId = methodLattice.getThisLoc();
-      if (thisLocId == null) {
+      if ((!md.isStatic()) && thisLocId == null) {
         throw new Error("Method '" + md + "' does not have the definition of 'this' location at "
             + md.getClassDesc().getSourceFileName());
       }
       CompositeLocation thisLoc = new CompositeLocation(new Location(md, thisLocId));
       paramList.add(0, thisLoc);
-
-      // System.out.println("### ReturnLocGenerator=" + md);
-      // System.out.println("### md2ReturnLoc.get(md)=" + md2ReturnLoc.get(md));
-
       md2ReturnLocGen.put(md, new ReturnLocGenerator(md2ReturnLoc.get(md), md, paramList, md
           + " of " + cd.getSourceFileName()));
     }
@@ -605,7 +608,13 @@ public class FlowDownCheck {
       // check 'for loop' case
       BlockNode bn = ln.getInitializer();
       bn.getVarTable().setParent(nametable);
-
+      // need to check initialization node
+//      checkLocationFromBlockNode(md, bn.getVarTable(), bn, constraint);
+      for(int i=0; i<bn.size(); i++) {
+        BlockStatementNode bsn=bn.get(i);
+        checkLocationFromBlockStatementNode(md, bn.getVarTable(),bsn, constraint);
+      }
+      
       // calculate glb location of condition and update statements
       CompositeLocation condLoc =
           checkLocationFromExpressionNode(md, bn.getVarTable(), ln.getCondition(),
@@ -681,7 +690,7 @@ public class FlowDownCheck {
         }
         if (!isOwned) {
           throw new Error(
-              "It is now allowed to create the reference alias from the reference not owned by the method at "
+              "It is not allowed to create the reference alias from the reference not owned by the method at "
                   + generateErrorMessage(md.getClassDesc(), tn));
         }
 
@@ -728,11 +737,12 @@ public class FlowDownCheck {
 
   private void checkDeclarationInSubBlockNode(MethodDescriptor md, SymbolTable nametable,
       SubBlockNode sbn) {
-    checkDeclarationInBlockNode(md, nametable.getParent(), sbn.getBlockNode());
+    checkDeclarationInBlockNode(md, nametable, sbn.getBlockNode());
   }
 
   private CompositeLocation checkLocationFromBlockExpressionNode(MethodDescriptor md,
       SymbolTable nametable, BlockExpressionNode ben, CompositeLocation constraint) {
+
     CompositeLocation compLoc =
         checkLocationFromExpressionNode(md, nametable, ben.getExpression(), null, constraint, false);
     // addTypeLocation(ben.getExpression().getType(), compLoc);
@@ -1527,10 +1537,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 +1554,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 +1596,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;