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