changes: 1) refactoring codes 2) forgot to implement ownsership checking in the flow...
authoryeom <yeom>
Thu, 1 Sep 2011 23:07:45 +0000 (23:07 +0000)
committeryeom <yeom>
Thu, 1 Sep 2011 23:07:45 +0000 (23:07 +0000)
Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
Robust/src/Analysis/SSJava/FlowDownCheck.java
Robust/src/Analysis/SSJava/LinearTypeCheck.java
Robust/src/Analysis/SSJava/SSJavaAnalysis.java
Robust/src/Analysis/SSJava/SSJavaType.java

index dfc6fc295705631114dcfc6414851a6747a708a7..6cf343e48ab21384776b3ffd59143ff9433506b5 100644 (file)
@@ -1,5 +1,8 @@
 package Analysis.SSJava;
 
+import java.io.BufferedWriter;
+import java.io.FileWriter;
+import java.io.IOException;
 import java.util.HashSet;
 import java.util.Hashtable;
 import java.util.Iterator;
@@ -9,6 +12,7 @@ import java.util.Stack;
 
 import Analysis.CallGraph.CallGraph;
 import Analysis.Loops.LoopFinder;
+import IR.ClassDescriptor;
 import IR.Descriptor;
 import IR.FieldDescriptor;
 import IR.MethodDescriptor;
@@ -203,14 +207,36 @@ public class DefinitelyWrittenCheck {
 
   }
 
+  private void writeReadMapFile() {
+
+    String fileName = "SharedLocationReadMap";
+
+    try {
+      BufferedWriter bw = new BufferedWriter(new FileWriter(fileName + ".txt"));
+
+      Set<MethodDescriptor> keySet = mapMethodDescriptorToReadSummary.keySet();
+      for (Iterator iterator = keySet.iterator(); iterator.hasNext();) {
+        MethodDescriptor mdKey = (MethodDescriptor) iterator.next();
+        ReadSummary summary = mapMethodDescriptorToReadSummary.get(mdKey);
+        bw.write("Method " + mdKey + "::\n");
+        bw.write(summary + "\n\n");
+      }
+      bw.close();
+    } catch (IOException e) {
+      e.printStackTrace();
+    }
+
+  }
+
   private void sharedLocationAnalysis() {
     // verify that all concrete locations of shared location are cleared out at
     // the same time once per the out-most loop
 
     computeReadSharedDescriptorSet();
 
-    System.out.println("###");
-    System.out.println("READ MAP=" + mapMethodDescriptorToReadSummary);
+    if (state.SSJAVADEBUG) {
+      writeReadMapFile();
+    }
 
     // methodDescriptorsToVisitStack.clear();
     // methodDescriptorsToVisitStack.add(sortedDescriptors.peekFirst());
@@ -275,8 +301,7 @@ public class DefinitelyWrittenCheck {
       boolean onlyVisitSSJavaLoop) {
 
     if (state.SSJAVADEBUG) {
-      System.out.println("Definite clearance for shared locations Analyzing: " + md + " "
-          + onlyVisitSSJavaLoop);
+      System.out.println("SSJAVA: Definite clearance for shared locations Analyzing: " + md);
     }
 
     FlatMethod fm = state.getMethodFlat(md);
@@ -1179,9 +1204,9 @@ public class DefinitelyWrittenCheck {
 
       TypeExtension te = td.getType().getExtension();
       if (te != null) {
-        if (te instanceof CompositeLocation) {
-          CompositeLocation comp = (CompositeLocation) te;
-
+        if (te instanceof SSJavaType) {
+          SSJavaType ssType = (SSJavaType) te;
+          CompositeLocation comp = ssType.getCompLoc();
           return comp.get(comp.getSize() - 1);
         } else {
           return (Location) te;
@@ -1753,7 +1778,7 @@ public class DefinitelyWrittenCheck {
   private void methodReadOverWrite_analyzeMethod(FlatMethod fm, Set<NTuple<Descriptor>> readSet,
       Set<NTuple<Descriptor>> overWriteSet, Set<NTuple<Descriptor>> writeSet) {
     if (state.SSJAVADEBUG) {
-      System.out.println("Definitely written Analyzing: " + fm);
+      System.out.println("SSJAVA: Definitely written Analyzing: " + fm);
     }
 
     // intraprocedural analysis
index a1397dae02aa1ccaff911dff574af5c1f5318eaf..ab026926d52d0a30363bba1c6ebaf53d8826d147 100644 (file)
@@ -23,6 +23,7 @@ import IR.Operation;
 import IR.State;
 import IR.SymbolTable;
 import IR.TypeDescriptor;
+import IR.TypeExtension;
 import IR.VarDescriptor;
 import IR.Tree.ArrayAccessNode;
 import IR.Tree.AssignmentNode;
@@ -221,7 +222,9 @@ public class FlowDownCheck {
       while (!toAnalyzeMethodIsEmpty()) {
         MethodDescriptor md = toAnalyzeMethodNext();
         if (ssjava.needTobeAnnotated(md)) {
-          System.out.println("SSJAVA: Checking assignments: " + md);
+          if (state.SSJAVADEBUG) {
+            System.out.println("SSJAVA: Checking Flow-down Rules: " + md);
+          }
           checkMethodBody(cd, md, null);
         }
       }
@@ -292,7 +295,6 @@ public class FlowDownCheck {
   private void checkDeclarationInMethodBody(ClassDescriptor cd, MethodDescriptor md) {
     BlockNode bn = state.getMethodBody(md);
 
-
     // first, check annotations on method parameters
     List<CompositeLocation> paramList = new ArrayList<CompositeLocation>();
     for (int i = 0; i < md.numParameters(); i++) {
@@ -346,8 +348,8 @@ public class FlowDownCheck {
       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));
+      // 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()));
@@ -657,6 +659,32 @@ public class FlowDownCheck {
     return new CompositeLocation();
   }
 
+  private void checkOwnership(MethodDescriptor md, TreeNode tn, ExpressionNode srcExpNode) {
+
+    if (srcExpNode.kind() == Kind.NameNode || srcExpNode.kind() == Kind.FieldAccessNode) {
+      if (srcExpNode.getType().isPtr() && !srcExpNode.getType().isNull()) {
+        // first, check the linear type
+        // RHS reference should be owned by the current method
+        FieldDescriptor fd = getFieldDescriptorFromExpressionNode(srcExpNode);
+        boolean isOwned;
+        if (fd == null) {
+          // local var case
+          isOwned = ((SSJavaType) srcExpNode.getType().getExtension()).isOwned();
+        } else {
+          // field case
+          isOwned = ssjava.isOwnedByMethod(md, fd);
+        }
+        if (!isOwned) {
+          throw new Error(
+              "It is now allowed to create the reference alias from the reference not owned by the method at "
+                  + generateErrorMessage(md.getClassDesc(), tn));
+        }
+
+      }
+    }
+
+  }
+
   private CompositeLocation checkLocationFromDeclarationNode(MethodDescriptor md,
       SymbolTable nametable, DeclarationNode dn, CompositeLocation constraint) {
 
@@ -665,12 +693,16 @@ public class FlowDownCheck {
     CompositeLocation destLoc = d2loc.get(vd);
 
     if (dn.getExpression() != null) {
+
+      checkOwnership(md, dn, dn.getExpression());
+
       CompositeLocation expressionLoc =
           checkLocationFromExpressionNode(md, nametable, dn.getExpression(),
               new CompositeLocation(), constraint, false);
       // addTypeLocation(dn.getExpression().getType(), expressionLoc);
 
       if (expressionLoc != null) {
+
         // checking location order
         if (!CompositeLattice.isGreaterThan(expressionLoc, destLoc,
             generateErrorMessage(md.getClassDesc(), dn))) {
@@ -874,8 +906,9 @@ public class FlowDownCheck {
 
       }
 
-//      System.out.println("\n#checkLocationFromMethodInvokeNode=" + min.printNode(0)
-//          + " baseLocation=" + baseLocation + " constraint=" + constraint);
+      // System.out.println("\n#checkLocationFromMethodInvokeNode=" +
+      // min.printNode(0)
+      // + " baseLocation=" + baseLocation + " constraint=" + constraint);
 
       if (constraint != null) {
         int compareResult =
@@ -889,8 +922,9 @@ public class FlowDownCheck {
           // no need to check constraints!
           CompositeLocation calleeConstraint =
               translateCallerLocToCalleeLoc(calleeMD, baseLocation, constraint);
-//          System.out.println("check method body for constraint:" + calleeMD + " calleeConstraint="
-//              + calleeConstraint);
+          // System.out.println("check method body for constraint:" + calleeMD +
+          // " calleeConstraint="
+          // + calleeConstraint);
           checkMethodBody(calleeMD.getClassDesc(), calleeMD, calleeConstraint);
         }
       }
@@ -964,8 +998,10 @@ public class FlowDownCheck {
 
     String errorMsg = generateErrorMessage(md.getClassDesc(), min);
 
-//    System.out.println("checkCallerArgumentLocationConstraints=" + min.printNode(0));
-//    System.out.println("base location=" + callerBaseLoc + " constraint=" + constraint);
+    // System.out.println("checkCallerArgumentLocationConstraints=" +
+    // min.printNode(0));
+    // System.out.println("base location=" + callerBaseLoc + " constraint=" +
+    // constraint);
 
     for (int i = 0; i < calleeParamList.size(); i++) {
       CompositeLocation calleeParamLoc = calleeParamList.get(i);
@@ -1010,7 +1046,8 @@ public class FlowDownCheck {
       translate.addLocation(calleeParamLoc.get(i));
     }
 
-//    System.out.println("TRANSLATED=" + translate + " from calleeParamLoc=" + calleeParamLoc);
+    // System.out.println("TRANSLATED=" + translate + " from calleeParamLoc=" +
+    // calleeParamLoc);
 
     return translate;
   }
@@ -1031,9 +1068,10 @@ public class FlowDownCheck {
       argList.add(callerArg);
     }
 
-//    System.out.println("\n## computeReturnLocation=" + min.getMethod() + " argList=" + argList);
+    // System.out.println("\n## computeReturnLocation=" + min.getMethod() +
+    // " argList=" + argList);
     CompositeLocation ceilLoc = md2ReturnLocGen.get(min.getMethod()).computeReturnLocation(argList);
-//    System.out.println("## ReturnLocation=" + ceilLoc);
+    // System.out.println("## ReturnLocation=" + ceilLoc);
 
     return ceilLoc;
 
@@ -1042,7 +1080,7 @@ public class FlowDownCheck {
   private void checkCalleeConstraints(MethodDescriptor md, SymbolTable nametable,
       MethodInvokeNode min, CompositeLocation callerBaseLoc, CompositeLocation constraint) {
 
-//    System.out.println("checkCalleeConstraints=" + min.printNode(0));
+    // System.out.println("checkCalleeConstraints=" + min.printNode(0));
 
     MethodDescriptor calleemd = min.getMethod();
 
@@ -1076,7 +1114,7 @@ public class FlowDownCheck {
       for (int i = 0; i < calleemd.numParameters(); i++) {
         VarDescriptor calleevd = (VarDescriptor) calleemd.getParameter(i);
         CompositeLocation calleeLoc = d2loc.get(calleevd);
-//        System.out.println("calleevd=" + calleevd + " loc=" + calleeLoc);
+        // System.out.println("calleevd=" + calleevd + " loc=" + calleeLoc);
         calleeParamList.add(calleeLoc);
       }
 
@@ -1096,8 +1134,9 @@ public class FlowDownCheck {
               continue CHECK;
             }
 
-//            System.out.println("calleeLoc1=" + calleeLoc1);
-//            System.out.println("calleeLoc2=" + calleeLoc2 + "calleeParamList=" + calleeParamList);
+            // System.out.println("calleeLoc1=" + calleeLoc1);
+            // System.out.println("calleeLoc2=" + calleeLoc2 +
+            // "calleeParamList=" + calleeParamList);
 
             int callerResult =
                 CompositeLattice.compare(callerLoc1, callerLoc2, true,
@@ -1196,11 +1235,13 @@ public class FlowDownCheck {
       // addTypeLocation(on.getRight().getType(), rightLoc);
     }
 
-//    System.out.println("\n# OP NODE=" + on.printNode(0));
-//    System.out.println("# left loc=" + leftLoc + " from " + on.getLeft().getClass());
-//    if (on.getRight() != null) {
-//      System.out.println("# right loc=" + rightLoc + " from " + on.getRight().getClass());
-//    }
+    // System.out.println("\n# OP NODE=" + on.printNode(0));
+    // System.out.println("# left loc=" + leftLoc + " from " +
+    // on.getLeft().getClass());
+    // if (on.getRight() != null) {
+    // System.out.println("# right loc=" + rightLoc + " from " +
+    // on.getRight().getClass());
+    // }
 
     Operation op = on.getOp();
 
@@ -1239,7 +1280,7 @@ public class FlowDownCheck {
       inputSet.add(rightLoc);
       CompositeLocation glbCompLoc =
           CompositeLattice.calculateGLB(inputSet, generateErrorMessage(cd, on));
-//      System.out.println("# glbCompLoc=" + glbCompLoc);
+      // System.out.println("# glbCompLoc=" + glbCompLoc);
       return glbCompLoc;
 
     default:
@@ -1289,7 +1330,7 @@ public class FlowDownCheck {
         VarDescriptor vd = (VarDescriptor) d;
         // localLoc = d2loc.get(vd);
         // the type of var descriptor has a composite location!
-        loc = ((CompositeLocation) vd.getType().getExtension()).clone();
+        loc = ((SSJavaType) vd.getType().getExtension()).getCompLoc().clone();
       } else if (d instanceof FieldDescriptor) {
         // the type of field descriptor has a location!
         FieldDescriptor fd = (FieldDescriptor) d;
@@ -1367,20 +1408,22 @@ public class FlowDownCheck {
     }
 
     loc = checkLocationFromExpressionNode(md, nametable, left, loc, constraint, false);
-//    System.out.println("### checkLocationFromFieldAccessNode=" + fan.printNode(0));
-//    System.out.println("### left=" + left.printNode(0));
+    // System.out.println("### checkLocationFromFieldAccessNode=" +
+    // fan.printNode(0));
+    // System.out.println("### left=" + left.printNode(0));
     if (!left.getType().isPrimitive()) {
       Location fieldLoc = getFieldLocation(fd);
       loc.addLocation(fieldLoc);
     }
-//    System.out.println("### field loc=" + loc);
+    // System.out.println("### field loc=" + loc);
     return loc;
   }
 
   private Location getFieldLocation(FieldDescriptor fd) {
 
-//    System.out.println("### getFieldLocation=" + fd);
-//    System.out.println("### fd.getType().getExtension()=" + fd.getType().getExtension());
+    // System.out.println("### getFieldLocation=" + fd);
+    // System.out.println("### fd.getType().getExtension()=" +
+    // fd.getType().getExtension());
 
     Location fieldLoc = (Location) fd.getType().getExtension();
 
@@ -1394,10 +1437,30 @@ public class FlowDownCheck {
 
   }
 
+  private FieldDescriptor getFieldDescriptorFromExpressionNode(ExpressionNode en) {
+
+    if (en.kind() == Kind.NameNode) {
+      NameNode nn = (NameNode) en;
+      if (nn.getField() != null) {
+        return nn.getField();
+      }
+
+      if (nn.getName() != null && nn.getName().getBase() != null) {
+        return getFieldDescriptorFromExpressionNode(nn.getExpression());
+      }
+
+    } else if (en.kind() == Kind.FieldAccessNode) {
+      FieldAccessNode fan = (FieldAccessNode) en;
+      return fan.getField();
+    }
+
+    return null;
+  }
+
   private CompositeLocation checkLocationFromAssignmentNode(MethodDescriptor md,
       SymbolTable nametable, AssignmentNode an, CompositeLocation loc, CompositeLocation constraint) {
 
-//    System.out.println("\n# ASSIGNMENTNODE=" + an.printNode(0));
+    // System.out.println("\n# ASSIGNMENTNODE=" + an.printNode(0));
 
     ClassDescriptor cd = md.getClassDesc();
 
@@ -1419,6 +1482,9 @@ public class FlowDownCheck {
     CompositeLocation srcLocation;
 
     if (!postinc) {
+
+      checkOwnership(md, an, an.getSrc());
+
       rhsLocation =
           checkLocationFromExpressionNode(md, nametable, an.getSrc(), new CompositeLocation(),
               constraint, false);
@@ -1433,10 +1499,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))) {
 
@@ -1464,9 +1530,9 @@ public class FlowDownCheck {
         srcLocation = rhsLocation;
       }
 
-//      System.out.println("srcLocation=" + srcLocation);
-//      System.out.println("rhsLocation=" + rhsLocation);
-//      System.out.println("constraint=" + constraint);
+      // System.out.println("srcLocation=" + srcLocation);
+      // System.out.println("rhsLocation=" + rhsLocation);
+      // System.out.println("constraint=" + constraint);
 
       if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, generateErrorMessage(cd, an))) {
 
@@ -1500,33 +1566,36 @@ public class FlowDownCheck {
           + generateErrorMessage(cd, n));
     }
 
-    if (annotationVec.size() > 1) { // variable can have at most one location
-      throw new Error(vd.getSymbol() + " has more than one location.");
-    }
+    int locDecCount = 0;
+    for (int i = 0; i < annotationVec.size(); i++) {
+      AnnotationDescriptor ad = annotationVec.elementAt(i);
 
-    AnnotationDescriptor ad = annotationVec.elementAt(0);
+      if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {
 
-    if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {
+        if (ad.getMarker().equals(SSJavaAnalysis.LOC)) {
+          locDecCount++;
+          if (locDecCount > 1) {// variable can have at most one location
+            throw new Error(vd.getSymbol() + " has more than one location declaration.");
+          }
+          String locDec = ad.getValue(); // check if location is defined
 
-      if (ad.getMarker().equals(SSJavaAnalysis.LOC)) {
-        String locDec = ad.getValue(); // check if location is defined
+          if (locDec.startsWith(SSJavaAnalysis.DELTA)) {
+            DeltaLocation deltaLoc = parseDeltaDeclaration(md, n, locDec);
+            d2loc.put(vd, deltaLoc);
+            addLocationType(vd.getType(), deltaLoc);
+          } else {
+            CompositeLocation compLoc = parseLocationDeclaration(md, n, locDec);
 
-        if (locDec.startsWith(SSJavaAnalysis.DELTA)) {
-          DeltaLocation deltaLoc = parseDeltaDeclaration(md, n, locDec);
-          d2loc.put(vd, deltaLoc);
-          addLocationType(vd.getType(), deltaLoc);
-        } else {
-          CompositeLocation compLoc = parseLocationDeclaration(md, n, locDec);
+            Location lastElement = compLoc.get(compLoc.getSize() - 1);
+            if (ssjava.isSharedLocation(lastElement)) {
+              ssjava.mapSharedLocation2Descriptor(lastElement, vd);
+            }
 
-          Location lastElement = compLoc.get(compLoc.getSize() - 1);
-          if (ssjava.isSharedLocation(lastElement)) {
-            ssjava.mapSharedLocation2Descriptor(lastElement, vd);
+            d2loc.put(vd, compLoc);
+            addLocationType(vd.getType(), compLoc);
           }
 
-          d2loc.put(vd, compLoc);
-          addLocationType(vd.getType(), compLoc);
         }
-
       }
     }
 
@@ -1562,7 +1631,8 @@ public class FlowDownCheck {
     Descriptor d = state.getClassSymbolTable().get(className);
 
     if (d == null) {
-//      System.out.println("state.getClassSymbolTable()=" + state.getClassSymbolTable());
+      // System.out.println("state.getClassSymbolTable()=" +
+      // state.getClassSymbolTable());
       throw new Error("The class in the location declaration '" + decl + "' does not exist at "
           + msg);
     }
@@ -1685,7 +1755,15 @@ public class FlowDownCheck {
 
   private void addLocationType(TypeDescriptor type, CompositeLocation loc) {
     if (type != null) {
-      type.setExtension(loc);
+      TypeExtension te = type.getExtension();
+      SSJavaType ssType;
+      if (te != null) {
+        ssType = (SSJavaType) te;
+        ssType.setCompLoc(loc);
+      } else {
+        ssType = new SSJavaType(loc);
+        type.setExtension(ssType);
+      }
     }
   }
 
@@ -1699,7 +1777,8 @@ public class FlowDownCheck {
 
     public static boolean isGreaterThan(CompositeLocation loc1, CompositeLocation loc2, String msg) {
 
-//      System.out.println("\nisGreaterThan=" + loc1 + " " + loc2 + " msg=" + msg);
+      // System.out.println("\nisGreaterThan=" + loc1 + " " + loc2 + " msg=" +
+      // msg);
       int baseCompareResult = compareBaseLocationSet(loc1, loc2, true, false, msg);
       if (baseCompareResult == ComparisonResult.EQUAL) {
         if (compareDelta(loc1, loc2) == ComparisonResult.GREATER) {
@@ -1718,7 +1797,7 @@ public class FlowDownCheck {
     public static int compare(CompositeLocation loc1, CompositeLocation loc2, boolean ignore,
         String msg) {
 
-//      System.out.println("compare=" + loc1 + " " + loc2);
+      // System.out.println("compare=" + loc1 + " " + loc2);
       int baseCompareResult = compareBaseLocationSet(loc1, loc2, false, ignore, msg);
 
       if (baseCompareResult == ComparisonResult.EQUAL) {
@@ -1835,7 +1914,7 @@ public class FlowDownCheck {
 
     public static CompositeLocation calculateGLB(Set<CompositeLocation> inputSet, String errMsg) {
 
-//      System.out.println("Calculating GLB=" + inputSet);
+      // System.out.println("Calculating GLB=" + inputSet);
       CompositeLocation glbCompLoc = new CompositeLocation();
 
       // calculate GLB of the first(priority) element
@@ -1967,7 +2046,7 @@ public class FlowDownCheck {
         }
       }
 
-//      System.out.println("GLB=" + glbCompLoc);
+      // System.out.println("GLB=" + glbCompLoc);
       return glbCompLoc;
 
     }
index aa500018e83fb30032c93370d3e1afadf963880d..3401093a3ff910dbbf025d38a6e4f5de325bb497 100644 (file)
@@ -13,6 +13,7 @@ import java.util.Vector;
 import Analysis.Liveness;
 import IR.AnnotationDescriptor;
 import IR.ClassDescriptor;
+import IR.FieldDescriptor;
 import IR.MethodDescriptor;
 import IR.Operation;
 import IR.State;
@@ -55,7 +56,7 @@ public class LinearTypeCheck {
   State state;
   SSJavaAnalysis ssjava;
   String needToNullify = null;
-  ExpressionNode prevAssignNode;
+  TreeNode prevAssignNode;
 
   Set<TreeNode> linearTypeCheckSet;
 
@@ -201,6 +202,9 @@ public class LinearTypeCheck {
   }
 
   private void checkMethodBody(ClassDescriptor cd, MethodDescriptor md) {
+    if (state.SSJAVADEBUG) {
+      System.out.println("SSJAVA: Linear Type Checking: " + md);
+    }
     BlockNode bn = state.getMethodBody(md);
     checkBlockNode(md, md.getParameterTable(), bn);
   }
@@ -452,6 +456,9 @@ public class LinearTypeCheck {
                 + "::" + min.getNumLine());
           }
 
+          // delegated arg is no longer to be available from here
+          linearTypeCheckSet.add(argNode);
+          mapTreeNode2FlatMethod.put(argNode, state.getMethodFlat(md));
         }
 
       }
@@ -549,93 +556,92 @@ public class LinearTypeCheck {
       postinc = false;
 
     if (!postinc) {
-
       checkExpressionNode(md, nametable, an.getSrc());
-
       if (isReference(an.getSrc().getType()) && isReference(an.getDest().getType())) {
+        checkAlias(md, an, an.getSrc());
+      }
 
-        if (an.getSrc().kind() == Kind.NameNode) {
-
-          NameNode nn = (NameNode) an.getSrc();
+    }
 
-          if (nn.getField() != null) {
-            needToNullify = nn.getField().getSymbol();
-            prevAssignNode = an;
-          } else if (nn.getExpression() != null) {
-            if (nn.getExpression() instanceof FieldAccessNode) {
-              FieldAccessNode fan = (FieldAccessNode) nn.getExpression();
-              needToNullify = fan.printNode(0);
-              prevAssignNode = an;
+  }
 
-            }
+  private boolean isFieldOfClass(ClassDescriptor classDesc, String varName) {
+    return classDesc.getFieldTable().contains(varName);
+  }
 
-          } else {
-            // local variable case
-            linearTypeCheckSet.add(an.getSrc());
-            mapTreeNode2FlatMethod.put(an.getSrc(), state.getMethodFlat(md));
-          }
-        } else if (an.getSrc().kind() == Kind.FieldAccessNode) {
-          FieldAccessNode fan = (FieldAccessNode) an.getSrc();
-          needToNullify = fan.printNode(0);
-          if (needToNullify.startsWith("this.")) {
-            needToNullify = needToNullify.substring(5);
-          }
-          prevAssignNode = an;
-        } else if (an.getSrc().kind() == Kind.ArrayAccessNode) {
-          TypeDescriptor srcType = an.getSrc().getType();
-          if (srcType.isPtr() && !srcType.isString()) {
-            throw new Error(
-                "Not allowed to create an alias to the middle of the multidimensional array at "
-                    + md.getClassDesc().getSourceFileName() + "::" + an.getNumLine());
-          }
-        } else if (an.getSrc().kind() == Kind.CreateObjectNode
-            || an.getSrc().kind() == Kind.MethodInvokeNode
-            || an.getSrc().kind() == Kind.ArrayInitializerNode
-            || an.getSrc().kind() == Kind.LiteralNode) {
+  private boolean isCreatingAlias(ExpressionNode en) {
 
-        } else {
-          throw new Error("Not allowed this type of assignment at "
-              + md.getClassDesc().getSourceFileName() + "::" + an.getNumLine());
-        }
+    int kind = en.kind();
+    if (kind == Kind.NameNode || kind == Kind.ArrayAccessNode || kind == Kind.FieldAccessNode) {
+      return true;
+    }
+    return false;
 
-        if (isCreatingAlias(an.getSrc())) {
+  }
 
-          TypeDescriptor srcType = getTypeDescriptor(an.getSrc());
-          boolean isSourceOwned = false;
+  private TypeDescriptor getTypeDescriptor(ExpressionNode en) {
+    if (en.kind() == Kind.NameNode) {
+      NameNode nn = (NameNode) en;
+      if (nn.getField() != null) {
+        return nn.getVar().getType();
+      } else if (nn.getVar() != null) {
+        return nn.getVar().getType();
+      } else {
+        return getTypeDescriptor(nn.getExpression());
+      }
+    } else if (en.kind() == Kind.FieldAccessNode) {
+      FieldAccessNode fan = (FieldAccessNode) en;
+      return getTypeDescriptor(fan.getExpression());
+    } else if (en.kind() == Kind.CreateObjectNode) {
+      CreateObjectNode con = (CreateObjectNode) en;
+      return con.getType();
+    } else if (en.kind() == Kind.ArrayAccessNode) {
+      ArrayAccessNode aan = (ArrayAccessNode) en;
+      return aan.getExpression().getType();
+    }
 
-          if (srcType.getExtension() != null) {
-            SSJavaType srcLocationType = (SSJavaType) srcType.getExtension();
-            isSourceOwned = srcLocationType.isOwned();
-          } else if (md.isConstructor()
-              && isFieldOfClass(md.getClassDesc(), an.getSrc().printNode(0))) {
-            isSourceOwned = true;
-          }
+    return null;
+  }
 
-          if (!isField(an.getDest())) {
-            if (isSourceOwned) {
-              // here, transfer ownership from LHS to RHS when it creates alias
-              TypeDescriptor destType = getTypeDescriptor(an.getDest());
-              destType.setExtension(new SSJavaType(isSourceOwned));
-            }
-          } else {
-            // if instance is not owned by the method, not able to store
-            // instance into field
-            if (!isSourceOwned) {
-              throw new Error(
-                  "Method is not allowed to store an instance not owned by itself into a field at "
-                      + md.getClassDesc().getSourceFileName() + "::" + an.getNumLine());
-            }
-          }
+  private FieldDescriptor getFieldDescriptorFromExpressionNode(ExpressionNode en) {
 
-        }
+    if (en.kind() == Kind.NameNode) {
+      NameNode nn = (NameNode) en;
+      if (nn.getField() != null) {
+        return nn.getField();
+      }
 
+      if (nn.getName() != null && nn.getName().getBase() != null) {
+        return getFieldDescriptorFromExpressionNode(nn.getExpression());
       }
 
+    } else if (en.kind() == Kind.FieldAccessNode) {
+      FieldAccessNode fan = (FieldAccessNode) en;
+      return fan.getField();
     }
 
+    return null;
+  }
+
+  private boolean isField(ExpressionNode en) {
+
+    if (en.kind() == Kind.NameNode) {
+      NameNode nn = (NameNode) en;
+      if (nn.getField() != null) {
+        return true;
+      }
+
+      if (nn.getName() != null && nn.getName().getBase() != null) {
+        return true;
+      }
+
+    } else if (en.kind() == Kind.FieldAccessNode) {
+      return true;
+    }
+    return false;
   }
 
-  private void checkSource(MethodDescriptor md, ExpressionNode src, ExpressionNode dst) {
+  private void checkAlias(MethodDescriptor md, TreeNode node, ExpressionNode src) {
 
     if (src.kind() == Kind.NameNode) {
 
@@ -643,15 +649,13 @@ public class LinearTypeCheck {
 
       if (nn.getField() != null) {
         needToNullify = nn.getField().getSymbol();
-        prevAssignNode = src;
+        prevAssignNode = node;
       } else if (nn.getExpression() != null) {
         if (nn.getExpression() instanceof FieldAccessNode) {
           FieldAccessNode fan = (FieldAccessNode) nn.getExpression();
           needToNullify = fan.printNode(0);
-          prevAssignNode = src;
-
+          prevAssignNode = node;
         }
-
       } else {
         // local variable case
         linearTypeCheckSet.add(src);
@@ -663,20 +667,23 @@ public class LinearTypeCheck {
       if (needToNullify.startsWith("this.")) {
         needToNullify = needToNullify.substring(5);
       }
-      prevAssignNode = src;
+      prevAssignNode = node;
     } else if (src.kind() == Kind.ArrayAccessNode) {
       TypeDescriptor srcType = src.getType();
       if (srcType.isPtr() && !srcType.isString()) {
         throw new Error(
             "Not allowed to create an alias to the middle of the multidimensional array at "
-                + md.getClassDesc().getSourceFileName() + "::" + src.getNumLine());
+                + md.getClassDesc().getSourceFileName() + "::" + node.getNumLine());
       }
     } else if (src.kind() == Kind.CreateObjectNode || src.kind() == Kind.MethodInvokeNode
         || src.kind() == Kind.ArrayInitializerNode || src.kind() == Kind.LiteralNode) {
-
+      if (node.kind() == Kind.DeclarationNode) {
+        DeclarationNode dn = (DeclarationNode) node;
+        dn.getVarDescriptor().getType().setExtension(new SSJavaType(true));
+      }
     } else {
       throw new Error("Not allowed this type of assignment at "
-          + md.getClassDesc().getSourceFileName() + "::" + src.getNumLine());
+          + md.getClassDesc().getSourceFileName() + "::" + node.getNumLine());
     }
 
     if (isCreatingAlias(src)) {
@@ -687,99 +694,48 @@ public class LinearTypeCheck {
       if (srcType.getExtension() != null) {
         SSJavaType srcLocationType = (SSJavaType) srcType.getExtension();
         isSourceOwned = srcLocationType.isOwned();
-      } else if (md.isConstructor() && isFieldOfClass(md.getClassDesc(), src.printNode(0))) {
-        isSourceOwned = true;
-      }
 
-      if (!isField(dst)) {
         if (isSourceOwned) {
-          // here, transfer ownership from LHS to RHS when it creates alias
-          TypeDescriptor destType = getTypeDescriptor(dst);
-          destType.setExtension(new SSJavaType(isSourceOwned));
-        }
-      } else {
-        // if instance is not owned by the method, not able to store
-        // instance into field
-        if (!isSourceOwned) {
-          throw new Error(
-              "Method is not allowed to store an instance not owned by itself into a field at "
-                  + md.getClassDesc().getSourceFileName() + "::" + src.getNumLine());
+          if (isField(src)) {
+            ssjava.setFieldOnwership(md, getFieldDescriptorFromExpressionNode(src));
+          }
         }
-      }
-
-    }
-
-  }
-
-  private boolean isFieldOfClass(ClassDescriptor classDesc, String varName) {
-    return classDesc.getFieldTable().contains(varName);
-  }
-
-  private boolean isCreatingAlias(ExpressionNode en) {
-
-    int kind = en.kind();
-    if (kind == Kind.NameNode || kind == Kind.ArrayAccessNode || kind == Kind.FieldAccessNode) {
-      return true;
-    }
-    return false;
-
-  }
-
-  private TypeDescriptor getTypeDescriptor(ExpressionNode en) {
-    if (en.kind() == Kind.NameNode) {
-      NameNode nn = (NameNode) en;
-      if (nn.getField() != null) {
-        return nn.getVar().getType();
-      } else if (nn.getVar() != null) {
-        return nn.getVar().getType();
-      } else {
-        return getTypeDescriptor(nn.getExpression());
-      }
-    } else if (en.kind() == Kind.FieldAccessNode) {
-      FieldAccessNode fan = (FieldAccessNode) en;
-      return getTypeDescriptor(fan.getExpression());
-    } else if (en.kind() == Kind.CreateObjectNode) {
-      CreateObjectNode con = (CreateObjectNode) en;
-      return con.getType();
-    } else if (en.kind() == Kind.ArrayAccessNode) {
-      ArrayAccessNode aan = (ArrayAccessNode) en;
-      return aan.getExpression().getType();
-    }
-
-    return null;
-  }
 
-  private boolean isField(ExpressionNode en) {
-
-    if (en.kind() == Kind.NameNode) {
-      NameNode nn = (NameNode) en;
-      if (nn.getField() != null) {
-        return true;
+      } else if (md.isConstructor() && isFieldOfClass(md.getClassDesc(), src.printNode(0))) {
+        isSourceOwned = true;
+        ssjava.setFieldOnwership(md, getFieldDescriptorFromExpressionNode(src));
       }
 
-      if (nn.getName() != null && nn.getName().getBase() != null) {
-        return true;
+      if (node.kind() == Kind.AssignmentNode) {
+        AssignmentNode an = (AssignmentNode) node;
+        if (isField(an.getDest())) {
+          // if instance is not owned by the method, not able to store
+          // instance into field
+          if (!isSourceOwned) {
+            throw new Error(
+                "Method is not allowed to store an instance not owned by itself into a field at "
+                    + md.getClassDesc().getSourceFileName() + "::" + node.getNumLine());
+          }
+        } else {
+          if (isSourceOwned) {
+            // here, transfer ownership from LHS to RHS when it creates alias
+            TypeDescriptor destType = getTypeDescriptor(an.getDest());
+            destType.setExtension(new SSJavaType(isSourceOwned));
+          }
+        }
       }
 
-    } else if (en.kind() == Kind.FieldAccessNode) {
-      return true;
     }
-    return false;
+
   }
 
   private void checkDeclarationNode(MethodDescriptor md, SymbolTable nametable, DeclarationNode dn) {
     if (dn.getExpression() != null) {
-      checkExpressionNode(md, nametable, dn.getExpression());
-      if (dn.getExpression().kind() == Kind.CreateObjectNode) {
-        dn.getVarDescriptor().getType().setExtension(new SSJavaType(true));
-      } else if (dn.getExpression().kind() == Kind.ArrayAccessNode
-          && dn.getExpression().getType().isPtr()) {
-        throw new Error(
-            "Not allowed to create an alias to the middle of the multidimensional array at "
-                + md.getClassDesc().getSourceFileName() + "::" + dn.getNumLine());
+      ExpressionNode src = dn.getExpression();
+      if (isReference(src.getType())) {
+        checkAlias(md, dn, src);
       }
     }
-
   }
 
   private boolean isReference(TypeDescriptor td) {
index e2b63da2729a96fbfe65dfdc6d70b8314e609f6c..67b50e543aaac82b114999f7b360cb75cbc6af46 100644 (file)
@@ -21,6 +21,7 @@ import Analysis.Loops.LoopTerminate;
 import IR.AnnotationDescriptor;
 import IR.ClassDescriptor;
 import IR.Descriptor;
+import IR.FieldDescriptor;
 import IR.MethodDescriptor;
 import IR.State;
 import IR.SymbolTable;
@@ -80,6 +81,9 @@ public class SSJavaAnalysis {
   // points to method containing SSJAVA Loop
   private MethodDescriptor methodContainingSSJavaLoop;
 
+  // keep the field ownership from the linear type checking
+  Hashtable<MethodDescriptor, Set<FieldDescriptor>> mapMethodToOwnedFieldSet;
+
   CallGraph callgraph;
 
   LinearTypeCheck checker;
@@ -98,6 +102,7 @@ public class SSJavaAnalysis {
     this.linearTypeCheckMethodSet = new HashSet<MethodDescriptor>();
     this.bf = bf;
     this.trustWorthyMDSet = new HashSet<MethodDescriptor>();
+    this.mapMethodToOwnedFieldSet = new Hashtable<MethodDescriptor, Set<FieldDescriptor>>();
   }
 
   public void doCheck() {
@@ -110,7 +115,7 @@ public class SSJavaAnalysis {
     parseLocationAnnotation();
     doFlowDownCheck();
     doDefinitelyWrittenCheck();
-    // debugDoLoopCheck();
+    debugDoLoopCheck();
   }
 
   private void debugDoLoopCheck() {
@@ -513,4 +518,23 @@ public class SSJavaAnalysis {
     }
     return false;
   }
+
+  public void setFieldOnwership(MethodDescriptor md, FieldDescriptor field) {
+
+    Set<FieldDescriptor> fieldSet = mapMethodToOwnedFieldSet.get(md);
+    if (fieldSet == null) {
+      fieldSet = new HashSet<FieldDescriptor>();
+      mapMethodToOwnedFieldSet.put(md, fieldSet);
+    }
+    fieldSet.add(field);
+  }
+
+  public boolean isOwnedByMethod(MethodDescriptor md, FieldDescriptor field) {
+    Set<FieldDescriptor> fieldSet = mapMethodToOwnedFieldSet.get(md);
+    if (fieldSet != null) {
+      return fieldSet.contains(field);
+    }
+    return false;
+  }
+
 }
index 750b0347e1128aa02005620f2a3d39884edb64d3..07dff574e62b2be14a795864b8b4fad6ae02e485 100644 (file)
@@ -7,6 +7,11 @@ public class SSJavaType implements TypeExtension {
   private boolean isOwned;
   private CompositeLocation compLoc;
 
+  public SSJavaType(CompositeLocation compLoc) {
+    this.isOwned = false;
+    this.compLoc = compLoc;
+  }
+
   public SSJavaType(boolean isOwned) {
     this.isOwned = isOwned;
   }