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