changes.

diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
index 21d7b33c99d28ffc6e47bd0f88c98debf5a2b830..c6d2b3589579494c2bc40cff6ba9cc2f648e5fd7 100644 (file)
--- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
+++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
@@ -783,14 +783,10 @@ public class DefinitelyWrittenCheck {
 
     assert ssjavaLoopEntrance != null;
 
-    System.out.println("ssjavaLoopEntrance=" + ssjavaLoopEntrance);
-
     // assume that ssjava loop is top-level loop in method, not nested loop
     Set nestedLoop = loopFinder.nestedLoops();
     for (Iterator loopIter = nestedLoop.iterator(); loopIter.hasNext();) {
       LoopFinder lf = (LoopFinder) loopIter.next();
-      System.out.println("lf=" + lf.loopEntrances());
-      System.out.println("elements=" + lf.loopIncElements());
       if (lf.loopEntrances().iterator().next().equals(ssjavaLoopEntrance)) {
         ssjavaLoop = lf;
       }
@@ -913,9 +909,9 @@ public class DefinitelyWrittenCheck {
           TypeDescriptor td = rhs.getType().dereference();
           fld = getArrayField(td);
         }
-        
-        if(fld.isFinal() && fld.isStatic()){
-          // if field is final and static, no need to check 
+
+        if (fld.isFinal() /* && fld.isStatic() */) {
+          // if field is final and static, no need to check
           break;
         }
 
@@ -961,7 +957,6 @@ public class DefinitelyWrittenCheck {
       case FKind.FlatCall: {
         FlatCall fc = (FlatCall) fn;
         bindHeapPathCallerArgWithCaleeParam(fc);
-
         // add <hp,statement,false> in which hp is an element of
         // READ_bound set
         // of callee: callee has 'read' requirement!
@@ -1157,7 +1152,8 @@ public class DefinitelyWrittenCheck {
         (LinkedList<MethodDescriptor>) sortedDescriptors.clone();
 
     // no need to analyze method having ssjava loop
-    methodContainingSSJavaLoop = descriptorListToAnalyze.removeFirst();
+    // methodContainingSSJavaLoop = descriptorListToAnalyze.removeFirst();
+    methodContainingSSJavaLoop = ssjava.getMethodContainingSSJavaLoop();
 
     // current descriptors to visit in fixed-point interprocedural analysis,
     // prioritized by
@@ -1302,9 +1298,9 @@ public class DefinitelyWrittenCheck {
         TypeDescriptor td = rhs.getType().dereference();
         fld = getArrayField(td);
       }
-      
-      if(fld.isFinal() && fld.isStatic()){
-        // if field is final and static, no need to check 
+
+      if (fld.isFinal() /* && fld.isStatic() */) {
+        // if field is final and static, no need to check
         break;
       }
 
@@ -1372,24 +1368,26 @@ public class DefinitelyWrittenCheck {
 
       FlatCall fc = (FlatCall) fn;
 
-      bindHeapPathCallerArgWithCaleeParam(fc);
+      if (fc.getThis() != null) {
+        bindHeapPathCallerArgWithCaleeParam(fc);
 
-      // add heap path, which is an element of READ_bound set and is not
-      // an
-      // element of WT set, to the caller's READ set
-      for (Iterator iterator = calleeUnionBoundReadSet.iterator(); iterator.hasNext();) {
-        NTuple<Descriptor> read = (NTuple<Descriptor>) iterator.next();
-        if (!writtenSet.contains(read)) {
-          readSet.add(read);
+        // add heap path, which is an element of READ_bound set and is not
+        // an
+        // element of WT set, to the caller's READ set
+        for (Iterator iterator = calleeUnionBoundReadSet.iterator(); iterator.hasNext();) {
+          NTuple<Descriptor> read = (NTuple<Descriptor>) iterator.next();
+          if (!writtenSet.contains(read)) {
+            readSet.add(read);
+          }
         }
-      }
-      writtenSet.removeAll(calleeUnionBoundReadSet);
+        writtenSet.removeAll(calleeUnionBoundReadSet);
 
-      // add heap path, which is an element of OVERWRITE_bound set, to the
-      // caller's WT set
-      for (Iterator iterator = calleeIntersectBoundOverWriteSet.iterator(); iterator.hasNext();) {
-        NTuple<Descriptor> write = (NTuple<Descriptor>) iterator.next();
-        writtenSet.add(write);
+        // add heap path, which is an element of OVERWRITE_bound set, to the
+        // caller's WT set
+        for (Iterator iterator = calleeIntersectBoundOverWriteSet.iterator(); iterator.hasNext();) {
+          NTuple<Descriptor> write = (NTuple<Descriptor>) iterator.next();
+          writtenSet.add(write);
+        }
       }
 
     }

diff --git a/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java b/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java
index 5dbcc8ad89b324218b0a3837bd8a3ab33ba1bda2..778c0553c5fe3699a88a79d060ce14bdcfd677c8 100644 (file)
--- a/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java
+++ b/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java
@@ -282,6 +282,7 @@ public class MethodAnnotationCheck {
       if (isSSJavaLoop) {
         throw new Error("Only outermost loop can be the self-stabilizing loop.");
       } else {
+        ssjava.setMethodContainingSSJavaLoop(md);
         annotatedMDSet.add(md);
         isSSJavaLoop = true;
       }

diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
index 70944c9c6f284ae8e5db53600a8cc3d721572283..fb1376330ce1704563d39494679e8a8920bf9bee 100644 (file)
--- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
+++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
@@ -77,6 +77,9 @@ public class SSJavaAnalysis {
   // the set of method descriptors annotated as "TRUST"
   Set<MethodDescriptor> trustWorthyMDSet;
 
+  // points to method containing SSJAVA Loop
+  private MethodDescriptor methodContainingSSJavaLoop;
+
   CallGraph callgraph;
 
   LinearTypeCheck checker;
@@ -104,10 +107,10 @@ public class SSJavaAnalysis {
     // if (state.SSJAVADEBUG) {
     // debugPrint();
     // }
-    // parseLocationAnnotation();
+    parseLocationAnnotation();
     // doFlowDownCheck();
-    // doDefinitelyWrittenCheck();
-    debugDoLoopCheck();
+    doDefinitelyWrittenCheck();
+    // debugDoLoopCheck();
   }
 
   private void debugDoLoopCheck() {
@@ -494,4 +497,11 @@ public class SSJavaAnalysis {
     return bf;
   }
 
+  public MethodDescriptor getMethodContainingSSJavaLoop() {
+    return methodContainingSSJavaLoop;
+  }
+
+  public void setMethodContainingSSJavaLoop(MethodDescriptor methodContainingSSJavaLoop) {
+    this.methodContainingSSJavaLoop = methodContainingSSJavaLoop;
+  }
 }

diff --git a/Robust/src/Tests/ssJava/mp3decoder/Header.java b/Robust/src/Tests/ssJava/mp3decoder/Header.java
index 8dc5237ff273db97d3ab539ded2dd098ed60b8fc..b98fea93bc1a144c87fbcf805e225415cce8a036 100644 (file)
--- a/Robust/src/Tests/ssJava/mp3decoder/Header.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/Header.java
@@ -119,7 +119,7 @@ public final class Header {
 
   Header() {
   }
-
+  
   @LATTICE("OUT<BUF,BUF<THIS,THISLOC=THIS,RETURNLOC=OUT")
   public String toString() {
     @LOC("BUF") StringBuffer buffer = new StringBuffer(200);
@@ -696,6 +696,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";

diff --git a/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java b/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java
index 31cd7a1c6e4c96703a3642147e22bd5c83adc60b..82989acbe584d6cd18a96ebe453fe9508f828570 100644 (file)
--- a/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java
@@ -87,7 +87,7 @@ final class LayerIIIDecoder implements FrameDecoder {
 
   // @LOC("SBT") private temporaire2[] III_scalefac_t;
   @LOC("SF2")
-  private temporaire2[] scalefac;
+  private final temporaire2[] scalefac;
   // private III_scalefac_t scalefac;
 
   @LOC("CH0")
@@ -96,7 +96,7 @@ final class LayerIIIDecoder implements FrameDecoder {
   private int frame_start;
   // @LOC("SI1") private int part2_start;
   @LOC("CH0")
-  private int channels;
+  private final int channels;
   @LOC("CH0")
   private int first_channel;
   @LOC("CH0")
@@ -243,7 +243,6 @@ final class LayerIIIDecoder implements FrameDecoder {
 
     nonzero[0] = nonzero[1] = 576;
 
-    br = new BitReserve();
     si = new III_side_info_t();
 
     initialized = true;
@@ -457,7 +456,14 @@ final class LayerIIIDecoder implements FrameDecoder {
     if (!initialized) {
       init(header);
     }
-
+    
+    // overwrites once per a loop
+    samples1 = new float[32];
+    samples2 = new float[32];
+    prevblck = new float[2][SBLIMIT * SSLIMIT];
+    si = new III_side_info_t();
+    //
+    
     @LOC("THIS,LayerIIIDecoder.HD1") int nSlots = header.slots();
 
     @LOC("THIS,LayerIIIDecoder.CH0") int gr;

diff --git a/Robust/src/Tests/ssJava/mp3decoder/Player.java b/Robust/src/Tests/ssJava/mp3decoder/Player.java
index 2e2b02cd0e7d8cf975b21489a1a6bb27ed0144b0..b7e8078eea84e7f0e32274da0874da46fef06e58 100644 (file)
--- a/Robust/src/Tests/ssJava/mp3decoder/Player.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/Player.java
@@ -112,9 +112,8 @@ public class Player {
   public boolean play(@LOC("IN") int frames) throws JavaLayerException {\r
     @LOC("T") boolean ret = true;\r
     \r
-    int maxFrame=frames-1;\r
     int count=0;\r
-    SSJAVA: while (count++ < maxFrame) {\r
+    SSJAVA: while (count++ < 2147483646) {\r
       ret = decodeFrame();\r
       if(!ret){\r
           break;\r

diff --git a/Robust/src/Tests/ssJava/mp3decoder/SynthesisFilter.java b/Robust/src/Tests/ssJava/mp3decoder/SynthesisFilter.java
index 0882baccb16f5cdaecbb7f02715725c3679eeb68..7a2d41e59c7fa66f40b5ae16b67f9aa2982204fe 100644 (file)
--- a/Robust/src/Tests/ssJava/mp3decoder/SynthesisFilter.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/SynthesisFilter.java
@@ -39,7 +39,7 @@
 final class SynthesisFilter {\r
 \r
   @LOC("IDX")\r
-  private int vidx = 1;\r
+  private int vidx;\r
   @LOC("V")\r
   private float[] v1;\r
   @LOC("V")\r
@@ -50,9 +50,9 @@ final class SynthesisFilter {
   @LOC("SAMPLE")\r
   private float[] samples; // 32 new subband samples\r
   @LOC("V")\r
-  private int channel;\r
+  public final int channel;\r
   @LOC("V")\r
-  private float scalefactor;\r
+  public final float scalefactor;\r
   @LOC("EQ")\r
   private float[] eq;\r
 \r
@@ -76,6 +76,7 @@ final class SynthesisFilter {
    */\r
   public SynthesisFilter(int channelnumber, float factor, float[] eq0) {\r
 \r
+    vidx = 1;\r
     d16 = splitArray(d, 16);\r
 \r
     v1 = new float[512];\r
@@ -125,8 +126,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
+    TERMINATE: for (@LOC("C") int i = 31; i >= 0; i--) {\r
       samples[i] = s[i] * eq[i];\r
     }\r
   }\r