Allow to declare a composite location for the initial program counter location.

[IRC.git] / Robust / src / Analysis / SSJava / FlowDownCheck.java

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 45ceee7537df0f509f70b62a3ababa32bd803424..2e879b18b0a18f32133f4bd509129704b16894f9 100644 (file)
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -226,7 +226,8 @@ public class FlowDownCheck {
           if (state.SSJAVADEBUG) {
             System.out.println("SSJAVA: Checking Flow-down Rules: " + md);
           }
-          checkMethodBody(cd, md, null);
+          CompositeLocation calleePCLOC = ssjava.getPCLocation(md);
+          checkMethodBody(cd, md, calleePCLOC);
         }
       }
     }
@@ -320,6 +321,12 @@ public class FlowDownCheck {
         } else if (an.getMarker().equals(ssjava.THISLOC)) {
           String thisLoc = an.getValue();
           ssjava.getMethodLattice(md).setThisLoc(thisLoc);
+        } else if (an.getMarker().equals(ssjava.GLOBALLOC)) {
+          String globalLoc = an.getValue();
+          ssjava.getMethodLattice(md).setGlobalLoc(globalLoc);
+        } else if (an.getMarker().equals(ssjava.PCLOC)) {
+          String pcLocDeclaration = an.getValue();
+          ssjava.setPCLocation(md, parseLocationDeclaration(md, null, pcLocDeclaration));
         }
       }
     }
@@ -606,9 +613,13 @@ public class FlowDownCheck {
     } else {
       // check 'for loop' case
       BlockNode bn = ln.getInitializer();
-      // need to check initialization node
-      checkLocationFromBlockNode(md, nametable, bn, constraint);
       bn.getVarTable().setParent(nametable);
+      // need to check initialization node
+      // checkLocationFromBlockNode(md, bn.getVarTable(), bn, constraint);
+      for (int i = 0; i < bn.size(); i++) {
+        BlockStatementNode bsn = bn.get(i);
+        checkLocationFromBlockStatementNode(md, bn.getVarTable(), bsn, constraint);
+      }
 
       // calculate glb location of condition and update statements
       CompositeLocation condLoc =
@@ -732,11 +743,12 @@ public class FlowDownCheck {
 
   private void checkDeclarationInSubBlockNode(MethodDescriptor md, SymbolTable nametable,
       SubBlockNode sbn) {
-    checkDeclarationInBlockNode(md, nametable.getParent(), sbn.getBlockNode());
+    checkDeclarationInBlockNode(md, nametable, sbn.getBlockNode());
   }
 
   private CompositeLocation checkLocationFromBlockExpressionNode(MethodDescriptor md,
       SymbolTable nametable, BlockExpressionNode ben, CompositeLocation constraint) {
+
     CompositeLocation compLoc =
         checkLocationFromExpressionNode(md, nametable, ben.getExpression(), null, constraint, false);
     // addTypeLocation(ben.getExpression().getType(), compLoc);
@@ -925,19 +937,79 @@ public class FlowDownCheck {
       // min.printNode(0)
       // + " baseLocation=" + baseLocation + " constraint=" + constraint);
 
+      // setup the location list of caller's arguments
+      List<CompositeLocation> callerArgList = new ArrayList<CompositeLocation>();
+
+      if (min.numArgs() > 0) {
+        // setup caller args set
+        // first, add caller's base(this) location
+        callerArgList.add(baseLocation);
+        // second, add caller's arguments
+        for (int i = 0; i < min.numArgs(); i++) {
+          ExpressionNode en = min.getArg(i);
+          CompositeLocation callerArgLoc =
+              checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(),
+                  constraint, false);
+          callerArgList.add(callerArgLoc);
+        }
+      }
+
+      // setup the location list of callee's parameters
+      MethodDescriptor calleemd = min.getMethod();
+      MethodLattice<String> calleeLattice = ssjava.getMethodLattice(calleemd);
+      CompositeLocation calleeThisLoc =
+          new CompositeLocation(new Location(calleemd, calleeLattice.getThisLoc()));
+      List<CompositeLocation> calleeParamList = new ArrayList<CompositeLocation>();
+      // 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);
+      }
+
       if (constraint != null) {
-        int compareResult =
-            CompositeLattice.compare(constraint, baseLocation, true, generateErrorMessage(cd, min));
-        if (compareResult != ComparisonResult.GREATER) {
-          // if the current constraint is higher than method's THIS location
-          // no need to check constraints!
-          CompositeLocation calleeConstraint =
-              translateCallerLocToCalleeLoc(calleeMD, baseLocation, constraint);
-          // System.out.println("check method body for constraint:" + calleeMD +
-          // " calleeConstraint="
-          // + calleeConstraint);
-          checkMethodBody(calleeMD.getClassDesc(), calleeMD, calleeConstraint);
+        // check whether the PC location is lower than one of the
+        // argument locations. If it is lower, the callee has to have @PCLOC
+        // annotation that declares the program counter that is higher than
+        // corresponding parameter
+
+        CompositeLocation calleePCLOC = ssjava.getPCLocation(calleemd);
+
+        for (int idx = 0; idx < callerArgList.size(); idx++) {
+          CompositeLocation argLocation = callerArgList.get(idx);
+
+          int compareResult =
+              CompositeLattice
+                  .compare(argLocation, constraint, true, generateErrorMessage(cd, min));
+
+          // need to check that param is higher than PCLOC
+          if (compareResult == ComparisonResult.GREATER) {
+
+            CompositeLocation paramLocation = calleeParamList.get(idx);
+
+            int paramCompareResult =
+                CompositeLattice.compare(calleePCLOC, paramLocation, true,
+                    generateErrorMessage(cd, min));
+
+            if (paramCompareResult == ComparisonResult.GREATER) {
+              throw new Error(
+                  "The program counter location "
+                      + constraint
+                      + " is lower than the argument(idx="
+                      + idx
+                      + ") location "
+                      + argLocation
+                      + ". Need to specify that the initial PC location of the callee, which is currently set to "
+                      + calleePCLOC + ", is lower than " + paramLocation + " in the method "
+                      + calleeMD.getSymbol() + ":" + min.getNumLine());
+            }
+
+          }
+
         }
+
       }
 
       checkCalleeConstraints(md, nametable, min, baseLocation, constraint);