From: yeom <yeom>
Date: Tue, 26 Jul 2011 18:57:38 +0000 (+0000)
Subject: bug fix on callee constraint checking: previously only checked ordering constraints... 
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=IRC.git;a=commitdiff_plain;h=d3b1f73e10381d3c1f8e01c4505715365ba5d891

bug fix on callee constraint checking: previously only checked ordering constraints of parameters without considering default parameter 'this'
---

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 2a0b8a7a..f24d0fe0 100644
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -826,8 +826,6 @@ public class FlowDownCheck {
       SymbolTable nametable, MethodInvokeNode min, CompositeLocation loc,
       CompositeLocation constraint) {
 
-    checkCalleeConstraints(md, nametable, min, constraint);
-
     CompositeLocation baseLocation = null;
     if (min.getExpression() != null) {
       baseLocation =
@@ -838,6 +836,8 @@ public class FlowDownCheck {
       baseLocation = new CompositeLocation(new Location(md, thisLocId));
     }
 
+    checkCalleeConstraints(md, nametable, min, baseLocation, constraint);
+
     if (!min.getMethod().getReturnType().isVoid()) {
       // If method has a return value, compute the highest possible return
       // location in the caller's perspective
@@ -876,55 +876,89 @@ public class FlowDownCheck {
   }
 
   private void checkCalleeConstraints(MethodDescriptor md, SymbolTable nametable,
-      MethodInvokeNode min, CompositeLocation constraint) {
+      MethodInvokeNode min, CompositeLocation callerBaseLoc, CompositeLocation constraint) {
+
+    MethodDescriptor calleemd = min.getMethod();
+
+    MethodLattice<String> calleeLattice = ssjava.getMethodLattice(calleemd);
+    CompositeLocation calleeThisLoc =
+        new CompositeLocation(new Location(calleemd, calleeLattice.getThisLoc()));
 
-    if (min.numArgs() > 1) {
+    List<CompositeLocation> callerArgList = new ArrayList<CompositeLocation>();
+    List<CompositeLocation> calleeParamList = new ArrayList<CompositeLocation>();
+
+    if (min.numArgs() > 0) {
       // caller needs to guarantee that it passes arguments in regarding to
       // callee's hierarchy
+
+      // setup caller args set
+      // first, add caller's base(this) location
+      callerArgList.add(callerBaseLoc);
+      // second, add caller's arguments
       for (int i = 0; i < min.numArgs(); i++) {
         ExpressionNode en = min.getArg(i);
-        CompositeLocation callerArg1 =
+        CompositeLocation callerArgLoc =
             checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(), constraint,
                 false);
+        callerArgList.add(callerArgLoc);
+      }
 
-        VarDescriptor calleevd = (VarDescriptor) min.getMethod().getParameter(i);
-        CompositeLocation calleeLoc1 = d2loc.get(calleevd);
-
-        if (!callerArg1.get(0).isTop()) {
-          // here, check if ordering relations among caller's args respect
-          // ordering relations in-between callee's args
-          for (int currentIdx = 0; currentIdx < min.numArgs(); currentIdx++) {
-            if (currentIdx != i) { // skip itself
-              ExpressionNode argExp = min.getArg(currentIdx);
-
-              CompositeLocation callerArg2 =
-                  checkLocationFromExpressionNode(md, nametable, argExp, new CompositeLocation(),
-                      constraint, false);
-
-              VarDescriptor calleevd2 = (VarDescriptor) min.getMethod().getParameter(currentIdx);
-              CompositeLocation calleeLoc2 = d2loc.get(calleevd2);
-
-              int callerResult =
-                  CompositeLattice.compare(callerArg1, callerArg2,
-                      generateErrorMessage(md.getClassDesc(), min));
-              int calleeResult =
-                  CompositeLattice.compare(calleeLoc1, calleeLoc2,
-                      generateErrorMessage(md.getClassDesc(), min));
-
-              if (calleeResult == ComparisonResult.GREATER
-                  && callerResult != ComparisonResult.GREATER) {
-                // If calleeLoc1 is higher than calleeLoc2
-                // then, caller should have same ordering relation in-bet
-                // callerLoc1 & callerLoc2
-
-                throw new Error("Caller doesn't respect ordering relations among method arguments:"
-                    + md.getClassDesc().getSourceFileName() + ":" + min.getNumLine());
+      // setup callee params set
+      // first, add callee's this location
+      calleeParamList.add(calleeThisLoc);
+      // second, add callee's parameters
+      for (int i = 0; i < calleemd.numParameters(); i++) {
+        VarDescriptor calleevd = (VarDescriptor) calleemd.getParameter(i);
+        CompositeLocation calleeLoc = d2loc.get(calleevd);
+        calleeParamList.add(calleeLoc);
+      }
+
+      // here, check if ordering relations among caller's args respect
+      // ordering relations in-between callee's args
+      for (int i = 0; i < calleeParamList.size(); i++) {
+        CompositeLocation calleeLoc1 = calleeParamList.get(i);
+        CompositeLocation callerLoc1 = callerArgList.get(i);
+
+        for (int j = 0; j < calleeParamList.size(); j++) {
+          if (i != j) {
+            CompositeLocation calleeLoc2 = calleeParamList.get(j);
+            CompositeLocation callerLoc2 = callerArgList.get(j);
+
+            int callerResult =
+                CompositeLattice.compare(callerLoc1, callerLoc2,
+                    generateErrorMessage(md.getClassDesc(), min));
+            int calleeResult =
+                CompositeLattice.compare(calleeLoc1, calleeLoc2,
+                    generateErrorMessage(md.getClassDesc(), min));
+
+            if (calleeResult == ComparisonResult.GREATER
+                && callerResult != ComparisonResult.GREATER) {
+              // If calleeLoc1 is higher than calleeLoc2
+              // then, caller should have same ordering relation in-bet
+              // callerLoc1 & callerLoc2
+
+              String paramName1, paramName2;
+
+              if (i == 0) {
+                paramName1 = "'THIS'";
+              } else {
+                paramName1 = "'parameter " + calleemd.getParamName(i - 1) + "'";
+              }
+
+              if (j == 0) {
+                paramName2 = "'THIS'";
+              } else {
+                paramName2 = "'parameter " + calleemd.getParamName(j - 1) + "'";
               }
 
+              throw new Error(
+                  "Caller doesn't respect an ordering relation among method arguments: callee expects that "
+                      + paramName1 + " should be higher than " + paramName2 + " at "
+                      + md.getClassDesc().getSourceFileName() + ":" + min.getNumLine());
             }
           }
-        }
 
+        }
       }
 
     }
@@ -1659,7 +1693,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