Repair/RepairCompiler/MCC/IR/RepairGenerator.java

   1 package MCC.IR;
   2
   3 import java.io.*;
   4 import java.util.*;
   5 import MCC.State;
   6 import MCC.Compiler;
   7
   8 public class RepairGenerator {
   9     State state;
  10     java.io.PrintWriter outputrepair = null;
  11     java.io.PrintWriter outputaux = null;
  12     java.io.PrintWriter outputhead = null;
  13     String name="foo";
  14     String headername;
  15     static VarDescriptor oldmodel=null;
  16     static VarDescriptor newmodel=null;
  17     static VarDescriptor worklist=null;
  18     static VarDescriptor repairtable=null;
  19     static VarDescriptor goodflag=null;
  20     Rule currentrule=null;
  21     Hashtable updatenames;
  22     HashSet usedupdates;
  23     Termination termination;
  24     Set removed;
  25     HashSet togenerate;
  26     static boolean DEBUG=false;
  27     Cost cost;
  28     Sources sources;
  29     ModelRuleDependence mrd;
  30
  31     public RepairGenerator(State state, Termination t) {
  32         this.state = state;
  33         updatenames=new Hashtable();
  34         usedupdates=new HashSet();
  35         termination=t;
  36         removed=t.removedset;
  37         togenerate=new HashSet();
  38         togenerate.addAll(termination.conjunctions);
  39         if (Compiler.REPAIR)
  40             togenerate.removeAll(removed);
  41         GraphNode.computeclosure(togenerate,removed);
  42         cost=new Cost();
  43         sources=new Sources(state);
  44         mrd=ModelRuleDependence.doAnalysis(state);
  45         Repair.repairgenerator=this;
  46     }
  47
  48     private void generatetypechecks(boolean flag) {
  49         if (flag) {
  50             DotExpr.DOTYPECHECKS=true;
  51             VarExpr.DOTYPECHECKS=true;
  52             DotExpr.DONULL=true;
  53             VarExpr.DONULL=true;
  54         } else {
  55             VarExpr.DOTYPECHECKS=false;
  56             DotExpr.DOTYPECHECKS=false;
  57             VarExpr.DONULL=true;
  58             DotExpr.DONULL=true;
  59         }
  60     }
  61
  62
  63     private void name_updates() {
  64         int count=0;
  65         for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
  66             GraphNode gn=(GraphNode) it.next();
  67             TermNode tn=(TermNode) gn.getOwner();
  68             MultUpdateNode mun=tn.getUpdate();
  69             if (togenerate.contains(gn))
  70             for (int i=0;i<mun.numUpdates();i++) {
  71                 UpdateNode un=mun.getUpdate(i);
  72                 String name="update"+String.valueOf(count++);
  73                 updatenames.put(un,name);
  74             }
  75         }
  76     }
  77
  78     public void generate(OutputStream outputrepair, OutputStream outputaux,OutputStream outputhead, String st) {
  79         this.outputrepair = new java.io.PrintWriter(outputrepair, true);
  80         this.outputaux = new java.io.PrintWriter(outputaux, true);
  81         this.outputhead = new java.io.PrintWriter(outputhead, true);
  82         headername=st;
  83         name_updates();
  84         generatetypechecks(true);
  85         generate_tokentable();
  86         generate_hashtables();
  87         generate_stateobject();
  88         generate_call();
  89         generate_start();
  90         generate_rules();
  91         generate_checks();
  92         generate_teardown();
  93         CodeWriter crhead = new StandardCodeWriter(this.outputhead);
  94         CodeWriter craux = new StandardCodeWriter(this.outputaux);
  95         crhead.outputline("};");
  96         craux.outputline("}");
  97         generatetypechecks(false);
  98         generate_computesizes();
  99         generatetypechecks(true);
 100         generate_recomputesizes();
 101         generatetypechecks(false);
 102         generate_updates();
 103         StructureGenerator sg=new StructureGenerator(state,this);
 104         sg.buildall();
 105         crhead.outputline("#endif");
 106     }
 107
 108     String ststate="state";
 109     String stmodel="model";
 110     String strepairtable="repairtable";
 111     String stleft="left";
 112     String stright="right";
 113     String stnew="newvalue";
 114
 115     private void generate_updates() {
 116         int count=0;
 117         CodeWriter crhead = new StandardCodeWriter(outputhead);
 118         CodeWriter craux = new StandardCodeWriter(outputaux);
 119
 120         /* Rewrite globals */
 121
 122         for (Iterator it=this.state.stGlobals.descriptors();it.hasNext();) {
 123             VarDescriptor vd=(VarDescriptor)it.next();
 124             craux.outputline("#define "+vd.getSafeSymbol()+" "+ststate+"->"+vd.getSafeSymbol());
 125         }
 126
 127         for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
 128             GraphNode gn=(GraphNode) it.next();
 129             TermNode tn=(TermNode) gn.getOwner();
 130             MultUpdateNode mun=tn.getUpdate();
 131             boolean isrelation=(mun.getDescriptor() instanceof RelationDescriptor);
 132             if (togenerate.contains(gn))
 133             for (int i=0;i<mun.numUpdates();i++) {
 134                 UpdateNode un=mun.getUpdate(i);
 135                 String methodname=(String)updatenames.get(un);
 136
 137                 switch(mun.op) {
 138                 case MultUpdateNode.ADD:
 139                     if (isrelation) {
 140                         crhead.outputline("void "+methodname+"("+name+"_state * " +ststate+","+name+" * "+stmodel+", RepairHash * "+strepairtable+", int "+stleft+", int "+stright+");");
 141                         craux.outputline("void "+methodname+"("+name+"_state * "+ ststate+","+name+" * "+stmodel+", RepairHash * "+strepairtable+", int "+stleft+", int "+stright+")");
 142                     } else {
 143                         crhead.outputline("void "+methodname+"("+name+"_state * "+ ststate+","+name+" * "+stmodel+", RepairHash * "+strepairtable+", int "+stleft+");");
 144                         craux.outputline("void "+methodname+"("+name+"_state * "+ststate+","+name+" * "+stmodel+", RepairHash * "+strepairtable+", int "+stleft+")");
 145                     }
 146                     craux.startblock();
 147                     craux.outputline("int maybe=0;");
 148                     final SymbolTable st = un.getRule().getSymbolTable();
 149                     CodeWriter cr = new StandardCodeWriter(outputaux) {
 150                         public SymbolTable getSymbolTable() { return st; }
 151                     };
 152                     un.generate(cr, false, false, stleft,stright, null,this);
 153                     craux.outputline("if (maybe) printf(\"REALLY BAD\");");
 154                     craux.endblock();
 155                     break;
 156                 case MultUpdateNode.REMOVE: {
 157                     Rule r=un.getRule();
 158                     String methodcall="void "+methodname+"("+name+"_state * "+ststate+","+name+" * "+stmodel+", RepairHash * "+strepairtable;
 159                     for(int j=0;j<r.numQuantifiers();j++) {
 160                         Quantifier q=r.getQuantifier(j);
 161                         if (q instanceof SetQuantifier) {
 162                             SetQuantifier sq=(SetQuantifier) q;
 163                             methodcall+=","+sq.getVar().getType().getGenerateType().getSafeSymbol()+" "+sq.getVar().getSafeSymbol();
 164                         } else if (q instanceof RelationQuantifier) {
 165                             RelationQuantifier rq=(RelationQuantifier) q;
 166
 167                             methodcall+=","+rq.x.getType().getGenerateType().getSafeSymbol()+" "+rq.x.getSafeSymbol();
 168                             methodcall+=","+rq.y.getType().getGenerateType().getSafeSymbol()+" "+rq.y.getSafeSymbol();
 169                         } else if (q instanceof ForQuantifier) {
 170                             ForQuantifier fq=(ForQuantifier) q;
 171                             methodcall+=",int "+fq.getVar().getSafeSymbol();
 172                         }
 173                     }
 174                     methodcall+=")";
 175                     crhead.outputline(methodcall+";");
 176                     craux.outputline(methodcall);
 177                     craux.startblock();
 178                     craux.outputline("int maybe=0;");
 179                     final SymbolTable st2 = un.getRule().getSymbolTable();
 180                     CodeWriter cr2 = new StandardCodeWriter(outputaux) {
 181                         public SymbolTable getSymbolTable() { return st2; }
 182                     };
 183                     un.generate(cr2, true, false, null,null, null,this);
 184                     craux.outputline("if (maybe) printf(\"REALLY BAD\");");
 185                     craux.endblock();
 186                 }
 187                     break;
 188                 case MultUpdateNode.MODIFY: {
 189                     Rule r=un.getRule();
 190                     String methodcall="void "+methodname+"("+name+"_state * "+ststate+","+name+" * "+stmodel+", RepairHash * "+strepairtable;
 191                     for(int j=0;j<r.numQuantifiers();j++) {
 192                         Quantifier q=r.getQuantifier(j);
 193                         if (q instanceof SetQuantifier) {
 194                             SetQuantifier sq=(SetQuantifier) q;
 195                             methodcall+=","+sq.getVar().getType().getGenerateType().getSafeSymbol()+" "+sq.getVar().getSafeSymbol();
 196                         } else if (q instanceof RelationQuantifier) {
 197                             RelationQuantifier rq=(RelationQuantifier) q;
 198
 199                             methodcall+=", "+rq.x.getType().getGenerateType().getSafeSymbol()+" "+rq.x.getSafeSymbol();
 200                             methodcall+=", "+rq.y.getType().getGenerateType().getSafeSymbol()+" "+rq.y.getSafeSymbol();
 201                         } else if (q instanceof ForQuantifier) {
 202                             ForQuantifier fq=(ForQuantifier) q;
 203                             methodcall+=", int "+fq.getVar().getSafeSymbol();
 204                         }
 205                     }
 206                     methodcall+=", "+stleft+", "+stright+", "+stnew;
 207                     methodcall+=")";
 208                     crhead.outputline(methodcall+";");
 209                     craux.outputline(methodcall);
 210                     craux.startblock();
 211                     craux.outputline("int maybe=0;");
 212                     final SymbolTable st2 = un.getRule().getSymbolTable();
 213                     CodeWriter cr2 = new StandardCodeWriter(outputaux) {
 214                         public SymbolTable getSymbolTable() { return st2; }
 215                     };
 216                     un.generate(cr2, false, true, stleft, stright, stnew, this);
 217                     craux.outputline("if (maybe) printf(\"REALLY BAD\");");
 218                     craux.endblock();
 219                 }
 220                     break;
 221
 222                 default:
 223                     throw new Error("Nonimplement Update");
 224                 }
 225             }
 226         }
 227     }
 228
 229     private void generate_call() {
 230         CodeWriter cr = new StandardCodeWriter(outputrepair);
 231         VarDescriptor vdstate=VarDescriptor.makeNew("repairstate");
 232         cr.outputline(name+"_state * "+vdstate.getSafeSymbol()+"=new "+name+"_state();");
 233         Iterator globals=state.stGlobals.descriptors();
 234         while (globals.hasNext()) {
 235             VarDescriptor vd=(VarDescriptor) globals.next();
 236             cr.outputline(vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+"=("+vd.getType().getGenerateType().getSafeSymbol()+")"+vd.getSafeSymbol()+";");
 237         }
 238         /* Insert repair here */
 239         cr.outputline(vdstate.getSafeSymbol()+"->doanalysis();");
 240         globals=state.stGlobals.descriptors();
 241         while (globals.hasNext()) {
 242             VarDescriptor vd=(VarDescriptor) globals.next();
 243             cr.outputline("*(("+vd.getType().getGenerateType().getSafeSymbol()+"*) &"+vd.getSafeSymbol()+")="+vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+";");
 244         }
 245         cr.outputline("delete "+vdstate.getSafeSymbol()+";");
 246     }
 247
 248     private void generate_tokentable() {
 249         CodeWriter cr = new StandardCodeWriter(outputrepair);
 250         Iterator tokens = TokenLiteralExpr.tokens.keySet().iterator();
 251
 252         cr.outputline("");
 253         cr.outputline("// Token values");
 254         cr.outputline("");
 255
 256         while (tokens.hasNext()) {
 257             Object token = tokens.next();
 258             cr.outputline("// " + token.toString() + " = " + TokenLiteralExpr.tokens.get(token).toString());
 259         }
 260
 261         cr.outputline("");
 262         cr.outputline("");
 263     }
 264
 265     private void generate_stateobject() {
 266         CodeWriter crhead = new StandardCodeWriter(outputhead);
 267         crhead.outputline("class "+name+"_state {");
 268         crhead.outputline("public:");
 269         Iterator globals=state.stGlobals.descriptors();
 270         while (globals.hasNext()) {
 271             VarDescriptor vd=(VarDescriptor) globals.next();
 272             crhead.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+";");
 273         }
 274         crhead.outputline("void computesizes(int *,int **);");
 275         crhead.outputline("void recomputesizes();");
 276     }
 277
 278     private void generate_computesizes() {
 279         int max=TypeDescriptor.counter;
 280         TypeDescriptor[] tdarray=new TypeDescriptor[max];
 281         for(Iterator it=state.stTypes.descriptors();it.hasNext();) {
 282             TypeDescriptor ttd=(TypeDescriptor)it.next();
 283             tdarray[ttd.getId()]=ttd;
 284         }
 285         final SymbolTable st = state.stGlobals;
 286         CodeWriter cr = new StandardCodeWriter(outputaux) {
 287                 public SymbolTable getSymbolTable() { return st; }
 288             };
 289
 290         cr.outputline("void "+name+"_state::computesizes(int *sizearray,int **numele) {");
 291         for(int i=0;i<max;i++) {
 292             TypeDescriptor td=tdarray[i];
 293             Expr size=td.getSizeExpr();
 294             VarDescriptor vd=VarDescriptor.makeNew("size");
 295             size.generate(cr,vd);
 296             cr.outputline("sizearray["+i+"]="+vd.getSafeSymbol()+";");
 297         }
 298         for(int i=0;i<max;i++) {
 299             TypeDescriptor td=tdarray[i];
 300             if (td instanceof StructureTypeDescriptor) {
 301                 StructureTypeDescriptor std=(StructureTypeDescriptor) td;
 302                 for(int j=0;j<std.fieldlist.size();j++) {
 303                     FieldDescriptor fd=(FieldDescriptor)std.fieldlist.get(j);
 304                     if (fd instanceof ArrayDescriptor) {
 305                         ArrayDescriptor ad=(ArrayDescriptor)fd;
 306                         Expr index=ad.getIndexBound();
 307                         VarDescriptor vd=VarDescriptor.makeNew("index");
 308                         index.generate(cr,vd);
 309                         cr.outputline("numele["+i+"]["+j+"]="+vd.getSafeSymbol()+";");
 310                     }
 311                 }
 312             }
 313         }
 314         cr.outputline("}");
 315     }
 316
 317     private void generate_recomputesizes() {
 318         int max=TypeDescriptor.counter;
 319         TypeDescriptor[] tdarray=new TypeDescriptor[max];
 320         for(Iterator it=state.stTypes.descriptors();it.hasNext();) {
 321             TypeDescriptor ttd=(TypeDescriptor)it.next();
 322             tdarray[ttd.getId()]=ttd;
 323         }
 324         final SymbolTable st = state.stGlobals;
 325         CodeWriter cr = new StandardCodeWriter(outputaux) {
 326                 public SymbolTable getSymbolTable() { return st; }
 327             };
 328         cr.outputline("void "+name+"_state::recomputesizes() {");
 329         for(int i=0;i<max;i++) {
 330             TypeDescriptor td=tdarray[i];
 331             Expr size=td.getSizeExpr();
 332             VarDescriptor vd=VarDescriptor.makeNew("size");
 333             size.generate(cr,vd);
 334         }
 335         for(int i=0;i<max;i++) {
 336             TypeDescriptor td=tdarray[i];
 337             if (td instanceof StructureTypeDescriptor) {
 338                 StructureTypeDescriptor std=(StructureTypeDescriptor) td;
 339                 for(int j=0;j<std.fieldlist.size();j++) {
 340                     FieldDescriptor fd=(FieldDescriptor)std.fieldlist.get(j);
 341                     if (fd instanceof ArrayDescriptor) {
 342                         ArrayDescriptor ad=(ArrayDescriptor)fd;
 343                         Expr index=ad.getIndexBound();
 344                         VarDescriptor vd=VarDescriptor.makeNew("index");
 345                         index.generate(cr,vd);
 346                     }
 347                 }
 348             }
 349         }
 350         cr.outputline("}");
 351     }
 352
 353
 354     private void generate_hashtables() {
 355         CodeWriter craux = new StandardCodeWriter(outputaux);
 356         CodeWriter crhead = new StandardCodeWriter(outputhead);
 357         crhead.outputline("#ifndef "+name+"_h");
 358         crhead.outputline("#define "+name+"_h");
 359         crhead.outputline("#include \"SimpleHash.h\"");
 360         crhead.outputline("extern \"C\" {");
 361         crhead.outputline("#include \"instrument.h\"");
 362         crhead.outputline("}");
 363         crhead.outputline("#include <stdio.h>");
 364         crhead.outputline("#include <stdlib.h>");
 365         crhead.outputline("class "+name+" {");
 366         crhead.outputline("public:");
 367         crhead.outputline(name+"();");
 368         crhead.outputline("~"+name+"();");
 369         craux.outputline("#include \""+headername+"\"");
 370         craux.outputline("#include \"size.h\"");
 371
 372         craux.outputline(name+"::"+name+"() {");
 373         craux.outputline("// creating hashtables ");
 374
 375         /* build sets */
 376         Iterator sets = state.stSets.descriptors();
 377
 378         /* first pass create all the hash tables */
 379         while (sets.hasNext()) {
 380             SetDescriptor set = (SetDescriptor) sets.next();
 381             crhead.outputline("SimpleHash* " + set.getSafeSymbol() + "_hash;");
 382             craux.outputline(set.getSafeSymbol() + "_hash = new SimpleHash();");
 383         }
 384
 385         /* second pass build relationships between hashtables */
 386         sets = state.stSets.descriptors();
 387
 388         while (sets.hasNext()) {
 389             SetDescriptor set = (SetDescriptor) sets.next();
 390             Iterator subsets = set.subsets();
 391
 392             while (subsets.hasNext()) {
 393                 SetDescriptor subset = (SetDescriptor) subsets.next();
 394                 craux.outputline(subset.getSafeSymbol() + "_hash->addParent(" + set.getSafeSymbol() + "_hash);");
 395             }
 396         }
 397
 398         /* build relations */
 399         Iterator relations = state.stRelations.descriptors();
 400
 401         /* first pass create all the hash tables */
 402         while (relations.hasNext()) {
 403             RelationDescriptor relation = (RelationDescriptor) relations.next();
 404
 405             if (relation.testUsage(RelationDescriptor.IMAGE)) {
 406                 crhead.outputline("SimpleHash* " + relation.getSafeSymbol() + "_hash;");
 407                 craux.outputline(relation.getSafeSymbol() + "_hash = new SimpleHash();");
 408             }
 409
 410             if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
 411                 crhead.outputline("SimpleHash* " + relation.getSafeSymbol() + "_hashinv;");
 412                 craux.outputline(relation.getSafeSymbol() + "_hashinv = new SimpleHash();");
 413             }
 414         }
 415
 416         craux.outputline("}");
 417         crhead.outputline("};");
 418         craux.outputline(name+"::~"+name+"() {");
 419         craux.outputline("// deleting hashtables");
 420
 421         /* build destructor */
 422         sets = state.stSets.descriptors();
 423
 424         /* first pass create all the hash tables */
 425         while (sets.hasNext()) {
 426             SetDescriptor set = (SetDescriptor) sets.next();
 427             craux.outputline("delete "+set.getSafeSymbol() + "_hash;");
 428         }
 429
 430         /* destroy relations */
 431         relations = state.stRelations.descriptors();
 432
 433         /* first pass create all the hash tables */
 434         while (relations.hasNext()) {
 435             RelationDescriptor relation = (RelationDescriptor) relations.next();
 436
 437             if (relation.testUsage(RelationDescriptor.IMAGE)) {
 438                 craux.outputline("delete "+relation.getSafeSymbol() + "_hash;");
 439             }
 440
 441             if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
 442                 craux.outputline("delete " + relation.getSafeSymbol() + "_hashinv;");
 443             }
 444         }
 445         craux.outputline("}");
 446     }
 447
 448     private void generate_start() {
 449         CodeWriter crhead = new StandardCodeWriter(outputhead);
 450         CodeWriter craux = new StandardCodeWriter(outputaux);
 451         oldmodel=VarDescriptor.makeNew("oldmodel");
 452         newmodel=VarDescriptor.makeNew("newmodel");
 453         worklist=VarDescriptor.makeNew("worklist");
 454         goodflag=VarDescriptor.makeNew("goodflag");
 455         repairtable=VarDescriptor.makeNew("repairtable");
 456         crhead.outputline("void doanalysis();");
 457         craux.outputline("void "+name +"_state::doanalysis()");
 458         craux.startblock();
 459         craux.outputline("int highmark;");
 460         craux.outputline("initializestack(&highmark);");
 461         craux.outputline("typeobject *typeobject1=gettypeobject();");
 462         craux.outputline("typeobject1->computesizes(this);");
 463         craux.outputline("recomputesizes();");
 464         craux.outputline(name+ " * "+oldmodel.getSafeSymbol()+"=0;");
 465         craux.outputline("WorkList * "+worklist.getSafeSymbol()+" = new WorkList();");
 466         craux.outputline("RepairHash * "+repairtable.getSafeSymbol()+"=0;");
 467         craux.outputline("while (1)");
 468         craux.startblock();
 469         craux.outputline(name+ " * "+newmodel.getSafeSymbol()+"=new "+name+"();");
 470     }
 471
 472     private void generate_teardown() {
 473         CodeWriter cr = new StandardCodeWriter(outputaux);
 474         cr.endblock();
 475     }
 476
 477     Set ruleset=null;
 478     private void generate_rules() {
 479         /* first we must sort the rules */
 480         RelationDescriptor.prefix = newmodel.getSafeSymbol()+"->";
 481         SetDescriptor.prefix = newmodel.getSafeSymbol()+"->";
 482         System.out.println("SCC="+(mrd.numSCC()-1));
 483         for(int sccindex=0;sccindex<mrd.numSCC();sccindex++) {
 484             ruleset=mrd.getSCC(sccindex);
 485             boolean needworklist=mrd.hasCycle(sccindex);
 486
 487             if (!needworklist) {
 488                 Iterator iterator_rs = ruleset.iterator();
 489                 while (iterator_rs.hasNext()) {
 490                     Rule rule = (Rule) iterator_rs.next();
 491                     {
 492                         final SymbolTable st = rule.getSymbolTable();
 493                         CodeWriter cr = new StandardCodeWriter(outputaux) {
 494                                 public SymbolTable getSymbolTable() { return st; }
 495                             };
 496                         cr.outputline("// build " +escape(rule.toString()));
 497                         cr.startblock();
 498                         cr.outputline("int maybe=0;");
 499                         ListIterator quantifiers = rule.quantifiers();
 500                         while (quantifiers.hasNext()) {
 501                             Quantifier quantifier = (Quantifier) quantifiers.next();
 502                             quantifier.generate_open(cr);
 503                         }
 504
 505                         /* pretty print! */
 506                         cr.output("//");
 507                         rule.getGuardExpr().prettyPrint(cr);
 508                         cr.outputline("");
 509
 510                         /* now we have to generate the guard test */
 511                         VarDescriptor guardval = VarDescriptor.makeNew();
 512                         rule.getGuardExpr().generate(cr, guardval);
 513                         cr.outputline("if (" + guardval.getSafeSymbol() + ")");
 514                         cr.startblock();
 515
 516                         /* now we have to generate the inclusion code */
 517                         currentrule=rule;
 518                         rule.getInclusion().generate(cr);
 519                         cr.endblock();
 520                         while (quantifiers.hasPrevious()) {
 521                             Quantifier quantifier = (Quantifier) quantifiers.previous();
 522                             cr.endblock();
 523                         }
 524                         cr.endblock();
 525                         cr.outputline("");
 526                         cr.outputline("");
 527                     }
 528                 }
 529             } else {
 530                 CodeWriter cr2 = new StandardCodeWriter(outputaux);
 531
 532                 for(Iterator initialworklist=ruleset.iterator();initialworklist.hasNext();) {
 533                     /** Construct initial worklist set */
 534                     Rule rule=(Rule)initialworklist.next();
 535                     cr2.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
 536                 }
 537
 538                 cr2.outputline("while ("+worklist.getSafeSymbol()+"->hasMoreElements())");
 539                 cr2.startblock();
 540                 VarDescriptor idvar=VarDescriptor.makeNew("id");
 541                 cr2.outputline("int "+idvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getid();");
 542
 543                 String elseladder = "if";
 544
 545                 Iterator iterator_rules = ruleset.iterator();
 546                 while (iterator_rules.hasNext()) {
 547
 548                     Rule rule = (Rule) iterator_rules.next();
 549                     int dispatchid = rule.getNum();
 550
 551                     {
 552                         final SymbolTable st = rule.getSymbolTable();
 553                         CodeWriter cr = new StandardCodeWriter(outputaux) {
 554                                 public SymbolTable getSymbolTable() { return st; }
 555                             };
 556
 557                         cr.indent();
 558                         cr.outputline(elseladder + " ("+idvar.getSafeSymbol()+" == " + dispatchid + ")");
 559                         cr.startblock();
 560                         cr.outputline("int maybe=0;");
 561                         VarDescriptor typevar=VarDescriptor.makeNew("type");
 562                         VarDescriptor leftvar=VarDescriptor.makeNew("left");
 563                         VarDescriptor rightvar=VarDescriptor.makeNew("right");
 564                         cr.outputline("int "+typevar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->gettype();");
 565                         cr.outputline("int "+leftvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getlvalue();");
 566                         cr.outputline("int "+rightvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getrvalue();");
 567                         cr.outputline("// build " +escape(rule.toString()));
 568
 569
 570                         for (int j=0;j<rule.numQuantifiers();j++) {
 571                             Quantifier quantifier = rule.getQuantifier(j);
 572                             quantifier.generate_open(cr, typevar.getSafeSymbol(),j,leftvar.getSafeSymbol(),rightvar.getSafeSymbol());
 573                         }
 574
 575                         /* pretty print! */
 576                         cr.output("//");
 577
 578                         rule.getGuardExpr().prettyPrint(cr);
 579                         cr.outputline("");
 580
 581                         /* now we have to generate the guard test */
 582
 583                         VarDescriptor guardval = VarDescriptor.makeNew();
 584                         rule.getGuardExpr().generate(cr, guardval);
 585
 586                         cr.outputline("if (" + guardval.getSafeSymbol() + ")");
 587                         cr.startblock();
 588
 589                         /* now we have to generate the inclusion code */
 590                         currentrule=rule;
 591                         rule.getInclusion().generate(cr);
 592                         cr.endblock();
 593
 594                         for (int j=0;j<rule.numQuantifiers();j++) {
 595                             cr.endblock();
 596                         }
 597
 598                         // close startblocks generated by DotExpr memory checks
 599                         //DotExpr.generate_memory_endblocks(cr);
 600
 601                         cr.endblock(); // end else-if WORKLIST ladder
 602
 603                         elseladder = "else if";
 604                     }
 605                 }
 606                 cr2.outputline("else");
 607                 cr2.startblock();
 608                 cr2.outputline("printf(\"VERY BAD !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\\n\\n\");");
 609                 cr2.outputline("exit(1);");
 610                 cr2.endblock();
 611                 // end block created for worklist
 612                 cr2.outputline(worklist.getSafeSymbol()+"->pop();");
 613                 cr2.endblock();
 614             }
 615         }
 616     }
 617
 618     public static String escape(String s) {
 619         String newstring="";
 620         for(int i=0;i<s.length();i++) {
 621             char c=s.charAt(i);
 622             if (c=='"')
 623                 newstring+="\"";
 624             else
 625                 newstring+=c;
 626         }
 627         return newstring;
 628     }
 629
 630     private void generate_checks() {
 631
 632         /* do constraint checks */
 633         Vector constraints = state.vConstraints;
 634
 635         for (int i = 0; i < constraints.size(); i++) {
 636             Constraint constraint = (Constraint) constraints.elementAt(i);
 637
 638             {
 639                 final SymbolTable st = constraint.getSymbolTable();
 640                 CodeWriter cr = new StandardCodeWriter(outputaux) {
 641                         public SymbolTable getSymbolTable() { return st; }
 642                     };
 643                 cr.outputline("// checking " + escape(constraint.toString()));
 644                 cr.startblock();
 645
 646                 ListIterator quantifiers = constraint.quantifiers();
 647
 648                 while (quantifiers.hasNext()) {
 649                     Quantifier quantifier = (Quantifier) quantifiers.next();
 650                     quantifier.generate_open(cr);
 651                 }
 652
 653                 cr.outputline("int maybe = 0;");
 654
 655                 /* now we have to generate the guard test */
 656
 657                 VarDescriptor constraintboolean = VarDescriptor.makeNew("constraintboolean");
 658                 constraint.getLogicStatement().generate(cr, constraintboolean);
 659
 660                 cr.outputline("if (maybe)");
 661                 cr.startblock();
 662                 cr.outputline("printf(\"maybe fail " +  escape(constraint.toString()) + ". \\n\");");
 663                 cr.outputline("exit(1);");
 664                 cr.endblock();
 665
 666                 cr.outputline("else if (!" + constraintboolean.getSafeSymbol() + ")");
 667                 cr.startblock();
 668                 if (!Compiler.REPAIR)
 669                     cr.outputline("printf(\"fail " + escape(constraint.toString()) + ". \\n\");");
 670                 else {
 671                 /* Do repairs */
 672                 /* Build new repair table */
 673                 cr.outputline("if ("+repairtable.getSafeSymbol()+")");
 674                 cr.outputline("delete "+repairtable.getSafeSymbol()+";");
 675                 cr.outputline(repairtable.getSafeSymbol()+"=new RepairHash();");
 676
 677
 678                 /* Compute cost of each repair */
 679                 VarDescriptor mincost=VarDescriptor.makeNew("mincost");
 680                 VarDescriptor mincostindex=VarDescriptor.makeNew("mincostindex");
 681                 DNFConstraint dnfconst=constraint.dnfconstraint;
 682                 if (dnfconst.size()<=1) {
 683                     cr.outputline("int "+mincostindex.getSafeSymbol()+"=0;");
 684                 }
 685                 if (dnfconst.size()>1) {
 686                     cr.outputline("int "+mincostindex.getSafeSymbol()+";");
 687                     boolean first=true;
 688                     for(int j=0;j<dnfconst.size();j++) {
 689                         Conjunction conj=dnfconst.get(j);
 690                         GraphNode gn=(GraphNode)termination.conjtonodemap.get(conj);
 691                         if (removed.contains(gn))
 692                             continue;
 693
 694                         VarDescriptor costvar;
 695                         if (first) {
 696                             costvar=mincost;
 697                         } else
 698                             costvar=VarDescriptor.makeNew("cost");
 699                         for(int k=0;k<conj.size();k++) {
 700                             DNFPredicate dpred=conj.get(k);
 701                             Predicate p=dpred.getPredicate();
 702                             boolean negate=dpred.isNegated();
 703                             VarDescriptor predvalue=VarDescriptor.makeNew("Predicatevalue");
 704                             p.generate(cr,predvalue);
 705                             if (negate)
 706                                 cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
 707                             else
 708                                 cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
 709                             if (k==0)
 710                                 cr.outputline("int "+costvar.getSafeSymbol()+"="+cost.getCost(dpred)+";");
 711                             else
 712                                 cr.outputline(costvar.getSafeSymbol()+"+="+cost.getCost(dpred)+";");
 713                         }
 714
 715                         if(!first) {
 716                             cr.outputline("if ("+costvar.getSafeSymbol()+"<"+mincost.getSafeSymbol()+")");
 717                             cr.startblock();
 718                             cr.outputline(mincost.getSafeSymbol()+"="+costvar.getSafeSymbol()+";");
 719                             cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
 720                             cr.endblock();
 721                         } else
 722                             cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
 723                         first=false;
 724                     }
 725                 }
 726                 cr.outputline("switch("+mincostindex.getSafeSymbol()+") {");
 727                 for(int j=0;j<dnfconst.size();j++) {
 728                     Conjunction conj=dnfconst.get(j);
 729                     GraphNode gn=(GraphNode)termination.conjtonodemap.get(conj);
 730                     if (removed.contains(gn))
 731                         continue;
 732                     cr.outputline("case "+j+":");
 733                     for(int k=0;k<conj.size();k++) {
 734                         DNFPredicate dpred=conj.get(k);
 735                         Predicate p=dpred.getPredicate();
 736                         boolean negate=dpred.isNegated();
 737                         VarDescriptor predvalue=VarDescriptor.makeNew("Predicatevalue");
 738                         p.generate(cr,predvalue);
 739                         if (negate)
 740                             cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
 741                         else
 742                             cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
 743                         cr.startblock();
 744                         if (p instanceof InclusionPredicate)
 745                             generateinclusionrepair(conj,dpred, cr);
 746                         else if (p instanceof ExprPredicate) {
 747                             ExprPredicate ep=(ExprPredicate)p;
 748                             if (ep.getType()==ExprPredicate.SIZE)
 749                                 generatesizerepair(conj,dpred,cr);
 750                             else if (ep.getType()==ExprPredicate.COMPARISON)
 751                                 generatecomparisonrepair(conj,dpred,cr);
 752                         } else throw new Error("Unrecognized Predicate");
 753                         cr.endblock();
 754                     }
 755                     /* Update model */
 756                     cr.outputline("break;");
 757                 }
 758                 cr.outputline("}");
 759
 760                 cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
 761                 cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
 762                 cr.outputline(oldmodel.getSafeSymbol()+"="+newmodel.getSafeSymbol()+";");
 763                 cr.outputline("goto rebuild;");  /* Rebuild model and all */
 764                 }
 765                 cr.endblock();
 766
 767                 while (quantifiers.hasPrevious()) {
 768                     Quantifier quantifier = (Quantifier) quantifiers.previous();
 769                     cr.endblock();
 770                 }
 771                 cr.endblock();
 772                 cr.outputline("");
 773                 cr.outputline("");
 774             }
 775         }
 776         CodeWriter cr = new StandardCodeWriter(outputaux);
 777         cr.startblock();
 778         cr.outputline("if ("+repairtable.getSafeSymbol()+")");
 779         cr.outputline("delete "+repairtable.getSafeSymbol()+";");
 780         cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
 781         cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
 782         cr.outputline("delete "+newmodel.getSafeSymbol()+";");
 783         cr.outputline("delete "+worklist.getSafeSymbol()+";");
 784         cr.outputline("resettypemap();");
 785         cr.outputline("break;");
 786         cr.endblock();
 787         cr.outputline("rebuild:");
 788         cr.outputline(";");
 789
 790     }
 791
 792     private MultUpdateNode getmultupdatenode(Conjunction conj, DNFPredicate dpred, int repairtype) {
 793         MultUpdateNode mun=null;
 794         GraphNode gn=(GraphNode) termination.conjtonodemap.get(conj);
 795         for(Iterator edgeit=gn.edges();(mun==null)&&edgeit.hasNext();) {
 796             GraphNode gn2=((GraphNode.Edge) edgeit.next()).getTarget();
 797             TermNode tn2=(TermNode)gn2.getOwner();
 798             if (tn2.getType()==TermNode.ABSTRACT) {
 799                 AbstractRepair ar=tn2.getAbstract();
 800                 if (((repairtype==-1)||(ar.getType()==repairtype))&&
 801                     ar.getPredicate()==dpred) {
 802                     for(Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
 803                         GraphNode gn3=((GraphNode.Edge) edgeit2.next()).getTarget();
 804                         if (!removed.contains(gn3)) {
 805                             TermNode tn3=(TermNode)gn3.getOwner();
 806                             if (tn3.getType()==TermNode.UPDATE) {
 807                                 mun=tn3.getUpdate();
 808                                 break;
 809                             }
 810                         }
 811                     }
 812                 }
 813             }
 814         }
 815         return mun;
 816     }
 817
 818     /** Generates abstract (and concrete) repair for a comparison */
 819
 820     private void generatecomparisonrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
 821         MultUpdateNode munmodify=getmultupdatenode(conj,dpred,AbstractRepair.MODIFYRELATION);
 822         MultUpdateNode munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
 823         MultUpdateNode munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
 824         ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
 825         RelationDescriptor rd=(RelationDescriptor)ep.getDescriptor();
 826         boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
 827         boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
 828         boolean inverted=ep.inverted();
 829         boolean negated=dpred.isNegated();
 830         OpExpr expr=(OpExpr)ep.expr;
 831         Opcode opcode=expr.getOpcode();
 832         VarDescriptor leftside=VarDescriptor.makeNew("leftside");
 833         VarDescriptor rightside=VarDescriptor.makeNew("rightside");
 834         VarDescriptor newvalue=VarDescriptor.makeNew("newvalue");
 835         if (!inverted) {
 836             expr.getLeftExpr().generate(cr,leftside);
 837             expr.getRightExpr().generate(cr,newvalue);
 838             cr.outputline(rd.getRange().getType().getGenerateType().getSafeSymbol()+" "+rightside.getSafeSymbol()+";");
 839             cr.outputline(rd.getSafeSymbol()+"_hash->get("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
 840         } else {
 841             expr.getLeftExpr().generate(cr,rightside);
 842             expr.getRightExpr().generate(cr,newvalue);
 843             cr.outputline(rd.getDomain().getType().getGenerateType().getSafeSymbol()+" "+leftside.getSafeSymbol()+";");
 844             cr.outputline(rd.getSafeSymbol()+"_hashinv->get("+leftside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
 845         }
 846         if (negated)
 847             if (opcode==Opcode.GT) {
 848                 opcode=Opcode.LE;
 849             } else if (opcode==Opcode.GE) {
 850                 opcode=Opcode.LT;
 851             } else if (opcode==Opcode.LT) {
 852                 opcode=Opcode.GE;
 853             } else if (opcode==Opcode.LE) {
 854                 opcode=Opcode.GT;
 855             } else if (opcode==Opcode.EQ) {
 856                 opcode=Opcode.NE;
 857             } else if (opcode==Opcode.NE) {
 858                 opcode=Opcode.EQ;
 859             } else {
 860                 throw new Error("Unrecognized Opcode");
 861             }
 862
 863         if (opcode==Opcode.GT) {
 864             cr.outputline(newvalue.getSafeSymbol()+"++;");
 865         } else if (opcode==Opcode.GE) {
 866             /* Equal */
 867         } else if (opcode==Opcode.LT) {
 868             cr.outputline(newvalue.getSafeSymbol()+"--;");
 869         } else if (opcode==Opcode.LE) {
 870             /* Equal */
 871         } else if (opcode==Opcode.EQ) {
 872             /* Equal */
 873         } else if (opcode==Opcode.NE) { /* search for FLAGNE if this is changed*/
 874             cr.outputline(newvalue.getSafeSymbol()+"++;");
 875         } else {
 876             throw new Error("Unrecognized Opcode");
 877         }
 878         /* Do abstract repairs */
 879         if (usageimage) {
 880             cr.outputline(rd.getSafeSymbol()+"_hash->remove("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
 881             if (!inverted) {
 882                 cr.outputline(rd.getSafeSymbol()+"_hash->add("+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
 883             } else {
 884                 cr.outputline(rd.getSafeSymbol()+"_hash->add("+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
 885             }
 886         }
 887         if (usageinvimage) {
 888             cr.outputline(rd.getSafeSymbol()+"_hashinv->remove("+rightside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
 889             if (!inverted) {
 890                 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+newvalue.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
 891             } else {
 892                 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+rightside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
 893             }
 894         }
 895         /* Do concrete repairs */
 896         if (munmodify!=null) {
 897             for(int i=0;i<state.vRules.size();i++) {
 898                 Rule r=(Rule)state.vRules.get(i);
 899                 if (r.getInclusion().getTargetDescriptors().contains(rd)) {
 900                     for(int j=0;j<munmodify.numUpdates();j++) {
 901                         UpdateNode un=munmodify.getUpdate(j);
 902                         if (un.getRule()==r) {
 903                             /* Update for rule r */
 904                             String name=(String)updatenames.get(un);
 905                             cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+",(int) &"+name+","+newvalue.getSafeSymbol()+");");
 906                         }
 907                     }
 908                 }
 909             }
 910
 911         } else {
 912             /* Start with scheduling removal */
 913             for(int i=0;i<state.vRules.size();i++) {
 914                 Rule r=(Rule)state.vRules.get(i);
 915                 if (r.getInclusion().getTargetDescriptors().contains(rd)) {
 916                     for(int j=0;j<munremove.numUpdates();j++) {
 917                         UpdateNode un=munremove.getUpdate(i);
 918                         if (un.getRule()==r) {
 919                             /* Update for rule r */
 920                             String name=(String)updatenames.get(un);
 921                             cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+",(int) &"+name+");");
 922                         }
 923                     }
 924                 }
 925             }
 926             /* Now do addition */
 927             UpdateNode un=munadd.getUpdate(0);
 928             String name=(String)updatenames.get(un);
 929             if (!inverted) {
 930                 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
 931             } else {
 932                 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
 933             }
 934         }
 935     }
 936
 937     public void generatesizerepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr) {
 938         ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
 939         OpExpr expr=(OpExpr)ep.expr;
 940         Opcode opcode=expr.getOpcode();
 941         {
 942             boolean negated=dpred.isNegated();
 943             if (negated)
 944                 if (opcode==Opcode.GT) {
 945                     opcode=Opcode.LE;
 946                 } else if (opcode==Opcode.GE) {
 947                     opcode=Opcode.LT;
 948                 } else if (opcode==Opcode.LT) {
 949                     opcode=Opcode.GE;
 950                 } else if (opcode==Opcode.LE) {
 951                     opcode=Opcode.GT;
 952                 } else if (opcode==Opcode.EQ) {
 953                     opcode=Opcode.NE;
 954                 } else if (opcode==Opcode.NE) {
 955                     opcode=Opcode.EQ;
 956                 } else {
 957                     throw new Error("Unrecognized Opcode");
 958                 }
 959         }
 960         MultUpdateNode munremove;
 961
 962         MultUpdateNode munadd;
 963         if (ep.getDescriptor() instanceof RelationDescriptor) {
 964             munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
 965             munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
 966         } else {
 967             munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMSET);
 968             munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTOSET);
 969         }
 970         int size=ep.rightSize();
 971         VarDescriptor sizevar=VarDescriptor.makeNew("size");
 972         ((OpExpr)expr).left.generate(cr, sizevar);
 973         VarDescriptor change=VarDescriptor.makeNew("change");
 974         cr.outputline("int "+change.getSafeSymbol()+";");
 975         boolean generateadd=false;
 976         boolean generateremove=false;
 977         if (opcode==Opcode.GT) {
 978             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
 979             generateadd=true;
 980             generateremove=false;
 981         } else if (opcode==Opcode.GE) {
 982             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
 983             generateadd=true;
 984             generateremove=false;
 985         } else if (opcode==Opcode.LT) {
 986             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size-1)+"-"+sizevar.getSafeSymbol()+";");
 987             generateadd=false;
 988             generateremove=true;
 989         } else if (opcode==Opcode.LE) {
 990             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
 991             generateadd=false;
 992             generateremove=true;
 993         } else if (opcode==Opcode.EQ) {
 994             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
 995             if (size==0)
 996                 generateadd=false;
 997             else
 998                 generateadd=true;
 999             generateremove=true;
1000         } else if (opcode==Opcode.NE) {
1001             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
1002             generateadd=true;
1003             generateremove=false;
1004         } else {
1005             throw new Error("Unrecognized Opcode");
1006         }
1007         Descriptor d=ep.getDescriptor();
1008         if (generateremove) {
1009             cr.outputline("for(;"+change.getSafeSymbol()+"<0;"+change.getSafeSymbol()+"++)");
1010             cr.startblock();
1011             /* Find element to remove */
1012             VarDescriptor leftvar=VarDescriptor.makeNew("leftvar");
1013             VarDescriptor rightvar=VarDescriptor.makeNew("rightvar");
1014             if (d instanceof RelationDescriptor) {
1015                 if (ep.inverted()) {
1016                     rightvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
1017                     cr.outputline("int "+leftvar.getSafeSymbol()+";");
1018                     cr.outputline(d.getSafeSymbol()+"_hashinv->get((int)"+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
1019                 } else {
1020                     leftvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
1021                     cr.outputline("int "+rightvar.getSafeSymbol()+"=0;");
1022                     cr.outputline(d.getSafeSymbol()+"_hash->get((int)"+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
1023                 }
1024             } else {
1025                 cr.outputline("int "+leftvar.getSafeSymbol()+"="+d.getSafeSymbol()+"_hash->firstkey();");
1026             }
1027             /* Generate abstract remove instruction */
1028             if (d instanceof RelationDescriptor) {
1029                 RelationDescriptor rd=(RelationDescriptor) d;
1030                 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1031                 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1032                 if (usageimage)
1033                     cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1034                 if (usageinvimage)
1035                     cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1036             } else {
1037                 cr.outputline(d.getSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1038             }
1039             /* Generate concrete remove instruction */
1040             for(int i=0;i<state.vRules.size();i++) {
1041                 Rule r=(Rule)state.vRules.get(i);
1042                 if (r.getInclusion().getTargetDescriptors().contains(d)) {
1043                     for(int j=0;j<munremove.numUpdates();j++) {
1044                         UpdateNode un=munremove.getUpdate(j);
1045                         if (un.getRule()==r) {
1046                                 /* Update for rule rule r */
1047                             String name=(String)updatenames.get(un);
1048                             if (d instanceof RelationDescriptor) {
1049                                 cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
1050                             } else {
1051                                 cr.outputline(repairtable.getSafeSymbol()+"->addset("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
1052                             }
1053                         }
1054                     }
1055                 }
1056             }
1057             cr.endblock();
1058         }
1059         if (generateadd) {
1060
1061             cr.outputline("for(;"+change.getSafeSymbol()+">0;"+change.getSafeSymbol()+"--)");
1062             cr.startblock();
1063             VarDescriptor newobject=VarDescriptor.makeNew("newobject");
1064             if (d instanceof RelationDescriptor) {
1065                 VarDescriptor otherside=((ImageSetExpr)((SizeofExpr)((OpExpr)ep.expr).left).setexpr).vd;
1066                 RelationDescriptor rd=(RelationDescriptor)d;
1067                 if (sources.relsetSource(rd,!ep.inverted())) {
1068                     /* Set Source */
1069                     SetDescriptor sd=sources.relgetSourceSet(rd,!ep.inverted());
1070                     VarDescriptor iterator=VarDescriptor.makeNew("iterator");
1071                     cr.outputline(sd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";");
1072                     cr.outputline("for("+iterator.getSafeSymbol()+"="+sd.getSafeSymbol()+"_hash->iterator();"+iterator.getSafeSymbol()+".hasNext();)");
1073                     cr.startblock();
1074                     if (ep.inverted()) {
1075                         cr.outputline("if !"+rd.getSafeSymbol()+"_hashinv->contains("+iterator.getSafeSymbol()+"->key(),"+otherside.getSafeSymbol()+")");
1076                     } else {
1077                         cr.outputline("if !"+rd.getSafeSymbol()+"_hash->contains("+otherside.getSafeSymbol()+","+iterator.getSafeSymbol()+"->key())");
1078                     }
1079                     cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();");
1080                     cr.outputline(iterator.getSafeSymbol()+"->next();");
1081                     cr.endblock();
1082                 } else if (sources.relallocSource(rd,!ep.inverted())) {
1083                     /* Allocation Source*/
1084                     sources.relgenerateSourceAlloc(cr,newobject,rd,!ep.inverted());
1085                 } else throw new Error("No source for adding to Relation");
1086                 if (ep.inverted()) {
1087                     boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1088                     boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1089                     if (usageimage)
1090                         cr.outputline(rd.getSafeSymbol()+"_hash->add("+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
1091                     if (usageinvimage)
1092                         cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1093
1094                     UpdateNode un=munadd.getUpdate(0);
1095                     String name=(String)updatenames.get(un);
1096                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
1097                 } else {
1098                     boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1099                     boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1100                     if (usageimage)
1101                         cr.outputline(rd.getSafeSymbol()+"_hash->add("+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1102                     if (usageinvimage)
1103                         cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
1104                     UpdateNode un=munadd.getUpdate(0);
1105                     String name=(String)updatenames.get(un);
1106                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1107                 }
1108             } else {
1109                 SetDescriptor sd=(SetDescriptor)d;
1110                 if (sources.setSource(sd)) {
1111                     /* Set Source */
1112                     /* Set Source */
1113                     SetDescriptor sourcesd=sources.getSourceSet(sd);
1114                     VarDescriptor iterator=VarDescriptor.makeNew("iterator");
1115                     cr.outputline(sourcesd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";");
1116                     cr.outputline("for("+iterator.getSafeSymbol()+"="+sourcesd.getSafeSymbol()+"_hash->iterator();"+iterator.getSafeSymbol()+".hasNext();)");
1117                     cr.startblock();
1118                     cr.outputline("if !"+sd.getSafeSymbol()+"_hash->contains("+iterator.getSafeSymbol()+"->key())");
1119                     cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();");
1120                     cr.outputline(iterator.getSafeSymbol()+"->next();");
1121                     cr.endblock();
1122                 } else if (sources.allocSource(sd)) {
1123                     /* Allocation Source*/
1124                     sources.generateSourceAlloc(cr,newobject,sd);
1125                 } else throw new Error("No source for adding to Set");
1126                 cr.outputline(sd.getSafeSymbol()+"_hash->add("+newobject.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1127                 UpdateNode un=munadd.getUpdate(0);
1128                 String name=(String)updatenames.get(un);
1129                 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1130             }
1131             cr.endblock();
1132         }
1133     }
1134
1135     public void generateinclusionrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
1136         InclusionPredicate ip=(InclusionPredicate) dpred.getPredicate();
1137         boolean negated=dpred.isNegated();
1138         MultUpdateNode mun=getmultupdatenode(conj,dpred,-1);
1139         VarDescriptor leftvar=VarDescriptor.makeNew("left");
1140         ip.expr.generate(cr, leftvar);
1141
1142         if (negated) {
1143             if (ip.setexpr instanceof ImageSetExpr) {
1144                 ImageSetExpr ise=(ImageSetExpr) ip.setexpr;
1145                 VarDescriptor rightvar=ise.getVar();
1146                 boolean inverse=ise.inverted();
1147                 RelationDescriptor rd=ise.getRelation();
1148                 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1149                 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1150                 if (inverse) {
1151                     if (usageimage)
1152                         cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1153                     if (usageinvimage)
1154                         cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1155                 } else {
1156                     if (usageimage)
1157                         cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1158                     if (usageinvimage)
1159                         cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1160                 }
1161                 for(int i=0;i<state.vRules.size();i++) {
1162                     Rule r=(Rule)state.vRules.get(i);
1163                     if (r.getInclusion().getTargetDescriptors().contains(rd)) {
1164                         for(int j=0;j<mun.numUpdates();j++) {
1165                             UpdateNode un=mun.getUpdate(i);
1166                             if (un.getRule()==r) {
1167                                 /* Update for rule rule r */
1168                                 String name=(String)updatenames.get(un);
1169                                 if (inverse) {
1170                                     cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
1171                                 } else {
1172                                     cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
1173                                 }
1174                             }
1175                         }
1176                     }
1177                 }
1178             } else {
1179                 SetDescriptor sd=ip.setexpr.sd;
1180                 cr.outputline(sd.getSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1181
1182                 for(int i=0;i<state.vRules.size();i++) {
1183                     Rule r=(Rule)state.vRules.get(i);
1184                     if (r.getInclusion().getTargetDescriptors().contains(sd)) {
1185                         for(int j=0;j<mun.numUpdates();j++) {
1186                             UpdateNode un=mun.getUpdate(i);
1187                             if (un.getRule()==r) {
1188                                 /* Update for rule rule r */
1189                                 String name=(String)updatenames.get(un);
1190                                 cr.outputline(repairtable.getSafeSymbol()+"->addset("+sd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
1191                             }
1192                         }
1193                     }
1194                 }
1195             }
1196         } else {
1197             /* Generate update */
1198             if (ip.setexpr instanceof ImageSetExpr) {
1199                 ImageSetExpr ise=(ImageSetExpr) ip.setexpr;
1200                 VarDescriptor rightvar=ise.getVar();
1201                 boolean inverse=ise.inverted();
1202                 RelationDescriptor rd=ise.getRelation();
1203                 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1204                 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1205                 if (inverse) {
1206                     if (usageimage)
1207                         cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1208                     if (usageinvimage)
1209                         cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1210                 } else {
1211                     if (usageimage)
1212                         cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1213                     if (usageinvimage)
1214                         cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1215                 }
1216                 UpdateNode un=mun.getUpdate(0);
1217                 String name=(String)updatenames.get(un);
1218                 if (inverse) {
1219                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
1220                 } else {
1221                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
1222                 }
1223             } else {
1224                 SetDescriptor sd=ip.setexpr.sd;
1225                 cr.outputline(sd.getSafeSymbol() + "_hash->add((int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1226
1227                 UpdateNode un=mun.getUpdate(0);
1228                 /* Update for rule rule r */
1229                 String name=(String)updatenames.get(un);
1230                 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
1231             }
1232         }
1233     }
1234
1235     public static Vector getrulelist(Descriptor d) {
1236         Vector dispatchrules = new Vector();
1237         Vector rules = State.currentState.vRules;
1238
1239         for (int i = 0; i < rules.size(); i++) {
1240             Rule rule = (Rule) rules.elementAt(i);
1241             Set requiredsymbols = rule.getRequiredDescriptors();
1242
1243             // #TBD#: in general this is wrong because these descriptors may contain descriptors
1244             // bound in "in?" expressions which need to be dealt with in a topologically sorted
1245             // fashion...
1246
1247             if (rule.getRequiredDescriptors().contains(d)) {
1248                 dispatchrules.addElement(rule);
1249             }
1250         }
1251         return dispatchrules;
1252     }
1253
1254     private boolean need_compensation(Rule r) {
1255         if (!Compiler.REPAIR)
1256             return false;
1257         GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
1258         for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
1259             GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
1260             GraphNode gn2=edge.getTarget();
1261             if (!removed.contains(gn2)) {
1262                 TermNode tn2=(TermNode)gn2.getOwner();
1263                 if (tn2.getType()==TermNode.CONSEQUENCE)
1264                     return false;
1265             }
1266         }
1267         return true;
1268     }
1269
1270     private UpdateNode find_compensation(Rule r) {
1271         GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
1272         for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
1273             GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
1274             GraphNode gn2=edge.getTarget();
1275             if (!removed.contains(gn2)) {
1276                 TermNode tn2=(TermNode)gn2.getOwner();
1277                 if (tn2.getType()==TermNode.UPDATE) {
1278                     MultUpdateNode mun=tn2.getUpdate();
1279                     for(int i=0;i<mun.numUpdates();i++) {
1280                         UpdateNode un=mun.getUpdate(i);
1281                         if (un.getRule()==r)
1282                             return un;
1283                     }
1284                 }
1285             }
1286         }
1287         throw new Error("No Compensation Update could be found");
1288     }
1289
1290     public void generate_dispatch(CodeWriter cr, RelationDescriptor rd, String leftvar, String rightvar) {
1291         boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1292         boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1293
1294         if (!(usageinvimage||usageimage)) /* not used at all*/
1295             return;
1296
1297         cr.outputline("// RELATION DISPATCH ");
1298         cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
1299         if (usageimage)
1300             cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hash->contains("+leftvar+","+rightvar+"))");
1301         else
1302             cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hashinv->contains("+rightvar+","+leftvar+"))");
1303         cr.startblock(); {
1304             /* Adding new item */
1305             /* Perform safety checks */
1306             cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
1307             cr.outputline(repairtable.getSafeSymbol()+"->containsrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+"))");
1308             cr.startblock(); {
1309                 /* Have update to call into */
1310                 VarDescriptor mdfyptr=VarDescriptor.makeNew("modifyptr");
1311                 cr.outputline("int "+mdfyptr.getSafeSymbol()+"="+repairtable.getSafeSymbol()+"->getrelation2("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");");
1312
1313                 String parttype="";
1314                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1315                     if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
1316                         parttype=parttype+", int, int";
1317                     else
1318                         parttype=parttype+", int";
1319                 }
1320                 VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
1321                 VarDescriptor tmpptr=VarDescriptor.makeNew("tempupdateptr");
1322
1323                 String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
1324                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1325                     Quantifier q=currentrule.getQuantifier(i);
1326                     if (q instanceof SetQuantifier) {
1327                         SetQuantifier sq=(SetQuantifier) q;
1328                         methodcall+=","+sq.getVar().getSafeSymbol();
1329                     } else if (q instanceof RelationQuantifier) {
1330                         RelationQuantifier rq=(RelationQuantifier) q;
1331                         methodcall+=","+rq.x.getSafeSymbol();
1332                         methodcall+=","+rq.y.getSafeSymbol();
1333                     } else if (q instanceof ForQuantifier) {
1334                         ForQuantifier fq=(ForQuantifier) q;
1335                         methodcall+=","+fq.getVar().getSafeSymbol();
1336                     }
1337                 }
1338
1339
1340
1341                 cr.outputline("void *"+tmpptr.getSafeSymbol()+"=");
1342                 cr.outputline("(void *) "+repairtable.getSafeSymbol()+"->getrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");");
1343                 cr.outputline("if ("+mdfyptr.getSafeSymbol()+")");
1344                 {
1345                     cr.startblock();
1346                     cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+"int,int,int)="+"(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+"int,int,int)) "+tmpptr.getSafeSymbol());
1347                     cr.outputline(methodcall+leftvar+", "+rightvar+", "+mdfyptr.getSafeSymbol() +");");
1348                     cr.endblock();
1349                 }
1350                 cr.outputline("else ");
1351                 {
1352                     cr.startblock();
1353                     cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")="+"(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+tmpptr.getSafeSymbol());
1354                     cr.outputline(methodcall+");");
1355                     cr.endblock();
1356                 }
1357                 cr.outputline("goto rebuild;");
1358             }
1359             cr.endblock();
1360             /* Build standard compensation actions */
1361             if (need_compensation(currentrule)) {
1362                 UpdateNode un=find_compensation(currentrule);
1363                 String name=(String)updatenames.get(un);
1364                 usedupdates.add(un); /* Mark as used */
1365                 String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
1366                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1367                     Quantifier q=currentrule.getQuantifier(i);
1368                     if (q instanceof SetQuantifier) {
1369                         SetQuantifier sq=(SetQuantifier) q;
1370                         methodcall+=","+sq.getVar().getSafeSymbol();
1371                     } else if (q instanceof RelationQuantifier) {
1372                         RelationQuantifier rq=(RelationQuantifier) q;
1373                         methodcall+=","+rq.x.getSafeSymbol();
1374                         methodcall+=","+rq.y.getSafeSymbol();
1375                     } else if (q instanceof ForQuantifier) {
1376                         ForQuantifier fq=(ForQuantifier) q;
1377                         methodcall+=","+fq.getVar().getSafeSymbol();
1378                     }
1379                 }
1380                 methodcall+=");";
1381                 cr.outputline(methodcall);
1382                 cr.outputline("goto rebuild;");
1383             }
1384         }
1385         cr.endblock();
1386
1387         String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
1388         cr.outputline("int " + addeditem + ";");
1389         if (rd.testUsage(RelationDescriptor.IMAGE)) {
1390             cr.outputline(addeditem + " = " + rd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + rightvar+ ");");
1391         }
1392
1393         if (rd.testUsage(RelationDescriptor.INVIMAGE)) {
1394             cr.outputline(addeditem + " = " + rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar + ", (int)" + leftvar + ");");
1395         }
1396
1397
1398
1399         Vector dispatchrules = getrulelist(rd);
1400
1401         Set toremove=new HashSet();
1402         for(int i=0;i<dispatchrules.size();i++) {
1403             Rule r=(Rule)dispatchrules.get(i);
1404             if (!ruleset.contains(r))
1405                 toremove.add(r);
1406         }
1407         dispatchrules.removeAll(toremove);
1408         if (dispatchrules.size() == 0) {
1409             cr.outputline("// nothing to dispatch");
1410             return;
1411         }
1412
1413         cr.outputline("if (" + addeditem + ")");
1414         cr.startblock();
1415
1416         for(int i = 0; i < dispatchrules.size(); i++) {
1417             Rule rule = (Rule) dispatchrules.elementAt(i);
1418             if (rule.getGuardExpr().getRequiredDescriptors().contains(rd)) {
1419                 /* Guard depends on this relation, so we recomput everything */
1420                 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
1421             } else {
1422                 for (int j=0;j<rule.numQuantifiers();j++) {
1423                     Quantifier q=rule.getQuantifier(j);
1424                     if (q.getRequiredDescriptors().contains(rd)) {
1425                         /* Generate add */
1426                         cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+leftvar+","+rightvar+");");
1427                     }
1428                 }
1429             }
1430         }
1431
1432         cr.endblock();
1433     }
1434
1435
1436     public void generate_dispatch(CodeWriter cr, SetDescriptor sd, String setvar) {
1437
1438         cr.outputline("// SET DISPATCH ");
1439
1440         cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
1441         cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+sd.getJustSafeSymbol()+"_hash->contains("+setvar+"))");
1442         cr.startblock(); {
1443             /* Adding new item */
1444             /* Perform safety checks */
1445             cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
1446             cr.outputline(repairtable.getSafeSymbol()+"->containsset("+sd.getNum()+","+currentrule.getNum()+","+setvar+"))");
1447             cr.startblock(); {
1448                 /* Have update to call into */
1449                 VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
1450                 String parttype="";
1451                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1452                     if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
1453                         parttype=parttype+", int, int";
1454                     else
1455                         parttype=parttype+", int";
1456                 }
1457                 cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")=");
1458                 cr.outputline("(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+repairtable.getSafeSymbol()+"->getset("+sd.getNum()+","+currentrule.getNum()+","+setvar+");");
1459                 String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+
1460                               repairtable.getSafeSymbol();
1461                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1462                     Quantifier q=currentrule.getQuantifier(i);
1463                     if (q instanceof SetQuantifier) {
1464                         SetQuantifier sq=(SetQuantifier) q;
1465                         methodcall+=","+sq.getVar().getSafeSymbol();
1466                     } else if (q instanceof RelationQuantifier) {
1467                         RelationQuantifier rq=(RelationQuantifier) q;
1468                         methodcall+=","+rq.x.getSafeSymbol();
1469                         methodcall+=","+rq.y.getSafeSymbol();
1470                     } else if (q instanceof ForQuantifier) {
1471                         ForQuantifier fq=(ForQuantifier) q;
1472                         methodcall+=","+fq.getVar().getSafeSymbol();
1473                     }
1474                 }
1475                 methodcall+=");";
1476                 cr.outputline(methodcall);
1477                 cr.outputline("goto rebuild;");
1478             }
1479             cr.endblock();
1480             /* Build standard compensation actions */
1481             if (need_compensation(currentrule)) {
1482                 UpdateNode un=find_compensation(currentrule);
1483                 String name=(String)updatenames.get(un);
1484                 usedupdates.add(un); /* Mark as used */
1485
1486                 String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+
1487                               repairtable.getSafeSymbol();
1488                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1489                     Quantifier q=currentrule.getQuantifier(i);
1490                     if (q instanceof SetQuantifier) {
1491                         SetQuantifier sq=(SetQuantifier) q;
1492                         methodcall+=","+sq.getVar().getSafeSymbol();
1493                     } else if (q instanceof RelationQuantifier) {
1494                         RelationQuantifier rq=(RelationQuantifier) q;
1495                         methodcall+=","+rq.x.getSafeSymbol();
1496                         methodcall+=","+rq.y.getSafeSymbol();
1497                     } else if (q instanceof ForQuantifier) {
1498                         ForQuantifier fq=(ForQuantifier) q;
1499                         methodcall+=","+fq.getVar().getSafeSymbol();
1500                     }
1501                 }
1502                 methodcall+=");";
1503                 cr.outputline(methodcall);
1504                 cr.outputline("goto rebuild;");
1505             }
1506         }
1507         cr.endblock();
1508
1509         String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
1510         cr.outputline("int " + addeditem + " = 1;");
1511         cr.outputline(addeditem + " = " + sd.getSafeSymbol() + "_hash->add((int)" + setvar +  ", (int)" + setvar + ");");
1512         cr.startblock();
1513         Vector dispatchrules = getrulelist(sd);
1514
1515         Set toremove=new HashSet();
1516         for(int i=0;i<dispatchrules.size();i++) {
1517             Rule r=(Rule)dispatchrules.get(i);
1518             if (!ruleset.contains(r))
1519                 toremove.add(r);
1520         }
1521         dispatchrules.removeAll(toremove);
1522
1523         if (dispatchrules.size() == 0) {
1524             cr.outputline("// nothing to dispatch");
1525             cr.endblock();
1526             return;
1527         }
1528         cr.outputline("if ("+addeditem+")");
1529         cr.startblock();
1530         for(int i = 0; i < dispatchrules.size(); i++) {
1531             Rule rule = (Rule) dispatchrules.elementAt(i);
1532             if (SetDescriptor.expand(rule.getGuardExpr().getRequiredDescriptors()).contains(sd)) {
1533                 /* Guard depends on this relation, so we recompute everything */
1534                 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
1535             } else {
1536                 for (int j=0;j<rule.numQuantifiers();j++) {
1537                     Quantifier q=rule.getQuantifier(j);
1538                     if (SetDescriptor.expand(q.getRequiredDescriptors()).contains(sd)) {
1539                         /* Generate add */
1540                         cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+setvar+",0);");
1541                     }
1542                 }
1543             }
1544         }
1545
1546         cr.endblock();
1547         cr.endblock();
1548     }
1549 }