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