bug fix on the glb function of the lattice + working on the checking with the composi...

diff --git a/Robust/src/Analysis/SSJava/CompositeLocation.java b/Robust/src/Analysis/SSJava/CompositeLocation.java
index bed509d82bef30b8fecc14eae8afd756109e256c..df13d0ca441a984e7f717c97f131504c7a0c5bce 100644 (file)
--- a/Robust/src/Analysis/SSJava/CompositeLocation.java
+++ b/Robust/src/Analysis/SSJava/CompositeLocation.java
@@ -70,7 +70,46 @@ public class CompositeLocation extends Location {
     return baseLocationSet;
   }
 
+  public int getNumofDelta() {
+
+    int result = 0;
+
+    if (locTuple.size() == 1) {
+      Location locElement = locTuple.at(0);
+      if (locElement instanceof DeltaLocation) {
+        result++;
+        result += getNumofDelta((DeltaLocation) locElement);
+      }
+    }
+    return result;
+  }
+
+  public int getNumofDelta(DeltaLocation delta) {
+    int result = 0;
+
+    if (delta.getDeltaOperandLocationVec().size() == 1) {
+      Location locElement = delta.getDeltaOperandLocationVec().get(0);
+      if (locElement instanceof DeltaLocation) {
+        result++;
+        result += getNumofDelta((DeltaLocation) locElement);
+      }
+    }
+
+    return result;
+  }
+
   public String toString() {
+
+    // for better representation
+    // if compositeLoc has only one single location,
+    // just print out single location
+    // if(locTuple.size()==1){
+    // Location locElement=locTuple.at(0);
+    // if(locElement instanceof Location){
+    // return locElement.toString();
+    // }
+    // }
+
     String rtr = "CompLoc[";
 
     int tupleSize = locTuple.size();

diff --git a/Robust/src/Analysis/SSJava/DeltaLocation.java b/Robust/src/Analysis/SSJava/DeltaLocation.java
index 8e71c86c41ba0e3bcc805b26b2ee4d1de5df1eb8..e9233e2a500a7e4de967a8d62623d12b5a21cfaa 100644 (file)
--- a/Robust/src/Analysis/SSJava/DeltaLocation.java
+++ b/Robust/src/Analysis/SSJava/DeltaLocation.java
@@ -13,7 +13,7 @@ public class DeltaLocation extends Location {
     super(cd);
     operandVec = new Vector<Location>();
   }
-
+  
   public void addDeltaOperand(Location op) {
     operandVec.add(op);
   }

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index e38603665199ee8d58a3df1909f493edfa4ca259..f5afbc508a673a61bf61b9ebfb3aaec56cbaf5d5 100644 (file)
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -363,28 +363,16 @@ public class FlowDownCheck {
 
     Lattice<String> locOrder = (Lattice<String>) state.getCd2LocationOrder().get(md.getClassDesc());
 
-    checkExpressionNode(md, nametable, on.getLeft(), null);
-    if (on.getRight() != null)
-      checkExpressionNode(md, nametable, on.getRight(), null);
+    CompositeLocation leftOpLoc = new CompositeLocation(md.getClassDesc());
+    getLocationFromExpressionNode(md, nametable, on.getLeft(), leftOpLoc);
 
-    TypeDescriptor ltd = on.getLeft().getType();
-    TypeDescriptor rtd = on.getRight() != null ? on.getRight().getType() : null;
-
-    if (ltd.getAnnotationMarkers().size() == 0) {
-      // constant value
-      // TODO
-      // ltd.addAnnotationMarker(new AnnotationDescriptor(Lattice.TOP));
-    }
-    if (rtd != null && rtd.getAnnotationMarkers().size() == 0) {
-      // constant value
-      // TODO
-      // rtd.addAnnotationMarker(new AnnotationDescriptor(Lattice.TOP));
+    CompositeLocation rightOpLoc = new CompositeLocation(md.getClassDesc());
+    if (on.getRight() != null) {
+      getLocationFromExpressionNode(md, nametable, on.getRight(), rightOpLoc);
     }
 
-    System.out.println("checking op node");
-    System.out.println("td=" + td);
-    System.out.println("ltd=" + ltd);
-    System.out.println("rtd=" + rtd);
+    TypeDescriptor ltd = on.getLeft().getType();
+    TypeDescriptor rtd = on.getRight() != null ? on.getRight().getType() : null;
 
     Operation op = on.getOp();
 
@@ -564,17 +552,10 @@ public class FlowDownCheck {
     case Operation.RIGHTSHIFT:
     case Operation.URIGHTSHIFT:
 
-      // Set<String> operandSet = new HashSet<String>();
-      // String leftLoc = ltd.getAnnotationMarkers().get(0).getMarker();
-      // String rightLoc = rtd.getAnnotationMarkers().get(0).getMarker();
-      //
-      // operandSet.add(leftLoc);
-      // operandSet.add(rightLoc);
-
-      // TODO
-      // String glbLoc = locOrder.getGLB(operandSet);
-      // on.getType().addAnnotationMarker(new AnnotationDescriptor(glbLoc));
-      // System.out.println(glbLoc + "<-" + leftLoc + " " + rightLoc);
+      Set<CompositeLocation> inputSet = new HashSet<CompositeLocation>();
+      inputSet.add(leftLoc);
+      inputSet.add(rightLoc);
+      CompositeLattice.calculateGLB(inputSet, cd, loc);
 
       break;
 
@@ -582,15 +563,6 @@ public class FlowDownCheck {
       throw new Error(op.toString());
     }
 
-    // if (td != null) {
-    // String lhsLoc = td.getAnnotationMarkers().get(0).getMarker();
-    // if (locOrder.isGreaterThan(lhsLoc,
-    // on.getType().getAnnotationMarkers().get(0).getMarker())) {
-    // throw new Error("The location of LHS is higher than RHS: " +
-    // on.printNode(0));
-    // }
-    // }
-
   }
 
   private void getLocationFromLiteralNode(MethodDescriptor md, SymbolTable nametable,
@@ -686,7 +658,6 @@ public class FlowDownCheck {
     }
 
     ClassDescriptor cd = md.getClassDesc();
-    Lattice<String> locOrder = (Lattice<String>) state.getCd2LocationOrder().get(cd);
 
     Location destLocation = td2loc.get(an.getDest().getType());
 
@@ -871,15 +842,26 @@ public class FlowDownCheck {
 
       int baseCompareResult = compareBaseLocationSet(compLoc1, compLoc2);
       if (baseCompareResult == ComparisonResult.EQUAL) {
-        // TODO
-        // need to compare # of delta operand
+        if (compareDelta(compLoc1, compLoc2) == ComparisonResult.GREATER) {
+          return true;
+        } else {
+          return false;
+        }
       } else if (baseCompareResult == ComparisonResult.GREATER) {
         return true;
       } else {
         return false;
       }
 
-      return false;
+    }
+
+    private static int compareDelta(CompositeLocation compLoc1, CompositeLocation compLoc2) {
+
+      if (compLoc1.getNumofDelta() < compLoc2.getNumofDelta()) {
+        return ComparisonResult.GREATER;
+      } else {
+        return ComparisonResult.LESS;
+      }
     }
 
     private static int compareBaseLocationSet(CompositeLocation compLoc1, CompositeLocation compLoc2) {
@@ -933,6 +915,54 @@ public class FlowDownCheck {
       return ComparisonResult.GREATER;
     }
 
+    public static CompositeLocation calculateGLB(Set<CompositeLocation> inputSet,
+        ClassDescriptor enclosingCD, CompositeLocation loc) {
+
+      Hashtable<ClassDescriptor, Set<Location>> cd2locSet =
+          new Hashtable<ClassDescriptor, Set<Location>>();
+
+      // creating mapping from class -> set of locations
+      for (Iterator iterator = inputSet.iterator(); iterator.hasNext();) {
+        CompositeLocation compLoc = (CompositeLocation) iterator.next();
+        Set<Location> baseLocationSet = compLoc.getBaseLocationSet();
+        for (Iterator iterator2 = baseLocationSet.iterator(); iterator2.hasNext();) {
+          Location locElement = (Location) iterator2.next();
+          ClassDescriptor locCD = locElement.getClassDescriptor();
+
+          Set<Location> locSet = cd2locSet.get(locCD);
+          if (locSet == null) {
+            locSet = new HashSet<Location>();
+          }
+          locSet.add(locElement);
+
+          cd2locSet.put(locCD, locSet);
+
+        }
+      }
+
+      // calculating GLB element for each class
+      for (Iterator<ClassDescriptor> iterator = cd2locSet.keySet().iterator(); iterator.hasNext();) {
+        ClassDescriptor localCD = iterator.next();
+
+        Set<Location> locSetofClass = cd2locSet.get(localCD);
+
+        Set<String> locIdentifierSet = new HashSet<String>();
+
+        for (Iterator<Location> locIterator = locSetofClass.iterator(); locIterator.hasNext();) {
+          Location locElement = locIterator.next();
+          locIdentifierSet.add(locElement.getLocIdentifier());
+        }
+
+        Lattice<String> locOrder = (Lattice<String>) state.getCd2LocationOrder().get(localCD);
+        String glbLocIdentifer = locOrder.getGLB(locIdentifierSet);
+
+        Location localGLB = new Location(localCD, glbLocIdentifer);
+        loc.addLocation(localGLB);
+      }
+
+      return loc;
+    }
+
   }
 
   class ComparisonResult {

diff --git a/Robust/src/Util/Lattice.java b/Robust/src/Util/Lattice.java
index 7d2ce4b9370b7da62ce58568fe13fc392a0609b4..16b867117a4cf50a1c4810c59bc722ef34298ce5 100644 (file)
--- a/Robust/src/Util/Lattice.java
+++ b/Robust/src/Util/Lattice.java
@@ -153,8 +153,25 @@ public class Lattice<T> {
     for (Iterator<T> iterator = inputSet.iterator(); iterator.hasNext();) {
       T element = iterator.next();
       lowerSet.addAll(getLowerSet(element, new HashSet<T>()));
+      lowerSet.add(element);
     }
 
+    // an element of lower bound should be lower than every input set
+    Set<T> toberemoved = new HashSet<T>();
+    for (Iterator<T> inputIterator = inputSet.iterator(); inputIterator.hasNext();) {
+      T inputElement = inputIterator.next();
+
+      for (Iterator iterator = lowerSet.iterator(); iterator.hasNext();) {
+        T lowerElement = (T) iterator.next();
+        if (!inputElement.equals(lowerElement)) {
+          if (!isGreaterThan(inputElement, lowerElement)) {
+            toberemoved.add(lowerElement);
+          }
+        }
+      }
+    }
+    lowerSet.removeAll(toberemoved);
+
     // calculate the greatest element of lower set
     // find an element A, where every lower bound B of lowerSet, B<A
     for (Iterator<T> iterator = lowerSet.iterator(); iterator.hasNext();) {