7 public class Termination {
9 Hashtable conjunctionmap;
11 HashSet abstractrepair;
12 HashSet abstractrepairadd;
15 HashSet consequencenodes;
18 Hashtable scopesatisfy;
19 Hashtable scopefalsify;
20 Hashtable consequence;
21 Hashtable abstractadd;
22 Hashtable abstractremove;
23 Hashtable conjtonodemap;
24 Hashtable predtoabstractmap;
26 ComputeMaxSize maxsize;
28 AbstractInterferes abstractinterferes;
29 ConcreteInterferes concreteinterferes;
30 ConstraintDependence constraintdependence;
32 ArrayAnalysis arrayanalysis;
35 public Termination(State state) {
37 conjunctions=new HashSet();
38 conjunctionmap=new Hashtable();
39 abstractrepair=new HashSet();
40 abstractrepairadd=new HashSet();
41 scopenodes=new HashSet();
42 scopesatisfy=new Hashtable();
43 scopefalsify=new Hashtable();
44 consequence=new Hashtable();
45 updatenodes=new HashSet();
46 consequencenodes=new HashSet();
47 abstractadd=new Hashtable();
48 abstractremove=new Hashtable();
49 conjtonodemap=new Hashtable();
50 predtoabstractmap=new Hashtable();
55 for(int i=0;i<state.vRules.size();i++)
56 System.out.println(state.vRules.get(i));
57 for(int i=0;i<state.vConstraints.size();i++)
58 System.out.println(state.vConstraints.get(i));
60 sources=new Sources(state);
61 maxsize=new ComputeMaxSize(state);
62 exactsize=new ExactSize(state);
63 arrayanalysis=new ArrayAnalysis(state,this);
65 abstractinterferes=new AbstractInterferes(this);
66 concreteinterferes=new ConcreteInterferes(this);
67 generateconjunctionnodes();
68 constraintdependence=new ConstraintDependence(state,this);
71 generaterepairnodes();
72 generatedatastructureupdatenodes();
73 generatecompensationnodes();
75 generateabstractedges();
77 generateupdateedges();
80 HashSet superset=new HashSet();
81 superset.addAll(conjunctions);
82 HashSet closureset=new HashSet();
84 GraphNode.computeclosure(superset,closureset);
86 GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
87 } catch (Exception e) {
91 for(Iterator it=updatenodes.iterator();it.hasNext();) {
92 GraphNode gn=(GraphNode)it.next();
93 TermNode tn=(TermNode)gn.getOwner();
94 MultUpdateNode mun=tn.getUpdate();
95 System.out.println(gn.getTextLabel());
96 System.out.println(mun.toString());
98 GraphAnalysis ga=new GraphAnalysis(this);
99 removedset=ga.doAnalysis();
100 if (removedset==null) {
101 System.out.println("Can't generate terminating repair algorithm!");
105 System.out.println("Removing:");
106 for(Iterator it=removedset.iterator();it.hasNext();) {
107 GraphNode gn=(GraphNode)it.next();
108 System.out.println(gn.getTextLabel());
111 superset=new HashSet();
112 superset.addAll(conjunctions);
113 superset.removeAll(removedset);
114 GraphNode.computeclosure(superset,removedset);
116 GraphNode.DOTVisitor.visit(new FileOutputStream("graphfinal.dot"),superset);
117 } catch (Exception e) {
121 constraintdependence.traversedependences(this);
125 /** This method generates a node for each conjunction in the DNF
126 * form of each constraint. It also converts the quantifiers into
127 * conjunctions also - constraints can be satisfied by removing
128 * items from the sets and relations they are quantified over */
130 void generateconjunctionnodes() {
131 Vector constraints=state.vConstraints;
132 // Constructs conjunction nodes
133 for(int i=0;i<constraints.size();i++) {
134 Constraint c=(Constraint)constraints.get(i);
135 DNFConstraint dnf=c.dnfconstraint;
136 for(int j=0;j<dnf.size();j++) {
137 TermNode tn=new TermNode(c,dnf.get(j));
138 GraphNode gn=new GraphNode("Conj"+i+"A"+j,
139 "Conj ("+i+","+j+") "+dnf.get(j).name()
141 conjunctions.add(gn);
142 if (!conjunctionmap.containsKey(c))
143 conjunctionmap.put(c,new HashSet());
144 ((Set)conjunctionmap.get(c)).add(gn);
145 conjtonodemap.put(dnf.get(j),gn);
147 // Construct quantifier "conjunction" nodes
148 for(int j=0;j<c.numQuantifiers();j++) {
149 Quantifier q=c.getQuantifier(j);
150 if (q instanceof SetQuantifier) {
151 SetQuantifier sq=(SetQuantifier)q;
152 VarExpr ve=new VarExpr(sq.getVar());
153 InclusionPredicate ip=new InclusionPredicate(ve,new SetExpr(sq.getSet()));
154 DNFConstraint dconst=new DNFConstraint(ip);
156 TermNode tn=new TermNode(c,dconst.get(0));
157 tn.setquantifiernode();
158 GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
159 "Conj ("+i+","+j+") "+dconst.get(0).name()
161 conjunctions.add(gn);
162 if (!conjunctionmap.containsKey(c))
163 conjunctionmap.put(c,new HashSet());
164 ((Set)conjunctionmap.get(c)).add(gn);
165 conjtonodemap.put(dconst.get(0),gn);
167 } else if (q instanceof RelationQuantifier) {
168 RelationQuantifier rq=(RelationQuantifier)q;
169 VarExpr ve=new VarExpr(rq.y);
170 InclusionPredicate ip=new InclusionPredicate(ve,new ImageSetExpr(rq.x,rq.getRelation()));
171 DNFConstraint dconst=new DNFConstraint(ip);
173 TermNode tn=new TermNode(c,dconst.get(0));
174 tn.setquantifiernode();
175 GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
176 "Conj ("+i+","+j+") "+dconst.get(0).name()
178 conjunctions.add(gn);
179 if (!conjunctionmap.containsKey(c))
180 conjunctionmap.put(c,new HashSet());
181 ((Set)conjunctionmap.get(c)).add(gn);
182 conjtonodemap.put(dconst.get(0),gn);
189 void generateupdateedges() {
190 for(Iterator updateiterator=updatenodes.iterator();updateiterator.hasNext();) {
191 GraphNode gn=(GraphNode)updateiterator.next();
192 TermNode tn=(TermNode)gn.getOwner();
193 MultUpdateNode mun=tn.getUpdate();
194 for(int i=0;i<mun.numUpdates();i++) {
195 UpdateNode un=mun.getUpdate(i);
196 for(int j=0;j<un.numUpdates();j++) {
197 Updates u=un.getUpdate(j);
198 if (u.getType()==Updates.ABSTRACT) {
199 Expr e=u.getLeftExpr();
200 boolean negated=u.negate;
201 if (e instanceof TupleOfExpr) {
202 TupleOfExpr toe=(TupleOfExpr)e;
204 GraphNode agn=(GraphNode)abstractremove.get(toe.relation);
205 GraphNode.Edge edge=new GraphNode.Edge("requires",agn);
208 GraphNode agn=(GraphNode)abstractadd.get(toe.relation);
209 GraphNode.Edge edge=new GraphNode.Edge("requires",agn);
212 } else if (e instanceof ElementOfExpr) {
213 ElementOfExpr eoe=(ElementOfExpr)e;
215 GraphNode agn=(GraphNode)abstractremove.get(eoe.set);
216 GraphNode.Edge edge=new GraphNode.Edge("requires",agn);
219 GraphNode agn=(GraphNode)abstractadd.get(eoe.set);
220 GraphNode.Edge edge=new GraphNode.Edge("requires",agn);
223 } else throw new Error("Unrecognized Abstract Update");
228 /* Cycle through the rules to look for possible conflicts */
229 for(int i=0;i<state.vRules.size();i++) {
230 Rule r=(Rule) state.vRules.get(i);
231 if (concreteinterferes.interferes(mun,r,true)) {
232 GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
233 GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
236 if (concreteinterferes.interferes(mun,r,false)) {
237 GraphNode scopenode=(GraphNode)scopefalsify.get(r);
238 GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
245 void generateabstractedges() {
246 for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
247 GraphNode gn=(GraphNode)absiterator.next();
248 TermNode tn=(TermNode)gn.getOwner();
249 AbstractRepair ar=(AbstractRepair)tn.getAbstract();
251 for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
252 GraphNode gn2=(GraphNode)conjiterator.next();
253 TermNode tn2=(TermNode)gn2.getOwner();
254 Conjunction conj=tn2.getConjunction();
255 Constraint cons=tn2.getConstraint();
257 for(int i=0;i<conj.size();i++) {
258 DNFPredicate dp=conj.get(i);
259 if (AbstractInterferes.interferes(ar,cons)||
260 abstractinterferes.interferes(ar,dp)) {
261 GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
268 for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
269 GraphNode gn2=(GraphNode)scopeiterator.next();
270 TermNode tn2=(TermNode)gn2.getOwner();
271 ScopeNode sn2=tn2.getScope();
272 if (AbstractInterferes.interferes(ar,sn2.getRule(),sn2.getSatisfy())) {
273 GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
280 void generatescopenodes() {
281 for(int i=0;i<state.vRules.size();i++) {
282 Rule r=(Rule) state.vRules.get(i);
283 ScopeNode satisfy=new ScopeNode(r,true);
284 TermNode tnsatisfy=new TermNode(satisfy);
285 GraphNode gnsatisfy=new GraphNode("SatisfyRule"+i,tnsatisfy);
286 ConsequenceNode cnsatisfy=new ConsequenceNode();
287 TermNode ctnsatisfy=new TermNode(cnsatisfy);
288 GraphNode cgnsatisfy=new GraphNode("ConseqSatisfyRule"+i,ctnsatisfy);
289 consequence.put(satisfy,cgnsatisfy);
290 GraphNode.Edge esat=new GraphNode.Edge("consequencesatisfy"+i,cgnsatisfy);
291 gnsatisfy.addEdge(esat);
292 consequencenodes.add(cgnsatisfy);
293 scopesatisfy.put(r,gnsatisfy);
294 scopenodes.add(gnsatisfy);
296 ScopeNode falsify=new ScopeNode(r,false);
297 TermNode tnfalsify=new TermNode(falsify);
298 GraphNode gnfalsify=new GraphNode("FalsifyRule"+i,tnfalsify);
299 ConsequenceNode cnfalsify=new ConsequenceNode();
300 TermNode ctnfalsify=new TermNode(cnfalsify);
301 GraphNode cgnfalsify=new GraphNode("ConseqFalsifyRule"+i,ctnfalsify);
302 consequence.put(falsify,cgnfalsify);
303 GraphNode.Edge efals=new GraphNode.Edge("consequencefalsify"+i,cgnfalsify);
304 gnfalsify.addEdge(efals);
305 consequencenodes.add(cgnfalsify);
306 scopefalsify.put(r,gnfalsify);
307 scopenodes.add(gnfalsify);
311 void generatescopeedges() {
312 for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
313 GraphNode gn=(GraphNode)scopeiterator.next();
314 TermNode tn=(TermNode)gn.getOwner();
315 ScopeNode sn=tn.getScope();
317 /* Interference edges with conjunctions */
318 for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
319 GraphNode gn2=(GraphNode)conjiterator.next();
320 TermNode tn2=(TermNode)gn2.getOwner();
321 Conjunction conj=tn2.getConjunction();
322 Constraint constr=tn2.getConstraint();
323 for(int i=0;i<conj.size();i++) {
324 DNFPredicate dp=conj.get(i);
325 if (abstractinterferes.interferes(sn,dp)||
326 AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),constr)) {
327 GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
328 GraphNode gnconseq=(GraphNode)consequence.get(sn);
335 /* Now see if this could effect other model defintion rules */
336 for(int i=0;i<state.vRules.size();i++) {
337 Rule r=(Rule) state.vRules.get(i);
338 if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,true)) {
339 GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
340 GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
341 GraphNode gnconseq=(GraphNode)consequence.get(sn);
344 if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,false)) {
345 GraphNode scopenode=(GraphNode)scopefalsify.get(r);
346 GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
347 GraphNode gnconseq=(GraphNode)consequence.get(sn);
354 /** This method generates the abstract repair nodes. */
355 void generaterepairnodes() {
356 /* Generate repairs of conjunctions */
357 for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
358 GraphNode gn=(GraphNode)conjiterator.next();
359 TermNode tn=(TermNode)gn.getOwner();
360 Conjunction conj=tn.getConjunction();
361 for(int i=0;i<conj.size();i++) {
362 DNFPredicate dp=conj.get(i);
363 int[] array=dp.getPredicate().getRepairs(dp.isNegated(),this);
364 Descriptor d=dp.getPredicate().getDescriptor();
365 for(int j=0;j<array.length;j++) {
366 AbstractRepair ar=new AbstractRepair(dp,array[j],d);
367 TermNode tn2=new TermNode(ar);
368 GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),gn.getTextLabel()+" #"+i+" "+ar.type(),tn2);
369 GraphNode.Edge e=new GraphNode.Edge("abstract",gn2);
371 if (!predtoabstractmap.containsKey(dp))
372 predtoabstractmap.put(dp,new HashSet());
373 ((Set)predtoabstractmap.get(dp)).add(gn2);
374 abstractrepair.add(gn2);
378 /* Generate additional abstract repairs */
379 Vector setdescriptors=state.stSets.getAllDescriptors();
380 for(int i=0;i<setdescriptors.size();i++) {
381 SetDescriptor sd=(SetDescriptor)setdescriptors.get(i);
383 VarExpr ve=new VarExpr("DUMMY");
384 InclusionPredicate ip=new InclusionPredicate(ve,new SetExpr(sd));
385 DNFPredicate tp=new DNFPredicate(false,ip);
386 AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTOSET, sd);
387 TermNode tn=new TermNode(ar);
388 GraphNode gn=new GraphNode("AbstractAddSetRule"+i,tn);
389 if (!predtoabstractmap.containsKey(tp))
390 predtoabstractmap.put(tp,new HashSet());
391 ((Set)predtoabstractmap.get(tp)).add(gn);
392 abstractrepair.add(gn);
393 abstractrepairadd.add(gn);
394 abstractadd.put(sd,gn);
396 DNFPredicate tp2=new DNFPredicate(true,ip);
397 AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMSET, sd);
398 TermNode tn2=new TermNode(ar2);
399 GraphNode gn2=new GraphNode("AbstractRemSetRule"+i,tn2);
400 if (!predtoabstractmap.containsKey(tp2))
401 predtoabstractmap.put(tp2,new HashSet());
402 ((Set)predtoabstractmap.get(tp2)).add(gn2);
403 abstractrepair.add(gn2);
404 abstractrepairadd.add(gn2);
405 abstractremove.put(sd,gn2);
408 Vector relationdescriptors=state.stRelations.getAllDescriptors();
409 for(int i=0;i<relationdescriptors.size();i++) {
410 RelationDescriptor rd=(RelationDescriptor)relationdescriptors.get(i);
411 VarDescriptor vd1=new VarDescriptor("DUMMY1");
412 VarExpr ve2=new VarExpr("DUMMY2");
414 InclusionPredicate ip=new InclusionPredicate(ve2,new ImageSetExpr(vd1, rd));
416 DNFPredicate tp=new DNFPredicate(false,ip);
417 AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTORELATION, rd);
418 TermNode tn=new TermNode(ar);
419 GraphNode gn=new GraphNode("AbstractAddRelRule"+i,tn);
420 if (!predtoabstractmap.containsKey(tp))
421 predtoabstractmap.put(tp,new HashSet());
422 ((Set)predtoabstractmap.get(tp)).add(gn);
423 abstractrepair.add(gn);
424 abstractrepairadd.add(gn);
425 abstractadd.put(rd,gn);
427 DNFPredicate tp2=new DNFPredicate(true,ip);
428 AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMRELATION, rd);
429 TermNode tn2=new TermNode(ar2);
430 GraphNode gn2=new GraphNode("AbstractRemRelRule"+i,tn2);
431 if (!predtoabstractmap.containsKey(tp2))
432 predtoabstractmap.put(tp2,new HashSet());
433 ((Set)predtoabstractmap.get(tp2)).add(gn2);
434 abstractrepair.add(gn2);
435 abstractrepairadd.add(gn2);
436 abstractremove.put(rd,gn2);
440 int compensationcount=0;
441 void generatecompensationnodes() {
442 for(int i=0;i<state.vRules.size();i++) {
443 Rule r=(Rule) state.vRules.get(i);
444 Vector possiblerules=new Vector();
446 for(int j=0;j<(r.numQuantifiers()+r.getDNFNegGuardExpr().size());j++) {
447 GraphNode gn=(GraphNode)scopesatisfy.get(r);
448 TermNode tn=(TermNode) gn.getOwner();
449 ScopeNode sn=tn.getScope();
450 MultUpdateNode mun=new MultUpdateNode(sn);
451 TermNode tn2=new TermNode(mun);
452 GraphNode gn2=new GraphNode("CompRem"+compensationcount,tn2);
453 UpdateNode un=new UpdateNode(r);
455 if (j<r.numQuantifiers()) {
456 /* Remove quantifier */
457 Quantifier q=r.getQuantifier(j);
458 if (q instanceof RelationQuantifier) {
459 RelationQuantifier rq=(RelationQuantifier)q;
460 TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
461 toe.td=ReservedTypeDescriptor.INT;
462 Updates u=new Updates(toe,true);
464 if (abstractremove.containsKey(rq.relation)) {
465 GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
466 GraphNode.Edge e=new GraphNode.Edge("requires",agn);
469 continue; /* Abstract repair doesn't exist */
471 } else if (q instanceof SetQuantifier) {
472 SetQuantifier sq=(SetQuantifier)q;
473 ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
474 eoe.td=ReservedTypeDescriptor.INT;
475 Updates u=new Updates(eoe,true);
477 if (abstractremove.containsKey(sq.set)) {
478 GraphNode agn=(GraphNode)abstractremove.get(sq.set);
479 GraphNode.Edge e=new GraphNode.Edge("requires",agn);
482 continue; /* Abstract repair doesn't exist */
488 /* Negate conjunction */
489 int c=j-r.numQuantifiers();
490 if (!processconjunction(un,r.getDNFNegGuardExpr().get(c))) {
494 if (!un.checkupdates()) /* Make sure we have a good update */
498 GraphNode.Edge e=new GraphNode.Edge("abstract"+compensationcount,gn2);
501 updatenodes.add(gn2);
506 void generatedatastructureupdatenodes() {
507 for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
508 GraphNode gn=(GraphNode)absiterator.next();
509 TermNode tn=(TermNode) gn.getOwner();
510 AbstractRepair ar=tn.getAbstract();
511 if (ar.getType()==AbstractRepair.ADDTOSET) {
512 generateaddtosetrelation(gn,ar);
513 } else if (ar.getType()==AbstractRepair.REMOVEFROMSET) {
514 generateremovefromsetrelation(gn,ar);
515 } else if (ar.getType()==AbstractRepair.ADDTORELATION) {
516 generateaddtosetrelation(gn,ar);
517 } else if (ar.getType()==AbstractRepair.REMOVEFROMRELATION) {
518 generateremovefromsetrelation(gn,ar);
519 } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
520 /* Generate remove/add pairs */
521 generateremovefromsetrelation(gn,ar);
522 generateaddtosetrelation(gn,ar);
523 /* Generate atomic modify */
524 generatemodifyrelation(gn,ar);
530 /** This method generates concrete data structure updates which
531 * remove an object (or tuple) from a set (or relation).*/
533 int removefromcount=0;
534 void generateremovefromsetrelation(GraphNode gn,AbstractRepair ar) {
535 /* Construct the set of all rules which could add something to the given set or relation */
537 Vector possiblerules=new Vector();
538 for(int i=0;i<state.vRules.size();i++) {
539 Rule r=(Rule) state.vRules.get(i);
540 if ((r.getInclusion() instanceof SetInclusion)&&
541 (ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()))
542 possiblerules.add(r);
543 if ((r.getInclusion() instanceof RelationInclusion)&&
544 (ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation()))
545 possiblerules.add(r);
547 if (possiblerules.size()==0)
550 /* Loop through different ways of falsifying each of these rules */
551 int[] count=new int[possiblerules.size()];
552 while(remains(count,possiblerules,true)) {
553 MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.REMOVE);
554 TermNode tn=new TermNode(mun);
555 GraphNode gn2=new GraphNode("UpdateRem"+removefromcount,tn);
557 boolean goodflag=true;
558 for(int i=0;i<possiblerules.size();i++) {
559 Rule r=(Rule)possiblerules.get(i);
560 UpdateNode un=new UpdateNode(r);
562 if (count[i]<r.numQuantifiers()) {
563 /* Remove quantifier */
564 Quantifier q=r.getQuantifier(count[i]);
565 if (q instanceof RelationQuantifier) {
566 RelationQuantifier rq=(RelationQuantifier)q;
567 TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
568 toe.td=ReservedTypeDescriptor.INT;
569 Updates u=new Updates(toe,true);
571 if (abstractremove.containsKey(rq.relation)) {
572 GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
573 GraphNode.Edge e=new GraphNode.Edge("requires",agn);
576 goodflag=false;break; /* Abstract repair doesn't exist */
578 } else if (q instanceof SetQuantifier) {
579 SetQuantifier sq=(SetQuantifier)q;
580 ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
581 eoe.td=ReservedTypeDescriptor.INT;
582 Updates u=new Updates(eoe,true);
584 if (abstractremove.containsKey(sq.set)) {
585 GraphNode agn=(GraphNode)abstractremove.get(sq.set);
586 GraphNode.Edge e=new GraphNode.Edge("requires",agn);
589 goodflag=false;break; /* Abstract repair doesn't exist */
591 } else {goodflag=false;break;}
593 int c=count[i]-r.numQuantifiers();
594 if (!processconjunction(un,r.getDNFNegGuardExpr().get(c))) {
595 goodflag=false;break;
598 if (!un.checkupdates()) {
605 GraphNode.Edge e=new GraphNode.Edge("abstract"+removefromcount,gn2);
608 updatenodes.add(gn2);
610 increment(count,possiblerules,true);
614 /** This method increments to the next possibility. */
616 static private void increment(int count[], Vector rules,boolean isremove) {
618 for(int i=0;i<(rules.size()-1);i++) {
619 int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size();
628 /** This method test if there remain any possibilities to loop
630 static private boolean remains(int count[], Vector rules, boolean isremove) {
631 for(int i=0;i<rules.size();i++) {
632 int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size();
640 /** This method generates data structure updates to implement the
641 * abstract atomic modification specified by ar. */
644 void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {
645 RelationDescriptor rd=(RelationDescriptor)ar.getDescriptor();
646 ExprPredicate exprPredicate=(ExprPredicate)ar.getPredicate().getPredicate();
647 boolean inverted=exprPredicate.inverted();
655 // construct set of possible rules
656 Vector possiblerules=new Vector();
657 for(int i=0;i<state.vRules.size();i++) {
658 Rule r=(Rule) state.vRules.get(i);
659 if ((r.getInclusion() instanceof RelationInclusion)&&
660 (rd==((RelationInclusion)r.getInclusion()).getRelation()))
661 possiblerules.add(r);
663 if (possiblerules.size()==0)
666 // increment through this set
667 int[] count=new int[possiblerules.size()];
668 while(remains(count,possiblerules,false)) {
669 MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.MODIFY);
670 TermNode tn=new TermNode(mun);
671 GraphNode gn2=new GraphNode("UpdateMod"+removefromcount,tn);
673 boolean goodflag=true;
674 for(int i=0;i<possiblerules.size();i++) {
675 Rule r=(Rule)possiblerules.get(i);
676 UpdateNode un=new UpdateNode(r);
679 if (!processconjunction(un,r.getDNFGuardExpr().get(c))) {
680 goodflag=false;break;
682 RelationInclusion ri=(RelationInclusion)r.getInclusion();
683 if (!(ri.getLeftExpr() instanceof VarExpr)) {
684 if (ri.getLeftExpr().isValue()) {
685 Updates up=new Updates(ri.getLeftExpr(),leftindex);
690 else un.addInvariant(ri.getLeftExpr());
693 VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
695 Updates up=new Updates(ri.getLeftExpr(),leftindex);
700 if (!(ri.getRightExpr() instanceof VarExpr)) {
701 if (ri.getRightExpr().isValue()) {
702 Updates up=new Updates(ri.getRightExpr(),rightindex);
708 un.addInvariant(ri.getLeftExpr());
711 VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
713 Updates up=new Updates(ri.getRightExpr(),rightindex);
715 } else if (!inverted)
719 if (!un.checkupdates()) {
726 GraphNode.Edge e=new GraphNode.Edge("abstract"+modifycount,gn2);
729 updatenodes.add(gn2);
731 increment(count,possiblerules,false);
735 /** Generate concrete data structure update to add an object(or
736 * tuple) to a set (or relation). */
738 static int addtocount=0;
739 void generateaddtosetrelation(GraphNode gn, AbstractRepair ar) {
740 for(int i=0;i<state.vRules.size();i++) {
741 Rule r=(Rule) state.vRules.get(i);
742 /* See if this is a good rule*/
743 if ((r.getInclusion() instanceof SetInclusion&&
744 ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
745 (r.getInclusion() instanceof RelationInclusion&&
746 ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation())) {
748 /* First solve for quantifiers */
749 Vector bindings=new Vector();
750 /* Construct bindings */
751 if (!constructbindings(bindings,r,false))
753 //Generate add instruction
754 DNFRule dnfrule=r.getDNFGuardExpr();
755 for(int j=0;j<dnfrule.size();j++) {
756 Inclusion inc=r.getInclusion();
757 UpdateNode un=new UpdateNode(r);
758 un.addBindings(bindings);
759 /* Now build update for tuple/set inclusion condition */
760 if(inc instanceof SetInclusion) {
761 SetInclusion si=(SetInclusion)inc;
762 if (!(si.elementexpr instanceof VarExpr)) {
763 if (si.elementexpr.isValue()) {
764 Updates up=new Updates(si.elementexpr,0);
767 /* We're an add to set*/
768 System.out.println("Rule: "+r);
769 ArrayAnalysis.AccessPath rap=arrayanalysis.analyzeExpr(r,si.elementexpr);
770 System.out.println("Attempting perform array add");
771 SetDescriptor set=sources.setSource(si.getSet())?
772 sources.getSourceSet(si.getSet()):null;
775 System.out.println("Non-null source set");
776 ArrayAnalysis.AccessPath ap=arrayanalysis.getSet(set);
777 if (rap==ArrayAnalysis.AccessPath.NONE)
779 System.out.println("A");
782 System.out.println("B");
783 if (!constructarrayupdate(un, si.elementexpr, rap, 0))
785 System.out.println("C");
788 VarDescriptor vd=((VarExpr)si.elementexpr).getVar();
790 Updates up=new Updates(si.elementexpr,0);
794 } else if (inc instanceof RelationInclusion) {
795 RelationInclusion ri=(RelationInclusion)inc;
796 if (!(ri.getLeftExpr() instanceof VarExpr)) {
797 if (ri.getLeftExpr().isValue()) {
798 Updates up=new Updates(ri.getLeftExpr(),0);
801 /* We don't handly relation modifies */
802 if (ar.getType()==AbstractRepair.MODIFYRELATION)
804 /* We're an add to relation*/
805 ArrayAnalysis.AccessPath rap=arrayanalysis.analyzeExpr(r,ri.getLeftExpr());
806 SetDescriptor set=sources.relsetSource(ri.getRelation(),true /* Domain*/)?
807 sources.relgetSourceSet(ri.getRelation(),true):null;
810 ArrayAnalysis.AccessPath ap=arrayanalysis.getSet(set);
812 if (rap==ArrayAnalysis.AccessPath.NONE||
814 !constructarrayupdate(un, ri.getLeftExpr(), rap, 0))
818 VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
820 Updates up=new Updates(ri.getLeftExpr(),0);
824 if (!(ri.getRightExpr() instanceof VarExpr)) {
825 if (ri.getRightExpr().isValue()) {
826 Updates up=new Updates(ri.getRightExpr(),1);
829 /* We don't handly relation modifies */
830 if (ar.getType()==AbstractRepair.MODIFYRELATION)
832 /* We're an add to relation*/
833 ArrayAnalysis.AccessPath rap=arrayanalysis.analyzeExpr(r,ri.getRightExpr());
834 SetDescriptor set=sources.relsetSource(ri.getRelation(),false /* Range*/)?
835 sources.relgetSourceSet(ri.getRelation(),false):null;
838 ArrayAnalysis.AccessPath ap=arrayanalysis.getSet(set);
840 if (rap==ArrayAnalysis.AccessPath.NONE||
842 !constructarrayupdate(un, ri.getRightExpr(), rap, 1))
846 VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
848 Updates up=new Updates(ri.getRightExpr(),1);
853 //Finally build necessary updates to satisfy conjunction
854 RuleConjunction ruleconj=dnfrule.get(j);
856 /* Add in updates for quantifiers */
857 MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.ADD);
858 TermNode tn=new TermNode(mun);
859 GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
861 if (processquantifiers(gn2,un, r)&&
862 processconjunction(un,ruleconj)&&
865 GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
868 updatenodes.add(gn2);
875 boolean constructarrayupdate(UpdateNode un, Expr lexpr, ArrayAnalysis.AccessPath ap, int slotnumber) {
876 System.out.println("Constructing array update");
878 for (int i=ap.numFields()-1;i>=0;i--) {
882 e=((DotExpr)e).getExpr();
884 while (e instanceof CastExpr)
885 e=((CastExpr)e).getExpr();
887 DotExpr de=(DotExpr)e;
888 FieldDescriptor fd=ap.getField(i);
889 if (fd instanceof ArrayDescriptor) {
890 // We have an ArrayDescriptor!
891 Expr index=de.getIndex();
892 if (!index.isValue()) {/* Not assignable */
893 System.out.println("ERROR:Index isn't assignable");
896 Updates updates=new Updates(index,i,ap,lexpr,slotnumber);
897 un.addUpdate(updates);
903 /** This method constructs bindings for an update using rule
904 * r. The boolean flag isremoval indicates that the update
905 * performs a removal. The function returns true if it is able to
906 * generate a valid set of bindings and false otherwise. */
908 boolean constructbindings(Vector bindings, Rule r, boolean isremoval) {
909 boolean goodupdate=true;
910 Inclusion inc=r.getInclusion();
911 for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
912 Quantifier q=(Quantifier)iterator.next();
913 if ((q instanceof SetQuantifier)||(q instanceof ForQuantifier)) {
914 VarDescriptor vd=null;
915 SetDescriptor set=null;
916 if (q instanceof SetQuantifier) {
917 vd=((SetQuantifier)q).getVar();
918 set=((SetQuantifier)q).getSet();
920 vd=((ForQuantifier)q).getVar();
922 if(inc instanceof SetInclusion) {
923 SetInclusion si=(SetInclusion)inc;
924 if ((si.elementexpr instanceof VarExpr)&&
925 (((VarExpr)si.elementexpr).getVar()==vd)) {
926 /* Can solve for v */
927 Binding binding=new Binding(vd,0);
928 bindings.add(binding);
932 } else if (inc instanceof RelationInclusion) {
933 RelationInclusion ri=(RelationInclusion)inc;
936 if ((ri.getLeftExpr() instanceof VarExpr)&&
937 (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
938 /* Can solve for v */
939 Binding binding=new Binding(vd,0);
940 bindings.add(binding);
942 if ((ri.getRightExpr() instanceof VarExpr)&&
943 (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
944 /* Can solve for v */
945 Binding binding=new Binding(vd,0);
946 bindings.add(binding);
950 } else throw new Error("Inclusion not recognized");
953 /* Removals don't need bindings anymore
954 Binding binding=new Binding(vd);
955 bindings.add(binding);*/
957 } else if (q instanceof SetQuantifier) {
958 /* Create new element to bind to */
959 // search if the set 'set' has a size
960 Binding binding=new Binding(vd,set,exactsize.getsize(set)==1);
961 bindings.add(binding);
966 } else if (q instanceof RelationQuantifier) {
967 RelationQuantifier rq=(RelationQuantifier)q;
968 for(int k=0;k<2;k++) {
969 VarDescriptor vd=(k==0)?rq.x:rq.y;
970 if(inc instanceof SetInclusion) {
971 SetInclusion si=(SetInclusion)inc;
972 if ((si.elementexpr instanceof VarExpr)&&
973 (((VarExpr)si.elementexpr).getVar()==vd)) {
974 /* Can solve for v */
975 Binding binding=new Binding(vd,0);
976 bindings.add(binding);
979 } else if (inc instanceof RelationInclusion) {
980 RelationInclusion ri=(RelationInclusion)inc;
983 if ((ri.getLeftExpr() instanceof VarExpr)&&
984 (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
985 /* Can solve for v */
986 Binding binding=new Binding(vd,0);
987 bindings.add(binding);
989 if ((ri.getRightExpr() instanceof VarExpr)&&
990 (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
991 /* Can solve for v */
992 Binding binding=new Binding(vd,0);
993 bindings.add(binding);
997 } else throw new Error("Inclusion not recognized");
1000 /* Removals don't need bindings anymore
1001 Binding binding=new Binding(vd);
1002 bindings.add(binding);*/
1009 } else throw new Error("Quantifier not recognized");
1014 /** Adds updates that add an item to the appropriate set or
1015 * relation quantified over by the model definition rule.. */
1017 boolean processquantifiers(GraphNode gn,UpdateNode un, Rule r) {
1018 Inclusion inc=r.getInclusion();
1019 for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
1020 Quantifier q=(Quantifier)iterator.next();
1021 /* Add quantifier */
1022 /* FIXME: Analysis to determine when this update is necessary */
1023 if (q instanceof RelationQuantifier) {
1024 RelationQuantifier rq=(RelationQuantifier)q;
1025 TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
1026 toe.td=ReservedTypeDescriptor.INT;
1027 Updates u=new Updates(toe,false);
1029 if (abstractadd.containsKey(rq.relation)) {
1030 GraphNode agn=(GraphNode)abstractadd.get(rq.relation);
1031 GraphNode.Edge e=new GraphNode.Edge("requires",agn);
1037 } else if (q instanceof SetQuantifier) {
1038 SetQuantifier sq=(SetQuantifier)q;
1039 if (un.getBinding(sq.var).getType()==Binding.SEARCH) {
1040 Binding b=un.getBinding(sq.var);
1041 Constraint reqc=exactsize.getConstraint(b.getSet());
1042 constraintdependence.requiresConstraint(gn,reqc);
1043 continue; /* Don't need to ensure addition for search */
1046 ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
1047 eoe.td=ReservedTypeDescriptor.INT;
1048 Updates u=new Updates(eoe,false);
1050 if (abstractadd.containsKey(sq.set)) {
1051 GraphNode agn=(GraphNode)abstractadd.get(sq.set);
1052 GraphNode.Edge e=new GraphNode.Edge("requires",agn);
1057 } else return false;
1062 /** This method generates the necessary updates to satisfy the
1063 * conjunction ruleconj. */
1065 boolean processconjunction(UpdateNode un,RuleConjunction ruleconj){
1067 for(int k=0;k<ruleconj.size();k++) {
1068 DNFExpr de=ruleconj.get(k);
1069 Expr e=de.getExpr();
1070 if (e instanceof OpExpr) {
1071 OpExpr ex=(OpExpr)de.getExpr();
1072 Opcode op=ex.getOpcode();
1073 Updates up=new Updates(ex.left,ex.right,op, de.getNegation());
1075 } else if (e instanceof ElementOfExpr) {
1076 Updates up=new Updates(e,de.getNegation());
1078 } else if (e instanceof TupleOfExpr) {
1079 Updates up=new Updates(e,de.getNegation());
1081 } else if (e instanceof BooleanLiteralExpr) {
1082 boolean truth=((BooleanLiteralExpr)e).getValue();
1083 if (de.getNegation())
1090 System.out.println(e.getClass().getName());
1091 throw new Error("Unrecognized Expr");
1097 public boolean analyzeQuantifiers(Quantifiers qs,Set set) {
1098 for(int i=0;i<qs.numQuantifiers();i++) {
1099 Quantifier q=qs.getQuantifier(i);
1100 if (set.contains(q))
1102 if (q instanceof SetQuantifier) {
1103 SetDescriptor sd=((SetQuantifier)q).getSet();
1104 if (maxsize.getsize(sd)<=1&&
1105 maxsize.getsize(sd)>=0)
1107 } else if (q instanceof RelationQuantifier) {
1108 RelationDescriptor rd=((RelationQuantifier)q).getRelation();
1109 if (maxsize.getsize(rd)<=1&&
1110 maxsize.getsize(rd)>=0)