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(f))
 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     private boolean rulesensurefunction(Function f) {
 175         boolean foundrule=false;
 176         for(int i=0;i<state.vRules.size();i++) {
 177             Rule r=(Rule)state.vRules.get(i);
 178             if (r.getInclusion().getTargetDescriptors().contains(f.getRelation())) {
 179                 RelationInclusion ri=(RelationInclusion)r.getInclusion();
 180                 Expr e=f.isInverse()?ri.getRightExpr():ri.getLeftExpr();
 181                 SetDescriptor sd=e.getSet();
 182                 if (sd==null)
 183                     return false;
 184                 if (!(sd.isSubset(f.getSet())||f.getSet().isSubset(sd)))
 185                     continue; /* This rule doesn't effect the function */
 186                 if (foundrule) /* two different rules are a problem */
 187                     return false;
 188                 if (!((e instanceof VarExpr)&&(r.numQuantifiers()==1)))
 189                     return false;
 190                 VarExpr ve=(VarExpr)e;
 191                 Quantifier q=r.getQuantifier(0);
 192                 if (!(q instanceof SetQuantifier))
 193                     return false;
 194                 SetQuantifier sq=(SetQuantifier)q;
 195                 if (ve.getVar()!=sq.getVar())
 196                     return false;
 197                 if (!sq.getSet().isSubset(f.getSet()))
 198                     return false;
 199                 if (!((r.getGuardExpr() instanceof BooleanLiteralExpr)&&
 200                       ((BooleanLiteralExpr)r.getGuardExpr()).getValue()==true))
 201                     return false;
 202                 Expr e2=f.isInverse()?ri.getLeftExpr():ri.getRightExpr();
 203                 if (e2.isSafe())
 204                     foundrule=true;
 205                 else
 206                     return false;
 207             }
 208         }
 209         return foundrule;
 210     }
 211
 212     private Set providesfunction(Function f) {
 213         HashSet set=new HashSet();
 214         for(int i=0;i<state.vConstraints.size();i++) {
 215             Constraint c=(Constraint)state.vConstraints.get(i);
 216             boolean goodconstraint=true;
 217             DNFConstraint dnfconst=c.dnfconstraint;
 218             for(int j=0;j<dnfconst.size();j++) {
 219                 Conjunction conj=dnfconst.get(j);
 220                 boolean conjprovides=false;
 221                 for(int k=0;k<conj.size();k++) {
 222                     DNFPredicate dpred=conj.get(k);
 223                     if (!dpred.isNegated()&&
 224                         (dpred.getPredicate() instanceof ExprPredicate)&&
 225                         ((ExprPredicate)dpred.getPredicate()).getType()==ExprPredicate.SIZE) {
 226                         ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
 227                         if (ep.isRightInt()&&
 228                             ep.rightSize()==1&&
 229                             ep.getOp()==Opcode.EQ&&
 230                             ep.inverted()==f.isInverse()&&
 231                             ep.getDescriptor()==f.getRelation()) {
 232                             ImageSetExpr se=(ImageSetExpr) ((SizeofExpr) ((OpExpr)ep.expr).left).getSetExpr();
 233                             VarDescriptor vd=se.getVar();
 234                             if (c.numQuantifiers()==1) {
 235                                 for(int l=0;l<c.numQuantifiers();l++) {
 236                                     Quantifier q=c.getQuantifier(l);
 237                                     if (q instanceof SetQuantifier&&
 238                                         ((SetQuantifier)q).getVar()==vd) {
 239                                         SetDescriptor sd=((SetQuantifier)q).getSet();
 240                                         if (sd.isSubset(f.getSet()))
 241                                             conjprovides=true;
 242                                     }
 243                                 }
 244                             } else
 245                                 break;
 246                         }
 247                     }
 248                 }
 249                 if (!conjprovides) {
 250                     goodconstraint=false;
 251                     break;
 252                 }
 253             }
 254             if (goodconstraint)
 255                 set.add(c);
 256         }
 257         return set;
 258     }
 259
 260     public static class Function {
 261         private RelationDescriptor rd;
 262         private SetDescriptor sd;
 263         private boolean inverse;
 264         private Expr expr;
 265
 266         public Function(RelationDescriptor r, SetDescriptor sd, boolean inverse,Expr e) {
 267             this.inverse=inverse;
 268             this.sd=sd;
 269             this.rd=r;
 270             this.expr=e;
 271         }
 272
 273         public Expr getExpr() {
 274             return expr;
 275         }
 276
 277         public SetDescriptor getSet() {
 278             return sd;
 279         }
 280
 281         public RelationDescriptor getRelation() {
 282             return rd;
 283         }
 284
 285         public boolean isInverse() {
 286             return inverse;
 287         }
 288     }
 289
 290 }