fixed another problem of the flow-down check. If an assignment statement has OP+EQ...

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index a16a6e9ff784ad5da0624a5a3d7a0c2e4d79e138..f466b0edbe8abaedb2c3931d54a883e8d0007e5f 100644 (file)
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -1563,8 +1563,6 @@ public class FlowDownCheck {
   private CompositeLocation checkLocationFromAssignmentNode(MethodDescriptor md,
       SymbolTable nametable, AssignmentNode an, CompositeLocation loc, CompositeLocation constraint) {
 
   private CompositeLocation checkLocationFromAssignmentNode(MethodDescriptor md,
       SymbolTable nametable, AssignmentNode an, CompositeLocation loc, CompositeLocation constraint) {
 

-    // System.out.println("\n# ASSIGNMENTNODE=" + an.printNode(0));
-

     ClassDescriptor cd = md.getClassDesc();
 
     Set<CompositeLocation> inputGLBSet = new HashSet<CompositeLocation>();
     ClassDescriptor cd = md.getClassDesc();
 
     Set<CompositeLocation> inputGLBSet = new HashSet<CompositeLocation>();


@@ -1592,20 +1590,22 @@ public class FlowDownCheck {
           checkLocationFromExpressionNode(md, nametable, an.getSrc(), new CompositeLocation(),
               constraint, false);
 
           checkLocationFromExpressionNode(md, nametable, an.getSrc(), new CompositeLocation(),
               constraint, false);
 

-      srcLocation = rhsLocation;
+      if (an.getOperation().getOp() >= 2 && an.getOperation().getOp() <= 12) {
+        // if assignment contains OP+EQ operator, need to merge location types
+        // of LHS & RHS into the RHS
+        Set<CompositeLocation> srcGLBSet = new HashSet<CompositeLocation>();
+        srcGLBSet.add(rhsLocation);
+        srcGLBSet.add(destLocation);
+        srcLocation = CompositeLattice.calculateGLB(srcGLBSet, generateErrorMessage(cd, an));
+      } else {
+        srcLocation = rhsLocation;
+      }

 
 

-      // if (!rhsLocation.get(rhsLocation.getSize() - 1).isTop()) {

       if (constraint != null) {
       if (constraint != null) {

-        inputGLBSet.add(rhsLocation);
+        inputGLBSet.add(srcLocation);

         inputGLBSet.add(constraint);
         srcLocation = CompositeLattice.calculateGLB(inputGLBSet, generateErrorMessage(cd, an));
       }
         inputGLBSet.add(constraint);
         srcLocation = CompositeLattice.calculateGLB(inputGLBSet, generateErrorMessage(cd, an));
       }

-      // }
-
-      // System.out.println("dstLocation=" + destLocation);
-      // System.out.println("rhsLocation=" + rhsLocation);
-      // System.out.println("srcLocation=" + srcLocation);
-      // System.out.println("constraint=" + constraint);

 
       if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, generateErrorMessage(cd, an))) {
 
 
       if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, generateErrorMessage(cd, an))) {
 


@@ -1643,10 +1643,6 @@ public class FlowDownCheck {
         srcLocation = rhsLocation;
       }
 
         srcLocation = rhsLocation;
       }
 

-      // System.out.println("srcLocation=" + srcLocation);
-      // System.out.println("rhsLocation=" + rhsLocation);
-      // System.out.println("constraint=" + constraint);
-

       if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, generateErrorMessage(cd, an))) {
 
         if (srcLocation.equals(destLocation)) {
       if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, generateErrorMessage(cd, an))) {
 
         if (srcLocation.equals(destLocation)) {

diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/Classifier.java b/Robust/src/Benchmarks/SSJava/EyeTracking/Classifier.java
index f5a3c6deba751655f6d1c181570b13522aa5c618..ec19504c828db073bc1948cb1e750b8c85bd5ad5 100644 (file)
--- a/Robust/src/Benchmarks/SSJava/EyeTracking/Classifier.java
+++ b/Robust/src/Benchmarks/SSJava/EyeTracking/Classifier.java
@@ -74,7 +74,7 @@ public class Classifier {
    * @param translationY
    * @return true if this region was classified as face, else false
    */
    * @param translationY
    * @return true if this region was classified as face, else false
    */

-  @LATTICE("OUT<V,V<C,C<THIS,THIS<IN,C*,V*,THISLOC=THIS,RETURNLOC=OUT")
+  @LATTICE("OUT<V,V<C,C<THIS,THIS<IN,C*,V*,OUT*,THISLOC=THIS,RETURNLOC=OUT")

   @PCLOC("THIS,Classifier.C")
   public boolean classifyFace(@LOC("THIS,Classifier.C") IntegralImageData image,
       @LOC("THIS,Classifier.C") float scaleFactor, @LOC("THIS,Classifier.C") int translationX,
   @PCLOC("THIS,Classifier.C")
   public boolean classifyFace(@LOC("THIS,Classifier.C") IntegralImageData image,
       @LOC("THIS,Classifier.C") float scaleFactor, @LOC("THIS,Classifier.C") int translationX,

diff --git a/Robust/src/Benchmarks/SSJava/MP3Decoder/BitReserve.java b/Robust/src/Benchmarks/SSJava/MP3Decoder/BitReserve.java
index d6dc322fb8d86a5d5069395daa1ccc73e9bac2cd..190fd65c3dc4e104b4a8ee2f204f842cbe0e8fd6 100644 (file)
--- a/Robust/src/Benchmarks/SSJava/MP3Decoder/BitReserve.java
+++ b/Robust/src/Benchmarks/SSJava/MP3Decoder/BitReserve.java
@@ -38,7 +38,7 @@
 // REVIEW: there is no range checking, so buffer underflow or overflow\r
 // can silently occur.\r
 @LATTICE("BUF<OFF,BUF<BIT,BIT*,OFF*")\r
 // REVIEW: there is no range checking, so buffer underflow or overflow\r
 // can silently occur.\r
 @LATTICE("BUF<OFF,BUF<BIT,BIT*,OFF*")\r

-@METHODDEFAULT("OUT<THIS,THIS<IN,IN*,THISLOC=THIS,RETURNLOC=OUT")\r
+@METHODDEFAULT("OUT<THIS,THIS<IN,IN*,OUT*,THISLOC=THIS,RETURNLOC=OUT")\r

 final class BitReserve {\r
   /**\r
    * Size of the internal buffer to store the reserved bits. Must be a power of\r
 final class BitReserve {\r
   /**\r
    * Size of the internal buffer to store the reserved bits. Must be a power of\r

diff --git a/Robust/src/Benchmarks/SSJava/MP3Decoder/LayerIIIDecoder.java b/Robust/src/Benchmarks/SSJava/MP3Decoder/LayerIIIDecoder.java
index 02ff7476914c2683b2e4d5ffad9d3948d1e49b98..52fdb3d4534d2b1fec54d4571569e78606f22a90 100644 (file)
--- a/Robust/src/Benchmarks/SSJava/MP3Decoder/LayerIIIDecoder.java
+++ b/Robust/src/Benchmarks/SSJava/MP3Decoder/LayerIIIDecoder.java
@@ -47,7 +47,7 @@
 // 10th added for get_scale_factors
 // llth added for decode
 // @LATTICE("IS1D*,RO<IS1D,IS1D<SI2,SI2<SI1,SI<P2S,SF1<CH0,SF0*,SFB_SH<NS,NS<SI,SFB_SH*,SFB<SFB_SH,C,C*,SI1<SF2,SF2<SFB,SF1<BR,LR*,OUT<LR,LR<RO,NZ*,SI<SF1,SI1<NZ,NZ<SI,SI1<SBI,SBI<SI,BUF<FT,SF1<SF0,SF0<HD1,BR<ST,ST,FT<SP,SP<OUT,OUT<SI1,SI1<SI,P2S<CH0,CH0<MAX0,MAX0<BR1,FS<BR1,BR1<BR,BR<HD1,HD1<HD,OUT*,BR1*,SI1*,MAX0*,CH0*,RAW,TS,F,C,K,LY,VAR,IR,IP,CSH,GLSFD3,GLSFD4,GLSFD5,GLSFF4,GLSFF2,GLSFF3,GLSFF1,GSF4,GSF5,GSF1,GSF2,GSF3,HD2,HD3,BT,GR,RO6,RO5,RO9,RO8,RO7,RO4,RO1,RO3,RO2,SH,ME,TMP2,S,LSF,J")
 // 10th added for get_scale_factors
 // llth added for decode
 // @LATTICE("IS1D*,RO<IS1D,IS1D<SI2,SI2<SI1,SI<P2S,SF1<CH0,SF0*,SFB_SH<NS,NS<SI,SFB_SH*,SFB<SFB_SH,C,C*,SI1<SF2,SF2<SFB,SF1<BR,LR*,OUT<LR,LR<RO,NZ*,SI<SF1,SI1<NZ,NZ<SI,SI1<SBI,SBI<SI,BUF<FT,SF1<SF0,SF0<HD1,BR<ST,ST,FT<SP,SP<OUT,OUT<SI1,SI1<SI,P2S<CH0,CH0<MAX0,MAX0<BR1,FS<BR1,BR1<BR,BR<HD1,HD1<HD,OUT*,BR1*,SI1*,MAX0*,CH0*,RAW,TS,F,C,K,LY,VAR,IR,IP,CSH,GLSFD3,GLSFD4,GLSFD5,GLSFF4,GLSFF2,GLSFF3,GLSFF1,GSF4,GSF5,GSF1,GSF2,GSF3,HD2,HD3,BT,GR,RO6,RO5,RO9,RO8,RO7,RO4,RO1,RO3,RO2,SH,ME,TMP2,S,LSF,J")

-@LATTICE("SI0*,INIT*,ISR*,ISP*,HD<CH0,LR<ISR,ISR<ISP,SI1<SF2,NS*,CH0<ST,ST<INIT,IS1D*,RO1<RO,RO1*,RO<IS1D,IS1D<SI2,SI2<SI1,BR<NS,NS<SI,SFB_SH*,SFB<SFB_SH,C,C*,SF2<SFB,LR*,TSOUT*,OUT1<PREV,PREV<RAWFULL,RAWFULL<RAWOUT,RAWOUT<TSOUT,TSOUT<OUT0,OUT0<LR,ISP<RO1,NZ*,SI<SI0,SI0<SF15,SF15<SF1,BR1<NZ,NZ<BR,SI1<RT,RT<SBI,SBI<SI,BUF<FT,SF1<HD1,SF1<HD1,FT<SP,SP<OUT1,SI1<SI,SFB_SH<BR1,BR1<BR,HD1<HD,OUT0*,OUT1*,BR1*,SI1*,CH0*")
+@LATTICE("SI0*,INIT*,ISR*,ISP*,HD<CH0,LR<ISR,ISR<ISP,SI1<SF2,NS*,CH0<ST,ST<INIT,IS1D*,RO1<RO,RO1*,RO<IS1D,IS1D<SI2,SI2<SI1,BR<NS,NS<SI,SFB_SH*,SFB<SFB_SH,C,C*,SF2<SFB,LR*,TSOUT*,OUT1<PREV,PREV<RAWFULL,RAWFULL<RAWOUT,RAWOUT<TSOUT,TSOUT<OUT0,OUT0<LR,ISP<RO1,NZ*,SI<SI0,SI0<SF15,SF15<SF1,BR1<NZ,NZ<BR,SI1<RT,RT<SBI,SBI<SI,BUF<FT,SF1<HD1,SF1<HD1,FT<SP,SP<OUT1,SI1<SI,SFB_SH<BR1,BR1<BR,HD1<HD,OUT0*,OUT1*,BR1*,SI1*,CH0*,RO*,RAWOUT*")

 @METHODDEFAULT("OUT<V,V<THIS,THIS<SH,SH<IN,SH*,THISLOC=THIS,GLOBALLOC=IN,RETURNLOC=OUT")
 final class LayerIIIDecoder implements FrameDecoder {
   static final double d43 = (4.0 / 3.0);
 @METHODDEFAULT("OUT<V,V<THIS,THIS<SH,SH<IN,SH*,THISLOC=THIS,GLOBALLOC=IN,RETURNLOC=OUT")
 final class LayerIIIDecoder implements FrameDecoder {
   static final double d43 = (4.0 / 3.0);