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 (!sq.getSet().isSubset(f.getSet()))
 203                     return false;
 204                 if (!(((r.getGuardExpr() instanceof BooleanLiteralExpr)&&
 205                        ((BooleanLiteralExpr)r.getGuardExpr()).getValue()==true))||isPartial)
 206                     return false;
 207                 Expr e2=f.isInverse()?ri.getLeftExpr():ri.getRightExpr();
 208                 if (e2.isSafe())
 209                     foundrule=true;
 210                 else
 211                     return false;
 212             }
 213         }
 214         return foundrule;
 215     }
 216
 217     private Set providesfunction(Function f) {
 218         HashSet set=new HashSet();
 219         for(int i=0;i<state.vConstraints.size();i++) {
 220             Constraint c=(Constraint)state.vConstraints.get(i);
 221             boolean goodconstraint=true;
 222             DNFConstraint dnfconst=c.dnfconstraint;
 223             for(int j=0;j<dnfconst.size();j++) {
 224                 Conjunction conj=dnfconst.get(j);
 225                 boolean conjprovides=false;
 226                 for(int k=0;k<conj.size();k++) {
 227                     DNFPredicate dpred=conj.get(k);
 228                     if (!dpred.isNegated()&&
 229                         (dpred.getPredicate() instanceof ExprPredicate)&&
 230                         ((ExprPredicate)dpred.getPredicate()).getType()==ExprPredicate.SIZE) {
 231                         ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
 232                         if (ep.isRightInt()&&
 233                             ep.rightSize()==1&&
 234                             ep.getOp()==Opcode.EQ&&
 235                             ep.inverted()==f.isInverse()&&
 236                             ep.getDescriptor()==f.getRelation()) {
 237                             ImageSetExpr se=(ImageSetExpr) ((SizeofExpr) ((OpExpr)ep.expr).left).getSetExpr();
 238                             VarDescriptor vd=se.getVar();
 239                             if (c.numQuantifiers()==1) {
 240                                 for(int l=0;l<c.numQuantifiers();l++) {
 241                                     Quantifier q=c.getQuantifier(l);
 242                                     if (q instanceof SetQuantifier&&
 243                                         ((SetQuantifier)q).getVar()==vd) {
 244                                         SetDescriptor sd=((SetQuantifier)q).getSet();
 245                                         if (sd.isSubset(f.getSet()))
 246                                             conjprovides=true;
 247                                     }
 248                                 }
 249                             } else
 250                                 break;
 251                         }
 252                     }
 253                 }
 254                 if (!conjprovides) {
 255                     goodconstraint=false;
 256                     break;
 257                 }
 258             }
 259             if (goodconstraint)
 260                 set.add(c);
 261         }
 262         return set;
 263     }
 264
 265
 266     /** This method determines whether the model definition rules
 267      * ensure that the relation r (or inverse relation if inverse is
 268      * true) evaluated on the domain sd is either a function (if
 269      * isPartial=false) or a partial function (if isPartial=true). */
 270
 271     static public boolean rulesensurefunction(State state,RelationDescriptor r, SetDescriptor sd,boolean inverse, boolean isPartial) {
 272         return rulesensurefunction(state, new Function(r,sd,inverse,null),isPartial);
 273     }
 274
 275     public static class Function {
 276         private RelationDescriptor rd;
 277         private SetDescriptor sd;
 278         private boolean inverse;
 279         private Expr expr;
 280
 281         public Function(RelationDescriptor r, SetDescriptor sd, boolean inverse,Expr e) {
 282             this.inverse=inverse;
 283             this.sd=sd;
 284             this.rd=r;
 285             this.expr=e;
 286         }
 287
 288         public Expr getExpr() {
 289             return expr;
 290         }
 291
 292         public SetDescriptor getSet() {
 293             return sd;
 294         }
 295
 296         public RelationDescriptor getRelation() {
 297             return rd;
 298         }
 299
 300         public boolean isInverse() {
 301             return inverse;
 302         }
 303     }
 304
 305 }