mp3decoder passes the loop termination analysis.

diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
index a9f2e85853148123b2982b62790ee8a8cf952fa4..70944c9c6f284ae8e5db53600a8cc3d721572283 100644 (file)
--- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
+++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
@@ -3,14 +3,19 @@ package Analysis.SSJava;
 import java.io.BufferedWriter;
 import java.io.FileWriter;
 import java.io.IOException;
+import java.util.ArrayList;
+import java.util.Collections;
+import java.util.Comparator;
 import java.util.HashSet;
 import java.util.Hashtable;
 import java.util.Iterator;
+import java.util.List;
 import java.util.Set;
 import java.util.StringTokenizer;
 import java.util.Vector;
 
 import Analysis.CallGraph.CallGraph;
+import Analysis.Loops.GlobalFieldType;
 import Analysis.Loops.LoopOptimize;
 import Analysis.Loops.LoopTerminate;
 import IR.AnnotationDescriptor;
@@ -18,6 +23,7 @@ import IR.ClassDescriptor;
 import IR.Descriptor;
 import IR.MethodDescriptor;
 import IR.State;
+import IR.SymbolTable;
 import IR.TypeUtil;
 import IR.Flat.BuildFlat;
 import IR.Flat.FlatMethod;
@@ -92,7 +98,7 @@ public class SSJavaAnalysis {
   }
 
   public void doCheck() {
-     doMethodAnnotationCheck();
+    doMethodAnnotationCheck();
     // computeLinearTypeCheckMethodSet();
     // doLinearTypeCheck();
     // if (state.SSJAVADEBUG) {
@@ -101,6 +107,47 @@ public class SSJavaAnalysis {
     // parseLocationAnnotation();
     // doFlowDownCheck();
     // doDefinitelyWrittenCheck();
+    debugDoLoopCheck();
+  }
+
+  private void debugDoLoopCheck() {
+    GlobalFieldType gft = new GlobalFieldType(callgraph, state, tu.getMain());
+    LoopOptimize lo = new LoopOptimize(gft, tu);
+
+    SymbolTable classtable = state.getClassSymbolTable();
+
+    List<ClassDescriptor> toanalyzeList = new ArrayList<ClassDescriptor>();
+    List<MethodDescriptor> toanalyzeMethodList = new ArrayList<MethodDescriptor>();
+
+    toanalyzeList.addAll(classtable.getValueSet());
+    Collections.sort(toanalyzeList, new Comparator<ClassDescriptor>() {
+      public int compare(ClassDescriptor o1, ClassDescriptor o2) {
+        return o1.getClassName().compareTo(o2.getClassName());
+      }
+    });
+
+    for (int i = 0; i < toanalyzeList.size(); i++) {
+      ClassDescriptor cd = toanalyzeList.get(i);
+
+      SymbolTable methodtable = cd.getMethodTable();
+      toanalyzeMethodList.clear();
+      toanalyzeMethodList.addAll(methodtable.getValueSet());
+      Collections.sort(toanalyzeMethodList, new Comparator<MethodDescriptor>() {
+        public int compare(MethodDescriptor o1, MethodDescriptor o2) {
+          return o1.getSymbol().compareTo(o2.getSymbol());
+        }
+      });
+
+      for (int mdIdx = 0; mdIdx < toanalyzeMethodList.size(); mdIdx++) {
+        MethodDescriptor md = toanalyzeMethodList.get(mdIdx);
+        if (needTobeAnnotated(md)) {
+          lo.analyze(state.getMethodFlat(md));
+          doLoopTerminationCheck(lo, state.getMethodFlat(md));
+        }
+      }
+
+    }
+
   }
 
   public void addTrustMethod(MethodDescriptor md) {
@@ -409,7 +456,7 @@ public class SSJavaAnalysis {
   }
 
   public void doLoopTerminationCheck(LoopOptimize lo, FlatMethod fm) {
-    LoopTerminate lt = new LoopTerminate(this,state);
+    LoopTerminate lt = new LoopTerminate(this, state);
     if (needTobeAnnotated(fm.getMethod())) {
       lt.terminateAnalysis(fm, lo.getLoopInvariant(fm));
     }

diff --git a/Robust/src/ClassLibrary/SSJava/String.java b/Robust/src/ClassLibrary/SSJava/String.java
index 4734915fc9ae86aff15900076d239753e07c88ba..5f963399aa7367339848f523a3b73cad3d2c4c67 100644 (file)
--- a/Robust/src/ClassLibrary/SSJava/String.java
+++ b/Robust/src/ClassLibrary/SSJava/String.java
@@ -323,6 +323,7 @@ public class String {
       tmp = -x;
     else
       tmp = x;
+    TERMINATE:
     do {
       tmp = tmp / 10;
       length = length + 1;
@@ -341,6 +342,7 @@ public class String {
     } else
       voffset = 0;
 
+    TERMINATE:
     do {
       chararray[--length + voffset] = (char) (x % 10 + '0');
       x = x / 10;
@@ -366,6 +368,8 @@ public class String {
       tmp = -x;
     else
       tmp = x;
+    
+    TERMINATE:
     do {
       tmp = tmp / 10;
       length = length + 1;
@@ -384,6 +388,7 @@ public class String {
     } else
       voffset = 0;
 
+    TERMINATE:
     do {
       chararray[--length + voffset] = (char) (x % 10 + '0');
       x = x / 10;

diff --git a/Robust/src/Tests/ssJava/mp3decoder/BitReserve.java b/Robust/src/Tests/ssJava/mp3decoder/BitReserve.java
index e4167f00b0048a7c334801c46521dfba40f69068..15f4a068c2f5058091e0a1fa8f0c3e49aebe70f6 100644 (file)
--- a/Robust/src/Tests/ssJava/mp3decoder/BitReserve.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/BitReserve.java
@@ -93,11 +93,13 @@ final class BitReserve {
 \r
     @LOC("THIS,BitReserve.BIT") int pos = buf_byte_idx;\r
     if (pos + N < BUFSIZE) {\r
+      TERMINATE:\r
       while (N-- > 0) {\r
         val <<= 1;\r
         val |= ((buf[pos++] != 0) ? 1 : 0);\r
       }\r
     } else {\r
+      TERMINATE:\r
       while (N-- > 0) {\r
         val <<= 1;\r
         val |= ((buf[pos] != 0) ? 1 : 0);\r

diff --git a/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java b/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java
index cd0d38e6021b7af49bf8c92242afe1a7d8db3cbe..31cd7a1c6e4c96703a3642147e22bd5c83adc60b 100644 (file)
--- a/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java
@@ -948,7 +948,8 @@ final class LayerIIIDecoder implements FrameDecoder {
 
     m = 0;
     for (@LOC("THIS,LayerIIIDecoder.NS") int i = 0; i < 4; i++) {
-      for (@LOC("THIS,LayerIIIDecoder.NS") int j = 0; j < nr_of_sfb_block[blocknumber][blocktypenumber][i]; j++) {
+      int jmax=nr_of_sfb_block[blocknumber][blocktypenumber][i];
+      for (@LOC("THIS,LayerIIIDecoder.NS") int j = 0; j < jmax; j++) {
         scalefac_buffer[m] = (new_slen[i] == 0) ? 0 : br.hgetbits(new_slen[i]);
         m++;
 
@@ -1071,6 +1072,7 @@ final class LayerIIIDecoder implements FrameDecoder {
 
     index = 0;
     // Read bigvalues area
+    TERMINATE:
     for (@LOC("THIS,LayerIIIDecoder.BR,BitReserve.BIT") int i = 0; i < (si.ch[ch].gr[gr].big_values << 1); i +=
         2) {
 
@@ -1103,6 +1105,7 @@ final class LayerIIIDecoder implements FrameDecoder {
     // h = huffcodetab.ht[si.ch[ch].gr[gr].count1table_select + 32];
     num_bits = br.hsstell();
 
+    TERMINATE:
     while ((num_bits < part2_3_end) && (index < 576)) {
 
       huffcodetab.huffman_decoder(htIdx, x, y, v, w, br);
@@ -1497,11 +1500,12 @@ final class LayerIIIDecoder implements FrameDecoder {
             for (@LOC("THIS,LayerIIIDecoder.RO1") int j = 0; j < 3; j++) {
               @LOC("THIS,LayerIIIDecoder.RO1") int sfbcnt;
               sfbcnt = 2;
+              TERMINATE:
               for (sfb = 12; sfb >= 3; sfb--) {
                 i = sfBandIndex[sfreq].s[sfb];
                 lines = sfBandIndex[sfreq].s[sfb + 1] - i;
                 i = (i << 2) - i + (j + 1) * lines - 1;
-
+                TERMINATE:
                 while (lines > 0) {
                   if (ro[1][i / 18][i % 18] != 0.0f) {
                     // MDM: in java, array access is very slow.
@@ -1528,6 +1532,7 @@ final class LayerIIIDecoder implements FrameDecoder {
                 sb = sfBandIndex[sfreq].s[sfb + 1] - temp;
                 i = (temp << 2) - temp + j * sb;
 
+                TERMINATE:
                 for (; sb > 0; sb--) {
                   is_pos[i] = scalefac[1].s[j][sfb];
                   if (is_pos[i] != 7)
@@ -1546,7 +1551,7 @@ final class LayerIIIDecoder implements FrameDecoder {
               temp = sfBandIndex[sfreq].s[11];
               sb = sfBandIndex[sfreq].s[12] - temp;
               i = (temp << 2) - temp + j * sb;
-
+              TERMINATE:
               for (; sb > 0; sb--) {
                 is_pos[i] = is_pos[sfb];
 
@@ -1563,6 +1568,7 @@ final class LayerIIIDecoder implements FrameDecoder {
               i = 2;
               ss = 17;
               sb = -1;
+              TERMINATE:
               while (i >= 0) {
                 if (ro[1][i][ss] != 0.0f) {
                   sb = (i << 4) + (i << 1) + ss;
@@ -1582,6 +1588,7 @@ final class LayerIIIDecoder implements FrameDecoder {
               i = sfBandIndex[sfreq].l[i];
               for (; sfb < 8; sfb++) {
                 sb = sfBandIndex[sfreq].l[sfb + 1] - sfBandIndex[sfreq].l[sfb];
+                TERMINATE:
                 for (; sb > 0; sb--) {
                   is_pos[i] = scalefac[1].l[sfb];
                   if (is_pos[i] != 7)
@@ -1597,11 +1604,12 @@ final class LayerIIIDecoder implements FrameDecoder {
             for (@LOC("THIS,LayerIIIDecoder.RO1") int j = 0; j < 3; j++) {
               @LOC("THIS,LayerIIIDecoder.RO1") int sfbcnt;
               sfbcnt = -1;
+              TERMINATE:
               for (sfb = 12; sfb >= 0; sfb--) {
                 temp = sfBandIndex[sfreq].s[sfb];
                 lines = sfBandIndex[sfreq].s[sfb + 1] - temp;
                 i = (temp << 2) - temp + (j + 1) * lines - 1;
-
+                TERMINATE:
                 while (lines > 0) {
                   if (ro[1][i / 18][i % 18] != 0.0f) {
                     // MDM: in java, array access is very slow.
@@ -1621,6 +1629,7 @@ final class LayerIIIDecoder implements FrameDecoder {
                 temp = sfBandIndex[sfreq].s[sfb];
                 sb = sfBandIndex[sfreq].s[sfb + 1] - temp;
                 i = (temp << 2) - temp + j * sb;
+                TERMINATE:
                 for (; sb > 0; sb--) {
                   is_pos[i] = scalefac[1].s[j][sfb];
                   if (is_pos[i] != 7)
@@ -1639,7 +1648,7 @@ final class LayerIIIDecoder implements FrameDecoder {
               sfb = (temp << 2) - temp + j * sb;
               sb = sfBandIndex[sfreq].s[12] - temp2;
               i = (temp2 << 2) - temp2 + j * sb;
-
+              TERMINATE:
               for (; sb > 0; sb--) {
                 is_pos[i] = is_pos[sfb];
 
@@ -1657,6 +1666,7 @@ final class LayerIIIDecoder implements FrameDecoder {
           i = 31;
           ss = 17;
           sb = 0;
+          TERMINATE:
           while (i >= 0) {
             if (ro[1][i][ss] != 0.0f) {
               sb = (i << 4) + (i << 1) + ss;
@@ -1677,6 +1687,7 @@ final class LayerIIIDecoder implements FrameDecoder {
           i = sfBandIndex[sfreq].l[i];
           for (; sfb < 21; sfb++) {
             sb = sfBandIndex[sfreq].l[sfb + 1] - sfBandIndex[sfreq].l[sfb];
+            TERMINATE:
             for (; sb > 0; sb--) {
               is_pos[i] = scalefac[1].l[sfb];
               if (is_pos[i] != 7)
@@ -1688,6 +1699,7 @@ final class LayerIIIDecoder implements FrameDecoder {
             }
           }
           sfb = sfBandIndex[sfreq].l[20];
+          TERMINATE:
           for (sb = 576 - sfBandIndex[sfreq].l[21]; (sb > 0) && (i < 576); sb--) {
             is_pos[i] = is_pos[sfb]; // error here : i >=576
 

diff --git a/Robust/src/Tests/ssJava/mp3decoder/Player.java b/Robust/src/Tests/ssJava/mp3decoder/Player.java
index 83851e297c749ae17143de3d8aed154414a871f5..2e2b02cd0e7d8cf975b21489a1a6bb27ed0144b0 100644 (file)
--- a/Robust/src/Tests/ssJava/mp3decoder/Player.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/Player.java
@@ -111,9 +111,14 @@ public class Player {
   @RETURNLOC("T")\r
   public boolean play(@LOC("IN") int frames) throws JavaLayerException {\r
     @LOC("T") boolean ret = true;\r
-\r
-    SSJAVA: while (frames-- > 0 && ret) {\r
+    \r
+    int maxFrame=frames-1;\r
+    int count=0;\r
+    SSJAVA: while (count++ < maxFrame) {\r
       ret = decodeFrame();\r
+      if(!ret){\r
+          break;\r
+      }\r
     }\r
 \r
     /*\r
@@ -190,6 +195,7 @@ public class Player {
       @LOC("C") int sum = 0;\r
       @LOC("C") short[] outbuf = SampleBufferWrapper.getBuffer();\r
       // short[] outbuf = output.getBuffer();\r
+      TERMINATE:\r
       for (@LOC("C") int i = 0; i < SampleBufferWrapper.getBufferLength(); i++) {\r
         // System.out.println(outbuf[i]);\r
         sum += outbuf[i];\r

diff --git a/Robust/src/Tests/ssJava/mp3decoder/SynthesisFilter.java b/Robust/src/Tests/ssJava/mp3decoder/SynthesisFilter.java
index bc86eb80a14b881b6a3ed703014e1a58c73622c1..0882baccb16f5cdaecbb7f02715725c3679eeb68 100644 (file)
--- a/Robust/src/Tests/ssJava/mp3decoder/SynthesisFilter.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/SynthesisFilter.java
@@ -125,6 +125,7 @@ final class SynthesisFilter {
   }\r
 \r
   public void input_samples(@LOC("IN") float[] s) {\r
+    TERMINATE:\r
     for (@LOC("C") int i = 31; i >= 0; i--) {\r
       samples[i] = s[i] * eq[i];\r
     }\r

diff --git a/Robust/src/Tests/ssJava/mp3decoder/huffcodetab.java b/Robust/src/Tests/ssJava/mp3decoder/huffcodetab.java
index 2f52c134f871a9516b45f9681414937b9ad758ca..4442b8d20a2cba620c21a307ed56ef5c338b867b 100644 (file)
--- a/Robust/src/Tests/ssJava/mp3decoder/huffcodetab.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/huffcodetab.java
@@ -540,7 +540,7 @@ final class huffcodetab {
      * \r
      * int bits[] = bitbuf;\r
      */\r
-    do {\r
+    TERMINATE: do {\r
       if (ht[htIdx].val[point][0] == 0) { /* end of tree */\r
         x[0] = ht[htIdx].val[point][1] >>> 4;\r
         y[0] = ht[htIdx].val[point][1] & 0xf;\r
@@ -556,11 +556,11 @@ final class huffcodetab {
        */\r
       // if (bits[bitIndex++]!=0)\r
       if (br.hget1bit() != 0) {\r
-        while (ht[htIdx].val[point][1] >= MXOFF)\r
+        TERMINATE: while (ht[htIdx].val[point][1] >= MXOFF)\r
           point += ht[htIdx].val[point][1];\r
         point += ht[htIdx].val[point][1];\r
       } else {\r
-        while (ht[htIdx].val[point][0] >= MXOFF)\r
+        TERMINATE: while (ht[htIdx].val[point][0] >= MXOFF)\r
           point += ht[htIdx].val[point][0];\r
         point += ht[htIdx].val[point][0];\r
       }\r