From ae167f46cf7dc9319b2614e41e73996110fb7afa Mon Sep 17 00:00:00 2001 From: yeom Date: Sat, 20 Aug 2011 00:57:51 +0000 Subject: [PATCH] mp3decoder passes the loop termination analysis. --- .../src/Analysis/SSJava/SSJavaAnalysis.java | 51 ++++++++++++++++++- Robust/src/ClassLibrary/SSJava/String.java | 5 ++ .../Tests/ssJava/mp3decoder/BitReserve.java | 2 + .../ssJava/mp3decoder/LayerIIIDecoder.java | 22 ++++++-- .../src/Tests/ssJava/mp3decoder/Player.java | 10 +++- .../ssJava/mp3decoder/SynthesisFilter.java | 1 + .../Tests/ssJava/mp3decoder/huffcodetab.java | 6 +-- 7 files changed, 85 insertions(+), 12 deletions(-) diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java index a9f2e858..70944c9c 100644 --- 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 toanalyzeList = new ArrayList(); + List toanalyzeMethodList = new ArrayList(); + + toanalyzeList.addAll(classtable.getValueSet()); + Collections.sort(toanalyzeList, new Comparator() { + 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() { + 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 4734915f..5f963399 100644 --- 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 e4167f00..15f4a068 100644 --- a/Robust/src/Tests/ssJava/mp3decoder/BitReserve.java +++ b/Robust/src/Tests/ssJava/mp3decoder/BitReserve.java @@ -93,11 +93,13 @@ final class BitReserve { @LOC("THIS,BitReserve.BIT") int pos = buf_byte_idx; if (pos + N < BUFSIZE) { + TERMINATE: while (N-- > 0) { val <<= 1; val |= ((buf[pos++] != 0) ? 1 : 0); } } else { + TERMINATE: while (N-- > 0) { val <<= 1; val |= ((buf[pos] != 0) ? 1 : 0); diff --git a/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java b/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java index cd0d38e6..31cd7a1c 100644 --- 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 83851e29..2e2b02cd 100644 --- 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") public boolean play(@LOC("IN") int frames) throws JavaLayerException { @LOC("T") boolean ret = true; - - SSJAVA: while (frames-- > 0 && ret) { + + int maxFrame=frames-1; + int count=0; + SSJAVA: while (count++ < maxFrame) { ret = decodeFrame(); + if(!ret){ + break; + } } /* @@ -190,6 +195,7 @@ public class Player { @LOC("C") int sum = 0; @LOC("C") short[] outbuf = SampleBufferWrapper.getBuffer(); // short[] outbuf = output.getBuffer(); + TERMINATE: for (@LOC("C") int i = 0; i < SampleBufferWrapper.getBufferLength(); i++) { // System.out.println(outbuf[i]); sum += outbuf[i]; diff --git a/Robust/src/Tests/ssJava/mp3decoder/SynthesisFilter.java b/Robust/src/Tests/ssJava/mp3decoder/SynthesisFilter.java index bc86eb80..0882bacc 100644 --- a/Robust/src/Tests/ssJava/mp3decoder/SynthesisFilter.java +++ b/Robust/src/Tests/ssJava/mp3decoder/SynthesisFilter.java @@ -125,6 +125,7 @@ final class SynthesisFilter { } public void input_samples(@LOC("IN") float[] s) { + TERMINATE: for (@LOC("C") int i = 31; i >= 0; i--) { samples[i] = s[i] * eq[i]; } diff --git a/Robust/src/Tests/ssJava/mp3decoder/huffcodetab.java b/Robust/src/Tests/ssJava/mp3decoder/huffcodetab.java index 2f52c134..4442b8d2 100644 --- a/Robust/src/Tests/ssJava/mp3decoder/huffcodetab.java +++ b/Robust/src/Tests/ssJava/mp3decoder/huffcodetab.java @@ -540,7 +540,7 @@ final class huffcodetab { * * int bits[] = bitbuf; */ - do { + TERMINATE: do { if (ht[htIdx].val[point][0] == 0) { /* end of tree */ x[0] = ht[htIdx].val[point][1] >>> 4; y[0] = ht[htIdx].val[point][1] & 0xf; @@ -556,11 +556,11 @@ final class huffcodetab { */ // if (bits[bitIndex++]!=0) if (br.hget1bit() != 0) { - while (ht[htIdx].val[point][1] >= MXOFF) + TERMINATE: while (ht[htIdx].val[point][1] >= MXOFF) point += ht[htIdx].val[point][1]; point += ht[htIdx].val[point][1]; } else { - while (ht[htIdx].val[point][0] >= MXOFF) + TERMINATE: while (ht[htIdx].val[point][0] >= MXOFF) point += ht[htIdx].val[point][0]; point += ht[htIdx].val[point][0]; } -- 2.34.1