changes.

diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
index b1f7029ed0fb0d42616f7f667095356ef0d96e95..21d7b33c99d28ffc6e47bd0f88c98debf5a2b830 100644 (file)
--- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
+++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
@@ -17,13 +17,16 @@ import IR.State;
 import IR.TypeDescriptor;
 import IR.Flat.FKind;
 import IR.Flat.FlatCall;
+import IR.Flat.FlatElementNode;
 import IR.Flat.FlatFieldNode;
 import IR.Flat.FlatLiteralNode;
 import IR.Flat.FlatMethod;
 import IR.Flat.FlatNode;
 import IR.Flat.FlatOpNode;
+import IR.Flat.FlatSetElementNode;
 import IR.Flat.FlatSetFieldNode;
 import IR.Flat.TempDescriptor;
+import IR.Tree.Modifiers;
 import Util.Pair;
 
 public class DefinitelyWrittenCheck {
@@ -82,6 +85,9 @@ public class DefinitelyWrittenCheck {
   // when analyzing flatcall, need to re-schedule set of callee
   private Set<MethodDescriptor> calleesToEnqueue;
 
+  public static final String arrayElementFieldName = "___element_";
+  static protected Hashtable<TypeDescriptor, FieldDescriptor> mapTypeToArrayField;
+
   private Set<ClearingSummary> possibleCalleeCompleteSummarySetToCaller;
 
   private LinkedList<MethodDescriptor> sortedDescriptors;
@@ -117,6 +123,7 @@ public class DefinitelyWrittenCheck {
     this.methodDescriptorsToVisitStack = new Stack<MethodDescriptor>();
     this.calleesToEnqueue = new HashSet<MethodDescriptor>();
     this.possibleCalleeCompleteSummarySetToCaller = new HashSet<ClearingSummary>();
+    this.mapTypeToArrayField = new Hashtable<TypeDescriptor, FieldDescriptor>();
     this.LOCAL = new TempDescriptor("LOCAL");
   }
 
@@ -776,10 +783,14 @@ 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;
       }
@@ -890,10 +901,23 @@ public class DefinitelyWrittenCheck {
       case FKind.FlatFieldNode:
       case FKind.FlatElementNode: {
 
-        FlatFieldNode ffn = (FlatFieldNode) fn;
-        lhs = ffn.getDst();
-        rhs = ffn.getSrc();
-        fld = ffn.getField();
+        if (fn.kind() == FKind.FlatFieldNode) {
+          FlatFieldNode ffn = (FlatFieldNode) fn;
+          lhs = ffn.getDst();
+          rhs = ffn.getSrc();
+          fld = ffn.getField();
+        } else {
+          FlatElementNode fen = (FlatElementNode) fn;
+          lhs = fen.getDst();
+          rhs = fen.getSrc();
+          TypeDescriptor td = rhs.getType().dereference();
+          fld = getArrayField(td);
+        }
+        
+        if(fld.isFinal() && fld.isStatic()){
+          // if field is final and static, no need to check 
+          break;
+        }
 
         // read field
         NTuple<Descriptor> srcHeapPath = mapHeapPath.get(rhs);
@@ -913,9 +937,17 @@ public class DefinitelyWrittenCheck {
       case FKind.FlatSetFieldNode:
       case FKind.FlatSetElementNode: {
 
-        FlatSetFieldNode fsfn = (FlatSetFieldNode) fn;
-        lhs = fsfn.getDst();
-        fld = fsfn.getField();
+        if (fn.kind() == FKind.FlatSetFieldNode) {
+          FlatSetFieldNode fsfn = (FlatSetFieldNode) fn;
+          lhs = fsfn.getDst();
+          fld = fsfn.getField();
+        } else {
+          FlatSetElementNode fsen = (FlatSetElementNode) fn;
+          lhs = fsen.getDst();
+          rhs = fsen.getSrc();
+          TypeDescriptor td = lhs.getType().dereference();
+          fld = getArrayField(td);
+        }
 
         // write(field)
         NTuple<Descriptor> lhsHeapPath = computePath(lhs);
@@ -1253,15 +1285,28 @@ public class DefinitelyWrittenCheck {
     }
       break;
 
-    case FKind.FlatFieldNode:
-    case FKind.FlatElementNode: {
+    case FKind.FlatElementNode:
+    case FKind.FlatFieldNode: {
 
       // y=x.f;
 
-      FlatFieldNode ffn = (FlatFieldNode) fn;
-      lhs = ffn.getDst();
-      rhs = ffn.getSrc();
-      fld = ffn.getField();
+      if (fn.kind() == FKind.FlatFieldNode) {
+        FlatFieldNode ffn = (FlatFieldNode) fn;
+        lhs = ffn.getDst();
+        rhs = ffn.getSrc();
+        fld = ffn.getField();
+      } else {
+        FlatElementNode fen = (FlatElementNode) fn;
+        lhs = fen.getDst();
+        rhs = fen.getSrc();
+        TypeDescriptor td = rhs.getType().dereference();
+        fld = getArrayField(td);
+      }
+      
+      if(fld.isFinal() && fld.isStatic()){
+        // if field is final and static, no need to check 
+        break;
+      }
 
       // set up heap path
       NTuple<Descriptor> srcHeapPath = mapHeapPath.get(rhs);
@@ -1292,10 +1337,19 @@ public class DefinitelyWrittenCheck {
     case FKind.FlatSetElementNode: {
 
       // x.f=y;
-      FlatSetFieldNode fsfn = (FlatSetFieldNode) fn;
-      lhs = fsfn.getDst();
-      fld = fsfn.getField();
-      rhs = fsfn.getSrc();
+
+      if (fn.kind() == FKind.FlatSetFieldNode) {
+        FlatSetFieldNode fsfn = (FlatSetFieldNode) fn;
+        lhs = fsfn.getDst();
+        fld = fsfn.getField();
+        rhs = fsfn.getSrc();
+      } else {
+        FlatSetElementNode fsen = (FlatSetElementNode) fn;
+        lhs = fsen.getDst();
+        rhs = fsen.getSrc();
+        TypeDescriptor td = lhs.getType().dereference();
+        fld = getArrayField(td);
+      }
 
       // set up heap path
       NTuple<Descriptor> lhsHeapPath = mapHeapPath.get(lhs);
@@ -1351,6 +1405,17 @@ public class DefinitelyWrittenCheck {
 
   }
 
+  static public FieldDescriptor getArrayField(TypeDescriptor td) {
+    FieldDescriptor fd = mapTypeToArrayField.get(td);
+    if (fd == null) {
+      fd =
+          new FieldDescriptor(new Modifiers(Modifiers.PUBLIC), td, arrayElementFieldName, null,
+              false);
+      mapTypeToArrayField.put(td, fd);
+    }
+    return fd;
+  }
+
   private void mergeSharedLocationAnaylsis(ClearingSummary curr, Set<ClearingSummary> inSet) {
 
     if (inSet.size() == 0) {

diff --git a/Robust/src/Tests/ssJava/mp3decoder/LayerIIDecoder.java b/Robust/src/Tests/ssJava/mp3decoder/LayerIIDecoder.java
index 0f51113e4c630b851f51c8734012db96ddefa1b3..a6740fac04c0c3abcd26e2c8cf3a9c694602e6bb 100644 (file)
--- a/Robust/src/Tests/ssJava/mp3decoder/LayerIIDecoder.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/LayerIIDecoder.java
@@ -758,7 +758,7 @@ class LayerIIDecoder extends LayerIDecoder implements FrameDecoder
         /**
          * Class for layer II subbands in joint stereo mode.
          */
-     @LATTICE("S<L,L<H,L<ARR,ARR<F,SN<F,GN<F,F<H,H<SH,SN*,GN*")
+     @LATTICE("S<L,L<H,L<ARR,ARR<F,SN<F,GN<F,F<H,H<SH,SN*,GN*,L*")
        @METHODDEFAULT("OUT<V,V<SH,SH<THIS,THIS<IN,SH*,THISLOC=THIS,GLOBALLOC=IN")
        static class SubbandLayer2IntensityStereo extends SubbandLayer2
        {

diff --git a/Robust/src/Tests/ssJava/mp3decoder/Player.java b/Robust/src/Tests/ssJava/mp3decoder/Player.java
index d898e9124f6f7e8d4411d4dce6628fcbe4b436cf..647e4c945bd6fce05a1a081fd62da8a1c88862cb 100644 (file)
--- a/Robust/src/Tests/ssJava/mp3decoder/Player.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/Player.java
@@ -209,7 +209,7 @@ public class Player
         * \r
         * @return true if there are no more frames to decode, false otherwise.\r
         */\r
-       @LATTICE("O,THISLOC=O")\r
+       @LATTICE("O<TH,THISLOC=TH")\r
        @RETURNLOC("O")\r
        protected boolean decodeFrame() throws JavaLayerException\r
        {               \r

diff --git a/Robust/src/Tests/ssJava/mp3decoder/SampleBuffer.java b/Robust/src/Tests/ssJava/mp3decoder/SampleBuffer.java
index 0ff8bc285f5dec23677e5d9fbf7272941a9c4929..b32bacde738f7962bcd67a59b7b638677a11fcba 100644 (file)
--- a/Robust/src/Tests/ssJava/mp3decoder/SampleBuffer.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/SampleBuffer.java
@@ -91,7 +91,7 @@ public class SampleBuffer extends Obuffer
     
   }
 
-  @LATTICE("D<IN,D<C,THISLOC=D,C*")
+  @LATTICE("D<IN,IN<C,THISLOC=D,C*")
   public void appendSamples(@LOC("IN") int channel, @LOC("IN") float[] f)
   {
     @LOC("D,SampleBuffer.BUFP") int pos = bufferp[channel];