From b31fa5222b2fff2a5c294ccf8c2bb95eec78fe1a Mon Sep 17 00:00:00 2001
From: yeom <yeom>
Date: Thu, 14 Apr 2011 21:20:14 +0000
Subject: [PATCH] extends the grammar to have a way to define a new type of
 location that is allowed to have spinning values

---
 Robust/src/Analysis/SSJava/FlowDownCheck.java | 12 ++++++----
 Robust/src/IR/State.java                      | 10 ++++++++
 Robust/src/IR/Tree/BuildIR.java               | 23 +++++++++++++------
 Robust/src/Parse/java14.cup                   |  5 ++++
 4 files changed, 39 insertions(+), 11 deletions(-)

diff --git a/Robust/src/Analysis/SSJava/FlowDownCheck.java b/Robust/src/Analysis/SSJava/FlowDownCheck.java
index f596794a..ac4899c5 100644
--- a/Robust/src/Analysis/SSJava/FlowDownCheck.java
+++ b/Robust/src/Analysis/SSJava/FlowDownCheck.java
@@ -201,6 +201,9 @@ public class FlowDownCheck {
         checkDeclarationInBlockStatementNode(md, nametable, bsn);
       }
     }
+
+    // check loop body
+    checkDeclarationInBlockNode(md, nametable, ln.getBody());
   }
 
   private void checkMethodBody(ClassDescriptor cd, MethodDescriptor md) {
@@ -925,7 +928,7 @@ public class FlowDownCheck {
 
     public static boolean isGreaterThan(Location loc1, Location loc2, ClassDescriptor priorityCD) {
 
-      //System.out.println("isGreaterThan=" + loc1 + " ? " + loc2);
+      // System.out.println("isGreaterThan=" + loc1 + " ? " + loc2);
       CompositeLocation compLoc1;
       CompositeLocation compLoc2;
 
@@ -946,7 +949,8 @@ public class FlowDownCheck {
       }
 
       // comparing two composite locations
-      // System.out.println("compare base location=" + compLoc1 + " ? " + compLoc2);
+      // System.out.println("compare base location=" + compLoc1 + " ? " +
+      // compLoc2);
 
       int baseCompareResult = compareBaseLocationSet(compLoc1, compLoc2, priorityCD);
       if (baseCompareResult == ComparisonResult.EQUAL) {
@@ -991,8 +995,8 @@ public class FlowDownCheck {
 
       if (priorityLoc1.getLocIdentifier().equals(priorityLoc2.getLocIdentifier())) {
         // have the same level of local hierarchy
-      } else if (locationOrder.isGreaterThan(priorityLoc1.getLocIdentifier(), priorityLoc2
-          .getLocIdentifier())) {
+      } else if (locationOrder.isGreaterThan(priorityLoc1.getLocIdentifier(),
+          priorityLoc2.getLocIdentifier())) {
         // if priority loc of compLoc1 is higher than compLoc2
         // then, compLoc 1 is higher than compLoc2
         return ComparisonResult.GREATER;
diff --git a/Robust/src/IR/State.java b/Robust/src/IR/State.java
index dc488eab..22f31a27 100644
--- a/Robust/src/IR/State.java
+++ b/Robust/src/IR/State.java
@@ -40,6 +40,7 @@ public class State {
     this.excprefetch=new HashSet();
     this.classpath=new Vector();
     this.cd2locationOrderMap=new Hashtable();
+    this.cd2locationPropertyMap=new Hashtable();
     this.lines=0;
   }
 
@@ -206,6 +207,7 @@ public class State {
   private int numstaticblocks=0;
   private int arraycount=0;
   public Hashtable cd2locationOrderMap;
+  public Hashtable cd2locationPropertyMap;
   public boolean OPTIMIZE=false;
   public boolean LINENUM=false;
 
@@ -357,4 +359,12 @@ public class State {
     return cd2locationOrderMap;
   }
   
+  public void addLocationPropertySet(ClassDescriptor cd, Set<String> set){
+    cd2locationPropertyMap.put(cd,set);
+  }
+  
+  public Hashtable getCd2LocationPropertyMap(){
+    return cd2locationOrderMap;
+  }
+  
 }
diff --git a/Robust/src/IR/Tree/BuildIR.java b/Robust/src/IR/Tree/BuildIR.java
index 04ba43b1..2f0277a1 100644
--- a/Robust/src/IR/Tree/BuildIR.java
+++ b/Robust/src/IR/Tree/BuildIR.java
@@ -504,17 +504,26 @@ public void parseInitializers(ClassDescriptor cn){
   private void parseLocationOrder(ClassDescriptor cd, ParseNode pn) {
     ParseNodeVector pnv = pn.getChildren();
     Lattice<String> locOrder =
-        new Lattice<String>("_top_","_bottom_");
+        new Lattice<String>("_top_","_bottom_");            
+    Set<String> spinLocSet=new HashSet<String>();
     for (int i = 0; i < pnv.size(); i++) {
       ParseNode loc = pnv.elementAt(i);
-      String lowerLoc=loc.getChildren().elementAt(0).getLabel();
-      String higherLoc= loc.getChildren().elementAt(1).getLabel();
-      locOrder.put(higherLoc, lowerLoc);
-      if (locOrder.isIntroducingCycle(higherLoc)) {
-        throw new Error("Error: the order relation " + lowerLoc + " < " + higherLoc
-            + " introduces a cycle.");
+      if(isNode(loc,"location_property")){
+        String spinLoc=loc.getChildren().elementAt(0).getLabel();
+        spinLocSet.add(spinLoc);
+      }else{
+        String lowerLoc=loc.getChildren().elementAt(0).getLabel();
+        String higherLoc= loc.getChildren().elementAt(1).getLabel();
+        locOrder.put(higherLoc, lowerLoc);
+        if (locOrder.isIntroducingCycle(higherLoc)) {
+          throw new Error("Error: the order relation " + lowerLoc + " < " + higherLoc
+              + " introduces a cycle.");
+        }
       }
     }
+    if(spinLocSet.size()>0){
+      state.addLocationPropertySet(cd, spinLocSet);
+    }
     state.addLocationOrder(cd, locOrder);
   }
   
diff --git a/Robust/src/Parse/java14.cup b/Robust/src/Parse/java14.cup
index 65ccd7a4..e72d7c9d 100644
--- a/Robust/src/Parse/java14.cup
+++ b/Robust/src/Parse/java14.cup
@@ -1309,6 +1309,11 @@ location_order ::=
 		pn.addChild(loc2);
 		RESULT=pn;         
         :}
+	|	IDENTIFIER:loc MULT{:
+	      	ParseNode pn=new ParseNode("location_property",parser.lexer.line_num);		
+		pn.addChild(loc);
+		RESULT=pn;
+	:}
         ;
 
 // 19.9) Interfaces
-- 
2.34.1