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