Repair/RepairCompiler/MCC/IR/RepairGenerator.java

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