Repair/RepairCompiler/MCC/IR/ImplicitSchema.java

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