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