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