From: yeom <yeom>
Date: Thu, 15 Dec 2011 21:32:43 +0000 (+0000)
Subject: New shared loc analysis found a shared location that is not overwritten completely... 
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=IRC.git;a=commitdiff_plain;h=a439ce60d72a530ab13734d49369e172af891fec

New shared loc analysis found a shared location that is not overwritten completely in the synthesis filter. Decoder adds input samples to the Synthesis Filter in circular fashion, which means it needs to keep the last position of the previous loop of the decode to the circular queue. However, the value of start index does not matter because the synthesis filter resumes a normal behavior, as long as data is added to the synthesis filter in a row. Therefore, a workaround solution is that BitStream, which is trusted to ss, assigns the index of header that is incremented by one, and then the decoder overwrites the location of the last position in the Synthesis Filter using the header index. Even the header index value is corrupted, the synthesis filter will resume because BitStream is going to providing following headers.
---

diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
index c2790bfb..26b7c9ba 100644
--- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
+++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
@@ -184,10 +184,6 @@ public class DefinitelyWrittenCheck {
       methodReadWriteSetAnalysis();
       computeSharedCoverSet();
 
-      // System.out.println("$$$=" +
-      // mapMethodToSharedLocCoverSet.get(methodContainingSSJavaLoop));
-      // System.exit(0);
-
       sharedLocAnalysis();
 
       eventLoopAnalysis();
@@ -361,7 +357,8 @@ public class DefinitelyWrittenCheck {
 
                 // computing gen/kill set
                 computeKILLSetForWrite(curr, killSet, lhsLocTuple, lhsHeapPath);
-                if (!dstLoc.equals(srcLoc)) {
+
+                if (!ssjava.isSameHeightWrite(fn)) {
                   computeGENSetForHigherWrite(curr, killSet, lhsLocTuple, lhsHeapPath);
                   updateDeleteSetForHigherWrite(currDeleteSet, lhsLocTuple, lhsHeapPath);
                 } else {
@@ -1642,7 +1639,6 @@ public class DefinitelyWrittenCheck {
       Hashtable<NTuple<Descriptor>, Set<WriteAge>> KILLSet) {
 
     Set<NTuple<Descriptor>> boundMustWriteSet = mapFlatNodeToBoundMustWriteSet.get(fc);
-    System.out.println("#boundMustWriteSet=" + boundMustWriteSet);
 
     for (Iterator iterator = boundMustWriteSet.iterator(); iterator.hasNext();) {
       NTuple<Descriptor> heapPath = (NTuple<Descriptor>) iterator.next();
diff --git a/Robust/src/Benchmarks/SSJava/MP3Decoder/BitstreamWrapper.java b/Robust/src/Benchmarks/SSJava/MP3Decoder/BitstreamWrapper.java
index 6a3209d1..344370c0 100644
--- a/Robust/src/Benchmarks/SSJava/MP3Decoder/BitstreamWrapper.java
+++ b/Robust/src/Benchmarks/SSJava/MP3Decoder/BitstreamWrapper.java
@@ -1,6 +1,7 @@
 public class BitstreamWrapper {
 
   private static Bitstream stream;
+  private static int idx=0;
 
   @TRUST
   public static void init(String filename) {
@@ -11,7 +12,9 @@ public class BitstreamWrapper {
 
   @TRUST
   public static Header readFrame() {
-    return stream.readFrame();
+    Header h=stream.readFrame();
+    h.idx=idx++;
+    return h;
   }
 
 }
diff --git a/Robust/src/Benchmarks/SSJava/MP3Decoder/Header.java b/Robust/src/Benchmarks/SSJava/MP3Decoder/Header.java
index 189028fa..ebcce028 100644
--- a/Robust/src/Benchmarks/SSJava/MP3Decoder/Header.java
+++ b/Robust/src/Benchmarks/SSJava/MP3Decoder/Header.java
@@ -117,9 +117,12 @@ public final class Header {
   @LOC("T")
   private BitReserve br;
 
+  @LOC("T")
+  private int idx;
+
   Header() {
   }
-  
+
   @LATTICE("OUT<BUF,BUF<THIS,THISLOC=THIS,RETURNLOC=OUT")
   public String toString() {
     @LOC("BUF") StringBuffer buffer = new StringBuffer(200);
@@ -696,7 +699,7 @@ public final class Header {
    * 
    * @return bitrate in bps
    */
-  
+
   @RETURNLOC("THIS,Header.FS")
   public String bitrate_string() {
     @LOC("THIS,Header.T") String kbs = " kb/s";
@@ -839,5 +842,14 @@ public final class Header {
   public BitReserve getBitReserve() {
     return br;
   }
+  
+  @RETURNLOC("THIS,Header.T")
+  public int getIdx() {
+    return idx;
+  }
 
+  public int setIdx(int idx) {
+    return this.idx = idx;
+  }
+  
 }
diff --git a/Robust/src/Benchmarks/SSJava/MP3Decoder/LayerIIIDecoder.java b/Robust/src/Benchmarks/SSJava/MP3Decoder/LayerIIIDecoder.java
index 7023a94c..a5546321 100644
--- a/Robust/src/Benchmarks/SSJava/MP3Decoder/LayerIIIDecoder.java
+++ b/Robust/src/Benchmarks/SSJava/MP3Decoder/LayerIIIDecoder.java
@@ -515,17 +515,11 @@ final class LayerIIIDecoder implements FrameDecoder {
     @LOC("THIS,LayerIIIDecoder.HD1") int version = header.version();
 
     // additional codes for the definitely written property
-    filter_pos = (filter_pos + 4) & 0xf;
+    filter_pos = (header.getIdx() * 4) & 0xf;
     filter1.vidx = 1;
     filter2.vidx = 1;
     filter1.actual_write_pos = filter_pos;
     filter2.actual_write_pos = filter_pos;
-    //
-
-    // System.out.println("filter1=" + filter1.vidx + " " +
-    // filter1.actual_write_pos);
-    // System.out.println("filter1=" + filter2.vidx + " " +
-    // filter2.actual_write_pos);
 
     // here 'gr' and 'max_gr' should be higher than 'ch','channels', and more
     for (gr = 0; gr < max_gr; gr++) { // two granules per channel
diff --git a/Robust/src/Benchmarks/SSJava/MP3Decoder/Player.java b/Robust/src/Benchmarks/SSJava/MP3Decoder/Player.java
index d0ef553a..965c7036 100644
--- a/Robust/src/Benchmarks/SSJava/MP3Decoder/Player.java
+++ b/Robust/src/Benchmarks/SSJava/MP3Decoder/Player.java
@@ -124,8 +124,7 @@ public class Player {
     System.out.println("Gobble sentinel: +++");
 
     // @LOC("IN") int count = 0;
-    SSJAVA: while (Counter.idx() < 2147483646) {
-      Counter.inc();
+    SSJAVA: while (true) {
       if (h == null) {
         break;
       }