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() {
48 if (!checkconflicts()) /* Do we have conflicting concrete updates */
50 if (computeordering()) /* Ordering exists */
55 private boolean computeordering() {
56 /* Build dependency graph between updates */
57 HashSet graph=new HashSet();
58 Hashtable mapping=new Hashtable();
59 for(int i=0;i<updates.size();i++) {
60 Updates u=(Updates)updates.get(i);
61 GraphNode gn=new GraphNode(String.valueOf(i),u);
65 for(int i=0;i<updates.size();i++) {
66 Updates u1=(Updates)updates.get(i);
69 for(int j=0;j<updates.size();j++) {
70 Updates u2=(Updates)updates.get(j);
73 Descriptor d=u1.getDescriptor();
78 subexpr=((DotExpr)u2.getLeftExpr()).getExpr();
79 intindex=((DotExpr)u2.getLeftExpr()).getIndex();
81 if (u2.getRightExpr().usesDescriptor(d)||
82 (subexpr!=null&&subexpr.usesDescriptor(d))||
83 (intindex!=null&&intindex.usesDescriptor(d))) {
84 /* Add edge for dependency */
85 GraphNode gn1=(GraphNode) mapping.get(u1);
86 GraphNode gn2=(GraphNode) mapping.get(u2);
87 GraphNode.Edge e=new GraphNode.Edge("dependency",gn2);
93 if (!GraphNode.DFS.depthFirstSearch(graph)) /* DFS & check for acyclicity */
96 TreeSet topologicalsort = new TreeSet(new Comparator() {
97 public boolean equals(Object obj) { return false; }
98 public int compare(Object o1, Object o2) {
99 GraphNode g1 = (GraphNode) o1;
100 GraphNode g2 = (GraphNode) o2;
101 return g2.getFinishingTime() - g1.getFinishingTime();
104 topologicalsort.addAll(graph);
105 Vector sortedvector=new Vector();
106 for(Iterator sort=topologicalsort.iterator();sort.hasNext();) {
107 GraphNode gn=(GraphNode)sort.next();
108 sortedvector.add(gn.getOwner());
110 updates=sortedvector; //replace updates with the sorted array
114 private boolean checkconflicts() {
115 Set toremove=new HashSet();
116 for(int i=0;i<updates.size();i++) {
117 Updates u1=(Updates)updates.get(i);
118 if (!u1.isAbstract()) {
119 Descriptor d=u1.getDescriptor();
120 for(int j=0;j<invariants.size();j++) {
121 Expr invariant=(Expr)invariants.get(j);
122 if (invariant.usesDescriptor(d))
126 for(int j=0;j<updates.size();j++) {
127 Updates u2=(Updates)updates.get(j);
130 if (u1.isAbstract()||u2.isAbstract())
131 continue; /* Abstract updates are already accounted for by graph */
132 if (u1.getDescriptor()!=u2.getDescriptor())
133 continue; /* No interference - different descriptors */
135 if ((u1.getOpcode()==Opcode.GT||u1.getOpcode()==Opcode.GE)&&
136 (u2.getOpcode()==Opcode.GT||u2.getOpcode()==Opcode.GE))
137 continue; /* Can be satisfied simultaneously */
139 if ((u1.getOpcode()==Opcode.LT||u1.getOpcode()==Opcode.LE)&&
140 (u2.getOpcode()==Opcode.LT||u2.getOpcode()==Opcode.LE))
142 if ((u1.getOpcode()==u2.getOpcode())&&
143 u1.isExpr()&&u2.isExpr()&&
144 u1.getRightExpr().equals(null, u2.getRightExpr())) {
145 /*We'll remove the second occurence*/
153 /* Handle = or != NULL */
154 if ((((u1.getOpcode()==Opcode.EQ)&&(u2.getOpcode()==Opcode.NE))||
155 ((u1.getOpcode()==Opcode.NE)&&(u2.getOpcode()==Opcode.EQ)))&&
156 (((u1.isExpr()&&u1.getRightExpr().isNull())&&(!u2.isExpr()||u2.getRightExpr().isNonNull()))
157 ||((!u1.isExpr()||u1.getRightExpr().isNonNull())&&(u2.isExpr()&&u2.getRightExpr().isNull())))) {
158 if (u1.getOpcode()==Opcode.NE)
165 /* Handle = and != to different constants */
166 if ((((u1.getOpcode()==Opcode.EQ)&&(u2.getOpcode()==Opcode.NE))||
167 ((u1.getOpcode()==Opcode.NE)&&(u2.getOpcode()==Opcode.EQ)))&&
168 (u1.isExpr()&&u1.getRightExpr() instanceof LiteralExpr)&&
169 (u2.isExpr()&&u2.getRightExpr() instanceof LiteralExpr)&&
170 !u1.getRightExpr().equals(u2.getRightExpr())) {
171 if (u1.getOpcode()==Opcode.NE)
178 /* Compatible operations < & <= */
179 if (((u1.getOpcode()==Opcode.LT)||(u1.getOpcode()==Opcode.LE))&&
180 ((u2.getOpcode()==Opcode.LT)||(u2.getOpcode()==Opcode.LE)))
183 /* Compatible operations > & >= */
184 if (((u1.getOpcode()==Opcode.GT)||(u1.getOpcode()==Opcode.GE))&&
185 ((u2.getOpcode()==Opcode.GT)||(u2.getOpcode()==Opcode.GE)))
190 /* Equality & Comparisons */
193 return false; /* They interfere */
196 updates.removeAll(toremove);
200 public void addBinding(Binding b) {
202 binding.put(b.getVar(),b);
205 public int numBindings() {
206 return bindings.size();
209 public Binding getBinding(int i) {
210 return (Binding)bindings.get(i);
213 public Binding getBinding(VarDescriptor vd) {
214 if (binding.containsKey(vd))
215 return (Binding)binding.get(vd);
220 public void addInvariant(Expr e) {
224 public int numInvariants() {
225 return invariants.size();
228 public Expr getInvariant(int i) {
229 return (Expr)invariants.get(i);
232 public void addUpdate(Updates u) {
236 public int numUpdates() {
237 return updates.size();
239 public Updates getUpdate(int i) {
240 return (Updates)updates.get(i);
243 private MultUpdateNode getMultUpdateNode(boolean negate, Descriptor d, RepairGenerator rg) {
244 Termination termination=rg.termination;
245 MultUpdateNode mun=null;
248 gn=(GraphNode)termination.abstractremove.get(d);
250 gn=(GraphNode)termination.abstractadd.get(d);
251 TermNode tn=(TermNode)gn.getOwner();
252 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
253 GraphNode gn2=((GraphNode.Edge) edgeit.next()).getTarget();
254 if (!rg.removed.contains(gn2)) {
255 TermNode tn2=(TermNode)gn2.getOwner();
256 if (tn2.getType()==TermNode.UPDATE) {
263 throw new Error("Can't find update node!");
267 public void generate_abstract(CodeWriter cr, Updates u, RepairGenerator rg) {
268 State state=rg.state;
269 Expr abstractexpr=u.getLeftExpr();
270 boolean negated=u.negate;
274 boolean istuple=false;
275 if (abstractexpr instanceof TupleOfExpr) {
276 TupleOfExpr toe=(TupleOfExpr) abstractexpr;
281 } else if (abstractexpr instanceof ElementOfExpr) {
282 ElementOfExpr eoe=(ElementOfExpr) abstractexpr;
287 throw new Error("Unsupported Expr");
289 MultUpdateNode mun=getMultUpdateNode(negated,d,rg);
290 VarDescriptor leftvar=VarDescriptor.makeNew("leftvar");
291 VarDescriptor rightvar=VarDescriptor.makeNew("rightvar");
292 left.generate(cr, leftvar);
294 right.generate(cr,rightvar);
298 RelationDescriptor rd=(RelationDescriptor)d;
299 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
300 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
302 cr.outputline("SimpleHashremove("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
304 cr.outputline("SimpleHashremove("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hashinv, (int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
306 for(int i=0;i<state.vRules.size();i++) {
307 Rule r=(Rule)state.vRules.get(i);
308 if (r.getInclusion().getTargetDescriptors().contains(rd)) {
309 for(int j=0;j<mun.numUpdates();j++) {
310 UpdateNode un=mun.getUpdate(i);
311 if (un.getRule()==r) {
312 /* Update for rule rule r */
313 String name=(String)rg.updatenames.get(un);
314 cr.outputline("RepairHashaddrelation("+rg.strepairtable+","+rd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
320 SetDescriptor sd=(SetDescriptor) d;
321 cr.outputline("SimpleHashremove("+rg.stmodel+"->"+sd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
323 for(int i=0;i<state.vRules.size();i++) {
324 Rule r=(Rule)state.vRules.get(i);
325 if (r.getInclusion().getTargetDescriptors().contains(sd)) {
326 for(int j=0;j<mun.numUpdates();j++) {
327 UpdateNode un=mun.getUpdate(j);
328 if (un.getRule()==r) {
329 /* Update for rule rule r */
330 String name=(String)rg.updatenames.get(un);
331 cr.outputline("RepairHashaddset("+rg.strepairtable+","+sd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
338 /* Generate update */
340 RelationDescriptor rd=(RelationDescriptor) d;
341 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
342 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
344 cr.outputline("SimpleHashadd("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
346 cr.outputline("SimpleHashadd("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hashinv, (int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
348 UpdateNode un=mun.getUpdate(0);
349 String name=(String)rg.updatenames.get(un);
350 cr.outputline(name+"(this,"+rg.stmodel+","+rg.strepairtable+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
352 SetDescriptor sd=(SetDescriptor)d;
353 cr.outputline("SimpleHashadd("+rg.stmodel+"->"+sd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
355 UpdateNode un=mun.getUpdate(0);
356 /* Update for rule rule r */
357 String name=(String)rg.updatenames.get(un);
358 cr.outputline(name+"(this,"+rg.stmodel+","+rg.strepairtable+","+leftvar.getSafeSymbol()+");");
363 public void generate(CodeWriter cr, boolean removal, boolean modify, String slot0, String slot1, String slot2, RepairGenerator rg) {
364 if (!removal&&!modify)
365 generate_bindings(cr, slot0,slot1);
366 for(int i=0;i<updates.size();i++) {
367 Updates u=(Updates)updates.get(i);
368 VarDescriptor right=VarDescriptor.makeNew("right");
369 if (u.getType()==Updates.ABSTRACT) {
370 generate_abstract(cr, u, rg);
374 switch(u.getType()) {
376 u.getRightExpr().generate(cr,right);
378 case Updates.POSITION:
379 case Updates.ACCESSPATH:
380 if (u.getRightPos()==0) {
381 cr.addDeclaration("int", right.getSafeSymbol());
382 cr.outputline(right.getSafeSymbol()+"="+slot0+";");
383 } else if (u.getRightPos()==1) {
384 cr.addDeclaration("int", right.getSafeSymbol());
385 cr.outputline(right.getSafeSymbol()+"="+slot1+";");
386 } else if (u.getRightPos()==2) {
387 cr.addDeclaration("int", right.getSafeSymbol());
388 cr.outputline(right.getSafeSymbol()+"="+slot2+";");
389 } else throw new Error("Error w/ Position");
395 if (u.getType()==Updates.ACCESSPATH) {
396 VarDescriptor newright=VarDescriptor.makeNew("right");
397 generate_accesspath(cr, right,newright,u);
400 VarDescriptor left=VarDescriptor.makeNew("left");
401 u.getLeftExpr().generate(cr,left);
402 Opcode op=u.getOpcode();
403 cr.outputline("if (!("+left.getSafeSymbol()+op+right.getSafeSymbol()+"))");
407 cr.outputline(right.getSafeSymbol()+"++;");
408 else if (op==Opcode.GE)
410 else if (op==Opcode.EQ)
412 else if (op==Opcode.NE)
413 cr.outputline(right.getSafeSymbol()+"++;");
414 else if (op==Opcode.LT)
415 cr.outputline(right.getSafeSymbol()+"--;");
416 else if (op==Opcode.LE)
418 else throw new Error();
420 VarDescriptor vd=((VarExpr)u.getLeftExpr()).getVar();
421 cr.outputline(vd.getSafeSymbol()+"="+right.getSafeSymbol()+";");
422 } else if (u.isField()) {
424 Expr subexpr=((DotExpr)u.getLeftExpr()).getExpr();
425 Expr intindex=((DotExpr)u.getLeftExpr()).getIndex();
426 VarDescriptor subvd=VarDescriptor.makeNew("subexpr");
427 VarDescriptor indexvd=VarDescriptor.makeNew("index");
428 subexpr.generate(cr,subvd);
430 intindex.generate(cr,indexvd);
431 FieldDescriptor fd=(FieldDescriptor)u.getDescriptor();
432 StructureTypeDescriptor std=(StructureTypeDescriptor)subexpr.getType();
433 Expr offsetbits = std.getOffsetExpr(fd);
434 if (fd instanceof ArrayDescriptor) {
435 fd = ((ArrayDescriptor) fd).getField();
438 if (intindex != null) {
439 Expr basesize = fd.getBaseSizeExpr();
440 offsetbits = new OpExpr(Opcode.ADD, offsetbits, new OpExpr(Opcode.MULT, basesize, intindex));
442 Expr offsetbytes = new OpExpr(Opcode.SHR, offsetbits,new IntegerLiteralExpr(3));
443 Expr byteaddress=new OpExpr(Opcode.ADD, offsetbytes, subexpr);
444 VarDescriptor addr=VarDescriptor.makeNew("byteaddress");
445 byteaddress.generate(cr,addr);
447 if (fd.getType() instanceof ReservedTypeDescriptor && !fd.getPtr()) {
448 ReservedTypeDescriptor rtd=(ReservedTypeDescriptor)fd.getType();
449 if (rtd==ReservedTypeDescriptor.INT) {
450 cr.outputline("*((int *) "+addr.getSafeSymbol()+")="+right.getSafeSymbol()+";");
451 } else if (rtd==ReservedTypeDescriptor.SHORT) {
452 cr.outputline("*((short *) "+addr.getSafeSymbol()+")="+right.getSafeSymbol()+";");
453 } else if (rtd==ReservedTypeDescriptor.BYTE) {
454 cr.outputline("*((char *) "+addr.getSafeSymbol()+")="+right.getSafeSymbol()+";");
455 } else if (rtd==ReservedTypeDescriptor.BIT) {
456 Expr tmp = new OpExpr(Opcode.SHL, offsetbytes, new IntegerLiteralExpr(3));
457 Expr offset=new OpExpr(Opcode.SUB, offsetbits, tmp);
458 Expr mask=new OpExpr(Opcode.SHL, new IntegerLiteralExpr(1), offset);
459 VarDescriptor maskvar=VarDescriptor.makeNew("mask");
460 mask.generate(cr,maskvar);
461 cr.outputline("*((char *) "+addr.getSafeSymbol()+")|="+maskvar.getSafeSymbol()+";");
462 cr.outputline("if (!"+right.getSafeSymbol()+")");
463 cr.outputline("*((char *) "+addr.getSafeSymbol()+")^="+maskvar.getSafeSymbol()+";");
464 } else throw new Error();
467 cr.outputline("*((int *) "+addr.getSafeSymbol()+")="+right.getSafeSymbol()+";");
475 private void generate_accesspath(CodeWriter cr, VarDescriptor right, VarDescriptor newright, Updates u) {
476 Vector dotvector=new Vector();
477 Expr ptr=u.getRightExpr();
478 VarExpr rightve=new VarExpr(right);
479 right.td=ReservedTypeDescriptor.INT;
482 /* Does something other than a dereference? */
484 if (ptr instanceof DotExpr)
485 ptr=((DotExpr)ptr).left;
486 else if (ptr instanceof CastExpr)
487 ptr=((CastExpr)ptr).getExpr();
488 if (ptr instanceof VarExpr) {
489 /* Finished constructing vector */
493 ArrayAnalysis.AccessPath ap=u.getAccessPath();
494 VarDescriptor init=VarDescriptor.makeNew("init");
496 cr.addDeclaration("int", init.getSafeSymbol());
497 cr.outputline(init.getSafeSymbol()+"= SimpleHashfirstkey("+ap.getSet().getSafeSymbol()+"_hash);");
498 init.td=ap.getSet().getType();
502 Expr newexpr=new VarExpr(init);
504 for(int i=dotvector.size()-1;i>=0;i--) {
505 Expr e=(Expr)dotvector.get(i);
506 if (e instanceof CastExpr) {
508 newexpr=new CastExpr(((CastExpr)e).getType(),newexpr);
509 } else if (e instanceof DotExpr) {
510 DotExpr de=(DotExpr)e;
511 if (de.getField() instanceof ArrayDescriptor) {
512 DotExpr de2=new DotExpr(newexpr,de.field,new IntegerLiteralExpr(0));
514 de2.fieldtype=de.fieldtype;
516 OpExpr offset=new OpExpr(Opcode.SUB,rightve,de2);
517 OpExpr index=new OpExpr(Opcode.DIV,offset,de.fieldtype.getSizeExpr());
518 if (u.getRightPos()==apindex) {
519 index.generate(cr,newright);
522 DotExpr de3=new DotExpr(newexpr,de.field,index);
525 de3.fieldtype=de.fieldtype;
529 DotExpr de2=new DotExpr(newexpr,de.field,null);
531 de2.fieldtype=de.fieldtype;
536 } else throw new Error();
541 private void generate_bindings(CodeWriter cr, String slot0, String slot1) {
542 for(int i=0;i<bindings.size();i++) {
543 Binding b=(Binding)bindings.get(i);
545 if (b.getType()==Binding.SEARCH) {
546 VarDescriptor vd=b.getVar();
547 cr.addDeclaration(vd.getType().getGenerateType().getSafeSymbol(), vd.getSafeSymbol());
548 cr.outputline(vd.getSafeSymbol()+"=SimpleHashfirstkey("+b.getSet().getSafeSymbol()+"_hash);");
549 } else if (b.getType()==Binding.CREATE) {
550 throw new Error("Creation not supported");
551 // source.generateSourceAlloc(cr,vd,b.getSet());
553 VarDescriptor vd=b.getVar();
554 switch(b.getPosition()) {
556 cr.addDeclaration(vd.getType().getGenerateType().getSafeSymbol(), vd.getSafeSymbol());
557 cr.outputline(vd.getSafeSymbol()+"="+slot0+";");
560 cr.addDeclaration(vd.getType().getGenerateType().getSafeSymbol(), vd.getSafeSymbol());
561 cr.outputline(vd.getSafeSymbol()+"="+slot1+";");
564 throw new Error("Slot >1 doesn't exist.");