From: yeom <yeom>
Date: Wed, 1 Jun 2011 01:26:29 +0000 (+0000)
Subject: having a location namespace. location names appeared in field lattice declaration... 
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=100445a0803f91bd20b9e490755a75ec8fb35365;p=IRC.git

having a location namespace. location names appeared in field lattice declaration are only valid within the declaration annotation. therefore a field location, which is an element of a composite location, will be specified by 'className.FieldLocation'. assuming that classname is unique right now but probably better to have a way to set each lattice with unique name.
---

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index 980a3266..f213b81b 100644
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -988,6 +988,24 @@ public class FlowDownCheck {
     return deltaLoc;
   }
 
+  private Location parseFieldLocDeclaraton(String decl) {
+
+    int idx = decl.indexOf(".");
+    String className = decl.substring(0, idx);
+    String fieldName = decl.substring(idx + 1);
+
+    Descriptor d = state.getClassSymbolTable().get(className);
+
+    assert (d instanceof ClassDescriptor);
+    SSJavaLattice<String> lattice = ssjava.getClassLattice((ClassDescriptor) d);
+    if (!lattice.containsKey(fieldName)) {
+      throw new Error("The location " + fieldName + " is not defined in the field lattice of '"
+          + className + "'.");
+    }
+
+    return new Location(d, fieldName);
+  }
+
   private CompositeLocation parseLocationDeclaration(MethodDescriptor md, TreeNode n, String locDec) {
 
     CompositeLocation compLoc = new CompositeLocation();
@@ -1017,16 +1035,18 @@ public class FlowDownCheck {
 
     for (int i = 1; i < locIdList.size(); i++) {
       String locName = locIdList.get(i);
-      ClassDescriptor cd = fieldLocName2cd.get(locName);
-
-      SSJavaLattice<String> fieldLattice = CompositeLattice.getLatticeByDescriptor(cd);
 
-      if (fieldLattice == null || (!fieldLattice.containsKey(locName))) {
-        throw new Error("Location " + locName + " is not defined in the field lattice at "
-            + cd.getSourceFileName() + ".");
-      }
-
-      Location fieldLoc = new Location(cd, locName);
+      Location fieldLoc = parseFieldLocDeclaraton(locName);
+      // ClassDescriptor cd = fieldLocName2cd.get(locName);
+      // SSJavaLattice<String> fieldLattice =
+      // CompositeLattice.getLatticeByDescriptor(cd);
+      //
+      // if (fieldLattice == null || (!fieldLattice.containsKey(locName))) {
+      // throw new Error("Location " + locName +
+      // " is not defined in the field lattice at "
+      // + cd.getSourceFileName() + ".");
+      // }
+      // Location fieldLoc = new Location(cd, locName);
       compLoc.addLocation(fieldLoc);
     }
 
diff --git a/Robust/src/Analysis/SSJava/MethodLattice.java b/Robust/src/Analysis/SSJava/MethodLattice.java
index 39a9b461..095c736e 100644
--- a/Robust/src/Analysis/SSJava/MethodLattice.java
+++ b/Robust/src/Analysis/SSJava/MethodLattice.java
@@ -1,7 +1,5 @@
 package Analysis.SSJava;
 
-import Util.Lattice;
-
 public class MethodLattice<T> extends SSJavaLattice<T> {
 
   private T thisLoc;
diff --git a/Robust/src/Tests/ssJava/flowdown/test.java b/Robust/src/Tests/ssJava/flowdown/test.java
index 5ca81e3f..b0ac6246 100644
--- a/Robust/src/Tests/ssJava/flowdown/test.java
+++ b/Robust/src/Tests/ssJava/flowdown/test.java
@@ -40,21 +40,21 @@ public class test{
     }
     
     public void doit2(){
-	@LOC("methodH,testL") int localVarL;	
+	@LOC("methodH,test.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;
+	@LOC("methodT,test.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("methodT,test.testM,Foo.FC,Bar.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]
@@ -71,10 +71,10 @@ public class test{
       
     @LATTICE("mL<mH,THISLOC=mH")
     public void doDelta(){
-	@LOC("DELTA(mH,testH)") int varDelta;
+	@LOC("DELTA(mH,test.testH)") int varDelta;
 	// LOC(varDelta) is slightly lower than [mH, testH]
 
-	@LOC("DELTA(DELTA(mH,testH))") int varDeltax2;
+	@LOC("DELTA(DELTA(mH,test.testH))") int varDeltax2;
 	// applying double delta to [mH,testH]
 	
 	varDelta=fieldH; // [mH,testH] -> DELTA[mh,testH]
@@ -132,7 +132,7 @@ public class test{
 
     @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]
+	@LOC("DELTA(mH,test.testH,Foo.FA)") int value=globalFoo.a; // LOC(globalFoo.a)=[mH,testH,FA]
 	globalFoo.b=value;		
     }  
 
@@ -217,6 +217,5 @@ class Bar{
     @LOC("BB") int b1;
     @LOC("BC") int c;   
     @LOC("BC") static int d;
-
-
 }
+