These checking do the reconstruction of the model and invoke concrete repairs.
authorbdemsky <bdemsky>
Tue, 17 Feb 2004 18:53:08 +0000 (18:53 +0000)
committerbdemsky <bdemsky>
Tue, 17 Feb 2004 18:53:08 +0000 (18:53 +0000)
14 files changed:
Repair/RepairCompiler/MCC/Compiler.java
Repair/RepairCompiler/MCC/IR/Descriptor.java
Repair/RepairCompiler/MCC/IR/ForQuantifier.java
Repair/RepairCompiler/MCC/IR/ImplicitSchema.java
Repair/RepairCompiler/MCC/IR/Quantifier.java
Repair/RepairCompiler/MCC/IR/RelationDescriptor.java
Repair/RepairCompiler/MCC/IR/RelationInclusion.java
Repair/RepairCompiler/MCC/IR/RelationQuantifier.java
Repair/RepairCompiler/MCC/IR/Repair.java
Repair/RepairCompiler/MCC/IR/RepairGenerator.java
Repair/RepairCompiler/MCC/IR/SetDescriptor.java
Repair/RepairCompiler/MCC/IR/SetInclusion.java
Repair/RepairCompiler/MCC/IR/SetQuantifier.java
Repair/RepairCompiler/MCC/IR/Termination.java

index ebda670ebd356603137db75373233fba87bd4b85..1c0d7e1a3174b56e39aa45cfe19dce680b4443b5 100755 (executable)
@@ -55,11 +55,11 @@ public class Compiler {
            success = semantics(state) || error(state, "Semantic analysis failed, not attempting variable initialization.");
 
 
-
+           Termination termination=null;
            if (REPAIR) {
                /* Check partition constraints */
                (new ImplicitSchema(state)).update();
-               Termination t=new Termination(state);
+               termination=new Termination(state);
            }
             state.printall();
             (new DependencyBuilder(state)).calculate();
@@ -85,16 +85,23 @@ public class Compiler {
             
             try {
                 FileOutputStream gcode = new FileOutputStream(cli.infile + ".cc");
-                FileOutputStream gcode2 = new FileOutputStream(cli.infile + "_aux.cc");
-                FileOutputStream gcode3 = new FileOutputStream(cli.infile + "_aux.h");
+
 
                 // do model optimizations
                 //(new Optimizer(state)).optimize();
 
-                //NaiveGenerator ng = new NaiveGenerator(state);
-                //ng.generate(gcode);
-                RepairGenerator wg = new RepairGenerator(state);
-                wg.generate(gcode,gcode2,gcode3, cli.infile + "_aux.h");
+
+               if(REPAIR) {
+                   FileOutputStream gcode2 = new FileOutputStream(cli.infile + "_aux.cc");
+                   FileOutputStream gcode3 = new FileOutputStream(cli.infile + "_aux.h");
+                   RepairGenerator wg = new RepairGenerator(state,termination);
+                   wg.generate(gcode,gcode2,gcode3, cli.infile + "_aux.h");
+                   gcode2.close();
+                   gcode3.close();
+               } else {
+                   WorklistGenerator ng = new WorklistGenerator(state);
+                   ng.generate(gcode);
+               }
                 gcode.close();
             } catch (Exception e) {
                 e.printStackTrace();
index 99eb8d9c7e43636ee09377e5a764327025854eb0..3755a1c1e8950b4c6eb896b253732e4f385ad6da 100755 (executable)
@@ -10,15 +10,19 @@ public abstract class Descriptor {
 
     protected String name;
     protected String safename;
+    static int count=0;
+    int uniqueid;
     
     public Descriptor(String name) {
        this.name = name;
         this.safename = "__" + name + "__";
+       this.uniqueid=count++;
     }
 
     protected Descriptor(String name, String safename) {
        this.name = name;
         this.safename = safename;
+       this.uniqueid=count++;
     }
     
     public String toString() {
@@ -32,5 +36,7 @@ public abstract class Descriptor {
     public String getSafeSymbol() {
         return safename;
     }
-
+    public int getNum() {
+       return uniqueid;
+    }
 }
index 86cf50a893e438a28e6de533c95e4bcd977d272e..7cefd2c14a92216c0f7d78674dcd3abcaf0f62af 100755 (executable)
@@ -45,6 +45,11 @@ public class ForQuantifier extends Quantifier {
         writer.startblock();
     }
 
+    public void generate_open(CodeWriter writer, String type,int number, String
+left,String right) {
+       generate_open(writer);
+    }
+
     public int generate_worklistload(CodeWriter writer, int offset) {        
         String varname = var.getSafeSymbol();
         writer.outputline("int " + varname + " = wi->word" + offset + ";"); 
index 7e8aee5aca37d2697b51692012c827031155e76c..b00c06b31d335cfc1671c2789f83d74ee93a71b9 100755 (executable)
@@ -1,5 +1,7 @@
 package MCC.IR;
 import MCC.State;
+import MCC.Compiler;
+
 import java.util.*;
 
 public class ImplicitSchema {
@@ -11,7 +13,9 @@ public class ImplicitSchema {
     }
 
     public void update() {
-       updaterules();
+       if (Compiler.REPAIR) {
+           updaterules();
+       }
        updateconstraints();
        updaterelationconstraints();
     }
index 4b50b307f29090bda6c9a96c96fc7ef712fac03b..c03c521932b9e8fd467405cd776779cadc74d4e8 100755 (executable)
@@ -9,4 +9,5 @@ public abstract class Quantifier {
 
     public abstract int generate_worklistload(CodeWriter writer, int offset);
     public abstract int generate_workliststore(CodeWriter writer, int offset);
+    public abstract void generate_open(CodeWriter writer, String type,int number, String left,String right);
 }
index 22abc8bdba43be8de98518f8565c39047acaa8e6..e138ed28b28feff798595bfa610c5709d8f94b20 100755 (executable)
@@ -11,7 +11,7 @@ public class RelationDescriptor extends Descriptor {
     SetDescriptor domain;
     SetDescriptor range;
     boolean bStatic;
-
+    public static String prefix="";
     public static final Usage NONE = new Usage("NONE");
     public static final Usage IMAGE = new Usage("IMAGE");
     public static final Usage INVIMAGE = new Usage("INVIMAGE");
@@ -71,7 +71,7 @@ public class RelationDescriptor extends Descriptor {
             usage = BOTH;
         } else {
             usage = newusage;
-        }             
+        }
 
         //System.out.println(getSymbol() + " usage: " + oldusage + " + " + newusage + " => " + usage);
     }
@@ -80,13 +80,11 @@ public class RelationDescriptor extends Descriptor {
         return (usage == BOTH) || (testusage == usage);
     }
 
-}
-
-
-
-
-
-
-
-
+    public String getSafeSymbol() {
+       return prefix+safename;
+    }
 
+    public String getJustSafeSymbol() {
+       return safename;
+    }
+}
index 76d60acc09b356e293fa1b764f70efa802326a73..4e415bfbc8f57b86f45dd18bc463f4faf6b7b0fd 100755 (executable)
@@ -71,7 +71,7 @@ public class RelationInclusion extends Inclusion {
 
         if (!typesafe) {
             String check = "int " + typesafecheck + " = " ;
-            
+
             if (!(relation.getDomain() instanceof ReservedSetDescriptor)) {
                 check += relation.getDomain().getSafeSymbol() + "_hash->contains(" + ld.getSafeSymbol() + ") && ";
             }
@@ -79,7 +79,7 @@ public class RelationInclusion extends Inclusion {
             if (!(relation.getRange() instanceof ReservedSetDescriptor)) {
                 check += relation.getRange().getSafeSymbol() + "_hash->contains(" + rd.getSafeSymbol() + ") && ";
             }
-        
+
             check += "1;"; // terminate boolean expression
 
             writer.outputline(check);
@@ -88,35 +88,30 @@ public class RelationInclusion extends Inclusion {
         }
 
         String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
-        writer.outputline("int " + addeditem + ";");
-
-        if (relation.testUsage(RelationDescriptor.IMAGE)) {
-            writer.outputline(addeditem + " = " + relation.getSafeSymbol() + "_hash->add((int)" + ld.getSafeSymbol() + ", (int)" + rd.getSafeSymbol() + ");");
-        } 
-        
-        if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
-            writer.outputline(addeditem + " = " + relation.getSafeSymbol() + "_hashinv->add((int)" + rd.getSafeSymbol() + ", (int)" + ld.getSafeSymbol() + ");");
-        }
-        
+       if (!Compiler.REPAIR) {
+           writer.outputline("int " + addeditem + ";");
+           if (relation.testUsage(RelationDescriptor.IMAGE)) {
+               writer.outputline(addeditem + " = " + relation.getSafeSymbol() + "_hash->add((int)" + ld.getSafeSymbol() + ", (int)" + rd.getSafeSymbol() + ");");
+           }
+           
+           if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
+               writer.outputline(addeditem + " = " + relation.getSafeSymbol() + "_hashinv->add((int)" + rd.getSafeSymbol() + ", (int)" + ld.getSafeSymbol() + ");");
+           }
+       } else {
+           Repair.generate_dispatch(writer, relation, ld.getSafeSymbol(), rd.getSafeSymbol());
+       }
+       
         if (RelationInclusion.worklist) {
             writer.outputline("if (" + addeditem + ")");
-            writer.startblock(); {                
+            writer.startblock(); {
                 WorkList.generate_dispatch(writer, relation, rd.getSafeSymbol(), ld.getSafeSymbol());
             }
             writer.endblock();
         }
 
-        if (Compiler.REPAIR) {
-            writer.outputline("if (" + addeditem + ")");
-            writer.startblock(); {                
-                Repair.generate_dispatch(writer, relation, rd.getSafeSymbol(), ld.getSafeSymbol());
-            }
-            writer.endblock();
-        }
-
         if (!typesafe) {
             writer.endblock();
-        }            
+        }
 
         //writer.outputline("printf(\"" + relation.getSafeSymbol() + " (add): <%d, %d>\\n\", " + ld.getSafeSymbol() + ", " + rd.getSafeSymbol() + ");");
     }
index 193e02cec8b3845f90224bce8286540580d27c95..66b79f52141e0e1d3b578dbf012ae12eeeda7820 100755 (executable)
@@ -40,6 +40,30 @@ public class RelationQuantifier extends Quantifier {
         writer.outputline(x.getType().getGenerateType() + " " + x.getSafeSymbol() + " = (" + x.getType().getGenerateType() + ") " + x.getSafeSymbol() + "_iterator->key();");
     }
 
+    public void generate_open(CodeWriter writer, String type,int number, String left,String right) {
+       VarDescriptor tmp=VarDescriptor.makeNew("flag");
+        writer.outputline("SimpleIterator* " + x.getSafeSymbol() + "_iterator = " + relation.getSafeSymbol() + "_hash->iterator();");
+       writer.outputline("int "+tmp.getSafeSymbol()+"=0;");
+       writer.outputline("if ("+type+"=="+number+")");
+       writer.outputline(tmp.getSafeSymbol()+"=1;");
+       
+       writer.outputline("while("+tmp.getSafeSymbol()+"||(("+type+"!="+number+")&&"+x.getSafeSymbol() + "_iterator->hasNext()))");
+        writer.startblock();
+        writer.outputline(x.getType().getGenerateType() + " " + x.getSafeSymbol() + ";");
+        writer.outputline(y.getType().getGenerateType() + " " + y.getSafeSymbol() + ";");
+       writer.outputline("if ("+type+"=="+number+")");
+       writer.startblock();
+       writer.outputline(tmp.getSafeSymbol()+"=0;");
+        writer.outputline(x.getSafeSymbol() + " = (" + x.getType().getGenerateType() + ") " + left + ";");
+        writer.outputline(y.getSafeSymbol() + " = (" + y.getType().getGenerateType() + ") " + right + ";");
+       writer.endblock();
+       writer.outputline("else");
+       writer.startblock();
+        writer.outputline(y.getSafeSymbol() + " = (" + y.getType().getGenerateType() + ") " + x.getSafeSymbol() + "_iterator->next();");        
+        writer.outputline(x.getSafeSymbol() + " = (" + x.getType().getGenerateType() + ") " + x.getSafeSymbol() + "_iterator->key();");
+       writer.endblock();
+    }
+
     public int generate_worklistload(CodeWriter writer, int offset) {        
         String varx = x.getSafeSymbol();
         String vary = y.getSafeSymbol();
index e2fd969e1b284b55dd2943f9731a123ba241e47b..0191ff0f0b5988c2bbc8c349f39027da0fb93f43 100755 (executable)
@@ -4,83 +4,14 @@ import MCC.State;
 import java.util.*;
 
 public class Repair {
-
-
-    public static Vector getrulelist(Descriptor d) {
-
-        Vector dispatchrules = new Vector();
-        Vector rules = State.currentState.vRules;        
-        
-        for (int i = 0; i < rules.size(); i++) {
-            Rule rule = (Rule) rules.elementAt(i);
-            Set requiredsymbols = rule.getRequiredDescriptors();
-            
-            // #TBD#: in general this is wrong because these descriptors may contain descriptors
-            // bound in "in?" expressions which need to be dealt with in a topologically sorted
-            // fashion...
-
-            if (rule.getRequiredDescriptors().contains(d)) {
-                dispatchrules.addElement(rule);
-            }
-        }
-        return dispatchrules;
-    }
-    
+    public static RepairGenerator repairgenerator=null;
 
     public static void generate_dispatch(CodeWriter cr, RelationDescriptor rd, String leftvar, String rightvar) {
-
-        cr.outputline("// RELATION DISPATCH ");        
-
-        Vector dispatchrules = getrulelist(rd);
-        
-        if (dispatchrules.size() == 0) {
-            cr.outputline("// nothing to dispatch");
-            return;
-        }
-       
-        for(int i = 0; i < dispatchrules.size(); i++) {
-            Rule rule = (Rule) dispatchrules.elementAt(i);
-           if (rule.getGuardExpr().getRequiredDescriptors().contains(rd)) {
-               /* Guard depends on this relation, so we recomput everything */
-               cr.outputline("WORKLIST->add("+rule.getNum()+",-1,0,0);");
-           } else {
-               for (int j=0;j<rule.numQuantifiers();j++) {
-                   Quantifier q=rule.getQuantifier(j);
-                   if (q.getRequiredDescriptors().contains(rd)) {
-                       /* Generate add */
-                       cr.outputline("WORKLIST->add("+rule.getNum()+","+j+","+leftvar+","+rightvar+");");
-                   }
-               }
-           }
-        }
+       repairgenerator.generate_dispatch(cr,rd,leftvar,rightvar);
     }
 
 
     public static void generate_dispatch(CodeWriter cr, SetDescriptor sd, String setvar) {
-               
-        cr.outputline("// SET DISPATCH ");        
-        Vector dispatchrules = getrulelist(sd);
-
-        if (dispatchrules.size() == 0) {
-            cr.outputline("// nothing to dispatch");
-            return;
-        }
-
-        for(int i = 0; i < dispatchrules.size(); i++) {
-            Rule rule = (Rule) dispatchrules.elementAt(i);
-           if (SetDescriptor.expand(rule.getGuardExpr().getRequiredDescriptors()).contains(sd)) {
-               /* Guard depends on this relation, so we recomput everything */
-               cr.outputline("WORKLIST->add("+rule.getNum()+",-1,0,0);");
-           } else {
-               for (int j=0;j<rule.numQuantifiers();j++) {
-                   Quantifier q=rule.getQuantifier(j);
-                   if (SetDescriptor.expand(q.getRequiredDescriptors()).contains(sd)) {
-                       /* Generate add */
-                       cr.outputline("WORKLIST->add("+rule.getNum()+","+j+","+setvar+",0);");
-                   }
-               }
-           }
-       }
+       repairgenerator.generate_dispatch(cr,sd,setvar);
     }
 }
index b20ae6f769923616550d1372df55bfe4004e4d9c..f1d66c058cd6c8a1e58b1ba97f8d7edd975d195c 100755 (executable)
@@ -12,8 +12,38 @@ public class RepairGenerator {
     java.io.PrintWriter outputhead = null;
     String name="foo";
     String headername;
-    public RepairGenerator(State state) {
+    static VarDescriptor oldmodel=null;
+    static VarDescriptor newmodel=null;
+    static VarDescriptor worklist=null;
+    static VarDescriptor repairtable=null;
+    static VarDescriptor goodflag=null;
+    Rule currentrule=null;
+    Hashtable updatenames;
+    HashSet usedupdates;
+    Termination termination;
+    Set removed;
+
+    public RepairGenerator(State state, Termination t) {
         this.state = state;
+       updatenames=new Hashtable();
+       usedupdates=new HashSet();
+       termination=t;
+       removed=t.removedset;
+       Repair.repairgenerator=this;
+    }
+
+    private void name_updates() {
+       int count=0;
+       for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
+           GraphNode gn=(GraphNode) it.next();
+           TermNode tn=(TermNode) gn.getOwner();
+           MultUpdateNode mun=tn.getUpdate();
+           for (int i=0;i<mun.numUpdates();i++) {
+               UpdateNode un=mun.getUpdate(i);
+               String name="update"+String.valueOf(count++);
+               updatenames.put(un,name);
+           }
+       }
     }
 
     public void generate(OutputStream outputrepair, OutputStream outputaux,OutputStream outputhead, String st) {
@@ -21,41 +51,40 @@ public class RepairGenerator {
         this.outputaux = new java.io.PrintWriter(outputaux, true); 
         this.outputhead = new java.io.PrintWriter(outputhead, true); 
         headername=st;
+       name_updates();
 
         generate_tokentable();
         generate_hashtables();
        generate_stateobject();
        generate_call();
-       /*        generate_worklist();
-        generate_rules();
+       generate_worklist();
+        generate_rules();/*
         generate_checks();
         generate_teardown();*/
-
     }
 
+    
+
     private void generate_call() {
         CodeWriter cr = new StandardCodeWriter(outputrepair);        
        VarDescriptor vdstate=VarDescriptor.makeNew("repairstate");
        cr.outputline(name+"_state * "+vdstate.getSafeSymbol()+"=new "+name+"_state();");
-       
-
        Iterator globals=state.stGlobals.descriptors();
        while (globals.hasNext()) {
            VarDescriptor vd=(VarDescriptor) globals.next();
            cr.outputline(vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+"=("+vd.getType().getGenerateType().getSafeSymbol()+")"+vd.getSafeSymbol()+";");
        }
        /* Insert repair here */
-
+       cr.outputline(vdstate.getSafeSymbol()+"->doanalysis();");
        globals=state.stGlobals.descriptors();
        while (globals.hasNext()) {
            VarDescriptor vd=(VarDescriptor) globals.next();
            cr.outputline("*(("+vd.getType().getGenerateType().getSafeSymbol()+"*) &"+vd.getSafeSymbol()+")="+vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+";");
        }
-       
-       cr.outputline("delete ("+vdstate.getSafeSymbol()+");");
+       cr.outputline("delete "+vdstate.getSafeSymbol()+";");
     }
-    private void generate_tokentable() {
 
+    private void generate_tokentable() {
         CodeWriter cr = new StandardCodeWriter(outputrepair);        
         Iterator tokens = TokenLiteralExpr.tokens.keySet().iterator();        
 
@@ -104,7 +133,7 @@ public class RepairGenerator {
             SetDescriptor set = (SetDescriptor) sets.next();
            crhead.outputline("SimpleHash* " + set.getSafeSymbol() + "_hash;");
             craux.outputline(set.getSafeSymbol() + "_hash = new SimpleHash();");
-        } 
+        }
         
         /* second pass build relationships between hashtables */
         sets = state.stSets.descriptors();
@@ -148,7 +177,7 @@ public class RepairGenerator {
         /* first pass create all the hash tables */
         while (sets.hasNext()) {
             SetDescriptor set = (SetDescriptor) sets.next();
-            craux.outputline("delete("+set.getSafeSymbol() + "_hash);");
+            craux.outputline("delete "+set.getSafeSymbol() + "_hash;");
         } 
         
         /* destroy relations */
@@ -159,38 +188,50 @@ public class RepairGenerator {
             RelationDescriptor relation = (RelationDescriptor) relations.next();
             
             if (relation.testUsage(RelationDescriptor.IMAGE)) {
-                craux.outputline("delete("+relation.getSafeSymbol() + "_hash);");
+                craux.outputline("delete "+relation.getSafeSymbol() + "_hash;");
             }
 
             if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
-                craux.outputline("delete(" + relation.getSafeSymbol() + ");");
+                craux.outputline("delete " + relation.getSafeSymbol() + ";");
             } 
         }
         craux.outputline("}");
     }
 
     private void generate_worklist() {
-        CodeWriter cr = new StandardCodeWriter(outputrepair);
-        cr.outputline("WORKLIST = new WorkList();");
+        CodeWriter crhead = new StandardCodeWriter(outputhead);
+        CodeWriter craux = new StandardCodeWriter(outputaux);
+       oldmodel=VarDescriptor.makeNew("oldmodel");
+       newmodel=VarDescriptor.makeNew("newmodel");
+       worklist=VarDescriptor.makeNew("worklist");
+       goodflag=VarDescriptor.makeNew("goodflag");
+       repairtable=VarDescriptor.makeNew("repairtable");
+       crhead.outputline("void doanalysis();");
+       craux.outputline("void "+name +"_state::doanalysis() {");
+       craux.outputline(name+ " * "+oldmodel.getSafeSymbol()+"=0;");
+        craux.outputline("WorkList * "+worklist.getSafeSymbol()+" = new WorkList();");
+       craux.outputline("RepairHash * "+repairtable.getSafeSymbol()+"=0;");
+       craux.outputline("while (1) {");
+       craux.outputline("int "+goodflag.getSafeSymbol()+"=1;");
+       craux.outputline(name+ " * "+newmodel.getSafeSymbol()+"=new "+name+"();");
     }
     
     private void generate_teardown() {
-        CodeWriter cr = new StandardCodeWriter(outputrepair);        
-        cr.outputline("delete WORKLIST;");
+       CodeWriter cr = new StandardCodeWriter(outputaux);        
+       cr.outputline("delete "+worklist.getSafeSymbol()+";");
     }
 
     private void generate_rules() {
-        
-        /* first we must sort the rules */
+       /* first we must sort the rules */
         Iterator allrules = state.vRules.iterator();
-
         Vector emptyrules = new Vector(); // rules with no quantifiers
         Vector worklistrules = new Vector(); // the rest of the rules
+       RelationDescriptor.prefix = newmodel.getSafeSymbol()+"->";
+       SetDescriptor.prefix = newmodel.getSafeSymbol()+"->";
 
         while (allrules.hasNext()) {
             Rule rule = (Rule) allrules.next();
             ListIterator quantifiers = rule.quantifiers();
-
             boolean noquantifiers = true;
             while (quantifiers.hasNext()) {
                 Quantifier quantifier = (Quantifier) quantifiers.next();
@@ -202,7 +243,6 @@ public class RepairGenerator {
                     break;
                 }
             }
-
             if (noquantifiers) {
                 emptyrules.add(rule);
             } else {
@@ -212,24 +252,19 @@ public class RepairGenerator {
        
         Iterator iterator_er = emptyrules.iterator();
         while (iterator_er.hasNext()) {
-
-            Rule rule = (Rule) iterator_er.next();            
-
+            Rule rule = (Rule) iterator_er.next();
             {
                 final SymbolTable st = rule.getSymbolTable();                
-                CodeWriter cr = new StandardCodeWriter(outputrepair) {
+                CodeWriter cr = new StandardCodeWriter(outputaux) {
                         public SymbolTable getSymbolTable() { return st; }
                     };
-                
-                cr.outputline("// build " + rule.getLabel());
+               cr.outputline("// build " + rule.getLabel());
                 cr.startblock();
-
                 ListIterator quantifiers = rule.quantifiers();
-
                 while (quantifiers.hasNext()) {
-                    Quantifier quantifier = (Quantifier) quantifiers.next();                   
+                    Quantifier quantifier = (Quantifier) quantifiers.next();
                     quantifier.generate_open(cr);
-                }            
+                }
                         
                 /* pretty print! */
                 cr.output("//");
@@ -237,65 +272,66 @@ public class RepairGenerator {
                 cr.outputline("");
 
                 /* now we have to generate the guard test */
-        
-                VarDescriptor guardval = VarDescriptor.makeNew();
+               VarDescriptor guardval = VarDescriptor.makeNew();
                 rule.getGuardExpr().generate(cr, guardval);
-                
-                cr.outputline("if (" + guardval.getSafeSymbol() + ")");
+               cr.outputline("if (" + guardval.getSafeSymbol() + ")");
                 cr.startblock();
 
                 /* now we have to generate the inclusion code */
+               currentrule=rule;
                 rule.getInclusion().generate(cr);
                 cr.endblock();
-
                 while (quantifiers.hasPrevious()) {
                     Quantifier quantifier = (Quantifier) quantifiers.previous();
                     cr.endblock();
                 }
-
                 cr.endblock();
                 cr.outputline("");
                 cr.outputline("");
             }
         }
 
-        CodeWriter cr2 = new StandardCodeWriter(outputrepair);        
+        CodeWriter cr2 = new StandardCodeWriter(outputaux);        
 
-        cr2.outputline("WORKLIST->reset();");
-        cr2.outputline("while (WORKLIST->hasMoreElements())");
+        cr2.outputline("while ("+goodflag.getSafeSymbol()+"&&"+worklist.getSafeSymbol()+"->hasMoreElements())");
         cr2.startblock();
-        cr2.outputline("WORKITEM *wi = (WORKITEM *) WORKLIST->nextElement();");
+       VarDescriptor idvar=VarDescriptor.makeNew("id");
+        cr2.outputline("int "+idvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getid();");
         
         String elseladder = "if";
 
         Iterator iterator_rules = worklistrules.iterator();
         while (iterator_rules.hasNext()) {
-            
-            Rule rule = (Rule) iterator_rules.next();            
+
+            Rule rule = (Rule) iterator_rules.next();
             int dispatchid = rule.getNum();
 
             {
-                final SymbolTable st = rule.getSymbolTable();                
-                CodeWriter cr = new StandardCodeWriter(outputrepair) {
+                final SymbolTable st = rule.getSymbolTable();
+                CodeWriter cr = new StandardCodeWriter(outputaux) {
                         public SymbolTable getSymbolTable() { return st; }
                     };
 
                 cr.indent();
-                cr.outputline(elseladder + " (wi->id == " + dispatchid + ")");
+                cr.outputline(elseladder + " ("+idvar.getSafeSymbol()+" == " + dispatchid + ")");
                 cr.startblock();
-
+               VarDescriptor typevar=VarDescriptor.makeNew("type");
+               VarDescriptor leftvar=VarDescriptor.makeNew("left");
+               VarDescriptor rightvar=VarDescriptor.makeNew("right");
+               cr.outputline("int "+typevar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->gettype();");
+               cr.outputline("int "+leftvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getlvalue();");
+               cr.outputline("int "+rightvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getrvalue();");
                 cr.outputline("// build " + rule.getLabel());
 
-                ListIterator quantifiers = rule.quantifiers();
 
-                int count = 0;
-                while (quantifiers.hasNext()) {
-                    Quantifier quantifier = (Quantifier) quantifiers.next();
-                    count = quantifier.generate_worklistload(cr, count );                    
-                }
-                        
+               for (int j=0;j<rule.numQuantifiers();j++) {
+                   Quantifier quantifier = rule.getQuantifier(j);
+                   quantifier.generate_open(cr, typevar.getSafeSymbol(),j,leftvar.getSafeSymbol(),rightvar.getSafeSymbol());
+               }
+
                 /* pretty print! */
                 cr.output("//");
+
                 rule.getGuardExpr().prettyPrint(cr);
                 cr.outputline("");
 
@@ -308,11 +344,16 @@ public class RepairGenerator {
                 cr.startblock();
 
                 /* now we have to generate the inclusion code */
+               currentrule=rule;
                 rule.getInclusion().generate(cr);
                 cr.endblock();
 
+               for (int j=0;j<rule.numQuantifiers();j++) {
+                   cr.endblock();
+               }
+
                 // close startblocks generated by DotExpr memory checks
-                //DotExpr.generate_memory_endblocks(cr);                
+                //DotExpr.generate_memory_endblocks(cr);
 
                 cr.endblock(); // end else-if WORKLIST ladder
 
@@ -325,10 +366,8 @@ public class RepairGenerator {
         cr2.outputline("printf(\"VERY BAD !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\\n\\n\");");
         cr2.outputline("exit(1);");
         cr2.endblock();
-
         // end block created for worklist
         cr2.endblock();
-
     }
 
     private void generate_checks() {
@@ -344,7 +383,7 @@ public class RepairGenerator {
 
                 final SymbolTable st = constraint.getSymbolTable();
                 
-                CodeWriter cr = new StandardCodeWriter(outputrepair) {
+                CodeWriter cr = new StandardCodeWriter(outputaux) {
                         public SymbolTable getSymbolTable() { return st; }
                     };
                 
@@ -388,12 +427,289 @@ public class RepairGenerator {
                 cr.endblock();
                 cr.outputline("");
                 cr.outputline("");
-            }
+            }          
+        }
+        outputaux.println("// if (__Success) { printf(\"all tests passed\"); }");
+    }    
+
+
+
+    public static Vector getrulelist(Descriptor d) {
+        Vector dispatchrules = new Vector();
+        Vector rules = State.currentState.vRules;
+
+        for (int i = 0; i < rules.size(); i++) {
+            Rule rule = (Rule) rules.elementAt(i);
+            Set requiredsymbols = rule.getRequiredDescriptors();
             
+            // #TBD#: in general this is wrong because these descriptors may contain descriptors
+            // bound in "in?" expressions which need to be dealt with in a topologically sorted
+            // fashion...
+
+            if (rule.getRequiredDescriptors().contains(d)) {
+                dispatchrules.addElement(rule);
+            }
         }
+        return dispatchrules;
+    }
 
-        outputrepair.println("// if (__Success) { printf(\"all tests passed\"); }");
-    }    
+    private boolean need_compensation(Rule r) {
+       GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
+       for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
+           GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
+           GraphNode gn2=edge.getTarget();
+           if (!removed.contains(gn2)) {
+               TermNode tn2=(TermNode)gn2.getOwner();
+               if (tn2.getType()==TermNode.CONSEQUENCE)
+                   return false;
+           }
+       }
+       return true;
+    }
+
+    private UpdateNode find_compensation(Rule r) {
+       GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
+       for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
+           GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
+           GraphNode gn2=edge.getTarget();
+           if (!removed.contains(gn2)) {
+               TermNode tn2=(TermNode)gn2.getOwner();
+               if (tn2.getType()==TermNode.UPDATE) {
+                   MultUpdateNode mun=tn2.getUpdate();
+                   for(int i=0;i<mun.numUpdates();i++) {
+                       UpdateNode un=mun.getUpdate(i);
+                       if (un.getRule()==r)
+                           return un;
+                   }
+               }
+           }
+       }
+       throw new Error("No Compensation Update could be found");
+    }
+
+    public void generate_dispatch(CodeWriter cr, RelationDescriptor rd, String leftvar, String rightvar) {
+       boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
+       boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
+
+       if (!(usageinvimage||usageimage)) /* not used at all*/
+           return;
+
+        cr.outputline("// RELATION DISPATCH ");
+       cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
+       if (usageimage)
+           cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hash->contains("+leftvar+","+rightvar+"))");
+       else
+           cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hashinv->contains("+rightvar+","+leftvar+"))");
+       cr.startblock(); {
+           /* Adding new item */
+           /* Perform safety checks */
+           cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
+           cr.outputline(repairtable.getSafeSymbol()+"->containsrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+"))");
+           cr.startblock(); {
+               /* Have update to call into */
+               VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
+               String parttype="";
+               for(int i=0;i<currentrule.numQuantifiers();i++) {
+                   if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
+                       parttype=parttype+", int, int";
+                   else
+                       parttype=parttype+", int";
+               }
+               cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")=");
+               cr.outputline("(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+repairtable.getSafeSymbol()+"->getrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");");
+               String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
+               for(int i=0;i<currentrule.numQuantifiers();i++) {
+                   Quantifier q=currentrule.getQuantifier(i);
+                   if (q instanceof SetQuantifier) {
+                       SetQuantifier sq=(SetQuantifier) q;
+                       methodcall+=","+sq.getVar().getSafeSymbol();
+                   } else if (q instanceof RelationQuantifier) {
+                       RelationQuantifier rq=(RelationQuantifier) q;
+                       methodcall+=","+rq.x.getSafeSymbol();
+                       methodcall+=","+rq.y.getSafeSymbol();
+                   } else if (q instanceof ForQuantifier) {
+                       ForQuantifier fq=(ForQuantifier) q;
+                       methodcall+=","+fq.getVar().getSafeSymbol();
+                   }
+               }
+               methodcall+=");";
+               cr.outputline(methodcall);
+               cr.outputline(goodflag.getSafeSymbol()+"=0;");
+               cr.outputline("continue;");
+           }
+           cr.endblock();
+           /* Build standard compensation actions */
+           if (need_compensation(currentrule)) {
+               UpdateNode un=find_compensation(currentrule);
+               String name=(String)updatenames.get(un);
+               usedupdates.add(un); /* Mark as used */
+               String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
+               for(int i=0;i<currentrule.numQuantifiers();i++) {
+                   Quantifier q=currentrule.getQuantifier(i);
+                   if (q instanceof SetQuantifier) {
+                       SetQuantifier sq=(SetQuantifier) q;
+                       methodcall+=","+sq.getVar().getSafeSymbol();
+                   } else if (q instanceof RelationQuantifier) {
+                       RelationQuantifier rq=(RelationQuantifier) q;
+                       methodcall+=","+rq.x.getSafeSymbol();
+                       methodcall+=","+rq.y.getSafeSymbol();
+                   } else if (q instanceof ForQuantifier) {
+                       ForQuantifier fq=(ForQuantifier) q;
+                       methodcall+=","+fq.getVar().getSafeSymbol();
+                   }
+               }
+               methodcall+=");";
+               cr.outputline(methodcall);
+               cr.outputline(goodflag.getSafeSymbol()+"=0;");
+               cr.outputline("continue;");
+           }
+       }
+       cr.endblock();
+
+        String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
+       cr.outputline("int " + addeditem + ";");
+       if (rd.testUsage(RelationDescriptor.IMAGE)) {
+           cr.outputline(addeditem + " = " + rd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + rightvar + ");");
+       }
+       
+       if (rd.testUsage(RelationDescriptor.INVIMAGE)) {
+           cr.outputline(addeditem + " = " + rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar + ", (int)" + leftvar + ");");
+       }
+       
+       cr.outputline("if (" + addeditem + ")");
+       cr.startblock();
+
+        Vector dispatchrules = getrulelist(rd);
+        
+        if (dispatchrules.size() == 0) {
+            cr.outputline("// nothing to dispatch");
+           cr.endblock();
+            return;
+        }
+       
+        for(int i = 0; i < dispatchrules.size(); i++) {
+            Rule rule = (Rule) dispatchrules.elementAt(i);
+           if (rule.getGuardExpr().getRequiredDescriptors().contains(rd)) {
+               /* Guard depends on this relation, so we recomput everything */
+               cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
+           } else {
+               for (int j=0;j<rule.numQuantifiers();j++) {
+                   Quantifier q=rule.getQuantifier(j);
+                   if (q.getRequiredDescriptors().contains(rd)) {
+                       /* Generate add */
+                       cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+leftvar+","+rightvar+");");
+                   }
+               }
+           }
+        }
+       cr.endblock();
+    }
+
+
+    public void generate_dispatch(CodeWriter cr, SetDescriptor sd, String setvar) {
+               
+        cr.outputline("// SET DISPATCH ");
+
+       cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
+       cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+sd.getJustSafeSymbol()+"_hash->contains("+setvar+"))");
+       cr.startblock(); {
+           /* Adding new item */
+           /* Perform safety checks */
+           cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
+           cr.outputline(repairtable.getSafeSymbol()+"->containsset("+sd.getNum()+","+currentrule.getNum()+","+setvar+"))");
+           cr.startblock(); {
+               /* Have update to call into */
+               VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
+               String parttype="";
+               for(int i=0;i<currentrule.numQuantifiers();i++) {
+                   if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
+                       parttype=parttype+", int, int";
+                   else
+                       parttype=parttype+", int";
+               }
+               cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")=");
+               cr.outputline("(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+repairtable.getSafeSymbol()+"->getset("+sd.getNum()+","+currentrule.getNum()+","+setvar+");");
+               String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+
+                             repairtable.getSafeSymbol();
+               for(int i=0;i<currentrule.numQuantifiers();i++) {
+                   Quantifier q=currentrule.getQuantifier(i);
+                   if (q instanceof SetQuantifier) {
+                       SetQuantifier sq=(SetQuantifier) q;
+                       methodcall+=","+sq.getVar().getSafeSymbol();
+                   } else if (q instanceof RelationQuantifier) {
+                       RelationQuantifier rq=(RelationQuantifier) q;
+                       methodcall+=","+rq.x.getSafeSymbol();
+                       methodcall+=","+rq.y.getSafeSymbol();
+                   } else if (q instanceof ForQuantifier) {
+                       ForQuantifier fq=(ForQuantifier) q;
+                       methodcall+=","+fq.getVar().getSafeSymbol();
+                   }
+               }
+               methodcall+=");";
+               cr.outputline(methodcall);
+               cr.outputline(goodflag.getSafeSymbol()+"=0;");
+               cr.outputline("continue;");
+           }
+           cr.endblock();
+           /* Build standard compensation actions */
+           if (need_compensation(currentrule)) {
+               UpdateNode un=find_compensation(currentrule);
+               String name=(String)updatenames.get(un);
+               usedupdates.add(un); /* Mark as used */
+
+               String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+
+                             repairtable.getSafeSymbol();
+               for(int i=0;i<currentrule.numQuantifiers();i++) {
+                   Quantifier q=currentrule.getQuantifier(i);
+                   if (q instanceof SetQuantifier) {
+                       SetQuantifier sq=(SetQuantifier) q;
+                       methodcall+=","+sq.getVar().getSafeSymbol();
+                   } else if (q instanceof RelationQuantifier) {
+                       RelationQuantifier rq=(RelationQuantifier) q;
+                       methodcall+=","+rq.x.getSafeSymbol();
+                       methodcall+=","+rq.y.getSafeSymbol();
+                   } else if (q instanceof ForQuantifier) {
+                       ForQuantifier fq=(ForQuantifier) q;
+                       methodcall+=","+fq.getVar().getSafeSymbol();
+                   }
+               }
+               methodcall+=");";
+               cr.outputline(methodcall);
+               cr.outputline(goodflag.getSafeSymbol()+"=0;");
+               cr.outputline("continue;");
+           }
+       }
+       cr.endblock();
+
+        String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
+       cr.outputline("int " + addeditem + " = 1;");
+       cr.outputline(addeditem + " = " + sd.getSafeSymbol() + "_hash->add((int)" + setvar +  ", (int)" + setvar + ");");
+       cr.startblock();
+        Vector dispatchrules = getrulelist(sd);
+
+        if (dispatchrules.size() == 0) {
+            cr.outputline("// nothing to dispatch");
+           cr.endblock();
+            return;
+        }
+
+        for(int i = 0; i < dispatchrules.size(); i++) {
+            Rule rule = (Rule) dispatchrules.elementAt(i);
+           if (SetDescriptor.expand(rule.getGuardExpr().getRequiredDescriptors()).contains(sd)) {
+               /* Guard depends on this relation, so we recompute everything */
+               cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
+           } else {
+               for (int j=0;j<rule.numQuantifiers();j++) {
+                   Quantifier q=rule.getQuantifier(j);
+                   if (SetDescriptor.expand(q.getRequiredDescriptors()).contains(sd)) {
+                       /* Generate add */
+                       cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+setvar+",0);");
+                   }
+               }
+           }
+       }
+       cr.endblock();
+    }
 
 }
 
index 767167e6d92cc8059760e370ed7c77488f66400f..c461537da3b6fc5ef0d590720342938873ce6c9f 100755 (executable)
@@ -12,6 +12,7 @@ public class SetDescriptor extends Descriptor {
     TypeDescriptor type;
     boolean partition;
     Vector subsets;       
+    public static String prefix="";
 
     public SetDescriptor(String name) {
         super(name);
@@ -22,7 +23,7 @@ public class SetDescriptor extends Descriptor {
     public static Set expand(Set descriptors) {
         HashSet expanded = new HashSet();
         Iterator d = descriptors.iterator();
-        
+
         while (d.hasNext()) {
             Descriptor descriptor = (Descriptor) d.next();
             
@@ -91,4 +92,10 @@ public class SetDescriptor extends Descriptor {
         return v;
     }        
 
+    public String getSafeSymbol() {
+       return prefix+safename;
+    }
+    public String getJustSafeSymbol() {
+       return safename;
+    }
 }
index f80c63116045c619663688ad1dcf103f1a94e319..fb0f9ec32f7b994aa768666a66d1cde370d9f3db 100755 (executable)
@@ -61,11 +61,16 @@ public class SetInclusion extends Inclusion {
 
         // we set equal to one so that if dostore == false the guard in teh 
         // metainclusion generation for the subrules and sub quantifiers will go on        
-        writer.outputline("int " + addeditem + " = 1;");
+
 
         if (dostore) {
-           writer.outputline(addeditem + " = " + set.getSafeSymbol() + "_hash->add((int)" + vd.getSafeSymbol() 
-                              +  ", (int)" + vd.getSafeSymbol() + ");");
+           if (!Compiler.REPAIR) {
+               writer.outputline("int " + addeditem + " = 1;");
+               writer.outputline(addeditem + " = " + set.getSafeSymbol() + "_hash->add((int)" + vd.getSafeSymbol() 
+                                 +  ", (int)" + vd.getSafeSymbol() + ");");
+           } else {
+               Repair.generate_dispatch(writer, set, vd.getSafeSymbol());
+           }
            
             if (SetInclusion.worklist) {
                 writer.outputline("if (" + addeditem + ")");
@@ -74,16 +79,7 @@ public class SetInclusion extends Inclusion {
                 }
                 writer.endblock();
             }
-            if (Compiler.REPAIR) {
-                writer.outputline("if (" + addeditem + ")");
-                writer.startblock(); {                
-                    Repair.generate_dispatch(writer, set, vd.getSafeSymbol());
-                }
-                writer.endblock();
-            }
-           
-        }
-        
+       }
     }
 
     public boolean typecheck(SemanticAnalyzer sa) {
index c9ef3dfb306d8492d08a00585c43008a3da4e4a1..9d03c8a16bba0cdd603de5c50db8864cae6dbb01 100755 (executable)
@@ -43,6 +43,25 @@ public class SetQuantifier extends Quantifier {
         writer.outputline(var.getType().getGenerateType() + " " + var.getSafeSymbol() + " = (" + var.getType().getGenerateType() + ") " + var.getSafeSymbol() + "_iterator->next();");
     }
   
+    public void generate_open(CodeWriter writer, String type,int number, String left,String right) {
+       VarDescriptor tmp=VarDescriptor.makeNew("flag");
+        writer.outputline("SimpleIterator* " + var.getSafeSymbol() + "_iterator = " + set.getSafeSymbol() + "_hash->iterator();");
+       writer.outputline("int "+tmp.getSafeSymbol()+"=0;");
+       writer.outputline("if ("+type+"=="+number+")");
+       writer.outputline(tmp.getSafeSymbol()+"=1;");
+
+       writer.outputline("while("+tmp.getSafeSymbol()+"||(("+type+"!="+number+")&&"+var.getSafeSymbol() + "_iterator->hasNext()))");
+        writer.startblock();
+        writer.outputline(var.getType().getGenerateType() + " " + var.getSafeSymbol() + ";");
+       writer.outputline("if ("+type+"=="+number+")");
+       writer.startblock();
+       writer.outputline(tmp.getSafeSymbol()+"=0;");
+        writer.outputline(var.getSafeSymbol() + " = (" + var.getType().getGenerateType() + ") " + left + ";");
+       writer.endblock();
+       writer.outputline("else");
+        writer.outputline(var.getSafeSymbol() + " = (" + var.getType().getGenerateType() + ") " + var.getSafeSymbol() + "_iterator->next();");
+    }
+  
     public int generate_worklistload(CodeWriter writer, int offset) {        
         String varname = var.getSafeSymbol();
         writer.outputline("int " + varname + " = wi->word" + offset + ";"); 
index ff5985fcefb81b24caafe0c254552203dd7de80d..695699c178193b74784c564323b5fb1b1ef2cabe 100755 (executable)
@@ -18,6 +18,8 @@ public class Termination {
     Hashtable abstractadd;
     Hashtable abstractremove;
 
+    Set removedset;
+
     State state;
 
     public Termination(State state) {
@@ -66,9 +68,9 @@ public class Termination {
            System.out.println(mun.toString());
        }
        GraphAnalysis ga=new GraphAnalysis(this);
-       Set toremove=ga.doAnalysis();
+       removedset=ga.doAnalysis();
        System.out.println("Removing:");
-       for(Iterator it=toremove.iterator();it.hasNext();) {
+       for(Iterator it=removedset.iterator();it.hasNext();) {
            GraphNode gn=(GraphNode)it.next();
            System.out.println(gn.getTextLabel());
        }