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         constructconjunctionnodes();
  22         constructconjunctionedges();
  23     }
  24
  25     public void addNode(GraphNode gn) {
  26         GraphNode gn2=new GraphNode(gn.getLabel(),gn.getTextLabel(),gn);
  27         nodes.add(gn2);
  28         nodetonode.put(gn,gn2);
  29     }
  30
  31     public void associateWithConstraint(GraphNode gn, Constraint c) {
  32         GraphNode ggn=(GraphNode)nodetonode.get(gn);
  33         GraphNode gc=(GraphNode)constonode.get(c);
  34         GraphNode.Edge e=new GraphNode.Edge("associated",ggn);
  35         gc.addEdge(e);
  36     }
  37
  38     public void requiresConstraint(GraphNode gn, Constraint c) {
  39         GraphNode ggn=(GraphNode)nodetonode.get(gn);
  40         GraphNode gc=(GraphNode)constonode.get(c);
  41         GraphNode.Edge e=new GraphNode.Edge("requires",gc);
  42         ggn.addEdge(e);
  43     }
  44
  45     /** Constructs a node for each Constraint */
  46     private void constructnodes() {
  47         for(int i=0;i<state.vConstraints.size();i++) {
  48             Constraint c=(Constraint)state.vConstraints.get(i);
  49             GraphNode gn=new GraphNode(c.toString(),c);
  50             constonode.put(c,gn);
  51             constnodes.add(gn);
  52         }
  53     }
  54
  55     private void constructconjunctionnodes() {
  56         for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
  57             GraphNode conjnode=(GraphNode)it.next();
  58             TermNode tn=(TermNode)conjnode.getOwner();
  59             Conjunction conj=tn.getConjunction();
  60             addNode(conjnode);
  61         }
  62         for(int i=0;i<state.vConstraints.size();i++) {
  63             Constraint c=(Constraint)state.vConstraints.get(i);
  64             Set conjset=(Set)termination.conjunctionmap.get(c);
  65             for(Iterator it=conjset.iterator();it.hasNext();) {
  66                 GraphNode gn=(GraphNode)it.next();
  67                 associateWithConstraint(gn,c);
  68             }
  69         }
  70     }
  71
  72     private void constructconjunctionedges() {
  73         for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
  74             GraphNode conjnode=(GraphNode)it.next();
  75             TermNode tn=(TermNode)conjnode.getOwner();
  76             Conjunction conj=tn.getConjunction();
  77             for(int i=0;i<conj.size();i++) {
  78                 DNFPredicate dpred=conj.get(i);
  79                 Predicate pred=dpred.getPredicate();
  80                 Expr expr=null;
  81                 if (pred instanceof InclusionPredicate) {
  82                     InclusionPredicate ip=(InclusionPredicate)pred;
  83                     expr=ip.expr;
  84                 } else if (pred instanceof ExprPredicate) {
  85                     ExprPredicate ep=(ExprPredicate)pred;
  86                     expr=ep.expr;
  87                 } else throw new Error("Unrecognized Predicate");
  88                 Set functions=expr.getfunctions();
  89                 if (functions==null)
  90                     continue;
  91                 for(Iterator fit=functions.iterator();fit.hasNext();) {
  92                     Function f=(Function)fit.next();
  93                     if (rulesensurefunction(f))
  94                         continue; //no constraint needed to ensure
  95
  96                     Set s=providesfunction(f);
  97                     if (s.size()==0) {
  98                         System.out.println("Error: No constraint ensures that [forall v in "+f.getSet()+"], size(v."+(f.isInverse()?"~":"")+f.getRelation()+")=1");
  99                         System.exit(-1);
 100                     }
 101                     Constraint c=(Constraint)s.iterator().next(); //Take the first one
 102                     requiresConstraint(conjnode,c);
 103                 }
 104             }
 105         }
 106     }
 107
 108     private boolean rulesensurefunction(Function f) {
 109         boolean foundrule=false;
 110         for(int i=0;i<state.vRules.size();i++) {
 111             Rule r=(Rule)state.vRules.get(i);
 112             if (r.getInclusion().getTargetDescriptors().contains(f.getRelation())) {
 113                 RelationInclusion ri=(RelationInclusion)r.getInclusion();
 114                 Expr e=f.isInverse()?ri.getRightExpr():ri.getLeftExpr();
 115                 SetDescriptor sd=e.getSet();
 116                 if (!(sd.isSubset(f.getSet())||f.getSet().isSubset(sd)))
 117                     continue; /* This rule doesn't effect the function */
 118                 if (foundrule) /* two different rules are a problem */
 119                     return false;
 120                 if (!((e instanceof VarExpr)&&(r.numQuantifiers()==1)))
 121                     return false;
 122                 VarExpr ve=(VarExpr)e;
 123                 Quantifier q=r.getQuantifier(0);
 124                 if (!(q instanceof SetQuantifier))
 125                     return false;
 126                 SetQuantifier sq=(SetQuantifier)q;
 127                 if (ve.getVar()!=sq.getVar())
 128                     return false;
 129                 if (!sq.getSet().isSubset(f.getSet()))
 130                     return false;
 131                 if (!((r.getGuardExpr() instanceof BooleanLiteralExpr)&&
 132                       ((BooleanLiteralExpr)r.getGuardExpr()).getValue()==true))
 133                     return false;
 134                 Expr e2=f.isInverse()?ri.getLeftExpr():ri.getRightExpr();
 135                 if (e2.isSafe())
 136                     foundrule=true;
 137                 else
 138                     return false;
 139             }
 140         }
 141         return foundrule;
 142     }
 143
 144     private Set providesfunction(Function f) {
 145         HashSet set=new HashSet();
 146         for(int i=0;i<state.vConstraints.size();i++) {
 147             Constraint c=(Constraint)state.vConstraints.get(i);
 148             boolean goodconstraint=true;
 149             DNFConstraint dnfconst=c.dnfconstraint;
 150             for(int j=0;j<dnfconst.size();j++) {
 151                 Conjunction conj=dnfconst.get(j);
 152                 boolean conjprovides=false;
 153                 for(int k=0;k<conj.size();k++) {
 154                     DNFPredicate dpred=conj.get(k);
 155                     if (!dpred.isNegated()&&
 156                         (dpred.getPredicate() instanceof ExprPredicate)&&
 157                         ((ExprPredicate)dpred.getPredicate()).getType()==ExprPredicate.SIZE) {
 158                         ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
 159                         if (ep.isRightInt()&&
 160                             ep.rightSize()==1&&
 161                             ep.getOp()==Opcode.EQ&&
 162                             ep.inverted()==f.isInverse()&&
 163                             ep.getDescriptor()==f.getRelation()) {
 164                             ImageSetExpr se=(ImageSetExpr) ((SizeofExpr) ((OpExpr)ep.expr).left).getSetExpr();
 165                             VarDescriptor vd=se.getVar();
 166                             if (c.numQuantifiers()==1) {
 167                                 for(int l=0;l<c.numQuantifiers();l++) {
 168                                     Quantifier q=c.getQuantifier(l);
 169                                     if (q instanceof SetQuantifier&&
 170                                         ((SetQuantifier)q).getVar()==vd) {
 171                                         SetDescriptor sd=((SetQuantifier)q).getSet();
 172                                         if (sd.isSubset(f.getSet()))
 173                                             conjprovides=true;
 174                                     }
 175                                 }
 176                             } else
 177                                 break;
 178                         }
 179                     }
 180                 }
 181                 if (!conjprovides) {
 182                     goodconstraint=false;
 183                     break;
 184                 }
 185             }
 186             if (goodconstraint)
 187                 set.add(c);
 188         }
 189         return set;
 190     }
 191
 192     public static class Function {
 193         private RelationDescriptor rd;
 194         private SetDescriptor sd;
 195         private boolean inverse;
 196
 197         public Function(RelationDescriptor r, SetDescriptor sd, boolean inverse) {
 198             this.inverse=inverse;
 199             this.sd=sd;
 200             this.rd=r;
 201         }
 202
 203         public SetDescriptor getSet() {
 204             return sd;
 205         }
 206
 207         public RelationDescriptor getRelation() {
 208             return rd;
 209         }
 210
 211         public boolean isInverse() {
 212             return inverse;
 213         }
 214     }
 215
 216 }