New shared loc analysis found a shared location that is not overwritten completely...
authoryeom <yeom>
Thu, 15 Dec 2011 21:32:43 +0000 (21:32 +0000)
committeryeom <yeom>
Thu, 15 Dec 2011 21:32:43 +0000 (21:32 +0000)
Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
Robust/src/Benchmarks/SSJava/MP3Decoder/BitstreamWrapper.java
Robust/src/Benchmarks/SSJava/MP3Decoder/Header.java
Robust/src/Benchmarks/SSJava/MP3Decoder/LayerIIIDecoder.java
Robust/src/Benchmarks/SSJava/MP3Decoder/Player.java

index c2790bf..26b7c9b 100644 (file)
@@ -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();
index 6a3209d..344370c 100644 (file)
@@ -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;
   }
 
 }
index 189028f..ebcce02 100644 (file)
@@ -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;
+  }
+  
 }
index 7023a94..a554632 100644 (file)
@@ -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
index d0ef553..965c703 100644 (file)
@@ -124,8 +124,7 @@ public class Player {
     System.out.println("Gobble sentinel: +++");\r
 \r
     // @LOC("IN") int count = 0;\r
-    SSJAVA: while (Counter.idx() < 2147483646) {\r
-      Counter.inc();\r
+    SSJAVA: while (true) {\r
       if (h == null) {\r
         break;\r
       }\r