src/Test/dirkreader.cc

   1 #include <iostream>
   2 #include <fstream>
   3 #include "csolver.h"
   4 #include "hashset.h"
   5 #include "cppvector.h"
   6 #include <dirent.h>
   7 #include <string>
   8 #include <sstream>
   9 #include "common.h"
  10 using namespace std;
  11 const char * assertstart = "ASSERTSTART";
  12 const char * assertend = "ASSERTEND";
  13 const char * satstart = "SATSTART";
  14 const char * satend = "SATEND";
  15
  16 int skipahead(const char * token1, const char * token2);
  17 char * readuntilend(const char * token);
  18 BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset);
  19 void processEquality(char * constraint, int &offset);
  20 void dumpSMTproblem(string &smtProblem, long long id);
  21 void renameDumpFile(const char *path, long long id);
  22 void addASSERTConstraintToSMTProblem(string & smtProblem, char * assert);
  23 void addSATConstraintToSMTProblem(string &smtProblem, char * sat);
  24 void createSATtuneDumps (char *assert, char *sat, long long &smtID);
  25
  26 std::ifstream * file;
  27 Order * order;
  28 MutableSet * set;
  29 class intwrapper {
  30 public:
  31   intwrapper(int _val) : value(_val) {
  32   }
  33   int32_t value;
  34 };
  35
  36 unsigned int iw_hash_function(intwrapper *i) {
  37   return i->value;
  38 }
  39
  40 bool iw_equals(intwrapper *key1, intwrapper *key2) {
  41   return (key1->value == key2->value);
  42 }
  43
  44 typedef Hashset<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashsetIW;
  45 typedef SetIterator<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashsetIWIterator;
  46 class OrderRec {
  47 public:
  48   OrderRec() : set (NULL), value(-1), alloced(false) {
  49   }
  50   ~OrderRec() {
  51     if (set != NULL) {
  52       set->resetAndDelete();
  53       delete set;
  54     }
  55   }
  56   HashsetIW * set;
  57   int32_t value;
  58   bool alloced;
  59 };
  60
  61 typedef Hashtable<intwrapper *, OrderRec *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashtableIW;
  62 typedef Hashtable<intwrapper *, Boolean *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashtableBV;
  63 Vector<OrderRec*> * orderRecVector = NULL;
  64 HashtableIW * ordertable = NULL;
  65 HashtableBV * vartable = new HashtableBV();
  66 HashsetIW * intSet = new HashsetIW();
  67 HashsetIW * boolSet = new HashsetIW();
  68
  69 void cleanAndFreeOrderRecVector(){
  70         for(uint i=0; i< orderRecVector->getSize(); i++){
  71                 delete orderRecVector->get(i);
  72         }
  73         orderRecVector->clear();
  74 }
  75
  76 int main(int numargs, char ** argv) {
  77   file = new std::ifstream(argv[1]);
  78   char * assert = NULL;
  79   char * sat = NULL;
  80   string smtProblem = "";
  81   long long smtID=0L;
  82   Vector<OrderRec*> orderRecs;
  83   orderRecVector = &orderRecs;
  84   while(true) {
  85     int retval = skipahead(assertstart, satstart);
  86     printf("%d\n", retval);
  87     if (retval == 0){
  88       break;
  89     }
  90     if (retval == 1) {
  91       if (assert != NULL){
  92         free(assert);
  93         assert = NULL;
  94         dumpSMTproblem(smtProblem, smtID);
  95         smtProblem = "";
  96         intSet->reset();
  97         boolSet->reset();
  98       }
  99       assert = readuntilend(assertend);
 100       addASSERTConstraintToSMTProblem(smtProblem, assert);
 101       //cout << "INFO: SMTProblem After adding ASSERT Constraints\n" << smtProblem << "\n&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&\n";
 102       printf("[%s]\n", assert);
 103     } else if (retval == 2) {
 104       if (sat != NULL) {
 105         free(sat);
 106         sat = NULL;
 107         vartable->resetAndDeleteKeys();
 108         ordertable->reset();
 109         cleanAndFreeOrderRecVector();
 110       } else {
 111         ordertable = new HashtableIW();
 112       }
 113       sat = readuntilend(satend);
 114       createSATtuneDumps(assert, sat, smtID);
 115       addSATConstraintToSMTProblem(smtProblem, sat);
 116       //cout << "INFO: SMTProblem After adding SAT Constraints\n" << smtProblem << "\n&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&\n";
 117     }
 118   }
 119
 120   if(smtID == 0L){
 121         char trueString [] = "true";
 122         ordertable = new HashtableIW();
 123         createSATtuneDumps(assert, trueString, smtID);
 124         addSATConstraintToSMTProblem(smtProblem, trueString);
 125   }
 126   dumpSMTproblem(smtProblem, smtID);
 127   cleanAndFreeOrderRecVector();
 128   if(ordertable != NULL){
 129         delete ordertable;
 130   }
 131   if(assert != NULL){
 132         free(assert);
 133   }
 134   if(sat != NULL){
 135         free(sat);
 136   }
 137   vartable->resetAndDeleteKeys();
 138   delete vartable;
 139   file->close();
 140   delete file;
 141 }
 142
 143 void createSATtuneDumps (char *assert, char *sat, long long &smtID){
 144         CSolver *solver = new CSolver();
 145         solver->turnoffOptimizations();
 146         set = solver->createMutableSet(1);
 147         order = solver->createOrder(SATC_TOTAL, (Set *) set);
 148         int offset = 0;
 149         processEquality(sat, offset);
 150         offset = 0;
 151         processEquality(assert, offset);
 152         offset = 0;
 153         solver->addConstraint(parseConstraint(solver, sat, offset));
 154         offset = 0;
 155         solver->addConstraint(parseConstraint(solver, assert, offset));
 156         printf("[%s]\n", sat);
 157         solver->finalizeMutableSet(set);
 158         solver->serialize();
 159         solver->printConstraints();
 160         smtID= getTimeNano();
 161         renameDumpFile("./", smtID);
 162         delete solver;
 163 }
 164
 165 void doExit(const char * message){
 166         printf("%s", message);
 167         exit(-1);
 168 }
 169
 170 void doExit() {
 171         doExit("Parse Error\n");
 172 }
 173
 174 void renameDumpFile(const char *path, long long id) {
 175         struct dirent *entry;
 176         DIR *dir = opendir(path);
 177         if (dir == NULL) {
 178                 return;
 179         }
 180         char newname[128] ={0};
 181         sprintf(newname, "%lld.dump", id);
 182         bool duplicate = false;
 183         while ((entry = readdir(dir)) != NULL) {
 184                  if(strstr(entry->d_name, "DUMP") != NULL){
 185                         if(duplicate){
 186                                 doExit("Multiplle DUMP file exists. Make sure to clean them all before running the program");
 187                         }
 188                         int result= rename( entry->d_name , newname );
 189                         if ( result == 0 )
 190                                 printf ( "File successfully renamed to %s\n" , newname);
 191                         else
 192                                 doExit( "Error renaming file" );
 193                         duplicate = true;
 194                  }
 195         }
 196         closedir(dir);
 197 }
 198 template <class MyType>
 199 string to_string(MyType value){
 200         string number;
 201         std::stringstream strstream;
 202         strstream << value;
 203         strstream >> number;
 204         return number;
 205 }
 206
 207 void dumpDeclarations(std::ofstream& smtfile){
 208         HashsetIWIterator* iterator = intSet->iterator();
 209         smtfile << "(set-logic QF_LRA)" << endl;
 210         while(iterator->hasNext()){
 211                 intwrapper * iw = iterator->next();
 212                 string declare = "(declare-const O!"+ to_string<uint32_t>(iw->value) + " Real)\n";
 213                 smtfile << declare;
 214         }
 215         delete iterator;
 216
 217         iterator = boolSet->iterator();
 218         while(iterator->hasNext()){
 219                 intwrapper * iw = iterator->next();
 220                 string declare = "(declare-const S!" + to_string<uint32_t>(iw->value) + " Bool)\n";
 221                 smtfile << declare;
 222         }
 223         delete iterator;
 224 }
 225
 226 void addASSERTConstraintToSMTProblem(string & smtProblem, char * assert){
 227         string ssat(assert);
 228         string assertStatement = "(assert "+ ssat + "\n)\n";
 229         smtProblem += assertStatement;
 230 }
 231
 232 void addSATConstraintToSMTProblem(string &smtProblem, char * sat){
 233         string ssat(sat);
 234         string satStatement = "(push)\n(assert "+ ssat + "\n)\n(check-sat)\n(get-model)\n(pop)\n";
 235         smtProblem += satStatement;
 236 }
 237
 238
 239 void dumpSMTproblem(string &smtProblem, long long id){
 240         std::ofstream smtfile;
 241         string smtfilename = to_string<long long>(id) + ".smt";
 242         smtfile.open (smtfilename.c_str());
 243         if(!smtfile.is_open())
 244         {
 245                 doExit("Unable to create file.\n");
 246         }
 247         dumpDeclarations(smtfile);
 248         smtfile << smtProblem;
 249         smtfile.close();
 250         cout <<"************here is the SMT file*********" << endl << smtProblem  <<endl << "****************************" << endl;;
 251 }
 252
 253
 254 void skipwhitespace(char * constraint, int & offset) {
 255   //skip whitespace
 256   while (constraint[offset] == ' ' || constraint[offset] == '\n')
 257     offset++;
 258 }
 259
 260 int32_t getOrderVar(char *constraint, int & offset) {
 261   if (constraint[offset++] != 'O' || constraint[offset++] != '!' ) {
 262     doExit();
 263   }
 264   int32_t num = 0;
 265   while(true) {
 266     char next = constraint[offset];
 267     if (next >= '0' && next <= '9') {
 268       num = (num * 10) + (next - '0');
 269       offset++;
 270     } else
 271       return num;
 272   }
 273 }
 274
 275 int32_t getBooleanVar(char *constraint, int & offset) {
 276         if (constraint[offset++] != 'S' || constraint[offset++] != '!' ) {
 277                 cout << "Constraint= " << constraint << "\toffset=" << constraint[offset - 1] << " ******\n";
 278                 doExit();
 279         }
 280   int32_t num = 0;
 281   while(true) {
 282     char next = constraint[offset];
 283     if (next >= '0' && next <= '9') {
 284       num = (num * 10) + (next - '0');
 285       offset++;
 286     } else
 287       return num;
 288   }
 289 }
 290
 291 BooleanEdge checkBooleanVar(CSolver *solver, int32_t value) {
 292   intwrapper v(value);
 293   if (vartable->contains(&v)) {
 294     return BooleanEdge(vartable->get(&v));
 295   } else {
 296     Boolean* ve = solver->getBooleanVar(2).getBoolean();
 297     vartable->put(new intwrapper(value), ve);
 298     return BooleanEdge(ve);
 299   }
 300 }
 301
 302 void mergeVars(int32_t value1, int32_t value2) {
 303   intwrapper v1(value1);
 304   intwrapper v2(value2);
 305   OrderRec *r1 = ordertable->get(&v1);
 306   OrderRec *r2 = ordertable->get(&v2);
 307   if (r1 == r2) {
 308     if (r1 == NULL) {
 309       OrderRec * r = new OrderRec();
 310       orderRecVector->push(r);
 311       r->value = value1;
 312       r->set = new HashsetIW();
 313       intwrapper * k1 = new intwrapper(v1);
 314       intwrapper * k2 = new intwrapper(v2);
 315       r->set->add(k1);
 316       r->set->add(k2);
 317       ordertable->put(k1, r);
 318       ordertable->put(k2, r);
 319     }
 320   } else if (r1 == NULL) {
 321     intwrapper * k = new intwrapper(v1);
 322     ordertable->put(k, r2);
 323     r2->set->add(k);
 324   } else if (r2 == NULL) {
 325     intwrapper * k = new intwrapper(v2);
 326     ordertable->put(k, r1);
 327     r1->set->add(k);
 328   } else {
 329     SetIterator<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> * it1 = r1->set->iterator();
 330     while (it1->hasNext()) {
 331       intwrapper * k = it1->next();
 332       ordertable->put(k, r2);
 333       r2->set->add(k);
 334     }
 335     delete r2->set;
 336     r2->set = NULL;
 337     delete r2;
 338     delete it1;
 339   }
 340 }
 341
 342 int32_t checkordervar(CSolver * solver, int32_t value) {
 343   intwrapper v(value);
 344   OrderRec * rec = ordertable->get(&v);
 345   if (rec == NULL) {
 346     intwrapper * k = new intwrapper(value);
 347     rec = new OrderRec();
 348     orderRecVector->push(rec);
 349     rec->value = value;
 350     rec->set = new HashsetIW();
 351     rec->set->add(k);
 352     ordertable->put(k, rec);
 353   }
 354   if (!rec->alloced) {
 355     solver->addItem(set, rec->value);
 356     rec->alloced = true;
 357   }
 358   return rec->value;
 359 }
 360
 361 void processEquality(char * constraint, int &offset) {
 362   skipwhitespace(constraint, offset);
 363   if (strncmp(&constraint[offset], "(and",4) == 0) {
 364     offset +=4;
 365     Vector<BooleanEdge> vec;
 366     while(true) {
 367       skipwhitespace(constraint, offset);
 368       if (constraint[offset] == ')') {
 369         offset++;
 370         return;
 371       }
 372       processEquality(constraint, offset);
 373     }
 374   } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
 375     offset+=2;
 376     skipwhitespace(constraint, offset);
 377     getOrderVar(constraint, offset);
 378     skipwhitespace(constraint, offset);
 379     getOrderVar(constraint, offset);
 380     skipwhitespace(constraint, offset);
 381     if (constraint[offset++] != ')'){
 382             doExit();
 383     }
 384     return;
 385   } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
 386     offset+=2;
 387     skipwhitespace(constraint, offset);
 388     int v1=getOrderVar(constraint, offset);
 389     intwrapper iwv1(v1);
 390     if(intSet->get(&iwv1) == NULL){
 391         intSet->add(new intwrapper(v1));
 392     }
 393     skipwhitespace(constraint, offset);
 394     int v2=getOrderVar(constraint, offset);
 395     intwrapper iwv2(v2);
 396     if(intSet->get(&iwv2) == NULL){
 397         intSet->add(new intwrapper(v2));
 398     }
 399     skipwhitespace(constraint, offset);
 400     if (constraint[offset++] != ')')
 401       doExit();
 402     mergeVars(v1, v2);
 403     return;
 404   } else if (strncmp(&constraint[offset], "tr", 2) == 0){
 405         offset+=4;
 406         skipwhitespace(constraint, offset);
 407         return;
 408   }
 409   else{
 410         int32_t b1 = getBooleanVar(constraint, offset);
 411         intwrapper iwb1(b1);
 412         if(boolSet->get(&iwb1) == NULL){
 413             boolSet->add(new intwrapper(b1));
 414         }
 415         skipwhitespace(constraint, offset);
 416 return;
 417   }
 418 }
 419
 420 BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset) {
 421   skipwhitespace(constraint, offset);
 422   if (strncmp(&constraint[offset], "(and", 4) == 0) {
 423     offset +=4;
 424     Vector<BooleanEdge> vec;
 425     while(true) {
 426       skipwhitespace(constraint, offset);
 427       if (constraint[offset] == ')') {
 428         offset++;
 429         return solver->applyLogicalOperation(SATC_AND, vec.expose(), vec.getSize());
 430       }
 431       vec.push(parseConstraint(solver, constraint, offset));
 432     }
 433   } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
 434     offset+=2;
 435     skipwhitespace(constraint, offset);
 436     int32_t v1 = getOrderVar(constraint, offset);
 437     intwrapper iwv1(v1);
 438     if(intSet->get(&iwv1) == NULL){
 439         intSet->add(new intwrapper(v1));
 440     }
 441     skipwhitespace(constraint, offset);
 442     int32_t v2 = getOrderVar(constraint, offset);
 443     intwrapper iwv2(v2);
 444     if(intSet->get(&iwv2) == NULL){
 445         intSet->add(new intwrapper(v2));
 446     }
 447     skipwhitespace(constraint, offset);
 448     if (constraint[offset++] != ')')
 449       doExit();
 450     return solver->orderConstraint(order, checkordervar(solver, v1), checkordervar(solver, v2));
 451   } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
 452     offset+=2;
 453     skipwhitespace(constraint, offset);
 454     getOrderVar(constraint, offset);
 455     skipwhitespace(constraint, offset);
 456     getOrderVar(constraint, offset);
 457     skipwhitespace(constraint, offset);
 458     if (constraint[offset++] != ')')
 459       doExit();
 460     return solver->getBooleanTrue();
 461   }else if (strncmp(&constraint[offset], "tr", 2) == 0){
 462         offset+=4;
 463         skipwhitespace(constraint, offset);
 464         return solver->getBooleanTrue();
 465   }
 466   else {
 467     int32_t v = getBooleanVar(constraint, offset);
 468     intwrapper iwb1(v);
 469     if(boolSet->get(&iwb1) == NULL){
 470         boolSet->add(new intwrapper(v));
 471     }
 472     skipwhitespace(constraint, offset);
 473     return checkBooleanVar(solver, v);
 474   }
 475 }
 476
 477 int skipahead(const char * token1, const char * token2) {
 478   int index1 = 0, index2 = 0;
 479   char buffer[256];
 480   while(true) {
 481     if (token1[index1] == 0)
 482       return 1;
 483     if (token2[index2] == 0)
 484       return 2;
 485     if (file->eof())
 486       return 0;
 487     file->read(buffer, 1);
 488     if (buffer[0] == token1[index1])
 489       index1++;
 490     else
 491       index1 = 0;
 492     if (buffer[0] == token2[index2])
 493       index2++;
 494     else
 495       index2 = 0;
 496   }
 497 }
 498
 499 char * readuntilend(const char * token) {
 500   int index = 0;
 501   char buffer[256];
 502   int length = 256;
 503   int offset = 0;
 504   char * outbuffer = (char *) malloc(length);
 505   while(true) {
 506     if (token[index] == 0) {
 507       outbuffer[offset - index] = 0;
 508       return outbuffer;
 509     }
 510     if (file->eof()) {
 511       free(outbuffer);
 512       return NULL;
 513     }
 514
 515     file->read(buffer, 1);
 516     outbuffer[offset++] = buffer[0];
 517     if (offset == length) {
 518       length = length * 2;
 519       outbuffer = (char *) realloc(outbuffer, length);
 520     }
 521     if (buffer[0] == token[index])
 522       index++;
 523     else
 524       index=0;
 525   }
 526 }