constgen.cc

   1 /*      Copyright (c) 2015 Regents of the University of California
   2  *
   3  *      Author: Brian Demsky <bdemsky@uci.edu>
   4  *
   5  *      This program is free software; you can redistribute it and/or
   6  *      modify it under the terms of the GNU General Public License
   7  *      version 2 as published by the Free Software Foundation.
   8  */
   9
  10 #include "constgen.h"
  11 #include "mcexecution.h"
  12 #include "constraint.h"
  13 #include "branchrecord.h"
  14 #include "functionrecord.h"
  15 #include "equalsrecord.h"
  16 #include "storeloadset.h"
  17 #include "loadrf.h"
  18 #include "schedulebuilder.h"
  19 #include "model.h"
  20 #include <fcntl.h>
  21 #include <unistd.h>
  22 #include <sys/stat.h>
  23 #include "inc_solver.h"
  24 #include <sys/time.h>
  25
  26 long long myclock() {
  27         struct timeval tv;
  28         gettimeofday(&tv, NULL);
  29         return tv.tv_sec*1000000+tv.tv_usec;
  30 }
  31
  32 ConstGen::ConstGen(MCExecution *e) :
  33         storeloadtable(new StoreLoadSetHashTable()),
  34         loadtable(new LoadHashTable()),
  35         execution(e),
  36         workstack(new ModelVector<EPRecord *>()),
  37         threadactions(new ModelVector<ModelVector<EPRecord *> *>()),
  38         rpt(new RecPairTable()),
  39         numconstraints(0),
  40         goalset(new ModelVector<Constraint *>()),
  41         yieldlist(new ModelVector<EPRecord *>()),
  42         goalvararray(NULL),
  43         vars(new ModelVector<Constraint *>()),
  44         branchtable(new BranchTable()),
  45         functiontable(new FunctionTable()),
  46         equalstable(new EqualsTable()),
  47         schedulebuilder(new ScheduleBuilder(e, this)),
  48         nonlocaltrans(new RecordSet()),
  49         incompleteexploredbranch(new RecordSet()),
  50         execcondtable(new LoadHashTable()),
  51         solver(NULL),
  52         rectoint(new RecToIntTable()),
  53         yieldtable(new RecToConsTable()),
  54         varindex(1),
  55         schedule_graph(0),
  56         has_untaken_branches(false)
  57 {
  58 #ifdef STATS
  59         curr_stat=new MC_Stat();
  60         curr_stat->time=0;
  61         curr_stat->was_incremental=false;
  62         curr_stat->was_sat=true;
  63         curr_stat->fgoals=0;
  64         curr_stat->bgoals=0;
  65         stats=new ModelVector<struct MC_Stat *>();
  66 #endif
  67 }
  68
  69 ConstGen::~ConstGen() {
  70         reset();
  71         if (solver != NULL)
  72                 delete solver;
  73         for(uint i=0;i<vars->size();i++) {
  74                 Constraint *var=(*vars)[i];
  75                 Constraint *notvar=var->neg;
  76                 delete var;
  77                 delete notvar;
  78         }
  79         vars->clear();
  80         delete storeloadtable;
  81         delete loadtable;
  82         delete workstack;
  83         delete threadactions;
  84         delete rpt;
  85         delete goalset;
  86         delete yieldlist;
  87         delete vars;
  88         delete branchtable;
  89         delete functiontable;
  90         delete equalstable;
  91         delete schedulebuilder;
  92         delete nonlocaltrans;
  93         delete incompleteexploredbranch;
  94         delete execcondtable;
  95         delete rectoint;
  96         delete yieldtable;
  97 }
  98
  99 void resetstoreloadtable(StoreLoadSetHashTable * storeloadtable) {
 100         for(uint i=0;i<storeloadtable->capacity;i++) {
 101                 struct hashlistnode<const void *, StoreLoadSet *> * ptr=&storeloadtable->table[i];
 102                 if (ptr->val != NULL) {
 103                         if (ptr->val->removeAddress(ptr->key))
 104                                 delete ptr->val;
 105                         ptr->val=NULL;
 106                         ptr->key=NULL;
 107                 }
 108         }
 109
 110         if (storeloadtable->zero != NULL) {
 111                 if (storeloadtable->zero->val->removeAddress(storeloadtable->zero->key)) {
 112                         delete storeloadtable->zero->val;
 113                 } else
 114                         ASSERT(false);
 115                 model_free(storeloadtable->zero);
 116                 storeloadtable->zero = NULL;
 117         }
 118         storeloadtable->size = 0;
 119 }
 120
 121 void ConstGen::reset() {
 122         for(uint i=0;i<threadactions->size();i++) {
 123                 delete (*threadactions)[i];
 124         }
 125         if (goalvararray != NULL) {
 126                 model_free(goalvararray);
 127                 goalvararray=NULL;
 128         }
 129         functiontable->resetanddelete();
 130         equalstable->resetanddelete();
 131         branchtable->resetanddelete();
 132         loadtable->resetanddelete();
 133         execcondtable->resetanddelete();
 134         rpt->resetanddelete();
 135         resetstoreloadtable(storeloadtable);
 136         nonlocaltrans->reset();
 137         incompleteexploredbranch->reset();
 138         threadactions->clear();
 139         rectoint->reset();
 140         yieldtable->reset();
 141         yieldlist->clear();
 142         goalset->clear();
 143         varindex=1;
 144         numconstraints=0;
 145         has_untaken_branches=false;
 146 }
 147
 148 void ConstGen::translateGoals() {
 149         int size=goalset->size();
 150         goalvararray=(Constraint **) model_malloc(size*sizeof(Constraint *));
 151
 152         for(int i=0;i<size;i++) {
 153                 Constraint *goal=(*goalset)[i];
 154                 goalvararray[i]=getNewVar();
 155                 addConstraint(new Constraint(OR, goalvararray[i]->negate(), goal));
 156         }
 157         Constraint *atleastonegoal=new Constraint(OR, size, goalvararray);
 158         ADDCONSTRAINT(atleastonegoal, "atleastonegoal");
 159 }
 160
 161 bool ConstGen::canReuseEncoding() {
 162         if (solver == NULL)
 163                 return false;
 164         Constraint *array[goalset->size()];
 165         int remaininggoals=0;
 166
 167         //Zero out the achieved goals
 168         for(uint i=0;i<goalset->size();i++) {
 169                 Constraint *var=goalvararray[i];
 170                 if (var != NULL) {
 171                         array[remaininggoals++]=var;
 172                 }
 173         }
 174         if (remaininggoals == 0)
 175                 return false;
 176         Constraint *atleastonegoal=new Constraint(OR, remaininggoals, array);
 177         ADDCONSTRAINT(atleastonegoal, "atleastonegoal");
 178         solver->finishedClauses();
 179         clock_t start=myclock();
 180         bool *solution=runSolver();
 181         clock_t finish=myclock();
 182 #ifdef STATS
 183         if (curr_stat != NULL)
 184                 stats->push_back(curr_stat);
 185         curr_stat=new MC_Stat();
 186         curr_stat->time=finish-start;
 187         curr_stat->was_incremental=true;
 188         curr_stat->was_sat=(solution!=NULL);
 189         curr_stat->fgoals=0;
 190         curr_stat->bgoals=0;
 191 #endif
 192         model_print("start %lu, finish %lu\n", start,finish);
 193         model_print("Incremental time = %12.6f\n", ((double)(finish-start))/1000000);
 194
 195         if (solution==NULL) {
 196                 return false;
 197         }
 198
 199         //Zero out the achieved goals
 200         for(uint i=0;i<goalset->size();i++) {
 201                 Constraint *var=goalvararray[i];
 202                 if (var != NULL) {
 203                         if (solution[var->getVar()]) {
 204                                 //if (goalvararray[i] != NULL)
 205                                 //model_print("SAT clearing goal %d.\n", i);
 206
 207                                 goalvararray[i]=NULL;
 208                         }
 209                 }
 210         }
 211
 212         schedulebuilder->buildSchedule(solution);
 213         model_free(solution);
 214
 215         return true;
 216 }
 217
 218 bool ConstGen::process() {
 219 #ifdef DUMP_EVENT_GRAPHS
 220         printEventGraph();
 221 #endif
 222
 223         if (solver != NULL) {
 224                 delete solver;
 225                 solver = NULL;
 226         }
 227
 228         solver=new IncrementalSolver();
 229
 230         traverse(true);
 231         genTransOrderConstraints();
 232 #ifdef TSO
 233         genTSOTransOrderConstraints();
 234 #endif
 235         traverse(false);
 236         translateGoals();
 237         if (goalset->size()==0) {
 238 #ifdef STATS
 239                 stats->push_back(curr_stat);
 240                 for(uint i=0;i<stats->size();i++) {
 241                         struct MC_Stat *s=(*stats)[i];
 242                         model_print("time=%lld fgoals=%d bgoals=%d incremental=%d sat=%d\n", s->time, s->fgoals, s->bgoals, s->was_incremental, s->was_sat);
 243                 }
 244 #endif
 245                 model_print("No goals, done\n");
 246                 delete solver;
 247                 solver = NULL;
 248                 return true;
 249         }
 250
 251         if (model->params.branches && !has_untaken_branches) {
 252                 delete solver;
 253                 solver = NULL;
 254                 return true;
 255         }
 256
 257         solver->finishedClauses();
 258
 259         //Freeze the goal variables
 260         for(uint i=0;i<goalset->size();i++) {
 261                 Constraint *var=goalvararray[i];
 262                 solver->freeze(var->getVar());
 263         }
 264
 265         clock_t start=myclock();
 266         bool *solution=runSolver();
 267         clock_t finish=myclock();
 268 #ifdef STATS
 269         if (curr_stat != NULL)
 270                 stats->push_back(curr_stat);
 271         curr_stat=new MC_Stat();
 272         curr_stat->time=finish-start;
 273         curr_stat->was_incremental=false;
 274         curr_stat->was_sat=(solution!=NULL);
 275         curr_stat->fgoals=0;
 276         curr_stat->bgoals=0;
 277
 278         if (solution == NULL) {
 279                 stats->push_back(curr_stat);
 280                 for(uint i=0;i<stats->size();i++) {
 281                         struct MC_Stat *s=(*stats)[i];
 282                         model_print("time=%lld fgoals=%d bgoals=%d  incremental=%d sat=%d\n", s->time, s->fgoals, s->bgoals, s->was_incremental, s->was_sat);
 283                 }
 284
 285         }
 286 #endif
 287
 288         model_print("start %lu, finish %lu\n", start,finish);
 289         model_print("Initial time = %12.6f\n", ((double)(finish-start))/1000000);
 290
 291
 292         if (solution==NULL) {
 293                 delete solver;
 294                 solver = NULL;
 295                 return true;
 296         }
 297
 298         //Zero out the achieved goals
 299         for(uint i=0;i<goalset->size();i++) {
 300                 Constraint *var=goalvararray[i];
 301                 if (var != NULL) {
 302                         if (solution[var->getVar()]) {
 303                                 //if (goalvararray[i] != NULL)
 304                                 //      model_print("SAT clearing goal %d.\n", i);
 305                                 goalvararray[i]=NULL;
 306                         }
 307                 }
 308         }
 309
 310         schedulebuilder->buildSchedule(solution);
 311         model_free(solution);
 312         return false;
 313 }
 314
 315 void ConstGen::printEventGraph() {
 316         char buffer[128];
 317         sprintf(buffer, "eventgraph%u.dot",schedule_graph);
 318         schedule_graph++;
 319         int file=open(buffer,O_WRONLY|O_CREAT|O_TRUNC, S_IRWXU);
 320         model_dprintf(file, "digraph eventgraph {\n");
 321
 322         EPRecord *first=execution->getEPRecord(MCID_FIRST);
 323         printRecord(first, file);
 324         while(!workstack->empty()) {
 325                 EPRecord *record=workstack->back();
 326                 workstack->pop_back();
 327                 printRecord(record, file);
 328         }
 329
 330         model_dprintf(file, "}\n");
 331         close(file);
 332 }
 333
 334 void ConstGen::doPrint(EPRecord *record, int file) {
 335         model_dprintf(file, "%lu[label=\"",(uintptr_t)record);
 336         record->print(file);
 337         model_dprintf(file, "\"];\n");
 338         if (record->getNextRecord()!=NULL)
 339                 model_dprintf(file, "%lu->%lu;\n", (uintptr_t) record, (uintptr_t) record->getNextRecord());
 340
 341         if (record->getChildRecord()!=NULL)
 342                 model_dprintf(file, "%lu->%lu[color=red];\n", (uintptr_t) record, (uintptr_t) record->getChildRecord());
 343 }
 344
 345 void ConstGen::printRecord(EPRecord *record, int file) {
 346         do {
 347                 doPrint(record,file);
 348
 349                 if (record->getType()==LOOPENTER) {
 350                         workstack->push_back(record->getNextRecord());
 351                         workstack->push_back(record->getChildRecord());
 352                         return;
 353                 }
 354                 if (record->getChildRecord()!=NULL) {
 355                         workstack->push_back(record->getChildRecord());
 356                 }
 357                 if (record->getType()==NONLOCALTRANS) {
 358                         return;
 359                 }
 360                 if (record->getType()==LOOPEXIT) {
 361                         return;
 362                 }
 363                 if (record->getType()==BRANCHDIR) {
 364                         EPRecord *next=record->getNextRecord();
 365                         if (next != NULL)
 366                                 workstack->push_back(next);
 367                         for(uint i=0;i<record->numValues();i++) {
 368                                 EPValue *branchdir=record->getValue(i);
 369
 370                                 //Could have an empty branch, so make sure the branch actually
 371                                 //runs code
 372                                 if (branchdir->getFirstRecord()!=NULL) {
 373                                         workstack->push_back(branchdir->getFirstRecord());
 374                                         model_dprintf(file, "%lu->%lu[color=blue];\n", (uintptr_t) record, (uintptr_t) branchdir->getFirstRecord());
 375                                 }
 376                         }
 377                         return;
 378                 } else
 379                         record=record->getNextRecord();
 380         } while(record!=NULL);
 381 }
 382
 383
 384 /* This function traverses a thread's graph in execution order.  */
 385
 386 void ConstGen::traverse(bool initial) {
 387         EPRecord *first=execution->getEPRecord(MCID_FIRST);
 388         traverseRecord(first, initial);
 389         while(!workstack->empty()) {
 390                 EPRecord *record=workstack->back();
 391                 workstack->pop_back();
 392                 traverseRecord(record, initial);
 393         }
 394 }
 395
 396 /** This method looks for all other memory operations that could
 397                 potentially share a location, and build partitions of memory
 398                 locations such that all memory locations that can share the same
 399                 address are in the same group.
 400
 401                 These memory operations should share an encoding of addresses and
 402                 values.
 403  */
 404
 405 void ConstGen::groupMemoryOperations(EPRecord *op) {
 406         /** Handle our first address */
 407         IntHashSet *addrset=op->getSet(VC_ADDRINDEX);
 408         IntIterator *ait=addrset->iterator();
 409
 410         void *iaddr=(void *) ait->next();
 411         StoreLoadSet *isls=storeloadtable->get(iaddr);
 412         if (isls==NULL) {
 413                 isls=new StoreLoadSet();
 414                 storeloadtable->put(iaddr, isls);
 415         }
 416         isls->add(op);
 417
 418         while(ait->hasNext()) {
 419                 void *addr=(void *)ait->next();
 420                 StoreLoadSet *sls=storeloadtable->get(addr);
 421                 if (sls==NULL) {
 422                         storeloadtable->put(addr, isls);
 423                 } else if (sls!=isls) {
 424                         //must do merge
 425                         mergeSets(isls, sls);
 426                 }
 427         }
 428         delete ait;
 429 }
 430
 431
 432 RecordSet * ConstGen::computeConflictSet(EPRecord *store, EPRecord *load, RecordSet * baseset) {
 433         //See if we can determine addresses that store/load may use
 434         IntIterator * storeaddr=store->getSet(VC_ADDRINDEX)->iterator();
 435         int numaddr=0;void *commonaddr=NULL;
 436         while(storeaddr->hasNext()) {
 437                 void *addr=(void *) storeaddr->next();
 438                 if (load->getSet(VC_ADDRINDEX)->contains((uint64_t)addr)) {
 439                         commonaddr=addr;
 440                         numaddr++;
 441                 }
 442         }
 443         delete storeaddr;
 444
 445         ASSERT(numaddr!=0);
 446         if (numaddr!=1)
 447                 return NULL;
 448
 449         RecordSet *srscopy=baseset->copy();
 450         RecordIterator *sri=srscopy->iterator();
 451         while(sri->hasNext()) {
 452                 bool pruneconflictstore=false;
 453                 EPRecord *conflictstore=sri->next();
 454                 bool conflictafterstore=getOrderConstraint(store,conflictstore)->isTrue();
 455                 bool conflictbeforeload=getOrderConstraint(conflictstore,load)->isTrue();
 456
 457                 if (conflictafterstore) {
 458                         RecordIterator *sricheck=srscopy->iterator();
 459                         while(sricheck->hasNext()) {
 460                                 EPRecord *checkstore=sricheck->next();
 461                                 bool checkafterstore=getOrderConstraint(store, checkstore)->isTrue();
 462                                 if (!checkafterstore)
 463                                         continue;
 464                                 bool checkbeforeconflict=getOrderConstraint(checkstore,conflictstore)->isTrue();
 465                                 if (!checkbeforeconflict)
 466                                         continue;
 467
 468                                 //See if the checkstore must store to the relevant address
 469                                 IntHashSet * storeaddr=checkstore->getSet(VC_ADDRINDEX);
 470
 471                                 if (storeaddr->getSize()!=1 || !storeaddr->contains((uint64_t)commonaddr))
 472                                         continue;
 473
 474
 475                                 if (subsumesExecutionConstraint(checkstore, conflictstore)) {
 476                                         pruneconflictstore=true;
 477                                         break;
 478                                 }
 479                         }
 480                         delete sricheck;
 481                 }
 482
 483                 if (conflictbeforeload && !pruneconflictstore) {
 484                         RecordIterator *sricheck=srscopy->iterator();
 485                         while(sricheck->hasNext()) {
 486                                 EPRecord *checkstore=sricheck->next();
 487
 488                                 bool checkafterconflict=getOrderConstraint(conflictstore, checkstore)->isTrue();
 489                                 if (!checkafterconflict)
 490                                         continue;
 491
 492                                 bool checkbeforeload=getOrderConstraint(checkstore, load)->isTrue();
 493                                 if (!checkbeforeload)
 494                                         continue;
 495
 496                                 //See if the checkstore must store to the relevant address
 497                                 IntHashSet * storeaddr=checkstore->getSet(VC_ADDRINDEX);
 498                                 if (storeaddr->getSize()!=1 || !storeaddr->contains((uint64_t)commonaddr))
 499                                         continue;
 500
 501
 502                                 if (subsumesExecutionConstraint(checkstore, conflictstore)) {
 503                                         pruneconflictstore=true;
 504                                         break;
 505                                 }
 506                         }
 507                         delete sricheck;
 508                 }
 509                 if (pruneconflictstore) {
 510                         //This store is redundant
 511                         sri->remove();
 512                 }
 513         }
 514
 515         delete sri;
 516         return srscopy;
 517 }
 518
 519
 520 /** This method returns all stores that a load may read from. */
 521
 522 RecordSet * ConstGen::getMayReadFromSet(EPRecord *load) {
 523         if (load->getSet(VC_ADDRINDEX)->getSize()==1)
 524                 return getMayReadFromSetOpt(load);
 525
 526         RecordSet *srs=loadtable->get(load);
 527         ExecPoint *epload=load->getEP();
 528         thread_id_t loadtid=epload->get_tid();
 529         if (srs==NULL) {
 530                 srs=new RecordSet();
 531                 loadtable->put(load, srs);
 532
 533                 IntHashSet *addrset=load->getSet(VC_ADDRINDEX);
 534                 IntIterator *ait=addrset->iterator();
 535
 536                 while(ait->hasNext()) {
 537                         void *addr=(void *)ait->next();
 538                         RecordSet *rs=execution->getStoreTable(addr);
 539                         if (rs==NULL)
 540                                 continue;
 541
 542                         RecordIterator * rit=rs->iterator();
 543                         while(rit->hasNext()) {
 544                                 EPRecord *rec=rit->next();
 545                                 ExecPoint *epstore=rec->getEP();
 546                                 thread_id_t storetid=epstore->get_tid();
 547                                 if (storetid != loadtid ||
 548                                                 epstore->compare(epload) == CR_AFTER)
 549                                         srs->add(rec);
 550                         }
 551                         delete rit;
 552                 }
 553                 delete ait;
 554         }
 555         return srs;
 556 }
 557
 558
 559 RecordSet * ConstGen::getMayReadFromSetOpt(EPRecord *load) {
 560         RecordSet *srs=loadtable->get(load);
 561         ExecPoint *epload=load->getEP();
 562         thread_id_t loadtid=epload->get_tid();
 563         if (srs==NULL) {
 564                 srs=new RecordSet();
 565                 loadtable->put(load, srs);
 566
 567                 IntHashSet *addrset=load->getSet(VC_ADDRINDEX);
 568                 IntIterator *ait=addrset->iterator();
 569                 void *addr=(void *)ait->next();
 570                 delete ait;
 571
 572                 RecordSet *rs=execution->getStoreTable(addr);
 573                 RecordIterator * rit=rs->iterator();
 574                 ExecPoint *latest=NULL;
 575                 while(rit->hasNext()) {
 576                         EPRecord *store=rit->next();
 577                         ExecPoint *epstore=store->getEP();
 578                         thread_id_t storetid=epstore->get_tid();
 579                         if (storetid == loadtid && isAlwaysExecuted(store) &&
 580                                         store->getSet(VC_ADDRINDEX)->getSize()==1 &&
 581                                         epstore->compare(epload) == CR_AFTER &&
 582                                         (latest==NULL || latest->compare(epstore) == CR_AFTER)) {
 583                                 latest=epstore;
 584                         }
 585                 }
 586                 delete rit;
 587                 rit=rs->iterator();
 588                 while(rit->hasNext()) {
 589                         EPRecord *store=rit->next();
 590                         ExecPoint *epstore=store->getEP();
 591                         thread_id_t storetid=epstore->get_tid();
 592                         if (storetid == loadtid) {
 593                                 if (epstore->compare(epload) == CR_AFTER &&
 594                                                 (latest==NULL || epstore->compare(latest) != CR_AFTER))
 595                                         srs->add(store);
 596                         } else {
 597                                 srs->add(store);
 598                         }
 599                 }
 600                 delete rit;
 601         }
 602         return srs;
 603 }
 604
 605 /** This function merges two recordsets and updates the storeloadtable
 606                 accordingly. */
 607
 608 void ConstGen::mergeSets(StoreLoadSet *to, StoreLoadSet *from) {
 609         RecordIterator * sri=from->iterator();
 610         while(sri->hasNext()) {
 611                 EPRecord *rec=sri->next();
 612                 to->add(rec);
 613                 IntHashSet *addrset=rec->getSet(VC_ADDRINDEX);
 614                 IntIterator *ait=addrset->iterator();
 615                 while(ait->hasNext()) {
 616                         void *addr=(void *)ait->next();
 617                         storeloadtable->put(addr, to);
 618                 }
 619                 delete ait;
 620         }
 621         delete sri;
 622         delete from;
 623 }
 624
 625 #ifdef TSO
 626 /** This function creates ordering variables between stores and loads
 627  *  in same thread for TSO.  */
 628
 629 void ConstGen::insertTSOAction(EPRecord *load) {
 630         if (load->getType() != LOAD)
 631                 return;
 632         ExecPoint *load_ep=load->getEP();
 633         thread_id_t tid=load_ep->get_tid();
 634         uint thread=id_to_int(tid);
 635         ModelVector<EPRecord *> * vector=(*threadactions)[thread];
 636         uint j=vector->size()-1;
 637         while (j>0) {
 638                 EPRecord *oldrec=(*vector)[--j];
 639                 EventType oldrec_t=oldrec->getType();
 640
 641                 if (((oldrec_t == RMW) || (oldrec_t==FENCE)) &&
 642                                 isAlwaysExecuted(oldrec)) {
 643                         return;
 644                 } else if (oldrec_t == STORE) {
 645                         /* Only generate variables for things that can actually both run */
 646
 647                         createOrderConstraint(oldrec, load);
 648                 }
 649         }
 650 }
 651
 652 void ConstGen::genTSOTransOrderConstraints() {
 653         for(uint t1=0;t1<threadactions->size();t1++) {
 654                 ModelVector<EPRecord *> *tvec=(*threadactions)[t1];
 655                 uint size=tvec->size();
 656                 EPRecord *laststore=NULL;
 657                 for(uint store_i=0;store_i<size;store_i++) {
 658                         EPRecord *store=(*tvec)[store_i];
 659                         EventType store_t=store->getType();
 660                         if (store_t != STORE)
 661                                 continue;
 662                         EPRecord *lastload=NULL;
 663                         for(uint load_i=store_i+1;load_i<size;load_i++) {
 664                                 EPRecord *rec=(*tvec)[store_i];
 665                                 //Hit fence, don't need more stuff
 666                                 EventType rec_t=rec->getType();
 667                                 if (((rec_t == RMW) || (rec_t == FENCE)) &&
 668                                                 isAlwaysExecuted(rec))
 669                                         break;
 670                                 if (rec_t != LOAD)
 671                                         continue;
 672                                 if (laststore != NULL) {
 673                                         Constraint * storeload=getOrderConstraint(store, rec);
 674                                         Constraint * earlystoreload=getOrderConstraint(laststore, rec);
 675                                         Constraint * c=new Constraint(IMPLIES, storeload, earlystoreload);
 676                                         ADDCONSTRAINT(c, "earlystore");
 677                                 }
 678                                 if (lastload != NULL) {
 679                                         Constraint * storeearlyload=getOrderConstraint(store, lastload);
 680                                         Constraint * storeload=getOrderConstraint(store, rec);
 681                                         Constraint * c=new Constraint(IMPLIES, storeearlyload, storeload);
 682                                         ADDCONSTRAINT(c, "earlyload");
 683                                 }
 684                                 lastload=rec;
 685                         }
 686                         laststore=store;
 687                 }
 688         }
 689 }
 690 #endif
 691
 692 /** This function creates ordering constraints to implement SC for
 693                 memory operations.  */
 694
 695 void ConstGen::insertAction(EPRecord *record) {
 696         thread_id_t tid=record->getEP()->get_tid();
 697         uint thread=id_to_int(tid);
 698         if (threadactions->size()<=thread) {
 699                 uint oldsize=threadactions->size();
 700                 threadactions->resize(thread+1);
 701                 for(;oldsize<=thread;oldsize++) {
 702                         (*threadactions)[oldsize]=new ModelVector<EPRecord *>();
 703                 }
 704         }
 705
 706         (*threadactions)[thread]->push_back(record);
 707
 708         for(uint i=0;i<threadactions->size();i++) {
 709                 if (i==thread)
 710                         continue;
 711                 ModelVector<EPRecord *> * vector=(*threadactions)[i];
 712                 for(uint j=0;j<vector->size();j++) {
 713                         EPRecord *oldrec=(*vector)[j];
 714                         createOrderConstraint(oldrec, record);
 715                 }
 716         }
 717 #ifdef TSO
 718         insertTSOAction(record);
 719 #endif
 720 }
 721
 722 void ConstGen::genTransOrderConstraints() {
 723         for(uint t1=0;t1<threadactions->size();t1++) {
 724                 ModelVector<EPRecord *> *t1vec=(*threadactions)[t1];
 725                 for(uint t2=0;t2<t1;t2++) {
 726                         ModelVector<EPRecord *> *t2vec=(*threadactions)[t2];
 727                         genTransOrderConstraints(t1vec, t2vec);
 728                         genTransOrderConstraints(t2vec, t1vec);
 729                         for(uint t3=0;t3<t2;t3++) {
 730                                 ModelVector<EPRecord *> *t3vec=(*threadactions)[t3];
 731                                 genTransOrderConstraints(t1vec, t2vec, t3vec);
 732                         }
 733                 }
 734         }
 735 }
 736
 737 void ConstGen::genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVector<EPRecord *> *t2vec) {
 738         for(uint t1i=0;t1i<t1vec->size();t1i++) {
 739                 EPRecord *t1rec=(*t1vec)[t1i];
 740                 for(uint t2i=0;t2i<t2vec->size();t2i++) {
 741                         EPRecord *t2rec=(*t2vec)[t2i];
 742
 743                         /* Note: One only really needs to generate the first constraint
 744                                  in the first loop and the last constraint in the last loop.
 745                                  I tried this and performance suffered on linuxrwlocks and
 746                                  linuxlocks at the current time. BD - August 2014*/
 747                         Constraint *c21=getOrderConstraint(t2rec, t1rec);
 748
 749                         /* short circuit for the trivial case */
 750                         if (c21->isTrue())
 751                                 continue;
 752
 753                         for(uint t3i=t2i+1;t3i<t2vec->size();t3i++) {
 754                                 EPRecord *t3rec=(*t2vec)[t3i];
 755                                 Constraint *c13=getOrderConstraint(t1rec, t3rec);
 756 #ifdef TSO
 757                                 Constraint *c32=getOrderConstraint(t3rec, t2rec);
 758                                 if (!c32->isFalse()) {
 759                                         //Have a store->load that could be reordered, need to generate other constraint
 760                                         Constraint *c12=getOrderConstraint(t1rec, t2rec);
 761                                         Constraint *c23=getOrderConstraint(t2rec, t3rec);
 762                                         Constraint *c31=getOrderConstraint(t3rec, t1rec);
 763                                         Constraint *slarray[] = {c31, c23, c12};
 764                                         Constraint * intradelayedstore=new Constraint(OR, 3, slarray);
 765                                         ADDCONSTRAINT(intradelayedstore, "intradelayedstore");
 766                                 }
 767                                 Constraint * array[]={c21, c32, c13};
 768                                 Constraint *intratransorder=new Constraint(OR, 3, array);
 769 #else
 770                                 Constraint *intratransorder=new Constraint(OR, c21, c13);
 771 #endif
 772                                 ADDCONSTRAINT(intratransorder,"intratransorder");
 773                         }
 774
 775                         for(uint t0i=0;t0i<t1i;t0i++) {
 776                                 EPRecord *t0rec=(*t1vec)[t0i];
 777                                 Constraint *c02=getOrderConstraint(t0rec, t2rec);
 778 #ifdef TSO
 779                                 Constraint *c10=getOrderConstraint(t1rec, t0rec);
 780
 781                                 if (!c10->isFalse()) {
 782                                         //Have a store->load that could be reordered, need to generate other constraint
 783                                         Constraint *c01=getOrderConstraint(t0rec, t1rec);
 784                                         Constraint *c12=getOrderConstraint(t1rec, t2rec);
 785                                         Constraint *c20=getOrderConstraint(t2rec, t0rec);
 786                                         Constraint *slarray[] = {c01, c12, c20};
 787                                         Constraint * intradelayedstore=new Constraint(OR, 3, slarray);
 788                                         ADDCONSTRAINT(intradelayedstore, "intradelayedstore");
 789                                 }
 790                                 Constraint * array[]={c10, c21, c02};
 791                                 Constraint *intratransorder=new Constraint(OR, 3, array);
 792 #else
 793                                 Constraint *intratransorder=new Constraint(OR, c21, c02);
 794 #endif
 795                                 ADDCONSTRAINT(intratransorder,"intratransorder");
 796                         }
 797                 }
 798         }
 799 }
 800
 801
 802 void ConstGen::genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVector<EPRecord *> *t2vec, ModelVector<EPRecord *> * t3vec) {
 803         for(uint t1i=0;t1i<t1vec->size();t1i++) {
 804                 EPRecord *t1rec=(*t1vec)[t1i];
 805                 for(uint t2i=0;t2i<t2vec->size();t2i++) {
 806                         EPRecord *t2rec=(*t2vec)[t2i];
 807                         for(uint t3i=0;t3i<t3vec->size();t3i++) {
 808                                 EPRecord *t3rec=(*t3vec)[t3i];
 809                                 genTransOrderConstraint(t1rec, t2rec, t3rec);
 810                         }
 811                 }
 812         }
 813 }
 814
 815 void ConstGen::genTransOrderConstraint(EPRecord *t1rec, EPRecord *t2rec, EPRecord *t3rec) {
 816         Constraint *c21=getOrderConstraint(t2rec, t1rec);
 817         Constraint *c32=getOrderConstraint(t3rec, t2rec);
 818         Constraint *c13=getOrderConstraint(t1rec, t3rec);
 819         Constraint * cimpl1[]={c21, c32, c13};
 820         Constraint * c1=new Constraint(OR, 3, cimpl1);
 821         ADDCONSTRAINT(c1, "intertransorder");
 822
 823         Constraint *c12=getOrderConstraint(t1rec, t2rec);
 824         Constraint *c23=getOrderConstraint(t2rec, t3rec);
 825         Constraint *c31=getOrderConstraint(t3rec, t1rec);
 826         Constraint * cimpl2[]={c12, c23, c31};
 827         Constraint *c2=new Constraint(OR, 3, cimpl2);
 828         ADDCONSTRAINT(c2, "intertransorder");
 829 }
 830
 831 void ConstGen::addGoal(EPRecord *r, Constraint *c) {
 832         rectoint->put(r, goalset->size());
 833         goalset->push_back(c);
 834 }
 835
 836 void ConstGen::addBranchGoal(EPRecord *r, Constraint *c) {
 837         has_untaken_branches=true;
 838         rectoint->put(r, goalset->size());
 839         goalset->push_back(c);
 840 }
 841
 842 void ConstGen::achievedGoal(EPRecord *r) {
 843         if (rectoint->contains(r)) {
 844                 uint index=rectoint->get(r);
 845                 //if (goalvararray[index] != NULL)
 846                 //model_print("Run Clearing goal index %d\n",index);
 847                 goalvararray[index]=NULL;
 848         }
 849 }
 850
 851 void ConstGen::addConstraint(Constraint *c) {
 852         ModelVector<Constraint *> *vec=c->simplify();
 853         for(uint i=0;i<vec->size();i++) {
 854                 Constraint *simp=(*vec)[i];
 855                 if (simp->type==TRUE)
 856                         continue;
 857                 ASSERT(simp->type!=FALSE);
 858                 simp->printDIMACS(this);
 859 #ifdef VERBOSE_CONSTRAINTS
 860                 simp->print();
 861                 model_print("\n");
 862 #endif
 863                 numconstraints++;
 864                 simp->freerec();
 865         }
 866         delete vec;
 867 }
 868
 869 void ConstGen::printNegConstraint(uint value) {
 870         int val=-value;
 871         solver->addClauseLiteral(val);
 872 }
 873
 874 void ConstGen::printConstraint(uint value) {
 875         solver->addClauseLiteral(value);
 876 }
 877
 878 bool * ConstGen::runSolver() {
 879         int solution=solver->solve();
 880         if (solution == IS_UNSAT) {
 881                 return NULL;
 882         } else if (solution == IS_SAT) {
 883                 bool * assignments=(bool *)model_malloc(sizeof(bool)*(varindex+1));
 884                 for(uint i=0;i<=varindex;i++)
 885                         assignments[i]=solver->getValue(i);
 886                 return assignments;
 887         } else {
 888                 delete solver;
 889                 solver=NULL;
 890                 model_print_err("INDETER\n");
 891                 model_print("INDETER\n");
 892                 exit(-1);
 893                 return NULL;
 894         }
 895 }
 896
 897 Constraint * ConstGen::getOrderConstraint(EPRecord *first, EPRecord *second) {
 898 #ifndef TSO
 899         if (first->getEP()->get_tid()==second->getEP()->get_tid()) {
 900                 if (first->getEP()->compare(second->getEP())==CR_AFTER)
 901                         return &ctrue;
 902                 else {
 903                         return &cfalse;
 904                 }
 905         }
 906 #endif
 907         RecPair rp(first, second);
 908         RecPair *rpc=rpt->get(&rp);
 909 #ifdef TSO
 910         if ((rpc==NULL) &&
 911                         first->getEP()->get_tid()==second->getEP()->get_tid()) {
 912                 if (first->getEP()->compare(second->getEP())==CR_AFTER)
 913                         return &ctrue;
 914                 else {
 915                         return &cfalse;
 916                 }
 917         }
 918 #endif
 919         ASSERT(rpc!=NULL);
 920         //      delete rp;
 921         Constraint *c=rpc->constraint;
 922         if (rpc->epr1!=first) {
 923                 //have to flip arguments
 924                 return c->negate();
 925         } else {
 926                 return c;
 927         }
 928 }
 929
 930 bool ConstGen::getOrder(EPRecord *first, EPRecord *second, bool * satsolution) {
 931         RecPair rp(first, second);
 932         RecPair *rpc=rpt->get(&rp);
 933 #ifdef TSO
 934         if ((rpc==NULL) &&
 935                         first->getEP()->get_tid()==second->getEP()->get_tid()) {
 936                 if (first->getEP()->compare(second->getEP())==CR_AFTER)
 937                         return true;
 938                 else {
 939                         return false;
 940                 }
 941         }
 942 #endif
 943
 944         ASSERT(rpc!=NULL);
 945
 946         Constraint *c=rpc->constraint;
 947         CType type=c->getType();
 948         bool order;
 949
 950         if (type==TRUE)
 951                 order=true;
 952         else if (type==FALSE)
 953                 order=false;
 954         else {
 955                 uint index=c->getVar();
 956                 order=satsolution[index];
 957         }
 958         if (rpc->epr1==first)
 959                 return order;
 960         else
 961                 return !order;
 962 }
 963
 964 /** This function determines whether events first and second are
 965  * ordered by start and join operations.  */
 966
 967 bool ConstGen::orderThread(EPRecord *first, EPRecord *second) {
 968         ExecPoint * ep1=first->getEP();
 969         ExecPoint * ep2=second->getEP();
 970         thread_id_t thr1=ep1->get_tid();
 971         thread_id_t thr2=ep2->get_tid();
 972         Thread *tr2=execution->get_thread(thr2);
 973         EPRecord *thr2start=tr2->getParentRecord();
 974         if (thr2start!=NULL) {
 975                 ExecPoint *epthr2start=thr2start->getEP();
 976                 if (epthr2start->get_tid()==thr1 &&
 977                                 ep1->compare(epthr2start)==CR_AFTER)
 978                         return true;
 979         }
 980         ModelVector<EPRecord *> * joinvec=execution->getJoins();
 981         for(uint i=0;i<joinvec->size();i++) {
 982                 EPRecord *join=(*joinvec)[i];
 983                 ExecPoint *jp=join->getEP();
 984                 if (jp->get_tid()==thr2 &&
 985                                 jp->compare(ep2)==CR_AFTER)
 986                         return true;
 987         }
 988         return false;
 989 }
 990
 991 /** This function generates an ordering constraint for two events.  */
 992
 993 void ConstGen::createOrderConstraint(EPRecord *first, EPRecord *second) {
 994         RecPair * rp=new RecPair(first, second);
 995         if (!rpt->contains(rp)) {
 996                 if (orderThread(first, second))
 997                         rp->constraint=&ctrue;
 998                 else if (orderThread(second, first))
 999                         rp->constraint=&cfalse;
1000                 else
1001                         rp->constraint=getNewVar();
1002
1003                 rpt->put(rp, rp);
1004         } else {
1005                 delete rp;
1006         }
1007 }
1008
1009 Constraint * ConstGen::getNewVar() {
1010         Constraint *var;
1011         if (varindex>vars->size()) {
1012                 var=new Constraint(VAR, varindex);
1013                 Constraint *varneg=new Constraint(NOTVAR, varindex);
1014                 var->setNeg(varneg);
1015                 varneg->setNeg(var);
1016                 vars->push_back(var);
1017         } else {
1018                 var=(*vars)[varindex-1];
1019         }
1020         varindex++;
1021         return var;
1022 }
1023
1024 /** Gets an array of new variables.  */
1025
1026 void ConstGen::getArrayNewVars(uint num, Constraint **carray) {
1027         for(uint i=0;i<num;i++)
1028                 carray[i]=getNewVar();
1029 }
1030
1031 StoreLoadSet * ConstGen::getStoreLoadSet(EPRecord *record) {
1032         IntIterator *it=record->getSet(VC_ADDRINDEX)->iterator();
1033         void *addr=(void *)it->next();
1034         delete it;
1035         return storeloadtable->get(addr);
1036 }
1037
1038 /** Returns a constraint that is true if the output of record has the
1039                 given value. */
1040
1041 Constraint * ConstGen::getRetValueEncoding(EPRecord *record, uint64_t value) {
1042         switch(record->getType()) {
1043         case EQUALS:
1044                 return equalstable->get(record)->getValueEncoding(value);
1045         case FUNCTION:
1046                 return functiontable->get(record)->getValueEncoding(value);
1047         case LOAD: {
1048                 return getStoreLoadSet(record)->getValueEncoding(this, record, value);
1049         }
1050         case RMW: {
1051                 return getStoreLoadSet(record)->getRMWRValueEncoding(this, record, value);
1052         }
1053         default:
1054                 ASSERT(false);
1055                 exit(-1);
1056         }
1057 }
1058
1059 Constraint * ConstGen::getMemValueEncoding(EPRecord *record, uint64_t value) {
1060         switch(record->getType()) {
1061         case STORE:
1062                 return getStoreLoadSet(record)->getValueEncoding(this, record, value);
1063         case RMW:
1064                 return getStoreLoadSet(record)->getValueEncoding(this, record, value);
1065         default:
1066                 ASSERT(false);
1067                 exit(-1);
1068         }
1069 }
1070
1071 /** Return true if the execution of record implies the execution of
1072  *      recordsubsumes */
1073
1074 bool ConstGen::subsumesExecutionConstraint(EPRecord *recordsubsumes, EPRecord *record) {
1075         EPValue *branch=record->getBranch();
1076         EPValue *branchsubsumes=recordsubsumes->getBranch();
1077         if (branchsubsumes != NULL) {
1078                 bool branchsubsumed=false;
1079                 while(branch!=NULL) {
1080                         if (branchsubsumes==branch) {
1081                                 branchsubsumed=true;
1082                                 break;
1083                         }
1084                         branch=branch->getRecord()->getBranch();
1085                 }
1086                 if (!branchsubsumed)
1087                         return false;
1088         }
1089         RecordSet *srs=execcondtable->get(recordsubsumes);
1090
1091         if (srs!=NULL) {
1092                 RecordIterator *sri=srs->iterator();
1093                 while(sri->hasNext()) {
1094                         EPRecord *rec=sri->next();
1095
1096                         if (!getOrderConstraint(rec, record)->isTrue()) {
1097                                 delete sri;
1098                                 return false;
1099                         }
1100                 }
1101                 delete sri;
1102         }
1103         return true;
1104 }
1105
1106 Constraint * ConstGen::getExecutionConstraint(EPRecord *record) {
1107         EPValue *branch=record->getBranch();
1108         RecordSet *srs=execcondtable->get(record);
1109         int size=srs==NULL ? 0 : srs->getSize();
1110         if (branch!=NULL)
1111                 size++;
1112
1113         Constraint *array[size];
1114         int index=0;
1115         if (srs!=NULL) {
1116                 RecordIterator *sri=srs->iterator();
1117                 while(sri->hasNext()) {
1118                         EPRecord *rec=sri->next();
1119                         EPValue *recbranch=rec->getBranch();
1120                         BranchRecord *guardbr=branchtable->get(recbranch->getRecord());
1121                         array[index++]=guardbr->getBranch(recbranch)->negate();
1122                 }
1123                 delete sri;
1124         }
1125         if (branch!=NULL) {
1126                 BranchRecord *guardbr=branchtable->get(branch->getRecord());
1127                 array[index++]=guardbr->getBranch(branch);
1128         }
1129         if (index==0)
1130                 return &ctrue;
1131         else if (index==1)
1132                 return array[0];
1133         else
1134                 return new Constraint(AND, index, array);
1135 }
1136
1137 bool ConstGen::isAlwaysExecuted(EPRecord *record) {
1138         EPValue *branch=record->getBranch();
1139         RecordSet *srs=execcondtable->get(record);
1140         int size=srs==NULL ? 0 : srs->getSize();
1141         if (branch!=NULL)
1142                 size++;
1143
1144         return size==0;
1145 }
1146
1147 void ConstGen::insertBranch(EPRecord *record) {
1148         uint numvalue=record->numValues();
1149         /** need one value for new directions */
1150         if (numvalue<record->getLen()) {
1151                 numvalue++;
1152                 if (model->params.noexecyields) {
1153                         incompleteexploredbranch->add(record);
1154                 }
1155         }
1156         /** need extra value to represent that branch wasn't executed. **/
1157         bool alwaysexecuted=isAlwaysExecuted(record);
1158         if (!alwaysexecuted)
1159                 numvalue++;
1160         uint numbits=NUMBITS(numvalue-1);
1161         Constraint *bits[numbits];
1162         getArrayNewVars(numbits, bits);
1163         BranchRecord *br=new BranchRecord(record, numbits, bits, alwaysexecuted);
1164         branchtable->put(record, br);
1165 }
1166
1167 void ConstGen::processBranch(EPRecord *record) {
1168         BranchRecord *br=branchtable->get(record);
1169         if (record->numValues()<record->getLen()) {
1170                 Constraint *goal=br->getNewBranch();
1171                 ADDBRANCHGOAL(record, goal,"newbranch");
1172         }
1173
1174         /** Insert criteria of parent branch going the right way. **/
1175         Constraint *baseconstraint=getExecutionConstraint(record);
1176
1177         if (!isAlwaysExecuted(record)) {
1178                 Constraint *parentbranch=new Constraint(IMPLIES, br->getAnyBranch(), baseconstraint);
1179                 ADDCONSTRAINT(parentbranch, "parentbranch");
1180         }
1181
1182         /** Insert criteria for directions */
1183         ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1184         ASSERT(depvec->size()==1);
1185         EPRecord * val_record=(*depvec)[0];
1186         for(unsigned int i=0;i<record->numValues();i++) {
1187                 EPValue * branchval=record->getValue(i);
1188                 uint64_t val=branchval->getValue();
1189
1190                 if (val==0) {
1191                         Constraint *execconstraint=getExecutionConstraint(record);
1192                         Constraint *br_false=new Constraint(IMPLIES,
1193                                                                                                                                                                         new Constraint(AND, execconstraint,
1194                                                                                                                                                                                                                                  getRetValueEncoding(val_record, val)), br->getBranch(branchval));
1195                         ADDCONSTRAINT(br_false, "br_false");
1196                 } else {
1197                         if (record->getBranchAnyValue()) {
1198                                 if (getRetValueEncoding(val_record, 0)!=NULL) {
1199                                         Constraint *execconstraint=getExecutionConstraint(record);
1200                                         Constraint *br_true1=new Constraint(IMPLIES, new Constraint(AND, getRetValueEncoding(val_record, 0)->negate(),
1201                                                                                                                                                                                                                                                                                         execconstraint),
1202                                                                                                                                                                                         br->getBranch(branchval));
1203                                         ADDCONSTRAINT(br_true1, "br_true1");
1204                                 } else {
1205                                         for(unsigned int j=0;j<val_record->numValues();j++) {
1206                                                 EPValue * epval=val_record->getValue(j);
1207                                                 Constraint *execconstraint=getExecutionConstraint(record);
1208                                                 Constraint *valuematches=getRetValueEncoding(val_record, epval->getValue());
1209                                                 Constraint *br_true2=new Constraint(IMPLIES, new Constraint(AND, execconstraint, valuematches), br->getBranch(branchval));
1210                                                 ADDCONSTRAINT(br_true2, "br_true2");
1211                                         }
1212                                 }
1213                         } else {
1214                                 Constraint *execconstraint=getExecutionConstraint(record);
1215                                 Constraint *br_val=new Constraint(IMPLIES, new Constraint(AND, execconstraint, getRetValueEncoding(val_record, val)), br->getBranch(branchval));
1216                                 ADDCONSTRAINT(br_val, "br_val");
1217                         }
1218                 }
1219         }
1220 }
1221
1222 void ConstGen::insertFunction(EPRecord *record) {
1223         FunctionRecord * fr=new FunctionRecord(this, record);
1224         functiontable->put(record, fr);
1225 }
1226
1227 void ConstGen::insertEquals(EPRecord *record) {
1228         EqualsRecord * fr=new EqualsRecord(this, record);
1229         equalstable->put(record, fr);
1230 }
1231
1232 void ConstGen::processLoad(EPRecord *record) {
1233         LoadRF * lrf=new LoadRF(record, this);
1234         lrf->genConstraints(this);
1235         delete lrf;
1236         processAddresses(record);
1237 }
1238
1239 /** This procedure generates the constraints that set the address
1240                 variables for load/store/rmw operations. */
1241
1242 void ConstGen::processAddresses(EPRecord *record) {
1243         StoreLoadSet *sls=getStoreLoadSet(record);
1244         ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_ADDRINDEX);
1245         if (depvec==NULL) {
1246                 //we have a hard coded address
1247                 const void *addr=record->getValue(0)->getAddr();
1248                 Constraint *addrenc=sls->getAddressEncoding(this, record, addr);
1249                 ADDCONSTRAINT(addrenc,"fixedaddress");
1250         } else {
1251                 //we take as input an address and have to generate implications
1252                 //for each possible input address
1253                 ASSERT(depvec->size()==1);
1254                 EPRecord *src=(*depvec)[0];
1255                 IntIterator *it=record->getSet(VC_ADDRINDEX)->iterator();
1256
1257                 uintptr_t offset=record->getOffset();
1258
1259                 while(it->hasNext()) {
1260                         uint64_t addr=it->next();
1261                         Constraint *srcenc=getRetValueEncoding(src, addr-offset);
1262                         Constraint *addrenc=sls->getAddressEncoding(this, record, (void *) addr);
1263                         Constraint *addrmatch=new Constraint(IMPLIES, srcenc, addrenc);
1264                         ADDCONSTRAINT(addrmatch,"setaddress");
1265                 }
1266                 delete it;
1267         }
1268 }
1269
1270 void ConstGen::processCAS(EPRecord *record) {
1271         //First do the load
1272         LoadRF * lrf=new LoadRF(record, this);
1273         lrf->genConstraints(this);
1274         delete lrf;
1275         //Next see if we are successful
1276         Constraint *eq=getNewVar();
1277         ModelVector<EPRecord *> * depveccas=execution->getRevDependences(record, VC_OLDVALCASINDEX);
1278         if (depveccas==NULL) {
1279                 //Hard coded old value
1280                 IntIterator *iit=record->getSet(VC_OLDVALCASINDEX)->iterator();
1281                 uint64_t valcas=iit->next();
1282                 delete iit;
1283                 Constraint *rmwr=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, valcas);
1284                 if (rmwr==NULL) {
1285                         Constraint *cascond=eq->negate();
1286                         ADDCONSTRAINT(cascond, "cascond");
1287                 } else {
1288                         Constraint *cascond=generateEquivConstraint(eq, rmwr);
1289                         ADDCONSTRAINT(cascond, "cascond");
1290                 }
1291         } else {
1292                 ASSERT(depveccas->size()==1);
1293                 EPRecord *src=(*depveccas)[0];
1294                 IntIterator *it=getStoreLoadSet(record)->getValues()->iterator();
1295
1296                 while(it->hasNext()) {
1297                         uint64_t valcas=it->next();
1298                         Constraint *srcenc=getRetValueEncoding(src, valcas);
1299                         Constraint *storeenc=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, valcas);
1300
1301                         if (srcenc!=NULL && storeenc!=NULL) {
1302                                 Constraint *cond=new Constraint(AND,
1303                                                                                                                                                                 new Constraint(IMPLIES, srcenc->clone(), eq),
1304                                                                                                                                                                 new Constraint(IMPLIES, eq, srcenc));
1305                                 Constraint *cas=new Constraint(IMPLIES, storeenc, cond);
1306                                 ADDCONSTRAINT(cas, "cas");
1307                         } else if (srcenc==NULL) {
1308                                 Constraint *casfail=new Constraint(IMPLIES, storeenc, eq->negate());
1309                                 ADDCONSTRAINT(casfail,"casfail_eq");
1310                         } else {
1311                                 //srcenc must be non-null and store-encoding must be null
1312                                 srcenc->free();
1313                         }
1314                 }
1315                 delete it;
1316                 IntIterator *iit=record->getSet(VC_OLDVALCASINDEX)->iterator();
1317                 while(iit->hasNext()) {
1318                         uint64_t val=iit->next();
1319                         if (!getStoreLoadSet(record)->getValues()->contains(val)) {
1320                                 Constraint *srcenc=getRetValueEncoding(src, val);
1321                                 Constraint *casfail=new Constraint(IMPLIES, srcenc, eq->negate());
1322                                 ADDCONSTRAINT(casfail,"casfailretval");
1323                         }
1324                 }
1325                 delete iit;
1326         }
1327
1328         ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1329         if (depvec==NULL) {
1330                 IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
1331                 uint64_t val=iit->next();
1332                 delete iit;
1333                 Constraint *storeenc=getMemValueEncoding(record, val);
1334                 Constraint *casmemsuc=new Constraint(IMPLIES, eq, storeenc);
1335                 ADDCONSTRAINT(casmemsuc, "casmemsuc");
1336         } else {
1337                 ASSERT(depvec->size()==1);
1338                 EPRecord *src=(*depvec)[0];
1339                 IntIterator *it=record->getStoreSet()->iterator();
1340
1341                 while(it->hasNext()) {
1342                         uint64_t val=it->next();
1343                         Constraint *srcenc=getRetValueEncoding(src, val);
1344                         if (srcenc==NULL) {
1345                                 //this can happen for values that are in the store set because
1346                                 //we re-stored them on a failed CAS
1347                                 continue;
1348                         }
1349                         Constraint *storeenc=getMemValueEncoding(record, val);
1350                         Constraint *storevalue=new Constraint(IMPLIES, new Constraint(AND, eq, srcenc), storeenc);
1351                         ADDCONSTRAINT(storevalue,"casmemsuc");
1352                 }
1353                 delete it;
1354         }
1355         StoreLoadSet *sls=getStoreLoadSet(record);
1356
1357         Constraint *repeatval=generateEquivConstraint(sls->getNumValVars(), sls->getValVars(this, record), sls->getRMWRValVars(this, record));
1358         Constraint *failcas=new Constraint(IMPLIES, eq->negate(), repeatval);
1359         ADDCONSTRAINT(failcas,"casmemfail");
1360
1361         processAddresses(record);
1362 }
1363
1364 void ConstGen::processEXC(EPRecord *record) {
1365         //First do the load
1366         LoadRF * lrf=new LoadRF(record, this);
1367         lrf->genConstraints(this);
1368         delete lrf;
1369
1370         ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1371         if (depvec==NULL) {
1372                 IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
1373                 uint64_t val=iit->next();
1374                 delete iit;
1375                 Constraint *storeenc=getMemValueEncoding(record, val);
1376                 ADDCONSTRAINT(storeenc, "excmemsuc");
1377         } else {
1378                 ASSERT(depvec->size()==1);
1379                 EPRecord *src=(*depvec)[0];
1380                 IntIterator *it=record->getStoreSet()->iterator();
1381
1382                 while(it->hasNext()) {
1383                         uint64_t val=it->next();
1384                         Constraint *srcenc=getRetValueEncoding(src, val);
1385                         Constraint *storeenc=getMemValueEncoding(record, val);
1386                         Constraint *storevalue=new Constraint(IMPLIES, srcenc, storeenc);
1387                         ADDCONSTRAINT(storevalue,"excmemsuc");
1388                 }
1389                 delete it;
1390         }
1391
1392         processAddresses(record);
1393 }
1394
1395 void ConstGen::processAdd(EPRecord *record) {
1396         //First do the load
1397         LoadRF * lrf=new LoadRF(record, this);
1398         lrf->genConstraints(this);
1399         delete lrf;
1400         Constraint *var=getNewVar();
1401         Constraint *newadd=new Constraint(AND, var, getExecutionConstraint(record));
1402         ADDGOAL(record, newadd, "newadd");
1403
1404         ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1405         if (depvec==NULL) {
1406                 IntIterator *valit=record->getSet(VC_BASEINDEX)->iterator();
1407                 uint64_t val=valit->next();
1408                 delete valit;
1409                 IntHashSet *valset=getStoreLoadSet(record)->getValues();
1410                 IntIterator *sis=valset->iterator();
1411                 while(sis->hasNext()) {
1412                         uint64_t memval=sis->next();
1413                         uint64_t sumval=(memval+val)&getmask(record->getLen());
1414
1415                         if (valset->contains(sumval)) {
1416
1417                                 Constraint *loadenc=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, memval);
1418                                 Constraint *storeenc=getMemValueEncoding(record, sumval);
1419                                 Constraint *notvar=var->negate();
1420                                 Constraint *addinputfix=new Constraint(IMPLIES, loadenc, new Constraint(AND, storeenc, notvar));
1421                                 ADDCONSTRAINT(addinputfix, "addinputfix");
1422                         }
1423                 }
1424
1425                 delete sis;
1426         } else {
1427                 ASSERT(depvec->size()==1);
1428                 EPRecord *src=(*depvec)[0];
1429                 IntIterator *it=record->getStoreSet()->iterator();
1430                 IntHashSet *valset=getStoreLoadSet(record)->getValues();
1431
1432                 while(it->hasNext()) {
1433                         uint64_t val=it->next();
1434                         IntIterator *sis=valset->iterator();
1435                         while(sis->hasNext()) {
1436                                 uint64_t memval=sis->next();
1437                                 uint64_t sum=(memval+val)&getmask(record->getLen());
1438                                 if (valset->contains(sum)) {
1439                                         Constraint *srcenc=getRetValueEncoding(src, val);
1440                                         Constraint *loadenc=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, memval);
1441                                         Constraint *storeenc=getMemValueEncoding(record, sum);
1442                                         Constraint *notvar=var->negate();
1443                                         Constraint *addop=new Constraint(IMPLIES, new Constraint(AND, srcenc, loadenc),
1444                                                                                                                                                                          new Constraint(AND, notvar, storeenc));
1445                                         ADDCONSTRAINT(addop,"addinputvar");
1446                                 }
1447                         }
1448                         delete sis;
1449                 }
1450                 delete it;
1451         }
1452
1453         processAddresses(record);
1454 }
1455
1456 /** This function ensures that the value of a store's SAT variables
1457                 matches the store's input value.
1458
1459                 TODO: Could optimize the case where the encodings are the same...
1460  */
1461
1462 void ConstGen::processStore(EPRecord *record) {
1463         ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1464         if (depvec==NULL) {
1465                 //We have a hard coded value
1466                 uint64_t val=record->getValue(0)->getValue();
1467                 Constraint *storeenc=getMemValueEncoding(record, val);
1468                 ADDCONSTRAINT(storeenc,"storefix");
1469         } else {
1470                 //We have a value from an input
1471                 ASSERT(depvec->size()==1);
1472                 EPRecord *src=(*depvec)[0];
1473                 IntIterator *it=record->getStoreSet()->iterator();
1474
1475                 while(it->hasNext()) {
1476                         uint64_t val=it->next();
1477                         Constraint *srcenc=getRetValueEncoding(src, val);
1478                         Constraint *storeenc=getMemValueEncoding(record, val);
1479                         Constraint *storevalue=new Constraint(IMPLIES, srcenc, storeenc);
1480                         ADDCONSTRAINT(storevalue,"storevar");
1481                 }
1482                 delete it;
1483         }
1484         processAddresses(record);
1485 }
1486
1487 /** **/
1488
1489 void ConstGen::computeYieldCond(EPRecord *record) {
1490         ExecPoint *yieldep=record->getEP();
1491         EPRecord *prevyield=NULL;
1492         ExecPoint *prevyieldep=NULL;
1493
1494         for(int i=(int)(yieldlist->size()-1);i>=0;i--) {
1495                 EPRecord *tmpyield=(*yieldlist)[i];
1496                 ExecPoint *tmpep=tmpyield->getEP();
1497                 //Do we have a previous yield operation
1498                 if (yieldep->compare(tmpep)==CR_BEFORE) {
1499                         //Yes
1500                         prevyield=tmpyield;
1501                         prevyieldep=prevyield->getEP();
1502                         break;
1503                 }
1504         }
1505
1506         yieldlist->push_back(record);
1507
1508         ModelVector<Constraint *> * novel_branches=new ModelVector<Constraint *>();
1509         RecordIterator *sri=incompleteexploredbranch->iterator();
1510         while(sri->hasNext()) {
1511                 EPRecord * unexploredbranch=sri->next();
1512                 ExecPoint * branchep=unexploredbranch->getEP();
1513                 if (yieldep->compare(branchep)!=CR_BEFORE) {
1514                         //Branch does not occur before yield, so skip
1515                         continue;
1516                 }
1517
1518                 //See if the previous yield already accounts for this branch
1519                 if (prevyield != NULL &&
1520                                 prevyieldep->compare(branchep)==CR_BEFORE) {
1521                         //Branch occurs before previous yield, so we can safely skip this branch
1522                                                 continue;
1523                 }
1524
1525                 //This is a branch that could prevent this yield from being executed
1526                 BranchRecord *br=branchtable->get(unexploredbranch);
1527                 Constraint * novel_branch=br->getNewBranch();
1528                 novel_branches->push_back(novel_branch);
1529         }
1530
1531         int num_constraints=((prevyield==NULL)?0:1)+novel_branches->size();
1532         Constraint *carray[num_constraints];
1533         int arr_index=0;
1534
1535         if (prevyield!=NULL) {
1536                 carray[arr_index++]=yieldtable->get(prevyield);//get constraint for old yield
1537         }
1538         for(uint i=0;i<novel_branches->size();i++) {
1539                 carray[arr_index++]=(*novel_branches)[i];
1540         }
1541
1542         Constraint *cor=num_constraints!=0?new Constraint(OR, num_constraints, carray):&cfalse;
1543
1544         Constraint *var=getNewVar();
1545         //If the variable is true, then we need to have taken some branch
1546         //ahead of the yield
1547         Constraint *implies=new Constraint(IMPLIES, var, cor);
1548         ADDCONSTRAINT(implies, "possiblebranchnoyield");
1549         yieldtable->put(record, var);
1550
1551         delete novel_branches;
1552         delete sri;
1553 }
1554
1555
1556 /** Handle yields by just forbidding them via the SAT formula. */
1557
1558 void ConstGen::processYield(EPRecord *record) {
1559         if (model->params.noexecyields) {
1560                 computeYieldCond(record);
1561                 Constraint * noexecyield=getExecutionConstraint(record)->negate();
1562                 Constraint * branchaway=yieldtable->get(record);
1563                 Constraint * avoidbranch=new Constraint(OR, noexecyield, branchaway);
1564                 ADDCONSTRAINT(avoidbranch, "noexecyield");
1565         }
1566 }
1567
1568 void ConstGen::processLoopPhi(EPRecord *record) {
1569         EPRecordIDSet *phiset=record->getPhiLoopTable();
1570         EPRecordIDIterator *rit=phiset->iterator();
1571
1572         while(rit->hasNext()) {
1573                 struct RecordIDPair *rip=rit->next();
1574                 EPRecord *input=rip->idrecord;
1575
1576                 IntIterator * it=record->getSet(VC_BASEINDEX)->iterator();
1577                 while(it->hasNext()) {
1578                         uint64_t value=it->next();
1579                         Constraint * inputencoding=getRetValueEncoding(input, value);
1580                         if (inputencoding==NULL)
1581                                 continue;
1582                         Constraint * branchconstraint=getExecutionConstraint(rip->record);
1583                         Constraint * outputencoding=getRetValueEncoding(record, value);
1584                         Constraint * phiimplication=new Constraint(IMPLIES, new Constraint(AND, inputencoding, branchconstraint), outputencoding);
1585                         ADDCONSTRAINT(phiimplication,"philoop");
1586                 }
1587                 delete it;
1588         }
1589         delete rit;
1590 }
1591
1592 void ConstGen::processPhi(EPRecord *record) {
1593         ModelVector<EPRecord *> * inputs=execution->getRevDependences(record, VC_BASEINDEX);
1594         for(uint i=0;i<inputs->size();i++) {
1595                 EPRecord * input=(*inputs)[i];
1596
1597                 IntIterator * it=record->getSet(VC_BASEINDEX)->iterator();
1598                 while(it->hasNext()) {
1599                         uint64_t value=it->next();
1600                         Constraint * inputencoding=getRetValueEncoding(input, value);
1601                         if (inputencoding==NULL)
1602                                 continue;
1603                         Constraint * branchconstraint=getExecutionConstraint(input);
1604                         Constraint * outputencoding=getRetValueEncoding(record, value);
1605                         Constraint * phiimplication=new Constraint(IMPLIES, new Constraint(AND, inputencoding, branchconstraint), outputencoding);
1606                         ADDCONSTRAINT(phiimplication,"phi");
1607                 }
1608                 delete it;
1609         }
1610 }
1611
1612 void ConstGen::processFunction(EPRecord *record) {
1613         if (record->getLoopPhi()) {
1614                 processLoopPhi(record);
1615                 return;
1616         } else if (record->getPhi()) {
1617                 processPhi(record);
1618                 return;
1619         }
1620
1621         CGoalSet *knownbehaviors=record->completedGoalSet();
1622         CGoalIterator *cit=knownbehaviors->iterator();
1623         uint numinputs=record->getNumFuncInputs();
1624         EPRecord * inputs[numinputs];
1625         for(uint i=0;i<numinputs;i++) {
1626                 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, i+VC_BASEINDEX);
1627                 ASSERT(depvec->size()==1);
1628                 inputs[i]=(*depvec)[0];
1629         }
1630         while(cit->hasNext()) {
1631                 CGoal *goal=cit->next();
1632                 Constraint *carray[numinputs];
1633                 if (record->isSharedGoals()) {
1634                         bool badvalue=false;
1635                         for(uint i=0;i<numinputs;i++) {
1636                                 uint64_t inputval=goal->getValue(i+VC_BASEINDEX);
1637                                 if (!record->getSet(i+VC_BASEINDEX)->contains(inputval)) {
1638                                         badvalue=true;
1639                                         break;
1640                                 }
1641                         }
1642                         if (badvalue)
1643                                 continue;
1644                 }
1645
1646                 /* Build up constraints for each input */
1647                 for(uint i=0;i<numinputs;i++) {
1648                         uint64_t inputval=goal->getValue(i+VC_BASEINDEX);
1649                         Constraint * inputc=getRetValueEncoding(inputs[i], inputval);
1650                         ASSERT(inputc!=NULL);
1651                         carray[i]=inputc;
1652                 }
1653                 Constraint * outputconstraint=getRetValueEncoding(record, goal->getOutput());
1654                 if (numinputs==0) {
1655                         ADDCONSTRAINT(outputconstraint,"functionimpl");
1656                 } else {
1657                         Constraint * functionimplication=new Constraint(IMPLIES, new Constraint(AND, numinputs, carray), outputconstraint);
1658                         ADDCONSTRAINT(functionimplication,"functionimpl");
1659                 }
1660         }
1661         delete cit;
1662
1663         FunctionRecord *fr=functiontable->get(record);
1664         Constraint *goal=fr->getNoValueEncoding();
1665         Constraint *newfunc=new Constraint(AND, goal, getExecutionConstraint(record));
1666         ADDGOAL(record, newfunc, "newfunc");
1667 }
1668
1669 void ConstGen::processEquals(EPRecord *record) {
1670         ASSERT (record->getNumFuncInputs() == 2);
1671         EPRecord * inputs[2];
1672
1673         for(uint i=0;i<2;i++) {
1674                 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, i+VC_BASEINDEX);
1675                 if (depvec==NULL) {
1676                         inputs[i]=NULL;
1677                 } else if (depvec->size()==1) {
1678                         inputs[i]=(*depvec)[0];
1679                 }       else ASSERT(false);
1680         }
1681
1682         //rely on this being a variable
1683         Constraint * outputtrue=getRetValueEncoding(record, 1);
1684         ASSERT(outputtrue->getType()==VAR);
1685
1686         if (inputs[0]!=NULL && inputs[1]!=NULL &&
1687                         (inputs[0]->getType()==LOAD || inputs[0]->getType()==RMW) &&
1688                         (inputs[1]->getType()==LOAD || inputs[1]->getType()==RMW) &&
1689                         (getStoreLoadSet(inputs[0])==getStoreLoadSet(inputs[1]))) {
1690                 StoreLoadSet * sls=getStoreLoadSet(inputs[0]);
1691                 int numvalvars=sls->getNumValVars();
1692                 Constraint **valvar1=(inputs[0]->getType()==RMW) ? sls->getRMWRValVars(this, inputs[0]) : sls->getValVars(this, inputs[0]);
1693                 Constraint **valvar2=(inputs[1]->getType()==RMW) ? sls->getRMWRValVars(this, inputs[1]) : sls->getValVars(this, inputs[1]);
1694                 //new test
1695
1696                 Constraint *vars[numvalvars];
1697                 for(int i=0;i<numvalvars;i++) {
1698                         vars[i]=getNewVar();
1699                         Constraint *var1=valvar1[i];
1700                         Constraint *var2=valvar2[i];
1701                         Constraint * array[]={var1, var2->negate(), vars[i]->negate()};
1702                         Constraint * array2[]={var2, var1->negate(), vars[i]->negate()};
1703                         Constraint * a=new Constraint(OR, 3, array);
1704                         ADDCONSTRAINT(a, "equala");
1705                         Constraint * a2=new Constraint(OR, 3, array2);
1706                         ADDCONSTRAINT(a2, "equala2");
1707                         Constraint * arrayb[]={var1, var2, vars[i]};
1708                         Constraint * array2b[]={var2->negate(), var1->negate(), vars[i]};
1709                         Constraint * b=new Constraint(OR, 3, arrayb);
1710                         ADDCONSTRAINT(b, "equalb");
1711                         Constraint *b2=new Constraint(OR, 3, array2b);
1712                         ADDCONSTRAINT(b2, "equalb2");
1713                 }
1714                 ADDCONSTRAINT(new Constraint(IMPLIES, new Constraint(AND, numvalvars, vars), outputtrue),"impequal1");
1715
1716                 ADDCONSTRAINT(new Constraint(IMPLIES, outputtrue, new Constraint(AND, numvalvars, vars)), "impequal2");
1717
1718                 /*
1719
1720                    Constraint * functionimplication=new Constraint(IMPLIES,generateEquivConstraint(numvalvars, valvar1, valvar2), outputtrue);
1721                    ADDCONSTRAINT(functionimplication,"equalsimplspecial");
1722                    Constraint * functionimplicationneg=new Constraint(IMPLIES,outputtrue, generateEquivConstraint(numvalvars, valvar1, valvar2));
1723                    ADDCONSTRAINT(functionimplicationneg,"equalsimplspecialneg");
1724                  */
1725                 return;
1726         }
1727
1728         if (inputs[0]==NULL && inputs[1]==NULL) {
1729                 IntIterator *iit0=record->getSet(VC_BASEINDEX+0)->iterator();
1730                 uint64_t constval=iit0->next();
1731                 delete iit0;
1732                 IntIterator *iit1=record->getSet(VC_BASEINDEX+1)->iterator();
1733                 uint64_t constval2=iit1->next();
1734                 delete iit1;
1735
1736                 if (constval==constval2) {
1737                         ADDCONSTRAINT(outputtrue, "equalsconst");
1738                 } else {
1739                         ADDCONSTRAINT(outputtrue->negate(), "equalsconst");
1740                 }
1741                 return;
1742         }
1743
1744         if (inputs[0]==NULL ||
1745                         inputs[1]==NULL) {
1746                 int nullindex=inputs[0]==NULL ? 0 : 1;
1747                 IntIterator *iit=record->getSet(VC_BASEINDEX+nullindex)->iterator();
1748                 uint64_t constval=iit->next();
1749                 delete iit;
1750
1751                 record->getSet(VC_BASEINDEX+nullindex);
1752                 EPRecord *r=inputs[1-nullindex];
1753                 Constraint *l=getRetValueEncoding(r, constval);
1754                 Constraint *functionimplication=new Constraint(IMPLIES, l, outputtrue);
1755                 ADDCONSTRAINT(functionimplication,"equalsimpl");
1756
1757                 Constraint *l2=getRetValueEncoding(r, constval);
1758                 Constraint *functionimplication2=new Constraint(IMPLIES, outputtrue, l2);
1759                 ADDCONSTRAINT(functionimplication2,"equalsimpl");
1760         }
1761
1762         IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
1763         while(iit->hasNext()) {
1764                 uint64_t val1=iit->next();
1765
1766                 IntIterator *iit2=record->getSet(VC_BASEINDEX+1)->iterator();
1767                 while(iit2->hasNext()) {
1768                         uint64_t val2=iit2->next();
1769                         Constraint *l=getRetValueEncoding(inputs[0], val1);
1770                         Constraint *r=getRetValueEncoding(inputs[1], val2);
1771                         Constraint *imp=(val1==val2) ? outputtrue : outputtrue->negate();
1772                         Constraint * functionimplication=new Constraint(IMPLIES, new Constraint(AND, l, r), imp);
1773                         ADDCONSTRAINT(functionimplication,"equalsimpl");
1774                 }
1775                 delete iit2;
1776         }
1777         delete iit;
1778 }
1779
1780 #ifdef TSO
1781 void ConstGen::processFence(EPRecord *record) {
1782         //do we already account for the fence?
1783         if (isAlwaysExecuted(record))
1784                 return;
1785         ExecPoint * record_ep=record->getEP();
1786         thread_id_t tid=record_ep->get_tid();
1787         uint thread=id_to_int(tid);
1788         ModelVector<EPRecord *> *tvec=(*threadactions)[thread];
1789         uint size=tvec->size();
1790
1791         EPRecord *prevstore=NULL;
1792         uint i;
1793         for(i=0;i<size;i++) {
1794                 EPRecord *rec=(*tvec)[i];
1795                 if (rec->getType()==STORE) {
1796                         prevstore=rec;
1797                 }
1798                 if (rec == record) {
1799                         i++;
1800                         break;
1801                 }
1802         }
1803         if (prevstore == NULL) {
1804                 return;
1805         }
1806         for(;i<size;i++) {
1807                 EPRecord *rec=(*tvec)[i];
1808                 if (rec->getType()==LOAD) {
1809                         Constraint * condition=getExecutionConstraint(record);
1810                         Constraint * storeload=getOrderConstraint(prevstore, rec);
1811                         Constraint * c=new Constraint(IMPLIES, condition, storeload);
1812                         ADDCONSTRAINT(c, "fence");
1813                         return;
1814                 }
1815         }
1816 }
1817 #endif
1818
1819 /** processRecord performs actions on second traversal of event
1820                 graph. */
1821
1822 void ConstGen::processRecord(EPRecord *record) {
1823         switch (record->getType()) {
1824         case FUNCTION:
1825                 processFunction(record);
1826                 break;
1827         case EQUALS:
1828                 processEquals(record);
1829                 break;
1830         case LOAD:
1831                 processLoad(record);
1832                 break;
1833         case STORE:
1834                 processStore(record);
1835                 break;
1836 #ifdef TSO
1837         case FENCE:
1838                 processFence(record);
1839                 break;
1840 #endif
1841         case RMW:
1842 #ifdef TSO
1843                 processFence(record);
1844 #endif
1845                 if (record->getOp()==ADD) {
1846                         processAdd(record);
1847                 } else if (record->getOp()==CAS) {
1848                         processCAS(record);
1849                 } else if (record->getOp()==EXC) {
1850                         processEXC(record);
1851                 } else
1852                         ASSERT(0);
1853                 break;
1854         case YIELD:
1855                 processYield(record);
1856                 break;
1857         case BRANCHDIR:
1858                 processBranch(record);
1859                 break;
1860         default:
1861                 break;
1862         }
1863 }
1864
1865 /** visitRecord performs actions done on first traversal of event
1866  *      graph. */
1867
1868 void ConstGen::visitRecord(EPRecord *record) {
1869         switch (record->getType()) {
1870         case EQUALS:
1871                 recordExecCond(record);
1872                 insertEquals(record);
1873                 break;
1874         case FUNCTION:
1875                 recordExecCond(record);
1876                 insertFunction(record);
1877                 break;
1878 #ifdef TSO
1879         case FENCE:
1880                 recordExecCond(record);
1881                 insertAction(record);
1882                 break;
1883 #endif
1884         case LOAD:
1885                 recordExecCond(record);
1886                 insertAction(record);
1887                 groupMemoryOperations(record);
1888                 break;
1889         case STORE:
1890                 recordExecCond(record);
1891                 insertAction(record);
1892                 groupMemoryOperations(record);
1893                 break;
1894         case RMW:
1895                 recordExecCond(record);
1896                 insertAction(record);
1897                 groupMemoryOperations(record);
1898                 break;
1899         case BRANCHDIR:
1900                 recordExecCond(record);
1901                 insertBranch(record);
1902                 break;
1903         case LOOPEXIT:
1904                 recordExecCond(record);
1905                 break;
1906         case NONLOCALTRANS:
1907                 recordExecCond(record);
1908                 insertNonLocal(record);
1909                 break;
1910         case LABEL:
1911                 insertLabel(record);
1912                 break;
1913         case YIELD:
1914                 recordExecCond(record);
1915                 break;
1916         default:
1917                 break;
1918         }
1919 }
1920
1921 void ConstGen::recordExecCond(EPRecord *record) {
1922         ExecPoint *eprecord=record->getEP();
1923         EPValue * branchval=record->getBranch();
1924         EPRecord * branch=(branchval==NULL) ? NULL : branchval->getRecord();
1925         ExecPoint *epbranch= (branch==NULL) ? NULL : branch->getEP();
1926         RecordSet *srs=NULL;
1927         RecordIterator *sri=nonlocaltrans->iterator();
1928         while(sri->hasNext()) {
1929                 EPRecord *nonlocal=sri->next();
1930                 ExecPoint *epnl=nonlocal->getEP();
1931                 if (epbranch!=NULL) {
1932                         if (epbranch->compare(epnl)==CR_BEFORE) {
1933                                 //branch occurs after non local and thus will subsume condition
1934                                 //branch subsumes this condition
1935                                 continue;
1936                         }
1937                 }
1938                 if (eprecord->compare(epnl)==CR_BEFORE) {
1939                         //record occurs after non-local, so add it to set
1940                         if (srs==NULL)
1941                                 srs=new RecordSet();
1942                         srs->add(nonlocal);
1943                 }
1944         }
1945         delete sri;
1946         if (srs!=NULL)
1947                 execcondtable->put(record, srs);
1948 }
1949
1950 void ConstGen::insertNonLocal(EPRecord *record) {
1951         nonlocaltrans->add(record);
1952 }
1953
1954 void ConstGen::insertLabel(EPRecord *record) {
1955         RecordIterator *sri=nonlocaltrans->iterator();
1956         while(sri->hasNext()) {
1957                 EPRecord *nonlocal=sri->next();
1958                 if (nonlocal->getNextRecord()==record)
1959                         sri->remove();
1960         }
1961
1962         delete sri;
1963 }
1964
1965 void ConstGen::traverseRecord(EPRecord *record, bool initial) {
1966         do {
1967                 if (initial) {
1968                         visitRecord(record);
1969                 } else {
1970                         processRecord(record);
1971                 }
1972                 if (record->getType()==LOOPENTER) {
1973                         workstack->push_back(record->getNextRecord());
1974                         workstack->push_back(record->getChildRecord());
1975                         return;
1976                 }
1977                 if (record->getChildRecord()!=NULL) {
1978                         workstack->push_back(record->getChildRecord());
1979                 }
1980                 if (record->getType()==NONLOCALTRANS) {
1981                         return;
1982                 }
1983                 if (record->getType()==YIELD && model->params.noexecyields) {
1984                         return;
1985                 }
1986                 if (record->getType()==LOOPEXIT) {
1987                         return;
1988                 }
1989                 if (record->getType()==BRANCHDIR) {
1990                         EPRecord *next=record->getNextRecord();
1991                         if (next != NULL)
1992                                 workstack->push_back(next);
1993                         for(uint i=0;i<record->numValues();i++) {
1994                                 EPValue *branchdir=record->getValue(i);
1995
1996                                 //Could have an empty branch, so make sure the branch actually
1997                                 //runs code
1998                                 if (branchdir->getFirstRecord()!=NULL)
1999                                         workstack->push_back(branchdir->getFirstRecord());
2000                         }
2001                         return;
2002                 } else
2003                         record=record->getNextRecord();
2004         } while(record!=NULL);
2005 }
2006
2007 unsigned int RecPairHash(RecPair *rp) {
2008         uintptr_t v=(uintptr_t) rp->epr1;
2009         uintptr_t v2=(uintptr_t) rp->epr2;
2010         uintptr_t x=v^v2;
2011         uintptr_t a=v&v2;
2012         return (uint)((x>>4)^(a));
2013 }
2014
2015 bool RecPairEquals(RecPair *r1, RecPair *r2) {
2016         return ((r1->epr1==r2->epr1)&&(r1->epr2==r2->epr2)) ||
2017                                  ((r1->epr1==r2->epr2)&&(r1->epr2==r2->epr1));
2018 }