small changes: have a way to specify the location of "this".

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index c9077678ca31f202a639564ba0f46ab1e6735fff..eda6e0d6c6f40066630efaade6a5cb7eafd54ba5 100644 (file)
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -43,6 +43,7 @@ import IR.Tree.SubBlockNode;
 import IR.Tree.TertiaryNode;
 import IR.Tree.TreeNode;
 import Util.Lattice;
+import Util.Pair;
 
 public class FlowDownCheck {
 
@@ -915,8 +916,8 @@ public class FlowDownCheck {
       destLocation =
           srcLocation = checkLocationFromExpressionNode(md, nametable, an.getDest(), srcLocation);
 
-      if (!((Set<String>) state.getCd2LocationPropertyMap().get(cd)).contains(destLocation
-          .getLocation(cd).getLocIdentifier())) {
+      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());
       }
@@ -1188,7 +1189,8 @@ public class FlowDownCheck {
       if (priorityLoc1.getLocIdentifier().equals(priorityLoc2.getLocIdentifier())) {
         // have the same level of local hierarchy
 
-        Set<String> spinSet = (Set<String>) state.getCd2LocationPropertyMap().get(cd);
+        Set<String> spinSet =
+            (Set<String>) state.getCd2LocationPropertyMap().get(new Pair(cd, "spin"));
         if (spinSet != null && spinSet.contains(priorityLoc1.getLocIdentifier())) {
           // this location can be spinning
           return ComparisonResult.GREATER;

diff --git a/Robust/src/IR/State.java b/Robust/src/IR/State.java
index a5d048b2632df9ed1105c165d342dfd019b2e984..51ba8d3ad88d23539f58ed54010aa58096574f9a 100644 (file)
--- a/Robust/src/IR/State.java
+++ b/Robust/src/IR/State.java
@@ -3,6 +3,7 @@ import IR.Tree.*;
 import IR.Flat.*;
 import IR.*;
 import Util.Lattice;
+import Util.Pair;
 
 import java.util.*;
 import Analysis.TaskStateAnalysis.*;
@@ -368,8 +369,8 @@ public class State {
     return cd2locationOrderMap;
   }
 
-  public void addLocationPropertySet(ClassDescriptor cd, Set<String> set) {
-    cd2locationPropertyMap.put(cd,set);
+  public void addLocationProperty(Pair key, Object value) {
+    cd2locationPropertyMap.put(key,value);
   }
 
   public Hashtable getCd2LocationPropertyMap() {

diff --git a/Robust/src/IR/Tree/BuildIR.java b/Robust/src/IR/Tree/BuildIR.java
index 9dedbe76cd6c8f22fcdd482490738a3125952954..ca20689fe18fd3fcf6032f3ae1c4b541cffbc2df 100644 (file)
--- a/Robust/src/IR/Tree/BuildIR.java
+++ b/Robust/src/IR/Tree/BuildIR.java
@@ -1,6 +1,7 @@
 package IR.Tree;
 import IR.*;
 import Util.Lattice;
+import Util.Pair;
 
 import java.io.File;
 import java.util.*;
@@ -632,11 +633,16 @@ public class BuildIR {
     Lattice<String> locOrder =
       new Lattice<String>("_top_","_bottom_");
     Set<String> spinLocSet=new HashSet<String>();
+    String thisLoc=null;
     for (int i = 0; i < pnv.size(); i++) {
       ParseNode loc = pnv.elementAt(i);
       if(isNode(loc,"location_property")) {
-        String spinLoc=loc.getChildren().elementAt(0).getLabel();
-        spinLocSet.add(spinLoc);
+        if(loc.getFirstChild().getLabel().equals("location_multi")){
+          String spinLoc=loc.getFirstChild().getFirstChild().getLabel();
+          spinLocSet.add(spinLoc);
+        }else{
+          thisLoc=loc.getFirstChild().getFirstChild().getLabel();
+        }
       } else {
         if(loc.getChildren().size()==1){
           String locIentifier=loc.getChildren().elementAt(0).getLabel();
@@ -661,7 +667,10 @@ public class BuildIR {
                           locID + "' is not defined in the hierarchy of the class '"+cd +"'.");
         }
       }
-      state.addLocationPropertySet(cd, spinLocSet);
+      state.addLocationProperty(new Pair(cd,"spin"), spinLocSet);
+    }
+    if(thisLoc!=null){
+      state.addLocationProperty(new Pair(cd,"this"), thisLoc);
     }
     state.addLocationOrder(cd, locOrder);
   }

diff --git a/Robust/src/Parse/java14.cup b/Robust/src/Parse/java14.cup
index d37ae7f495abf6bea5666e01e07a4d465bcba57f..daf3c1818eea75d8cecc6464d1ab8cea0b9a0334 100644 (file)
--- a/Robust/src/Parse/java14.cup
+++ b/Robust/src/Parse/java14.cup
@@ -164,7 +164,8 @@ non terminal ParseNode explicit_constructor_invocation;
 non terminal ParseNode location_order_declaration, location_order_list, location_order;
 // 19.9.1) Interface Declarations
 non terminal ParseNode interface_declaration;
-non terminal ParseNode normal_interface_declaration, annotation_type_declaration;
+//non terminal ParseNode normal_interface_declaration
+non terminal ParseNode annotation_type_declaration;
 non terminal ParseNode extends_interfaces_opt, extends_interfaces;
 non terminal ParseNode interface_body;
 non terminal ParseNode interface_member_declarations_opt, interface_member_declarations;
@@ -288,7 +289,8 @@ non terminal ParseNode enum_body, enum_constants_opt, enum_constants, enum_const
 //non terminal ParseNode enum_arguments_opt, enum_body_declarations_opt;
 
 // annotation expressions
-non terminal ParseNode annotations_opt, annotations, annotations_at, annotation, annotation_body;
+// non terminal ParseNode annotations_opt, 
+non terminal ParseNode annotations, annotations_at, annotation, annotation_body;
 non terminal ParseNode normal_annotation_body, marker_annotation_body;
 non terminal ParseNode single_element_annotation_body;
 non terminal ParseNode annotation_type_body, annotation_type_element_declarations;
@@ -1319,7 +1321,7 @@ location_order ::=
         :}
        |       IDENTIFIER:loc MULT{:
                ParseNode pn=new ParseNode("location_property",parser.lexer.line_num);          
-               pn.addChild(loc);
+               pn.addChild("location_multi").addChild(loc);
                RESULT=pn;
        :}
        |       IDENTIFIER:loc {:
@@ -1327,6 +1329,11 @@ location_order ::=
                pn.addChild(loc);
                RESULT=pn;
        :}
+       |       THIS COLON IDENTIFIER:loc {:
+               ParseNode pn=new ParseNode("location_property",parser.lexer.line_num);
+               pn.addChild("location_this").addChild(loc);
+               RESULT=pn;
+       :}
         ;
 
 // 19.9) Interfaces