From: yeom <yeom>
Date: Sat, 20 Aug 2011 08:49:24 +0000 (+0000)
Subject: changes.
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=bafdf8895425a699f5550a970a2c8144e06ae1e2;p=IRC.git

changes.
---

diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
index 21d7b33c..c6d2b358 100644
--- 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 5dbcc8ad..778c0553 100644
--- 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 70944c9c..fb137633 100644
--- 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 8dc5237f..b98fea93 100644
--- 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 31cd7a1c..82989acb 100644
--- 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 2e2b02cd..b7e8078e 100644
--- 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 {
     @LOC("T") boolean ret = true;
     
-    int maxFrame=frames-1;
     int count=0;
-    SSJAVA: while (count++ < maxFrame) {
+    SSJAVA: while (count++ < 2147483646) {
       ret = decodeFrame();
       if(!ret){
           break;
diff --git a/Robust/src/Tests/ssJava/mp3decoder/SynthesisFilter.java b/Robust/src/Tests/ssJava/mp3decoder/SynthesisFilter.java
index 0882bacc..7a2d41e5 100644
--- a/Robust/src/Tests/ssJava/mp3decoder/SynthesisFilter.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/SynthesisFilter.java
@@ -39,7 +39,7 @@
 final class SynthesisFilter {
 
   @LOC("IDX")
-  private int vidx = 1;
+  private int vidx;
   @LOC("V")
   private float[] v1;
   @LOC("V")
@@ -50,9 +50,9 @@ final class SynthesisFilter {
   @LOC("SAMPLE")
   private float[] samples; // 32 new subband samples
   @LOC("V")
-  private int channel;
+  public final int channel;
   @LOC("V")
-  private float scalefactor;
+  public final float scalefactor;
   @LOC("EQ")
   private float[] eq;
 
@@ -76,6 +76,7 @@ final class SynthesisFilter {
    */
   public SynthesisFilter(int channelnumber, float factor, float[] eq0) {
 
+    vidx = 1;
     d16 = splitArray(d, 16);
 
     v1 = new float[512];
@@ -125,8 +126,7 @@ final class SynthesisFilter {
   }
 
   public void input_samples(@LOC("IN") float[] s) {
-    TERMINATE:
-    for (@LOC("C") int i = 31; i >= 0; i--) {
+    TERMINATE: for (@LOC("C") int i = 31; i >= 0; i--) {
       samples[i] = s[i] * eq[i];
     }
   }