changes on the loop termination analysis: associate a labeled statement with a corres...

diff --git a/Robust/src/Analysis/Loops/LoopTerminate.java b/Robust/src/Analysis/Loops/LoopTerminate.java
index 3cfbb3d0f1c1c202bb3af75b21aa286c21523526..f0111eb039dd0793f303eadf052767b214d80876 100644 (file)
--- a/Robust/src/Analysis/Loops/LoopTerminate.java
+++ b/Robust/src/Analysis/Loops/LoopTerminate.java
@@ -5,7 +5,9 @@ import java.util.HashSet;
 import java.util.Iterator;
 import java.util.Set;
 
+import Analysis.SSJava.SSJavaAnalysis;
 import IR.Operation;
+import IR.State;
 import IR.Flat.FKind;
 import IR.Flat.FlatCondBranch;
 import IR.Flat.FlatMethod;
@@ -28,10 +30,15 @@ public class LoopTerminate {
 
   Set<FlatNode> computed;
 
+  State state;
+  SSJavaAnalysis ssjava;
+
   /**
    * Constructor for Loop Termination Analysis
    */
-  public LoopTerminate() {
+  public LoopTerminate(SSJavaAnalysis ssjava, State state) {
+    this.ssjava = ssjava;
+    this.state = state;
     this.inductionSet = new HashSet<TempDescriptor>();
     this.inductionVar2DefNode = new HashMap<TempDescriptor, FlatNode>();
     this.derivedVar2basicInduction = new HashMap<TempDescriptor, TempDescriptor>();
@@ -93,10 +100,14 @@ public class LoopTerminate {
     assert loopEntrances.size() == 1;
     FlatNode loopEntrance = (FlatNode) loopEntrances.iterator().next();
 
-    init();
-    detectBasicInductionVar(loopElements);
-    detectDerivedInductionVar(loopElements);
-    checkConditionBranch(loopEntrance, loopElements);
+    String loopLabel = (String) state.fn2labelMap.get(loopEntrance);
+
+    if (loopLabel == null || !loopLabel.startsWith(ssjava.TERMINATE)) {
+      init();
+      detectBasicInductionVar(loopElements);
+      detectDerivedInductionVar(loopElements);
+      checkConditionBranch(loopEntrance, loopElements);
+    }
 
   }
 

diff --git a/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java b/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java
index bd585c07946071b4e58a5191068e29def188ceca..5dbcc8ad89b324218b0a3837bd8a3ab33ba1bda2 100644 (file)
--- a/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java
+++ b/Robust/src/Analysis/SSJava/MethodAnnotationCheck.java
@@ -203,20 +203,10 @@ public class MethodAnnotationCheck {
 
   private void checkBlockNode(MethodDescriptor md, SymbolTable nametable, BlockNode bn, boolean flag) {
     bn.getVarTable().setParent(nametable);
-    String label = bn.getLabel();
-    boolean isSSJavaLoop = flag;
-    if (label != null && label.equals(ssjava.SSJAVA)) {
-      if (isSSJavaLoop) {
-        throw new Error("Only outermost loop can be the self-stabilizing loop.");
-      } else {
-        annotatedMDSet.add(md);
-        isSSJavaLoop = true;
-      }
-    }
 
     for (int i = 0; i < bn.size(); i++) {
       BlockStatementNode bsn = bn.get(i);
-      checkBlockStatementNode(md, bn.getVarTable(), bsn, isSSJavaLoop);
+      checkBlockStatementNode(md, bn.getVarTable(), bsn, flag);
     }
 
   }
@@ -285,9 +275,21 @@ public class MethodAnnotationCheck {
   }
 
   private void checkLoopNode(MethodDescriptor md, SymbolTable nametable, LoopNode ln, boolean flag) {
+
+    String label = ln.getLabel();
+    boolean isSSJavaLoop = flag;
+    if (label != null && label.equals(ssjava.SSJAVA)) {
+      if (isSSJavaLoop) {
+        throw new Error("Only outermost loop can be the self-stabilizing loop.");
+      } else {
+        annotatedMDSet.add(md);
+        isSSJavaLoop = true;
+      }
+    }
+
     if (ln.getType() == LoopNode.WHILELOOP || ln.getType() == LoopNode.DOWHILELOOP) {
-      checkExpressionNode(md, nametable, ln.getCondition(), flag);
-      checkBlockNode(md, nametable, ln.getBody(), flag);
+      checkExpressionNode(md, nametable, ln.getCondition(), isSSJavaLoop);
+      checkBlockNode(md, nametable, ln.getBody(), isSSJavaLoop);
     } else {
       // For loop case
       /* Link in the initializer naming environment */
@@ -295,12 +297,12 @@ public class MethodAnnotationCheck {
       bn.getVarTable().setParent(nametable);
       for (int i = 0; i < bn.size(); i++) {
         BlockStatementNode bsn = bn.get(i);
-        checkBlockStatementNode(md, bn.getVarTable(), bsn, flag);
+        checkBlockStatementNode(md, bn.getVarTable(), bsn, isSSJavaLoop);
       }
       // check the condition
-      checkExpressionNode(md, bn.getVarTable(), ln.getCondition(), flag);
-      checkBlockNode(md, bn.getVarTable(), ln.getBody(), flag);
-      checkBlockNode(md, bn.getVarTable(), ln.getUpdate(), flag);
+      checkExpressionNode(md, bn.getVarTable(), ln.getCondition(), isSSJavaLoop);
+      checkBlockNode(md, bn.getVarTable(), ln.getBody(), isSSJavaLoop);
+      checkBlockNode(md, bn.getVarTable(), ln.getUpdate(), isSSJavaLoop);
     }
   }
 

diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
index d294a1928a8211b55a56d8d0072330e42518a8a8..a9f2e85853148123b2982b62790ee8a8cf952fa4 100644 (file)
--- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
+++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
@@ -92,15 +92,15 @@ public class SSJavaAnalysis {
   }
 
   public void doCheck() {
-    doMethodAnnotationCheck();
-    computeLinearTypeCheckMethodSet();
-    doLinearTypeCheck();
-    if (state.SSJAVADEBUG) {
-      debugPrint();
-    }
-    parseLocationAnnotation();
-    doFlowDownCheck();
-    doDefinitelyWrittenCheck();
+     doMethodAnnotationCheck();
+    // computeLinearTypeCheckMethodSet();
+    // doLinearTypeCheck();
+    // if (state.SSJAVADEBUG) {
+    // debugPrint();
+    // }
+    // parseLocationAnnotation();
+    // doFlowDownCheck();
+    // doDefinitelyWrittenCheck();
   }
 
   public void addTrustMethod(MethodDescriptor md) {
@@ -409,24 +409,12 @@ public class SSJavaAnalysis {
   }
 
   public void doLoopTerminationCheck(LoopOptimize lo, FlatMethod fm) {
-    LoopTerminate lt = new LoopTerminate();
+    LoopTerminate lt = new LoopTerminate(this,state);
     if (needTobeAnnotated(fm.getMethod())) {
       lt.terminateAnalysis(fm, lo.getLoopInvariant(fm));
     }
   }
 
-  public void doLoopTerminationCheck(LoopOptimize lo) {
-    LoopTerminate lt = new LoopTerminate();
-    for (Iterator iterator = annotationRequireSet.iterator(); iterator.hasNext();) {
-      MethodDescriptor md = (MethodDescriptor) iterator.next();
-      if (!skipLoopTerminate.containsKey(md)) {
-        FlatMethod fm = state.getMethodFlat(md);
-        lt.terminateAnalysis(fm, lo.getLoopInvariant(fm));
-      }
-    }
-
-  }
-
   public CallGraph getCallGraph() {
     return callgraph;
   }

diff --git a/Robust/src/IR/Flat/BuildFlat.java b/Robust/src/IR/Flat/BuildFlat.java
index dab3af931e3e79e2102fa359149fe8f45eef5109..a600b71a66953ad1ceafc5585992d0c229f2571e 100644 (file)
--- a/Robust/src/IR/Flat/BuildFlat.java
+++ b/Robust/src/IR/Flat/BuildFlat.java
@@ -309,10 +309,6 @@ public class BuildFlat {
       NodePair np=flattenBlockStatementNode(bn.get(i));
       FlatNode np_begin=np.getBegin();
       FlatNode np_end=np.getEnd();
-      if(bn.getLabel()!=null) {
-        // interim implementation to have the labeled statement
-        state.fn2labelMap.put(np_begin, bn.getLabel());
-      }
       if (begin==null) {
         begin=np_begin;
       }
@@ -1342,6 +1338,7 @@ public class BuildFlat {
   }
 
   private NodePair flattenLoopNode(LoopNode ln) {
+    
     HashSet oldbs=breakset;
     HashSet oldcs=continueset;
     breakset=new HashSet();
@@ -1383,6 +1380,9 @@ public class BuildFlat {
       }
       breakset=oldbs;
       continueset=oldcs;
+      if(ln.getLabel()!=null){
+        state.fn2labelMap.put(condition.getBegin(), ln.getLabel());
+      }
       return new NodePair(begin,nopend);
     } else if (ln.getType()==LoopNode.WHILELOOP) {
       TempDescriptor cond_temp=TempDescriptor.tempFactory("condition", new TypeDescriptor(TypeDescriptor.BOOLEAN));
@@ -1416,6 +1416,9 @@ public class BuildFlat {
       }
       breakset=oldbs;
       continueset=oldcs;
+      if(ln.getLabel()!=null){
+        state.fn2labelMap.put(begin, ln.getLabel());
+      }
       return new NodePair(begin,nopend);
     } else if (ln.getType()==LoopNode.DOWHILELOOP) {
       TempDescriptor cond_temp=TempDescriptor.tempFactory("condition", new TypeDescriptor(TypeDescriptor.BOOLEAN));
@@ -1448,6 +1451,9 @@ public class BuildFlat {
       }
       breakset=oldbs;
       continueset=oldcs;
+      if(ln.getLabel()!=null){
+        state.fn2labelMap.put(condition.getBegin(), ln.getLabel());
+      }
       return new NodePair(begin,nopend);
     } else throw new Error();
   }

diff --git a/Robust/src/IR/Tree/BlockNode.java b/Robust/src/IR/Tree/BlockNode.java
index 992928fb25854fe52e623b4cb1bc60c0bf220a39..e44e42de34d1360be380a0426c634df754038a7c 100644 (file)
--- a/Robust/src/IR/Tree/BlockNode.java
+++ b/Robust/src/IR/Tree/BlockNode.java
@@ -11,8 +11,6 @@ public class BlockNode extends TreeNode {
   public final static int NOBRACES=1;
   public final static int EXPRLIST=2;
 
-  String label=null;
-
   public BlockNode() {
     blockstatements=new Vector();
     table=new SymbolTable();
@@ -88,12 +86,4 @@ public class BlockNode extends TreeNode {
     return Kind.BlockNode;
   }
 
-  public void setLabel(String l) {
-    label=l;
-  }
-
-  public String getLabel() {
-    return label;
-  }
-
 }

diff --git a/Robust/src/IR/Tree/BuildIR.java b/Robust/src/IR/Tree/BuildIR.java
index f81d8bb959ab2dcc3839e219b2050ba7e181702c..cc3845eb77eb820bb20015a6b352d174a10a724e 100644 (file)
--- a/Robust/src/IR/Tree/BuildIR.java
+++ b/Robust/src/IR/Tree/BuildIR.java
@@ -1341,15 +1341,19 @@ public class BuildIR {
     return bn;
   }
 
-  public BlockNode parseSingleBlock(ParseNode pn) {
+  public BlockNode parseSingleBlock(ParseNode pn, String label){
     BlockNode bn=new BlockNode();
-    Vector bsv=parseBlockStatement(pn);
+    Vector bsv=parseBlockStatement(pn,label);
     for(int j=0; j<bsv.size(); j++) {
       bn.addBlockStatement((BlockStatementNode)bsv.get(j));
     }
     bn.setStyle(BlockNode.NOBRACES);
     return bn;
   }
+  
+  public BlockNode parseSingleBlock(ParseNode pn) {
+    return parseSingleBlock(pn,null);
+  }
 
   public Vector parseSESEBlock(Vector parentbs, ParseNode pn) {
     ParseNodeVector pnv=pn.getChildren();
@@ -1359,8 +1363,12 @@ public class BuildIR {
     }
     return bv;
   }
+  
+  public Vector parseBlockStatement(ParseNode pn){
+    return parseBlockStatement(pn,null);
+  }
 
-  public Vector parseBlockStatement(ParseNode pn) {
+  public Vector parseBlockStatement(ParseNode pn, String label) {
     Vector blockstatements=new Vector();
     if (isNode(pn,"tag_declaration")) {
       String name=pn.getChild("single").getTerminal();
@@ -1526,7 +1534,7 @@ public class BuildIR {
         // no condition clause, make a 'true' expression as the condition
         condition = (ExpressionNode) new LiteralNode("boolean", new Boolean(true));
       }
-      LoopNode ln=new LoopNode(init,condition,update,body);
+      LoopNode ln=new LoopNode(init,condition,update,body,label);
       ln.setNumLine(pn.getLine());
       blockstatements.add(ln);
     } else if (isNode(pn,"whilestatement")) {
@@ -1536,7 +1544,7 @@ public class BuildIR {
         // no condition clause, make a 'true' expression as the condition
         condition = (ExpressionNode) new LiteralNode("boolean", new Boolean(true));
       }
-      blockstatements.add(new LoopNode(condition,body,LoopNode.WHILELOOP));
+      blockstatements.add(new LoopNode(condition,body,LoopNode.WHILELOOP,label));
     } else if (isNode(pn,"dowhilestatement")) {
       ExpressionNode condition=parseExpression(pn.getChild("condition").getFirstChild());
       BlockNode body=parseSingleBlock(pn.getChild("statement").getFirstChild());
@@ -1544,7 +1552,7 @@ public class BuildIR {
         // no condition clause, make a 'true' expression as the condition
         condition = (ExpressionNode) new LiteralNode("boolean", new Boolean(true));
       }
-      blockstatements.add(new LoopNode(condition,body,LoopNode.DOWHILELOOP));
+      blockstatements.add(new LoopNode(condition,body,LoopNode.DOWHILELOOP,label));
     } else if (isNode(pn,"sese")) {
       ParseNode pnID=pn.getChild("identifier");
       String stID=null;
@@ -1575,9 +1583,8 @@ public class BuildIR {
       blockstatements.add(new GenReachNode(graphName) );
 
     } else if(isNode(pn,"labeledstatement")) {
-      String label = pn.getChild("name").getTerminal();
-      BlockNode bn=parseSingleBlock(pn.getChild("statement").getFirstChild());
-      bn.setLabel(label);
+      String labeledstatement = pn.getChild("name").getTerminal();
+      BlockNode bn=parseSingleBlock(pn.getChild("statement").getFirstChild(),labeledstatement);
       blockstatements.add(new SubBlockNode(bn));
     } else {
       System.out.println("---------------");

diff --git a/Robust/src/IR/Tree/LoopNode.java b/Robust/src/IR/Tree/LoopNode.java
index e85adf90b1d61defa413af4a7c118f09ceb03a48..f629d427df8a085950465579dd4e4972e1d76575 100644 (file)
--- a/Robust/src/IR/Tree/LoopNode.java
+++ b/Robust/src/IR/Tree/LoopNode.java
@@ -9,8 +9,9 @@ public class LoopNode extends BlockStatementNode {
   public static int FORLOOP=1;
   public static int WHILELOOP=2;
   public static int DOWHILELOOP=3;
+  String label=null;
 
-  public LoopNode(BlockNode initializer,ExpressionNode condition, BlockNode update, BlockNode body) {
+  public LoopNode(BlockNode initializer,ExpressionNode condition, BlockNode update, BlockNode body, String label) {
     this.initializer=initializer;
     this.condition=condition;
     this.update=update;
@@ -18,12 +19,14 @@ public class LoopNode extends BlockStatementNode {
     initializer.setStyle(BlockNode.EXPRLIST);
     update.setStyle(BlockNode.EXPRLIST);
     type=FORLOOP;
+    this.label=label;
   }
 
-  public LoopNode(ExpressionNode condition, BlockNode body, int type) {
+  public LoopNode(ExpressionNode condition, BlockNode body, int type, String label) {
     this.condition=condition;
     this.body=body;
     this.type=type;
+    this.label=label;
   }
 
   public BlockNode getInitializer() {
@@ -61,4 +64,12 @@ public class LoopNode extends BlockStatementNode {
   public int kind() {
     return Kind.LoopNode;
   }
+  
+  public void setLabel(String l) {
+    label=l;
+  }
+
+  public String getLabel() {
+    return label;
+  }
 }