return flag to indicate errors

[repair.git] / Repair / RepairCompiler / MCC / IR / RepairGenerator.java

diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
index cc07b7e342108a8df208fe2a6af6f7be26d9edb4..35925f35c0b2ba6309cc93fc7a1f837755552638 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
+++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java
@@ -10,7 +10,8 @@ public class RepairGenerator {
     PrintWrapper outputrepair = null;
     PrintWrapper outputaux = null;
     PrintWrapper outputhead = null;
-    String name="foo";
+    public static String name="foo";
+    public static String postfix="";
     String headername;
     static VarDescriptor oldmodel=null;
     static VarDescriptor newmodel=null;
@@ -57,7 +58,6 @@ public class RepairGenerator {
        }
     }
 
-
     private void name_updates() {
        int count=0;
        for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
@@ -67,7 +67,7 @@ public class RepairGenerator {
            if (togenerate.contains(gn))
            for (int i=0;i<mun.numUpdates();i++) {
                UpdateNode un=mun.getUpdate(i);
-               String name="update"+String.valueOf(count++);
+               String name="update"+RepairGenerator.name+String.valueOf(count++);
                updatenames.put(un,name);
            }
        }
@@ -107,6 +107,7 @@ public class RepairGenerator {
         generate_teardown();
        CodeWriter crhead = new StandardCodeWriter(this.outputhead);
        craux = new StandardCodeWriter(this.outputaux);
+       craux.outputline("return noerrors;");
        craux.emptyBuffer();
        craux.endblock();
 
@@ -275,7 +276,7 @@ public class RepairGenerator {
            cr.outputline(vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+"=("+vd.getType().getGenerateType().getSafeSymbol()+")"+vd.getSafeSymbol()+";");
        }
        /* Insert repair here */
-       cr.outputline("doanalysis("+vdstate.getSafeSymbol()+");");
+       cr.outputline("doanalysis"+postfix+"("+vdstate.getSafeSymbol()+");");
        globals=state.stGlobals.descriptors();
        while (globals.hasNext()) {
            VarDescriptor vd=(VarDescriptor) globals.next();
@@ -544,10 +545,12 @@ public class RepairGenerator {
            craux.outputline("int abstractcount;");
        }
 
-       crhead.outputline("void doanalysis(struct "+name+"_state *);");
-       craux.outputline("void doanalysis(struct "+name+"_state * thisvar)");
+       crhead.outputline("int doanalysis"+postfix+"(struct "+name+"_state *);");
+       craux.outputline("int doanalysis"+postfix+"(struct "+name+"_state * thisvar)");
+
        craux.startblock();
        craux.outputline("int highmark;"); /* This declaration is special...need it to be first */
+       craux.outputline("int noerrors=1;");
        craux.startBuffer();
 
        if (Compiler.TIME) {
@@ -568,7 +571,8 @@ public class RepairGenerator {
        craux.addDeclaration("struct RepairHash * ",repairtable.getSafeSymbol());
        craux.outputline(repairtable.getSafeSymbol()+"=0;");
        craux.outputline("initializestack(&highmark);");
-       craux.outputline("computesizes(thisvar);");
+       craux.outputline(name+"_statecomputesizes(thisvar, arsize, arnumelements);");
+       craux.outputline("computesizes();");
        craux.outputline(name+"_staterecomputesizes(thisvar);");
        craux.outputline("while (1)");
        craux.startblock();
@@ -639,6 +643,51 @@ public class RepairGenerator {
            cr.endblock();
        }
 
+        Iterator reliterator = state.stRelations.descriptors();
+       while (reliterator.hasNext()) {
+           RelationDescriptor rd = (RelationDescriptor) reliterator.next();
+
+
+           String relname = rd.getSafeSymbol();
+            if (rd.testUsage(RelationDescriptor.IMAGE)) {
+                cr.startblock();
+                cr.outputline("/* printing relation " + relname+"*/");
+                cr.outputline("printf(\"\\nPrinting relation " + rd.getSymbol() + " - %d elements \\n\", SimpleHashcountset("+relname+"_hash));");
+                cr.addDeclaration("struct SimpleIterator","__reliterator");
+                cr.outputline("SimpleHashiterator("+relname+"_hash,&__reliterator);");
+                cr.outputline("while (hasNext(&__reliterator))");
+                cr.startblock();
+                cr.addDeclaration("int","__relval");
+                cr.addDeclaration("int","__relval2");
+                cr.outputline("__relval2 = (int) key(&__reliterator);");
+                cr.outputline("__relval = (int) next(&__reliterator);");
+
+                cr.outputline("printf(\"<%ld,%ld> \", __relval2,__relval);");
+
+                cr.endblock();
+                cr.endblock();
+            } else if (rd.testUsage(RelationDescriptor.INVIMAGE)) {
+                cr.startblock();
+                cr.outputline("/* printing inv relation " + relname+"*/");
+                cr.outputline("printf(\"\\nPrinting relation using inv" + rd.getSymbol() + " - %d elements \\n\", SimpleHashcountset("+relname+"_hash));");
+                cr.addDeclaration("struct SimpleIterator","__reliterator");
+                cr.outputline("SimpleHashiterator("+relname+"_hashinv,&__reliterator);");
+                cr.outputline("while (hasNext(&__reliterator))");
+                cr.startblock();
+                cr.addDeclaration("int","__relval");
+                cr.addDeclaration("int","__relval2");
+                cr.outputline("__relval2 = (int) key(&__reliterator);");
+                cr.outputline("__relval = (int) next(&__reliterator);");
+
+
+                cr.outputline("printf(\"<%ld,%ld> \", __relval,__relval2);");
+
+                cr.endblock();
+                cr.endblock();
+            }
+
+       }
+
        cr.outputline("printf(\"\\n\\n------------------- END PRINTING\\n\");");
     }
 
@@ -885,11 +934,13 @@ public class RepairGenerator {
                 cr.outputline("if (maybe)");
                 cr.startblock();
                 cr.outputline("printf(\"maybe fail " +  escape(constraint.toString()) + ". \\n\");");
+               cr.outputline("noerrors=0;");
                //cr.outputline("exit(1);");
                 cr.endblock();
 
                 cr.outputline("else if (!" + constraintboolean.getSafeSymbol() + ")");
                 cr.startblock();
+               cr.outputline("noerrors=0;");
                 if (!Compiler.REPAIR||Compiler.GENERATEDEBUGHOOKS)
                    cr.outputline("printf(\"fail " + escape(constraint.toString()) + ". \\n\");");