changes.

diff --git a/Robust/src/Analysis/SSJava/DeltaLocation.java b/Robust/src/Analysis/SSJava/DeltaLocation.java
index 2f28df781482fac11c7f3a410d28af9487221248..13f1a6cba8bd8ba83c360e104f29cdd8aedd9496 100644 (file)
--- a/Robust/src/Analysis/SSJava/DeltaLocation.java
+++ b/Robust/src/Analysis/SSJava/DeltaLocation.java
@@ -1,90 +1,37 @@
 package Analysis.SSJava;
 
-import IR.ClassDescriptor;
-import IR.Descriptor;
-
 public class DeltaLocation extends CompositeLocation {
 
-  private Descriptor refOperand = null;
   private int numDelta;
 
-  public DeltaLocation() {
-  }
-
-  // public DeltaLocation(Set<Location> set) {
-  // locTuple.addAll(set);
-  // }
-
-  public DeltaLocation(ClassDescriptor cd, Descriptor refOperand) {
-    this.refOperand = refOperand;
-  }
-
-  public Descriptor getRefLocationId() {
-    return this.refOperand;
-  }
-
-  public void addDeltaOperand(Location op) {
-    locTuple.addElement(op);
+  public DeltaLocation(CompositeLocation comp, int numDelta) {
+    this.numDelta = numDelta;
+    this.locTuple = comp.getTuple();
   }
 
-  public NTuple<Location> getDeltaOperandLocationVec() {
-    return locTuple;
+  public int getNumDelta() {
+    return numDelta;
   }
 
-  // public Set<Location> getBaseLocationSet() {
-  //
-  // if (operandVec.size() == 1 && (operandVec.get(0) instanceof DeltaLocation))
-  // {
-  // // nested delta definition
-  // DeltaLocation deltaLoc = (DeltaLocation) operandVec.get(0);
-  // return deltaLoc.getBaseLocationSet();
-  // } else {
-  // Set<Location> set = new HashSet<Location>();
-  // set.addAll(operandVec);
-  // return set;
-  // }
-  //
-  // }
-
-  public boolean equals(Object o) {
-
-    if (!(o instanceof DeltaLocation)) {
-      return false;
-    }
-
-    DeltaLocation deltaLoc = (DeltaLocation) o;
-
-    if (deltaLoc.getDeltaOperandLocationVec().equals(getDeltaOperandLocationVec())) {
-      return true;
-    }
-    return false;
-  }
+  public String toString() {
 
-  public int hashCode() {
-    int hash = locTuple.hashCode();
-    if (refOperand != null) {
-      hash += refOperand.hashCode();
+    String rtr = "";
+    for (int i = 0; i < numDelta; i++) {
+      rtr += "DELTA[";
     }
-    return hash;
-  }
 
-  public String toString() {
-    String rtr = "delta(";
-
-    if (locTuple.size() != 0) {
-      int tupleSize = locTuple.size();
-      for (int i = 0; i < tupleSize; i++) {
-        Location locElement = locTuple.get(i);
-        if (i != 0) {
-          rtr += ",";
-        }
-        rtr += locElement;
+    int tupleSize = locTuple.size();
+    for (int i = 0; i < tupleSize; i++) {
+      Location locElement = locTuple.get(i);
+      if (i != 0) {
+        rtr += ",";
       }
-    } else {
-      rtr += "LOC_REF";
+      rtr += locElement;
     }
 
-    rtr += ")";
+    for (int i = 0; i < numDelta; i++) {
+      rtr += "]";
+    }
 
     return rtr;
   }

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 21fabb133d7252bd18947b173e4e938d415fdb7f..54a17f4435908f261cfc911cb4a69ddf7e0e4af7 100644 (file)
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -41,7 +41,6 @@ import IR.Tree.ReturnNode;
 import IR.Tree.SubBlockNode;
 import IR.Tree.TertiaryNode;
 import IR.Tree.TreeNode;
-import Util.Pair;
 
 public class FlowDownCheck {
 
@@ -112,39 +111,6 @@ public class FlowDownCheck {
 
     }
 
-    // // post-processing for delta location
-    // // for a nested delta location, assigning a concrete reference to delta
-    // // operand
-    // Set<Descriptor> tdSet = d2loc.keySet();
-    // for (Iterator iterator = tdSet.iterator(); iterator.hasNext();) {
-    // Descriptor td = (Descriptor) iterator.next();
-    // Location loc = d2loc.get(td);
-    //
-    // if (loc.getType() == Location.DELTA) {
-    // // if it contains delta reference pointing to another location element
-    // CompositeLocation compLoc = (CompositeLocation) loc;
-    //
-    // Location locElement = compLoc.getTuple().at(0);
-    // assert (locElement instanceof DeltaLocation);
-    //
-    // DeltaLocation delta = (DeltaLocation) locElement;
-    // Descriptor refType = delta.getRefLocationId();
-    // if (refType != null) {
-    // Location refLoc = d2loc.get(refType);
-    //
-    // assert (refLoc instanceof CompositeLocation);
-    // CompositeLocation refCompLoc = (CompositeLocation) refLoc;
-    //
-    // assert (refCompLoc.getTuple().at(0) instanceof DeltaLocation);
-    // DeltaLocation refDelta = (DeltaLocation) refCompLoc.getTuple().at(0);
-    //
-    // delta.addDeltaOperand(refDelta);
-    // // compLoc.addLocation(refDelta);
-    // }
-    //
-    // }
-    // }
-
     // phase2 : checking assignments
     toanalyze.addAll(classtable.getValueSet());
     toanalyze.addAll(state.getTaskSymbolTable().getValueSet());
@@ -861,13 +827,6 @@ public class FlowDownCheck {
     if (!left.getType().isPrimitive()) {
       FieldDescriptor fd = fan.getField();
       Location fieldLoc = (Location) fd.getType().getExtension();
-      // Location fieldLoc = d2loc.get(fd);
-
-      // in the case of "this.field", need to get rid of 'this' location from
-      // the composite location
-      // if (loc.getCd2Loc().containsKey(md.getClassDesc())) {
-      // loc.removieLocation(md.getClassDesc());
-      // }
       loc.addLocation(fieldLoc);
     }
 
@@ -892,11 +851,12 @@ public class FlowDownCheck {
     if (!postinc) {
       srcLocation = new CompositeLocation();
       srcLocation = checkLocationFromExpressionNode(md, nametable, an.getSrc(), srcLocation);
-//      System.out.println("an=" + an.printNode(0) + " an.getSrc()=" + an.getSrc().getClass()
-//          + " at " + cd.getSourceFileName() + "::" + an.getNumLine());
+      // System.out.println("an=" + an.printNode(0) + " an.getSrc()=" +
+      // an.getSrc().getClass()
+      // + " at " + cd.getSourceFileName() + "::" + an.getNumLine());
       if (!CompositeLattice.isGreaterThan(srcLocation, destLocation)) {
         throw new Error("The value flow from " + srcLocation + " to " + destLocation
-            + " does not respect location hierarchy on the assignment " + an.printNode(0) + "at "
+            + " does not respect location hierarchy on the assignment " + an.printNode(0) + " at "
             + cd.getSourceFileName() + "::" + an.getNumLine());
       }
     } else {
@@ -942,75 +902,39 @@ public class FlowDownCheck {
 
       if (ad.getMarker().equals(SSJavaAnalysis.LOC)) {
         String locDec = ad.getValue(); // check if location is defined
-        CompositeLocation compLoc = parseLocationDeclaration(md, n, locDec);
-        d2loc.put(vd, compLoc);
-        addTypeLocation(vd.getType(), compLoc);
-
-      } else if (ad.getMarker().equals(SSJavaAnalysis.DELTA)) {
-        // TODO
-        // CompositeLocation compLoc = new CompositeLocation(cd);
-        //
-        // if (ad.getValue().length() == 0) {
-        // throw new Error("Delta function of " + vd.getSymbol() +
-        // " does not have any locations: "
-        // + cd.getSymbol() + ".");
-        // }
-        //
-        // String deltaStr = ad.getValue();
-        // if (deltaStr.startsWith("LOC(")) {
-        //
-        // if (!deltaStr.endsWith(")")) {
-        // throw new Error("The declaration of the delta location is wrong at "
-        // + cd.getSourceFileName() + ":" + n.getNumLine());
-        // }
-        // String locationOperand = deltaStr.substring(4, deltaStr.length() -
-        // 1);
-        //
-        // nametable.get(locationOperand);
-        // Descriptor d = (Descriptor) nametable.get(locationOperand);
-        //
-        // if (d instanceof VarDescriptor) {
-        // VarDescriptor varDescriptor = (VarDescriptor) d;
-        // DeltaLocation deltaLoc = new DeltaLocation(cd, varDescriptor); //
-        // td2loc.put(vd.getType(),
-        // // compLoc);
-        // compLoc.addLocation(deltaLoc);
-        // } else if (d instanceof FieldDescriptor) {
-        // throw new Error("Applying delta operation to the field " +
-        // locationOperand
-        // + " is not allowed at " + cd.getSourceFileName() + ":" +
-        // n.getNumLine());
-        // }
-        // } else {
-        // StringTokenizer token = new StringTokenizer(deltaStr, ",");
-        // DeltaLocation deltaLoc = new DeltaLocation(cd);
-        //
-        // while (token.hasMoreTokens()) {
-        // String deltaOperand = token.nextToken();
-        // ClassDescriptor deltaCD = id2cd.get(deltaOperand);
-        // if (deltaCD == null) {
-        // // delta operand is not defined in the location hierarchy throw
-        // // new
-        // Error("Delta operand '" + deltaOperand + "' of declaration node '" +
-        // vd
-        // + "' is not defined by location hierarchies.");
-        // }
-        //
-        // Location loc = new Location(deltaCD, deltaOperand);
-        // deltaLoc.addDeltaOperand(loc);
-        // }
-        // compLoc.addLocation(deltaLoc);
-        //
-        // }
-        //
-        // d2loc.put(vd, compLoc);
-        // addTypeLocation(vd.getType(), compLoc);
+
+        if (locDec.startsWith(SSJavaAnalysis.DELTA)) {
+          DeltaLocation deltaLoc = parseDeltaDeclaration(md, n, locDec);
+          d2loc.put(vd, deltaLoc);
+          addTypeLocation(vd.getType(), deltaLoc);
+        } else {
+          CompositeLocation compLoc = parseLocationDeclaration(md, n, locDec);
+          d2loc.put(vd, compLoc);
+          addTypeLocation(vd.getType(), compLoc);
+        }
 
       }
     }
 
   }
 
+  private DeltaLocation parseDeltaDeclaration(MethodDescriptor md, TreeNode n, String locDec) {
+
+    int deltaCount = 0;
+    int dIdx = locDec.indexOf(SSJavaAnalysis.DELTA);
+    while (dIdx >= 0) {
+      deltaCount++;
+      int beginIdx = dIdx + 6;
+      locDec = locDec.substring(beginIdx, locDec.length() - 1);
+      dIdx = locDec.indexOf(SSJavaAnalysis.DELTA);
+    }
+
+    CompositeLocation compLoc = parseLocationDeclaration(md, n, locDec);
+    DeltaLocation deltaLoc = new DeltaLocation(compLoc, deltaCount);
+
+    return deltaLoc;
+  }
+
   private CompositeLocation parseLocationDeclaration(MethodDescriptor md, TreeNode n, String locDec) {
 
     CompositeLocation compLoc = new CompositeLocation();
@@ -1032,6 +956,9 @@ public class FlowDownCheck {
     SSJavaLattice<String> localLattice = CompositeLattice.getLatticeByDescriptor(md);
     Location localLoc = new Location(md, localLocId);
     if (localLattice == null || (!localLattice.containsKey(localLocId))) {
+      System.out.println("md=" + md);
+      System.out.println("localLattice=" + localLattice + " l=" + localLocId);
+      System.out.println("localLattice leemtn=" + localLattice.table);
       throw new Error("Location " + localLocId
           + " is not defined in the local variable lattice at "
           + md.getClassDesc().getSourceFileName() + "::" + n.getNumLine() + ".");
@@ -1115,36 +1042,7 @@ public class FlowDownCheck {
         // d2loc.put(fd, loc);
         addTypeLocation(fd.getType(), loc);
 
-      } else if (ad.getMarker().equals(SSJavaAnalysis.DELTA)) {
-
-        // if (ad.getValue().length() == 0) {
-        // throw new Error("Delta function of " + fd.getSymbol() +
-        // " does not have any locations: "
-        // + cd.getSymbol() + ".");
-        // }
-        //
-        // CompositeLocation compLoc = new CompositeLocation(cd);
-        // DeltaLocation deltaLoc = new DeltaLocation(cd);
-        //
-        // StringTokenizer token = new StringTokenizer(ad.getValue(), ",");
-        // while (token.hasMoreTokens()) {
-        // String deltaOperand = token.nextToken();
-        // ClassDescriptor deltaCD = id2cd.get(deltaOperand);
-        // if (deltaCD == null) {
-        // // delta operand is not defined in the location hierarchy
-        // throw new Error("Delta operand '" + deltaOperand +
-        // "' of field node '" + fd
-        // + "' is not defined by location hierarchies.");
-        // }
-        //
-        // Location loc = new Location(deltaCD, deltaOperand);
-        // deltaLoc.addDeltaOperand(loc);
-        // }
-        // compLoc.addLocation(deltaLoc);
-        // d2loc.put(fd, compLoc);
-        // addTypeLocation(fd.getType(), compLoc);
-
-      }
+      } 
     }
 
   }
@@ -1183,13 +1081,24 @@ public class FlowDownCheck {
     }
 
     private static int compareDelta(CompositeLocation dLoc1, CompositeLocation dLoc2) {
-      // TODO
-      return 0;
-      // if (compLoc1.getNumofDelta() < compLoc2.getNumofDelta()) {
-      // return ComparisonResult.GREATER;
-      // } else {
-      // return ComparisonResult.LESS;
-      // }
+
+      int deltaCount1 = 0;
+      int deltaCount2 = 0;
+      if (dLoc1 instanceof DeltaLocation) {
+        deltaCount1 = ((DeltaLocation) dLoc1).getNumDelta();
+      }
+
+      if (dLoc2 instanceof DeltaLocation) {
+        deltaCount2 = ((DeltaLocation) dLoc2).getNumDelta();
+      }
+      if (deltaCount1 < deltaCount2) {
+        return ComparisonResult.GREATER;
+      } else if (deltaCount1 == deltaCount2) {
+        return ComparisonResult.EQUAL;
+      } else {
+        return ComparisonResult.LESS;
+      }
+
     }
 
     private static int compareBaseLocationSet(CompositeLocation compLoc1, CompositeLocation compLoc2) {
@@ -1197,12 +1106,6 @@ public class FlowDownCheck {
       // if compLoc1 is greater than compLoc2, return true
       // else return false;
 
-      // if (compLoc1.getSize() != compLoc2.getSize()) {
-      // throw new Error("Failed to compare two locations of " + compLoc1 +
-      // " and " + compLoc2
-      // + " because they are not comparable.");
-      // }
-
       // compare one by one in according to the order of the tuple
       int numOfTie = 0;
       for (int i = 0; i < compLoc1.getSize(); i++) {
@@ -1347,7 +1250,7 @@ public class FlowDownCheck {
       if (d instanceof ClassDescriptor) {
         lattice = ssjava.getCd2lattice().get(d);
       } else if (d instanceof MethodDescriptor) {
-        if (ssjava.getMd2lattice().contains(d)) {
+        if (ssjava.getMd2lattice().containsKey(d)) {
           lattice = ssjava.getMd2lattice().get(d);
         } else {
           // use default lattice for the method

diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
index 573cc980d07c051c411a9b327b69691cf6b8d36b..838e51035185cf8b89c96f06cbf994aac521d010 100644 (file)
--- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
+++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
@@ -18,7 +18,7 @@ public class SSJavaAnalysis {
   public static final String THISLOC = "THISLOC";
   public static final String GLOBALLOC = "GLOBALLOC";
   public static final String LOC = "LOC";
-  public static final String DELTA = "delta";
+  public static final String DELTA = "DELTA";
   State state;
   FlowDownCheck flowDownChecker;
 
@@ -83,16 +83,19 @@ public class SSJavaAnalysis {
       for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
         MethodDescriptor md = (MethodDescriptor) method_it.next();
         // parsing location hierarchy declaration for the method
-        Vector<AnnotationDescriptor> methodAnnotations = cd.getModifier().getAnnotations();
-        for (int i = 0; i < methodAnnotations.size(); i++) {
-          AnnotationDescriptor an = methodAnnotations.elementAt(i);
-          if (an.getMarker().equals(LATTICE)) {
-            MethodLattice<String> locOrder =
-                new MethodLattice<String>(SSJavaLattice.TOP, SSJavaLattice.BOTTOM);
-            md2lattice.put(md, locOrder);
-            parseMethodLatticeDefinition(cd, an.getValue(), locOrder);
+        Vector<AnnotationDescriptor> methodAnnotations = md.getModifiers().getAnnotations();
+        if (methodAnnotations != null) {
+          for (int i = 0; i < methodAnnotations.size(); i++) {
+            AnnotationDescriptor an = methodAnnotations.elementAt(i);
+            if (an.getMarker().equals(LATTICE)) {
+              MethodLattice<String> locOrder =
+                  new MethodLattice<String>(SSJavaLattice.TOP, SSJavaLattice.BOTTOM);
+              md2lattice.put(md, locOrder);
+              parseMethodLatticeDefinition(cd, an.getValue(), locOrder);
+            }
           }
         }
+
       }
 
     }
@@ -199,7 +202,7 @@ public class SSJavaAnalysis {
   }
 
   public MethodLattice<String> getMethodLattice(MethodDescriptor md) {
-    if (md2lattice.contains(md)) {
+    if (md2lattice.containsKey(md)) {
       return md2lattice.get(md);
     } else {
       return cd2methodDefault.get(md.getClassDesc());