From ff3ceae6b47a1a01bc56fa55fa5770cba0bf252f Mon Sep 17 00:00:00 2001
From: yeom <yeom>
Date: Thu, 2 Aug 2012 21:06:46 +0000
Subject: [PATCH] fixed another problem of the flow-down check. If an
 assignment statement has OP+EQ operator(eg,+=,*=), calculate GLB of LHS & RHS
 and then assign it as the location type of RHS. + annotation fixes according
 to fix.

---
 Robust/src/Analysis/SSJava/FlowDownCheck.java | 26 ++++++++-----------
 .../SSJava/EyeTracking/Classifier.java        |  2 +-
 .../SSJava/MP3Decoder/BitReserve.java         |  2 +-
 .../SSJava/MP3Decoder/LayerIIIDecoder.java    |  2 +-
 4 files changed, 14 insertions(+), 18 deletions(-)

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index a16a6e9f..f466b0ed 100644
--- 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) {
 
-    // System.out.println("\n# ASSIGNMENTNODE=" + an.printNode(0));
-
     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);
 
-      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) {
-        inputGLBSet.add(rhsLocation);
+        inputGLBSet.add(srcLocation);
         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))) {
 
@@ -1643,10 +1643,6 @@ public class FlowDownCheck {
         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)) {
diff --git a/Robust/src/Benchmarks/SSJava/EyeTracking/Classifier.java b/Robust/src/Benchmarks/SSJava/EyeTracking/Classifier.java
index f5a3c6de..ec19504c 100644
--- 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
    */
-  @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,
diff --git a/Robust/src/Benchmarks/SSJava/MP3Decoder/BitReserve.java b/Robust/src/Benchmarks/SSJava/MP3Decoder/BitReserve.java
index d6dc322f..190fd65c 100644
--- 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
 // can silently occur.
 @LATTICE("BUF<OFF,BUF<BIT,BIT*,OFF*")
-@METHODDEFAULT("OUT<THIS,THIS<IN,IN*,THISLOC=THIS,RETURNLOC=OUT")
+@METHODDEFAULT("OUT<THIS,THIS<IN,IN*,OUT*,THISLOC=THIS,RETURNLOC=OUT")
 final class BitReserve {
   /**
    * Size of the internal buffer to store the reserved bits. Must be a power of
diff --git a/Robust/src/Benchmarks/SSJava/MP3Decoder/LayerIIIDecoder.java b/Robust/src/Benchmarks/SSJava/MP3Decoder/LayerIIIDecoder.java
index 02ff7476..52fdb3d4 100644
--- 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")
-@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);
-- 
2.34.1