more changes.

diff --git a/Robust/src/Analysis/SSJava/CompositeLocation.java b/Robust/src/Analysis/SSJava/CompositeLocation.java
index 0dd524db8fd7f06f4b00d80f927d294326a6cc91..8f396a57f541bea282413e63bc974b7f85c699bb 100644 (file)
--- a/Robust/src/Analysis/SSJava/CompositeLocation.java
+++ b/Robust/src/Analysis/SSJava/CompositeLocation.java
@@ -30,139 +30,13 @@ public class CompositeLocation implements TypeExtension {
   public Location get(int idx) {
     return locTuple.get(idx);
   }
-  
-  public boolean isEmpty(){
-    return locTuple.size()==0;
-  }
-
-  // public void addLocationSet(Set<Location> set) {
-  //
-  // for (Iterator iterator = set.iterator(); iterator.hasNext();) {
-  // Location location = (Location) iterator.next();
-  // locTuple.addElement(location);
-  // }
-  //
-  // }
-
-  // public Location getLocation(ClassDescriptor cd) {
-  //
-  // // need to get more optimization version later
-  // Set<Location> locSet = getBaseLocationSet();
-  // for (Iterator iterator = locSet.iterator(); iterator.hasNext();) {
-  // Location location = (Location) iterator.next();
-  // if (location.getClassDescriptor().equals(cd)) {
-  // return location;
-  // }
-  // }
-  //
-  // return null;
-  //
-  // }
-
-  // public Map<ClassDescriptor, Location> getCd2Loc() {
-  //
-  // Map<ClassDescriptor, Location> cd2loc = new Hashtable<ClassDescriptor,
-  // Location>();
-  //
-  // Set<Location> baseLocSet = getBaseLocationSet();
-  // for (Iterator iterator = baseLocSet.iterator(); iterator.hasNext();) {
-  // Location location = (Location) iterator.next();
-  // cd2loc.put(location.getClassDescriptor(), location);
-  // }
-  //
-  // return cd2loc;
-  //
-  // }
-
-  public NTuple<Location> getBaseLocationTuple() {
-
-    return locTuple;
-
-    // NTuple<Location> baseLocationTuple = new NTuple<Location>();
-    // int tupleSize = locTuple.size();
-    // for (int i = 0; i < tupleSize; i++) {
-    // Location locElement = locTuple.at(i);
-    //
-    // if (locElement instanceof DeltaLocation) {
-    // // baseLocationSet.addAll(((DeltaLocation)
-    // // locElement).getDeltaOperandLocationVec());
-    // baseLocationTuple.addAll(((DeltaLocation)
-    // locElement).getBaseLocationTuple());
-    // } else {
-    // baseLocationTuple.addElement(locElement);
-    // }
-    // }
-    // return baseLocationTuple;
 
+  public boolean isEmpty() {
+    return locTuple.size() == 0;
   }
 
-  // public List<Location> getBaseLocationList() {
-  //
-  // Set<Location> baseLocationSet = new HashSet<Location>();
-  // int tupleSize = locTuple.size();
-  // for (int i = 0; i < tupleSize; i++) {
-  // Location locElement = locTuple.at(i);
-  //
-  // if (locElement instanceof DeltaLocation) {
-  // // baseLocationSet.addAll(((DeltaLocation)
-  // // locElement).getDeltaOperandLocationVec());
-  // baseLocationSet.addAll(((DeltaLocation) locElement).getBaseLocationSet());
-  // } else {
-  // baseLocationSet.add(locElement);
-  // }
-  // }
-  // return baseLocationSet;
-  // }
-
-  // public int getNumofDelta() {
-  //
-  // int result = 0;
-  //
-  // if (locTuple.size() == 1) {
-  // Location locElement = locTuple.at(0);
-  // if (locElement instanceof DeltaLocation) {
-  // result++;
-  // result += getNumofDelta((DeltaLocation) locElement);
-  // }
-  // }
-  // return result;
-  // }
-
-  // public int getNumofDelta(DeltaLocation delta) {
-  // int result = 0;
-  //
-  // if (delta.getDeltaOperandLocationVec().size() == 1) {
-  // Location locElement = delta.getDeltaOperandLocationVec().at(0);
-  // if (locElement instanceof DeltaLocation) {
-  // result++;
-  // result += getNumofDelta((DeltaLocation) locElement);
-  // }
-  // }
-  //
-  // return result;
-  // }
-
-  // public void removieLocation(ClassDescriptor cd) {
-  // for (int i = 0; i < locTuple.size(); i++) {
-  // if (locTuple.at(i).getClassDescriptor().equals(cd)) {
-  // locTuple.removeAt(i);
-  // return;
-  // }
-  // }
-  // }
-
   public String toString() {
 
-    // for better representation
-    // if compositeLoc has only one single location,
-    // just print out single location
-    // if(locTuple.size()==1){
-    // Location locElement=locTuple.at(0);
-    // if(locElement instanceof Location){
-    // return locElement.toString();
-    // }
-    // }
-
     String rtr = "CompLoc[";
 
     int tupleSize = locTuple.size();

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 54a17f4435908f261cfc911cb4a69ddf7e0e4af7..3edbd818ce63d00d942e194ea5b0396d52d32712 100644 (file)
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -781,7 +781,7 @@ public class FlowDownCheck {
     NameDescriptor nd = nn.getName();
     if (nd.getBase() != null) {
       loc = checkLocationFromExpressionNode(md, nametable, nn.getExpression(), loc);
-      addTypeLocation(nn.getExpression().getType(), loc);
+      // addTypeLocation(nn.getExpression().getType(), loc);
     } else {
       String varname = nd.toString();
 
@@ -862,20 +862,14 @@ public class FlowDownCheck {
     } else {
       destLocation =
           srcLocation = checkLocationFromExpressionNode(md, nametable, an.getDest(), srcLocation);
-      // TODO
-      // if (!((Set<String>) state.getCd2LocationPropertyMap().get(new Pair(cd,
-      // "spin")))
-      // .contains(destLocation.getLocation(cd).getLocIdentifier())) {
-      // throw new Error("Location " + destLocation +
-      // " is not allowed to have spinning values at "
-      // + cd.getSourceFileName() + ":" + an.getNumLine());
-      // }
+
+      if (!CompositeLattice.isGreaterThan(srcLocation, destLocation)) {
+        throw new Error("Location " + destLocation
+            + " is not allowed to have the value flow that moves within the same location at "
+            + cd.getSourceFileName() + "::" + an.getNumLine());
+      }
 
     }
-    // if (an.getSrc() != null) {
-    // addTypeLocation(an.getSrc().getType(), srcLocation);
-    // }
-    // addTypeLocation(an.getDest().getType(), destLocation);
 
     return destLocation;
   }
@@ -956,9 +950,6 @@ public class FlowDownCheck {
     SSJavaLattice<String> localLattice = CompositeLattice.getLatticeByDescriptor(md);
     Location localLoc = new Location(md, localLocId);
     if (localLattice == null || (!localLattice.containsKey(localLocId))) {
-      System.out.println("md=" + md);
-      System.out.println("localLattice=" + localLattice + " l=" + localLocId);
-      System.out.println("localLattice leemtn=" + localLattice.table);
       throw new Error("Location " + localLocId
           + " is not defined in the local variable lattice at "
           + md.getClassDesc().getSourceFileName() + "::" + n.getNumLine() + ".");
@@ -1042,7 +1033,7 @@ public class FlowDownCheck {
         // d2loc.put(fd, loc);
         addTypeLocation(fd.getType(), loc);
 
-      } 
+      }
     }
 
   }
@@ -1063,8 +1054,6 @@ public class FlowDownCheck {
 
     public static boolean isGreaterThan(CompositeLocation loc1, CompositeLocation loc2) {
 
-      // System.out.println("\nisGreaterThan=" + loc1 + " ? " + loc2);
-
       int baseCompareResult = compareBaseLocationSet(loc1, loc2);
       if (baseCompareResult == ComparisonResult.EQUAL) {
         if (compareDelta(loc1, loc2) == ComparisonResult.GREATER) {
@@ -1133,10 +1122,16 @@ public class FlowDownCheck {
         }
 
         if (loc1.getLocIdentifier().equals(loc2.getLocIdentifier())) {
+          // check if the current location is the spinning location
+          if (lattice1.getSpinLocSet().contains(loc1.getLocIdentifier())) {
+            return ComparisonResult.GREATER;
+          }
           numOfTie++;
           continue;
         } else if (lattice1.isGreaterThan(loc1.getLocIdentifier(), loc2.getLocIdentifier())) {
           return ComparisonResult.GREATER;
+        } else {
+          return ComparisonResult.LESS;
         }
 
       }

diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
index 838e51035185cf8b89c96f06cbf994aac521d010..50d35f7c0d62fc355db8d984d806d34780b81b9a 100644 (file)
--- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
+++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
@@ -127,7 +127,7 @@ public class SSJavaAnalysis {
         locOrder.setGlobalLoc(globalLoc);
       } else if (orderElement.contains("*")) {
         // spin loc definition
-        locOrder.addSpinLoc(orderElement);
+        locOrder.addSpinLoc(orderElement.substring(0,orderElement.length()-1));
       } else {
         // single element
         locOrder.put(orderElement);
@@ -167,7 +167,7 @@ public class SSJavaAnalysis {
         }
       } else if (orderElement.contains("*")) {
         // spin loc definition
-        locOrder.addSpinLoc(orderElement);
+        locOrder.addSpinLoc(orderElement.substring(0,orderElement.length()-1));
       } else {
         // single element
         locOrder.put(orderElement);

diff --git a/Robust/src/Tests/ssJava/flowdown/test.java b/Robust/src/Tests/ssJava/flowdown/test.java
index f17f3f5b5b26f60fe642e75e84003d1f94ab405a..b0e75dadeb66e08e7672e19147e484f7e89b6ae3 100644 (file)
--- a/Robust/src/Tests/ssJava/flowdown/test.java
+++ b/Robust/src/Tests/ssJava/flowdown/test.java
@@ -27,13 +27,26 @@ public class test{
     }
     
     public void doit2(){
-       @LOC("methodH,testL") int localVarL;
-       
+       @LOC("methodH,testL") int localVarL;    
        // value flows from the field [local.methodH,field.testH]
        // to the local variable [local.methodL]
        localVarL=fieldH;
     }
 
+    public void doit3(){
+       @LOC("methodT,testL")int localVar=fooM.a+fooM.b;
+       // GLB(fooM.a,fooM.b)=LOC[methodT,testM,FB]
+       // LOC[lovalVar]=[methodT,testL] < GLB(fooM.a,fooM.b)
+    }
+
+    // creating composite location by object references
+    public void doit4(){
+       @LOC("methodT,testM,FC,BB") int localVar=fooM.bar.a; 
+       //LOC(fooM.bar.a)=[methodT,testM,FC,BA]
+       //localVar can flow into lower location of fooM.bar.a   
+       fooM.bar.c=localVar; //[methodT,testM,FC,BB] < [methodT,testM,FC,BA]
+    }
+
     // method has its own local variable lattice 
     @LATTICE("mL<mH,THISLOC=mH")
     public void doOwnLattice(){
@@ -57,6 +70,41 @@ public class test{
        fieldM=varDeltax2; //  DELTA[DELTA[mh,testH]] -> [mH,testM]     
     }
 
+    @LATTICE("mL<mSpin,mSpin<mH,mSpin*")
+    public void doSpinLoc(){
+       // if loc is defined with the suffix *, 
+       //value can be flowing around the same location
+       
+       @LOC("mH") int varH;
+       @LOC("mSpin") int varSpin;
+       @LOC("mL") int varL;
+
+       varH=10; 
+       while(varSpin>50000){
+           // value can be flowing back to the varSpin
+           // since 'varSpin' is location allowing value to move within
+           // the same abstract location
+           varSpin=varSpin+varH;     
+       }
+       varL=varSpin;
+    }
+
+    @LATTICE("mL<mH,THISLOC=mL")
+    public void doSpinField(){
+
+       @LOC("mH") int varH;
+       @LOC("mL") int varL;
+
+       @LOC("mH") Bar localBar=new Bar();
+
+       localBar.b2=localBar.b1; 
+       // LOC(localBar.b1)=[mH,BB]
+       // LOC(localBar.b2)=[mH,BB]
+       // b1 and b2 share the same abstract loc BB
+       // howerver, location BB allows values to be moving within itself
+       
+       localBar.b1++; // value can be moving among the same location
+    }
 }
 
 
@@ -67,6 +115,7 @@ class Foo{
     @LOC("FA") int a;
     @LOC("FB") int b;
     @LOC("FC") int c;
+    @LOC("FC") Bar bar;
        
     public Foo(){
     }
@@ -85,5 +134,14 @@ class Foo{
     public int doSomethingRtn(){
        return a+b; // going to return LOC[local.t,field.FB]
     }
-        
+
+}
+
+@LATTICE("BC<BB,BB<BA,BB*")
+class Bar{
+    @LOC("BA") int a;
+    @LOC("BB") int b2;
+    @LOC("BB") int b1;
+    @LOC("BC") int c;   
+
 }