Fixed some errors in the Repair Generator code.
[repair.git] / Repair / RepairCompiler / MCC / IR / ConstraintDependence.java
1 package MCC.IR;
2 import MCC.State;
3 import java.util.*;
4
5 public class ConstraintDependence {
6     State state;
7     HashSet constnodes;
8     HashSet nodes;
9     Hashtable constonode;
10     Hashtable nodetonode;
11     Termination termination;
12
13     ConstraintDependence(State state, Termination t) {
14         this.state=state;
15         this.termination=t;
16         constnodes=new HashSet();
17         nodes=new HashSet();
18         constonode=new Hashtable();
19         nodetonode=new Hashtable();
20         constructnodes();
21     }
22     
23     public Set computeOrdering() {
24         HashSet allnodes=new HashSet();
25         allnodes.addAll(constnodes);
26         allnodes.addAll(nodes);
27         boolean acyclic=GraphNode.DFS.depthFirstSearch(allnodes);
28         if (!acyclic) {
29             throw new Error("Cylic dependency between constraints.");
30         }
31         TreeSet topologicalsort = new TreeSet(new Comparator() {
32                 public boolean equals(Object obj) { return false; }
33                 public int compare(Object o1, Object o2) {
34                     GraphNode g1 = (GraphNode) o1;
35                     GraphNode g2 = (GraphNode) o2;
36                     return g1.getFinishingTime() - g2.getFinishingTime();
37                 }
38             });
39         
40         topologicalsort.addAll(constnodes);
41         return topologicalsort;
42     }
43
44     public void addNode(GraphNode gn) {
45         GraphNode gn2=new GraphNode(gn.getLabel(),gn.getTextLabel(),gn);
46         nodes.add(gn2);
47         nodetonode.put(gn,gn2);
48     }
49
50     public void associateWithConstraint(GraphNode gn, Constraint c) {
51         if (!nodetonode.containsKey(gn)) {
52             addNode(gn);
53         }
54         GraphNode ggn=(GraphNode)nodetonode.get(gn);
55         GraphNode gc=(GraphNode)constonode.get(c);
56         GraphNode.Edge e=new GraphNode.Edge("associated",ggn);
57         gc.addEdge(e);
58     }
59
60     public void requiresConstraint(GraphNode gn, Constraint c) {
61         if (!nodetonode.containsKey(gn)) {
62             addNode(gn);
63         }
64         GraphNode ggn=(GraphNode)nodetonode.get(gn);
65         GraphNode gc=(GraphNode)constonode.get(c);
66         GraphNode.Edge e=new GraphNode.Edge("requires",gc);
67         ggn.addEdge(e);
68     }
69
70     public void traversedependences(Termination termination) {
71         constructconjunctionnodes(termination);
72         constructconjunctionedges(termination);
73         Set removedset=termination.removedset;
74
75         for(int i=0;i<state.vConstraints.size();i++) {
76             Constraint c=(Constraint)state.vConstraints.get(i);
77             Set conjset=(Set)termination.conjunctionmap.get(c);
78             HashSet exploredset=new HashSet();
79
80             for(Iterator it=conjset.iterator();it.hasNext();) {
81                 GraphNode gn=(GraphNode)it.next();
82                 recursedependence(c,termination,exploredset,gn);
83             }
84         }
85     }
86
87     void recursedependence(Constraint c,Termination termination, HashSet exploredset, GraphNode gn) {
88         Set removedset=termination.removedset;
89         Set conjunctionset=termination.conjunctions;
90
91         if (removedset.contains(gn))
92             return;
93         exploredset.add(gn);
94         associateWithConstraint(gn,c);
95         for(Iterator it=gn.edges();it.hasNext();) {
96             GraphNode.Edge e=(GraphNode.Edge) it.next();
97             GraphNode gn2=e.getTarget();
98             if (!(exploredset.contains(gn2)||
99                   conjunctionset.contains(gn2)))
100                 recursedependence(c,termination,exploredset,gn2);
101         }
102     }
103
104     /** Constructs a node for each Constraint */
105     private void constructnodes() {
106         for(int i=0;i<state.vConstraints.size();i++) {
107             Constraint c=(Constraint)state.vConstraints.get(i);
108             GraphNode gn=new GraphNode(c.toString(),c);
109             constonode.put(c,gn);
110             constnodes.add(gn);
111         }
112     }
113     
114     private void constructconjunctionnodes(Termination termination) {
115         /*for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
116           GraphNode conjnode=(GraphNode)it.next();
117           TermNode tn=(TermNode)conjnode.getOwner();
118           Conjunction conj=tn.getConjunction();
119           addNode(conjnode);
120           }*/
121         Set removedset=termination.removedset;
122
123         for(int i=0;i<state.vConstraints.size();i++) {
124             Constraint c=(Constraint)state.vConstraints.get(i);
125             Set conjset=(Set)termination.conjunctionmap.get(c);
126             for(Iterator it=conjset.iterator();it.hasNext();) {
127                 GraphNode gn=(GraphNode)it.next();
128                 if (!removedset.contains(gn))
129                     associateWithConstraint(gn,c);
130             }
131         }
132     }
133
134     private void constructconjunctionedges(Termination termination) {
135         Set removedset=termination.removedset;
136         for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
137             GraphNode conjnode=(GraphNode)it.next();
138             if (removedset.contains(conjnode))
139                 continue;
140             
141             TermNode tn=(TermNode)conjnode.getOwner();
142             Conjunction conj=tn.getConjunction();
143             for(int i=0;i<conj.size();i++) {
144                 DNFPredicate dpred=conj.get(i);
145                 Predicate pred=dpred.getPredicate();
146                 Expr expr=null;
147                 if (pred instanceof InclusionPredicate) {
148                     InclusionPredicate ip=(InclusionPredicate)pred;
149                     expr=ip.expr;
150                 } else if (pred instanceof ExprPredicate) {
151                     ExprPredicate ep=(ExprPredicate)pred;
152                     expr=ep.expr;
153                 } else throw new Error("Unrecognized Predicate");
154                 Set functions=expr.getfunctions();
155                 if (functions==null)
156                     continue;
157                 for(Iterator fit=functions.iterator();fit.hasNext();) {
158                     Function f=(Function)fit.next();
159                     if (rulesensurefunction(state,f,false))
160                         continue; //no constraint needed to ensure
161
162                     Set s=providesfunction(f);
163                     if (s.size()==0) {
164                         System.out.println("Warning: No constraint ensures that [forall v in "+f.getSet()+"], size(v."+(f.isInverse()?"~":"")+f.getRelation()+")=1");
165                         continue;
166                     }
167                     Constraint c=(Constraint)s.iterator().next(); //Take the first one
168                     requiresConstraint(conjnode,c);
169                 }
170             }
171         }
172     }
173
174     /** This method determines whether the model definition rules
175      * ensure that the relation and evaluation domain descriped by f
176      * is either a function (if isPartial=false) or a partial function
177      * (if isPartial=true). */
178
179     static private boolean rulesensurefunction(State state,Function f, boolean isPartial) {
180         boolean foundrule=false;
181         for(int i=0;i<state.vRules.size();i++) {
182             Rule r=(Rule)state.vRules.get(i);
183             if (r.getInclusion().getTargetDescriptors().contains(f.getRelation())) {
184                 RelationInclusion ri=(RelationInclusion)r.getInclusion();
185                 Expr e=f.isInverse()?ri.getRightExpr():ri.getLeftExpr();
186                 SetDescriptor sd=e.getSet();
187                 if (sd==null)
188                     return false;
189                 if (state.setanalysis.noIntersection(f.getSet(),sd))
190                     continue; /* This rule doesn't effect the function */
191                 if (foundrule) /* two different rules are a problem */
192                     return false;
193                 if (!((e instanceof VarExpr)&&(r.numQuantifiers()==1)))
194                     return false;
195                 VarExpr ve=(VarExpr)e;
196                 Quantifier q=r.getQuantifier(0);
197                 if (!(q instanceof SetQuantifier))
198                     return false;
199                 SetQuantifier sq=(SetQuantifier)q;
200                 if (ve.getVar()!=sq.getVar())
201                     return false;
202                 if (!isPartial) {
203                     if (!sq.getSet().isSubset(f.getSet()))
204                         return false;
205                     if (!((r.getGuardExpr() instanceof BooleanLiteralExpr)&&
206                            ((BooleanLiteralExpr)r.getGuardExpr()).getValue()==true))
207                         return false;
208                 }
209                 Expr e2=f.isInverse()?ri.getLeftExpr():ri.getRightExpr();
210                 if (isPartial||e2.isSafe())
211                     foundrule=true;
212                 else
213                     return false;
214             }
215         }
216         return foundrule;
217     }
218  
219     private Set providesfunction(Function f) {
220         HashSet set=new HashSet();
221         for(int i=0;i<state.vConstraints.size();i++) {
222             Constraint c=(Constraint)state.vConstraints.get(i);
223             boolean goodconstraint=true;
224             DNFConstraint dnfconst=c.dnfconstraint;
225             for(int j=0;j<dnfconst.size();j++) {
226                 Conjunction conj=dnfconst.get(j);
227                 boolean conjprovides=false;
228                 for(int k=0;k<conj.size();k++) {
229                     DNFPredicate dpred=conj.get(k);
230                     if (!dpred.isNegated()&&
231                         (dpred.getPredicate() instanceof ExprPredicate)&&
232                         ((ExprPredicate)dpred.getPredicate()).getType()==ExprPredicate.SIZE) {
233                         ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
234                         if (ep.isRightInt()&&
235                             ep.rightSize()==1&&
236                             ep.getOp()==Opcode.EQ&&
237                             ep.inverted()==f.isInverse()&&
238                             ep.getDescriptor()==f.getRelation()) {
239                             ImageSetExpr se=(ImageSetExpr) ((SizeofExpr) ((OpExpr)ep.expr).left).getSetExpr();
240                             VarDescriptor vd=se.getVar();
241                             if (c.numQuantifiers()==1) {
242                                 for(int l=0;l<c.numQuantifiers();l++) {
243                                     Quantifier q=c.getQuantifier(l);
244                                     if (q instanceof SetQuantifier&&
245                                         ((SetQuantifier)q).getVar()==vd) {
246                                         SetDescriptor sd=((SetQuantifier)q).getSet();
247                                         if (sd.isSubset(f.getSet()))
248                                             conjprovides=true;
249                                     }
250                                 }
251                             } else
252                                 break;
253                         }
254                     }
255                 }
256                 if (!conjprovides) {
257                     goodconstraint=false;
258                     break;
259                 }
260             }
261             if (goodconstraint)
262                 set.add(c);
263         }
264         return set;
265     }
266
267
268     /** This method determines whether the model definition rules
269      * ensure that the relation r (or inverse relation if inverse is
270      * true) evaluated on the domain sd is either a function (if
271      * isPartial=false) or a partial function (if isPartial=true). */
272
273     static public boolean rulesensurefunction(State state,RelationDescriptor r, SetDescriptor sd,boolean inverse, boolean isPartial) {
274         return rulesensurefunction(state, new Function(r,sd,inverse,null),isPartial);
275     }
276
277     public static class Function {
278         private RelationDescriptor rd;
279         private SetDescriptor sd;
280         private boolean inverse;
281         private Expr expr;
282
283         public Function(RelationDescriptor r, SetDescriptor sd, boolean inverse,Expr e) {
284             this.inverse=inverse;
285             this.sd=sd;
286             this.rd=r;
287             this.expr=e;
288         }
289
290         public Expr getExpr() {
291             return expr;
292         }
293
294         public SetDescriptor getSet() {
295             return sd;
296         }
297
298         public RelationDescriptor getRelation() {
299             return rd;
300         }
301
302         public boolean isInverse() {
303             return inverse;
304         }
305     }
306
307 }