checking in changes

diff --git a/Robust/src/IR/Flat/BuildCode.java b/Robust/src/IR/Flat/BuildCode.java
index 4b68090158510d86b9bcdab0b3b531fc41435496..6f906751da426e574d13c17154af0b2abcbe68b4 100644 (file)
--- 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 f9c3c8e20cae1d22a412d2ee1f6589a90f193265..17e988f281f1a8eb6c9d670f10b5f501876677b5 100644 (file)
--- 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 ce2f09af7bd6a42694ffe820158c240bab4f5ba9..d890a920dc1c8a9ff67936a316ccdf6d62e1d2f5 100644 (file)
--- 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 005423ab2af315a1db7c1f569e48388d4ab7e0be..a40ed70d3b675d649db6dff2b39baa82d6000fbd 100644 (file)
--- 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 e7bc15a75fa20e4ec29ddb1d34c84e0fc95a5954..e3f5a4e53a0f62ad13d8515239283fde151e88b3 100644 (file)
--- 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 a2cfca3d7ae289daa7bbbfcb61ce057b69d10910..983c225c9381f2d954fdf290596974ec411b828b 100644 (file)
--- 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 f11cd0e66c9f66280d40d4ba1b3f5aba4bc41107..f5c2c6b8e0a5fd135ac686a5ac6677373e875a3f 100644 (file)
--- 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 f86471fbdc2bf9dc6737a50da9b0f70f319d0ee0..ad2e6a92c197b52e059eaa882a41698b3a77a3c8 100644 (file)
--- 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 a97cf4bb7a6377cdca38e76d3bb56df6d1a8b01d..818138debe8501e7a47ff59eac8220bca5dfce5b 100644 (file)
--- 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 0d365a9f83cb3471c900f5a3e7024e7bab748bb7..1caf13f24c0393b4f9d5488814e5059d73a9529e 100755 (executable)
--- 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