From 338b40f8f52cf09dc5fcef67796acc65a69758b9 Mon Sep 17 00:00:00 2001
From: yeom <yeom>
Date: Thu, 2 Aug 2012 00:48:32 +0000
Subject: [PATCH] add PCLOC annotations. all three benchmarks are type-checked
 now.

---
 Robust/src/Analysis/SSJava/FlowDownCheck.java | 55 +++++++++----------
 .../SSJava/EyeTracking/Classifier.java        |  1 +
 .../SSJava/EyeTracking/ClassifierTree.java    |  6 +-
 .../SSJava/EyeTracking/LEAImplementation.java |  4 +-
 .../SSJava/MP3Decoder/BitReserve.java         |  1 +
 .../SSJava/MP3Decoder/Equalizer.java          |  1 +
 .../SSJava/MP3Decoder/LayerIIIDecoder.java    |  4 ++
 .../SSJava/MP3Decoder/SideInfoBuffer.java     |  3 +-
 .../SSJava/MP3Decoder/huffcodetab.java        |  1 +
 Robust/src/ClassLibrary/SSJava/Math.java      |  1 +
 10 files changed, 46 insertions(+), 31 deletions(-)

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 2e879b18..a16a6e9f 100644
--- 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 87ada5b5..f5a3c6de 100644
--- 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 68407754..fa69d235 100644
--- 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 e77c0e24..cf564ff1 100644
--- 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 83ba5dfa..d6dc322f 100644
--- 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
    *          the number of
    */
+  @PCLOC("THIS,BitReserve.BIT")
   public int hgetbits(@LOC("THIS,BitReserve.BIT") int N) {
 
     totbit += N;
diff --git a/Robust/src/Benchmarks/SSJava/MP3Decoder/Equalizer.java b/Robust/src/Benchmarks/SSJava/MP3Decoder/Equalizer.java
index 90182cc8..f5aea8a6 100644
--- a/Robust/src/Benchmarks/SSJava/MP3Decoder/Equalizer.java
+++ b/Robust/src/Benchmarks/SSJava/MP3Decoder/Equalizer.java
@@ -173,6 +173,7 @@ public final class Equalizer {
    * 
    */
   @RETURNLOC("C")
+  @PCLOC("C")
   float getBandFactor(@LOC("IN") float eq) {
     if (eq == BAND_NOT_PRESENT)
       return 0.0f;
diff --git a/Robust/src/Benchmarks/SSJava/MP3Decoder/LayerIIIDecoder.java b/Robust/src/Benchmarks/SSJava/MP3Decoder/LayerIIIDecoder.java
index a5546321..02ff7476 100644
--- 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 6fef3fcf..de4a54dd 100644
--- 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 4442b8d2..ae59051b 100644
--- a/Robust/src/Benchmarks/SSJava/MP3Decoder/huffcodetab.java
+++ b/Robust/src/Benchmarks/SSJava/MP3Decoder/huffcodetab.java
@@ -508,6 +508,7 @@ final class huffcodetab {
    */
   @LATTICE("OUT<V1,THIS<V1,V1<V,V<IN,IN<C,C*,V*,THISLOC=THIS,GLOBALLOC=IN")
   @RETURNLOC("OUT,BitReserve.BIT")
+  @PCLOC("OUT,BitReserve.BIT")
   public static int huffman_decoder(@LOC("THIS,LayerIIIDecoder.SI2") int htIdx,
       @LOC("OUT,BitReserve.BIT") int[] x, @LOC("OUT,BitReserve.BIT") int[] y,
       @LOC("OUT,BitReserve.BIT") int[] v, @LOC("OUT,BitReserve.BIT") int[] w,
diff --git a/Robust/src/ClassLibrary/SSJava/Math.java b/Robust/src/ClassLibrary/SSJava/Math.java
index 3cb7eb10..355caf9b 100644
--- 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;
   }
-- 
2.34.1