Be able to get def reach state out at a given program point

diff --git a/Robust/src/Analysis/Disjoint/DefiniteReachAnalysis.java b/Robust/src/Analysis/Disjoint/DefiniteReachAnalysis.java
index 098fc9ca589979ecefde46d930c4d22d363d26a1..cb69890cadd700c1f822407cd94079973bb5ab2e 100644 (file)
--- a/Robust/src/Analysis/Disjoint/DefiniteReachAnalysis.java
+++ b/Robust/src/Analysis/Disjoint/DefiniteReachAnalysis.java
@@ -1,5 +1,6 @@
 package Analysis.Disjoint;
 
+import java.io.*;
 import java.util.*;
 
 import IR.*;
@@ -67,6 +68,18 @@ public class DefiniteReachAnalysis {
   }
 
 
+  public void writeState( FlatNode fn, String outputName ) {
+    DefiniteReachState state = makeIn( fn );
+    try {
+      BufferedWriter bw = new BufferedWriter( new FileWriter( outputName+".txt" ) );
+      bw.write( state.toString() );
+      bw.close();
+    } catch( IOException e ) {
+      System.out.println( "ERROR writing definite reachability state:\n  "+e );
+    }
+  }
+
+
   // get the current state for just after the given
   // program point
   private DefiniteReachState get( FlatNode fn ) {

diff --git a/Robust/src/Analysis/Disjoint/DefiniteReachState.java b/Robust/src/Analysis/Disjoint/DefiniteReachState.java
index 06525ffbdd75c35052479281f16dd8e2cd533fb4..a08b4a2b264f7243bfecca06cc85ce2df21ece65 100644 (file)
--- a/Robust/src/Analysis/Disjoint/DefiniteReachState.java
+++ b/Robust/src/Analysis/Disjoint/DefiniteReachState.java
@@ -37,7 +37,7 @@ public class DefiniteReachState {
     rs = new HashMap<TempDescriptor, DefReachKnown>();
   }
 
-  // what are the transfer functions that are relevant for this analyis?
+
 
   public void methodEntry(Set<TempDescriptor> parameters) {
     // R' := {}

diff --git a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
index d170b65efffd9298b72333865a62129530556dd6..5c230a4a6d19b48b1108b3cc9c6e56b8dbba24a0 100644 (file)
--- a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
+++ b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
@@ -1330,6 +1330,14 @@ public class DisjointAnalysis implements HeapAnalysis {
     } break;
 
 
+    case FKind.FlatGenDefReachNode: {
+      FlatGenDefReachNode fgdrn = (FlatGenDefReachNode) fn;
+      if( doDefiniteReachAnalysis ) {
+        definiteReachAnalysis.writeState( fn, fgdrn.getOutputName() );
+      }
+    } break;
+
+
     case FKind.FlatMethod: {
       // construct this method's initial heap model (IHM)
       // since we're working on the FlatMethod, we know

diff --git a/Robust/src/Analysis/Disjoint/PointerMethod.java b/Robust/src/Analysis/Disjoint/PointerMethod.java
index 5246c9b8deb1923e9a11ac37042f18a517a0e530..aaab9a8710da4790750c5ecbf3c1380a7095ed4b 100644 (file)
--- a/Robust/src/Analysis/Disjoint/PointerMethod.java
+++ b/Robust/src/Analysis/Disjoint/PointerMethod.java
@@ -99,6 +99,7 @@ public class PointerMethod {
     case FKind.FlatSESEEnterNode:
     case FKind.FlatSESEExitNode:
     case FKind.FlatGenReachNode:
+    case FKind.FlatGenDefReachNode:
     case FKind.FlatExit:
       return true;
 

diff --git a/Robust/src/Analysis/Loops/DeadCode.java b/Robust/src/Analysis/Loops/DeadCode.java
index c3ba42a01b541c733f946c46e242548e8ac02734..f944819c9db979fe0014d9705ddff24109464c27 100644 (file)
--- a/Robust/src/Analysis/Loops/DeadCode.java
+++ b/Robust/src/Analysis/Loops/DeadCode.java
@@ -38,6 +38,7 @@ nextfn:
         case FKind.FlatSESEEnterNode:
         case FKind.FlatSESEExitNode:
         case FKind.FlatGenReachNode:
+        case FKind.FlatGenDefReachNode:
           if (!useful.contains(fn)) {
             useful.add(fn);
             changed=true;

diff --git a/Robust/src/IR/Flat/BuildCode.java b/Robust/src/IR/Flat/BuildCode.java
index 5b32498fabf58f22f83f75eda0d409621f8f8a65..6773d14fde99696eee81728fd95385f3ddd330a6 100644 (file)
--- a/Robust/src/IR/Flat/BuildCode.java
+++ b/Robust/src/IR/Flat/BuildCode.java
@@ -2378,7 +2378,8 @@ fldloop:
       break;
 
     case FKind.FlatGenReachNode:
-      // this node is just for generating a reach graph
+    case FKind.FlatGenDefReachNode:
+      // these nodes are just for generating analysis data
       // in disjointness analysis at a particular program point
       break;
 

diff --git a/Robust/src/IR/Flat/BuildFlat.java b/Robust/src/IR/Flat/BuildFlat.java
index c506e7ada8f3d1b1139f1431c0ef53005dde145c..8eb9ce6a8132d484af47e35a7959352f7f706ab9 100644 (file)
--- a/Robust/src/IR/Flat/BuildFlat.java
+++ b/Robust/src/IR/Flat/BuildFlat.java
@@ -1608,6 +1608,11 @@ public class BuildFlat {
     return new NodePair(fgrn, fgrn);
   }
 
+  private NodePair flattenGenDefReachNode(GenDefReachNode gdrn) {
+    FlatGenDefReachNode fgdrn = new FlatGenDefReachNode(gdrn.getOutputName() );
+    return new NodePair(fgdrn, fgdrn);
+  }
+
   private NodePair flattenSESENode(SESENode sn) {
     if( sn.isStart() ) {
       FlatSESEEnterNode fsen=new FlatSESEEnterNode(sn);
@@ -1761,6 +1766,9 @@ public class BuildFlat {
     case Kind.GenReachNode:
       return flattenGenReachNode((GenReachNode)bsn);
 
+    case Kind.GenDefReachNode:
+      return flattenGenDefReachNode((GenDefReachNode)bsn);
+
     case Kind.ContinueBreakNode:
       return flattenContinueBreakNode((ContinueBreakNode)bsn);
     }

diff --git a/Robust/src/IR/Flat/FKind.java b/Robust/src/IR/Flat/FKind.java
index 89cbf47474c786afb2fd029cdb89e6cd8489855b..3acc8fc598b53c4116086b0c4e347a9cc9ee67b7 100644 (file)
--- a/Robust/src/IR/Flat/FKind.java
+++ b/Robust/src/IR/Flat/FKind.java
@@ -29,4 +29,5 @@ public class FKind {
   public static final int FlatInstanceOfNode=26;
   public static final int FlatExit=27;
   public static final int FlatGenReachNode=28;
+  public static final int FlatGenDefReachNode=29;
 }

diff --git a/Robust/src/IR/Flat/FlatGenDefReachNode.java b/Robust/src/IR/Flat/FlatGenDefReachNode.java
new file mode 100644 (file)
index 0000000..47e8dce
--- /dev/null
+++ b/Robust/src/IR/Flat/FlatGenDefReachNode.java
@@ -0,0 +1,35 @@
+package IR.Flat;
+import IR.TypeDescriptor;
+
+public class FlatGenDefReachNode extends FlatNode {
+  String outputName;
+
+  public FlatGenDefReachNode(String outputName) {
+    this.outputName = outputName;
+  }
+
+  public String getOutputName() {
+    return outputName;
+  }
+
+  public FlatNode clone(TempMap t) {
+    return new FlatGenDefReachNode(outputName);
+  }
+  public void rewriteUse(TempMap t) {
+  }
+  public void rewriteDst(TempMap t) {
+  }
+
+
+  public String toString() {
+    return "FlatGenDefReachNode_"+outputName;
+  }
+
+  public int kind() {
+    return FKind.FlatGenDefReachNode;
+  }
+
+  public TempDescriptor [] writesTemps() {
+    return new TempDescriptor[0];
+  }
+}

diff --git a/Robust/src/IR/Tree/BuildIR.java b/Robust/src/IR/Tree/BuildIR.java
index cc3845eb77eb820bb20015a6b352d174a10a724e..b95f781c2176967446fec93581e39114f7f17a1b 100644 (file)
--- a/Robust/src/IR/Tree/BuildIR.java
+++ b/Robust/src/IR/Tree/BuildIR.java
@@ -1578,10 +1578,15 @@ public class BuildIR {
       ParseNode idopt_pn=pn.getChild("identifier_opt");
       ParseNode name_pn=idopt_pn.getChild("name");
       // name_pn.getTerminal() gives you the label
+
     } else if (isNode(pn,"genreach")) {
       String graphName = pn.getChild("graphName").getTerminal();
       blockstatements.add(new GenReachNode(graphName) );
 
+    } else if (isNode(pn,"gen_def_reach")) {
+      String outputName = pn.getChild("outputName").getTerminal();
+      blockstatements.add(new GenDefReachNode(outputName) );
+
     } else if(isNode(pn,"labeledstatement")) {
       String labeledstatement = pn.getChild("name").getTerminal();
       BlockNode bn=parseSingleBlock(pn.getChild("statement").getFirstChild(),labeledstatement);

diff --git a/Robust/src/IR/Tree/GenDefReachNode.java b/Robust/src/IR/Tree/GenDefReachNode.java
new file mode 100644 (file)
index 0000000..aa180ef
--- /dev/null
+++ b/Robust/src/IR/Tree/GenDefReachNode.java
@@ -0,0 +1,22 @@
+package IR.Tree;
+
+public class GenDefReachNode extends BlockStatementNode {
+  String outputName;
+
+  public GenDefReachNode(String outputName) {
+    assert outputName != null;
+    this.outputName = outputName;
+  }
+
+  public String printNode(int indent) {
+    return "genDefReach "+outputName;
+  }
+
+  public String getOutputName() {
+    return outputName;
+  }
+
+  public int kind() {
+    return Kind.GenDefReachNode;
+  }
+}

diff --git a/Robust/src/IR/Tree/Kind.java b/Robust/src/IR/Tree/Kind.java
index 6887303ea68cd1e1803a9924eb1f3fa6f1304d3b..496d59a0ae72ebbe34b47cab6e54e48ea8e6e24f 100644 (file)
--- a/Robust/src/IR/Tree/Kind.java
+++ b/Robust/src/IR/Tree/Kind.java
@@ -34,4 +34,5 @@ public class Kind {
   public final static int SwitchLabelNode=31;
   public final static int SwitchBlockNode=32;
   public final static int ClassTypeNode=33;
+  public final static int GenDefReachNode=34;
 }

diff --git a/Robust/src/IR/Tree/SemanticCheck.java b/Robust/src/IR/Tree/SemanticCheck.java
index f6f5df32b19299db5a4d210efb03e76dcf18ee5d..f82fe80c457b9772525a79e56785d2af5038671e 100644 (file)
--- a/Robust/src/IR/Tree/SemanticCheck.java
+++ b/Robust/src/IR/Tree/SemanticCheck.java
@@ -389,6 +389,7 @@ public class SemanticCheck {
 
     case Kind.SESENode:
     case Kind.GenReachNode:
+    case Kind.GenDefReachNode:
       // do nothing, no semantic check for SESEs
       return;
     }

diff --git a/Robust/src/Lex/Keyword.java b/Robust/src/Lex/Keyword.java
index eea77f5e70954d3bd9932e022ee8b31e28bd4fa3..8edd81c8b9bf1ae983f9e502532a05a5139254d3 100644 (file)
--- a/Robust/src/Lex/Keyword.java
+++ b/Robust/src/Lex/Keyword.java
@@ -42,6 +42,7 @@ class Keyword extends Token {
     key_table.put("float", new Integer(Sym.FLOAT));
     key_table.put("for", new Integer(Sym.FOR));
     key_table.put("genreach", new Integer(Sym.GENREACH));
+    key_table.put("gendefreach", new Integer(Sym.GEN_DEF_REACH));
     key_table.put("goto", new Integer(Sym.GOTO));
     key_table.put("if", new Integer(Sym.IF));
     key_table.put("import", new Integer(Sym.IMPORT));

diff --git a/Robust/src/Lex/Lexer.java b/Robust/src/Lex/Lexer.java
index d6f18175fe625ba490ca0b141aa1a3fdad95c73a..c6113f9ac5ca4e5a3f07c585bed34bff96fb5c50 100644 (file)
--- a/Robust/src/Lex/Lexer.java
+++ b/Robust/src/Lex/Lexer.java
@@ -270,7 +270,7 @@ public class Lexer {
     "else", "enum",
     "extends", "external", "final", "finally",
     "flag", //keyword for failure aware computation
-    "float", "for", "genreach", "getoffset", "global", "goto", "if",
+    "float", "for", "gendefreach", "genreach", "getoffset", "global", "goto", "if",
     "implements",
     "import", "instanceof", "int",
     "interface",

diff --git a/Robust/src/Parse/java14.cup b/Robust/src/Parse/java14.cup
index 7e8f0d886e6d8ca1798d1aa56f5373a613747fd9..061fe2c9aa782d904fdd5e05e0e77567ac72ec05 100644 (file)
--- a/Robust/src/Parse/java14.cup
+++ b/Robust/src/Parse/java14.cup
@@ -108,6 +108,7 @@ terminal ENUM;
 
 // added for disjoint reachability analysis
 terminal GENREACH;
+terminal GEN_DEF_REACH;
 
 
 // 19.2) The Syntactic Grammar
@@ -204,6 +205,7 @@ non terminal ParseNode catches, catch_clause;
 non terminal ParseNode finally;
 //non terminal ParseNode assert_statement;
 non terminal ParseNode genreach_statement;
+non terminal ParseNode gen_def_reach_statement;
 // 19.12) Expressions
 non terminal ParseNode primary, primary_no_new_array;
 non terminal ParseNode class_instance_creation_expression;
@@ -1575,6 +1577,7 @@ statement_without_trailing_substatement ::=
        |       sese_statement:st {: RESULT=st; :}
        |       synchronized_statement:st {: RESULT=st; :}
        |       genreach_statement:st {: RESULT=st; :}
+       |       gen_def_reach_statement:st {: RESULT=st; :}
        |       throw_statement:st {: RESULT=st; :}
        |       try_statement:st {: RESULT=st; :}
 //     |       assert_statement
@@ -2541,3 +2544,10 @@ genreach_statement ::=
                pn.addChild("graphName").addChild(graphName);
                RESULT=pn; :}
        ;
+
+gen_def_reach_statement ::=
+               GEN_DEF_REACH IDENTIFIER:outputName SEMICOLON {: 
+               ParseNode pn=new ParseNode("gen_def_reach",parser.lexer.line_num);
+               pn.addChild("outputName").addChild(outputName);
+               RESULT=pn; :}
+       ;

diff --git a/Robust/src/Tests/disjoint/definite/test.java b/Robust/src/Tests/disjoint/definite/test.java
index 898d1d8725996b998b0498c5f193a5cacc14f0db..04defe83b18c8858933d131a9d9d8dce005b232e 100644 (file)
--- a/Robust/src/Tests/disjoint/definite/test.java
+++ b/Robust/src/Tests/disjoint/definite/test.java
@@ -18,6 +18,8 @@ public class Test {
 
     f = yodel( f, g );
 
+    gendefreach yo;
+
     System.out.println( f );
   }