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);
319 cr.outputline("if ("+repairtable.getSafeSymbol()+")");
320 cr.outputline("delete "+repairtable.getSafeSymbol()+";");
321 cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
322 cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
323 cr.outputline("delete "+newmodel.getSafeSymbol()+";");
324 cr.outputline("delete "+worklist.getSafeSymbol()+";");
328 private void generate_rules() {
329 /* first we must sort the rules */
330 Iterator allrules = state.vRules.iterator();
331 Vector emptyrules = new Vector(); // rules with no quantifiers
332 Vector worklistrules = new Vector(); // the rest of the rules
333 RelationDescriptor.prefix = newmodel.getSafeSymbol()+"->";
334 SetDescriptor.prefix = newmodel.getSafeSymbol()+"->";
336 while (allrules.hasNext()) {
337 Rule rule = (Rule) allrules.next();
338 ListIterator quantifiers = rule.quantifiers();
339 boolean noquantifiers = true;
340 while (quantifiers.hasNext()) {
341 Quantifier quantifier = (Quantifier) quantifiers.next();
342 if (quantifier instanceof ForQuantifier) {
343 // ok, because integers exist already!
346 noquantifiers = false;
351 emptyrules.add(rule);
353 worklistrules.add(rule);
357 Iterator iterator_er = emptyrules.iterator();
358 while (iterator_er.hasNext()) {
359 Rule rule = (Rule) iterator_er.next();
361 final SymbolTable st = rule.getSymbolTable();
362 CodeWriter cr = new StandardCodeWriter(outputaux) {
363 public SymbolTable getSymbolTable() { return st; }
365 cr.outputline("// build " +escape(rule.toString()));
367 ListIterator quantifiers = rule.quantifiers();
368 while (quantifiers.hasNext()) {
369 Quantifier quantifier = (Quantifier) quantifiers.next();
370 quantifier.generate_open(cr);
375 rule.getGuardExpr().prettyPrint(cr);
378 /* now we have to generate the guard test */
379 VarDescriptor guardval = VarDescriptor.makeNew();
380 rule.getGuardExpr().generate(cr, guardval);
381 cr.outputline("if (" + guardval.getSafeSymbol() + ")");
384 /* now we have to generate the inclusion code */
386 rule.getInclusion().generate(cr);
388 while (quantifiers.hasPrevious()) {
389 Quantifier quantifier = (Quantifier) quantifiers.previous();
398 CodeWriter cr2 = new StandardCodeWriter(outputaux);
400 cr2.outputline("while ("+goodflag.getSafeSymbol()+"&&"+worklist.getSafeSymbol()+"->hasMoreElements())");
402 VarDescriptor idvar=VarDescriptor.makeNew("id");
403 cr2.outputline("int "+idvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getid();");
405 String elseladder = "if";
407 Iterator iterator_rules = worklistrules.iterator();
408 while (iterator_rules.hasNext()) {
410 Rule rule = (Rule) iterator_rules.next();
411 int dispatchid = rule.getNum();
414 final SymbolTable st = rule.getSymbolTable();
415 CodeWriter cr = new StandardCodeWriter(outputaux) {
416 public SymbolTable getSymbolTable() { return st; }
420 cr.outputline(elseladder + " ("+idvar.getSafeSymbol()+" == " + dispatchid + ")");
422 VarDescriptor typevar=VarDescriptor.makeNew("type");
423 VarDescriptor leftvar=VarDescriptor.makeNew("left");
424 VarDescriptor rightvar=VarDescriptor.makeNew("right");
425 cr.outputline("int "+typevar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->gettype();");
426 cr.outputline("int "+leftvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getlvalue();");
427 cr.outputline("int "+rightvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getrvalue();");
428 cr.outputline("// build " +escape(rule.toString()));
431 for (int j=0;j<rule.numQuantifiers();j++) {
432 Quantifier quantifier = rule.getQuantifier(j);
433 quantifier.generate_open(cr, typevar.getSafeSymbol(),j,leftvar.getSafeSymbol(),rightvar.getSafeSymbol());
439 rule.getGuardExpr().prettyPrint(cr);
442 /* now we have to generate the guard test */
444 VarDescriptor guardval = VarDescriptor.makeNew();
445 rule.getGuardExpr().generate(cr, guardval);
447 cr.outputline("if (" + guardval.getSafeSymbol() + ")");
450 /* now we have to generate the inclusion code */
452 rule.getInclusion().generate(cr);
455 for (int j=0;j<rule.numQuantifiers();j++) {
459 // close startblocks generated by DotExpr memory checks
460 //DotExpr.generate_memory_endblocks(cr);
462 cr.endblock(); // end else-if WORKLIST ladder
464 elseladder = "else if";
468 cr2.outputline("else");
470 cr2.outputline("printf(\"VERY BAD !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\\n\\n\");");
471 cr2.outputline("exit(1);");
473 // end block created for worklist
477 public static String escape(String s) {
479 for(int i=0;i<s.length();i++) {
489 private void generate_checks() {
491 /* do constraint checks */
492 Vector constraints = state.vConstraints;
494 for (int i = 0; i < constraints.size(); i++) {
496 Constraint constraint = (Constraint) constraints.elementAt(i);
500 final SymbolTable st = constraint.getSymbolTable();
502 CodeWriter cr = new StandardCodeWriter(outputaux) {
503 public SymbolTable getSymbolTable() { return st; }
506 cr.outputline("// checking " + escape(constraint.toString()));
509 ListIterator quantifiers = constraint.quantifiers();
511 while (quantifiers.hasNext()) {
512 Quantifier quantifier = (Quantifier) quantifiers.next();
513 quantifier.generate_open(cr);
516 cr.outputline("int maybe = 0;");
518 /* now we have to generate the guard test */
520 VarDescriptor constraintboolean = VarDescriptor.makeNew("constraintboolean");
521 constraint.getLogicStatement().generate(cr, constraintboolean);
523 cr.outputline("if (maybe)");
525 cr.outputline("printf(\"maybe fail " + escape(constraint.toString()) + ". \");");
526 cr.outputline("exit(1);");
529 cr.outputline("else if (!" + constraintboolean.getSafeSymbol() + ")");
532 cr.outputline("printf(\"fail " + escape(constraint.toString()) + ". \");");
535 /* Build new repair table */
536 cr.outputline("if ("+repairtable.getSafeSymbol()+")");
537 cr.outputline("delete "+repairtable.getSafeSymbol()+";");
538 cr.outputline(repairtable.getSafeSymbol()+"=new RepairHash();");
541 /* Compute cost of each repair */
542 VarDescriptor mincost=VarDescriptor.makeNew("mincost");
543 VarDescriptor mincostindex=VarDescriptor.makeNew("mincostindex");
544 DNFConstraint dnfconst=constraint.dnfconstraint;
545 cr.outputline("int "+mincostindex.getSafeSymbol()+";");
546 if (dnfconst.size()>1) {
548 for(int j=0;j<dnfconst.size();j++) {
549 Conjunction conj=dnfconst.get(j);
550 GraphNode gn=(GraphNode)termination.conjtonodemap.get(conj);
551 if (removed.contains(gn))
554 VarDescriptor costvar;
558 costvar=VarDescriptor.makeNew("cost");
559 for(int k=0;k<conj.size();k++) {
560 DNFPredicate dpred=conj.get(k);
561 Predicate p=dpred.getPredicate();
562 boolean negate=dpred.isNegated();
563 VarDescriptor predvalue=VarDescriptor.makeNew("Predicatevalue");
564 p.generate(cr,predvalue);
566 cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
568 cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
570 cr.outputline("int "+costvar.getSafeSymbol()+"="+cost.getCost(dpred)+";");
572 cr.outputline(costvar.getSafeSymbol()+"+="+cost.getCost(dpred)+";");
576 cr.outputline("if ("+costvar.getSafeSymbol()+"<"+mincost.getSafeSymbol()+")");
578 cr.outputline(mincost.getSafeSymbol()+"="+costvar.getSafeSymbol()+";");
579 cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
582 cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
586 cr.outputline("switch("+mincostindex.getSafeSymbol()+") {");
587 for(int j=0;j<dnfconst.size();j++) {
588 Conjunction conj=dnfconst.get(j);
589 GraphNode gn=(GraphNode)termination.conjtonodemap.get(conj); if (removed.contains(gn))
591 cr.outputline("case "+j+":");
592 for(int k=0;k<conj.size();k++) {
593 DNFPredicate dpred=conj.get(k);
594 Predicate p=dpred.getPredicate();
595 boolean negate=dpred.isNegated();
596 VarDescriptor predvalue=VarDescriptor.makeNew("Predicatevalue");
597 p.generate(cr,predvalue);
599 cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
601 cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
603 if (p instanceof InclusionPredicate)
604 generateinclusionrepair(conj,dpred, cr);
605 else if (p instanceof ExprPredicate) {
606 ExprPredicate ep=(ExprPredicate)p;
607 if (ep.getType()==ExprPredicate.SIZE)
608 generatesizerepair(conj,dpred,cr);
609 else if (ep.getType()==ExprPredicate.COMPARISON)
610 generatecomparisonrepair(conj,dpred,cr);
611 } else throw new Error("Unrecognized Predicate");
616 cr.outputline("break;");
620 cr.outputline(goodflag.getSafeSymbol()+"=0;");
621 cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
622 cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
623 cr.outputline(oldmodel.getSafeSymbol()+"="+newmodel.getSafeSymbol()+";");
624 cr.outputline("break;"); /* Rebuild model and all */
628 while (quantifiers.hasPrevious()) {
629 Quantifier quantifier = (Quantifier) quantifiers.previous();
632 cr.outputline("if ("+goodflag.getSafeSymbol()+")");
633 cr.outputline("break;");
641 private MultUpdateNode getmultupdatenode(Conjunction conj, DNFPredicate dpred, int repairtype) {
642 MultUpdateNode mun=null;
643 GraphNode gn=(GraphNode) termination.conjtonodemap.get(conj);
644 for(Iterator edgeit=gn.edges();(mun==null)&&edgeit.hasNext();) {
645 GraphNode gn2=((GraphNode.Edge) edgeit.next()).getTarget();
646 TermNode tn2=(TermNode)gn2.getOwner();
647 if (tn2.getType()==TermNode.ABSTRACT) {
648 AbstractRepair ar=tn2.getAbstract();
649 if (((repairtype==-1)||(ar.getType()==repairtype))&&
650 ar.getPredicate()==dpred) {
651 for(Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
652 GraphNode gn3=((GraphNode.Edge) edgeit2.next()).getTarget();
653 if (!removed.contains(gn3)) {
654 TermNode tn3=(TermNode)gn3.getOwner();
655 if (tn3.getType()==TermNode.UPDATE) {
667 public void generatecomparisonrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
668 MultUpdateNode munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
669 MultUpdateNode munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
670 ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
671 RelationDescriptor rd=(RelationDescriptor)ep.getDescriptor();
672 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
673 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
674 boolean inverted=ep.inverted();
675 boolean negated=dpred.isNegated();
676 OpExpr expr=(OpExpr)ep.expr;
677 Opcode opcode=expr.getOpcode();
678 VarDescriptor leftside=VarDescriptor.makeNew("leftside");
679 VarDescriptor rightside=VarDescriptor.makeNew("rightside");
680 VarDescriptor newvalue=VarDescriptor.makeNew("newvalue");
682 expr.getLeftExpr().generate(cr,leftside);
683 expr.getRightExpr().generate(cr,newvalue);
684 cr.outputline(rd.getRange().getType().getGenerateType().getSafeSymbol()+" "+rightside.getSafeSymbol()+";");
685 cr.outputline(rd.getSafeSymbol()+"_hash->get("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
687 expr.getLeftExpr().generate(cr,rightside);
688 expr.getRightExpr().generate(cr,newvalue);
689 cr.outputline(rd.getDomain().getType().getGenerateType().getSafeSymbol()+" "+leftside.getSafeSymbol()+";");
690 cr.outputline(rd.getSafeSymbol()+"_hashinv->get("+leftside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
693 if (opcode==Opcode.GT) {
695 } else if (opcode==Opcode.GE) {
697 } else if (opcode==Opcode.LT) {
699 } else if (opcode==Opcode.LE) {
701 } else if (opcode==Opcode.EQ) {
703 } else if (opcode==Opcode.NE) {
706 throw new Error("Unrecognized Opcode");
709 if (opcode==Opcode.GT) {
710 cr.outputline(newvalue.getSafeSymbol()+"++;");
711 } else if (opcode==Opcode.GE) {
713 } else if (opcode==Opcode.LT) {
714 cr.outputline(newvalue.getSafeSymbol()+"--;");
715 } else if (opcode==Opcode.LE) {
717 } else if (opcode==Opcode.EQ) {
719 } else if (opcode==Opcode.NE) {
720 cr.outputline(newvalue.getSafeSymbol()+"++;");
722 throw new Error("Unrecognized Opcode");
724 /* Do abstract repairs */
726 cr.outputline(rd.getSafeSymbol()+"_hash->remove("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
728 cr.outputline(rd.getSafeSymbol()+"_hash->add("+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
730 cr.outputline(rd.getSafeSymbol()+"_hash->add("+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
734 cr.outputline(rd.getSafeSymbol()+"_hashinv->remove("+rightside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
736 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+newvalue.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
738 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+rightside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
741 /* Do concrete repairs */
742 /* Start with scheduling removal */
743 for(int i=0;i<state.vRules.size();i++) {
744 Rule r=(Rule)state.vRules.get(i);
745 if (r.getInclusion().getTargetDescriptors().contains(rd)) {
746 for(int j=0;j<munremove.numUpdates();j++) {
747 UpdateNode un=munremove.getUpdate(i);
748 if (un.getRule()==r) {
749 /* Update for rule r */
750 String name=(String)updatenames.get(un);
751 cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+",(int) &"+name+");");
756 /* Now do addition */
757 UpdateNode un=munadd.getUpdate(0);
758 String name=(String)updatenames.get(un);
760 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
762 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
766 public void generatesizerepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr) {
767 ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
768 OpExpr expr=(OpExpr)ep.expr;
769 Opcode opcode=expr.getOpcode();
771 boolean negated=dpred.isNegated();
773 if (opcode==Opcode.GT) {
775 } else if (opcode==Opcode.GE) {
777 } else if (opcode==Opcode.LT) {
779 } else if (opcode==Opcode.LE) {
781 } else if (opcode==Opcode.EQ) {
783 } else if (opcode==Opcode.NE) {
786 throw new Error("Unrecognized Opcode");
789 MultUpdateNode munremove;
791 MultUpdateNode munadd;
792 if (ep.getDescriptor() instanceof RelationDescriptor) {
793 munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
794 munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
796 munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMSET);
797 munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTOSET);
799 int size=ep.leftsize();
800 VarDescriptor sizevar=VarDescriptor.makeNew("size");
801 ((OpExpr)expr).left.generate(cr, sizevar);
802 VarDescriptor change=VarDescriptor.makeNew("change");
803 cr.outputline("int "+change.getSafeSymbol()+";");
804 boolean generateadd=false;
805 boolean generateremove=false;
806 if (opcode==Opcode.GT) {
807 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
809 generateremove=false;
810 } else if (opcode==Opcode.GE) {
811 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
813 generateremove=false;
814 } else if (opcode==Opcode.LT) {
815 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size-1)+"-"+sizevar.getSafeSymbol()+";");
818 } else if (opcode==Opcode.LE) {
819 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
822 } else if (opcode==Opcode.EQ) {
823 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
826 } else if (opcode==Opcode.NE) {
827 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
829 generateremove=false;
831 throw new Error("Unrecognized Opcode");
833 Descriptor d=ep.getDescriptor();
834 if (generateremove) {
835 cr.outputline("for(;"+change.getSafeSymbol()+"<0;"+change.getSafeSymbol()+"++)");
837 /* Find element to remove */
838 VarDescriptor leftvar=VarDescriptor.makeNew("leftvar");
839 VarDescriptor rightvar=VarDescriptor.makeNew("rightvar");
840 if (d instanceof RelationDescriptor) {
842 rightvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
843 cr.outputline("int "+leftvar.getSafeSymbol()+";");
844 cr.outputline(d.getSafeSymbol()+"_hashinv->get((int)"+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
846 leftvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
847 cr.outputline("int "+rightvar.getSafeSymbol()+";");
848 cr.outputline(d.getSafeSymbol()+"_hash->get((int)"+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
851 cr.outputline("int "+leftvar.getSafeSymbol()+"="+d.getSafeSymbol()+"_hash->firstkey();");
853 /* Generate abstract remove instruction */
854 if (d instanceof RelationDescriptor) {
855 RelationDescriptor rd=(RelationDescriptor) d;
856 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
857 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
859 cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + rightvar + ");");
861 cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar + ", (int)" + leftvar + ");");
863 cr.outputline(d.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + leftvar + ");");
865 /* Generate concrete remove instruction */
866 for(int i=0;i<state.vRules.size();i++) {
867 Rule r=(Rule)state.vRules.get(i);
868 if (r.getInclusion().getTargetDescriptors().contains(d)) {
869 for(int j=0;j<munremove.numUpdates();j++) {
870 UpdateNode un=munremove.getUpdate(i);
871 if (un.getRule()==r) {
872 /* Update for rule rule r */
873 String name=(String)updatenames.get(un);
874 if (d instanceof RelationDescriptor) {
875 cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
877 cr.outputline(repairtable.getSafeSymbol()+"->addset("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
887 cr.outputline("for(;"+change.getSafeSymbol()+">0;"+change.getSafeSymbol()+"--)");
889 VarDescriptor newobject=VarDescriptor.makeNew("newobject");
890 if (d instanceof RelationDescriptor) {
891 VarDescriptor otherside=((ImageSetExpr)((SizeofExpr)ep.expr).setexpr).vd;
892 RelationDescriptor rd=(RelationDescriptor)d;
893 if (sources.relsetSource(rd,!ep.inverted())) {
895 SetDescriptor sd=sources.relgetSourceSet(rd,!ep.inverted());
896 VarDescriptor iterator=VarDescriptor.makeNew("iterator");
897 cr.outputline(sd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";");
898 cr.outputline("for("+iterator.getSafeSymbol()+"="+sd.getSafeSymbol()+"_hash->iterator();"+iterator.getSafeSymbol()+".hasNext();)");
901 cr.outputline("if !"+rd.getSafeSymbol()+"_hashinv->contains("+iterator.getSafeSymbol()+"->key(),"+otherside.getSafeSymbol()+")");
903 cr.outputline("if !"+rd.getSafeSymbol()+"_hash->contains("+otherside.getSafeSymbol()+","+iterator.getSafeSymbol()+"->key())");
905 cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();");
906 cr.outputline(iterator.getSafeSymbol()+"->next();");
908 } else if (sources.relallocSource(rd,!ep.inverted())) {
909 /* Allocation Source*/
910 sources.relgenerateSourceAlloc(cr,newobject,rd,!ep.inverted());
911 } else throw new Error("No source for adding to Relation");
913 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
914 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
916 cr.outputline(rd.getSafeSymbol()+"_hash->add("+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
918 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
920 UpdateNode un=munadd.getUpdate(0);
921 String name=(String)updatenames.get(un);
922 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
924 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
925 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
927 cr.outputline(rd.getSafeSymbol()+"_hash->add("+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
929 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
930 UpdateNode un=munadd.getUpdate(0);
931 String name=(String)updatenames.get(un);
932 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
935 SetDescriptor sd=(SetDescriptor)d;
936 if (sources.setSource(sd)) {
939 SetDescriptor sourcesd=sources.getSourceSet(sd);
940 VarDescriptor iterator=VarDescriptor.makeNew("iterator");
941 cr.outputline(sourcesd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";");
942 cr.outputline("for("+iterator.getSafeSymbol()+"="+sourcesd.getSafeSymbol()+"_hash->iterator();"+iterator.getSafeSymbol()+".hasNext();)");
944 cr.outputline("if !"+sd.getSafeSymbol()+"_hash->contains("+iterator.getSafeSymbol()+"->key())");
945 cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();");
946 cr.outputline(iterator.getSafeSymbol()+"->next();");
948 } else if (sources.allocSource(sd)) {
949 /* Allocation Source*/
950 sources.generateSourceAlloc(cr,newobject,sd);
951 } else throw new Error("No source for adding to Set");
952 cr.outputline(sd.getSafeSymbol()+"_hash->add("+newobject.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
953 UpdateNode un=munadd.getUpdate(0);
954 String name=(String)updatenames.get(un);
955 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
961 public void generateinclusionrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
962 InclusionPredicate ip=(InclusionPredicate) dpred.getPredicate();
963 boolean negated=dpred.isNegated();
964 MultUpdateNode mun=getmultupdatenode(conj,dpred,-1);
965 VarDescriptor leftvar=VarDescriptor.makeNew("left");
966 ip.expr.generate(cr, leftvar);
969 if (ip.setexpr instanceof ImageSetExpr) {
970 ImageSetExpr ise=(ImageSetExpr) ip.setexpr;
971 VarDescriptor rightvar=ise.getVar();
972 boolean inverse=ise.inverted();
973 RelationDescriptor rd=ise.getRelation();
974 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
975 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
978 cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + rightvar + ", (int)" + leftvar + ");");
980 cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + leftvar + ", (int)" + rightvar + ");");
983 cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + rightvar + ");");
985 cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar + ", (int)" + leftvar + ");");
987 for(int i=0;i<state.vRules.size();i++) {
988 Rule r=(Rule)state.vRules.get(i);
989 if (r.getInclusion().getTargetDescriptors().contains(rd)) {
990 for(int j=0;j<mun.numUpdates();j++) {
991 UpdateNode un=mun.getUpdate(i);
992 if (un.getRule()==r) {
993 /* Update for rule rule r */
994 String name=(String)updatenames.get(un);
996 cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
998 cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
1005 SetDescriptor sd=ip.setexpr.sd;
1006 cr.outputline(sd.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + leftvar + ");");
1008 for(int i=0;i<state.vRules.size();i++) {
1009 Rule r=(Rule)state.vRules.get(i);
1010 if (r.getInclusion().getTargetDescriptors().contains(sd)) {
1011 for(int j=0;j<mun.numUpdates();j++) {
1012 UpdateNode un=mun.getUpdate(i);
1013 if (un.getRule()==r) {
1014 /* Update for rule rule r */
1015 String name=(String)updatenames.get(un);
1016 cr.outputline(repairtable.getSafeSymbol()+"->addset("+sd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
1023 /* Generate update */
1024 if (ip.setexpr instanceof ImageSetExpr) {
1025 ImageSetExpr ise=(ImageSetExpr) ip.setexpr;
1026 VarDescriptor rightvar=ise.getVar();
1027 boolean inverse=ise.inverted();
1028 RelationDescriptor rd=ise.getRelation();
1029 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1030 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1033 cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + rightvar + ", (int)" + leftvar + ");");
1035 cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + leftvar + ", (int)" + rightvar + ");");
1038 cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + rightvar + ");");
1040 cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar + ", (int)" + leftvar + ");");
1042 UpdateNode un=mun.getUpdate(0);
1043 String name=(String)updatenames.get(un);
1045 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
1047 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
1050 SetDescriptor sd=ip.setexpr.sd;
1051 cr.outputline(sd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + leftvar + ");");
1053 UpdateNode un=mun.getUpdate(0);
1054 /* Update for rule rule r */
1055 String name=(String)updatenames.get(un);
1056 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
1063 public static Vector getrulelist(Descriptor d) {
1064 Vector dispatchrules = new Vector();
1065 Vector rules = State.currentState.vRules;
1067 for (int i = 0; i < rules.size(); i++) {
1068 Rule rule = (Rule) rules.elementAt(i);
1069 Set requiredsymbols = rule.getRequiredDescriptors();
1071 // #TBD#: in general this is wrong because these descriptors may contain descriptors
1072 // bound in "in?" expressions which need to be dealt with in a topologically sorted
1075 if (rule.getRequiredDescriptors().contains(d)) {
1076 dispatchrules.addElement(rule);
1079 return dispatchrules;
1082 private boolean need_compensation(Rule r) {
1083 GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
1084 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
1085 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
1086 GraphNode gn2=edge.getTarget();
1087 if (!removed.contains(gn2)) {
1088 TermNode tn2=(TermNode)gn2.getOwner();
1089 if (tn2.getType()==TermNode.CONSEQUENCE)
1096 private UpdateNode find_compensation(Rule r) {
1097 GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
1098 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
1099 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
1100 GraphNode gn2=edge.getTarget();
1101 if (!removed.contains(gn2)) {
1102 TermNode tn2=(TermNode)gn2.getOwner();
1103 if (tn2.getType()==TermNode.UPDATE) {
1104 MultUpdateNode mun=tn2.getUpdate();
1105 for(int i=0;i<mun.numUpdates();i++) {
1106 UpdateNode un=mun.getUpdate(i);
1107 if (un.getRule()==r)
1113 throw new Error("No Compensation Update could be found");
1116 public void generate_dispatch(CodeWriter cr, RelationDescriptor rd, String leftvar, String rightvar) {
1117 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1118 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1120 if (!(usageinvimage||usageimage)) /* not used at all*/
1123 cr.outputline("// RELATION DISPATCH ");
1124 cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
1126 cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hash->contains("+leftvar+","+rightvar+"))");
1128 cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hashinv->contains("+rightvar+","+leftvar+"))");
1130 /* Adding new item */
1131 /* Perform safety checks */
1132 cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
1133 cr.outputline(repairtable.getSafeSymbol()+"->containsrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+"))");
1135 /* Have update to call into */
1136 VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
1138 for(int i=0;i<currentrule.numQuantifiers();i++) {
1139 if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
1140 parttype=parttype+", int, int";
1142 parttype=parttype+", int";
1144 cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")=");
1145 cr.outputline("(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+repairtable.getSafeSymbol()+"->getrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");");
1146 String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
1147 for(int i=0;i<currentrule.numQuantifiers();i++) {
1148 Quantifier q=currentrule.getQuantifier(i);
1149 if (q instanceof SetQuantifier) {
1150 SetQuantifier sq=(SetQuantifier) q;
1151 methodcall+=","+sq.getVar().getSafeSymbol();
1152 } else if (q instanceof RelationQuantifier) {
1153 RelationQuantifier rq=(RelationQuantifier) q;
1154 methodcall+=","+rq.x.getSafeSymbol();
1155 methodcall+=","+rq.y.getSafeSymbol();
1156 } else if (q instanceof ForQuantifier) {
1157 ForQuantifier fq=(ForQuantifier) q;
1158 methodcall+=","+fq.getVar().getSafeSymbol();
1162 cr.outputline(methodcall);
1163 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1164 cr.outputline("continue;");
1167 /* Build standard compensation actions */
1168 if (need_compensation(currentrule)) {
1169 UpdateNode un=find_compensation(currentrule);
1170 String name=(String)updatenames.get(un);
1171 usedupdates.add(un); /* Mark as used */
1172 String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
1173 for(int i=0;i<currentrule.numQuantifiers();i++) {
1174 Quantifier q=currentrule.getQuantifier(i);
1175 if (q instanceof SetQuantifier) {
1176 SetQuantifier sq=(SetQuantifier) q;
1177 methodcall+=","+sq.getVar().getSafeSymbol();
1178 } else if (q instanceof RelationQuantifier) {
1179 RelationQuantifier rq=(RelationQuantifier) q;
1180 methodcall+=","+rq.x.getSafeSymbol();
1181 methodcall+=","+rq.y.getSafeSymbol();
1182 } else if (q instanceof ForQuantifier) {
1183 ForQuantifier fq=(ForQuantifier) q;
1184 methodcall+=","+fq.getVar().getSafeSymbol();
1188 cr.outputline(methodcall);
1189 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1190 cr.outputline("continue;");
1195 String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
1196 cr.outputline("int " + addeditem + ";");
1197 if (rd.testUsage(RelationDescriptor.IMAGE)) {
1198 cr.outputline(addeditem + " = " + rd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + rightvar + ");");
1201 if (rd.testUsage(RelationDescriptor.INVIMAGE)) {
1202 cr.outputline(addeditem + " = " + rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar + ", (int)" + leftvar + ");");
1205 cr.outputline("if (" + addeditem + ")");
1208 Vector dispatchrules = getrulelist(rd);
1210 if (dispatchrules.size() == 0) {
1211 cr.outputline("// nothing to dispatch");
1216 for(int i = 0; i < dispatchrules.size(); i++) {
1217 Rule rule = (Rule) dispatchrules.elementAt(i);
1218 if (rule.getGuardExpr().getRequiredDescriptors().contains(rd)) {
1219 /* Guard depends on this relation, so we recomput everything */
1220 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
1222 for (int j=0;j<rule.numQuantifiers();j++) {
1223 Quantifier q=rule.getQuantifier(j);
1224 if (q.getRequiredDescriptors().contains(rd)) {
1226 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+leftvar+","+rightvar+");");
1235 public void generate_dispatch(CodeWriter cr, SetDescriptor sd, String setvar) {
1237 cr.outputline("// SET DISPATCH ");
1239 cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
1240 cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+sd.getJustSafeSymbol()+"_hash->contains("+setvar+"))");
1242 /* Adding new item */
1243 /* Perform safety checks */
1244 cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
1245 cr.outputline(repairtable.getSafeSymbol()+"->containsset("+sd.getNum()+","+currentrule.getNum()+","+setvar+"))");
1247 /* Have update to call into */
1248 VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
1250 for(int i=0;i<currentrule.numQuantifiers();i++) {
1251 if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
1252 parttype=parttype+", int, int";
1254 parttype=parttype+", int";
1256 cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")=");
1257 cr.outputline("(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+repairtable.getSafeSymbol()+"->getset("+sd.getNum()+","+currentrule.getNum()+","+setvar+");");
1258 String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+
1259 repairtable.getSafeSymbol();
1260 for(int i=0;i<currentrule.numQuantifiers();i++) {
1261 Quantifier q=currentrule.getQuantifier(i);
1262 if (q instanceof SetQuantifier) {
1263 SetQuantifier sq=(SetQuantifier) q;
1264 methodcall+=","+sq.getVar().getSafeSymbol();
1265 } else if (q instanceof RelationQuantifier) {
1266 RelationQuantifier rq=(RelationQuantifier) q;
1267 methodcall+=","+rq.x.getSafeSymbol();
1268 methodcall+=","+rq.y.getSafeSymbol();
1269 } else if (q instanceof ForQuantifier) {
1270 ForQuantifier fq=(ForQuantifier) q;
1271 methodcall+=","+fq.getVar().getSafeSymbol();
1275 cr.outputline(methodcall);
1276 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1277 cr.outputline("continue;");
1280 /* Build standard compensation actions */
1281 if (need_compensation(currentrule)) {
1282 UpdateNode un=find_compensation(currentrule);
1283 String name=(String)updatenames.get(un);
1284 usedupdates.add(un); /* Mark as used */
1286 String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+
1287 repairtable.getSafeSymbol();
1288 for(int i=0;i<currentrule.numQuantifiers();i++) {
1289 Quantifier q=currentrule.getQuantifier(i);
1290 if (q instanceof SetQuantifier) {
1291 SetQuantifier sq=(SetQuantifier) q;
1292 methodcall+=","+sq.getVar().getSafeSymbol();
1293 } else if (q instanceof RelationQuantifier) {
1294 RelationQuantifier rq=(RelationQuantifier) q;
1295 methodcall+=","+rq.x.getSafeSymbol();
1296 methodcall+=","+rq.y.getSafeSymbol();
1297 } else if (q instanceof ForQuantifier) {
1298 ForQuantifier fq=(ForQuantifier) q;
1299 methodcall+=","+fq.getVar().getSafeSymbol();
1303 cr.outputline(methodcall);
1304 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1305 cr.outputline("continue;");
1310 String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
1311 cr.outputline("int " + addeditem + " = 1;");
1312 cr.outputline(addeditem + " = " + sd.getSafeSymbol() + "_hash->add((int)" + setvar + ", (int)" + setvar + ");");
1314 Vector dispatchrules = getrulelist(sd);
1316 if (dispatchrules.size() == 0) {
1317 cr.outputline("// nothing to dispatch");
1322 for(int i = 0; i < dispatchrules.size(); i++) {
1323 Rule rule = (Rule) dispatchrules.elementAt(i);
1324 if (SetDescriptor.expand(rule.getGuardExpr().getRequiredDescriptors()).contains(sd)) {
1325 /* Guard depends on this relation, so we recompute everything */
1326 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
1328 for (int j=0;j<rule.numQuantifiers();j++) {
1329 Quantifier q=rule.getQuantifier(j);
1330 if (SetDescriptor.expand(q.getRequiredDescriptors()).contains(sd)) {
1332 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+setvar+",0);");