7 public class RepairGenerator {
9 java.io.PrintWriter outputrepair = null;
10 java.io.PrintWriter outputaux = null;
11 java.io.PrintWriter outputhead = null;
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;
22 Termination termination;
25 static boolean DEBUG=false;
29 public RepairGenerator(State state, Termination t) {
31 updatenames=new Hashtable();
32 usedupdates=new HashSet();
35 togenerate=new HashSet();
36 togenerate.addAll(termination.conjunctions);
37 togenerate.removeAll(removed);
38 GraphNode.computeclosure(togenerate,removed);
41 sources=new Sources(state);
42 Repair.repairgenerator=this;
45 private void name_updates() {
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);
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);
67 generate_tokentable();
68 generate_hashtables();
69 generate_stateobject();
75 CodeWriter crhead = new StandardCodeWriter(this.outputhead);
76 CodeWriter craux = new StandardCodeWriter(this.outputaux);
77 crhead.outputline("};");
78 craux.outputline("}");
82 private void generate_updates() {
84 CodeWriter crhead = new StandardCodeWriter(outputhead);
85 CodeWriter craux = new StandardCodeWriter(outputaux);
88 String repairtable="repairtable";
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());
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);
109 case MultUpdateNode.ADD:
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+")");
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+")");
118 final SymbolTable st = un.getRule().getSymbolTable();
119 CodeWriter cr = new StandardCodeWriter(outputaux) {
120 public SymbolTable getSymbolTable() { return st; }
122 un.generate(cr, false, left,right);
125 case MultUpdateNode.REMOVE:
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;
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();
144 crhead.outputline(methodcall+";");
145 craux.outputline(methodcall);
147 final SymbolTable st2 = un.getRule().getSymbolTable();
148 CodeWriter cr2 = new StandardCodeWriter(outputaux) {
149 public SymbolTable getSymbolTable() { return st2; }
151 un.generate(cr2, true, null,null);
154 case MultUpdateNode.MODIFY:
156 throw new Error("Nonimplement Update");
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()+";");
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()+";");
178 cr.outputline("delete "+vdstate.getSafeSymbol()+";");
181 private void generate_tokentable() {
182 CodeWriter cr = new StandardCodeWriter(outputrepair);
183 Iterator tokens = TokenLiteralExpr.tokens.keySet().iterator();
186 cr.outputline("// Token values");
189 while (tokens.hasNext()) {
190 Object token = tokens.next();
191 cr.outputline("// " + token.toString() + " = " + TokenLiteralExpr.tokens.get(token).toString());
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()+";");
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+"\"");
221 craux.outputline(name+"::"+name+"() {");
222 craux.outputline("// creating hashtables ");
225 Iterator sets = state.stSets.descriptors();
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();");
234 /* second pass build relationships between hashtables */
235 sets = state.stSets.descriptors();
237 while (sets.hasNext()) {
238 SetDescriptor set = (SetDescriptor) sets.next();
239 Iterator subsets = set.subsets();
241 while (subsets.hasNext()) {
242 SetDescriptor subset = (SetDescriptor) subsets.next();
243 craux.outputline(subset.getSafeSymbol() + "_hash->addParent(" + set.getSafeSymbol() + "_hash);");
247 /* build relations */
248 Iterator relations = state.stRelations.descriptors();
250 /* first pass create all the hash tables */
251 while (relations.hasNext()) {
252 RelationDescriptor relation = (RelationDescriptor) relations.next();
254 if (relation.testUsage(RelationDescriptor.IMAGE)) {
255 crhead.outputline("SimpleHash* " + relation.getSafeSymbol() + "_hash;");
256 craux.outputline(relation.getSafeSymbol() + "_hash = new SimpleHash();");
259 if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
260 crhead.outputline("SimpleHash* " + relation.getSafeSymbol() + "_hashinv;");
261 craux.outputline(relation.getSafeSymbol() + "_hashinv = new SimpleHash();");
265 craux.outputline("}");
266 crhead.outputline("};");
267 craux.outputline(name+"::~"+name+"() {");
268 craux.outputline("// deleting hashtables");
270 /* build destructor */
271 sets = state.stSets.descriptors();
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;");
279 /* destroy relations */
280 relations = state.stRelations.descriptors();
282 /* first pass create all the hash tables */
283 while (relations.hasNext()) {
284 RelationDescriptor relation = (RelationDescriptor) relations.next();
286 if (relation.testUsage(RelationDescriptor.IMAGE)) {
287 craux.outputline("delete "+relation.getSafeSymbol() + "_hash;");
290 if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
291 craux.outputline("delete " + relation.getSafeSymbol() + ";");
294 craux.outputline("}");
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()");
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)");
313 craux.outputline("int "+goodflag.getSafeSymbol()+"=1;");
314 craux.outputline(name+ " * "+newmodel.getSafeSymbol()+"=new "+name+"();");
317 private void generate_teardown() {
318 CodeWriter cr = new StandardCodeWriter(outputaux);
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()+"->";
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!
340 noquantifiers = false;
345 emptyrules.add(rule);
347 worklistrules.add(rule);
351 Iterator iterator_er = emptyrules.iterator();
352 while (iterator_er.hasNext()) {
353 Rule rule = (Rule) iterator_er.next();
355 final SymbolTable st = rule.getSymbolTable();
356 CodeWriter cr = new StandardCodeWriter(outputaux) {
357 public SymbolTable getSymbolTable() { return st; }
359 cr.outputline("// build " +escape(rule.toString()));
361 ListIterator quantifiers = rule.quantifiers();
362 while (quantifiers.hasNext()) {
363 Quantifier quantifier = (Quantifier) quantifiers.next();
364 quantifier.generate_open(cr);
369 rule.getGuardExpr().prettyPrint(cr);
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() + ")");
378 /* now we have to generate the inclusion code */
380 rule.getInclusion().generate(cr);
382 while (quantifiers.hasPrevious()) {
383 Quantifier quantifier = (Quantifier) quantifiers.previous();
392 CodeWriter cr2 = new StandardCodeWriter(outputaux);
394 cr2.outputline("while ("+goodflag.getSafeSymbol()+"&&"+worklist.getSafeSymbol()+"->hasMoreElements())");
396 VarDescriptor idvar=VarDescriptor.makeNew("id");
397 cr2.outputline("int "+idvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getid();");
399 String elseladder = "if";
401 Iterator iterator_rules = worklistrules.iterator();
402 while (iterator_rules.hasNext()) {
404 Rule rule = (Rule) iterator_rules.next();
405 int dispatchid = rule.getNum();
408 final SymbolTable st = rule.getSymbolTable();
409 CodeWriter cr = new StandardCodeWriter(outputaux) {
410 public SymbolTable getSymbolTable() { return st; }
414 cr.outputline(elseladder + " ("+idvar.getSafeSymbol()+" == " + dispatchid + ")");
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()));
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());
433 rule.getGuardExpr().prettyPrint(cr);
436 /* now we have to generate the guard test */
438 VarDescriptor guardval = VarDescriptor.makeNew();
439 rule.getGuardExpr().generate(cr, guardval);
441 cr.outputline("if (" + guardval.getSafeSymbol() + ")");
444 /* now we have to generate the inclusion code */
446 rule.getInclusion().generate(cr);
449 for (int j=0;j<rule.numQuantifiers();j++) {
453 // close startblocks generated by DotExpr memory checks
454 //DotExpr.generate_memory_endblocks(cr);
456 cr.endblock(); // end else-if WORKLIST ladder
458 elseladder = "else if";
462 cr2.outputline("else");
464 cr2.outputline("printf(\"VERY BAD !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\\n\\n\");");
465 cr2.outputline("exit(1);");
467 // end block created for worklist
468 cr2.outputline(worklist.getSafeSymbol()+"->pop();");
472 public static String escape(String s) {
474 for(int i=0;i<s.length();i++) {
484 private void generate_checks() {
486 /* do constraint checks */
487 Vector constraints = state.vConstraints;
489 for (int i = 0; i < constraints.size(); i++) {
491 Constraint constraint = (Constraint) constraints.elementAt(i);
495 final SymbolTable st = constraint.getSymbolTable();
497 CodeWriter cr = new StandardCodeWriter(outputaux) {
498 public SymbolTable getSymbolTable() { return st; }
501 cr.outputline("// checking " + escape(constraint.toString()));
504 ListIterator quantifiers = constraint.quantifiers();
506 while (quantifiers.hasNext()) {
507 Quantifier quantifier = (Quantifier) quantifiers.next();
508 quantifier.generate_open(cr);
511 cr.outputline("int maybe = 0;");
513 /* now we have to generate the guard test */
515 VarDescriptor constraintboolean = VarDescriptor.makeNew("constraintboolean");
516 constraint.getLogicStatement().generate(cr, constraintboolean);
518 cr.outputline("if (maybe)");
520 cr.outputline("printf(\"maybe fail " + escape(constraint.toString()) + ". \");");
521 cr.outputline("exit(1);");
524 cr.outputline("else if (!" + constraintboolean.getSafeSymbol() + ")");
527 cr.outputline("printf(\"fail " + escape(constraint.toString()) + ". \");");
530 /* Build new repair table */
531 cr.outputline("if ("+repairtable.getSafeSymbol()+")");
532 cr.outputline("delete "+repairtable.getSafeSymbol()+";");
533 cr.outputline(repairtable.getSafeSymbol()+"=new RepairHash();");
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;");
543 if (dnfconst.size()>1) {
544 cr.outputline("int "+mincostindex.getSafeSymbol()+";");
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))
552 VarDescriptor costvar;
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);
564 cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
566 cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
568 cr.outputline("int "+costvar.getSafeSymbol()+"="+cost.getCost(dpred)+";");
570 cr.outputline(costvar.getSafeSymbol()+"+="+cost.getCost(dpred)+";");
574 cr.outputline("if ("+costvar.getSafeSymbol()+"<"+mincost.getSafeSymbol()+")");
576 cr.outputline(mincost.getSafeSymbol()+"="+costvar.getSafeSymbol()+";");
577 cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
580 cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
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))
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);
597 cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
599 cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
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");
614 cr.outputline("break;");
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 */
626 while (quantifiers.hasPrevious()) {
627 Quantifier quantifier = (Quantifier) quantifiers.previous();
630 cr.outputline("if ("+goodflag.getSafeSymbol()+")");
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;");
640 cr.outputline("rebuild:");
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) {
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");
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()+");");
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()+");");
701 if (opcode==Opcode.GT) {
703 } else if (opcode==Opcode.GE) {
705 } else if (opcode==Opcode.LT) {
707 } else if (opcode==Opcode.LE) {
709 } else if (opcode==Opcode.EQ) {
711 } else if (opcode==Opcode.NE) {
714 throw new Error("Unrecognized Opcode");
717 if (opcode==Opcode.GT) {
718 cr.outputline(newvalue.getSafeSymbol()+"++;");
719 } else if (opcode==Opcode.GE) {
721 } else if (opcode==Opcode.LT) {
722 cr.outputline(newvalue.getSafeSymbol()+"--;");
723 } else if (opcode==Opcode.LE) {
725 } else if (opcode==Opcode.EQ) {
727 } else if (opcode==Opcode.NE) {
728 cr.outputline(newvalue.getSafeSymbol()+"++;");
730 throw new Error("Unrecognized Opcode");
732 /* Do abstract repairs */
734 cr.outputline(rd.getSafeSymbol()+"_hash->remove("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
736 cr.outputline(rd.getSafeSymbol()+"_hash->add("+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
738 cr.outputline(rd.getSafeSymbol()+"_hash->add("+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
742 cr.outputline(rd.getSafeSymbol()+"_hashinv->remove("+rightside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
744 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+newvalue.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
746 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+rightside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
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+");");
764 /* Now do addition */
765 UpdateNode un=munadd.getUpdate(0);
766 String name=(String)updatenames.get(un);
768 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
770 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
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();
779 boolean negated=dpred.isNegated();
781 if (opcode==Opcode.GT) {
783 } else if (opcode==Opcode.GE) {
785 } else if (opcode==Opcode.LT) {
787 } else if (opcode==Opcode.LE) {
789 } else if (opcode==Opcode.EQ) {
791 } else if (opcode==Opcode.NE) {
794 throw new Error("Unrecognized Opcode");
797 MultUpdateNode munremove;
799 MultUpdateNode munadd;
800 if (ep.getDescriptor() instanceof RelationDescriptor) {
801 munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
802 munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
804 munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMSET);
805 munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTOSET);
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()+";");
817 generateremove=false;
818 } else if (opcode==Opcode.GE) {
819 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
821 generateremove=false;
822 } else if (opcode==Opcode.LT) {
823 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size-1)+"-"+sizevar.getSafeSymbol()+";");
826 } else if (opcode==Opcode.LE) {
827 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
830 } else if (opcode==Opcode.EQ) {
831 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
834 } else if (opcode==Opcode.NE) {
835 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
837 generateremove=false;
839 throw new Error("Unrecognized Opcode");
841 Descriptor d=ep.getDescriptor();
842 if (generateremove) {
843 cr.outputline("for(;"+change.getSafeSymbol()+"<0;"+change.getSafeSymbol()+"++)");
845 /* Find element to remove */
846 VarDescriptor leftvar=VarDescriptor.makeNew("leftvar");
847 VarDescriptor rightvar=VarDescriptor.makeNew("rightvar");
848 if (d instanceof RelationDescriptor) {
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()+");");
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()+");");
859 cr.outputline("int "+leftvar.getSafeSymbol()+"="+d.getSafeSymbol()+"_hash->firstkey();");
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);
867 cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + rightvar + ");");
869 cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar + ", (int)" + leftvar + ");");
871 cr.outputline(d.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + leftvar + ");");
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+");");
885 cr.outputline(repairtable.getSafeSymbol()+"->addset("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
895 cr.outputline("for(;"+change.getSafeSymbol()+">0;"+change.getSafeSymbol()+"--)");
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())) {
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();)");
909 cr.outputline("if !"+rd.getSafeSymbol()+"_hashinv->contains("+iterator.getSafeSymbol()+"->key(),"+otherside.getSafeSymbol()+")");
911 cr.outputline("if !"+rd.getSafeSymbol()+"_hash->contains("+otherside.getSafeSymbol()+","+iterator.getSafeSymbol()+"->key())");
913 cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();");
914 cr.outputline(iterator.getSafeSymbol()+"->next();");
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");
921 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
922 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
924 cr.outputline(rd.getSafeSymbol()+"_hash->add("+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
926 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
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()+");");
932 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
933 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
935 cr.outputline(rd.getSafeSymbol()+"_hash->add("+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
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()+");");
943 SetDescriptor sd=(SetDescriptor)d;
944 if (sources.setSource(sd)) {
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();)");
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();");
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()+");");
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);
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);
986 cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + rightvar + ", (int)" + leftvar + ");");
988 cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + leftvar + ", (int)" + rightvar + ");");
991 cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + rightvar + ");");
993 cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar + ", (int)" + leftvar + ");");
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);
1004 cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
1006 cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
1013 SetDescriptor sd=ip.setexpr.sd;
1014 cr.outputline(sd.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + leftvar + ");");
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+");");
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);
1041 cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + rightvar + ", (int)" + leftvar + ");");
1043 cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + leftvar + ", (int)" + rightvar + ");");
1046 cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + rightvar + ");");
1048 cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar + ", (int)" + leftvar + ");");
1050 UpdateNode un=mun.getUpdate(0);
1051 String name=(String)updatenames.get(un);
1053 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
1055 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
1058 SetDescriptor sd=ip.setexpr.sd;
1059 cr.outputline(sd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + leftvar + ");");
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()+");");
1071 public static Vector getrulelist(Descriptor d) {
1072 Vector dispatchrules = new Vector();
1073 Vector rules = State.currentState.vRules;
1075 for (int i = 0; i < rules.size(); i++) {
1076 Rule rule = (Rule) rules.elementAt(i);
1077 Set requiredsymbols = rule.getRequiredDescriptors();
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
1083 if (rule.getRequiredDescriptors().contains(d)) {
1084 dispatchrules.addElement(rule);
1087 return dispatchrules;
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)
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)
1121 throw new Error("No Compensation Update could be found");
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);
1128 if (!(usageinvimage||usageimage)) /* not used at all*/
1131 cr.outputline("// RELATION DISPATCH ");
1132 cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
1134 cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hash->contains("+leftvar+","+rightvar+"))");
1136 cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hashinv->contains("+rightvar+","+leftvar+"))");
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+"))");
1143 /* Have update to call into */
1144 VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
1146 for(int i=0;i<currentrule.numQuantifiers();i++) {
1147 if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
1148 parttype=parttype+", int, int";
1150 parttype=parttype+", int";
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();
1170 cr.outputline(methodcall);
1171 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1172 cr.outputline("continue;");
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();
1196 cr.outputline(methodcall);
1197 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1198 cr.outputline("continue;");
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 + ");");
1209 if (rd.testUsage(RelationDescriptor.INVIMAGE)) {
1210 cr.outputline(addeditem + " = " + rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar + ", (int)" + leftvar + ");");
1213 cr.outputline("if (" + addeditem + ")");
1216 Vector dispatchrules = getrulelist(rd);
1218 if (dispatchrules.size() == 0) {
1219 cr.outputline("// nothing to dispatch");
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);");
1230 for (int j=0;j<rule.numQuantifiers();j++) {
1231 Quantifier q=rule.getQuantifier(j);
1232 if (q.getRequiredDescriptors().contains(rd)) {
1234 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+leftvar+","+rightvar+");");
1243 public void generate_dispatch(CodeWriter cr, SetDescriptor sd, String setvar) {
1245 cr.outputline("// SET DISPATCH ");
1247 cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
1248 cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+sd.getJustSafeSymbol()+"_hash->contains("+setvar+"))");
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+"))");
1255 /* Have update to call into */
1256 VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
1258 for(int i=0;i<currentrule.numQuantifiers();i++) {
1259 if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
1260 parttype=parttype+", int, int";
1262 parttype=parttype+", int";
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();
1283 cr.outputline(methodcall);
1284 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1285 cr.outputline("continue;");
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 */
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();
1311 cr.outputline(methodcall);
1312 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1313 cr.outputline("continue;");
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 + ");");
1322 Vector dispatchrules = getrulelist(sd);
1324 if (dispatchrules.size() == 0) {
1325 cr.outputline("// nothing to dispatch");
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);");
1336 for (int j=0;j<rule.numQuantifiers();j++) {
1337 Quantifier q=rule.getQuantifier(j);
1338 if (SetDescriptor.expand(q.getRequiredDescriptors()).contains(sd)) {
1340 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+setvar+",0);");