changes.
authoryeom <yeom>
Sat, 23 Jul 2011 00:13:36 +0000 (00:13 +0000)
committeryeom <yeom>
Sat, 23 Jul 2011 00:13:36 +0000 (00:13 +0000)
Robust/src/Analysis/SSJava/FlowDownCheck.java
Robust/src/Analysis/SSJava/MethodLattice.java
Robust/src/Analysis/SSJava/SSJavaAnalysis.java
Robust/src/Tests/ssJava/mp3decoder/BitReserve.java

index 0a1752c..f113341 100644 (file)
@@ -11,7 +11,6 @@ import java.util.Set;
 import java.util.StringTokenizer;
 import java.util.Vector;
 
-
 import Analysis.SSJava.FlowDownCheck.ComparisonResult;
 import Analysis.SSJava.FlowDownCheck.CompositeLattice;
 import IR.AnnotationDescriptor;
@@ -222,6 +221,7 @@ public class FlowDownCheck {
       while (!toAnalyzeMethodIsEmpty()) {
         MethodDescriptor md = toAnalyzeMethodNext();
         if (ssjava.needTobeAnnotated(md)) {
+          System.out.println("SSJAVA: Checking assignments: " + md);
           checkMethodBody(cd, md);
         }
       }
@@ -292,10 +292,18 @@ public class FlowDownCheck {
   private void checkDeclarationInMethodBody(ClassDescriptor cd, MethodDescriptor md) {
     BlockNode bn = state.getMethodBody(md);
 
-    if (ssjava.needTobeAnnotated(md)) {
-      // first, check annotations on method declaration
+    // first, check annotations on method parameters
+    List<CompositeLocation> paramList = new ArrayList<CompositeLocation>();
+    for (int i = 0; i < md.numParameters(); i++) {
+      // process annotations on method parameters
+      VarDescriptor vd = (VarDescriptor) md.getParameter(i);
+      assignLocationOfVarDescriptor(vd, md, md.getParameterTable(), bn);
+      paramList.add(d2loc.get(vd));
+    }
 
-      // parsing returnloc annotation
+    // second, check return location annotation
+    if (!md.getReturnType().isVoid()) {
+      CompositeLocation returnLocComp = null;
       Vector<AnnotationDescriptor> methodAnnotations = md.getModifiers().getAnnotations();
       if (methodAnnotations != null) {
         for (int i = 0; i < methodAnnotations.size(); i++) {
@@ -303,47 +311,42 @@ public class FlowDownCheck {
           if (an.getMarker().equals(ssjava.RETURNLOC)) {
             // developer explicitly defines method lattice
             String returnLocDeclaration = an.getValue();
-            CompositeLocation returnLocComp =
-                parseLocationDeclaration(md, null, returnLocDeclaration);
+            returnLocComp = parseLocationDeclaration(md, null, returnLocDeclaration);
             md2ReturnLoc.put(md, returnLocComp);
           }
         }
-        if (!md.getReturnType().isVoid() && !md2ReturnLoc.containsKey(md)) {
-          throw new Error("Return location is not specified for the method " + md + " at "
-              + cd.getSourceFileName());
-        }
       }
-
-      List<CompositeLocation> paramList = new ArrayList<CompositeLocation>();
-
-      boolean hasReturnValue = (!md.getReturnType().isVoid());
-      if (hasReturnValue) {
-        MethodLattice<String> methodLattice = ssjava.getMethodLattice(md);
-        String thisLocId = methodLattice.getThisLoc();
-        if (thisLocId == null) {
-          throw new Error("Method '" + md + "' does not have the definition of 'this' location at "
-              + md.getClassDesc().getSourceFileName());
+      if (returnLocComp == null) {
+        MethodLattice<String> methodDefaultLattice = ssjava.getMethodDefaultLattice(cd);
+        if (methodDefaultLattice.getReturnLoc() != null) {
+          returnLocComp = parseLocationDeclaration(md, null, methodDefaultLattice.getReturnLoc());
+          md2ReturnLoc.put(md, returnLocComp);
         }
-        CompositeLocation thisLoc = new CompositeLocation(new Location(md, thisLocId));
-        paramList.add(thisLoc);
       }
 
-      for (int i = 0; i < md.numParameters(); i++) {
-        // process annotations on method parameters
-        VarDescriptor vd = (VarDescriptor) md.getParameter(i);
-        assignLocationOfVarDescriptor(vd, md, md.getParameterTable(), bn);
-        if (hasReturnValue) {
-          paramList.add(d2loc.get(vd));
-        }
+      if (!md2ReturnLoc.containsKey(md)) {
+        throw new Error("Return location is not specified for the method " + md + " at "
+            + cd.getSourceFileName());
       }
 
-      if (hasReturnValue) {
-        md2ReturnLocGen.put(md, new ReturnLocGenerator(md2ReturnLoc.get(md), paramList,
-            generateErrorMessage(cd, null)));
+      // check this location
+      MethodLattice<String> methodLattice = ssjava.getMethodLattice(md);
+      String thisLocId = methodLattice.getThisLoc();
+      if (thisLocId == null) {
+        throw new Error("Method '" + md + "' does not have the definition of 'this' location at "
+            + md.getClassDesc().getSourceFileName());
       }
-      checkDeclarationInBlockNode(md, md.getParameterTable(), bn);
+      CompositeLocation thisLoc = new CompositeLocation(new Location(md, thisLocId));
+      paramList.add(0, thisLoc);
+
+      md2ReturnLocGen.put(md, new ReturnLocGenerator(md2ReturnLoc.get(md), paramList,
+          generateErrorMessage(cd, null)));
     }
 
+    // third, check declarations inside of method
+
+    checkDeclarationInBlockNode(md, md.getParameterTable(), bn);
+
   }
 
   private void checkDeclarationInBlockNode(MethodDescriptor md, SymbolTable nametable, BlockNode bn) {
@@ -528,6 +531,15 @@ public class FlowDownCheck {
           checkLocationFromExpressionNode(md, nametable, returnExp, new CompositeLocation(),
               constraint, false);
 
+      // if this return statement is inside branch, return value has an implicit
+      // flow from conditional location
+      if (constraint != null) {
+        Set<CompositeLocation> inputGLB = new HashSet<CompositeLocation>();
+        inputGLB.add(returnValueLoc);
+        inputGLB.add(constraint);
+        returnValueLoc = CompositeLattice.calculateGLB(inputGLB);
+      }
+
       // check if return value is equal or higher than RETRUNLOC of method
       // declaration annotation
       CompositeLocation declaredReturnLoc = md2ReturnLoc.get(md);
index 095c736..88eb7b7 100644 (file)
@@ -4,6 +4,7 @@ public class MethodLattice<T> extends SSJavaLattice<T> {
 
   private T thisLoc;
   private T globalLoc;
+  private T returnLoc;
 
   public MethodLattice(T top, T bottom) {
     super(top, bottom);
@@ -25,4 +26,12 @@ public class MethodLattice<T> extends SSJavaLattice<T> {
     return globalLoc;
   }
 
+  public void setReturnLoc(T returnLoc) {
+    this.returnLoc = returnLoc;
+  }
+
+  public T getReturnLoc() {
+    return returnLoc;
+  }
+
 }
index 17db8a8..5e0d556 100644 (file)
@@ -88,8 +88,9 @@ public class SSJavaAnalysis {
     System.out.println("SSJAVA: SSJava is checking the following methods:");
     for (Iterator<MethodDescriptor> iterator = annotationRequireSet.iterator(); iterator.hasNext();) {
       MethodDescriptor md = iterator.next();
-      System.out.println("SSJAVA: " + md);
+      System.out.print(" " + md);
     }
+    System.out.println();
   }
 
   private void doMethodAnnotationCheck() {
@@ -131,7 +132,7 @@ public class SSJavaAnalysis {
           MethodLattice<String> locOrder =
               new MethodLattice<String>(SSJavaLattice.TOP, SSJavaLattice.BOTTOM);
           cd2methodDefault.put(cd, locOrder);
-          parseMethodLatticeDefinition(cd, an.getValue(), locOrder);
+          parseMethodDefaultLatticeDefinition(cd, an.getValue(), locOrder);
         }
       }
 
@@ -149,7 +150,7 @@ public class SSJavaAnalysis {
                 MethodLattice<String> locOrder =
                     new MethodLattice<String>(SSJavaLattice.TOP, SSJavaLattice.BOTTOM);
                 md2lattice.put(md, locOrder);
-                parseMethodLatticeDefinition(cd, an.getValue(), locOrder);
+                parseMethodDefaultLatticeDefinition(cd, an.getValue(), locOrder);
               } else if (an.getMarker().equals(TERMINATE)) {
                 // developer explicitly wants to skip loop termination analysis
                 String value = an.getValue();
@@ -169,7 +170,7 @@ public class SSJavaAnalysis {
     }
   }
 
-  private void parseMethodLatticeDefinition(ClassDescriptor cd, String value,
+  private void parseMethodDefaultLatticeDefinition(ClassDescriptor cd, String value,
       MethodLattice<String> locOrder) {
 
     value = value.replaceAll(" ", ""); // remove all blank spaces
@@ -193,6 +194,9 @@ public class SSJavaAnalysis {
       } else if (orderElement.startsWith(GLOBALLOC + "=")) {
         String globalLoc = orderElement.substring(10);
         locOrder.setGlobalLoc(globalLoc);
+      } else if (orderElement.startsWith(RETURNLOC + "=")) {
+        String returnLoc = orderElement.substring(10);
+        locOrder.setReturnLoc(returnLoc);
       } else if (orderElement.contains("*")) {
         // spin loc definition
         locOrder.addSpinLoc(orderElement.substring(0, orderElement.length() - 1));
index 3c907a7..4f55821 100644 (file)
  *   Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.\r
  *----------------------------------------------------------------------\r
  */\r
-       \r
+\r
 /**\r
  * Implementation of Bit Reservoir for Layer III.\r
  * <p>\r
- * The implementation stores single bits as a word in the buffer. If\r
- * a bit is set, the corresponding word in the buffer will be non-zero.\r
- * If a bit is clear, the corresponding word is zero. Although this\r
- * may seem waseful, this can be a factor of two quicker than \r
- * packing 8 bits to a byte and extracting. \r
- * <p> \r
+ * The implementation stores single bits as a word in the buffer. If a bit is\r
+ * set, the corresponding word in the buffer will be non-zero. If a bit is\r
+ * clear, the corresponding word is zero. Although this may seem waseful, this\r
+ * can be a factor of two quicker than packing 8 bits to a byte and extracting.\r
+ * <p>\r
  */\r
 \r
 // REVIEW: there is no range checking, so buffer underflow or overflow\r
 // can silently occur.\r
-@LATTICE("SH<V,V<T,TOT<OFF,OFF<T,SH*,TOT*,OFF*")\r
-@METHODDEFAULT("OUT<V,V<C,C<IN,C*,THISLOC=V,GLOBALLOC=V")\r
-final class BitReserve\r
-{\r
-   /**\r
-    * Size of the internal buffer to store the reserved bits.\r
-    * Must be a power of 2. And x8, as each bit is stored as a single\r
-    * entry.\r
-    */\r
-    @LOC("T") private static final int BUFSIZE = 4096*8;\r
-       \r
-       /**\r
-        * Mask that can be used to quickly implement the\r
-        * modulus operation on BUFSIZE.\r
-        */\r
-    @LOC("V") private static final int BUFSIZE_MASK = BUFSIZE-1;\r
-       \r
-    @LOC("OFF") private int offset;\r
-    @LOC("TOT") private int totbit;\r
-    @LOC("SH") private int buf_byte_idx;\r
-    @LOC("V") private final int[] buf;\r
-    @LOC("T") private int buf_bit_idx;\r
-       \r
-   BitReserve()\r
-   {     \r
+@LATTICE("BUF<OFF,BIT,BIT*,OFF*")\r
+@METHODDEFAULT("OUT<THIS,THIS<IN,IN*,THISLOC=THIS,RETURNLOC=OUT")\r
+final class BitReserve {\r
+  /**\r
+   * Size of the internal buffer to store the reserved bits. Must be a power of\r
+   * 2. And x8, as each bit is stored as a single entry.\r
+   */\r
+  private static final int BUFSIZE = 4096 * 8;\r
+\r
+  /**\r
+   * Mask that can be used to quickly implement the modulus operation on\r
+   * BUFSIZE.\r
+   */\r
+  private static final int BUFSIZE_MASK = BUFSIZE - 1;\r
+\r
+  @LOC("OFF")\r
+  private int offset;\r
+\r
+  @LOC("BIT")\r
+  private int totbit;\r
+\r
+  @LOC("BIT")\r
+  private int buf_byte_idx;\r
+\r
+  @LOC("BUF")\r
+  private final int[] buf;\r
+\r
+  BitReserve() {\r
+    offset = 0;\r
+    totbit = 0;\r
+    buf_byte_idx = 0;\r
+    buf = new int[BUFSIZE];\r
+  }\r
+\r
+  /**\r
+   * Return totbit Field.\r
+   */\r
+\r
+  public int hsstell() {\r
+    return (totbit);\r
+  }\r
+\r
+  /**\r
+   * Read a number bits from the bit stream.\r
+   * \r
+   * @param N\r
+   *          the number of\r
+   */\r
+  public int hgetbits(@LOC("THIS,BitReserve.BIT") int N) {\r
+\r
+    totbit += N;\r
+\r
+    @LOC("OUT") int val = 0;\r
+\r
+    @LOC("THIS,BitReserve.BIT") int pos = buf_byte_idx;\r
+    if (pos + N < BUFSIZE) {\r
+      while (N-- > 0) {\r
+        val <<= 1;\r
+        val |= ((buf[pos++] != 0) ? 1 : 0);\r
+      }\r
+    } else {\r
+      while (N-- > 0) {\r
+        val <<= 1;\r
+        val |= ((buf[pos] != 0) ? 1 : 0);\r
+        pos = (pos + 1) & BUFSIZE_MASK;\r
+      }\r
+    }\r
+\r
+    buf_byte_idx = pos;\r
+\r
+    return val;\r
+\r
+  }\r
+\r
+  /**\r
+   * Returns next bit from reserve.\r
+   * \r
+   * @returns 0 if next bit is reset, or 1 if next bit is set.\r
+   */\r
+  public int hget1bit() {\r
+    totbit++;\r
+    @LOC("OUT") int val = buf[buf_byte_idx];\r
+    buf_byte_idx = (buf_byte_idx + 1) & BUFSIZE_MASK;\r
+    return val;\r
+  }\r
+\r
+  /**\r
+   * Write 8 bits into the bit stream.\r
+   */\r
+  @LATTICE("OUT<THIS,THIS<IN,THISLOC=THIS,GLOBALLOC=IN")\r
+  public void hputbuf(@LOC("IN") int val) {\r
+    @LOC("THIS,BitReserve.OFF") int ofs = offset;\r
+    buf[ofs++] = val & 0x80;\r
+    buf[ofs++] = val & 0x40;\r
+    buf[ofs++] = val & 0x20;\r
+    buf[ofs++] = val & 0x10;\r
+    buf[ofs++] = val & 0x08;\r
+    buf[ofs++] = val & 0x04;\r
+    buf[ofs++] = val & 0x02;\r
+    buf[ofs++] = val & 0x01;\r
+\r
+    if (ofs == BUFSIZE)\r
       offset = 0;\r
-      totbit = 0;\r
-      buf_byte_idx = 0;\r
-      buf = new int[BUFSIZE];\r
-   }\r
-      \r
-   \r
-   /**\r
-    * Return totbit Field.\r
-       */\r
-\r
-   @RETURNLOC("OUT")\r
-   public int hsstell() \r
-   { \r
-          return(totbit); \r
-   }\r
-\r
-   /**\r
-    * Read a number bits from the bit stream.\r
-    * @param N the number of\r
-       */\r
-   @LATTICE("OUT<SH,SH<THIS,THIS<C,C<GLOBAL,C*,SH*,THISLOC=THIS,GLOBALLOC=GLOBAL")\r
-   @RETURNLOC("OUT") \r
-   public int hgetbits(@LOC("C") int N)\r
-   {\r
-        totbit += N;\r
-        \r
-        @LOC("SH") int val = 0;\r
-        \r
-        @LOC("THIS,BitReserve.SH") int pos = buf_byte_idx;\r
-        if (pos+N < BUFSIZE)\r
-        {\r
-               while (N-- > 0)\r
-               {\r
-                       val <<= 1;\r
-                       val |= ((buf[pos++]!=0) ? 1 : 0);                \r
-               }\r
-       }\r
-        else\r
-        {       \r
-                while (N-- > 0)\r
-               {\r
-                        val <<= 1;                      \r
-                        val |= ((buf[pos]!=0) ? 1 : 0);\r
-                        pos = (pos+1) & BUFSIZE_MASK;\r
-               }                \r
-        }      \r
-        buf_byte_idx = pos;\r
-        return val;\r
-   }\r
-   \r
-        \r
-   \r
-   /**\r
-    * Read 1 bit from the bit stream.\r
-       */\r
-/*\r
-   public int hget1bit_old()\r
-   {\r
-         int val;\r
-         totbit++;\r
-         if (buf_bit_idx == 0)\r
-         {\r
-         buf_bit_idx = 8;\r
-            buf_byte_idx++;             \r
-         }\r
-      // BUFSIZE = 4096 = 2^12, so\r
-      // buf_byte_idx%BUFSIZE == buf_byte_idx & 0xfff\r
-      val = buf[buf_byte_idx & BUFSIZE_MASK] & putmask[buf_bit_idx];\r
-      buf_bit_idx--;\r
-         val = val >>> buf_bit_idx;\r
-      return val;   \r
-   }\r
- */\r
-   /**\r
-    * Returns next bit from reserve.\r
-    * @returns 0 if next bit is reset, or 1 if next bit is set.\r
-    */\r
-   @RETURNLOC("OUT")\r
-   public int hget1bit()\r
-   {             \r
-      totbit++;          \r
-      @LOC("OUT") int val = buf[buf_byte_idx];\r
-      buf_byte_idx = (buf_byte_idx+1) & BUFSIZE_MASK;\r
-      return val;\r
-   }\r
-   \r
-   /**\r
-    * Retrieves bits from the reserve.     \r
-    */\r
-/*   \r
-   public int readBits(int[] out, int len)\r
-   {\r
-               if (buf_bit_idx == 0)\r
-               {\r
-                  buf_bit_idx = 8;\r
-                  buf_byte_idx++;\r
-                  current = buf[buf_byte_idx & BUFSIZE_MASK];\r
-               }      \r
-               \r
-               \r
-               \r
-               // save total number of bits returned\r
-               len = buf_bit_idx;\r
-               buf_bit_idx = 0;\r
-                 \r
-               int b = current;\r
-               int count = len-1;\r
-                 \r
-               while (count >= 0)\r
-               {\r
-                   out[count--] = (b & 0x1);\r
-                   b >>>= 1;\r
-               }\r
-         \r
-               totbit += len;\r
-               return len;\r
-   }\r
-  */\r
-   \r
-   /**\r
-    * Write 8 bits into the bit stream.\r
-       */\r
-   @LATTICE("OUT<THIS,THIS<IN,THISLOC=THIS,GLOBALLOC=IN")\r
-   public void hputbuf(@LOC("IN") int val)\r
-   {             \r
-           @LOC("THIS,BitReserve.OFF") int ofs = offset;\r
-          buf[ofs++] = val & 0x80;\r
-          buf[ofs++] = val & 0x40;\r
-          buf[ofs++] = val & 0x20;\r
-          buf[ofs++] = val & 0x10;\r
-          buf[ofs++] = val & 0x08;\r
-          buf[ofs++] = val & 0x04;\r
-          buf[ofs++] = val & 0x02;\r
-          buf[ofs++] = val & 0x01;\r
-          \r
-          if (ofs==BUFSIZE)\r
-                       offset = 0;\r
-          else\r
-                       offset = ofs;\r
-          \r
-   }\r
\r
-   /**\r
-    * Rewind N bits in Stream.\r
-       */\r
-   public void rewindNbits(@LOC("IN") int N)\r
-   {\r
-         totbit -= N;            \r
-         buf_byte_idx -= N;\r
-         if (buf_byte_idx<0)\r
-                 buf_byte_idx += BUFSIZE;\r
-   }\r
-       \r
-   /**\r
-    * Rewind N bytes in Stream.\r
-       */\r
-   @LATTICE("THIS<BIT,BIT<N,THISLOC=THIS,GLOBALLOC=N")\r
-   public void rewindNbytes(@LOC("N") int N)\r
-   {\r
-          @LOC("BIT") int bits = (N << 3);\r
-         totbit -= bits;\r
-         buf_byte_idx -= bits;   \r
-         if (buf_byte_idx<0)\r
-                 buf_byte_idx += BUFSIZE;\r
-   }\r
+    else\r
+      offset = ofs;\r
+\r
+  }\r
+\r
+  /**\r
+   * Rewind N bits in Stream.\r
+   */\r
+  public void rewindNbits(@LOC("IN") int N) {\r
+    totbit -= N;\r
+    buf_byte_idx -= N;\r
+    if (buf_byte_idx < 0)\r
+      buf_byte_idx += BUFSIZE;\r
+  }\r
+\r
+  /**\r
+   * Rewind N bytes in Stream.\r
+   */\r
+  @LATTICE("THIS<BIT,BIT<N,THISLOC=THIS,GLOBALLOC=N")\r
+  public void rewindNbytes(@LOC("N") int N) {\r
+    @LOC("BIT") int bits = (N << 3);\r
+    totbit -= bits;\r
+    buf_byte_idx -= bits;\r
+    if (buf_byte_idx < 0)\r
+      buf_byte_idx += BUFSIZE;\r
+  }\r
 }\r