From d652086ece80e8083f30aab3e48346b87bf3ff9e Mon Sep 17 00:00:00 2001
From: yeom <yeom>
Date: Fri, 20 May 2011 18:51:22 +0000
Subject: [PATCH] fix bugs on the flow down rule and start annotating ssjava
 class library again

---
 Robust/src/Analysis/SSJava/FlowDownCheck.java | 143 ++++++++++--------
 Robust/src/ClassLibrary/SSJava/String.java    |  67 +++++++-
 Robust/src/Tests/ssJava/flowdown/test.java    |   1 +
 3 files changed, 136 insertions(+), 75 deletions(-)

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 65240aa1..de46e711 100644
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -265,7 +265,9 @@ public class FlowDownCheck {
       // matter what it is going to return.
       loc.addLocation(Location.createBottomLocation(md));
     } else {
-      loc = checkLocationFromExpressionNode(md, nametable, returnExp, loc);
+      // by default, return node has "bottom" location
+      // loc = checkLocationFromExpressionNode(md, nametable, returnExp, loc);
+      loc.addLocation(Location.createBottomLocation(md));
     }
     return loc;
   }
@@ -475,7 +477,7 @@ public class FlowDownCheck {
       break;
 
     case Kind.MethodInvokeNode:
-      compLoc = checkLocationFromMethodInvokeNode(md, nametable, (MethodInvokeNode) en);
+      compLoc = checkLocationFromMethodInvokeNode(md, nametable, (MethodInvokeNode) en, loc);
       break;
 
     case Kind.TertiaryNode:
@@ -556,30 +558,7 @@ public class FlowDownCheck {
   }
 
   private CompositeLocation checkLocationFromMethodInvokeNode(MethodDescriptor md,
-      SymbolTable nametable, MethodInvokeNode min) {
-
-    // Location baseLoc = null;
-    // if (min.getBaseName() != null) {
-    // Descriptor d = nametable.get(min.getBaseName().getSymbol());
-    // if (d instanceof VarDescriptor) {
-    // CompositeLocation varLoc = (CompositeLocation) ((VarDescriptor)
-    // d).getType().getExtension();
-    // return varLoc;
-    // } else {
-    // // it is field descriptor
-    // assert (d instanceof FieldDescriptor);
-    // CompositeLocation fieldLoc =
-    // (CompositeLocation) min.getExpression().getType().getExtension();
-    // return fieldLoc;
-    // }
-    // } else {
-    // // method invocation starting from this
-    // MethodLattice<String> methodLattice = ssjava.getMethodLattice(md);
-    // System.out.println("md=" + md + " lattice=" + methodLattice);
-    // String thisLocId = methodLattice.getThisLoc();
-    // baseLoc = new Location(md, thisLocId);
-    // }
-    // System.out.println("BASE LOC=" + baseLoc);
+      SymbolTable nametable, MethodInvokeNode min, CompositeLocation loc) {
 
     if (min.numArgs() > 1) {
       // caller needs to guarantee that it passes arguments in regarding to
@@ -627,7 +606,6 @@ public class FlowDownCheck {
     }
 
     // all arguments should be higher than the location of return value
-
     Set<CompositeLocation> inputGLBSet = new HashSet<CompositeLocation>();
     for (int i = 0; i < min.numArgs(); i++) {
       ExpressionNode en = min.getArg(i);
@@ -636,12 +614,39 @@ public class FlowDownCheck {
       inputGLBSet.add(callerArg);
     }
 
-    if (inputGLBSet.size() > 0) {
-      return CompositeLattice.calculateGLB(inputGLBSet);
+    // if (inputGLBSet.size() > 0) {
+    // return CompositeLattice.calculateGLB(inputGLBSet);
+    // } else {
+    // // if there are no arguments,
+    // // method invocation from the same class
+    // CompositeLocation compLoc = new CompositeLocation();
+    // return compLoc;
+    // }
+
+    Location baseLoc = null;
+    if (min.getBaseName() != null) {
+      Descriptor d = nametable.get(min.getBaseName().getSymbol());
+      if (d instanceof VarDescriptor) {
+        CompositeLocation varLoc = (CompositeLocation) ((VarDescriptor) d).getType().getExtension();
+        return varLoc;
+      } else {
+        // it is field descriptor
+        assert (d instanceof FieldDescriptor);
+        Location fieldLoc = (Location) min.getExpression().getType().getExtension();
+        CompositeLocation compLoc = new CompositeLocation();
+        MethodLattice<String> methodLattice = ssjava.getMethodLattice(md);
+        Location thisLoc = new Location(md, methodLattice.getThisLoc());
+        compLoc.addLocation(thisLoc);
+        compLoc.addLocation(fieldLoc);
+        return compLoc;
+      }
     } else {
-      // if there are no arguments,
-      // method invocation from the same class
+      // method invocation starting from this
+      MethodLattice<String> methodLattice = ssjava.getMethodLattice(md);
+      String thisLocId = methodLattice.getThisLoc();
+      baseLoc = new Location(md, thisLocId);
       CompositeLocation compLoc = new CompositeLocation();
+      compLoc.addLocation(baseLoc);
       return compLoc;
     }
 
@@ -658,12 +663,12 @@ public class FlowDownCheck {
 
     CompositeLocation arrayLoc =
         checkLocationFromExpressionNode(md, nametable, aan.getExpression(), new CompositeLocation());
-    addTypeLocation(aan.getExpression().getType(), arrayLoc);
+    // addTypeLocation(aan.getExpression().getType(), arrayLoc);
     glbInputSet.add(arrayLoc);
     CompositeLocation indexLoc =
         checkLocationFromExpressionNode(md, nametable, aan.getIndex(), new CompositeLocation());
     glbInputSet.add(indexLoc);
-    addTypeLocation(aan.getIndex().getType(), indexLoc);
+    // addTypeLocation(aan.getIndex().getType(), indexLoc);
 
     CompositeLocation glbLoc = CompositeLattice.calculateGLB(glbInputSet);
     return glbLoc;
@@ -714,11 +719,9 @@ public class FlowDownCheck {
       // addTypeLocation(on.getRight().getType(), rightLoc);
     }
 
-    // System.out.println("checking op node=" + on.printNode(0));
-    // System.out.println("left loc=" + leftLoc + " from " +
-    // on.getLeft().getClass());
-    // System.out.println("right loc=" + rightLoc + " from " +
-    // on.getRight().getClass());
+//    System.out.println("checking op node=" + on.printNode(0));
+//    System.out.println("left loc=" + leftLoc + " from " + on.getLeft().getClass());
+//    System.out.println("right loc=" + rightLoc + " from " + on.getRight().getClass());
 
     Operation op = on.getOp();
 
@@ -788,7 +791,12 @@ public class FlowDownCheck {
       if (varname.equals("this")) {
         // 'this' itself!
         MethodLattice<String> methodLattice = ssjava.getMethodLattice(md);
-        Location locElement = new Location(md, methodLattice.getThisLoc());
+        String thisLocId = methodLattice.getThisLoc();
+        if (thisLocId == null) {
+          throw new Error("The location for 'this' is not defined at "
+              + md.getClassDesc().getSourceFileName() + "::" + nn.getNumLine());
+        }
+        Location locElement = new Location(md, thisLocId);
         loc.addLocation(locElement);
         return loc;
       }
@@ -1210,16 +1218,9 @@ public class FlowDownCheck {
       String glbOfPriorityLoc = locOrder.getGLB(priorityLocIdentifierSet);
 
       glbCompLoc.addLocation(new Location(priorityDescriptor, glbOfPriorityLoc));
-
       Set<CompositeLocation> compSet = locId2CompLocSet.get(glbOfPriorityLoc);
 
-      if (compSet.size() == 1) {
-        // if GLB(x1,x2)==x1 or x2 : GLB case 2,3
-        CompositeLocation comp = compSet.iterator().next();
-        for (int i = 1; i < comp.getSize(); i++) {
-          glbCompLoc.addLocation(comp.get(i));
-        }
-      } else if (compSet.size() == 0) {
+      if (compSet == null) {
         // when GLB(x1,x2)!=x1 and !=x2 : GLB case 4
         // mean that the result is already lower than <x1,y1> and <x2,y2>
         // assign TOP to the rest of the location elements
@@ -1228,29 +1229,37 @@ public class FlowDownCheck {
           glbCompLoc.addLocation(Location.createTopLocation(inputComp.get(i).getDescriptor()));
         }
       } else {
-        // when GLB(x1,x2)==x1 and x2 : GLB case 1
-        // if more than one location shares the same priority GLB
-        // need to calculate the rest of GLB loc
-
-        int compositeLocSize = compSet.iterator().next().getSize();
-
-        Set<String> glbInputSet = new HashSet<String>();
-        Descriptor currentD = null;
-        for (int i = 1; i < compositeLocSize; i++) {
-          for (Iterator iterator = compSet.iterator(); iterator.hasNext();) {
-            CompositeLocation compositeLocation = (CompositeLocation) iterator.next();
-            Location currentLoc = compositeLocation.get(i);
-            currentD = currentLoc.getDescriptor();
-            // making set of the current location sharing the same idx
-            glbInputSet.add(currentLoc.getLocIdentifier());
+        if (compSet.size() == 1) {
+          // if GLB(x1,x2)==x1 or x2 : GLB case 2,3
+          CompositeLocation comp = compSet.iterator().next();
+          for (int i = 1; i < comp.getSize(); i++) {
+            glbCompLoc.addLocation(comp.get(i));
           }
-          // calculate glb for the current lattice
+        } else {
+          // when GLB(x1,x2)==x1 and x2 : GLB case 1
+          // if more than one location shares the same priority GLB
+          // need to calculate the rest of GLB loc
+
+          int compositeLocSize = compSet.iterator().next().getSize();
+
+          Set<String> glbInputSet = new HashSet<String>();
+          Descriptor currentD = null;
+          for (int i = 1; i < compositeLocSize; i++) {
+            for (Iterator iterator = compSet.iterator(); iterator.hasNext();) {
+              CompositeLocation compositeLocation = (CompositeLocation) iterator.next();
+              Location currentLoc = compositeLocation.get(i);
+              currentD = currentLoc.getDescriptor();
+              // making set of the current location sharing the same idx
+              glbInputSet.add(currentLoc.getLocIdentifier());
+            }
+            // calculate glb for the current lattice
 
-          SSJavaLattice<String> currentLattice = getLatticeByDescriptor(currentD);
-          String currentGLBLocId = currentLattice.getGLB(glbInputSet);
-          glbCompLoc.addLocation(new Location(currentD, currentGLBLocId));
-        }
+            SSJavaLattice<String> currentLattice = getLatticeByDescriptor(currentD);
+            String currentGLBLocId = currentLattice.getGLB(glbInputSet);
+            glbCompLoc.addLocation(new Location(currentD, currentGLBLocId));
+          }
 
+        }
       }
 
       return glbCompLoc;
diff --git a/Robust/src/ClassLibrary/SSJava/String.java b/Robust/src/ClassLibrary/SSJava/String.java
index 3111820d..6b85b662 100644
--- a/Robust/src/ClassLibrary/SSJava/String.java
+++ b/Robust/src/ClassLibrary/SSJava/String.java
@@ -1,15 +1,66 @@
-//@LATTICE("data<proc,proc<c,c<in,in*,c*,proc*,data*")
-@LATTICE("V<C, V<O")
-@DEFAULTMETHOD("O<V,V<I,V<C,THIS=O")
+@LATTICE("String_V<String_C, String_V<String_O")
+@METHODDEFAULT("StringDM_O<StringDM_V,StringDM_V<StringDM_C,StringDM_C<StringDM_I,THISLOC=StringDM_O,StringDM_C*")
 public class String {
 
-  @LOC("V") char value[];
-  @LOC("C") int count;
-  @LOC("O") int offset;
-  @LOC("V") private int cachedHashcode;
+  @LOC("String_V") char value[];
+  @LOC("String_C") int count;
+  @LOC("String_O") int offset;
+  @LOC("String_V") private int cachedHashcode;
 
   private String() {
   }
+
+  public String(@LOC("StringDM_I") char c) {
+    @LOC("StringDM_V") char[] str = new char[1];
+    str[0] = c;
+    String(str);
+  }
+
+  public String(@LOC("StringDM_I") char str[]) {
+    @LOC("StringDM_V") char charstr[]=new char[str.length];
+    for(@LOC("StringDM_C") int i=0; i<str.length; i++)
+      charstr[i]=str[i];
+    this.value=charstr;
+    this.count=str.length;
+    this.offset=0;
+  }
+
+  @LATTICE("StringM1_O<StringM1_V,StringM1_V<StringM1_C,StringM1_C<StringM1_I,THISLOC=StringM1_I,StringM1_C*")
+  public String concat(@LOC("StringM1_I") String str) {
+    @LOC("StringM1_O") String newstr=new String(); // create new one, it has OUT location
+    @LOC("StringM1_C") int newCount=this.count+str.count;
+
+    @LOC("StringM1_V") char charstr[]=new char[newCount];
+
+    // here, for loop introduces indirect flow from [C] to [V]
+    for(@LOC("StringM1_C") int i=0; i<count; i++) {
+      // value flows from GLB(THISLOC,C,THISLOC.V)=(THISLOC,TOP) to [V]
+      charstr[i]=value[i+offset]; 
+    }
+    for(@LOC("StringM1_C") int i=0; i<str.count; i++) {
+      charstr[i+count]=str.value[i+str.offset];
+    }
+
+    newstr.value=charstr;
+    // LOC(newstr.value)=[O,STRING_V] 
+    // LOC(charstr)=[V]
+    // [O,STRING_V] < [V]
+    
+    return newstr;
+  }
   
-  
+  public boolean equals(@LOC("StringDM_I") Object o) {
+    if (o.getType()!=getType()) // values are coming from [StringDM_I] and [THISLOC]
+      return false;
+    @LOC("StringDM_V") String s=(String)o;
+    if (s.count!=count)
+      return false;
+    for(@LOC("StringDM_C") int i=0; i<count; i++) {
+      if (s.value[i+s.offset]!=value[i+offset])
+        return false;
+    }
+    return true;
+  }
+
+
 }
diff --git a/Robust/src/Tests/ssJava/flowdown/test.java b/Robust/src/Tests/ssJava/flowdown/test.java
index 605957b3..46dfb95d 100644
--- a/Robust/src/Tests/ssJava/flowdown/test.java
+++ b/Robust/src/Tests/ssJava/flowdown/test.java
@@ -140,6 +140,7 @@ class Foo{
 }
 
 @LATTICE("BC<BB,BB<BA,BB*")
+@METHODDEFAULT("BARMD_L<BARMD_H,THISLOC=BARMD_H")
 class Bar{
     @LOC("BA") int a;
     @LOC("BB") int b2;
-- 
2.34.1