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