Repair/RepairCompiler/MCC/IR/ImplicitSchema.java

   1 package MCC.IR;
   2 import MCC.State;
   3 import MCC.Compiler;
   4
   5 import java.util.*;
   6
   7 public class ImplicitSchema {
   8     State state;
   9     SetAnalysis setanalysis;
  10     public ImplicitSchema(State state) {
  11         this.state=state;
  12         this.setanalysis=new SetAnalysis(state);
  13     }
  14
  15     public void update() {
  16         if (Compiler.REPAIR) {
  17             updaterules();
  18         }
  19         updateconstraints();
  20         updaterelationconstraints();
  21     }
  22
  23     boolean needDomain(RelationDescriptor rd) {
  24         return needDR(rd, true);
  25     }
  26
  27     boolean needDR(RelationDescriptor rd,boolean isdomain) {
  28         Vector rules=state.vRules;
  29         SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
  30         if (sd instanceof ReservedSetDescriptor)
  31             return false;
  32         for(int i=0;i<rules.size();i++) {
  33             Rule r=(Rule)rules.get(i);
  34             if ((r.numQuantifiers()==1)&&
  35                 (r.getQuantifier(0) instanceof RelationQuantifier)&&
  36                 (((RelationQuantifier)r.getQuantifier(0)).getRelation()==rd)&&
  37                 r.getInclusion().getTargetDescriptors().contains(sd)) {
  38                 SetInclusion rinc=(SetInclusion)r.getInclusion();
  39                 RelationQuantifier rq=(RelationQuantifier)r.getQuantifier(0);
  40                 VarDescriptor vd=isdomain?rq.x:rq.y;
  41                 if ((rinc.getExpr() instanceof VarExpr)&&
  42                     (((VarExpr)rinc.getExpr()).getVar()==vd)&&
  43                     (r.getGuardExpr() instanceof BooleanLiteralExpr)&&
  44                     (((BooleanLiteralExpr)r.getGuardExpr()).getValue()))
  45                     return false;
  46             }
  47         }
  48
  49
  50         for(int i=0;i<rules.size();i++) {
  51             Rule r=(Rule)rules.get(i);
  52             Inclusion inc=r.getInclusion();
  53             if (inc.getTargetDescriptors().contains(rd)) {
  54                 /* Need to check this rule */
  55                 boolean good=false;
  56                 RelationInclusion rinc=(RelationInclusion)inc;
  57                 Expr expr=isdomain?rinc.getLeftExpr():rinc.getRightExpr();
  58                 if (expr instanceof VarExpr) {
  59                     VarDescriptor vd=((VarExpr)expr).getVar();
  60                     assert vd!=null;
  61                     for (int j=0;j<r.numQuantifiers();j++) {
  62                         Quantifier q=r.getQuantifier(j);
  63                         if ((q instanceof SetQuantifier)&&
  64                             (((SetQuantifier)q).getVar()==vd)&&
  65                             (sd.allSubsets().contains(((SetQuantifier)q).getSet()))) {
  66                             good=true;
  67                             break;
  68                         }
  69                         if ((q instanceof RelationQuantifier)&&
  70                             (
  71                             ((((RelationQuantifier)q).x==vd)&&
  72                             (sd.allSubsets().contains(((RelationQuantifier)q).getRelation().getDomain())))
  73                             ||
  74                             ((((RelationQuantifier)q).y==vd)&&
  75                             (sd.allSubsets().contains(((RelationQuantifier)q).getRelation().getRange())))
  76                             )) {
  77                             good=true;
  78                             break;
  79                         }
  80
  81                     }
  82                     if (good)
  83                         continue; /* Proved for this case */
  84                 }
  85                 for(int j=0;j<rules.size();j++) {
  86                     Rule r2=(Rule)rules.get(j);
  87                     Inclusion inc2=r2.getInclusion();
  88
  89                     if (checkimplication(r,r2,isdomain)) {
  90                         good=true;
  91                         break;
  92                     }
  93                 }
  94                 if (good)
  95                     continue;
  96
  97                 return true; /* Couldn't prove we didn't need */
  98             }
  99         }
 100         return false;
 101     }
 102
 103     boolean checkimplication(Rule r1, Rule r2, boolean isdomain) {
 104         /* r1 is the relation */
 105         /* See if this rule guarantees relation */
 106         /* Steps:
 107            1. match up quantifiers
 108            2. check inclusion condition
 109            3. see if guard expr of set rule is more general */
 110         RelationInclusion inc1=(RelationInclusion) r1.getInclusion();
 111         RelationDescriptor rd=inc1.getRelation();
 112         SetDescriptor sd=isdomain?rd.getDomain():rd.getRange();
 113         Expr expr=isdomain?inc1.getLeftExpr():inc1.getRightExpr();
 114
 115         Inclusion inc2=r2.getInclusion();
 116         if (!(inc2 instanceof SetInclusion))
 117             return false;
 118         SetInclusion sinc2=(SetInclusion)inc2;
 119         if (sinc2.getSet()!=sd)
 120             return false;
 121
 122         /* Construct a mapping between quantifiers */
 123         int[] mapping=new int[r2.numQuantifiers()];
 124         HashMap map=new HashMap();
 125         for(int i=0;i<r1.numQuantifiers();i++) {
 126             Quantifier q1=r1.getQuantifier(i);
 127             for (int j=0;j<r2.numQuantifiers();j++) {
 128                 if (mapping[j]==1)
 129                     continue; /* Its already used */
 130                 Quantifier q2=r2.getQuantifier(j);
 131                 if (q1 instanceof SetQuantifier && q2 instanceof SetQuantifier&&
 132                     ((SetQuantifier)q1).getSet()==((SetQuantifier)q2).getSet()) {
 133                     mapping[j]=1;
 134                     map.put(((SetQuantifier)q1).getVar(),((SetQuantifier)q2).getVar());
 135                     break;
 136                 }
 137                 if (q1 instanceof RelationQuantifier && q2 instanceof RelationQuantifier &&
 138                     ((RelationQuantifier)q1).getRelation()==((RelationQuantifier)q2).getRelation()) {
 139                     mapping[j]=1;
 140                     map.put(((RelationQuantifier)q1).x,((RelationQuantifier)q2).x);
 141                     map.put(((RelationQuantifier)q1).y,((RelationQuantifier)q2).y);
 142                     break;
 143                 }
 144                 if (q1 instanceof ForQuantifier && q2 instanceof ForQuantifier &&
 145                     ((ForQuantifier)q1).lower.equals(map,((ForQuantifier)q2).lower)&&
 146                     ((ForQuantifier)q1).upper.equals(map,((ForQuantifier)q2).upper)) {
 147                     mapping[j]=1;
 148                     map.put(((ForQuantifier)q1).getVar(),((ForQuantifier)q2).getVar());
 149                 }
 150             }
 151         }
 152
 153         /* Make sure all bindings in the set rule are bound */
 154         for (int i=0;i<r2.numQuantifiers();i++) {
 155             if (mapping[i]!=1)
 156                 return false;
 157         }
 158
 159         /* Built mapping */
 160         Expr sexpr=sinc2.getExpr();
 161         if (!expr.equals(map,sexpr))
 162             return false;  /* This rule doesn't add the right thing */
 163
 164         DNFRule drule1=r1.getDNFGuardExpr();
 165         DNFRule drule2=r2.getDNFGuardExpr();
 166         for (int i=0;i<drule1.size();i++) {
 167             RuleConjunction rconj1=drule1.get(i);
 168             boolean foundmatch=false;
 169             for (int j=0;j<drule2.size();j++) {
 170                 RuleConjunction rconj2=drule2.get(j);
 171                 /* Need to show than rconj2 is true if rconj1 is true */
 172                 if (implication(map,rconj1,rconj2,sinc2)) {
 173                     foundmatch=true;
 174                     break;
 175                 }
 176             }
 177             if (!foundmatch)
 178                 return false;
 179         }
 180         return true;
 181     }
 182
 183     boolean implication(HashMap map, RuleConjunction rc1, RuleConjunction rc2,SetInclusion si) {
 184         for(int i=0;i<rc2.size();i++) {
 185             /* Check that rc1 has all predicates that rc2 has */
 186             DNFExpr de2=rc2.get(i);
 187             /* Predicates for objects that aren't in set */
 188             if (de2.getNegation()&&
 189                 (de2.getExpr() instanceof ElementOfExpr)) {
 190                 ElementOfExpr eoe=(ElementOfExpr)de2.getExpr();
 191                 if (si.getSet().isSubset(eoe.set)&&
 192                     si.getExpr().equals(null,eoe.element))
 193                     continue; /* This predicate isn't a problem */
 194             }
 195             boolean havematch=false;
 196             for(int j=0;j<rc1.size();j++) {
 197                 DNFExpr de1=rc1.get(i);
 198                 if (de1.getNegation()!=de2.getNegation())
 199                     continue;
 200                 if (de1.getExpr().equals(map,de2.getExpr())) {
 201                     havematch=true;
 202                     break;
 203                 }
 204             }
 205             if (!havematch)
 206                 return false;
 207         }
 208         return true;
 209     }
 210
 211     boolean needRange(RelationDescriptor rd) {
 212         return needDR(rd, false);
 213     }
 214
 215     void updaterelationconstraints() {
 216         Vector reldescriptors=state.stRelations.getAllDescriptors();
 217         for(int i=0;i<reldescriptors.size();i++) {
 218             RelationDescriptor rd=(RelationDescriptor) reldescriptors.get(i);
 219             if (needDomain(rd)||needRange(rd)) {
 220
 221                 Constraint c=new Constraint();
 222                 /* Construct quantifier */
 223                 LogicStatement ls=null;
 224
 225                 RelationQuantifier rq=new RelationQuantifier();
 226                 String varname1=new String("relationvar1");
 227                 VarDescriptor var1=new VarDescriptor(varname1);
 228                 String varname2=new String("relationvar2");
 229                 VarDescriptor var2=new VarDescriptor(varname2);
 230                 rq.setTuple(var1,var2);
 231                 rq.setRelation(rd);
 232                 c.addQuantifier(rq);
 233                 c.getSymbolTable().add(var1);
 234                 c.getSymbolTable().add(var2);
 235                 var1.setType(rd.getDomain().getType());
 236                 var2.setType(rd.getRange().getType());
 237
 238                 if (needDomain(rd)) {
 239                     VarExpr ve1=new VarExpr(var1);
 240                     SetExpr se1=new SetExpr(rd.getDomain());
 241                     se1.td=rd.getDomain().getType();
 242                     ls=new InclusionPredicate(ve1,se1);
 243                 }
 244
 245
 246                 if (needRange(rd)) {
 247                     VarExpr ve2=new VarExpr(var2);
 248                     SetExpr se2=new SetExpr(rd.getRange());
 249                     se2.td=rd.getRange().getType();
 250                     LogicStatement incpred2=new InclusionPredicate(ve2,se2);
 251                     if (ls==null) ls=incpred2;
 252                     else ls=new LogicStatement(LogicStatement.AND,ls,incpred2);
 253                 }
 254                 rd.addUsage(RelationDescriptor.IMAGE);
 255
 256                 c.setLogicStatement(ls);
 257                 state.vConstraints.add(c);
 258             }
 259         }
 260     }
 261
 262     void updateconstraints() {
 263         Vector setdescriptors=state.stSets.getAllDescriptors();
 264         for(int i=0;i<setdescriptors.size();i++) {
 265             SetDescriptor sd=(SetDescriptor) setdescriptors.get(i);
 266             if(sd.isPartition()) {
 267                 Constraint c=new Constraint();
 268                 /* Construct quantifier */
 269                 SetQuantifier sq=new SetQuantifier();
 270                 String varname=new String("partitionvar");
 271                 VarDescriptor var=new VarDescriptor(varname);
 272                 c.getSymbolTable().add(var);
 273                 var.setType(sd.getType());
 274                 sq.setVar(var);
 275                 sq.setSet(sd);
 276                 c.addQuantifier(sq);
 277
 278                 /*Construct logic statement*/
 279                 LogicStatement ls=null;
 280                 for(int j=0;j<sd.getSubsets().size();j++) {
 281                     LogicStatement conj=null;
 282                     for(int k=0;k<sd.getSubsets().size();k++) {
 283                         VarExpr ve=new VarExpr(var);
 284                         SetExpr se=new SetExpr((SetDescriptor) sd.getSubsets().get(k));
 285                         se.td=sd.getType();
 286                         LogicStatement incpred=new InclusionPredicate(ve,se);
 287                         if (j!=k) {
 288                             incpred=new LogicStatement(LogicStatement.NOT ,incpred);
 289                         }
 290                         if (conj==null)
 291                             conj=incpred;
 292                         else
 293                             conj=new LogicStatement(LogicStatement.AND, conj, incpred);
 294                     }
 295                     if (ls==null)
 296                         ls=conj;
 297                     else
 298                         ls=new LogicStatement(LogicStatement.OR, ls, conj);
 299                 }
 300                 c.setLogicStatement(ls);
 301                 state.vConstraints.add(c);
 302             }
 303         }
 304     }
 305
 306     void updaterules() {
 307         Vector oldrules=state.vRules;
 308         Vector newrules=new Vector();
 309         for(int i=0;i<oldrules.size();i++) {
 310             Rule r=(Rule)oldrules.get(i);
 311             if (r.inclusion instanceof SetInclusion) {
 312                 SetDescriptor sd=((SetInclusion)r.inclusion).getSet();
 313                 Set supersets=setanalysis.getSuperset(sd);
 314                 if (supersets!=null)
 315                     for(Iterator superit=supersets.iterator();superit.hasNext();) {
 316                         SetDescriptor sd1=(SetDescriptor)superit.next();
 317                         Rule nr=new Rule();
 318                         nr.setGuardExpr(r.getGuardExpr());
 319                         nr.quantifiers=r.quantifiers;
 320                         nr.isstatic=r.isstatic;
 321                         nr.isdelay=r.isdelay;
 322                         nr.inclusion=new SetInclusion(((SetInclusion)r.inclusion).elementexpr,sd1);
 323                         nr.st=r.st;
 324                         nr.setnogenerate();
 325                         newrules.add(nr);
 326                         state.implicitrule.put(nr,r);
 327                     }
 328             }
 329         }
 330         oldrules.addAll(newrules);
 331     }
 332 }