12 public UpdateNode(Rule r) {
14 bindings=new Vector();
15 invariants=new Vector();
16 binding=new Hashtable();
20 public Rule getRule() {
24 public String toString() {
27 for(int i=0;i<bindings.size();i++)
28 st+=bindings.get(i).toString()+"\n";
29 st+="---------------------\n";
31 for(int i=0;i<updates.size();i++)
32 st+=updates.get(i).toString()+"\n";
33 st+="---------------------\n";
35 for(int i=0;i<invariants.size();i++)
36 st+=((Expr)invariants.get(i)).name()+"\n";
37 st+="---------------------\n";
41 public void addBindings(Vector v) {
42 for (int i=0;i<v.size();i++) {
43 addBinding((Binding)v.get(i));
47 public boolean checkupdates(State state) {
48 if (!checkconflicts()) /* Do we have conflicting concrete updates */
50 if (!checknoupdates(state))
52 if (computeordering()) /* Ordering exists */
57 private boolean checknoupdates(State state) {
58 Set noupdate=state.noupdate;
59 for(int i=0;i<updates.size();i++) {
60 Updates u=(Updates)updates.get(i);
62 continue; /* Abstract updates don't change fields */
63 Descriptor d=u.getDescriptor();
64 if (noupdate.contains(d))
70 private boolean computeordering() {
71 /* Build dependency graph between updates */
72 HashSet graph=new HashSet();
73 Hashtable mapping=new Hashtable();
74 for(int i=0;i<updates.size();i++) {
75 Updates u=(Updates)updates.get(i);
76 GraphNode gn=new GraphNode(String.valueOf(i),u);
80 for(int i=0;i<updates.size();i++) {
81 Updates u1=(Updates)updates.get(i);
84 for(int j=0;j<updates.size();j++) {
85 Updates u2=(Updates)updates.get(j);
88 Descriptor d=u1.getDescriptor();
93 subexpr=((DotExpr)u2.getLeftExpr()).getExpr();
94 intindex=((DotExpr)u2.getLeftExpr()).getIndex();
96 if (u2.getRightExpr().usesDescriptor(d)||
97 (subexpr!=null&&subexpr.usesDescriptor(d))||
98 (intindex!=null&&intindex.usesDescriptor(d))) {
99 /* Add edge for dependency */
100 GraphNode gn1=(GraphNode) mapping.get(u1);
101 GraphNode gn2=(GraphNode) mapping.get(u2);
102 GraphNode.Edge e=new GraphNode.Edge("dependency",gn2);
108 if (!GraphNode.DFS.depthFirstSearch(graph)) /* DFS & check for acyclicity */
111 TreeSet topologicalsort = new TreeSet(new Comparator() {
112 public boolean equals(Object obj) { return false; }
113 public int compare(Object o1, Object o2) {
114 GraphNode g1 = (GraphNode) o1;
115 GraphNode g2 = (GraphNode) o2;
116 return g2.getFinishingTime() - g1.getFinishingTime();
119 topologicalsort.addAll(graph);
120 Vector sortedvector=new Vector();
121 for(Iterator sort=topologicalsort.iterator();sort.hasNext();) {
122 GraphNode gn=(GraphNode)sort.next();
123 sortedvector.add(gn.getOwner());
125 updates=sortedvector; //replace updates with the sorted array
129 private boolean checkconflicts() {
130 Set toremove=new HashSet();
131 for(int i=0;i<updates.size();i++) {
132 Updates u1=(Updates)updates.get(i);
133 if (!u1.isAbstract()) {
134 Descriptor d=u1.getDescriptor();
135 for(int j=0;j<invariants.size();j++) {
136 Expr invariant=(Expr)invariants.get(j);
137 if (invariant.usesDescriptor(d))
141 for(int j=0;j<updates.size();j++) {
142 Updates u2=(Updates)updates.get(j);
145 if (u1.isAbstract()||u2.isAbstract())
146 continue; /* Abstract updates are already accounted for by graph */
147 if (u1.getDescriptor()!=u2.getDescriptor())
148 continue; /* No interference - different descriptors */
150 if ((u1.getOpcode()==Opcode.GT||u1.getOpcode()==Opcode.GE)&&
151 (u2.getOpcode()==Opcode.GT||u2.getOpcode()==Opcode.GE))
152 continue; /* Can be satisfied simultaneously */
154 if ((u1.getOpcode()==Opcode.LT||u1.getOpcode()==Opcode.LE)&&
155 (u2.getOpcode()==Opcode.LT||u2.getOpcode()==Opcode.LE))
157 if ((u1.getOpcode()==u2.getOpcode())&&
158 u1.isExpr()&&u2.isExpr()&&
159 u1.getRightExpr().equals(null, u2.getRightExpr())) {
160 /*We'll remove the second occurence*/
168 /* Handle = or != NULL */
169 if ((((u1.getOpcode()==Opcode.EQ)&&(u2.getOpcode()==Opcode.NE))||
170 ((u1.getOpcode()==Opcode.NE)&&(u2.getOpcode()==Opcode.EQ)))&&
171 (((u1.isExpr()&&u1.getRightExpr().isNull())&&(!u2.isExpr()||u2.getRightExpr().isNonNull()))
172 ||((!u1.isExpr()||u1.getRightExpr().isNonNull())&&(u2.isExpr()&&u2.getRightExpr().isNull())))) {
173 if (u1.getOpcode()==Opcode.NE)
180 /* Handle = and != to different constants */
181 if ((((u1.getOpcode()==Opcode.EQ)&&(u2.getOpcode()==Opcode.NE))||
182 ((u1.getOpcode()==Opcode.NE)&&(u2.getOpcode()==Opcode.EQ)))&&
183 (u1.isExpr()&&u1.getRightExpr() instanceof LiteralExpr)&&
184 (u2.isExpr()&&u2.getRightExpr() instanceof LiteralExpr)&&
185 !u1.getRightExpr().equals(u2.getRightExpr())) {
186 if (u1.getOpcode()==Opcode.NE)
193 /* Compatible operations < & <= */
194 if (((u1.getOpcode()==Opcode.LT)||(u1.getOpcode()==Opcode.LE))&&
195 ((u2.getOpcode()==Opcode.LT)||(u2.getOpcode()==Opcode.LE)))
198 /* Compatible operations > & >= */
199 if (((u1.getOpcode()==Opcode.GT)||(u1.getOpcode()==Opcode.GE))&&
200 ((u2.getOpcode()==Opcode.GT)||(u2.getOpcode()==Opcode.GE)))
205 /* Equality & Comparisons */
208 return false; /* They interfere */
211 updates.removeAll(toremove);
215 public void addBinding(Binding b) {
217 binding.put(b.getVar(),b);
220 public int numBindings() {
221 return bindings.size();
224 public Binding getBinding(int i) {
225 return (Binding)bindings.get(i);
228 public Binding getBinding(VarDescriptor vd) {
229 if (binding.containsKey(vd))
230 return (Binding)binding.get(vd);
235 public void addInvariant(Expr e) {
239 public int numInvariants() {
240 return invariants.size();
243 public Expr getInvariant(int i) {
244 return (Expr)invariants.get(i);
247 public void addUpdate(Updates u) {
251 public int numUpdates() {
252 return updates.size();
254 public Updates getUpdate(int i) {
255 return (Updates)updates.get(i);
258 private MultUpdateNode getMultUpdateNode(boolean negate, Descriptor d, RepairGenerator rg) {
259 Termination termination=rg.termination;
260 MultUpdateNode mun=null;
263 gn=(GraphNode)termination.abstractremove.get(d);
265 gn=(GraphNode)termination.abstractadd.get(d);
266 TermNode tn=(TermNode)gn.getOwner();
267 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
268 GraphNode gn2=((GraphNode.Edge) edgeit.next()).getTarget();
269 if (!rg.removed.contains(gn2)) {
270 TermNode tn2=(TermNode)gn2.getOwner();
271 if (tn2.getType()==TermNode.UPDATE) {
278 throw new Error("Can't find update node!");
282 public void generate_abstract(CodeWriter cr, Updates u, RepairGenerator rg) {
283 State state=rg.state;
284 Expr abstractexpr=u.getLeftExpr();
285 boolean negated=u.negate;
289 boolean istuple=false;
290 if (abstractexpr instanceof TupleOfExpr) {
291 TupleOfExpr toe=(TupleOfExpr) abstractexpr;
296 } else if (abstractexpr instanceof ElementOfExpr) {
297 ElementOfExpr eoe=(ElementOfExpr) abstractexpr;
302 throw new Error("Unsupported Expr");
304 MultUpdateNode mun=getMultUpdateNode(negated,d,rg);
305 VarDescriptor leftvar=VarDescriptor.makeNew("leftvar");
306 VarDescriptor rightvar=VarDescriptor.makeNew("rightvar");
307 left.generate(cr, leftvar);
309 right.generate(cr,rightvar);
313 RelationDescriptor rd=(RelationDescriptor)d;
314 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
315 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
317 cr.outputline("SimpleHashremove("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
319 cr.outputline("SimpleHashremove("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hashinv, (int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
321 for(int i=0;i<state.vRules.size();i++) {
322 Rule r=(Rule)state.vRules.get(i);
323 if (r.getInclusion().getTargetDescriptors().contains(rd)) {
324 for(int j=0;j<mun.numUpdates();j++) {
325 UpdateNode un=mun.getUpdate(i);
326 if (un.getRule()==r) {
327 /* Update for rule rule r */
328 String name=(String)rg.updatenames.get(un);
329 cr.outputline("RepairHashaddrelation("+rg.strepairtable+","+rd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
335 SetDescriptor sd=(SetDescriptor) d;
336 cr.outputline("SimpleHashremove("+rg.stmodel+"->"+sd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
338 for(int i=0;i<state.vRules.size();i++) {
339 Rule r=(Rule)state.vRules.get(i);
340 if (r.getInclusion().getTargetDescriptors().contains(sd)) {
341 for(int j=0;j<mun.numUpdates();j++) {
342 UpdateNode un=mun.getUpdate(j);
343 if (un.getRule()==r) {
344 /* Update for rule rule r */
345 String name=(String)rg.updatenames.get(un);
346 cr.outputline("RepairHashaddset("+rg.strepairtable+","+sd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
353 /* Generate update */
355 RelationDescriptor rd=(RelationDescriptor) d;
356 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
357 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
359 cr.outputline("SimpleHashadd("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
361 cr.outputline("SimpleHashadd("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hashinv, (int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
363 UpdateNode un=mun.getUpdate(0);
364 String name=(String)rg.updatenames.get(un);
365 cr.outputline(name+"(this,"+rg.stmodel+","+rg.strepairtable+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
367 SetDescriptor sd=(SetDescriptor)d;
368 cr.outputline("SimpleHashadd("+rg.stmodel+"->"+sd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
370 UpdateNode un=mun.getUpdate(0);
371 /* Update for rule rule r */
372 String name=(String)rg.updatenames.get(un);
373 cr.outputline(name+"(this,"+rg.stmodel+","+rg.strepairtable+","+leftvar.getSafeSymbol()+");");
378 public void generate(CodeWriter cr, boolean removal, boolean modify, String slot0, String slot1, String slot2, RepairGenerator rg) {
379 if (!removal&&!modify)
380 generate_bindings(cr, slot0,slot1);
381 for(int i=0;i<updates.size();i++) {
382 Updates u=(Updates)updates.get(i);
383 VarDescriptor right=VarDescriptor.makeNew("right");
384 if (u.getType()==Updates.ABSTRACT) {
385 generate_abstract(cr, u, rg);
389 switch(u.getType()) {
391 u.getRightExpr().generate(cr,right);
393 case Updates.POSITION:
394 case Updates.ACCESSPATH:
395 if (u.getRightPos()==0) {
396 cr.addDeclaration("int", right.getSafeSymbol());
397 cr.outputline(right.getSafeSymbol()+"="+slot0+";");
398 } else if (u.getRightPos()==1) {
399 cr.addDeclaration("int", right.getSafeSymbol());
400 cr.outputline(right.getSafeSymbol()+"="+slot1+";");
401 } else if (u.getRightPos()==2) {
402 cr.addDeclaration("int", right.getSafeSymbol());
403 cr.outputline(right.getSafeSymbol()+"="+slot2+";");
404 } else throw new Error("Error w/ Position");
410 if (u.getType()==Updates.ACCESSPATH) {
411 VarDescriptor newright=VarDescriptor.makeNew("right");
412 generate_accesspath(cr, right,newright,u);
415 VarDescriptor left=VarDescriptor.makeNew("left");
416 u.getLeftExpr().generate(cr,left);
417 Opcode op=u.getOpcode();
418 cr.outputline("if (!("+left.getSafeSymbol()+op+right.getSafeSymbol()+"))");
422 cr.outputline(right.getSafeSymbol()+"++;");
423 else if (op==Opcode.GE)
425 else if (op==Opcode.EQ)
427 else if (op==Opcode.NE)
428 cr.outputline(right.getSafeSymbol()+"++;");
429 else if (op==Opcode.LT)
430 cr.outputline(right.getSafeSymbol()+"--;");
431 else if (op==Opcode.LE)
433 else throw new Error();
435 VarDescriptor vd=((VarExpr)u.getLeftExpr()).getVar();
436 cr.outputline(vd.getSafeSymbol()+"="+right.getSafeSymbol()+";");
437 } else if (u.isField()) {
439 Expr subexpr=((DotExpr)u.getLeftExpr()).getExpr();
440 Expr intindex=((DotExpr)u.getLeftExpr()).getIndex();
441 VarDescriptor subvd=VarDescriptor.makeNew("subexpr");
442 VarDescriptor indexvd=VarDescriptor.makeNew("index");
443 subexpr.generate(cr,subvd);
445 intindex.generate(cr,indexvd);
446 FieldDescriptor fd=(FieldDescriptor)u.getDescriptor();
447 StructureTypeDescriptor std=(StructureTypeDescriptor)subexpr.getType();
448 Expr offsetbits = std.getOffsetExpr(fd);
449 if (fd instanceof ArrayDescriptor) {
450 fd = ((ArrayDescriptor) fd).getField();
453 if (intindex != null) {
454 Expr basesize = fd.getBaseSizeExpr();
455 offsetbits = new OpExpr(Opcode.ADD, offsetbits, new OpExpr(Opcode.MULT, basesize, intindex));
457 Expr offsetbytes = new OpExpr(Opcode.SHR, offsetbits,new IntegerLiteralExpr(3));
458 Expr byteaddress=new OpExpr(Opcode.ADD, offsetbytes, subexpr);
459 VarDescriptor addr=VarDescriptor.makeNew("byteaddress");
460 byteaddress.generate(cr,addr);
462 if (fd.getType() instanceof ReservedTypeDescriptor && !fd.getPtr()) {
463 ReservedTypeDescriptor rtd=(ReservedTypeDescriptor)fd.getType();
464 if (rtd==ReservedTypeDescriptor.INT) {
465 cr.outputline("*((int *) "+addr.getSafeSymbol()+")="+right.getSafeSymbol()+";");
466 } else if (rtd==ReservedTypeDescriptor.SHORT) {
467 cr.outputline("*((short *) "+addr.getSafeSymbol()+")="+right.getSafeSymbol()+";");
468 } else if (rtd==ReservedTypeDescriptor.BYTE) {
469 cr.outputline("*((char *) "+addr.getSafeSymbol()+")="+right.getSafeSymbol()+";");
470 } else if (rtd==ReservedTypeDescriptor.BIT) {
471 Expr tmp = new OpExpr(Opcode.SHL, offsetbytes, new IntegerLiteralExpr(3));
472 Expr offset=new OpExpr(Opcode.SUB, offsetbits, tmp);
473 Expr mask=new OpExpr(Opcode.SHL, new IntegerLiteralExpr(1), offset);
474 VarDescriptor maskvar=VarDescriptor.makeNew("mask");
475 mask.generate(cr,maskvar);
476 cr.outputline("*((char *) "+addr.getSafeSymbol()+")|="+maskvar.getSafeSymbol()+";");
477 cr.outputline("if (!"+right.getSafeSymbol()+")");
478 cr.outputline("*((char *) "+addr.getSafeSymbol()+")^="+maskvar.getSafeSymbol()+";");
479 } else throw new Error();
482 cr.outputline("*((int *) "+addr.getSafeSymbol()+")="+right.getSafeSymbol()+";");
490 private void generate_accesspath(CodeWriter cr, VarDescriptor right, VarDescriptor newright, Updates u) {
491 Vector dotvector=new Vector();
492 Expr ptr=u.getRightExpr();
493 VarExpr rightve=new VarExpr(right);
494 right.td=ReservedTypeDescriptor.INT;
497 /* Does something other than a dereference? */
499 if (ptr instanceof DotExpr)
500 ptr=((DotExpr)ptr).left;
501 else if (ptr instanceof CastExpr)
502 ptr=((CastExpr)ptr).getExpr();
503 if (ptr instanceof VarExpr) {
504 /* Finished constructing vector */
508 ArrayAnalysis.AccessPath ap=u.getAccessPath();
509 VarDescriptor init=VarDescriptor.makeNew("init");
511 cr.addDeclaration("int", init.getSafeSymbol());
512 cr.outputline(init.getSafeSymbol()+"= SimpleHashfirstkey("+ap.getSet().getSafeSymbol()+"_hash);");
513 init.td=ap.getSet().getType();
517 Expr newexpr=new VarExpr(init);
519 for(int i=dotvector.size()-1;i>=0;i--) {
520 Expr e=(Expr)dotvector.get(i);
521 if (e instanceof CastExpr) {
523 newexpr=new CastExpr(((CastExpr)e).getType(),newexpr);
524 } else if (e instanceof DotExpr) {
525 DotExpr de=(DotExpr)e;
526 if (de.getField() instanceof ArrayDescriptor) {
527 DotExpr de2=new DotExpr(newexpr,de.field,new IntegerLiteralExpr(0));
529 de2.fieldtype=de.fieldtype;
531 OpExpr offset=new OpExpr(Opcode.SUB,rightve,de2);
532 OpExpr index=new OpExpr(Opcode.DIV,offset,de.fieldtype.getSizeExpr());
533 if (u.getRightPos()==apindex) {
534 index.generate(cr,newright);
537 DotExpr de3=new DotExpr(newexpr,de.field,index);
540 de3.fieldtype=de.fieldtype;
544 DotExpr de2=new DotExpr(newexpr,de.field,null);
546 de2.fieldtype=de.fieldtype;
551 } else throw new Error();
556 private void generate_bindings(CodeWriter cr, String slot0, String slot1) {
557 for(int i=0;i<bindings.size();i++) {
558 Binding b=(Binding)bindings.get(i);
560 if (b.getType()==Binding.SEARCH) {
561 VarDescriptor vd=b.getVar();
562 cr.addDeclaration(vd.getType().getGenerateType().getSafeSymbol(), vd.getSafeSymbol());
563 cr.outputline(vd.getSafeSymbol()+"=SimpleHashfirstkey("+b.getSet().getSafeSymbol()+"_hash);");
564 } else if (b.getType()==Binding.CREATE) {
565 throw new Error("Creation not supported");
566 // source.generateSourceAlloc(cr,vd,b.getSet());
568 VarDescriptor vd=b.getVar();
569 switch(b.getPosition()) {
571 cr.addDeclaration(vd.getType().getGenerateType().getSafeSymbol(), vd.getSafeSymbol());
572 cr.outputline(vd.getSafeSymbol()+"="+slot0+";");
575 cr.addDeclaration(vd.getType().getGenerateType().getSafeSymbol(), vd.getSafeSymbol());
576 cr.outputline(vd.getSafeSymbol()+"="+slot1+";");
579 throw new Error("Slot >1 doesn't exist.");