Repair/RepairInterpreter/model.cc

   1 #include <stdio.h>
   2 #include <stdlib.h>
   3 #include <time.h>
   4 #include <fstream.h>
   5 #include <iostream.h>
   6 #include "classlist.h"
   7 #include "model.h"
   8 #include "token.h"
   9 #include "typeparser.h"
  10 #include "dparser.h"
  11 #include "aparser.h"
  12 #include "cparser.h"
  13 #include "oparser.h"
  14 #include "rparser.h"
  15 #include "dmodel.h"
  16 #include "omodel.h"
  17 #include "amodel.h"
  18 #include "tmodel.h"
  19 #include "list.h"
  20 #include "processabstract.h"
  21 #include "processobject.h"
  22 #include "processconcrete.h"
  23 #include "normalizer.h"
  24 #include "Hashtable.h"
  25 #include "element.h"
  26 #include "bitreader.h"
  27 #include "DefaultGuidance2.h"
  28 #include "DefaultGuidance.h"
  29 #include "DefaultGuidance3.h"
  30 #include "repair.h"
  31 #include "fieldcheck.h"
  32 #include "tmap.h"
  33 #include "string.h"
  34 #include "set.h"
  35 #include <sys/time.h>
  36
  37 Hashtable * model::gethashtable() {
  38   return env;
  39 }
  40
  41 bitreader * model::getbitreader() {
  42   return br;
  43 }
  44
  45 Guidance * model::getguidance() {
  46   return guidance;
  47 }
  48
  49 model::model(char *abstractfile, char *modelfile, char *spacefile, char *structfile, char *concretefile, char *rangefile)
  50 {
  51   parsestructfile(structfile);
  52
  53
  54   //Hashtable first for lookups
  55   env=new Hashtable((unsigned int (*)(void *)) & hashstring,(int (*)(void *,void *)) &equivalentstrings);
  56   //  env->put(&bstring,new Element(&badstruct,getstructure("arrayofstructs")));//should be of badstruct
  57   parseabstractfile(abstractfile);
  58   parsemodelfile(modelfile);
  59   parsespacefile(spacefile);
  60   parseconcretefile(concretefile);
  61   //  parserangefile(rangefile);
  62   // committing out because of memory problems
  63
  64   br=new bitreader(this,env);
  65   guidance=new DefGuidance(this);  // for the file system benchmark
  66
  67 #ifdef REPAIR
  68   repair=new Repair(this);
  69   if (!repair->analyzetermination()) {
  70 #ifdef DEBUGMESSAGES
  71     printf("Constraint set might not terminate and can't be repaired!\n");
  72 #endif
  73     exit(-1);
  74   }
  75   fc=new FieldCheck(this);
  76   fc->buildmaps();
  77   fc->analyze();
  78 #endif
  79   typmap=new typemap(this);
  80 }
  81
  82 void model::reset() {
  83   //  typmap->reset(); Don't rebuild trees
  84   domainrelation->reset();
  85 }
  86
  87 typemap * model::gettypemap() {
  88   return typmap;
  89 }
  90
  91 Repair * model::getrepair() {
  92   return repair;
  93 }
  94
  95 NormalForm * model::getnormalform(Constraint *c) {
  96   for (int i=0;i<numconstraint;i++) {
  97     if (c==constraintarray[i])
  98       return constraintnormal[i];
  99   }
 100   printf("Error finding normal form\n");
 101   exit(-1);
 102 }
 103
 104 int model::getnumconstraints() {
 105   return numconstraint;
 106 }
 107
 108 NormalForm * model::getnormalform(int i) {
 109   return constraintnormal[i];
 110 }
 111
 112 Constraint * model::getconstraint(int i) {
 113   return constraintarray[i];
 114 }
 115
 116
 117 // processes the model definition rules
 118 void model::doabstraction() {
 119   struct timeval begin,end;
 120   unsigned long time;
 121   gettimeofday(&begin,NULL);
 122
 123   pa=new processabstract(this);
 124   bool clean=false;
 125   /* Process rules until we reach a fixpoint*/
 126   /* First the normal rules */
 127   do {
 128     clean=false;
 129     for(int i=0;i<numrules;i++) {
 130       if(!rulearray[i]->isdelayed()) {
 131         pa->setclean();
 132         pa->processrule(rulearray[i]);
 133         if (pa->dirtyflagstatus())
 134           clean=true;
 135       }
 136     }
 137   } while(clean);
 138
 139   /* Then the delayed rules */
 140   do {
 141     clean=false;
 142     for(int i=0;i<numrules;i++) {
 143       if(rulearray[i]->isdelayed()) {
 144         pa->setclean();
 145         pa->processrule(rulearray[i]);
 146         if (pa->dirtyflagstatus())
 147           clean=true;
 148       }
 149     }
 150   } while(clean);
 151   gettimeofday(&end,NULL);
 152   time=(end.tv_sec-begin.tv_sec)*1000000+end.tv_usec-begin.tv_usec;
 153   printf("Time used for abstraction(us): %ld\n",time);
 154
 155   pa->printstats();
 156 }
 157
 158
 159 void model::triggerrule(Element *ele,char *set) {
 160   for(int i=0;i<numrules;i++) {
 161     if(rulearray[i]->isstatic()) {
 162       pa->processrule(rulearray[i], ele, set);
 163     }
 164   }
 165 }
 166
 167
 168 // processes the external constraints
 169 void model::doconcrete() {
 170   struct timeval begin,end;
 171   unsigned long time;
 172   gettimeofday(&begin,NULL);
 173
 174   processconcrete *pr=new processconcrete(this);
 175   for(int i=0;i<numconcrete;i++) {
 176     pr->processrule(concretearray[i]);
 177   }
 178   gettimeofday(&end,NULL);
 179   time=(end.tv_sec-begin.tv_sec)*1000000+end.tv_usec-begin.tv_usec;
 180   printf("Time used for concretization(us): %ld\n",time);
 181
 182   pr->printstats();
 183   delete(pr);
 184 }
 185
 186
 187
 188 // inserts faults that break the specifications
 189 void model::breakspec()
 190 {
 191   srandom((unsigned) time(NULL));
 192
 193   processobject *po = new processobject(this);
 194
 195   // takes each satisfied constraint and breaks it with probability prob_breakconstraint
 196   for (int i=0; i<numconstraint; i++)
 197     {
 198       Constraint *c = getconstraint(i);
 199       if (po->issatisfied(c))
 200         if (random()<prob_breakconstraint*RAND_MAX)
 201           po->breakconstraint(c);
 202     }
 203
 204   delete(po);
 205 }
 206
 207
 208
 209 // inserts faults that don not break the specifications
 210 void model::inserterrors()
 211 {
 212   printf("\nmodel::inserterrors CALLED\n\n");
 213
 214   srandom((unsigned) time(NULL));
 215
 216   processobject *po = new processobject(this);
 217
 218   // takes each satisfied constraint and modifies it with probability prob_modifyconstraint
 219   long int r;
 220   for (int i=0; i<numconstraint; i++)
 221     {
 222       Constraint *c = getconstraint(i);
 223 #ifdef DEBUGMESSAGES
 224       printf("Constraint: ");
 225       c->print();
 226       if (po->issatisfied(c))
 227         printf("     is satisfied\n");
 228       else printf("     is not satisfied\n");
 229       fflush(NULL);
 230 #endif
 231       if (po->issatisfied(c))
 232         {
 233           r=random();
 234 #ifdef DEBUGMESSAGES
 235           printf("r=%ld\n", r);
 236 #endif
 237           if (r<prob_modifyconstraint*RAND_MAX)
 238             po->modifyconstraint(c);
 239         }
 240     }
 241
 242   delete(po);
 243 }
 244
 245
 246
 247 // processes the internal constraints
 248 // returns true only if no violated constraints were found
 249 bool model::docheck()
 250 {
 251   struct timeval begin,end;
 252   unsigned long time;
 253   bool found=false;
 254   processobject *po=new processobject(this);
 255   bool t=false;
 256   gettimeofday(&begin,NULL);
 257
 258   do {
 259     t=false;
 260     /* Process rules until we reach a fixpoint*/
 261     for(int i=0;i<numconstraint;i++) {
 262       if (!po->processconstraint(constraintarray[i]))
 263         {
 264           found=true;
 265 #ifdef TOOL
 266           break;
 267 #endif
 268           t=true; //Got to keep running
 269         }
 270     }
 271   } while(t);
 272   gettimeofday(&end,NULL);
 273   time=(end.tv_sec-begin.tv_sec)*1000000+end.tv_usec-begin.tv_usec;
 274   printf("Time used for check(us): %ld\n",time);
 275   po->printstats();
 276   delete(po);
 277   //printf("return from docheck()");
 278   return found;
 279 }
 280
 281
 282 DomainRelation * model::getdomainrelation() {
 283   return domainrelation;
 284 }
 285
 286
 287
 288 /* reads the testspace file, which keeps the sets and relations involved;
 289    these sets and relations are managed by "domainrelation" */
 290 void model::parsespacefile(char *spacefile) {
 291   ifstream *ifs=new ifstream();
 292   ifs->open(spacefile);
 293   Reader *r=new Reader(ifs);
 294   Dparser *p=new Dparser(r);
 295   domainrelation=p->parsesetrelation();
 296
 297 #ifdef DEBUGMANYMESSAGES
 298   domainrelation->print();
 299 #endif
 300
 301   ifs->close();
 302   delete(ifs);
 303 }
 304
 305
 306
 307 /* reads the teststruct file, which keeps the structure definitions;
 308    these definitions are kept in "structurearray" */
 309 void model::parsestructfile(char *structfile) {
 310   ifstream *ifs=new ifstream();
 311   ifs->open(structfile);
 312   Reader *r=new Reader(ifs);
 313   Typeparser *p=new Typeparser(r);
 314   List *list=new List();
 315
 316   do {
 317     structure *st=p->parsestructure();
 318     if (st!=NULL) {
 319       list->addobject(st);
 320
 321 #ifdef DEBUGMANYMESSAGES
 322       st->print();
 323 #endif
 324
 325     }
 326     else
 327       break;
 328   } while(true);
 329   structurearray=new structure *[list->size()];
 330   list->toArray((void **)structurearray);
 331   numstarray=list->size();
 332
 333   ifs->close();
 334   delete(list);
 335   delete(ifs);
 336 }
 337
 338
 339 /* parses the testabstract file, which contains the model definition rules
 340    these rules are kept in "rulearray" */
 341 void model::parseabstractfile(char *abstractfile) {
 342   ifstream *ifs=new ifstream();
 343   ifs->open(abstractfile);
 344   Reader *r=new Reader(ifs);
 345   AParser *p=new AParser(r);
 346   List *list=new List();
 347   int countstatic=0;
 348   do {
 349     Rule *ru=p->parserule();
 350     if (ru!=NULL) {
 351       list->addobject(ru);
 352       if(ru->isstatic())
 353         countstatic++;
 354 #ifdef DEBUGMANYMESSAGES
 355       ru->print();
 356 #endif
 357     }
 358     else
 359       break;
 360   } while(true);
 361   rulearray=new Rule *[list->size()];
 362   list->toArray((void **)rulearray);
 363   numrules=list->size();
 364   numrulenormal=countstatic;
 365   rulenormal=new NormalForm *[countstatic];
 366   int count=0;
 367   for(int i=0;i<numrules;i++) {
 368     if(rulearray[i]->isstatic()) {
 369       rulenormal[count++]=new NormalForm(rulearray[i]);
 370     }
 371   }
 372   ifs->close();
 373   delete(ifs);
 374   delete(list);
 375 }
 376
 377
 378
 379 /* parses the testconcrete file, which contains the external constraints;
 380    these constraints are kept in "concretearray" */
 381 void model::parseconcretefile(char *abstractfile) {
 382   ifstream *ifs=new ifstream();
 383   ifs->open(abstractfile);
 384   Reader *r=new Reader(ifs);
 385   CParser *p=new CParser(r);
 386   List *list=new List();
 387   do {
 388     Rule *ru=p->parserule();
 389     if (ru!=NULL) {
 390       list->addobject(ru);
 391 #ifdef DEBUGMANYMESSAGES
 392       ru->print();
 393 #endif
 394     }
 395     else
 396       break;
 397   } while(true);
 398   concretearray=new Rule *[list->size()];
 399   list->toArray((void **)concretearray);
 400   numconcrete=list->size();
 401
 402   ifs->close();
 403   delete(ifs);
 404   delete(list);
 405 }
 406
 407
 408
 409 /* parses the testmodel file, which contains the internal constraints
 410    these constraints are kept in constraintarray;
 411    the constraints in normal form are kept in constraintnormal */
 412 void model::parsemodelfile(char *modelfile) {
 413   ifstream* ifs=new ifstream();
 414   ifs->open(modelfile);
 415   Reader *r=new Reader(ifs);
 416   Parser *p=new Parser(r);
 417   List *list=new List();
 418   do {
 419     Constraint *c=p->parseconstraint();
 420     if (c!=NULL) {
 421       list->addobject(c);
 422 #ifdef DEBUGMANYMESSAGES
 423       c->print();
 424 #endif
 425     } else
 426       break;
 427   } while(true);
 428
 429   constraintarray=new Constraint *[list->size()];
 430   list->toArray((void **)constraintarray);
 431   numconstraint=list->size();
 432   constraintnormal=new NormalForm *[list->size()];
 433   for(int i=0;i<list->size();i++)
 434     constraintnormal[i]=new NormalForm(constraintarray[i]);
 435
 436   ifs->close();
 437   delete(ifs);
 438   delete(list);
 439 }
 440
 441
 442
 443 /* reads the testrange file, which keeps the ranges of the relations
 444    of the form "relation: A -> token".
 445    This information is used only by the fault injection mechanism.
 446    This file should be read only after the testspace file.
 447 */
 448 void model::parserangefile(char *rangefile)
 449 {
 450   ifstream *ifs=new ifstream();
 451   ifs->open(rangefile);
 452   Reader *r = new Reader(ifs);
 453   RParser *rp = new RParser(r);
 454
 455   do {
 456     char* relation = rp->parserelation();
 457
 458     if (relation != NULL)
 459       {
 460 #ifdef DEBUGMANYMESSAGES
 461         printf("Reading relation: %s\n", relation);
 462         fflush(NULL);
 463 #endif
 464
 465         // find the given relation, whose range should be of type "token"
 466         DRelation *drel = domainrelation->getrelation(relation);
 467         if (strcmp(drel->getrange(), "token") != 0)
 468           {
 469             printf("Error! Range of %s should be of type token.", relation);
 470             exit(0);
 471           }
 472
 473         WorkSet *ws = rp->parseworkset();
 474 #ifdef DEBUGMANYMESSAGES
 475         printf("The range for %s is:\n", relation);
 476         void *obj = ws->firstelement();
 477         while (obj)
 478           {
 479             printf("%s ", (char *) obj);
 480             obj = ws->getnextelement(obj);
 481           }
 482         fflush(NULL);
 483         printf("\n\n");
 484 #endif
 485         drel->settokenrange(ws);
 486         delete(relation);
 487       }
 488     else
 489       break;
 490   } while(true);
 491
 492   ifs->close();
 493   delete(ifs);
 494   delete(r);
 495   delete(rp);
 496 }
 497
 498
 499
 500 structure * model::getstructure(char *name) {
 501   for(int i=0;i<numstarray;i++) {
 502     if (equivalentstrings(name,structurearray[i]->getname())) {
 503       /* got match */
 504       return structurearray[i];
 505     }
 506   }
 507   return NULL;
 508 }
 509
 510 FieldCheck * model::getfieldcheck() {
 511   return fc;
 512 }
 513
 514 int model::getnumrulenormal() {
 515   return numrulenormal;
 516 }
 517
 518 NormalForm * model::getrulenormal(int i) {
 519   return rulenormal[i];
 520 }
 521
 522 bool model::subtypeof(structure *sub,structure *super) {
 523   while(sub!=NULL) {
 524     if (sub==super)
 525       return true;
 526     if (sub->getsubtype()==NULL)
 527       return false;
 528     sub=getstructure(sub->getsubtype()->getname());
 529   }
 530   printf("Error in subtypeof\n");
 531   return false; /* Should get here*/
 532 }