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