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