1) changes on the definitely written analysis: it only takes care about locations...

2) bug fix on the definitely written analysis: static method doesn't have implicit 'this' argument.
3) add a set of static functions that initialize array elements
4) changes on mp3decoder: move init() method out of SSJava loop and start to use SSJava array init method

diff --git a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
index 2536171de0ec1049f11cba86a0988f63991ca57f..cec3a49d32ea1b075bdcfea5edb1bf3f2045368a 100644 (file)
--- a/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
+++ b/Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java
@@ -57,6 +57,10 @@ public class DefinitelyWrittenCheck {
   // overwritten on every possible path during method invocation
   private Hashtable<FlatMethod, Set<NTuple<Descriptor>>> mapFlatMethodToOverWrite;
 
+  // maps a flat method to the WRITE that is the set of heap path that is
+  // written to
+  private Hashtable<FlatMethod, Set<NTuple<Descriptor>>> mapFlatMethodToWrite;
+
   // points to method containing SSJAVA Loop
   private MethodDescriptor methodContainingSSJavaLoop;
 
@@ -98,6 +102,7 @@ public class DefinitelyWrittenCheck {
 
   private Set<NTuple<Descriptor>> calleeUnionBoundReadSet;
   private Set<NTuple<Descriptor>> calleeIntersectBoundOverWriteSet;
+  private Set<NTuple<Descriptor>> calleeBoundWriteSet;
 
   private TempDescriptor LOCAL;
 
@@ -110,10 +115,12 @@ public class DefinitelyWrittenCheck {
     this.mapHeapPath = new Hashtable<Descriptor, NTuple<Descriptor>>();
     this.mapFlatMethodToRead = new Hashtable<FlatMethod, Set<NTuple<Descriptor>>>();
     this.mapFlatMethodToOverWrite = new Hashtable<FlatMethod, Set<NTuple<Descriptor>>>();
+    this.mapFlatMethodToWrite = new Hashtable<FlatMethod, Set<NTuple<Descriptor>>>();
     this.definitelyWrittenResults =
         new Hashtable<FlatNode, Hashtable<NTuple<Descriptor>, Hashtable<FlatNode, Boolean>>>();
     this.calleeUnionBoundReadSet = new HashSet<NTuple<Descriptor>>();
     this.calleeIntersectBoundOverWriteSet = new HashSet<NTuple<Descriptor>>();
+    this.calleeBoundWriteSet = new HashSet<NTuple<Descriptor>>();
 
     this.mapMethodDescriptorToCompleteClearingSummary =
         new Hashtable<MethodDescriptor, ClearingSummary>();
@@ -131,8 +138,8 @@ public class DefinitelyWrittenCheck {
     if (!ssjava.getAnnotationRequireSet().isEmpty()) {
       methodReadOverWriteAnalysis();
       writtenAnalyis();
-      sharedLocationAnalysis();
-      checkSharedLocationResult();
+      // sharedLocationAnalysis();
+      // checkSharedLocationResult();
     }
   }
 
@@ -143,7 +150,6 @@ public class DefinitelyWrittenCheck {
     ClearingSummary result =
         mapMethodDescriptorToCompleteClearingSummary.get(sortedDescriptors.peekFirst());
 
-
     Set<NTuple<Descriptor>> hpKeySet = result.keySet();
     for (Iterator iterator = hpKeySet.iterator(); iterator.hasNext();) {
       NTuple<Descriptor> hpKey = (NTuple<Descriptor>) iterator.next();
@@ -342,18 +348,36 @@ 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);
+      }
+
+      // FlatFieldNode ffn = (FlatFieldNode) fn;
+      // lhs = ffn.getDst();
+      // rhs = ffn.getSrc();
+      // fld = ffn.getField();
 
       // read field
       NTuple<Descriptor> srcHeapPath = mapHeapPath.get(rhs);
+
+      // if (srcHeapPath != null) {
+      // // if lhs srcHeapPath is null, it means that it is not reachable from
+      // // callee's parameters. so just ignore it
       NTuple<Descriptor> fldHeapPath = new NTuple<Descriptor>(srcHeapPath.getList());
 
       if (fld.getType().isImmutable()) {
         readLocation(curr, fldHeapPath, fld);
       }
+      // }
 
     }
       break;
@@ -395,8 +419,8 @@ public class DefinitelyWrittenCheck {
       MethodDescriptor mdCallee = fc.getMethod();
       FlatMethod fmCallee = state.getMethodFlat(mdCallee);
       Set<MethodDescriptor> setPossibleCallees = new HashSet<MethodDescriptor>();
-      TypeDescriptor typeDesc = fc.getThis().getType();
-      setPossibleCallees.addAll(callGraph.getMethods(mdCallee, typeDesc));
+      // TypeDescriptor typeDesc = fc.getThis().getType();
+      setPossibleCallees.addAll(callGraph.getMethods(mdCallee));
 
       possibleCalleeCompleteSummarySetToCaller.clear();
 
@@ -453,15 +477,17 @@ public class DefinitelyWrittenCheck {
     Hashtable<Integer, NTuple<Descriptor>> mapArgIdx2CallerArgHeapPath =
         new Hashtable<Integer, NTuple<Descriptor>>();
 
-    // arg idx is starting from 'this' arg
-    NTuple<Descriptor> thisHeapPath = mapHeapPath.get(fc.getThis());
-    if (thisHeapPath == null) {
-      // method is called without creating new flat node representing 'this'
-      thisHeapPath = new NTuple<Descriptor>();
-      thisHeapPath.add(fc.getThis());
-    }
+    if (fc.getThis() != null) {
+      // arg idx is starting from 'this' arg
+      NTuple<Descriptor> thisHeapPath = mapHeapPath.get(fc.getThis());
+      if (thisHeapPath == null) {
+        // method is called without creating new flat node representing 'this'
+        thisHeapPath = new NTuple<Descriptor>();
+        thisHeapPath.add(fc.getThis());
+      }
 
-    mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath);
+      mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath);
+    }
 
     for (int i = 0; i < fc.numArgs(); i++) {
       TempDescriptor arg = fc.getArg(i);
@@ -635,10 +661,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);
+      }
+
+      // FlatFieldNode ffn = (FlatFieldNode) fn;
+      // lhs = ffn.getDst();
+      // rhs = ffn.getSrc();
+      // fld = ffn.getField();
 
       // read field
       NTuple<Descriptor> srcHeapPath = mapHeapPath.get(rhs);
@@ -954,12 +993,13 @@ 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!
 
-        
+
         for (Iterator iterator = calleeUnionBoundReadSet.iterator(); iterator.hasNext();) {
           NTuple<Descriptor> read = (NTuple<Descriptor>) iterator.next();
           Hashtable<FlatNode, Boolean> gen = curr.get(read);
@@ -1030,80 +1070,119 @@ public class DefinitelyWrittenCheck {
     // caller
     calleeUnionBoundReadSet.clear();
     calleeIntersectBoundOverWriteSet.clear();
+    calleeBoundWriteSet.clear();
 
-    MethodDescriptor mdCallee = fc.getMethod();
-    FlatMethod fmCallee = state.getMethodFlat(mdCallee);
-    Set<MethodDescriptor> setPossibleCallees = new HashSet<MethodDescriptor>();
-    TypeDescriptor typeDesc = fc.getThis().getType();
-    setPossibleCallees.addAll(callGraph.getMethods(mdCallee, typeDesc));
+    if (ssjava.isSSJavaUtil(fc.getMethod().getClassDesc())) {
+      // ssjava util case!
+      // have write effects on the first argument
+      TempDescriptor arg = fc.getArg(0);
+      NTuple<Descriptor> argHeapPath = computePath(arg);
+      calleeIntersectBoundOverWriteSet.add(argHeapPath);
+    } else {
+      MethodDescriptor mdCallee = fc.getMethod();
+      // FlatMethod fmCallee = state.getMethodFlat(mdCallee);
+      Set<MethodDescriptor> setPossibleCallees = new HashSet<MethodDescriptor>();
+      // setPossibleCallees.addAll(callGraph.getMethods(mdCallee, typeDesc));
+      setPossibleCallees.addAll(callGraph.getMethods(mdCallee));
 
-    // create mapping from arg idx to its heap paths
-    Hashtable<Integer, NTuple<Descriptor>> mapArgIdx2CallerArgHeapPath =
-        new Hashtable<Integer, NTuple<Descriptor>>();
+      // create mapping from arg idx to its heap paths
+      Hashtable<Integer, NTuple<Descriptor>> mapArgIdx2CallerArgHeapPath =
+          new Hashtable<Integer, NTuple<Descriptor>>();
 
-    // arg idx is starting from 'this' arg
-    NTuple<Descriptor> thisHeapPath = mapHeapPath.get(fc.getThis());
-    if (thisHeapPath == null) {
-      // method is called without creating new flat node representing 'this'
-      thisHeapPath = new NTuple<Descriptor>();
-      thisHeapPath.add(fc.getThis());
-    }
+      // arg idx is starting from 'this' arg
+      if (fc.getThis() != null) {
+        NTuple<Descriptor> thisHeapPath = mapHeapPath.get(fc.getThis());
+        if (thisHeapPath == null) {
+          // method is called without creating new flat node representing 'this'
+          thisHeapPath = new NTuple<Descriptor>();
+          thisHeapPath.add(fc.getThis());
+        }
 
-    mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath);
+        mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath);
+      }
 
-    for (int i = 0; i < fc.numArgs(); i++) {
-      TempDescriptor arg = fc.getArg(i);
-      NTuple<Descriptor> argHeapPath = computePath(arg);
-      mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(i + 1), argHeapPath);
-    }
+      for (int i = 0; i < fc.numArgs(); i++) {
+        TempDescriptor arg = fc.getArg(i);
+        NTuple<Descriptor> argHeapPath = computePath(arg);
+        mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(i + 1), argHeapPath);
+      }
 
-    for (Iterator iterator = setPossibleCallees.iterator(); iterator.hasNext();) {
-      MethodDescriptor callee = (MethodDescriptor) iterator.next();
-      FlatMethod calleeFlatMethod = state.getMethodFlat(callee);
+      for (Iterator iterator = setPossibleCallees.iterator(); iterator.hasNext();) {
+        MethodDescriptor callee = (MethodDescriptor) iterator.next();
+        FlatMethod calleeFlatMethod = state.getMethodFlat(callee);
 
-      // binding caller's args and callee's params
+        // binding caller's args and callee's params
 
-      Set<NTuple<Descriptor>> calleeReadSet = mapFlatMethodToRead.get(calleeFlatMethod);
-      if (calleeReadSet == null) {
-        calleeReadSet = new HashSet<NTuple<Descriptor>>();
-        mapFlatMethodToRead.put(calleeFlatMethod, calleeReadSet);
-      }
-      Set<NTuple<Descriptor>> calleeOverWriteSet = mapFlatMethodToOverWrite.get(calleeFlatMethod);
-      if (calleeOverWriteSet == null) {
-        calleeOverWriteSet = new HashSet<NTuple<Descriptor>>();
-        mapFlatMethodToOverWrite.put(calleeFlatMethod, calleeOverWriteSet);
-      }
+        Set<NTuple<Descriptor>> calleeReadSet = mapFlatMethodToRead.get(calleeFlatMethod);
+        if (calleeReadSet == null) {
+          calleeReadSet = new HashSet<NTuple<Descriptor>>();
+          mapFlatMethodToRead.put(calleeFlatMethod, calleeReadSet);
+        }
 
-      Hashtable<Integer, TempDescriptor> mapParamIdx2ParamTempDesc =
-          new Hashtable<Integer, TempDescriptor>();
-      for (int i = 0; i < calleeFlatMethod.numParameters(); i++) {
-        TempDescriptor param = calleeFlatMethod.getParameter(i);
-        mapParamIdx2ParamTempDesc.put(Integer.valueOf(i), param);
+        Set<NTuple<Descriptor>> calleeOverWriteSet = mapFlatMethodToOverWrite.get(calleeFlatMethod);
+
+        if (calleeOverWriteSet == null) {
+          calleeOverWriteSet = new HashSet<NTuple<Descriptor>>();
+          mapFlatMethodToOverWrite.put(calleeFlatMethod, calleeOverWriteSet);
+        }
+
+        Set<NTuple<Descriptor>> calleeWriteSet = mapFlatMethodToWrite.get(calleeFlatMethod);
+
+        if (calleeWriteSet == null) {
+          calleeWriteSet = new HashSet<NTuple<Descriptor>>();
+          mapFlatMethodToWrite.put(calleeFlatMethod, calleeWriteSet);
+        }
+
+        Hashtable<Integer, TempDescriptor> mapParamIdx2ParamTempDesc =
+            new Hashtable<Integer, TempDescriptor>();
+        int offset = 0;
+        if (calleeFlatMethod.getMethod().isStatic()) {
+          // static method does not have implicit 'this' arg
+          offset = 1;
+        }
+        for (int i = 0; i < calleeFlatMethod.numParameters(); i++) {
+          TempDescriptor param = calleeFlatMethod.getParameter(i);
+          mapParamIdx2ParamTempDesc.put(Integer.valueOf(i + offset), param);
+        }
+
+        Set<NTuple<Descriptor>> calleeBoundReadSet =
+            bindSet(calleeReadSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath);
+        // union of the current read set and the current callee's
+        // read set
+        calleeUnionBoundReadSet.addAll(calleeBoundReadSet);
+        Set<NTuple<Descriptor>> calleeBoundOverWriteSet =
+            bindSet(calleeOverWriteSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath);
+        // intersection of the current overwrite set and the current
+        // callee's
+        // overwrite set
+        merge(calleeIntersectBoundOverWriteSet, calleeBoundOverWriteSet);
+
+        Set<NTuple<Descriptor>> boundWriteSetFromCallee =
+            bindSet(calleeWriteSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath);
+        calleeBoundWriteSet.addAll(boundWriteSetFromCallee);
       }
 
-      Set<NTuple<Descriptor>> calleeBoundReadSet =
-          bindSet(calleeReadSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath);
-      // union of the current read set and the current callee's
-      // read set
-      calleeUnionBoundReadSet.addAll(calleeBoundReadSet);
-      Set<NTuple<Descriptor>> calleeBoundWriteSet =
-          bindSet(calleeOverWriteSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath);
-      // intersection of the current overwrite set and the current
-      // callee's
-      // overwrite set
-      merge(calleeIntersectBoundOverWriteSet, calleeBoundWriteSet);
     }
 
   }
 
   private void checkFlag(boolean booleanValue, FlatNode fn, NTuple<Descriptor> hp) {
     if (booleanValue) {
-      throw new Error(
-          "There is a variable, which is reachable through references "
-              + hp
-              + ", who comes back to the same read statement without being overwritten at the out-most iteration at "
-              + methodContainingSSJavaLoop.getClassDesc().getSourceFileName() + "::"
-              + fn.getNumLine());
+      // the definitely written analysis only takes care about locations that
+      // are written to inside of the SSJava loop
+      for (Iterator iterator = calleeBoundWriteSet.iterator(); iterator.hasNext();) {
+        NTuple<Descriptor> write = (NTuple<Descriptor>) iterator.next();
+        if (hp.startsWith(write)) {
+          // it has write effect!
+          //throw new Error(
+          System.out.println("###"+
+              "There is a variable, which is reachable through references "
+                  + hp
+                  + ", who comes back to the same read statement without being overwritten at the out-most iteration at "
+                  + methodContainingSSJavaLoop.getClassDesc().getSourceFileName() + "::"
+                  + fn.getNumLine());
+        }
+      }
     }
   }
 
@@ -1174,15 +1253,19 @@ public class DefinitelyWrittenCheck {
 
       Set<NTuple<Descriptor>> readSet = new HashSet<NTuple<Descriptor>>();
       Set<NTuple<Descriptor>> overWriteSet = new HashSet<NTuple<Descriptor>>();
+      Set<NTuple<Descriptor>> writeSet = new HashSet<NTuple<Descriptor>>();
 
-      methodReadOverWrite_analyzeMethod(fm, readSet, overWriteSet);
+      methodReadOverWrite_analyzeMethod(fm, readSet, overWriteSet, writeSet);
 
       Set<NTuple<Descriptor>> prevRead = mapFlatMethodToRead.get(fm);
       Set<NTuple<Descriptor>> prevOverWrite = mapFlatMethodToOverWrite.get(fm);
+      Set<NTuple<Descriptor>> prevWrite = mapFlatMethodToWrite.get(fm);
 
-      if (!(readSet.equals(prevRead) && overWriteSet.equals(prevOverWrite))) {
+      if (!(readSet.equals(prevRead) && overWriteSet.equals(prevOverWrite) && writeSet
+          .equals(prevWrite))) {
         mapFlatMethodToRead.put(fm, readSet);
         mapFlatMethodToOverWrite.put(fm, overWriteSet);
+        mapFlatMethodToWrite.put(fm, writeSet);
 
         // results for callee changed, so enqueue dependents caller for
         // further
@@ -1204,7 +1287,7 @@ public class DefinitelyWrittenCheck {
   }
 
   private void methodReadOverWrite_analyzeMethod(FlatMethod fm, Set<NTuple<Descriptor>> readSet,
-      Set<NTuple<Descriptor>> overWriteSet) {
+      Set<NTuple<Descriptor>> overWriteSet, Set<NTuple<Descriptor>> writeSet) {
     if (state.SSJAVADEBUG) {
       System.out.println("Definitely written Analyzing: " + fm);
     }
@@ -1227,7 +1310,7 @@ public class DefinitelyWrittenCheck {
         }
       }
 
-      methodReadOverWrite_nodeActions(fn, curr, readSet, overWriteSet);
+      methodReadOverWrite_nodeActions(fn, curr, readSet, overWriteSet, writeSet);
 
       Set<NTuple<Descriptor>> writtenSetPrev = mapFlatNodeToWrittenSet.get(fn);
       if (!curr.equals(writtenSetPrev)) {
@@ -1240,10 +1323,12 @@ public class DefinitelyWrittenCheck {
 
     }
 
+
   }
 
   private void methodReadOverWrite_nodeActions(FlatNode fn, Set<NTuple<Descriptor>> writtenSet,
-      Set<NTuple<Descriptor>> readSet, Set<NTuple<Descriptor>> overWriteSet) {
+      Set<NTuple<Descriptor>> readSet, Set<NTuple<Descriptor>> overWriteSet,
+      Set<NTuple<Descriptor>> writeSet) {
     TempDescriptor lhs;
     TempDescriptor rhs;
     FieldDescriptor fld;
@@ -1320,7 +1405,7 @@ public class DefinitelyWrittenCheck {
           }
         }
 
-        //no need to kill hp(x.f) from WT
+        // no need to kill hp(x.f) from WT
       }
 
     }
@@ -1356,6 +1441,8 @@ public class DefinitelyWrittenCheck {
         // write(x.f)
         // need to add hp(y) to WT
         writtenSet.add(newHeapPath);
+
+        writeSet.add(newHeapPath);
       }
 
     }
@@ -1365,26 +1452,31 @@ public class DefinitelyWrittenCheck {
 
       FlatCall fc = (FlatCall) fn;
 
-      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);
-          }
-        }
+      bindHeapPathCallerArgWithCaleeParam(fc);
 
-        // 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 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 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 WRITE_BOUND set, to the
+      // caller's writeSet
+      for (Iterator iterator = calleeBoundWriteSet.iterator(); iterator.hasNext();) {
+        NTuple<Descriptor> write = (NTuple<Descriptor>) iterator.next();
+        writeSet.add(write);
+      }
 
     }
       break;
@@ -1521,7 +1613,6 @@ public class DefinitelyWrittenCheck {
 
       NTuple<Descriptor> callerArgHeapPath = mapCallerArgIdx2HeapPath.get(idx);
       TempDescriptor calleeParam = mapParamIdx2ParamTempDesc.get(idx);
-
       for (Iterator iterator2 = calleeSet.iterator(); iterator2.hasNext();) {
         NTuple<Descriptor> element = (NTuple<Descriptor>) iterator2.next();
         if (element.startsWith(calleeParam)) {

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 89ba80910b6723329e45ed83585ce2f935ed350c..259893ce05396cae07296c3fb0cdea3968be48d1 100644 (file)
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -852,7 +852,8 @@ public class FlowDownCheck {
       isSystemout = baseName.getSymbol().equals("System.out");
     }
 
-    if (!ssjava.isTrustMethod(calleeMD) && !calleeMD.getModifiers().isNative() && !isSystemout) {
+    if (!ssjava.isSSJavaUtil(calleeMD.getClassDesc()) && !ssjava.isTrustMethod(calleeMD)
+        && !calleeMD.getModifiers().isNative() && !isSystemout) {
 
       CompositeLocation baseLocation = null;
       if (min.getExpression() != null) {
@@ -897,7 +898,8 @@ public class FlowDownCheck {
 
       checkCalleeConstraints(md, nametable, min, baseLocation, constraint);
 
-      checkCallerArgumentLocationConstraints(md, nametable, min, baseLocation, constraint);
+      // checkCallerArgumentLocationConstraints(md, nametable, min,
+      // baseLocation, constraint);
 
       if (!min.getMethod().getReturnType().isVoid()) {
         // If method has a return value, compute the highest possible return
@@ -1359,13 +1361,13 @@ public class FlowDownCheck {
         return loc;
       }
     }
-    
-    if(left instanceof ArrayAccessNode){
+
+    if (left instanceof ArrayAccessNode) {
       System.out.println("HEREE!!");
-      ArrayAccessNode aan=(ArrayAccessNode)left;
-      left=aan.getExpression();
+      ArrayAccessNode aan = (ArrayAccessNode) left;
+      left = aan.getExpression();
     }
-    
+
     loc = checkLocationFromExpressionNode(md, nametable, left, loc, constraint, false);
     System.out.println("### checkLocationFromFieldAccessNode=" + fan.printNode(0));
     System.out.println("### left=" + left.printNode(0));
@@ -1373,7 +1375,7 @@ public class FlowDownCheck {
       Location fieldLoc = getFieldLocation(fd);
       loc.addLocation(fieldLoc);
     }
-    System.out.println("### field loc="+loc);
+    System.out.println("### field loc=" + loc);
     return loc;
   }
 

diff --git a/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java b/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java
index 778c0553c5fe3699a88a79d060ce14bdcfd677c8..b4a862a4560c030c1cb8bdc1cdb4e3d21f213aa1 100644 (file)
--- a/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java
+++ b/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java
@@ -64,7 +64,7 @@ public class MethodAnnotationCheck {
       ClassDescriptor cd = (ClassDescriptor) obj;
       toanalyze.remove(cd);
 
-      if (!cd.isInterface()) {
+      if (!ssjava.isSSJavaUtil(cd) && !cd.isInterface()) {
         for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
           MethodDescriptor md = (MethodDescriptor) method_it.next();
           checkTrustworthyMethodAnnotation(md);

diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
index fb1376330ce1704563d39494679e8a8920bf9bee..28635cab814d01d53f614bb8b247b91a15a33f41 100644 (file)
--- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
+++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
@@ -97,16 +97,16 @@ public class SSJavaAnalysis {
     this.mapSharedLocation2DescriptorSet = new Hashtable<Location, Set<Descriptor>>();
     this.linearTypeCheckMethodSet = new HashSet<MethodDescriptor>();
     this.bf = bf;
-    trustWorthyMDSet = new HashSet<MethodDescriptor>();
+    this.trustWorthyMDSet = new HashSet<MethodDescriptor>();
   }
 
   public void doCheck() {
     doMethodAnnotationCheck();
     // computeLinearTypeCheckMethodSet();
     // doLinearTypeCheck();
-    // if (state.SSJAVADEBUG) {
-    // debugPrint();
-    // }
+    if (state.SSJAVADEBUG) {
+      debugPrint();
+    }
     parseLocationAnnotation();
     // doFlowDownCheck();
     doDefinitelyWrittenCheck();
@@ -450,8 +450,10 @@ public class SSJavaAnalysis {
     ClassDescriptor cd = md.getClassDesc();
     // if a method requires to be annotated, class containg that method also
     // requires to be annotated
-    annotationRequireClassSet.add(cd);
-    annotationRequireSet.add(md);
+    if (!isSSJavaUtil(cd)) {
+      annotationRequireClassSet.add(cd);
+      annotationRequireSet.add(md);
+    }
   }
 
   public Set<MethodDescriptor> getAnnotationRequireSet() {
@@ -504,4 +506,11 @@ public class SSJavaAnalysis {
   public void setMethodContainingSSJavaLoop(MethodDescriptor methodContainingSSJavaLoop) {
     this.methodContainingSSJavaLoop = methodContainingSSJavaLoop;
   }
+
+  public boolean isSSJavaUtil(ClassDescriptor cd) {
+    if (cd.getSymbol().equals("SSJAVA")) {
+      return true;
+    }
+    return false;
+  }
 }

diff --git a/Robust/src/ClassLibrary/SSJava/SSJAVA.java b/Robust/src/ClassLibrary/SSJava/SSJAVA.java
new file mode 100644 (file)
index 0000000..fbe5dad
--- /dev/null
+++ b/Robust/src/ClassLibrary/SSJava/SSJAVA.java
@@ -0,0 +1,47 @@
+public class SSJAVA {
+
+  // Definitely written analysis assumes that the first parameter may have write
+  // effects through the below methods
+
+  static void arrayinit(float array[], float value) {
+    for (int i = 0; i < array.length; i++) {
+      array[i] = value;
+    }
+  }
+
+  static void arrayinit(int array[], int value) {
+    for (int i = 0; i < array.length; i++) {
+      array[i] = value;
+    }
+  }
+
+  static void arrayinit(float array[][][], int size_1, int size_2, int size_3, float value) {
+
+    for (int idx1 = 0; idx1 < size_1; idx1++) {
+      if (array[idx1].length != size_2) {
+        throw new Error("Array initilizatiion failed to assign to all of elements.");
+      }
+      for (int idx2 = 0; idx2 < size_2; idx2++) {
+        if (array[idx1][idx2].length != size_2) {
+          throw new Error("Array initilizatiion failed to assign to all of elements.");
+        }
+        for (int idx3 = 0; idx3 < size_3; idx3++) {
+          array[idx1][idx2][idx3] = value;
+        }
+      }
+    }
+  }
+
+  static void arrayinit(float array[][], int size_1, int size_2, float value) {
+
+    for (int idx1 = 0; idx1 < size_1; idx1++) {
+      if (array[idx1].length != size_2) {
+        throw new Error("Array initilizatiion failed to assign to all of elements.");
+      }
+      for (int idx2 = 0; idx2 < size_2; idx2++) {
+        array[idx1][idx2] = value;
+      }
+    }
+  }
+
+}

diff --git a/Robust/src/Tests/ssJava/mp3decoder/Decoder.java b/Robust/src/Tests/ssJava/mp3decoder/Decoder.java
index 944868477e6c7bb3a0a154121b9436ff5ac92020..12287b1c94b781f71e4386edcfaa535aa79355d1 100644 (file)
--- a/Robust/src/Tests/ssJava/mp3decoder/Decoder.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/Decoder.java
@@ -127,6 +127,35 @@ public class Decoder implements DecoderErrors {
   // if (filter2 != null)\r
   // filter2.setEQ(factors);\r
   // }\r
+  @LATTICE("THIS<VAR,THISLOC=THIS,VAR*")\r
+  public void init( @LOC("THIS,Decoder.H") Header header) {\r
+    @LOC("VAR") float scalefactor = 32700.0f;\r
+\r
+    @LOC("THIS,Decoder.PARAM") int mode = header.mode();\r
+    @LOC("THIS,Decoder.PARAM") int layer = header.layer();\r
+    @LOC("THIS,Decoder.PARAM") int channels = mode == Header.SINGLE_CHANNEL ? 1 : 2;\r
+\r
+    // set up output buffer if not set up by client.\r
+    // if (output == null)\r
+    // output = new SampleBuffer(header.frequency(), channels);\r
+    SampleBufferWrapper.init(header.frequency(), channels);\r
+\r
+    @LOC("THIS,Decoder.FACTORS") float[] factors = equalizer.getBandFactors();\r
+    @LOC("THIS,Decoder.FILTER") SynthesisFilter filter1 =\r
+        new SynthesisFilter(0, scalefactor, factors);\r
+\r
+    // REVIEW: allow mono output for stereo\r
+    @LOC("THIS,Decoder.FILTER") SynthesisFilter filter2 = null;\r
+    if (channels == 2) {\r
+      filter2 = new SynthesisFilter(1, scalefactor, factors);\r
+    }\r
+\r
+    outputChannels = channels;\r
+    outputFrequency = header.frequency();\r
+\r
+    l3decoder = new LayerIIIDecoder(header,filter1, filter2, OutputChannels.BOTH_CHANNELS);\r
+\r
+  }\r
 \r
   /**\r
    * Decodes one frame from an MPEG audio bitstream.\r
@@ -141,36 +170,6 @@ public class Decoder implements DecoderErrors {
   @LATTICE("THIS<VAR,THISLOC=THIS,VAR*")\r
   public void decodeFrame(@LOC("THIS,Decoder.H") Header header) throws DecoderException {\r
 \r
-    if (!initialized) {\r
-      @LOC("VAR") float scalefactor = 32700.0f;\r
-\r
-      @LOC("THIS,Decoder.PARAM") int mode = header.mode();\r
-      @LOC("THIS,Decoder.PARAM") int layer = header.layer();\r
-      @LOC("THIS,Decoder.PARAM") int channels = mode == Header.SINGLE_CHANNEL ? 1 : 2;\r
-\r
-      // set up output buffer if not set up by client.\r
-      // if (output == null)\r
-      // output = new SampleBuffer(header.frequency(), channels);\r
-      SampleBufferWrapper.init(header.frequency(), channels);\r
-\r
-      @LOC("THIS,Decoder.FACTORS") float[] factors = equalizer.getBandFactors();\r
-      @LOC("THIS,Decoder.FILTER") SynthesisFilter filter1 =\r
-          new SynthesisFilter(0, scalefactor, factors);\r
-\r
-      // REVIEW: allow mono output for stereo\r
-      @LOC("THIS,Decoder.FILTER") SynthesisFilter filter2 = null;\r
-      if (channels == 2) {\r
-        filter2 = new SynthesisFilter(1, scalefactor, factors);\r
-      }\r
-\r
-      outputChannels = channels;\r
-      outputFrequency = header.frequency();\r
-\r
-      l3decoder = new LayerIIIDecoder(filter1, filter2, OutputChannels.BOTH_CHANNELS);\r
-\r
-      initialized = true;\r
-    }\r
-\r
     SampleBufferWrapper.clear_buffer();\r
     l3decoder.decode(header);\r
     // SampleBufferWrapper.getOutput().write_buffer(1);\r

diff --git a/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java b/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java
index 8714428bb07d9728353fddea7c47c1e4c08cc26b..602ea5b1f34c67e7a7ba4579230184c0a2d43135 100644 (file)
--- a/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/LayerIIIDecoder.java
@@ -113,7 +113,7 @@ final class LayerIIIDecoder implements FrameDecoder {
   private boolean initialized = false;
 
   // constructor for the linear type system
-  public LayerIIIDecoder(@DELEGATE @LOC("VAR") SynthesisFilter filtera,
+  public LayerIIIDecoder(Header h, @DELEGATE @LOC("VAR") SynthesisFilter filtera,
       @DELEGATE @LOC("VAR") SynthesisFilter filterb, @LOC("VAR") int which_ch0) {
 
     filter1 = filtera;
@@ -205,6 +205,7 @@ final class LayerIIIDecoder implements FrameDecoder {
     scalefac_buffer = new int[54];
     // END OF scalefac_buffer
 
+    init(h);
   }
 
   @LATTICE("THIS<C,THIS<IN,C*,THISLOC=THIS")
@@ -456,13 +457,22 @@ final class LayerIIIDecoder implements FrameDecoder {
   @LATTICE("HEADER<VAR,VAR<THIS,C<THIS,THIS<IN,THISLOC=THIS,C*,VAR*")
   public void decode(@LOC("THIS,LayerIIIDecoder.HD") Header header) {
 
-    if (!initialized) {
-      init(header);
-    }
+    // if (!initialized) {
+    // init(header);
+    // }
 
     // overwrites once per a loop
-    samples1 = new float[32];
-    samples2 = new float[32];
+    SSJAVA.arrayinit(samples1, 0);
+    SSJAVA.arrayinit(samples2, 0);
+    SSJAVA.arrayinit(ro, 2, SBLIMIT, SSLIMIT, 0);
+    SSJAVA.arrayinit(lr, 2, SBLIMIT, SSLIMIT, 0);
+    SSJAVA.arrayinit(is_pos, 7);
+    SSJAVA.arrayinit(is_ratio, 0);
+    SSJAVA.arrayinit(out_1d, 0);
+    SSJAVA.arrayinit(inter, 0);
+    SSJAVA.arrayinit(k, 2, SBLIMIT * SSLIMIT, 0);
+    SSJAVA.arrayinit(is_1d, 0);
+    CheckSumHuff = 0;
     // prevblck = new float[2][SBLIMIT * SSLIMIT];
     si = new III_side_info_t();
     //
@@ -1379,9 +1389,9 @@ final class LayerIIIDecoder implements FrameDecoder {
 
     if ((si.ch[ch].gr[gr].window_switching_flag != 0) && (si.ch[ch].gr[gr].block_type == 2)) {
 
-      for (index = 0; index < 576; index++) {
-        inter[index] = 0.0f;
-      }
+      // for (index = 0; index < 576; index++) {
+      // inter[index] = 0.0f;
+      // }
 
       if (si.ch[ch].gr[gr].mixed_block_flag != 0) {
         // NO REORDER FOR LOW 2 SUBBANDS
@@ -1495,12 +1505,10 @@ final class LayerIIIDecoder implements FrameDecoder {
       @LOC("THIS,LayerIIIDecoder.LR") int io_type = (si.ch[0].gr[gr].scalefac_compress & 1);
 
       // initialization
-
-      for (i = 0; i < 576; i++) {
-        is_pos[i] = 7;
-
-        is_ratio[i] = 0.0f;
-      }
+      // for (i = 0; i < 576; i++) {
+      // is_pos[i] = 7;
+      // is_ratio[i] = 0.0f;
+      // }
 
       if (i_stereo) {
         if ((si.ch[0].gr[gr].window_switching_flag != 0) && (si.ch[0].gr[gr].block_type == 2)) {

diff --git a/Robust/src/Tests/ssJava/mp3decoder/Player.java b/Robust/src/Tests/ssJava/mp3decoder/Player.java
index d82e6e8919b8d49bad2ce04a23a01650e13aa970..e3a92107591b6890580c11cb63f1daaeb2a5da71 100644 (file)
--- a/Robust/src/Tests/ssJava/mp3decoder/Player.java
+++ b/Robust/src/Tests/ssJava/mp3decoder/Player.java
@@ -107,16 +107,22 @@ public class Player {
    * @return true if the last frame was played, or false if there are more\r
    *         frames.\r
    */\r
-  @LATTICE("T<IN,T*,IN*,THISLOC=T")\r
-  @RETURNLOC("T")\r
+  @LATTICE("OUT<THIS,THIS<IN,IN*,THISLOC=THIS")\r
+  @RETURNLOC("OUT")\r
   public boolean play(@LOC("IN") int frames) throws JavaLayerException {\r
-    @LOC("T") boolean ret = true;\r
-    \r
-    @LOC("T") int count=0;\r
+    @LOC("OUT") boolean ret = true;\r
+\r
+    // initialization before ssjava loop\r
+    @LOC("THIS,Player.FR") boolean init = true;\r
+    @LOC("THIS,Player.ST") Header h = BitstreamWrapper.readFrame();\r
+    decoder.init(h);\r
+\r
+    @LOC("IN") int count = 0;\r
     SSJAVA: while (count++ < 2147483646) {\r
-      ret = decodeFrame();\r
-      if(!ret){\r
-          break;\r
+      ret = decodeFrame(init, h);\r
+      init = false;\r
+      if (!ret) {\r
+        break;\r
       }\r
     }\r
 \r
@@ -175,14 +181,17 @@ public class Player {
    * @return true if there are no more frames to decode, false otherwise.\r
    */\r
   @LATTICE("C<THIS,O<THIS,THIS<IN,C*,THISLOC=THIS,RETURNLOC=O,GLOBALLOC=THIS")\r
-  protected boolean decodeFrame() throws JavaLayerException {\r
+  protected boolean decodeFrame(@LOC("THIS,Player.FR") boolean init, @LOC("THIS,Player.ST") Header h)\r
+      throws JavaLayerException {\r
     try {\r
       // AudioDevice out = audio;\r
       // if (out==null)\r
       // return false;\r
 \r
       // Header h = bitstream.readFrame();\r
-      @LOC("THIS,Player.ST") Header h = BitstreamWrapper.readFrame();\r
+      if (!init) {\r
+        h = BitstreamWrapper.readFrame();\r
+      }\r
 \r
       if (h == null)\r
         return false;\r
@@ -194,8 +203,7 @@ public class Player {
       @LOC("C") int sum = 0;\r
       @LOC("C") short[] outbuf = SampleBufferWrapper.getBuffer();\r
       // short[] outbuf = output.getBuffer();\r
-      TERMINATE:\r
-      for (@LOC("C") int i = 0; i < SampleBufferWrapper.getBufferLength(); i++) {\r
+      TERMINATE: for (@LOC("C") int i = 0; i < SampleBufferWrapper.getBufferLength(); i++) {\r
         // System.out.println(outbuf[i]);\r
         sum += outbuf[i];\r
       }\r