fixes on method annoatation checking: when a method needs to be annotated, all of...
authoryeom <yeom>
Wed, 20 Jul 2011 21:50:05 +0000 (21:50 +0000)
committeryeom <yeom>
Wed, 20 Jul 2011 21:50:05 +0000 (21:50 +0000)
Robust/src/Analysis/SSJava/FlowDownCheck.java
Robust/src/Analysis/SSJava/MethodAnnotationCheck.java
Robust/src/Analysis/SSJava/SSJavaAnalysis.java
Robust/src/Tests/ssJava/mp3decoder/LayerIDecoder.java
Robust/src/Tests/ssJava/mp3decoder/Obuffer.java
Robust/src/Tests/ssJava/mp3decoder/Subband.java

index 4589aaca24fe1ceea100100b0e069d8be49aeeb1..41439daac6f3976d774d59078f981f69d027be1e 100644 (file)
@@ -100,16 +100,17 @@ public class FlowDownCheck {
     // desciptor' & 'location'
     toanalyze.addAll(classtable.getValueSet());
     toanalyze.addAll(state.getTaskSymbolTable().getValueSet());
+
     while (!toanalyze.isEmpty()) {
       Object obj = toanalyze.iterator().next();
       ClassDescriptor cd = (ClassDescriptor) obj;
       toanalyze.remove(cd);
 
-      if (ssjava.needToBeAnnoated(cd) && (!cd.isInterface())) {
+      if (ssjava.needToBeAnnoated(cd)) {
 
         ClassDescriptor superDesc = cd.getSuperDesc();
-        if (superDesc != null && (!superDesc.isInterface())
-            && (!superDesc.getSymbol().equals("Object"))) {
+
+        if (superDesc != null && (!superDesc.getSymbol().equals("Object"))) {
           checkOrderingInheritance(superDesc, cd);
         }
 
@@ -151,7 +152,8 @@ public class FlowDownCheck {
     SSJavaLattice<String> subLattice = ssjava.getClassLattice(cd);
 
     if (superLattice != null) {
-
+      // if super class doesn't define lattice, then we don't need to check its
+      // subclass
       if (subLattice == null) {
         throw new Error("If a parent class '" + superCd
             + "' has a ordering lattice, its subclass '" + cd + "' should have one.");
@@ -169,10 +171,32 @@ public class FlowDownCheck {
               + "' that is defined by its superclass '" + superCd + "'.");
         }
       }
+    }
+
+    MethodLattice<String> superMethodDefaultLattice = ssjava.getMethodDefaultLattice(superCd);
+    MethodLattice<String> subMethodDefaultLattice = ssjava.getMethodDefaultLattice(cd);
+
+    if (superMethodDefaultLattice != null) {
+      if (subMethodDefaultLattice == null) {
+        throw new Error("When a parent class '" + superCd
+            + "' defines a default method lattice, its subclass '" + cd + "' should define one.");
+      }
+
+      Set<Pair<String, String>> superPairSet = superMethodDefaultLattice.getOrderingPairSet();
+      Set<Pair<String, String>> subPairSet = subMethodDefaultLattice.getOrderingPairSet();
+
+      for (Iterator iterator = superPairSet.iterator(); iterator.hasNext();) {
+        Pair<String, String> pair = (Pair<String, String>) iterator.next();
+
+        if (!subPairSet.contains(pair)) {
+          throw new Error("Subclass '" + cd + "' does not have the relative ordering '"
+              + pair.getSecond() + " < " + pair.getFirst()
+              + "' that is defined by its superclass '" + superCd
+              + "' in the method default lattice.");
+        }
+      }
 
     }
-    // if super class doesn't define lattice, then we don't need to check its
-    // subclass
 
   }
 
@@ -183,9 +207,9 @@ public class FlowDownCheck {
   private void checkDeclarationInMethodBody(ClassDescriptor cd, MethodDescriptor md) {
     BlockNode bn = state.getMethodBody(md);
 
-    // parsing returnloc annotation
     if (ssjava.needTobeAnnotated(md)) {
 
+      // parsing returnloc annotation
       Vector<AnnotationDescriptor> methodAnnotations = md.getModifiers().getAnnotations();
       if (methodAnnotations != null) {
         for (int i = 0; i < methodAnnotations.size(); i++) {
@@ -198,44 +222,42 @@ public class FlowDownCheck {
             md2ReturnLoc.put(md, returnLocComp);
           }
         }
-
         if (!md.getReturnType().isVoid() && !md2ReturnLoc.containsKey(md)) {
           throw new Error("Return location is not specified for the method " + md + " at "
               + cd.getSourceFileName());
         }
-
       }
-    }
 
-    List<CompositeLocation> paramList = new ArrayList<CompositeLocation>();
+      List<CompositeLocation> paramList = new ArrayList<CompositeLocation>();
 
-    boolean hasReturnValue = (!md.getReturnType().isVoid());
-    if (hasReturnValue) {
-      MethodLattice<String> methodLattice = ssjava.getMethodLattice(md);
-      String thisLocId = methodLattice.getThisLoc();
-      if (thisLocId == null) {
-        throw new Error("Method '" + md + "' does not have the definition of 'this' location at "
-            + md.getClassDesc().getSourceFileName());
+      boolean hasReturnValue = (!md.getReturnType().isVoid());
+      if (hasReturnValue) {
+        MethodLattice<String> methodLattice = ssjava.getMethodLattice(md);
+        String thisLocId = methodLattice.getThisLoc();
+        if (thisLocId == null) {
+          throw new Error("Method '" + md + "' does not have the definition of 'this' location at "
+              + md.getClassDesc().getSourceFileName());
+        }
+        CompositeLocation thisLoc = new CompositeLocation(new Location(md, thisLocId));
+        paramList.add(thisLoc);
       }
-      CompositeLocation thisLoc = new CompositeLocation(new Location(md, thisLocId));
-      paramList.add(thisLoc);
-    }
 
-    for (int i = 0; i < md.numParameters(); i++) {
-      // process annotations on method parameters
-      VarDescriptor vd = (VarDescriptor) md.getParameter(i);
-      assignLocationOfVarDescriptor(vd, md, md.getParameterTable(), bn);
-      if (hasReturnValue) {
-        paramList.add(d2loc.get(vd));
+      for (int i = 0; i < md.numParameters(); i++) {
+        // process annotations on method parameters
+        VarDescriptor vd = (VarDescriptor) md.getParameter(i);
+        assignLocationOfVarDescriptor(vd, md, md.getParameterTable(), bn);
+        if (hasReturnValue) {
+          paramList.add(d2loc.get(vd));
+        }
       }
-    }
 
-    if (hasReturnValue) {
-      md2ReturnLocGen.put(md, new ReturnLocGenerator(md2ReturnLoc.get(md), paramList,
-          generateErrorMessage(cd, null)));
+      if (hasReturnValue) {
+        md2ReturnLocGen.put(md, new ReturnLocGenerator(md2ReturnLoc.get(md), paramList,
+            generateErrorMessage(cd, null)));
+      }
+      checkDeclarationInBlockNode(md, md.getParameterTable(), bn);
     }
 
-    checkDeclarationInBlockNode(md, md.getParameterTable(), bn);
   }
 
   private void checkDeclarationInBlockNode(MethodDescriptor md, SymbolTable nametable, BlockNode bn) {
@@ -403,15 +425,26 @@ public class FlowDownCheck {
 
     ExpressionNode returnExp = rn.getReturnExpression();
 
-    CompositeLocation expLoc;
+    CompositeLocation returnValueLoc;
     if (returnExp != null) {
-      expLoc = checkLocationFromExpressionNode(md, nametable, returnExp, new CompositeLocation());
+      returnValueLoc =
+          checkLocationFromExpressionNode(md, nametable, returnExp, new CompositeLocation());
+
       // check if return value is equal or higher than RETRUNLOC of method
       // declaration annotation
-      CompositeLocation returnLocAt = md2ReturnLoc.get(md);
+      CompositeLocation declaredReturnLoc = md2ReturnLoc.get(md);
 
-      if (CompositeLattice
-          .compare(returnLocAt, expLoc, generateErrorMessage(md.getClassDesc(), rn)) != ComparisonResult.LESS) {
+      System.out.println("\nreturnLocAt=" + declaredReturnLoc);
+      System.out.println("returnValueLoc=" + returnValueLoc);
+      System.out.println("COMPARE RESULT="
+          + CompositeLattice.compare(declaredReturnLoc, returnValueLoc,
+              generateErrorMessage(md.getClassDesc(), rn)));
+
+      int compareResult =
+          CompositeLattice.compare(returnValueLoc, declaredReturnLoc,
+              generateErrorMessage(md.getClassDesc(), rn));
+
+      if (compareResult == ComparisonResult.LESS || compareResult == ComparisonResult.INCOMPARABLE) {
         throw new Error(
             "Return value location is not equal or higher than the declaraed return location at "
                 + md.getClassDesc().getSourceFileName() + "::" + rn.getNumLine());
@@ -563,13 +596,15 @@ public class FlowDownCheck {
   private CompositeLocation checkLocationFromDeclarationNode(MethodDescriptor md,
       SymbolTable nametable, DeclarationNode dn) {
 
-    System.out.println("DeclarationNode=" + dn.printNode(0) + " "
+    System.out.println("##DeclarationNode=" + dn.printNode(0) + " "
         + generateErrorMessage(md.getClassDesc(), dn));
 
     VarDescriptor vd = dn.getVarDescriptor();
 
     CompositeLocation destLoc = d2loc.get(vd);
 
+    System.out.println("##DeclarationNode destLoc=" + destLoc + " of vd=" + vd + " of md=" + md);
+
     if (dn.getExpression() != null) {
       CompositeLocation expressionLoc =
           checkLocationFromExpressionNode(md, nametable, dn.getExpression(),
@@ -772,9 +807,9 @@ public class FlowDownCheck {
     }
 
     System.out.println("##");
-    System.out.println("min.getMethod()=" + min.getMethod());
-    System.out.println("md2ReturnLocGen.get(min.getMethod())="
-        + md2ReturnLocGen.get(min.getMethod()));
+    System.out.println("min.getMethod()=" + min.getMethod() + " argList=" + argList);
+    System.out.println("computeReturnLocation="
+        + md2ReturnLocGen.get(min.getMethod()).computeReturnLocation(argList));
 
     return md2ReturnLocGen.get(min.getMethod()).computeReturnLocation(argList);
 
@@ -783,6 +818,8 @@ public class FlowDownCheck {
   private void checkCalleeConstraints(MethodDescriptor md, SymbolTable nametable,
       MethodInvokeNode min) {
 
+    System.out.println("checkCalleeConstraints " + generateErrorMessage(md.getClassDesc(), min));
+
     if (min.numArgs() > 1) {
       // caller needs to guarantee that it passes arguments in regarding to
       // callee's hierarchy
@@ -808,12 +845,16 @@ public class FlowDownCheck {
               VarDescriptor calleevd2 = (VarDescriptor) min.getMethod().getParameter(currentIdx);
               CompositeLocation calleeLoc2 = d2loc.get(calleevd2);
 
+              System.out.println("#callerResult=" + callerArg1 + " " + callerArg2);
+              System.out.println("#calleeResult=" + calleeLoc1 + " " + calleeLoc2);
+
               int callerResult =
                   CompositeLattice.compare(callerArg1, callerArg2,
                       generateErrorMessage(md.getClassDesc(), min));
               int calleeResult =
                   CompositeLattice.compare(calleeLoc1, calleeLoc2,
                       generateErrorMessage(md.getClassDesc(), min));
+
               if (calleeResult == ComparisonResult.GREATER
                   && callerResult != ComparisonResult.GREATER) {
                 // If calleeLoc1 is higher than calleeLoc2
@@ -1088,12 +1129,13 @@ public class FlowDownCheck {
       }
       srcLocation = new CompositeLocation();
       srcLocation = checkLocationFromExpressionNode(md, nametable, an.getSrc(), srcLocation);
-      
-//      System.out.println(" an= " + an.printNode(0) + " an.getSrc()=" + an.getSrc().getClass()
-//          + " at " + cd.getSourceFileName() + "::" + an.getNumLine());
-//      System.out.println("srcLocation=" + srcLocation);
-//      System.out.println("dstLocation=" + destLocation);
-      
+
+      // System.out.println(" an= " + an.printNode(0) + " an.getSrc()=" +
+      // an.getSrc().getClass()
+      // + " at " + cd.getSourceFileName() + "::" + an.getNumLine());
+      // System.out.println("srcLocation=" + srcLocation);
+      // System.out.println("dstLocation=" + destLocation);
+
       if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, generateErrorMessage(cd, an))) {
         throw new Error("The value flow from " + srcLocation + " to " + destLocation
             + " does not respect location hierarchy on the assignment " + an.printNode(0) + " at "
@@ -1120,41 +1162,39 @@ public class FlowDownCheck {
     ClassDescriptor cd = md.getClassDesc();
     Vector<AnnotationDescriptor> annotationVec = vd.getType().getAnnotationMarkers();
 
-    if (!md.getModifiers().isAbstract()) {
-      // currently enforce every variable to have corresponding location
-      if (annotationVec.size() == 0) {
-        throw new Error("Location is not assigned to variable " + vd.getSymbol()
-            + " in the method " + md.getSymbol() + " of the class " + cd.getSymbol());
-      }
-
-      if (annotationVec.size() > 1) { // variable can have at most one location
-        throw new Error(vd.getSymbol() + " has more than one location.");
-      }
+    // currently enforce every variable to have corresponding location
+    if (annotationVec.size() == 0) {
+      throw new Error("Location is not assigned to variable " + vd.getSymbol() + " in the method "
+          + md.getSymbol() + " of the class " + cd.getSymbol());
+    }
 
-      AnnotationDescriptor ad = annotationVec.elementAt(0);
+    if (annotationVec.size() > 1) { // variable can have at most one location
+      throw new Error(vd.getSymbol() + " has more than one location.");
+    }
 
-      if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {
+    AnnotationDescriptor ad = annotationVec.elementAt(0);
 
-        if (ad.getMarker().equals(SSJavaAnalysis.LOC)) {
-          String locDec = ad.getValue(); // check if location is defined
+    if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {
 
-          if (locDec.startsWith(SSJavaAnalysis.DELTA)) {
-            DeltaLocation deltaLoc = parseDeltaDeclaration(md, n, locDec);
-            d2loc.put(vd, deltaLoc);
-            addLocationType(vd.getType(), deltaLoc);
-          } else {
-            CompositeLocation compLoc = parseLocationDeclaration(md, n, locDec);
+      if (ad.getMarker().equals(SSJavaAnalysis.LOC)) {
+        String locDec = ad.getValue(); // check if location is defined
 
-            Location lastElement = compLoc.get(compLoc.getSize() - 1);
-            if (ssjava.isSharedLocation(lastElement)) {
-              ssjava.mapSharedLocation2Descriptor(lastElement, vd);
-            }
+        if (locDec.startsWith(SSJavaAnalysis.DELTA)) {
+          DeltaLocation deltaLoc = parseDeltaDeclaration(md, n, locDec);
+          d2loc.put(vd, deltaLoc);
+          addLocationType(vd.getType(), deltaLoc);
+        } else {
+          CompositeLocation compLoc = parseLocationDeclaration(md, n, locDec);
 
-            d2loc.put(vd, compLoc);
-            addLocationType(vd.getType(), compLoc);
+          Location lastElement = compLoc.get(compLoc.getSize() - 1);
+          if (ssjava.isSharedLocation(lastElement)) {
+            ssjava.mapSharedLocation2Descriptor(lastElement, vd);
           }
 
+          d2loc.put(vd, compLoc);
+          addLocationType(vd.getType(), compLoc);
         }
+
       }
     }
 
@@ -1361,7 +1401,7 @@ public class FlowDownCheck {
 
     public static int compare(CompositeLocation loc1, CompositeLocation loc2, String msg) {
 
-      // System.out.println("compare=" + loc1 + " " + loc2);
+      System.out.println("compare=" + loc1 + " " + loc2);
       int baseCompareResult = compareBaseLocationSet(loc1, loc2, false, msg);
 
       if (baseCompareResult == ComparisonResult.EQUAL) {
@@ -1691,6 +1731,12 @@ class ReturnLocGenerator {
     // compute GLB of arguments subset that are same or higher than return
     // location
     CompositeLocation glb = CompositeLattice.calculateGLB(inputGLB);
+
+    System.out.println("### computeReturnLocation");
+    System.out.println("### args=" + args);
+    System.out.println("### calculateGLB=" + inputGLB);
+    System.out.println("### glb=" + glb);
+
     return glb;
   }
 }
index f8145c56a3607c697decace0796dafd76a79cce2..d1914e0294d192d3a6b595c1d50888e8543679f2 100644 (file)
@@ -92,7 +92,6 @@ public class MethodAnnotationCheck {
 
             if (calleeMD.getClassDesc().isInterface()) {
               calleeMD.getClassDesc();
-
             }
 
             tovisit.add(calleeMD);
@@ -150,6 +149,35 @@ public class MethodAnnotationCheck {
           }
         }
       }
+
+      // need to check super classess if the current method is inherited from
+      // them, all of ancestor method should be annoated
+      ClassDescriptor currentCd = cd;
+      ClassDescriptor superCd = tu.getSuper(currentCd);
+      while (!superCd.getSymbol().equals("Object")) {
+        Set possiblematches = superCd.getMethodTable().getSet(md.getSymbol());
+        for (Iterator methodit = possiblematches.iterator(); methodit.hasNext();) {
+          MethodDescriptor matchmd = (MethodDescriptor) methodit.next();
+          if (md.matches(matchmd)) {
+            ssjava.addAnnotationRequire(matchmd);
+          }
+        }
+        currentCd = superCd;
+        superCd = tu.getSuper(currentCd);
+      }
+
+      Set<ClassDescriptor> superIFSet = tu.getSuperIFs(cd);
+      for (Iterator iterator = superIFSet.iterator(); iterator.hasNext();) {
+        ClassDescriptor parentInterface = (ClassDescriptor) iterator.next();
+        Set possiblematches = parentInterface.getMethodTable().getSet(md.getSymbol());
+        for (Iterator methodit = possiblematches.iterator(); methodit.hasNext();) {
+          MethodDescriptor matchmd = (MethodDescriptor) methodit.next();
+          if (md.matches(matchmd)) {
+            ssjava.addAnnotationRequire(matchmd);
+          }
+        }
+      }
+
     }
 
   }
index 80468a94ab9ef69733dfd916d09ba717d023d8d4..17db8a82f3b31da98bcc908b3545bad64b5a8a0c 100644 (file)
@@ -269,6 +269,10 @@ public class SSJavaAnalysis {
     return cd2lattice.get(cd);
   }
 
+  public MethodLattice<String> getMethodDefaultLattice(ClassDescriptor cd) {
+    return cd2methodDefault.get(cd);
+  }
+
   public MethodLattice<String> getMethodLattice(MethodDescriptor md) {
     if (md2lattice.containsKey(md)) {
       return md2lattice.get(md);
@@ -291,9 +295,10 @@ public class SSJavaAnalysis {
 
   public void addAnnotationRequire(MethodDescriptor md) {
 
+    ClassDescriptor cd = md.getClassDesc();
     // if a method requires to be annotated, class containg that method also
     // requires to be annotated
-    annotationRequireClassSet.add(md.getClassDesc());
+    annotationRequireClassSet.add(cd);
     annotationRequireSet.add(md);
   }
 
index dfc39286ba6554e7844f4650a31058de4c956725..b3572bf143acffcdc064cf1ac0c13b5885d54ffe 100644 (file)
         * and in derived class for intensity stereo mode
         */
      @LATTICE("S<L,L<H,H<SH,SH*,S*")
-       @METHODDEFAULT("OUT<V,V<SH,SH<IN,SH*,THISLOC=V,GLOBALLOC=IN")
+     @METHODDEFAULT("OUT<V,V<SH,SH<THIS,THIS<IN,SH*,THISLOC=THIS,GLOBALLOC=IN")
        static class SubbandLayer1 extends Subband
        {
 
         * Class for layer I subbands in joint stereo mode.
         */
      @LATTICE("S<L,L<H,H<SH,SH*")
-       @METHODDEFAULT("OUT<V,V<SH,SH<IN,SH*,THISLOC=V,GLOBALLOC=IN")
+     @METHODDEFAULT("OUT<V,V<SH,SH<THIS,THIS<IN,SH*,THISLOC=THIS,GLOBALLOC=IN")
        static class SubbandLayer1IntensityStereo extends SubbandLayer1
        {
          @LOC("L") protected float             channel2_scalefactor;
         * Class for layer I subbands in stereo mode.
         */     
      @LATTICE("S<L,L<H,H<SH,SH*,S*")
-       @METHODDEFAULT("OUT<V,V<SH,SH<IN,SH*,THISLOC=V,GLOBALLOC=IN")
+     @METHODDEFAULT("OUT<V,V<SH,SH<THIS,THIS<IN,SH*,THISLOC=THIS,GLOBALLOC=IN")
        static class SubbandLayer1Stereo extends SubbandLayer1
        {
          @LOC("H") protected int               channel2_allocation;
index 836ff889891d01e9e1b223e4c8be4bdc277bdd5d..2db93ef0c0bb2a287d8d031a635efa20a812cbd5 100644 (file)
@@ -46,7 +46,7 @@ public abstract class Obuffer
   /**
    * Takes a 16 Bit PCM sample.
    */
-  public abstract void append(int channel, short value);
+  public abstract void append(@LOC("IN") int channel, @LOC("IN") short value);
 
   /**
    * Accepts 32 new PCM samples. 
@@ -86,7 +86,7 @@ public abstract class Obuffer
   /**
    * Write the samples to the file or directly to the audio hardware.
    */
-  public abstract void write_buffer(int val);
+  public abstract void write_buffer(@LOC("IN") int val);
   public abstract void close();
 
   /**
index f6ad8c82da932ec15ccd5f328d127695de6bfd2e..bf0319ab22b4229b593bd23463d16b6d0e87ebe0 100644 (file)
@@ -4,6 +4,7 @@
  * Abstract base class for subband classes of layer I and II
  */
 @LATTICE("S<L,L<H,H<SH")
+@METHODDEFAULT("OUT<V,V<SH,SH<THIS,THIS<IN,SH*,THISLOC=THIS,GLOBALLOC=IN")
 static abstract class Subband
 {
  /*
@@ -32,8 +33,12 @@ static abstract class Subband
   0.00000190734863f, 0.00000151386361f, 0.00000120155435f, 0.00000000000000f /* illegal scalefactor */
   };
 
-  public abstract void read_allocation (Bitstream stream, Header header, Crc16 crc) throws DecoderException;
-  public abstract void read_scalefactor (Bitstream stream, Header header);
-  public abstract boolean read_sampledata (Bitstream stream);
-  public abstract boolean put_next_sample (int channels, SynthesisFilter filter1, SynthesisFilter filter2);
+  public abstract void read_allocation (@LOC("IN")  Bitstream stream, @LOC("IN") Header header, @LOC("IN") Crc16 crc) throws DecoderException;
+  public abstract void read_scalefactor (@LOC("IN") Bitstream stream, @LOC("IN") Header header);
+  
+  @RETURNLOC("OUT")
+  public abstract boolean read_sampledata (@LOC("IN") Bitstream stream);
+  
+  @RETURNLOC("OUT")
+  public abstract boolean put_next_sample (@LOC("IN") int channels,@LOC("IN")  SynthesisFilter filter1,@LOC("IN")  SynthesisFilter filter2);
 };