From: yeom <yeom>
Date: Tue, 24 May 2011 00:45:34 +0000 (+0000)
Subject: bug fixes and few extra things:
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=96113b0465d7bfaac70a4bddc83b811a65560907;p=IRC.git

bug fixes and few extra things:
-static final field has TOP location by default
-do not allow to copy values from one class global variable to another class global variable since they're not comparable.
---

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index de46e711..8efeba5b 100644
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -272,8 +272,8 @@ public class FlowDownCheck {
     return loc;
   }
 
-  private boolean hasOnlyLiteralValue(ExpressionNode returnExp) {
-    if (returnExp.kind() == Kind.LiteralNode) {
+  private boolean hasOnlyLiteralValue(ExpressionNode en) {
+    if (en.kind() == Kind.LiteralNode) {
       return true;
     } else {
       return false;
@@ -397,12 +397,11 @@ public class FlowDownCheck {
 
     CompositeLocation destLoc = d2loc.get(vd);
 
-    ClassDescriptor localCD = md.getClassDesc();
     if (dn.getExpression() != null) {
       CompositeLocation expressionLoc =
           checkLocationFromExpressionNode(md, nametable, dn.getExpression(),
               new CompositeLocation());
-      addTypeLocation(dn.getExpression().getType(), expressionLoc);
+      // addTypeLocation(dn.getExpression().getType(), expressionLoc);
 
       if (expressionLoc != null) {
         // checking location order
@@ -627,7 +626,8 @@ public class FlowDownCheck {
     if (min.getBaseName() != null) {
       Descriptor d = nametable.get(min.getBaseName().getSymbol());
       if (d instanceof VarDescriptor) {
-        CompositeLocation varLoc = (CompositeLocation) ((VarDescriptor) d).getType().getExtension();
+        CompositeLocation varLoc =
+            ((CompositeLocation) ((VarDescriptor) d).getType().getExtension()).clone();
         return varLoc;
       } else {
         // it is field descriptor
@@ -719,9 +719,11 @@ 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();
 
@@ -783,6 +785,7 @@ public class FlowDownCheck {
 
     NameDescriptor nd = nn.getName();
     if (nd.getBase() != null) {
+
       loc = checkLocationFromExpressionNode(md, nametable, nn.getExpression(), loc);
       // addTypeLocation(nn.getExpression().getType(), loc);
     } else {
@@ -812,11 +815,30 @@ public class FlowDownCheck {
         // the type of field descriptor has a location!
         FieldDescriptor fd = (FieldDescriptor) d;
 
-        // the location of field access starts from this, followed by field
-        // location
-        MethodLattice<String> localLattice = ssjava.getMethodLattice(md);
-        Location thisLoc = new Location(md, localLattice.getThisLoc());
-        loc.addLocation(thisLoc);
+        if (fd.isStatic()) {
+          if (fd.isFinal()) {
+            // if it is 'static final', the location has TOP since no one can
+            // change its value
+            loc.addLocation(Location.createTopLocation(md));
+          } else {
+            // if 'static', the location has pre-assigned global loc
+            MethodLattice<String> localLattice = ssjava.getMethodLattice(md);
+            String globalLocId = localLattice.getGlobalLoc();
+            if (globalLocId == null) {
+              throw new Error("Global location element is not defined in the method " + md);
+            }
+            Location globalLoc = new Location(md, globalLocId);
+
+            loc.addLocation(globalLoc);
+          }
+        } else {
+          // the location of field access starts from this, followed by field
+          // location
+          MethodLattice<String> localLattice = ssjava.getMethodLattice(md);
+          Location thisLoc = new Location(md, localLattice.getThisLoc());
+          loc.addLocation(thisLoc);
+        }
+
         Location fieldLoc = (Location) fd.getType().getExtension();
         loc.addLocation(fieldLoc);
       }
@@ -855,11 +877,19 @@ public class FlowDownCheck {
         checkLocationFromExpressionNode(md, nametable, an.getDest(), new CompositeLocation());
 
     CompositeLocation srcLocation = new CompositeLocation();
+
     if (!postinc) {
+      if (hasOnlyLiteralValue(an.getSrc())) {
+        // if source is literal value, src location is TOP. so do not need to
+        // compare!
+        return destLocation;
+      }
       srcLocation = new CompositeLocation();
       srcLocation = checkLocationFromExpressionNode(md, nametable, an.getSrc(), srcLocation);
-//      System.out.println("an=" + an.printNode(0) + " an.getSrc()=" + an.getSrc().getClass()
+//      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)) {
         throw new Error("The value flow from " + srcLocation + " to " + destLocation
             + " does not respect location hierarchy on the assignment " + an.printNode(0) + " at "
@@ -1060,7 +1090,7 @@ public class FlowDownCheck {
 
     public static boolean isGreaterThan(CompositeLocation loc1, CompositeLocation loc2) {
 
-//      System.out.println("isGreaterThan= " + loc1 + " " + loc2);
+      // System.out.println("isGreaterThan= " + loc1 + " " + loc2);
 
       int baseCompareResult = compareBaseLocationSet(loc1, loc2);
       if (baseCompareResult == ComparisonResult.EQUAL) {
diff --git a/Robust/src/Analysis/SSJava/SingleReferenceCheck.java b/Robust/src/Analysis/SSJava/SingleReferenceCheck.java
index 1bd0bf03..5053e29e 100644
--- a/Robust/src/Analysis/SSJava/SingleReferenceCheck.java
+++ b/Robust/src/Analysis/SSJava/SingleReferenceCheck.java
@@ -120,33 +120,25 @@ public class SingleReferenceCheck {
   }
 
   private void checkAssignmentNode(AssignmentNode an) {
-
-    if (an.getSrc() != null) {
-      if (an.getSrc().getType().isPtr() && (!an.getSrc().getType().isNull())
-          && !(an.getSrc() instanceof CreateObjectNode)) {
-        if (an.getSrc() instanceof CastNode) {
-          needToNullify = ((CastNode) an.getSrc()).getExpression().printNode(0);
-        } else {
-          needToNullify = an.getSrc().printNode(0);
-        }
-      }
-
-    }
+    needToNullify(an.getSrc());
   }
 
   private void checkDeclarationNode(DeclarationNode dn) {
+    needToNullify(dn.getExpression());
+  }
 
-    if (dn.getExpression() != null) {
-      if (dn.getExpression().getType().isPtr() && !(dn.getExpression() instanceof CreateObjectNode)) {
+  private void needToNullify(ExpressionNode en) {
 
-        if (dn.getExpression() instanceof CastNode) {
-          needToNullify = ((CastNode) dn.getExpression()).getExpression().printNode(0);
+    if (en != null && en.getType().isPtr() && !en.getType().isString()) {
+      if (en.kind() != Kind.CreateObjectNode && en.kind() != Kind.LiteralNode) {
+        if (en.kind() == Kind.CastNode) {
+          needToNullify = ((CastNode) en).getExpression().printNode(0);
         } else {
-          needToNullify = dn.getExpression().printNode(0);
+          needToNullify = en.printNode(0);
         }
-
       }
     }
+
   }
 
 }
diff --git a/Robust/src/Tests/ssJava/flowdown/test.java b/Robust/src/Tests/ssJava/flowdown/test.java
index 71ed4f1a..57d24006 100644
--- a/Robust/src/Tests/ssJava/flowdown/test.java
+++ b/Robust/src/Tests/ssJava/flowdown/test.java
@@ -1,17 +1,21 @@
 @LATTICE("testL<testM,testM<testH")
-@METHODDEFAULT("methodL<methodH,methodH<methodT,THISLOC=methodT")
+@METHODDEFAULT("methodL<methodH,methodH<methodT,THISLOC=methodT,GLOBALLOC=methodT")
 public class test{
 
     @LOC("testH") int fieldH;
     @LOC("testM") int fieldM;
     @LOC("testL") int fieldL;
     @LOC("testM") Foo fooM;
+    @LOC("testH") static int globalH;
+    @LOC("testH") static Foo globalFoo;
+    @LOC("testH") static final String finalValue="FINAL";
+
 
     public static void main (@LOC("methodH") String args[]){       
 	@LOC("methodH") test t=new test();
 	t.doit();
     }
-
+    
     public void doit(){
 	@LOC("methodH") int localH; // LOC=[local.methodH]
 	fooM=new Foo(); // LOC=[local.methodT, field.testM]
@@ -114,13 +118,32 @@ public class test{
 	@LOC("methodL") Bar newBar_2;
 	newBar_2=f_1.bar;
 	f_1.bar=null; // should assign null here 
-	
+    }
+    
+
+    @LATTICE("mL<mM,mM<mH,GLOBALLOC=mH,THISLOC=mL")
+    public void globalField(){       
+	@LOC("DELTA(mH,testH,FA)") int value=globalFoo.a; // LOC(globalFoo.a)=[mH,testH,FA]
+	globalFoo.b=value;		
+    }  
+
+    public void globalTopField(){
+	@LOC("methodH") String valueH;
+	valueH=finalValue; // LOC(finalVAlue)=[TOP,testH]
+    }
+
+    public void globalCopy(){
+	// do not allow the below case
+	// it copies something from one calss global variable 
+	// to another class global variable
+
+	//globalH=Foo.d;
     }
 
 }
 
 
-@LATTICE("FC<FB,FB<FA")
+@LATTICE("FD<FC,FC<FB,FB<FA")
 @METHODDEFAULT("fm_L<fm_M1,fm_L<fm_M2,fm_M1<fm_H,fm_M2<fm_H,THISLOC=fm_H")
 class Foo{
 	
@@ -128,6 +151,7 @@ class Foo{
     @LOC("FB") int b;
     @LOC("FC") int c;
     @LOC("FC") Bar bar;
+    @LOC("FA") static int d;
 	
     public Foo(){
     }
@@ -156,5 +180,7 @@ class Bar{
     @LOC("BB") int b2;
     @LOC("BB") int b1;
     @LOC("BC") int c;   
+    @LOC("BC") static int d;
+
 
 }