New shared loc analysis found a shared location that is not overwritten completely...

diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
index c2790bfbd21356a6a1e9af401056262c2ecda561..26b7c9ba0abc17366e577efdc23e061ba5b00e44 100644 (file)
--- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
+++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
@@ -184,10 +184,6 @@ public class DefinitelyWrittenCheck {
       methodReadWriteSetAnalysis();
       computeSharedCoverSet();
 
       methodReadWriteSetAnalysis();
       computeSharedCoverSet();
 

-      // System.out.println("$$$=" +
-      // mapMethodToSharedLocCoverSet.get(methodContainingSSJavaLoop));
-      // System.exit(0);
-

       sharedLocAnalysis();
 
       eventLoopAnalysis();
       sharedLocAnalysis();
 
       eventLoopAnalysis();


@@ -361,7 +357,8 @@ public class DefinitelyWrittenCheck {
 
                 // computing gen/kill set
                 computeKILLSetForWrite(curr, killSet, lhsLocTuple, lhsHeapPath);
 
                 // 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 {
                   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);
       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();
 
     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 6a3209d11889d82450551da056e34e4ebb52df41..344370c00b21619bf02aac726afacc4618665fa4 100644 (file)
--- 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;
 public class BitstreamWrapper {
 
   private static Bitstream stream;

+  private static int idx=0;

 
   @TRUST
   public static void init(String filename) {
 
   @TRUST
   public static void init(String filename) {


@@ -11,7 +12,9 @@ public class BitstreamWrapper {
 
   @TRUST
   public static Header readFrame() {
 
   @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 189028fa2813cc22cd53596efe27b4a165743af7..ebcce028050a1f44d54eefff00d5d1db4166c658 100644 (file)
--- 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 BitReserve br;
 

+  @LOC("T")
+  private int idx;
+

   Header() {
   }
   Header() {
   }

-  
+

   @LATTICE("OUT<BUF,BUF<THIS,THISLOC=THIS,RETURNLOC=OUT")
   public String toString() {
     @LOC("BUF") StringBuffer buffer = new StringBuffer(200);
   @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
    */
    * 
    * @return bitrate in bps
    */

-  
+

   @RETURNLOC("THIS,Header.FS")
   public String bitrate_string() {
     @LOC("THIS,Header.T") String kbs = " kb/s";
   @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;
   }
   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 7023a94c2dd71f790f56e7395223078b0338b4d4..a5546321ece1b529c4a4a9b7f8251cc2eb6cd601 100644 (file)
--- 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
     @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;
     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
 
     // 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 d0ef553aff75f90ffdf97367de116a20dd4077f1..965c70362a71059f6e2943beb2348585937e6f2b 100644 (file)
--- 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: +++");\r
 \r
     // @LOC("IN") int count = 0;\r
     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
       if (h == null) {\r
         break;\r
       }\r