From: yeom <yeom>
Date: Mon, 23 May 2011 19:40:03 +0000 (+0000)
Subject: having a new check that verifies the single reference constraint: only allows a singl... 
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=e829e3236610feee79d556f46bcba3ed757f2f7c;p=IRC.git

having a new check that verifies the single reference constraint: only allows a single reference, not aliases. The reference location must be destroyed after a variable or field is read. plus, changes on ssjava class library and test cases according to new checking.
---

diff --git a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
index 50d35f7c..f9790deb 100644
--- a/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
+++ b/Robust/src/Analysis/SSJava/SSJavaAnalysis.java
@@ -42,6 +42,7 @@ public class SSJavaAnalysis {
     parseLocationAnnotation();
     doFlowDownCheck();
     doLoopCheck();
+    doSingleReferenceCheck();
   }
 
   public void doFlowDownCheck() {
@@ -54,6 +55,11 @@ public class SSJavaAnalysis {
     checker.definitelyWrittenCheck();
   }
 
+  public void doSingleReferenceCheck() {
+    SingleReferenceCheck checker = new SingleReferenceCheck(state);
+    checker.singleReferenceCheck();
+  }
+
   private void parseLocationAnnotation() {
     Iterator it = state.getClassSymbolTable().getDescriptorsIterator();
     while (it.hasNext()) {
@@ -127,7 +133,7 @@ public class SSJavaAnalysis {
         locOrder.setGlobalLoc(globalLoc);
       } else if (orderElement.contains("*")) {
         // spin loc definition
-        locOrder.addSpinLoc(orderElement.substring(0,orderElement.length()-1));
+        locOrder.addSpinLoc(orderElement.substring(0, orderElement.length() - 1));
       } else {
         // single element
         locOrder.put(orderElement);
@@ -167,7 +173,7 @@ public class SSJavaAnalysis {
         }
       } else if (orderElement.contains("*")) {
         // spin loc definition
-        locOrder.addSpinLoc(orderElement.substring(0,orderElement.length()-1));
+        locOrder.addSpinLoc(orderElement.substring(0, orderElement.length() - 1));
       } else {
         // single element
         locOrder.put(orderElement);
diff --git a/Robust/src/Analysis/SSJava/SingleReferenceCheck.java b/Robust/src/Analysis/SSJava/SingleReferenceCheck.java
new file mode 100644
index 00000000..1bd0bf03
--- /dev/null
+++ b/Robust/src/Analysis/SSJava/SingleReferenceCheck.java
@@ -0,0 +1,152 @@
+package Analysis.SSJava;
+
+import java.util.Iterator;
+
+import IR.ClassDescriptor;
+import IR.MethodDescriptor;
+import IR.State;
+import IR.Tree.AssignmentNode;
+import IR.Tree.BlockExpressionNode;
+import IR.Tree.BlockNode;
+import IR.Tree.BlockStatementNode;
+import IR.Tree.CastNode;
+import IR.Tree.CreateObjectNode;
+import IR.Tree.DeclarationNode;
+import IR.Tree.ExpressionNode;
+import IR.Tree.Kind;
+import IR.Tree.LoopNode;
+import IR.Tree.SubBlockNode;
+
+public class SingleReferenceCheck {
+
+  static State state;
+  String needToNullify = null;
+
+  public SingleReferenceCheck(State state) {
+    this.state = state;
+  }
+
+  public void singleReferenceCheck() {
+    Iterator it = state.getClassSymbolTable().getDescriptorsIterator();
+    while (it.hasNext()) {
+      ClassDescriptor cd = (ClassDescriptor) it.next();
+      for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
+        MethodDescriptor md = (MethodDescriptor) method_it.next();
+        checkMethodBody(cd, md);
+      }
+    }
+  }
+
+  private void checkMethodBody(ClassDescriptor cd, MethodDescriptor fm) {
+    BlockNode bn = state.getMethodBody(fm);
+    for (int i = 0; i < bn.size(); i++) {
+      checkBlockStatementNode(cd, bn.get(i));
+    }
+
+  }
+
+  private boolean checkNullifying(BlockStatementNode bsn) {
+
+    if (bsn.kind() == Kind.BlockExpressionNode) {
+      ExpressionNode en = ((BlockExpressionNode) bsn).getExpression();
+      if (en.kind() == Kind.AssignmentNode) {
+        AssignmentNode an = (AssignmentNode) en;
+
+        if (an.getSrc().getType().isNull() && an.getDest().printNode(0).equals(needToNullify)) {
+          needToNullify = null;
+          return true;
+        }
+      }
+    }
+
+    return false;
+  }
+
+  private void checkBlockStatementNode(ClassDescriptor cd, BlockStatementNode bsn) {
+
+    if (needToNullify != null) {
+      if (!checkNullifying(bsn)) {
+        throw new Error(
+            "Reference field, which is read by a method, should be assigned to null before executing any following statement of the reference copy statement at "
+                + cd.getSourceFileName() + "::" + bsn.getNumLine());
+      }
+    }
+
+    switch (bsn.kind()) {
+    case Kind.BlockExpressionNode:
+      checkExpressionNode(((BlockExpressionNode) bsn).getExpression());
+      break;
+
+    case Kind.DeclarationNode:
+      checkDeclarationNode((DeclarationNode) bsn);
+      break;
+
+    case Kind.SubBlockNode:
+      checkSubBlockNode(cd, (SubBlockNode) bsn);
+      return;
+
+    case Kind.LoopNode:
+      checkLoopNode(cd, (LoopNode) bsn);
+      break;
+    }
+
+  }
+
+  private void checkLoopNode(ClassDescriptor cd, LoopNode ln) {
+    if (ln.getType() == LoopNode.FORLOOP) {
+      checkBlockNode(cd, ln.getInitializer());
+    }
+    checkBlockNode(cd, ln.getBody());
+  }
+
+  private void checkSubBlockNode(ClassDescriptor cd, SubBlockNode sbn) {
+    checkBlockNode(cd, sbn.getBlockNode());
+  }
+
+  private void checkBlockNode(ClassDescriptor cd, BlockNode bn) {
+    for (int i = 0; i < bn.size(); i++) {
+      checkBlockStatementNode(cd, bn.get(i));
+    }
+  }
+
+  private void checkExpressionNode(ExpressionNode en) {
+
+    switch (en.kind()) {
+    case Kind.AssignmentNode:
+      checkAssignmentNode((AssignmentNode) en);
+      break;
+    }
+
+  }
+
+  private void checkAssignmentNode(AssignmentNode an) {
+
+    if (an.getSrc() != null) {
+      if (an.getSrc().getType().isPtr() && (!an.getSrc().getType().isNull())
+          && !(an.getSrc() instanceof CreateObjectNode)) {
+        if (an.getSrc() instanceof CastNode) {
+          needToNullify = ((CastNode) an.getSrc()).getExpression().printNode(0);
+        } else {
+          needToNullify = an.getSrc().printNode(0);
+        }
+      }
+
+    }
+  }
+
+  private void checkDeclarationNode(DeclarationNode dn) {
+
+    if (dn.getExpression() != null) {
+      if (dn.getExpression().getType().isPtr() && !(dn.getExpression() instanceof CreateObjectNode)) {
+
+        if (dn.getExpression() instanceof CastNode) {
+          needToNullify = ((CastNode) dn.getExpression()).getExpression().printNode(0);
+        } else {
+          needToNullify = dn.getExpression().printNode(0);
+        }
+
+      }
+    }
+  }
+
+}
diff --git a/Robust/src/ClassLibrary/SSJava/String.java b/Robust/src/ClassLibrary/SSJava/String.java
index 6b85b662..4b061a82 100644
--- a/Robust/src/ClassLibrary/SSJava/String.java
+++ b/Robust/src/ClassLibrary/SSJava/String.java
@@ -21,6 +21,7 @@ public class String {
     for(@LOC("StringDM_C") int i=0; i<str.length; i++)
       charstr[i]=str[i];
     this.value=charstr;
+    charstr=null;
     this.count=str.length;
     this.offset=0;
   }
@@ -42,6 +43,7 @@ public class String {
     }
 
     newstr.value=charstr;
+    charstr=null;
     // LOC(newstr.value)=[O,STRING_V] 
     // LOC(charstr)=[V]
     // [O,STRING_V] < [V]
@@ -53,6 +55,7 @@ public class String {
     if (o.getType()!=getType()) // values are coming from [StringDM_I] and [THISLOC]
       return false;
     @LOC("StringDM_V") String s=(String)o;
+    o=null;
     if (s.count!=count)
       return false;
     for(@LOC("StringDM_C") int i=0; i<count; i++) {
diff --git a/Robust/src/Tests/ssJava/flowdown/test.java b/Robust/src/Tests/ssJava/flowdown/test.java
index 46dfb95d..71ed4f1a 100644
--- a/Robust/src/Tests/ssJava/flowdown/test.java
+++ b/Robust/src/Tests/ssJava/flowdown/test.java
@@ -107,6 +107,16 @@ public class test{
 	localBar.b1++; // value can be moving among the same location
     }
 
+    public void uniqueReference(){
+	
+	@LOC("methodH") Foo f_1=new Foo();
+	f_1.bar=new Bar();
+	@LOC("methodL") Bar newBar_2;
+	newBar_2=f_1.bar;
+	f_1.bar=null; // should assign null here 
+	
+    }
+
 }