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