X-Git-Url: http://plrg.eecs.uci.edu/git/?p=IRC.git;a=blobdiff_plain;f=Robust%2Fsrc%2FAnalysis%2FSSJava%2FFlowDownCheck.java;h=d01e094eb24759c0f8991a0ebaaf34de383dd7f2;hp=f466b0edbe8abaedb2c3931d54a883e8d0007e5f;hb=98bc69de0d44f8c7b7e4ce2e11f398e8a0e0a1e7;hpb=ff3ceae6b47a1a01bc56fa55fa5770cba0bf252f

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index f466b0ed..d01e094e 100644
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -668,7 +668,6 @@ public class FlowDownCheck {
             constraint, false);
 
     // addLocationType(isn.getCondition().getType(), condLoc);
-
     constraint = generateNewConstraint(constraint, condLoc);
     checkLocationFromBlockNode(md, nametable, isn.getTrueBlock(), constraint);
 
@@ -1021,6 +1020,10 @@ public class FlowDownCheck {
         // location in the caller's perspective
         CompositeLocation ceilingLoc =
             computeCeilingLocationForCaller(md, nametable, min, baseLocation, constraint);
+
+        if (ceilingLoc == null) {
+          return new CompositeLocation(Location.createTopLocation(md));
+        }
         return ceilingLoc;
       }
     }
@@ -1140,7 +1143,9 @@ public class FlowDownCheck {
     List<CompositeLocation> argList = new ArrayList<CompositeLocation>();
 
     // by default, method has a THIS parameter
-    argList.add(baseLocation);
+    if (!md.isStatic()) {
+      argList.add(baseLocation);
+    }
 
     for (int i = 0; i < min.numArgs(); i++) {
       ExpressionNode en = min.getArg(i);
@@ -1162,11 +1167,10 @@ public class FlowDownCheck {
   private void checkCalleeConstraints(MethodDescriptor md, SymbolTable nametable,
       MethodInvokeNode min, CompositeLocation callerBaseLoc, CompositeLocation constraint) {
 
-    // System.out.println("checkCalleeConstraints=" + min.printNode(0));
-
     MethodDescriptor calleemd = min.getMethod();
 
     MethodLattice<String> calleeLattice = ssjava.getMethodLattice(calleemd);
+
     CompositeLocation calleeThisLoc =
         new CompositeLocation(new Location(calleemd, calleeLattice.getThisLoc()));
 
@@ -1179,7 +1183,8 @@ public class FlowDownCheck {
 
       // setup caller args set
       // first, add caller's base(this) location
-      callerArgList.add(callerBaseLoc);
+      if (!calleemd.isStatic())
+        callerArgList.add(callerBaseLoc);
       // second, add caller's arguments
       for (int i = 0; i < min.numArgs(); i++) {
         ExpressionNode en = min.getArg(i);
@@ -1191,7 +1196,8 @@ public class FlowDownCheck {
 
       // setup callee params set
       // first, add callee's this location
-      calleeParamList.add(calleeThisLoc);
+      if (!calleemd.isStatic())
+        calleeParamList.add(calleeThisLoc);
       // second, add callee's parameters
       for (int i = 0; i < calleemd.numParameters(); i++) {
         VarDescriptor calleevd = (VarDescriptor) calleemd.getParameter(i);
@@ -1499,26 +1505,28 @@ public class FlowDownCheck {
       }
     }
 
+    Set<CompositeLocation> inputGLB = new HashSet<CompositeLocation>();
     if (left instanceof ArrayAccessNode) {
       ArrayAccessNode aan = (ArrayAccessNode) left;
-      left = aan.getExpression();
+      CompositeLocation indexLoc =
+          checkLocationFromExpressionNode(md, nametable, aan.getIndex(), loc, constraint, false);
+      inputGLB.add(indexLoc);
     }
 
     loc = checkLocationFromExpressionNode(md, nametable, left, loc, constraint, false);
-    // System.out.println("### checkLocationFromFieldAccessNode=" +
-    // fan.printNode(0));
-    // System.out.println("### left=" + left.printNode(0));
 
     if (!left.getType().isPrimitive()) {
 
-      if (fd.getSymbol().equals("length")) {
+      if (!fd.getSymbol().equals("length")) {
         // array.length access, return the location of the array
-        return loc;
+        Location fieldLoc = getFieldLocation(fd);
+        loc.addLocation(fieldLoc);
       }
 
-      Location fieldLoc = getFieldLocation(fd);
-      loc.addLocation(fieldLoc);
     }
+
+    inputGLB.add(loc);
+    loc = CompositeLattice.calculateGLB(inputGLB, generateErrorMessage(md.getClassDesc(), fan));
     return loc;
   }
 
@@ -1562,7 +1570,6 @@ public class FlowDownCheck {
 
   private CompositeLocation checkLocationFromAssignmentNode(MethodDescriptor md,
       SymbolTable nametable, AssignmentNode an, CompositeLocation loc, CompositeLocation constraint) {
-
     ClassDescriptor cd = md.getClassDesc();
 
     Set<CompositeLocation> inputGLBSet = new HashSet<CompositeLocation>();
@@ -1602,9 +1609,16 @@ public class FlowDownCheck {
       }
 
       if (constraint != null) {
-        inputGLBSet.add(srcLocation);
-        inputGLBSet.add(constraint);
-        srcLocation = CompositeLattice.calculateGLB(inputGLBSet, generateErrorMessage(cd, an));
+
+        if (!CompositeLattice.isGreaterThan(constraint, destLocation, generateErrorMessage(cd, an))) {
+          throw new Error("The value flow from " + constraint + " to " + destLocation
+              + " does not respect location hierarchy on the assignment " + an.printNode(0)
+              + " at " + cd.getSourceFileName() + "::" + an.getNumLine());
+        }
+        // inputGLBSet.add(srcLocation);
+        // inputGLBSet.add(constraint);
+        // srcLocation = CompositeLattice.calculateGLB(inputGLBSet,
+        // generateErrorMessage(cd, an));
       }
 
       if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, generateErrorMessage(cd, an))) {
@@ -1636,9 +1650,17 @@ public class FlowDownCheck {
                   constraint, false);
 
       if (constraint != null) {
-        inputGLBSet.add(rhsLocation);
-        inputGLBSet.add(constraint);
-        srcLocation = CompositeLattice.calculateGLB(inputGLBSet, generateErrorMessage(cd, an));
+
+        if (!CompositeLattice.isGreaterThan(constraint, destLocation, generateErrorMessage(cd, an))) {
+          throw new Error("The value flow from " + constraint + " to " + destLocation
+              + " does not respect location hierarchy on the assignment " + an.printNode(0)
+              + " at " + cd.getSourceFileName() + "::" + an.getNumLine());
+        }
+        // inputGLBSet.add(rhsLocation);
+        // inputGLBSet.add(constraint);
+        // srcLocation = CompositeLattice.calculateGLB(inputGLBSet,
+        // generateErrorMessage(cd, an));
+        srcLocation = rhsLocation;
       } else {
         srcLocation = rhsLocation;
       }
@@ -2081,7 +2103,6 @@ public class FlowDownCheck {
 
       SSJavaLattice<String> locOrder = getLatticeByDescriptor(priorityDescriptor);
       String glbOfPriorityLoc = locOrder.getGLB(priorityLocIdentifierSet);
-
       glbCompLoc.addLocation(new Location(priorityDescriptor, glbOfPriorityLoc));
       Set<CompositeLocation> compSet = locId2CompLocSet.get(glbOfPriorityLoc);
 
@@ -2343,6 +2364,9 @@ class ReturnLocGenerator {
       // compute GLB of arguments subset that are same or higher than return
       // location
       if (inputGLB.isEmpty()) {
+        if (args.size() == 0) {
+          return null;
+        }
         CompositeLocation rtr =
             new CompositeLocation(Location.createTopLocation(args.get(0).get(0).getDescriptor()));
         return rtr;