Repair/RepairInterpreter/processconcrete.cc

   1 #include <stdlib.h>
   2 #include <assert.h>
   3 #include "processconcrete.h"
   4 #include "processabstract.h"
   5 #include "amodel.h"
   6 #include "omodel.h"
   7 #include "dmodel.h"
   8 #include "cmodel.h"
   9 #include "Hashtable.h"
  10 #include "element.h"
  11 #include "common.h"
  12 #include "bitreader.h"
  13 #include "bitwriter.h"
  14 #include "model.h"
  15 #include "set.h"
  16 #include "Relation.h"
  17 static int concretecheck=0;
  18 static int concretetrigger=0;
  19
  20 processconcrete::processconcrete(model *m) {
  21   globalmodel=m;
  22   bw=new bitwriter(globalmodel,m->gethashtable());
  23   br=new bitreader(globalmodel,m->gethashtable());
  24 }
  25
  26 void processconcrete::printstats() {
  27   printf("Concretization Rules Checked: %d Triggered: %d\n",concretecheck,concretetrigger);
  28 }
  29
  30
  31 void processconcrete::processrule(Rule *r) {
  32   State *st=new State(r,globalmodel->gethashtable());
  33   if (st->initializestate(this, globalmodel)) {
  34     while(true) {
  35       concretecheck++;
  36       if (evaluatestatementa(r->getstatementa(),st->env)) {
  37         concretetrigger++;
  38         satisfystatementb((CStatementb *)r->getstatementb(),st->env);
  39       }
  40
  41       if (!st->increment(this, globalmodel))
  42         break; /* done */
  43     }
  44   }
  45   delete(st);
  46 }
  47
  48 processconcrete::~processconcrete() {
  49   delete(br);
  50 }
  51
  52 bool processconcrete::evaluatestatementa(Statementa *sa, Hashtable *env) {
  53   switch(sa->gettype()) {
  54   case STATEMENTA_OR:
  55     return evaluatestatementa(sa->getleft(),env)||evaluatestatementa(sa->getright(),env);
  56   case STATEMENTA_AND:
  57     return evaluatestatementa(sa->getleft(),env)&&evaluatestatementa(sa->getright(),env);
  58   case STATEMENTA_NOT:
  59     return !evaluatestatementa(sa->getleft(),env);
  60   case STATEMENTA_EQUALS: {
  61     Element *left=evaluateexpr((CAElementexpr *)sa->getleftee(),env);
  62     Element *right=evaluateexpr((CAElementexpr *)sa->getrightee(),env);
  63     bool tvalue=left->equals(right);
  64     delete(left);
  65     delete(right);
  66     return tvalue;
  67   }
  68   case STATEMENTA_LT: {
  69     Element *left=evaluateexpr((CAElementexpr *)sa->getleftee(),env);
  70     Element *right=evaluateexpr((CAElementexpr *)sa->getrightee(),env);
  71     if (!left->isnumber()||
  72         !right->isnumber()) {
  73       printf("Bad lt compare\n");
  74       exit(-1);
  75     }
  76     bool tvalue=left->intvalue()<right->intvalue();
  77     delete(left);
  78     delete(right);
  79     return tvalue;
  80   }
  81   case STATEMENTA_TRUE:
  82     return true;
  83   }
  84 }
  85
  86 void processconcrete::satisfystatementb(CStatementb *sb, Hashtable *env) {
  87   Element * rvalue=evaluateexpr((CAElementexpr *)sb->getright(),env);
  88   Element *index=NULL;
  89   if (sb->gettype()==CSTATEMENTB_ARRAYASSIGN)
  90     index=evaluateexpr((CAElementexpr *)sb->getleft(),env);
  91   Field *field=sb->getfield();
  92   Element *src=evaluateexpr(sb->getexpr(),env);
  93   bw->writefieldorarray(src,field,index,rvalue);
  94   delete(rvalue);
  95   if (index!=NULL)
  96     delete(index);
  97   delete(src);
  98 }
  99
 100 Element * processconcrete::evaluateexpr(Expr *e, Hashtable *env) {
 101   switch(e->gettype()) {
 102   case EXPR_LABEL:
 103     return new Element((Element *)env->get(e->getlabel()->label()));
 104   case EXPR_FIELD: {
 105     Element *old=evaluateexpr(e->getexpr(),env);
 106     Element *newe=br->readfieldorarray(evaluateexpr(e->getexpr(),env),e->getfield(),NULL);
 107     delete(old);
 108     return newe;
 109   }
 110   case EXPR_CAST: {
 111     Element *old=evaluateexpr(e->getexpr(),env);
 112     char *type=e->getcasttype();
 113     structure *st=globalmodel->getstructure(type);
 114     Element *newe=new Element(old->getobject(),st);
 115     delete(old);
 116     return newe;
 117   }
 118   case EXPR_ARRAY: {
 119     Element *old=evaluateexpr(e->getexpr(),env);
 120     Element *index=evaluateexpr(e->getindex(),env);
 121     Element *newe=br->readfieldorarray(evaluateexpr(e->getexpr(),env),e->getfield(),index);
 122     delete(old);
 123     delete(index);
 124     return newe;
 125   }
 126   }
 127 }
 128
 129 Element * processconcrete::evaluateexpr(CAElementexpr *ee, Hashtable *env) {
 130   switch(ee->gettype()) {
 131   case CAELEMENTEXPR_LABEL:
 132     {
 133       return new Element((Element *)env->get(ee->getlabel()->label()));
 134     }
 135   case CAELEMENTEXPR_NULL:
 136     {
 137       return new Element();
 138     }
 139   case CAELEMENTEXPR_SUB:
 140     {
 141       CAElementexpr *left=ee->getleft();
 142       CAElementexpr *right=ee->getright();
 143       Element *leftval=evaluateexpr(left,env);
 144       Element *rightval=evaluateexpr(right,env);
 145       Element *diff=new Element(leftval->intvalue()-rightval->intvalue());
 146       delete(leftval);delete(rightval);
 147       return diff;
 148     }
 149   case CAELEMENTEXPR_ADD:
 150     {
 151       CAElementexpr *left=ee->getleft();
 152       CAElementexpr *right=ee->getright();
 153       Element *leftval=evaluateexpr(left,env);
 154       Element *rightval=evaluateexpr(right,env);
 155       Element *sum=new Element(leftval->intvalue()+rightval->intvalue());
 156       delete(leftval);delete(rightval);
 157       return sum;
 158     }
 159   case CAELEMENTEXPR_MULT:
 160     {
 161       CAElementexpr *left=ee->getleft();
 162       CAElementexpr *right=ee->getright();
 163       Element *leftval=evaluateexpr(left,env);
 164       Element *rightval=evaluateexpr(right,env);
 165       Element *diff=new Element(leftval->intvalue()*rightval->intvalue());
 166       delete(leftval);delete(rightval);
 167       return diff;
 168     }
 169   case CAELEMENTEXPR_DIV:
 170     {
 171       CAElementexpr *left=ee->getleft();
 172       CAElementexpr *right=ee->getright();
 173       Element *leftval=evaluateexpr(left,env);
 174       Element *rightval=evaluateexpr(right,env);
 175       Element *diff=new Element(leftval->intvalue()/rightval->intvalue());
 176       delete(leftval);delete(rightval);
 177       return diff;
 178     }
 179   case CAELEMENTEXPR_LIT:
 180     {
 181       Literal *l=ee->getliteral();
 182       switch(l->gettype()) {
 183       case LITERAL_NUMBER:
 184         return new Element(l->number());
 185       case LITERAL_TOKEN:
 186         return new Element(copystr(l->token()));
 187       case LITERAL_BOOL:
 188         return new Element(l->getbool());
 189       default:
 190         printf("ERROR with lit type\n");
 191         exit(-1);
 192       }
 193     }
 194   case CAELEMENTEXPR_SIZEOF:
 195     {
 196     Setexpr * setexpr=ee->getsetexpr();
 197     switch(setexpr->gettype()) {
 198     case SETEXPR_LABEL:
 199       return new Element(globalmodel->getdomainrelation()->getset(setexpr->getsetlabel()->getname())->getset()->size());
 200     case SETEXPR_REL: {
 201       Element *key=(Element *)env->get(setexpr->getlabel()->label());
 202       WorkSet *ws=globalmodel->getdomainrelation()->getrelation(setexpr->getrelation()->getname())->getrelation()->getset(key);
 203       if (ws==NULL)
 204         return new Element(0);
 205       else
 206         return new Element(ws->size());
 207     }
 208     case SETEXPR_INVREL: {
 209       Element *key=(Element *)env->get(setexpr->getlabel()->label());
 210       WorkSet *ws=globalmodel->getdomainrelation()->getrelation(setexpr->getrelation()->getname())->getrelation()->invgetset(key);
 211       if (ws==NULL)
 212         return new Element(0);
 213       else
 214         return new Element(ws->size());
 215     }
 216     }
 217     }
 218   case CAELEMENTEXPR_ELEMENT: {
 219     Element *index=evaluateexpr(ee->getleft(),env);
 220     int ind=index->intvalue();
 221     delete(index);
 222
 223     Setexpr * setexpr=ee->getsetexpr();
 224     switch(setexpr->gettype()) {
 225     case SETEXPR_LABEL:
 226       return new Element((Element *)globalmodel->getdomainrelation()->getset(setexpr->getsetlabel()->getname())->getset()->getelement(ind));
 227     case SETEXPR_REL: {
 228       Element *key=(Element *)env->get(setexpr->getlabel()->label());
 229       return new Element((Element *)globalmodel->getdomainrelation()->getrelation(setexpr->getrelation()->getname())->getrelation()->getset(key)->getelement(ind));
 230     }
 231     case SETEXPR_INVREL: {
 232       Element *key=(Element *)env->get(setexpr->getlabel()->label());
 233       return new Element((Element *)globalmodel->getdomainrelation()->getrelation(setexpr->getrelation()->getname())->getrelation()->invgetset(key)->getelement(ind));
 234     }
 235     }
 236   }
 237   case CAELEMENTEXPR_RELATION:
 238     {
 239       Element *e=evaluateexpr(ee->getleft(),env);
 240       Element *r=(Element *)globalmodel->getdomainrelation()->getrelation(ee->getrelation()->getname())->getrelation()->getobj(e);
 241       return new Element(r);
 242     }
 243   }
 244 }