fix bugs and changes on method checking

diff --git a/Robust/src/Analysis/SSJava/DeltaLocation.java b/Robust/src/Analysis/SSJava/DeltaLocation.java
index d4795153db489e7999a838feb120f86568fafc3d..2a627ea057d60400fd05d973963d7f1ac36ae3d9 100644 (file)
--- a/Robust/src/Analysis/SSJava/DeltaLocation.java
+++ b/Robust/src/Analysis/SSJava/DeltaLocation.java
@@ -52,4 +52,24 @@ public class DeltaLocation extends CompositeLocation {
     return clone;
   }
 
+  public boolean equals(Object o) {
+
+    if (!(o instanceof DeltaLocation)) {
+      return false;
+    }
+
+    DeltaLocation deltaLoc = (DeltaLocation) o;
+
+    if (deltaLoc.getTuple().equals(getTuple()) && deltaLoc.getNumDelta() == numDelta) {
+      return true;
+    } else {
+      return false;
+    }
+
+  }
+
+  public int hashCode() {
+    return locTuple.hashCode() + numDelta;
+  }
+
 }

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 4fd0f1084d8ac09eabd26256d97ce77b264603b7..46374bcd9e00053431ec05c2bec1ec87132edaeb 100644 (file)
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -9,6 +9,8 @@ import java.util.Set;
 import java.util.StringTokenizer;
 import java.util.Vector;
 
+import Analysis.SSJava.FlowDownCheck.ComparisonResult;
+import Analysis.SSJava.FlowDownCheck.CompositeLattice;
 import IR.AnnotationDescriptor;
 import IR.ClassDescriptor;
 import IR.Descriptor;
@@ -53,6 +55,9 @@ public class FlowDownCheck {
   // mapping from 'descriptor' to 'composite location'
   Hashtable<Descriptor, CompositeLocation> d2loc;
 
+  Hashtable<MethodDescriptor, CompositeLocation> md2ReturnLoc;
+  Hashtable<MethodDescriptor, ReturnLocGenerator> md2ReturnLocGen;
+
   // mapping from 'locID' to 'class descriptor'
   Hashtable<String, ClassDescriptor> fieldLocName2cd;
 
@@ -62,6 +67,8 @@ public class FlowDownCheck {
     this.toanalyze = new HashSet();
     this.d2loc = new Hashtable<Descriptor, CompositeLocation>();
     this.fieldLocName2cd = new Hashtable<String, ClassDescriptor>();
+    this.md2ReturnLoc = new Hashtable<MethodDescriptor, CompositeLocation>();
+    this.md2ReturnLocGen = new Hashtable<MethodDescriptor, ReturnLocGenerator>();
   }
 
   public void init() {
@@ -167,11 +174,53 @@ public class FlowDownCheck {
 
   private void checkDeclarationInMethodBody(ClassDescriptor cd, MethodDescriptor md) {
     BlockNode bn = state.getMethodBody(md);
+
+    // parsing returnloc annotation
+    if (ssjava.hasAnnotation(md)) {
+      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(ssjava.RETURNLOC)) {
+            // developer explicitly defines method lattice
+            String returnLocDeclaration = an.getValue();
+            CompositeLocation returnLocComp =
+                parseLocationDeclaration(md, null, returnLocDeclaration);
+            md2ReturnLoc.put(md, returnLocComp);
+          }
+        }
+
+        if (!md.getReturnType().isVoid() && !md2ReturnLoc.containsKey(md)) {
+          throw new Error("Return location is not specified for the method " + md + " at "
+              + cd.getSourceFileName());
+        }
+
+      }
+    }
+
+    List<CompositeLocation> paramList = new ArrayList<CompositeLocation>();
+
+    boolean hasReturnValue = (!md.getReturnType().isVoid());
+    if (hasReturnValue) {
+      MethodLattice<String> methodLattice = ssjava.getMethodLattice(md);
+      String thisLocId = methodLattice.getThisLoc();
+      CompositeLocation thisLoc = new CompositeLocation(new Location(md, thisLocId));
+      paramList.add(thisLoc);
+    }
+
     for (int i = 0; i < md.numParameters(); i++) {
       // process annotations on method parameters
       VarDescriptor vd = (VarDescriptor) md.getParameter(i);
       assignLocationOfVarDescriptor(vd, md, md.getParameterTable(), bn);
+      if (hasReturnValue) {
+        paramList.add(d2loc.get(vd));
+      }
     }
+
+    if (hasReturnValue) {
+      md2ReturnLocGen.put(md, new ReturnLocGenerator(md2ReturnLoc.get(md), paramList));
+    }
+
     checkDeclarationInBlockNode(md, md.getParameterTable(), bn);
   }
 
@@ -229,22 +278,19 @@ public class FlowDownCheck {
     // it will return the lowest location in the block node
     CompositeLocation lowestLoc = null;
 
-    // if(bn.get(0).kind() == Kind.LoopNode){
-    // System.out.println("####="+bn.get(0).printNode(0));
-    // }
-
     for (int i = 0; i < bn.size(); i++) {
       BlockStatementNode bsn = bn.get(i);
       CompositeLocation bLoc = checkLocationFromBlockStatementNode(md, bn.getVarTable(), bsn);
-      if (lowestLoc == null) {
-        lowestLoc = bLoc;
-      } else {
-        if (!bLoc.isEmpty()) {
+      if (!bLoc.isEmpty()) {
+        if (lowestLoc == null) {
+          lowestLoc = bLoc;
+        } else {
           if (CompositeLattice.isGreaterThan(lowestLoc, bLoc)) {
             lowestLoc = bLoc;
           }
         }
       }
+
     }
     return lowestLoc;
   }
@@ -294,19 +340,6 @@ public class FlowDownCheck {
     CompositeLocation expLoc =
         checkLocationFromExpressionNode(md, nametable, returnExp, new CompositeLocation());
 
-    // callee should have a relative ordering in-between parameters and return
-    // value, which is required by caller's constraint
-    for (int i = 0; i < md.numParameters(); i++) {
-      Descriptor calleevd = md.getParameter(i);
-      CompositeLocation calleeParamLoc = d2loc.get(calleevd);
-
-      // here, parameter(input value) should be higher than result(output)
-      if ((!expLoc.get(0).isTop()) && !CompositeLattice.isGreaterThan(calleeParamLoc, expLoc)) {
-        throw new Error("Callee " + md + " doesn't have the ordering relation between parameter '"
-            + calleevd + "' and its return value '" + returnExp.printNode(0) + "'.");
-      }
-    }
-
     // by default, return node has "bottom" location
     CompositeLocation loc = new CompositeLocation();
     loc.addLocation(Location.createBottomLocation(md));
@@ -459,14 +492,7 @@ public class FlowDownCheck {
 
     } else {
 
-      // if (destLoc instanceof Location) {
-      // CompositeLocation comp = new CompositeLocation();
-      // comp.addLocation(destLoc);
-      // return comp;
-      // } else {
-      // return (CompositeLocation) destLoc;
-      // }
-      return destLoc;
+      return new CompositeLocation();
 
     }
 
@@ -604,26 +630,32 @@ public class FlowDownCheck {
       SymbolTable nametable, MethodInvokeNode min, CompositeLocation loc) {
 
     checkCalleeConstraints(md, nametable, min);
+    if (!min.getMethod().getReturnType().isVoid()) {
+      CompositeLocation ceilingLoc = computeCeilingLocationForCaller(md, nametable, min);
+      return ceilingLoc;
+    }
+
+    return new CompositeLocation();
+
+  }
+
+  private CompositeLocation computeCeilingLocationForCaller(MethodDescriptor md,
+      SymbolTable nametable, MethodInvokeNode min) {
+
+    List<CompositeLocation> argList = new ArrayList<CompositeLocation>();
+
+    String thisLocId = ssjava.getMethodLattice(md).getThisLoc();
+    CompositeLocation thisLoc = new CompositeLocation(new Location(md, thisLocId));
+    argList.add(thisLoc);
 
-    // all we need to care about is that
-    // method output(return value) should be lower than input values(method
-    // parameters)
-    Set<CompositeLocation> inputGLBSet = new HashSet<CompositeLocation>();
     for (int i = 0; i < min.numArgs(); i++) {
       ExpressionNode en = min.getArg(i);
       CompositeLocation callerArg =
           checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation());
-      inputGLBSet.add(callerArg);
+      argList.add(callerArg);
     }
 
-    if (inputGLBSet.size() > 0) {
-      return CompositeLattice.calculateGLB(inputGLBSet);
-    } else {
-      // if there are no arguments, just return TOP location
-      CompositeLocation compLoc = new CompositeLocation();
-      compLoc.addLocation(Location.createTopLocation(md));
-      return compLoc;
-    }
+    return md2ReturnLocGen.get(min.getMethod()).computeReturnLocation(argList);
 
   }
 
@@ -1032,7 +1064,7 @@ public class FlowDownCheck {
     if (localLattice == null || (!localLattice.containsKey(localLocId))) {
       throw new Error("Location " + localLocId
           + " is not defined in the local variable lattice at "
-          + md.getClassDesc().getSourceFileName() + "::" + n.getNumLine() + ".");
+          + md.getClassDesc().getSourceFileName() + "::" + (n != null ? n.getNumLine() : "") + ".");
     }
     compLoc.addLocation(localLoc);
 
@@ -1153,6 +1185,19 @@ public class FlowDownCheck {
 
     }
 
+    public static int compare(CompositeLocation loc1, CompositeLocation loc2) {
+
+//      System.out.println("compare=" + loc1 + " " + loc2);
+      int baseCompareResult = compareBaseLocationSet(loc1, loc2);
+
+      if (baseCompareResult == ComparisonResult.EQUAL) {
+        return compareDelta(loc1, loc2);
+      } else {
+        return baseCompareResult;
+      }
+
+    }
+
     private static int compareDelta(CompositeLocation dLoc1, CompositeLocation dLoc2) {
 
       int deltaCount1 = 0;
@@ -1273,7 +1318,7 @@ public class FlowDownCheck {
         String priorityLocId = priorityLoc.getLocIdentifier();
         priorityLocIdentifierSet.add(priorityLocId);
 
-        if (locId2CompLocSet.contains(priorityLocId)) {
+        if (locId2CompLocSet.containsKey(priorityLocId)) {
           locId2CompLocSet.get(priorityLocId).add(compLoc);
         } else {
           Set<CompositeLocation> newSet = new HashSet<CompositeLocation>();
@@ -1300,17 +1345,27 @@ public class FlowDownCheck {
         // when GLB(x1,x2)!=x1 and !=x2 : GLB case 4
         // mean that the result is already lower than <x1,y1> and <x2,y2>
         // assign TOP to the rest of the location elements
+
+        // in this case, do not take care about delta
         CompositeLocation inputComp = inputSet.iterator().next();
         for (int i = 1; i < inputComp.getSize(); i++) {
           glbCompLoc.addLocation(Location.createTopLocation(inputComp.get(i).getDescriptor()));
         }
       } else {
         if (compSet.size() == 1) {
+
           // if GLB(x1,x2)==x1 or x2 : GLB case 2,3
           CompositeLocation comp = compSet.iterator().next();
           for (int i = 1; i < comp.getSize(); i++) {
             glbCompLoc.addLocation(comp.get(i));
           }
+
+          // if input location corresponding to glb is a delta, need to apply
+          // delta to glb result
+          if (comp instanceof DeltaLocation) {
+            glbCompLoc = new DeltaLocation(glbCompLoc, 1);
+          }
+
         } else {
           // when GLB(x1,x2)==x1 and x2 : GLB case 1
           // if more than one location shares the same priority GLB
@@ -1335,6 +1390,19 @@ public class FlowDownCheck {
             glbCompLoc.addLocation(new Location(currentD, currentGLBLocId));
           }
 
+          // if input location corresponding to glb is a delta, need to apply
+          // delta to glb result
+
+          for (Iterator iterator = compSet.iterator(); iterator.hasNext();) {
+            CompositeLocation compLoc = (CompositeLocation) iterator.next();
+            if (compLoc instanceof DeltaLocation) {
+              if (glbCompLoc.equals(compLoc)) {
+                glbCompLoc = new DeltaLocation(glbCompLoc, 1);
+                break;
+              }
+            }
+          }
+
         }
       }
 
@@ -1367,8 +1435,65 @@ public class FlowDownCheck {
     public static final int GREATER = 0;
     public static final int EQUAL = 1;
     public static final int LESS = 2;
+    public static final int INCOMPARABLE = 3;
     int result;
 
   }
 
 }
+
+class ReturnLocGenerator {
+
+  public static final int PARAMISHIGHER = 0;
+  public static final int PARAMISSAME = 1;
+  public static final int IGNORE = 2;
+
+  Hashtable<Integer, Integer> paramIdx2paramType;
+
+  public ReturnLocGenerator(CompositeLocation returnLoc, List<CompositeLocation> params) {
+    // creating mappings
+
+    paramIdx2paramType = new Hashtable<Integer, Integer>();
+    for (int i = 0; i < params.size(); i++) {
+      CompositeLocation param = params.get(i);
+      int compareResult = CompositeLattice.compare(param, returnLoc);
+
+      int type;
+      if (compareResult == ComparisonResult.GREATER) {
+        type = 0;
+      } else if (compareResult == ComparisonResult.EQUAL) {
+        type = 1;
+      } else {
+        type = 2;
+      }
+      paramIdx2paramType.put(new Integer(i), new Integer(type));
+    }
+
+  }
+
+  public CompositeLocation computeReturnLocation(List<CompositeLocation> args) {
+
+    // compute the highest possible location in caller's side
+    assert paramIdx2paramType.keySet().size() == args.size();
+
+    Set<CompositeLocation> inputGLB = new HashSet<CompositeLocation>();
+    for (int i = 0; i < args.size(); i++) {
+      int type = (paramIdx2paramType.get(new Integer(i))).intValue();
+      CompositeLocation argLoc = args.get(i);
+      if (type == PARAMISHIGHER) {
+        // return loc is lower than param
+        System.out.println("argLoc=" + argLoc);
+        DeltaLocation delta = new DeltaLocation(argLoc, 1);
+        inputGLB.add(delta);
+      } else if (type == PARAMISSAME) {
+        // return loc is equal or lower than param
+        inputGLB.add(argLoc);
+      }
+    }
+
+    // compute GLB of arguments subset that are same or higher than return
+    // location
+    CompositeLocation glb = CompositeLattice.calculateGLB(inputGLB);
+    return glb;
+  }
+}

diff --git a/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java b/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java
index 9ef4b4a8c6701f32d2f81d29709696a2048996bf..9f61ee213d1e8545b14f7dbfcecb0512384454b3 100644 (file)
--- a/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java
+++ b/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java
@@ -165,7 +165,7 @@ public class MethodAnnotationCheck {
       break;
 
     case Kind.DeclarationNode:
-      // checkLocationFromDeclarationNode(md, nametable, (DeclarationNode) bsn);
+      checkDeclarationNode(md, nametable, (DeclarationNode) bsn, flag);
       break;
 
     case Kind.IfStatementNode:
@@ -183,14 +183,15 @@ public class MethodAnnotationCheck {
     }
   }
 
-  void checkDeclarationNode(MethodDescriptor md, SymbolTable nametable, DeclarationNode dn,
+  private void checkDeclarationNode(MethodDescriptor md, SymbolTable nametable, DeclarationNode dn,
       boolean flag) {
     if (dn.getExpression() != null) {
       checkExpressionNode(md, nametable, dn.getExpression(), flag);
     }
   }
 
-  void checkReturnNode(MethodDescriptor md, SymbolTable nametable, ReturnNode rn, boolean flag) {
+  private void checkReturnNode(MethodDescriptor md, SymbolTable nametable, ReturnNode rn,
+      boolean flag) {
     if (rn.getReturnExpression() != null) {
       if (md.getReturnType() != null) {
         checkExpressionNode(md, nametable, rn.getReturnExpression(), flag);
@@ -198,7 +199,7 @@ public class MethodAnnotationCheck {
     }
   }
 
-  void checkLoopNode(MethodDescriptor md, SymbolTable nametable, LoopNode ln, boolean flag) {
+  private void checkLoopNode(MethodDescriptor md, SymbolTable nametable, LoopNode ln, boolean flag) {
     if (ln.getType() == LoopNode.WHILELOOP || ln.getType() == LoopNode.DOWHILELOOP) {
       checkExpressionNode(md, nametable, ln.getCondition(), flag);
       checkBlockNode(md, nametable, ln.getBody(), flag);
@@ -218,8 +219,8 @@ public class MethodAnnotationCheck {
     }
   }
 
-  void checkIfStatementNode(MethodDescriptor md, SymbolTable nametable, IfStatementNode isn,
-      boolean flag) {
+  private void checkIfStatementNode(MethodDescriptor md, SymbolTable nametable,
+      IfStatementNode isn, boolean flag) {
     checkExpressionNode(md, nametable, isn.getCondition(), flag);
     checkBlockNode(md, nametable, isn.getTrueBlock(), flag);
     if (isn.getFalseBlock() != null) {

diff --git a/Robust/src/Util/Lattice.java b/Robust/src/Util/Lattice.java
index e22103c5d5b9bc9d23fb757333dac1f4807acf18..22ed8d64f99c711882b2c9728e1f6390c54bd00c 100644 (file)
--- a/Robust/src/Util/Lattice.java
+++ b/Robust/src/Util/Lattice.java
@@ -125,6 +125,25 @@ public class Lattice<T> {
     return table.containsKey(o);
   }
 
+  public boolean isComparable(T a, T b) {
+
+    Set<T> neighborSet = get(a);
+
+    if (neighborSet == null) {
+      return false;
+    } else if (neighborSet.contains(b)) {
+      return true;
+    } else {
+      boolean reachable = false;
+      for (Iterator<T> iterator = neighborSet.iterator(); iterator.hasNext();) {
+        T neighbor = iterator.next();
+        reachable = reachable || isComparable(neighbor, b);
+      }
+      return reachable;
+    }
+
+  }
+
   public boolean isGreaterThan(T a, T b) {
 
     if (a.equals(top)) {
@@ -232,7 +251,7 @@ public class Lattice<T> {
     while (!needtovisit.isEmpty()) {
       T key = needtovisit.iterator().next();
       Set<T> lowerSet = table.get(key);
-      if(lowerSet!=null){
+      if (lowerSet != null) {
         for (Iterator iterator = lowerSet.iterator(); iterator.hasNext();) {
           T lowerItem = (T) iterator.next();
           set.add(new Pair(key, lowerItem));