From: bdemsky <bdemsky>
Date: Thu, 7 Sep 2006 23:40:05 +0000 (+0000)
Subject: checking in changes
X-Git-Tag: preEdgeChange~832
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=cacaf39ca7d94217f19f4944229a3a331bb96e02;p=IRC.git

checking in changes
---

diff --git a/Robust/src/IR/Flat/BuildCode.java b/Robust/src/IR/Flat/BuildCode.java
index 4b680901..6f906751 100644
--- a/Robust/src/IR/Flat/BuildCode.java
+++ b/Robust/src/IR/Flat/BuildCode.java
@@ -158,6 +158,9 @@ public class BuildCode {
 	outmethod.println("#include \"methodheaders.h\"");
 	outmethod.println("#include \"virtualtable.h\"");
 	outmethod.println("#include <runtime.h>");
+	if (state.CONSCHECK) {
+	    outmethod.println("#include \"checkers.h\"");
+	}
 	outclassdefs.println("extern int classsize[];");
 	outclassdefs.println("extern int * pointerarray[];");
 
@@ -920,14 +923,29 @@ public class BuildCode {
     }
 
     private void generateFlatCheckNode(FlatMethod fm,  FlatCheckNode fcn, PrintWriter output) {
-	output.print(fcn.getSpec()+"(");
-	TempDescriptor[] temps=fcn.getTemps();
-	for(int i=0;i<temps.length;i++) {
-	    if (i!=0)
-		output.print(", ");
-	    output.print(generateTemp(fm, temps[i]));
+
+	if (state.CONSCHECK) {
+	    String specname=fcn.getSpec();
+	    String varname="repairstate___";
+	    output.println("{");
+
+	    output.println("struct "+specname+"_state * "+varname+"=allocate"+specname+"_state();");
+
+
+	    TempDescriptor[] temps=fcn.getTemps();
+	    String[] vars=fcn.getVars();
+	    for(int i=0;i<temps.length;i++) {
+		output.println(varname+"->"+vars[i]+"=(int)"+generateTemp(fm, temps[i])+";");
+	    }
+
+	    output.println("if (doanalysis"+specname+"("+varname+")) {");
+	    output.println("free"+specname+"_state("+varname+");");
+	    output.println("} else {");
+	    output.println("free"+specname+"_state("+varname+");");
+	    output.println("}");
+
+	    output.println("}");
 	}
-	output.println(");");
     }
 
     private void generateFlatCall(FlatMethod fm, FlatCall fc, PrintWriter output) {
diff --git a/Robust/src/IR/Flat/BuildFlat.java b/Robust/src/IR/Flat/BuildFlat.java
index f9c3c8e2..17e988f2 100644
--- a/Robust/src/IR/Flat/BuildFlat.java
+++ b/Robust/src/IR/Flat/BuildFlat.java
@@ -748,17 +748,19 @@ public class BuildFlat {
 	for(int i=0;i<ccs.size();i++) {
 	    ConstraintCheck cc=(ConstraintCheck) ccs.get(i);
 	    /* Flatten the arguments */
-	    TempDescriptor[] temps=new TempDescriptor[cc.numArgs()];	    
+	    TempDescriptor[] temps=new TempDescriptor[cc.numArgs()];
+	    String[] vars=new String[cc.numArgs()];
 	    for(int j=0;j<cc.numArgs();j++) {
 		ExpressionNode en=cc.getArg(j);
 		TempDescriptor td=TempDescriptor.tempFactory("arg",en.getType());
 		temps[j]=td;
+		vars[j]=cc.getVar(j);
 		NodePair np=flattenExpressionNode(en, td);
 		last.addNext(np.getBegin());
 		last=np.getEnd();
 	    }
 	    
-	    FlatCheckNode fcn=new FlatCheckNode(cc.getSpec(), temps);
+	    FlatCheckNode fcn=new FlatCheckNode(cc.getSpec(), vars, temps);
 	    last.addNext(fcn);
 	    last=fcn;
 	}
diff --git a/Robust/src/IR/Flat/FlatCheckNode.java b/Robust/src/IR/Flat/FlatCheckNode.java
index ce2f09af..d890a920 100644
--- a/Robust/src/IR/Flat/FlatCheckNode.java
+++ b/Robust/src/IR/Flat/FlatCheckNode.java
@@ -2,10 +2,12 @@ package IR.Flat;
 
 public class FlatCheckNode extends FlatNode {
     TempDescriptor [] temps;
+    String [] vars;
     String spec;
 
-    public FlatCheckNode(String spec, TempDescriptor[] temps) {
+    public FlatCheckNode(String spec, String[] vars, TempDescriptor[] temps) {
 	this.spec=spec;
+	this.vars=vars;
 	this.temps=temps;
     }
 
@@ -17,6 +19,10 @@ public class FlatCheckNode extends FlatNode {
 	return spec;
     }
 
+    public String[] getVars() {
+	return vars;
+    }
+
     public TempDescriptor [] getTemps() {
 	return temps;
     }
diff --git a/Robust/src/IR/State.java b/Robust/src/IR/State.java
index 005423ab..a40ed70d 100644
--- a/Robust/src/IR/State.java
+++ b/Robust/src/IR/State.java
@@ -24,6 +24,7 @@ public class State {
     public boolean TASK;
     public String structfile;
     public String main;
+    public boolean CONSCHECK=false;
 
     public SymbolTable classes;
     public SymbolTable tasks;
diff --git a/Robust/src/IR/Tree/BuildIR.java b/Robust/src/IR/Tree/BuildIR.java
index e7bc15a7..e3f5a4e5 100644
--- a/Robust/src/IR/Tree/BuildIR.java
+++ b/Robust/src/IR/Tree/BuildIR.java
@@ -117,10 +117,11 @@ public class BuildIR {
     public ConstraintCheck parseConstraintCheck(ParseNode pn) {
 	if (isNode(pn,"cons_check")) {
 	    String specname=pn.getChild("name").getChild("identifier").getTerminal();
-	    Vector args=parseArgumentList(pn);
+	    Vector[] args=parseConsArgumentList(pn);
 	    ConstraintCheck cc=new ConstraintCheck(specname);
-	    for(int i=0;i<args.size();i++) {
-		cc.addArgument((ExpressionNode)args.get(i));
+	    for(int i=0;i<args[0].size();i++) {
+		cc.addVariable((String)args[0].get(i));
+		cc.addArgument((ExpressionNode)args[1].get(i));
 	    }
 	    return cc;
 	} else throw new Error();
@@ -412,6 +413,23 @@ public class BuildIR {
 	return arglist;
     }
 
+    private Vector[] parseConsArgumentList(ParseNode pn) {
+	Vector arglist=new Vector();
+	Vector varlist=new Vector();
+	ParseNode an=pn.getChild("cons_argument_list");
+	if (an==null)   /* No argument list */
+	    return new Vector[] {varlist, arglist};
+	ParseNodeVector anv=an.getChildren();
+	for(int i=0;i<anv.size();i++) {
+	    ParseNode cpn=anv.elementAt(i);
+	    ParseNode var=cpn.getChild("var");
+	    ParseNode exp=cpn.getChild("exp");
+	    varlist.add(var.getTerminal());
+	    arglist.add(parseExpression(exp));
+	}
+	return new Vector[] {varlist, arglist};
+    }
+
     private ExpressionNode parseAssignmentExpression(ParseNode pn) {
 	AssignOperation ao=new AssignOperation(pn.getChild("op").getTerminal());
 	ParseNodeVector pnv=pn.getChild("args").getChildren();
diff --git a/Robust/src/IR/Tree/ConstraintCheck.java b/Robust/src/IR/Tree/ConstraintCheck.java
index a2cfca3d..983c225c 100644
--- a/Robust/src/IR/Tree/ConstraintCheck.java
+++ b/Robust/src/IR/Tree/ConstraintCheck.java
@@ -6,10 +6,16 @@ import java.util.Vector;
 public class ConstraintCheck {
     String specname;
     Vector args;
+    Vector vars;
 
     public ConstraintCheck(String specname) {
 	this.specname=specname;
 	args=new Vector();
+	vars=new Vector();
+    }
+
+    public void addVariable(String var) {
+	vars.add(var);
     }
 
     public void addArgument(ExpressionNode en) {
@@ -28,11 +34,16 @@ public class ConstraintCheck {
 	return (ExpressionNode) args.get(i);
     }
 
+    public String getVar(int i) {
+	return (String) args.get(i);
+    }
+
     public String printNode(int indent) {
 	String str="assert("+specname+"(";
 	for(int i=0;i<numArgs();i++) {
 	    if (i>0)
 		str+=",";
+	    str+=getVar(i)+" : ";
 	    str+=getArg(i).printNode(0);
 	}
 	return str+")";
diff --git a/Robust/src/Main/Main.java b/Robust/src/Main/Main.java
index f11cd0e6..f5c2c6b8 100644
--- a/Robust/src/Main/Main.java
+++ b/Robust/src/Main/Main.java
@@ -29,6 +29,8 @@ public class Main {
 	      state.main=args[++i];
 	  else if (option.equals("-struct"))
 	      state.structfile=args[++i];
+	  else if (option.equals("-conscheck"))
+	      state.CONSCHECK=true;
 	  else if (option.equals("-task"))
 	      state.TASK=true;
 	  else if (option.equals("-help")) {
@@ -38,6 +40,7 @@ public class Main {
 	      System.out.println("-mainclass -- main function to call");
 	      System.out.println("-precise -- use precise garbage collection");
 
+	      System.out.println("-conscheck -- turn on consistency checking");
 	      System.out.println("-help -- print out help");
 	      System.exit(0);
 	  } else {
diff --git a/Robust/src/Parse/java14.cup b/Robust/src/Parse/java14.cup
index f86471fb..ad2e6a92 100644
--- a/Robust/src/Parse/java14.cup
+++ b/Robust/src/Parse/java14.cup
@@ -196,6 +196,7 @@ non terminal ParseNode return_statement;
 // 19.12) Expressions
 non terminal ParseNode primary, primary_no_new_array;
 non terminal ParseNode class_instance_creation_expression;
+non terminal ParseNode cons_argument_list_opt, cons_argument_list;
 non terminal ParseNode argument_list_opt, argument_list;
 //non terminal ParseNode array_creation_init;
 non terminal ParseNode array_creation_uninit;
@@ -337,7 +338,7 @@ cons_checks ::= cons_check:cc {:
 		RESULT=ccs;
 	:};
 
-cons_check ::=	IDENTIFIER:name LPAREN argument_list_opt:args RPAREN {: 
+cons_check ::=	IDENTIFIER:name LPAREN cons_argument_list_opt:args RPAREN {: 
 		ParseNode pn=new ParseNode("cons_check");
 		pn.addChild("name").addChild("identifier").addChild(name);
 		pn.addChild(args);
@@ -1217,10 +1218,33 @@ class_instance_creation_expression ::=
 //	|	name DOT NEW IDENTIFIER
 //			LPAREN argument_list_opt RPAREN class_body
 	;
+cons_argument_list_opt ::=
+	{: RESULT=new ParseNode("empty"); :}
+	|	argument_list:args {: RESULT=args; :}
+	;
+
+cons_argument_list ::=
+		IDENTIFIER:id COLON expression:exp {:
+		ParseNode pn=new ParseNode("cons_argument_list");
+		ParseNode pnarg=pn.addChild("binding");
+		pnarg.addChild("var").addChild(id);
+		pnarg.addChild("exp").addChild(exp);
+		RESULT=pn;
+	:}
+	|	argument_list:list COMMA IDENTIFIER:id COLON expression:exp {:
+		ParseNode pnarg=new ParseNode("binding");
+		pnarg.addChild("var").addChild(id);
+		pnarg.addChild("exp").addChild(exp);
+		list.addChild(pnarg);
+		RESULT=list;
+	:}
+	;
+
 argument_list_opt ::=
 	{: RESULT=new ParseNode("empty"); :}
 	|	argument_list:args {: RESULT=args; :}
 	;
+
 argument_list ::=
 		expression:exp {:
 		ParseNode pn=new ParseNode("argument_list");
diff --git a/Robust/src/Runtime/runtime.c b/Robust/src/Runtime/runtime.c
index a97cf4bb..818138de 100644
--- a/Robust/src/Runtime/runtime.c
+++ b/Robust/src/Runtime/runtime.c
@@ -18,6 +18,9 @@ jmp_buf error_handler;
 #include "Queue.h"
 #include "SimpleHash.h"
 #include "GenericHashtable.h"
+#ifdef CONSCHECK
+#include "initialize.h"
+#endif
 
 struct Queue * activetasks;
 struct parameterwrapper * objectqueues[NUMCLASSES];
@@ -25,6 +28,9 @@ struct genhashtable * failedtasks;
 
 int main(int argc, char **argv) {
   GC_init();
+#ifdef CONSCHECK
+  initializemmap();
+#endif
   {
   int i;
   /* Allocate startup object */
diff --git a/Robust/src/buildscriptrepair b/Robust/src/buildscriptrepair
index 0d365a9f..1caf13f2 100755
--- a/Robust/src/buildscriptrepair
+++ b/Robust/src/buildscriptrepair
@@ -18,8 +18,8 @@ shift
 
 mkdir $BUILDDIR
 java -cp $ROBUSTROOT/../cup/:$ROBUSTROOT Main.Main -classlibrary \
-$ROBUSTROOT/ClassLibrary/ -dir $BUILDDIR -struct $MAINFILE -struct \
-structfile -task $@
+$ROBUSTROOT/ClassLibrary/ -dir $BUILDDIR -struct $MAINFILE -conscheck \
+-struct structfile -task $@
 
 # Build all of the consistency specs
 
@@ -27,6 +27,7 @@ cd $SPECDIR
 mkdir $BUILDDIR/specdir
 cp $REPAIRROOT/MCC/CRuntime/* $BUILDDIR/specdir
 
+echo > $BUILDDIR/specs
 # compile specs into C code
 for i in *
 do
@@ -43,18 +44,20 @@ done
 
 cd $BUILDDIR/specdir
 ./buildrobust
+echo > $BUILDDIR/checkers.h
 for i in `cat $BUILDDIR/specs`
 do
 gcc -O0 -g -c $i\_aux.c
+echo \#include \"specdir\/$i\_aux.h\" >> $BUILDDIR/checkers.h
 done
 
 #build and link everything
 
-cd $CURDIR
-gcc -I$ROBUSTROOT/Runtime -I. -IRuntime/include -Itmpbuilddirectory \
--O0 -DBOEHM_GC -LRuntime/lib/ -lgc -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 $BUILDDIR/specdir/*.o \
--o $MAINFILE.bin
+cd $CURDIR gcc -I$ROBUSTROOT/Runtime -I. -I$BUILDDIR/specdir \
+-IRuntime/include -I$BUILDDIR -O0 -DBOEHM_GC -DCONSCHECK \
+-LRuntime/lib/ -lgc -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 $BUILDDIR/specdir/*.o -o \
+$MAINFILE.bin