From 1547524f4827779d53b2c7bc5754256f5f4a794a Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky>
Date: Wed, 30 Aug 2006 22:07:28 +0000
Subject: [PATCH] adding support for consistency checking

---
 Robust/src/IR/Flat/BuildCode.java       | 63 ++++++++++++++++++++++++-
 Robust/src/IR/State.java                |  4 +-
 Robust/src/IR/Tree/BuildIR.java         | 26 +++++++++-
 Robust/src/IR/Tree/ConstraintCheck.java | 25 ++++++++++
 Robust/src/IR/Tree/FlagEffect.java      |  4 --
 Robust/src/IR/Tree/TaskExitNode.java    |  8 +++-
 Robust/src/IR/TypeDescriptor.java       | 31 +++++++++++-
 Robust/src/Main/Main.java               |  3 ++
 Robust/src/Parse/java14.cup             | 29 +++++++++++-
 Robust/src/buildscripttask              |  2 +-
 10 files changed, 182 insertions(+), 13 deletions(-)
 create mode 100644 Robust/src/IR/Tree/ConstraintCheck.java

diff --git a/Robust/src/IR/Flat/BuildCode.java b/Robust/src/IR/Flat/BuildCode.java
index 94f6e620..1dea8b46 100644
--- a/Robust/src/IR/Flat/BuildCode.java
+++ b/Robust/src/IR/Flat/BuildCode.java
@@ -44,6 +44,7 @@ public class BuildCode {
 	/* Create output streams to write to */
 	PrintWriter outclassdefs=null;
 	PrintWriter outstructs=null;
+	PrintWriter outrepairstructs=null;
 	PrintWriter outmethodheader=null;
 	PrintWriter outmethod=null;
 	PrintWriter outvirtual=null;
@@ -67,13 +68,16 @@ public class BuildCode {
 		str=new FileOutputStream(PREFIX+"taskdefs.c");
 		outtaskdefs=new java.io.PrintWriter(str, true);
 	    }
+	    if (state.structfile!=null) {
+		str=new FileOutputStream(PREFIX+state.structfile+".struct");
+		outrepairstructs=new java.io.PrintWriter(str, true);
+	    }
 	} catch (Exception e) {
 	    e.printStackTrace();
 	    System.exit(-1);
 	}
 
 	/* Build the virtual dispatch tables */
-
 	buildVirtualTables(outvirtual);
 
 	/* Output includes */
@@ -221,12 +225,69 @@ public class BuildCode {
 	}
 	if (state.TASK)
 	    outstructs.println("#define MAXTASKPARAMS "+maxtaskparams);
+
+
+	/* Output structure definitions for repair tool */
+	if (state.structfile!=null) {
+	    buildRepairStructs(outrepairstructs);
+	    outrepairstructs.close();
+	}
+
 	outstructs.close();
 	outmethod.close();
     }
 
     private int maxcount=0;
 
+    private void buildRepairStructs(PrintWriter outrepairstructs) {
+	Iterator classit=state.getClassSymbolTable().getDescriptorsIterator();
+	while(classit.hasNext()) {
+	    ClassDescriptor cn=(ClassDescriptor)classit.next();
+	    outrepairstructs.println("structure "+cn.getSymbol()+" {");
+	    outrepairstructs.println("  int __type__;");
+	    if (cn.hasFlags()) {
+		outrepairstructs.println("  int __flag__;");
+		outrepairstructs.println("  int __flagptr__;");
+	    }
+	    printRepairStruct(cn, outrepairstructs);
+	    outrepairstructs.println("}\n");
+	}
+	
+	for(int i=0;i<state.numArrays();i++) {
+	    TypeDescriptor tdarray=arraytable[i];
+	    TypeDescriptor tdelement=tdarray.dereference();
+	    outrepairstructs.println("structure "+arraytype+"_"+state.getArrayNumber(tdarray)+" {");
+	    outrepairstructs.println("  int __type__;");
+	    printRepairStruct(typeutil.getClass(TypeUtil.ObjectClass), outrepairstructs);
+	    outrepairstructs.println("  int length;");
+	    if (tdelement.isClass()||tdelement.isArray())
+		outrepairstructs.println("  "+tdelement.getRepairSymbol()+" * elem[this.length];");
+	    else
+		outrepairstructs.println("  "+tdelement.getRepairSymbol()+" elem[this.length];");
+
+	    outrepairstructs.println("}\n");
+	}
+
+    }
+
+    private void printRepairStruct(ClassDescriptor cn, PrintWriter output) {
+	ClassDescriptor sp=cn.getSuperDesc();
+	if (sp!=null)
+	    printRepairStruct(sp, output);
+	
+	Vector fields=(Vector)fieldorder.get(cn);
+
+	for(int i=0;i<fields.size();i++) {
+	    FieldDescriptor fd=(FieldDescriptor)fields.get(i);
+	    if (fd.getType().isArray()) {
+		output.println("  "+arraytype+"_"+ state.getArrayNumber(fd.getType()) +" * "+fd.getSymbol()+";");
+	    } else if (fd.getType().isClass())
+		output.println("  "+fd.getType().getRepairSymbol()+" * "+fd.getSymbol()+";");
+	    else 
+		output.println("  "+fd.getType().getRepairSymbol()+" "+fd.getSymbol()+";");
+	}
+    }
+
     /** This method outputs TaskDescriptor information */
     void generateTaskDescriptor(PrintWriter output, TaskDescriptor task) {
 	for (int i=0;i<task.numParameters();i++) {
diff --git a/Robust/src/IR/State.java b/Robust/src/IR/State.java
index 7f6e485c..005423ab 100644
--- a/Robust/src/IR/State.java
+++ b/Robust/src/IR/State.java
@@ -5,8 +5,6 @@ import IR.*;
 import java.util.*;
 
 public class State {
-    public String main;
-
     public State() {
 	this.classes=new SymbolTable();
 	this.tasks=new SymbolTable();
@@ -24,6 +22,8 @@ public class State {
     /** Boolean flag which indicates whether compiler is compiling a task-based
      * program. */
     public boolean TASK;
+    public String structfile;
+    public String main;
 
     public SymbolTable classes;
     public SymbolTable tasks;
diff --git a/Robust/src/IR/Tree/BuildIR.java b/Robust/src/IR/Tree/BuildIR.java
index 12ae4bdb..f59206f2 100644
--- a/Robust/src/IR/Tree/BuildIR.java
+++ b/Robust/src/IR/Tree/BuildIR.java
@@ -103,6 +103,26 @@ public class BuildIR {
 	} else throw new Error();
     }
 
+    public Vector parseChecks(ParseNode pn) {
+	Vector ccs=new Vector();
+	ParseNodeVector pnv=pn.getChildren();
+	for(int i=0;i<pnv.size();i++) {
+	    ParseNode fn=pnv.elementAt(i);
+	    ConstraintCheck cc=parseConstraintCheck(fn);
+	    ccs.add(cc);
+	}
+	return ccs;
+    }
+
+    public ConstraintCheck parseConstraintCheck(ParseNode pn) {
+	if (isNode(pn,"cons_check")) {
+	    String varname=pn.getChild("name").getTerminal();
+	    String specname=pn.getChild("spec").getTerminal();
+	    ConstraintCheck cc=new ConstraintCheck(varname, specname);
+	    return cc;
+	} else throw new Error();
+    }
+
     public void parseParameterList(TaskDescriptor td, ParseNode pn) {
 	ParseNode paramlist=pn.getChild("task_parameter_list");
 	if (paramlist==null)
@@ -490,7 +510,11 @@ public class BuildIR {
 	    Vector vfe=null;
 	    if (pn.getChild("flag_effects_list")!=null)
 		vfe=parseFlags(pn.getChild("flag_effects_list"));
-	    blockstatements.add(new TaskExitNode(vfe));
+	    Vector ccs=null;
+	    if (pn.getChild("cons_checks")!=null)
+		ccs=parseChecks(pn.getChild("cons_checks"));
+	    
+	    blockstatements.add(new TaskExitNode(vfe, ccs));
 	} else if (isNode(pn,"return")) {
 	    if (isEmpty(pn.getTerminal()))
 		blockstatements.add(new ReturnNode());
diff --git a/Robust/src/IR/Tree/ConstraintCheck.java b/Robust/src/IR/Tree/ConstraintCheck.java
new file mode 100644
index 00000000..6af53608
--- /dev/null
+++ b/Robust/src/IR/Tree/ConstraintCheck.java
@@ -0,0 +1,25 @@
+package IR.Tree;
+
+import IR.*;
+
+public class ConstraintCheck {
+    String varname;
+    String specname;
+
+    public ConstraintCheck(String varname, String specname) {
+	this.varname=varname;
+	this.specname=specname;
+    }
+
+    public String getVarName() {
+	return varname;
+    }
+
+    public String getSpec() {
+	return specname;
+    }
+
+    public String printNode(int indent) {
+	return "assert "+varname+" "+specname;
+    }
+}
diff --git a/Robust/src/IR/Tree/FlagEffect.java b/Robust/src/IR/Tree/FlagEffect.java
index 8bc1c43e..506852c9 100644
--- a/Robust/src/IR/Tree/FlagEffect.java
+++ b/Robust/src/IR/Tree/FlagEffect.java
@@ -24,10 +24,6 @@ public class FlagEffect {
 	return name;
     }
 
-    public int kind() {
-	return Kind.FlagNode;
-    }
-
     public boolean getStatus() {
 	return status;
     }
diff --git a/Robust/src/IR/Tree/TaskExitNode.java b/Robust/src/IR/Tree/TaskExitNode.java
index 30f2640e..c26e0fc2 100644
--- a/Robust/src/IR/Tree/TaskExitNode.java
+++ b/Robust/src/IR/Tree/TaskExitNode.java
@@ -3,8 +3,10 @@ import java.util.Vector;
 
 public class TaskExitNode extends BlockStatementNode {
     Vector vfe;
-    public TaskExitNode(Vector vfe) {
+    Vector ccs;
+    public TaskExitNode(Vector vfe, Vector ccs) {
 	this.vfe=vfe;
+	this.ccs=ccs;
     }
 
     public String printNode(int indent) {
@@ -15,6 +17,10 @@ public class TaskExitNode extends BlockStatementNode {
 	return vfe;
     }
 
+    public Vector getChecks() {
+	return ccs;
+    }
+
     public int kind() {
 	return Kind.TaskExitNode;
     }
diff --git a/Robust/src/IR/TypeDescriptor.java b/Robust/src/IR/TypeDescriptor.java
index 9f564211..996225b6 100644
--- a/Robust/src/IR/TypeDescriptor.java
+++ b/Robust/src/IR/TypeDescriptor.java
@@ -98,8 +98,37 @@ public class TypeDescriptor extends Descriptor {
 	else throw new Error("Error Type: "+type);
     }
 
+    public String getRepairSymbol() {
+	if (isArray())
+	    return IR.Flat.BuildCode.arraytype;
+	else if (isClass())
+	    return class_desc.getSymbol();
+	else if (isByte())
+	    return "char";
+	else if (isChar())
+	    return "short";
+	else if (isShort())
+	    return "short";
+	else if (isInt())
+	    return "int";
+	else if (isBoolean()) //Booleans are ints in C
+	    return "int";
+	else if (isLong())
+	    return "long long";
+	else if (isVoid())
+	    return "void";
+	else if (isDouble())
+	    return "double";
+	else if (isFloat())
+	    return "float";
+	else throw new Error("Error Type: "+type);
+    }
+
     public String getSafeDescriptor() {
-	if (isClass())
+	//Can't safely use [ in C
+	if (isArray()) 
+	    return "_AR_"+this.dereference().getSafeDescriptor();
+	else if (isClass())
 	    return class_desc.getSafeDescriptor();
 	else if (isByte())
 	    return "C";
diff --git a/Robust/src/Main/Main.java b/Robust/src/Main/Main.java
index cf2f054f..f11cd0e6 100644
--- a/Robust/src/Main/Main.java
+++ b/Robust/src/Main/Main.java
@@ -27,11 +27,14 @@ public class Main {
 	      ClassLibraryPrefix=args[++i]+"/";
 	  else if (option.equals("-mainclass"))
 	      state.main=args[++i];
+	  else if (option.equals("-struct"))
+	      state.structfile=args[++i];
 	  else if (option.equals("-task"))
 	      state.TASK=true;
 	  else if (option.equals("-help")) {
 	      System.out.println("-classlibrary classlibrarydirectory -- directory where classlibrary is located");
 	      System.out.println("-dir outputdirectory -- output code in outputdirectory");
+	      System.out.println("-struct structfile -- output structure declarations for repair tool");
 	      System.out.println("-mainclass -- main function to call");
 	      System.out.println("-precise -- use precise garbage collection");
 
diff --git a/Robust/src/Parse/java14.cup b/Robust/src/Parse/java14.cup
index ec0ad3ed..f3e65f5f 100644
--- a/Robust/src/Parse/java14.cup
+++ b/Robust/src/Parse/java14.cup
@@ -238,6 +238,10 @@ non terminal ParseNode flag_list;
 non terminal ParseNode flag_list_opt;
 non terminal ParseNode flag_change;
 
+non terminal ParseNode cons_checks_opt;
+non terminal ParseNode cons_checks;
+non terminal ParseNode cons_check;
+
 start with goal;
 
 
@@ -315,8 +319,29 @@ flag_notexpression ::=
 	:}
 	;
 
-task_exitstatement ::= TASKEXIT flag_effects_opt:opt SEMICOLON{: 
-		RESULT=(new ParseNode("taskexit")).addChild(opt).getRoot();
+task_exitstatement ::= TASKEXIT flag_effects_opt:opt cons_checks_opt:cco SEMICOLON {: 
+		RESULT=(new ParseNode("taskexit")).addChild(opt).getRoot().addChild(cco).getRoot();
+	:};
+
+cons_checks_opt ::= ASSERT LPAREN cons_checks:cc RPAREN {: RESULT=cc; :}
+	| {: RESULT = new ParseNode("empty"); :}
+	;
+
+cons_checks ::= cons_check:cc {: 
+		ParseNode pn=new ParseNode("cons_checks");
+		pn.addChild(cc);
+		RESULT=pn;
+	:}
+	|	cons_checks:ccs COMMA cons_check:cc {: 
+		ccs.addChild(cc);
+		RESULT=ccs;
+	:};
+
+cons_check ::=	IDENTIFIER:id LBRACE IDENTIFIER:spec RBRACE {: 
+		ParseNode pn=new ParseNode("cons_check");
+		pn.addChild("name").addChild(id);
+		pn.addChild("spec").addChild(spec);
+		RESULT=pn;
 	:};
 
 flag_effects_opt ::= LPAREN flag_effects:fe RPAREN {:RESULT=fe;:}
diff --git a/Robust/src/buildscripttask b/Robust/src/buildscripttask
index d7f8f009..87843d72 100755
--- a/Robust/src/buildscripttask
+++ b/Robust/src/buildscripttask
@@ -3,5 +3,5 @@ ROBUSTROOT=~/research/Robust/src
 MAINFILE=$1
 shift
 mkdir tmpbuilddirectory
-java -cp $ROBUSTROOT/../cup/:$ROBUSTROOT Main.Main -classlibrary $ROBUSTROOT/ClassLibrary/ -dir tmpbuilddirectory -task $@
+java -cp $ROBUSTROOT/../cup/:$ROBUSTROOT Main.Main -classlibrary $ROBUSTROOT/ClassLibrary/ -dir tmpbuilddirectory -struct $MAINFILE -task $@
 gcc -I$ROBUSTROOT/Runtime -Itmpbuilddirectory -O0 -DTASK -g tmpbuilddirectory/methods.c tmpbuilddirectory/taskdefs.c $ROBUSTROOT/Runtime/runtime.c $ROBUSTROOT/Runtime/Queue.c $ROBUSTROOT/Runtime/SimpleHash.c $ROBUSTROOT/Runtime/checkpoint.c $ROBUSTROOT/Runtime/GenericHashtable.c -o $MAINFILE.bin
\ No newline at end of file
-- 
2.34.1