add PCLOC annotations. all three benchmarks are type-checked now.

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 2e879b18b0a18f32133f4bd509129704b16894f9..a16a6e9ff784ad5da0624a5a3d7a0c2e4d79e138 100644 (file)
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -903,7 +903,7 @@ public class FlowDownCheck {
       CompositeLocation constraint) {
 
     ClassDescriptor cd = md.getClassDesc();
-    MethodDescriptor calleeMD = min.getMethod();
+    MethodDescriptor calleeMethodDesc = min.getMethod();
 
     NameDescriptor baseName = min.getBaseName();
     boolean isSystemout = false;
@@ -911,8 +911,9 @@ public class FlowDownCheck {
       isSystemout = baseName.getSymbol().equals("System.out");
     }
 
-    if (!ssjava.isSSJavaUtil(calleeMD.getClassDesc()) && !ssjava.isTrustMethod(calleeMD)
-        && !calleeMD.getModifiers().isNative() && !isSystemout) {
+    if (!ssjava.isSSJavaUtil(calleeMethodDesc.getClassDesc())
+        && !ssjava.isTrustMethod(calleeMethodDesc) && !calleeMethodDesc.getModifiers().isNative()
+        && !isSystemout) {
 
       CompositeLocation baseLocation = null;
       if (min.getExpression() != null) {
@@ -940,11 +941,14 @@ public class FlowDownCheck {
       // setup the location list of caller's arguments
       List<CompositeLocation> callerArgList = new ArrayList<CompositeLocation>();
 
+      // setup the location list of callee's parameters
+      MethodLattice<String> calleeLattice = ssjava.getMethodLattice(calleeMethodDesc);
+      List<CompositeLocation> calleeParamList = 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
+        if (!calleeMethodDesc.isStatic()) {
+          callerArgList.add(baseLocation);
+        }
         for (int i = 0; i < min.numArgs(); i++) {
           ExpressionNode en = min.getArg(i);
           CompositeLocation callerArgLoc =
@@ -952,21 +956,18 @@ public class FlowDownCheck {
                   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 (!calleeMethodDesc.isStatic()) {
+          CompositeLocation calleeThisLoc =
+              new CompositeLocation(new Location(calleeMethodDesc, calleeLattice.getThisLoc()));
+          calleeParamList.add(calleeThisLoc);
+        }
+
+        for (int i = 0; i < calleeMethodDesc.numParameters(); i++) {
+          VarDescriptor calleevd = (VarDescriptor) calleeMethodDesc.getParameter(i);
+          CompositeLocation calleeLoc = d2loc.get(calleevd);
+          calleeParamList.add(calleeLoc);
+        }
       }
 
       if (constraint != null) {
@@ -975,17 +976,15 @@ public class FlowDownCheck {
         // annotation that declares the program counter that is higher than
         // corresponding parameter
 
-        CompositeLocation calleePCLOC = ssjava.getPCLocation(calleemd);
+        CompositeLocation calleePCLOC = ssjava.getPCLocation(calleeMethodDesc);
 
         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) {
+          if (!argLocation.get(0).isTop()
+              && CompositeLattice.compare(argLocation, constraint, true,
+                  generateErrorMessage(cd, min)) == ComparisonResult.GREATER) {
 
             CompositeLocation paramLocation = calleeParamList.get(idx);
 
@@ -1003,7 +1002,7 @@ public class FlowDownCheck {
                       + 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());
+                      + calleeMethodDesc.getSymbol() + ":" + min.getNumLine());
             }
 
           }

diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/Classifier.java b/Robust/src/Benchmarks/SSJava/EyeTracking/Classifier.java
index 87ada5b5eae8903520cbd4577ff56343b2038277..f5a3c6deba751655f6d1c181570b13522aa5c618 100644 (file)
--- a/Robust/src/Benchmarks/SSJava/EyeTracking/Classifier.java
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/Classifier.java
@@ -75,6 +75,7 @@ public class Classifier {
    * @return true if this region was classified as face, else false
    */
   @LATTICE("OUT<V,V<C,C<THIS,THIS<IN,C*,V*,THISLOC=THIS,RETURNLOC=OUT")
+  @PCLOC("THIS,Classifier.C")
   public boolean classifyFace(@LOC("THIS,Classifier.C") IntegralImageData image,
       @LOC("THIS,Classifier.C") float scaleFactor, @LOC("THIS,Classifier.C") int translationX,
       @LOC("THIS,Classifier.C") int translationY, @LOC("THIS,Classifier.C") float borderline) {

diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/ClassifierTree.java b/Robust/src/Benchmarks/SSJava/EyeTracking/ClassifierTree.java
index 68407754765f61cde443e12b0640557192aecf04..fa69d23518a887ea5c49c6272a7e52c9a4516002 100644 (file)
--- a/Robust/src/Benchmarks/SSJava/EyeTracking/ClassifierTree.java
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/ClassifierTree.java
@@ -1,3 +1,5 @@
+import SSJava.PCLOC;
+
 /*
  * Copyright 2009 (c) Florian Frankenberger (darkblue.de)
  * 
@@ -51,6 +53,7 @@ public class ClassifierTree {
    *         null if no face could be detected
    */
   @LATTICE("OUT<CXY,CXY<THIS,THIS<V,V<IMG,IMG<C,C<IN,C*,V*,FACTOR*,CXY*,THISLOC=THIS,RETURNLOC=OUT,GLOBALLOC=IN")
+  @PCLOC("C")
   public Rectangle2D locateFaceRadial(@LOC("IN") Image smallImage,
       @LOC("THIS,ClassifierTree.C") Rectangle2D lastCoordinates) {
 
@@ -181,7 +184,8 @@ public class ClassifierTree {
 
   }
 
-  @LATTICE("OUT<IN,OUT<THIS,THISLOC=THIS,RETURNLOC=OUT")
+  @LATTICE("OUT<IN,OUT<P,P<THIS,THISLOC=THIS,RETURNLOC=OUT")
+  @PCLOC("P")
   private static int sgn(@LOC("IN") float value) {
     return (value < 0 ? -1 : (value > 0 ? +1 : 1));
   }

diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/LEAImplementation.java b/Robust/src/Benchmarks/SSJava/EyeTracking/LEAImplementation.java
index e77c0e241abfdfa62b505bb5782f8e9063d0dd77..cf564ff1b0bf8e51f291ce4fc6b583d63910d224 100644 (file)
--- a/Robust/src/Benchmarks/SSJava/EyeTracking/LEAImplementation.java
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/LEAImplementation.java
@@ -37,6 +37,7 @@ public class LEAImplementation {
   }
 
   @LATTICE("OUT<V,V<THIS,THIS<IN,V*,THISLOC=THIS,RETURNLOC=OUT")
+  @PCLOC("THIS")
   public FaceAndEyePosition getEyePosition(@LOC("IN") Image image) {
     if (image == null)
       return null;
@@ -61,7 +62,8 @@ public class LEAImplementation {
     return new FaceAndEyePosition(lastRectangle, eyePosition);
   }
 
-  @LATTICE("OUT<IN,OUT<THIS,THISLOC=THIS,RETURNLOC=OUT")
+  @LATTICE("OUT<P,P<IN,OUT<THIS,THISLOC=THIS,RETURNLOC=OUT")
+  @PCLOC("P")
   private Point readEyes(@LOC("IN") Image image, @LOC("IN") Rectangle2D rect) {
     @LOC("OUT") EyeDetector ed = new EyeDetector(image, rect);
     return ed.detectEye();

diff --git a/Robust/src/Benchmarks/SSJava/MP3Decoder/BitReserve.java b/Robust/src/Benchmarks/SSJava/MP3Decoder/BitReserve.java
index 83ba5dfa4ed4c20e76de495c0b150c2aba4267c0..d6dc322fb8d86a5d5069395daa1ccc73e9bac2cd 100644 (file)
--- a/Robust/src/Benchmarks/SSJava/MP3Decoder/BitReserve.java
+++ b/Robust/src/Benchmarks/SSJava/MP3Decoder/BitReserve.java
@@ -85,6 +85,7 @@ final class BitReserve {
    * @param N\r
    *          the number of\r
    */\r
+  @PCLOC("THIS,BitReserve.BIT")\r
   public int hgetbits(@LOC("THIS,BitReserve.BIT") int N) {\r
 \r
     totbit += N;\r

diff --git a/Robust/src/Benchmarks/SSJava/MP3Decoder/Equalizer.java b/Robust/src/Benchmarks/SSJava/MP3Decoder/Equalizer.java
index 90182cc808e48a2254ddddef0d6ad59bac156a7c..f5aea8a68450021bda7f26359c85f5622cbe4747 100644 (file)
--- a/Robust/src/Benchmarks/SSJava/MP3Decoder/Equalizer.java
+++ b/Robust/src/Benchmarks/SSJava/MP3Decoder/Equalizer.java
@@ -173,6 +173,7 @@ public final class Equalizer {
    * \r
    */\r
   @RETURNLOC("C")\r
+  @PCLOC("C")\r
   float getBandFactor(@LOC("IN") float eq) {\r
     if (eq == BAND_NOT_PRESENT)\r
       return 0.0f;\r

diff --git a/Robust/src/Benchmarks/SSJava/MP3Decoder/LayerIIIDecoder.java b/Robust/src/Benchmarks/SSJava/MP3Decoder/LayerIIIDecoder.java
index a5546321ece1b529c4a4a9b7f8251cc2eb6cd601..02ff7476914c2683b2e4d5ffad9d3948d1e49b98 100644 (file)
--- a/Robust/src/Benchmarks/SSJava/MP3Decoder/LayerIIIDecoder.java
+++ b/Robust/src/Benchmarks/SSJava/MP3Decoder/LayerIIIDecoder.java
@@ -812,6 +812,7 @@ final class LayerIIIDecoder implements FrameDecoder {
         *
         */
   @LATTICE("THIS<IN,THISLOC=THIS,GLOBALLOC=IN")
+  @PCLOC("THIS,LayerIIIDecoder.SF15")
   private void get_scale_factors(@LOC("THIS,LayerIIIDecoder.SF1") Header header,
       @LOC("THIS,LayerIIIDecoder.SF1") int ch, @LOC("THIS,LayerIIIDecoder.SF1") int gr) {
 
@@ -926,6 +927,7 @@ final class LayerIIIDecoder implements FrameDecoder {
 
   // ssjava
   @LATTICE("M<THIS,THIS<IN,THIS<C,C*,M*,THISLOC=THIS,GLOBALLOC=THIS")
+  @PCLOC("THIS,LayerIIIDecoder.SI0")
   private void get_LSF_scale_data(@LOC("THIS,LayerIIIDecoder.SF15") Header header,
       @LOC("THIS,LayerIIIDecoder.SF15") int ch, @LOC("THIS,LayerIIIDecoder.SF15") int gr) {
 
@@ -1031,6 +1033,7 @@ final class LayerIIIDecoder implements FrameDecoder {
         *
         */
   @LATTICE("THIS<IN,THISLOC=THIS,GLOBALLOC=IN")
+  @PCLOC("THIS,LayerIIIDecoder.SF15")
   private void get_LSF_scale_factors(@LOC("THIS,LayerIIIDecoder.SF1") Header header,
       @LOC("THIS,LayerIIIDecoder.SF1") int ch, @LOC("THIS,LayerIIIDecoder.SF1") int gr) {
 
@@ -1223,6 +1226,7 @@ final class LayerIIIDecoder implements FrameDecoder {
   /**
         *
         */
+  @PCLOC("THIS,LayerIIIDecoder.LR")
   private void i_stereo_k_values(@LOC("THIS,LayerIIIDecoder.LR") int is_pos,
       @LOC("THIS,LayerIIIDecoder.LR") int io_type, @LOC("THIS,LayerIIIDecoder.LR") int i) {
     if (is_pos == 0) {

diff --git a/Robust/src/Benchmarks/SSJava/MP3Decoder/SideInfoBuffer.java b/Robust/src/Benchmarks/SSJava/MP3Decoder/SideInfoBuffer.java
index 6fef3fcf0ab5ef96a1ba1753042c4222d619b3ab..de4a54dd12926008ead0f687b50fd29b5f0def33 100644 (file)
--- a/Robust/src/Benchmarks/SSJava/MP3Decoder/SideInfoBuffer.java
+++ b/Robust/src/Benchmarks/SSJava/MP3Decoder/SideInfoBuffer.java
@@ -42,7 +42,8 @@ public class SideInfoBuffer {
       0x000000FF, 0x000001FF, 0x000003FF, 0x000007FF, 0x00000FFF, 0x00001FFF, 0x00003FFF,
       0x00007FFF, 0x0000FFFF, 0x0001FFFF };
 
-  @LATTICE("OUT<THIS,THIS<IN,OUT*,THISLOC=THIS,RETURNLOC=OUT")
+  @LATTICE("OUT<THIS,THIS<P,P<IN,OUT*,THISLOC=THIS,RETURNLOC=OUT")
+  @PCLOC("P")
   public int get_bits(@LOC("IN") int number_of_bits) {
     @LOC("OUT") int returnvalue = 0;
     @LOC("THIS,SideInfoBuffer.IDX") int sum = bitindex + number_of_bits;

diff --git a/Robust/src/Benchmarks/SSJava/MP3Decoder/huffcodetab.java b/Robust/src/Benchmarks/SSJava/MP3Decoder/huffcodetab.java
index 4442b8d20a2cba620c21a307ed56ef5c338b867b..ae59051bd203779f7c3c609cceb90712823dae91 100644 (file)
--- a/Robust/src/Benchmarks/SSJava/MP3Decoder/huffcodetab.java
+++ b/Robust/src/Benchmarks/SSJava/MP3Decoder/huffcodetab.java
@@ -508,6 +508,7 @@ final class huffcodetab {
    */\r
   @LATTICE("OUT<V1,THIS<V1,V1<V,V<IN,IN<C,C*,V*,THISLOC=THIS,GLOBALLOC=IN")\r
   @RETURNLOC("OUT,BitReserve.BIT")\r
+  @PCLOC("OUT,BitReserve.BIT")\r
   public static int huffman_decoder(@LOC("THIS,LayerIIIDecoder.SI2") int htIdx,\r
       @LOC("OUT,BitReserve.BIT") int[] x, @LOC("OUT,BitReserve.BIT") int[] y,\r
       @LOC("OUT,BitReserve.BIT") int[] v, @LOC("OUT,BitReserve.BIT") int[] w,\r

diff --git a/Robust/src/ClassLibrary/SSJava/Math.java b/Robust/src/ClassLibrary/SSJava/Math.java
index 3cb7eb104db07b246a266b5e44afedc4c881851c..355caf9b023fc72eb087ab47cdfcf72a01889276 100644 (file)
--- a/Robust/src/ClassLibrary/SSJava/Math.java
+++ b/Robust/src/ClassLibrary/SSJava/Math.java
@@ -53,6 +53,7 @@ public class Math {
   }
 
   @RETURNLOC("OUT")
+  @PCLOC("IN")
   public static int min(@LOC("IN") int a, @LOC("IN") int b) {
     return (a < b) ? a : b;
   }