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