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

The developer can declare the program counter location as a composite location that  starts with the location type of the current object 'this'. It provides more specific constraints on value flows between fields in the current object.

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index a851b020e2125457c9b34f63f18e84fcda44d63a..2e879b18b0a18f32133f4bd509129704b16894f9 100644 (file)
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -6,7 +6,6 @@ import java.util.Comparator;
 import java.util.HashSet;
 import java.util.Hashtable;
 import java.util.Iterator;
-import java.util.LinkedList;
 import java.util.List;
 import java.util.Set;
 import java.util.StringTokenizer;
@@ -227,8 +226,7 @@ public class FlowDownCheck {
           if (state.SSJAVADEBUG) {
             System.out.println("SSJAVA: Checking Flow-down Rules: " + md);
           }
-          CompositeLocation calleePCLOC =
-              new CompositeLocation(new Location(md, ssjava.getMethodLattice(md).getPCLoc()));
+          CompositeLocation calleePCLOC = ssjava.getPCLocation(md);
           checkMethodBody(cd, md, calleePCLOC);
         }
       }
@@ -327,8 +325,8 @@ public class FlowDownCheck {
           String globalLoc = an.getValue();
           ssjava.getMethodLattice(md).setGlobalLoc(globalLoc);
         } else if (an.getMarker().equals(ssjava.PCLOC)) {
-          String pcLoc = an.getValue();
-          ssjava.getMethodLattice(md).setPCLoc(pcLoc);
+          String pcLocDeclaration = an.getValue();
+          ssjava.setPCLocation(md, parseLocationDeclaration(md, null, pcLocDeclaration));
         }
       }
     }
@@ -977,30 +975,35 @@ public class FlowDownCheck {
         // annotation that declares the program counter that is higher than
         // corresponding parameter
 
-        CompositeLocation calleePCLOC =
-            new CompositeLocation(new Location(calleemd, calleeLattice.getPCLoc()));
+        CompositeLocation calleePCLOC = ssjava.getPCLocation(calleemd);
 
         for (int idx = 0; idx < callerArgList.size(); idx++) {
           CompositeLocation argLocation = callerArgList.get(idx);
 
           int compareResult =
               CompositeLattice
-                  .compare(constraint, argLocation, true, generateErrorMessage(cd, min));
+                  .compare(argLocation, constraint, true, generateErrorMessage(cd, min));
 
           // need to check that param is higher than PCLOC
-          if (compareResult != ComparisonResult.GREATER) {
+          if (compareResult == ComparisonResult.GREATER) {
 
             CompositeLocation paramLocation = calleeParamList.get(idx);
 
             int paramCompareResult =
-                CompositeLattice.compare(paramLocation, calleePCLOC, true,
+                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 location " + argLocation
-                  + ". Need to specify that the initial PC location of the callee is lower than "
-                  + paramLocation + ":" + min.getNumLine());
+            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());
             }
 
           }

diff --git a/Robust/src/Analysis/SSJava/MethodLattice.java b/Robust/src/Analysis/SSJava/MethodLattice.java
index 1b04d77a7cd58daed522e3244dcbe266da36aafd..88eb7b70f17088c1b4754ce1b30b6c12ad742750 100644 (file)
--- a/Robust/src/Analysis/SSJava/MethodLattice.java
+++ b/Robust/src/Analysis/SSJava/MethodLattice.java
@@ -1,17 +1,13 @@
 package Analysis.SSJava;
 
-import IR.MethodDescriptor;
-
 public class MethodLattice<T> extends SSJavaLattice<T> {
 
   private T thisLoc;
   private T globalLoc;
   private T returnLoc;
-  private T pcLoc;
 
   public MethodLattice(T top, T bottom) {
     super(top, bottom);
-    pcLoc = top;
   }
 
   public void setThisLoc(T thisLoc) {
@@ -38,12 +34,4 @@ public class MethodLattice<T> extends SSJavaLattice<T> {
     return returnLoc;
   }
 
-  public T getPCLoc() {
-    return pcLoc;
-  }
-
-  public void setPCLoc(T pcLoc) {
-    this.pcLoc = pcLoc;
-  }
-
 }

diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
index 121e4cb5fb135c56122f1f6dfbf25f0fbf72f017..b18edaf4152f4120b13496f0cd8ea027eba4e300 100644 (file)
--- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
+++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
@@ -6,18 +6,19 @@ import java.io.IOException;
 import java.util.ArrayList;
 import java.util.Collections;
 import java.util.Comparator;
+import java.util.HashMap;
 import java.util.HashSet;
 import java.util.Hashtable;
 import java.util.Iterator;
 import java.util.LinkedList;
 import java.util.List;
+import java.util.Map;
 import java.util.Set;
 import java.util.StringTokenizer;
 import java.util.Vector;
 
 import Analysis.CallGraph.CallGraph;
 import Analysis.Loops.GlobalFieldType;
-import Analysis.Loops.LoopFinder;
 import Analysis.Loops.LoopOptimize;
 import Analysis.Loops.LoopTerminate;
 import IR.AnnotationDescriptor;
@@ -85,6 +86,9 @@ public class SSJavaAnalysis {
   // the set of method descriptors annotated as "TRUST"
   Set<MethodDescriptor> trustWorthyMDSet;
 
+  // method -> the initial program counter location
+  Map<MethodDescriptor, CompositeLocation> md2pcLoc;
+
   // points to method containing SSJAVA Loop
   private MethodDescriptor methodContainingSSJavaLoop;
 
@@ -124,6 +128,7 @@ public class SSJavaAnalysis {
     this.sameHeightWriteFlatNodeSet = new HashSet<FlatNode>();
     this.mapDescriptorToSetDependents = new Hashtable<Descriptor, Set<MethodDescriptor>>();
     this.sortedDescriptors = new LinkedList<MethodDescriptor>();
+    this.md2pcLoc = new HashMap<MethodDescriptor, CompositeLocation>();
   }
 
   public void doCheck() {
@@ -407,9 +412,6 @@ public class SSJavaAnalysis {
       } else if (orderElement.startsWith(RETURNLOC + "=")) {
         String returnLoc = orderElement.substring(10);
         locOrder.setReturnLoc(returnLoc);
-      } else if (orderElement.startsWith(PCLOC + "=")) {
-        String pcLoc = orderElement.substring(6);
-        locOrder.setPCLoc(pcLoc);
       } else if (orderElement.endsWith("*")) {
         // spin loc definition
         locOrder.addSharedLoc(orderElement.substring(0, orderElement.length() - 1));
@@ -504,6 +506,19 @@ public class SSJavaAnalysis {
     }
   }
 
+  public CompositeLocation getPCLocation(MethodDescriptor md) {
+    if (!md2pcLoc.containsKey(md)) {
+      // by default, the initial pc location is TOP
+      CompositeLocation pcLoc = new CompositeLocation(new Location(md, Location.TOP));
+      md2pcLoc.put(md, pcLoc);
+    }
+    return md2pcLoc.get(md);
+  }
+
+  public void setPCLocation(MethodDescriptor md, CompositeLocation pcLoc) {
+    md2pcLoc.put(md, pcLoc);
+  }
+
   public boolean needToCheckLinearType(MethodDescriptor md) {
     return linearTypeCheckMethodSet.contains(md);
   }