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                                 Constraint * array[]={c21, c32, c13};
 750                                 Constraint *intratransorder=new Constraint(OR, 3, array);
 751 #else
 752                                 Constraint *intratransorder=new Constraint(OR, c21, c13);
 753 #endif
 754                                 ADDCONSTRAINT(intratransorder,"intratransorder");
 755                 }
 756
 757                         for(uint t0i=0;t0i<t1i;t0i++) {
 758                                 EPRecord *t0rec=(*t1vec)[t0i];
 759                                 Constraint *c02=getOrderConstraint(t0rec, t2rec);
 760 #ifdef TSO
 761                                 Constraint *c10=getOrderConstraint(t1rec, t0rec);
 762                                 Constraint * array[]={c10, c21, c02};
 763                                 Constraint *intratransorder=new Constraint(OR, 3, array);
 764 #else
 765                                 Constraint *intratransorder=new Constraint(OR, c21, c02);
 766 #endif
 767                                 ADDCONSTRAINT(intratransorder,"intratransorder");
 768                 }
 769                 }
 770         }
 771 }
 772
 773
 774 void ConstGen::genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVector<EPRecord *> *t2vec, ModelVector<EPRecord *> * t3vec) {
 775         for(uint t1i=0;t1i<t1vec->size();t1i++) {
 776                 EPRecord *t1rec=(*t1vec)[t1i];
 777                 for(uint t2i=0;t2i<t2vec->size();t2i++) {
 778                         EPRecord *t2rec=(*t2vec)[t2i];
 779                         for(uint t3i=0;t3i<t3vec->size();t3i++) {
 780                                 EPRecord *t3rec=(*t3vec)[t3i];
 781                                 genTransOrderConstraint(t1rec, t2rec, t3rec);
 782                         }
 783                 }
 784         }
 785 }
 786
 787 void ConstGen::genTransOrderConstraint(EPRecord *t1rec, EPRecord *t2rec, EPRecord *t3rec) {
 788         Constraint *c21=getOrderConstraint(t2rec, t1rec);
 789         Constraint *c32=getOrderConstraint(t3rec, t2rec);
 790         Constraint *c13=getOrderConstraint(t1rec, t3rec);
 791         Constraint * cimpl1[]={c21, c32, c13};
 792         Constraint * c1=new Constraint(OR, 3, cimpl1);
 793         ADDCONSTRAINT(c1, "intertransorder");
 794
 795         Constraint *c12=getOrderConstraint(t1rec, t2rec);
 796         Constraint *c23=getOrderConstraint(t2rec, t3rec);
 797         Constraint *c31=getOrderConstraint(t3rec, t1rec);
 798         Constraint * cimpl2[]={c12, c23, c31};
 799         Constraint *c2=new Constraint(OR, 3, cimpl2);
 800         ADDCONSTRAINT(c2, "intertransorder");
 801 }
 802
 803 void ConstGen::addGoal(EPRecord *r, Constraint *c) {
 804         rectoint->put(r, goalset->size());
 805         goalset->push_back(c);
 806 }
 807
 808 void ConstGen::addBranchGoal(EPRecord *r, Constraint *c) {
 809         has_untaken_branches=true;
 810         rectoint->put(r, goalset->size());
 811         goalset->push_back(c);
 812 }
 813
 814 void ConstGen::achievedGoal(EPRecord *r) {
 815         if (rectoint->contains(r)) {
 816                 uint index=rectoint->get(r);
 817                 //if (goalvararray[index] != NULL)
 818                 //model_print("Run Clearing goal index %d\n",index);
 819                 goalvararray[index]=NULL;
 820         }
 821 }
 822
 823 void ConstGen::addConstraint(Constraint *c) {
 824         ModelVector<Constraint *> *vec=c->simplify();
 825         for(uint i=0;i<vec->size();i++) {
 826                 Constraint *simp=(*vec)[i];
 827                 if (simp->type==TRUE)
 828                         continue;
 829                 ASSERT(simp->type!=FALSE);
 830                 simp->printDIMACS(this);
 831 #ifdef VERBOSE_CONSTRAINTS
 832                 simp->print();
 833                 model_print("\n");
 834 #endif
 835                 numconstraints++;
 836                 simp->freerec();
 837         }
 838         delete vec;
 839 }
 840
 841 void ConstGen::printNegConstraint(uint value) {
 842         int val=-value;
 843         solver->addClauseLiteral(val);
 844 }
 845
 846 void ConstGen::printConstraint(uint value) {
 847         solver->addClauseLiteral(value);
 848 }
 849
 850 bool * ConstGen::runSolver() {
 851         int solution=solver->solve();
 852         if (solution == IS_UNSAT) {
 853                 return NULL;
 854         } else if (solution == IS_SAT) {
 855                 bool * assignments=(bool *)model_malloc(sizeof(bool)*(varindex+1));
 856                 for(uint i=0;i<=varindex;i++)
 857                         assignments[i]=solver->getValue(i);
 858                 return assignments;
 859         } else {
 860                 delete solver;
 861                 solver=NULL;
 862                 dprintf(2, "INDETER\n");
 863                 model_print("INDETER\n");
 864                 exit(-1);
 865                 return NULL;
 866         }
 867 }
 868
 869 Constraint * ConstGen::getOrderConstraint(EPRecord *first, EPRecord *second) {
 870 #ifndef TSO
 871         if (first->getEP()->get_tid()==second->getEP()->get_tid()) {
 872                 if (first->getEP()->compare(second->getEP())==CR_AFTER)
 873                         return &ctrue;
 874                 else {
 875                         return &cfalse;
 876                 }
 877         }
 878 #endif
 879         RecPair rp(first, second);
 880         RecPair *rpc=rpt->get(&rp);
 881 #ifdef TSO
 882         if ((rpc==NULL) &&
 883                         first->getEP()->get_tid()==second->getEP()->get_tid()) {
 884                 if (first->getEP()->compare(second->getEP())==CR_AFTER)
 885                         return &ctrue;
 886                 else {
 887                         return &cfalse;
 888                 }
 889         }
 890 #endif
 891         ASSERT(rpc!=NULL);
 892         //      delete rp;
 893         Constraint *c=rpc->constraint;
 894         if (rpc->epr1!=first) {
 895                 //have to flip arguments
 896                 return c->negate();
 897         } else {
 898                 return c;
 899         }
 900 }
 901
 902 bool ConstGen::getOrder(EPRecord *first, EPRecord *second, bool * satsolution) {
 903         RecPair rp(first, second);
 904         RecPair *rpc=rpt->get(&rp);
 905 #ifdef TSO
 906         if ((rpc==NULL) &&
 907                         first->getEP()->get_tid()==second->getEP()->get_tid()) {
 908                 if (first->getEP()->compare(second->getEP())==CR_AFTER)
 909                         return true;
 910                 else {
 911                         return false;
 912                 }
 913         }
 914 #endif
 915
 916         ASSERT(rpc!=NULL);
 917
 918         Constraint *c=rpc->constraint;
 919         CType type=c->getType();
 920         bool order;
 921
 922         if (type==TRUE)
 923                 order=true;
 924         else if (type==FALSE)
 925                 order=false;
 926         else {
 927                 uint index=c->getVar();
 928                 order=satsolution[index];
 929         }
 930         if (rpc->epr1==first)
 931                 return order;
 932         else
 933                 return !order;
 934 }
 935
 936 /** This function determines whether events first and second are
 937  * ordered by start and join operations.  */
 938
 939 bool ConstGen::orderThread(EPRecord *first, EPRecord *second) {
 940         ExecPoint * ep1=first->getEP();
 941         ExecPoint * ep2=second->getEP();
 942         thread_id_t thr1=ep1->get_tid();
 943         thread_id_t thr2=ep2->get_tid();
 944         Thread *tr2=execution->get_thread(thr2);
 945         EPRecord *thr2start=tr2->getParentRecord();
 946         if (thr2start!=NULL) {
 947                 ExecPoint *epthr2start=thr2start->getEP();
 948                 if (epthr2start->get_tid()==thr1 &&
 949                                 ep1->compare(epthr2start)==CR_AFTER)
 950                         return true;
 951         }
 952         ModelVector<EPRecord *> * joinvec=execution->getJoins();
 953         for(uint i=0;i<joinvec->size();i++) {
 954                 EPRecord *join=(*joinvec)[i];
 955                 ExecPoint *jp=join->getEP();
 956                 if (jp->get_tid()==thr2 &&
 957                                 jp->compare(ep2)==CR_AFTER)
 958                         return true;
 959         }
 960         return false;
 961 }
 962
 963 /** This function generates an ordering constraint for two events.  */
 964
 965 void ConstGen::createOrderConstraint(EPRecord *first, EPRecord *second) {
 966         RecPair * rp=new RecPair(first, second);
 967         if (!rpt->contains(rp)) {
 968                 if (orderThread(first, second))
 969                         rp->constraint=&ctrue;
 970                 else if (orderThread(second, first))
 971                         rp->constraint=&cfalse;
 972                 else
 973                         rp->constraint=getNewVar();
 974
 975                 rpt->put(rp, rp);
 976         } else {
 977                 delete rp;
 978         }
 979 }
 980
 981 Constraint * ConstGen::getNewVar() {
 982         Constraint *var;
 983         if (varindex>vars->size()) {
 984                 var=new Constraint(VAR, varindex);
 985                 Constraint *varneg=new Constraint(NOTVAR, varindex);
 986                 var->setNeg(varneg);
 987                 varneg->setNeg(var);
 988                 vars->push_back(var);
 989         } else {
 990                 var=(*vars)[varindex-1];
 991         }
 992         varindex++;
 993         return var;
 994 }
 995
 996 /** Gets an array of new variables.  */
 997
 998 void ConstGen::getArrayNewVars(uint num, Constraint **carray) {
 999         for(uint i=0;i<num;i++)
1000                 carray[i]=getNewVar();
1001 }
1002
1003 StoreLoadSet * ConstGen::getStoreLoadSet(EPRecord *record) {
1004         IntIterator *it=record->getSet(VC_ADDRINDEX)->iterator();
1005         void *addr=(void *)it->next();
1006         delete it;
1007         return storeloadtable->get(addr);
1008 }
1009
1010 /** Returns a constraint that is true if the output of record has the
1011                 given value. */
1012
1013 Constraint * ConstGen::getRetValueEncoding(EPRecord *record, uint64_t value) {
1014         switch(record->getType()) {
1015         case EQUALS:
1016                 return equalstable->get(record)->getValueEncoding(value);
1017         case FUNCTION:
1018                 return functiontable->get(record)->getValueEncoding(value);
1019         case LOAD: {
1020                 return getStoreLoadSet(record)->getValueEncoding(this, record, value);
1021         }
1022         case RMW: {
1023                 return getStoreLoadSet(record)->getRMWRValueEncoding(this, record, value);
1024         }
1025         default:
1026                 ASSERT(false);
1027                 exit(-1);
1028         }
1029 }
1030
1031 Constraint * ConstGen::getMemValueEncoding(EPRecord *record, uint64_t value) {
1032         switch(record->getType()) {
1033         case STORE:
1034                 return getStoreLoadSet(record)->getValueEncoding(this, record, value);
1035         case RMW:
1036                 return getStoreLoadSet(record)->getValueEncoding(this, record, value);
1037         default:
1038                 ASSERT(false);
1039                 exit(-1);
1040         }
1041 }
1042
1043 /** Return true if the execution of record implies the execution of
1044  *      recordsubsumes */
1045
1046 bool ConstGen::subsumesExecutionConstraint(EPRecord *recordsubsumes, EPRecord *record) {
1047         EPValue *branch=record->getBranch();
1048         EPValue *branchsubsumes=recordsubsumes->getBranch();
1049         if (branchsubsumes != NULL) {
1050                 bool branchsubsumed=false;
1051                 while(branch!=NULL) {
1052                         if (branchsubsumes==branch) {
1053                                 branchsubsumed=true;
1054                                 break;
1055                         }
1056                         branch=branch->getRecord()->getBranch();
1057                 }
1058                 if (!branchsubsumed)
1059                         return false;
1060         }
1061         RecordSet *srs=execcondtable->get(recordsubsumes);
1062
1063         if (srs!=NULL) {
1064                 RecordIterator *sri=srs->iterator();
1065                 while(sri->hasNext()) {
1066                         EPRecord *rec=sri->next();
1067
1068                         if (!getOrderConstraint(rec, record)->isTrue()) {
1069                                 delete sri;
1070                                 return false;
1071                         }
1072                 }
1073                 delete sri;
1074         }
1075         return true;
1076 }
1077
1078 Constraint * ConstGen::getExecutionConstraint(EPRecord *record) {
1079         EPValue *branch=record->getBranch();
1080         RecordSet *srs=execcondtable->get(record);
1081         int size=srs==NULL?0:srs->getSize();
1082         if (branch!=NULL)
1083                 size++;
1084
1085         Constraint *array[size];
1086         int index=0;
1087         if (srs!=NULL) {
1088                 RecordIterator *sri=srs->iterator();
1089                 while(sri->hasNext()) {
1090                         EPRecord *rec=sri->next();
1091                         EPValue *recbranch=rec->getBranch();
1092                         BranchRecord *guardbr=branchtable->get(recbranch->getRecord());
1093                         array[index++]=guardbr->getBranch(recbranch)->negate();
1094                 }
1095                 delete sri;
1096         }
1097         if (branch!=NULL) {
1098                 BranchRecord *guardbr=branchtable->get(branch->getRecord());
1099                 array[index++]=guardbr->getBranch(branch);
1100         }
1101         if (index==0)
1102                 return &ctrue;
1103         else if (index==1)
1104                 return array[0];
1105         else
1106                 return new Constraint(AND, index, array);
1107 }
1108
1109 bool ConstGen::isAlwaysExecuted(EPRecord *record) {
1110         EPValue *branch=record->getBranch();
1111         RecordSet *srs=execcondtable->get(record);
1112         int size=srs==NULL?0:srs->getSize();
1113         if (branch!=NULL)
1114                 size++;
1115
1116         return size==0;
1117 }
1118
1119 void ConstGen::insertBranch(EPRecord *record) {
1120         uint numvalue=record->numValues();
1121         /** need one value for new directions */
1122         if (numvalue<record->getLen())
1123                 numvalue++;
1124         /** need extra value to represent that branch wasn't executed. **/
1125         bool alwaysexecuted=isAlwaysExecuted(record);
1126         if (!alwaysexecuted)
1127                 numvalue++;
1128         uint numbits=NUMBITS(numvalue-1);
1129         Constraint *bits[numbits];
1130         getArrayNewVars(numbits, bits);
1131         BranchRecord *br=new BranchRecord(record, numbits, bits, alwaysexecuted);
1132         branchtable->put(record, br);
1133 }
1134
1135 void ConstGen::processBranch(EPRecord *record) {
1136         BranchRecord *br=branchtable->get(record);
1137         if (record->numValues()<record->getLen()) {
1138                 Constraint *goal=br->getNewBranch();
1139                 ADDBRANCHGOAL(record, goal,"newbranch");
1140         }
1141
1142         /** Insert criteria of parent branch going the right way. **/
1143         Constraint *baseconstraint=getExecutionConstraint(record);
1144
1145         if (!isAlwaysExecuted(record)) {
1146                 Constraint *parentbranch=new Constraint(IMPLIES, br->getAnyBranch(), baseconstraint);
1147                 ADDCONSTRAINT(parentbranch, "parentbranch");
1148         }
1149
1150         /** Insert criteria for directions */
1151         ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1152         ASSERT(depvec->size()==1);
1153         EPRecord * val_record=(*depvec)[0];
1154         for(unsigned int i=0;i<record->numValues();i++) {
1155                 EPValue * branchval=record->getValue(i);
1156                 uint64_t val=branchval->getValue();
1157
1158                 if (val==0) {
1159                         Constraint *execconstraint=getExecutionConstraint(record);
1160                         Constraint *br_false=new Constraint(IMPLIES,
1161                                                                                                                                                                         new Constraint(AND, execconstraint,
1162                                                                                                                                                                                                                                  getRetValueEncoding(val_record, val)), br->getBranch(branchval));
1163                         ADDCONSTRAINT(br_false, "br_false");
1164                 } else {
1165                         if (record->getBranchAnyValue()) {
1166                                 if (getRetValueEncoding(val_record, 0)!=NULL) {
1167                                         Constraint *execconstraint=getExecutionConstraint(record);
1168                                         Constraint *br_true1=new Constraint(IMPLIES, new Constraint(AND, getRetValueEncoding(val_record, 0)->negate(),
1169                                                                                                                                                                                                                                                                                         execconstraint),
1170                                                                                                                                                                                                                                                                                         br->getBranch(branchval));
1171                                         ADDCONSTRAINT(br_true1, "br_true1");
1172                                 } else {
1173                                         for(unsigned int j=0;j<val_record->numValues();j++) {
1174                                                 EPValue * epval=val_record->getValue(j);
1175                                                 Constraint *execconstraint=getExecutionConstraint(record);
1176                                                 Constraint *valuematches=getRetValueEncoding(val_record, epval->getValue());
1177                                                 Constraint *br_true2=new Constraint(IMPLIES, new Constraint(AND, execconstraint, valuematches), br->getBranch(branchval));
1178                                                 ADDCONSTRAINT(br_true2, "br_true2");
1179                                         }
1180                                 }
1181                         } else {
1182                                 Constraint *execconstraint=getExecutionConstraint(record);
1183                                 Constraint *br_val=new Constraint(IMPLIES, new Constraint(AND, execconstraint, getRetValueEncoding(val_record, val)), br->getBranch(branchval));
1184                                 ADDCONSTRAINT(br_val, "br_val");
1185                         }
1186                 }
1187         }
1188 }
1189
1190 void ConstGen::insertFunction(EPRecord *record) {
1191         FunctionRecord * fr=new FunctionRecord(this, record);
1192         functiontable->put(record, fr);
1193 }
1194
1195 void ConstGen::insertEquals(EPRecord *record) {
1196         EqualsRecord * fr=new EqualsRecord(this, record);
1197         equalstable->put(record, fr);
1198 }
1199
1200 void ConstGen::processLoad(EPRecord *record) {
1201         LoadRF * lrf=new LoadRF(record, this);
1202         lrf->genConstraints(this);
1203         delete lrf;
1204         processAddresses(record);
1205 }
1206
1207 /** This procedure generates the constraints that set the address
1208                 variables for load/store/rmw operations. */
1209
1210 void ConstGen::processAddresses(EPRecord *record) {
1211         StoreLoadSet *sls=getStoreLoadSet(record);
1212         ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_ADDRINDEX);
1213         if (depvec==NULL) {
1214                 //we have a hard coded address
1215                 const void *addr=record->getValue(0)->getAddr();
1216                 Constraint *addrenc=sls->getAddressEncoding(this, record, addr);
1217                 ADDCONSTRAINT(addrenc,"fixedaddress");
1218         } else {
1219                 //we take as input an address and have to generate implications
1220                 //for each possible input address
1221                 ASSERT(depvec->size()==1);
1222                 EPRecord *src=(*depvec)[0];
1223                 IntIterator *it=record->getSet(VC_ADDRINDEX)->iterator();
1224
1225                 uintptr_t offset=record->getOffset();
1226
1227                 while(it->hasNext()) {
1228                         uint64_t addr=it->next();
1229                         Constraint *srcenc=getRetValueEncoding(src, addr-offset);
1230                         Constraint *addrenc=sls->getAddressEncoding(this, record, (void *) addr);
1231                         Constraint *addrmatch=new Constraint(IMPLIES, srcenc, addrenc);
1232                         ADDCONSTRAINT(addrmatch,"setaddress");
1233                 }
1234                 delete it;
1235         }
1236 }
1237
1238 void ConstGen::processCAS(EPRecord *record) {
1239         //First do the load
1240         LoadRF * lrf=new LoadRF(record, this);
1241         lrf->genConstraints(this);
1242         delete lrf;
1243         //Next see if we are successful
1244         Constraint *eq=getNewVar();
1245         ModelVector<EPRecord *> * depveccas=execution->getRevDependences(record, VC_OLDVALCASINDEX);
1246         if (depveccas==NULL) {
1247                 //Hard coded old value
1248                 IntIterator *iit=record->getSet(VC_OLDVALCASINDEX)->iterator();
1249                 uint64_t valcas=iit->next();
1250                 delete iit;
1251                 Constraint *rmwr=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, valcas);
1252                 if (rmwr==NULL) {
1253                         Constraint *cascond=eq->negate();
1254                         ADDCONSTRAINT(cascond, "cascond");
1255                 } else {
1256                         Constraint *cascond=generateEquivConstraint(eq, rmwr);
1257                         ADDCONSTRAINT(cascond, "cascond");
1258                 }
1259         } else {
1260                 ASSERT(depveccas->size()==1);
1261                 EPRecord *src=(*depveccas)[0];
1262                 IntIterator *it=getStoreLoadSet(record)->getValues()->iterator();
1263
1264                 while(it->hasNext()) {
1265                         uint64_t valcas=it->next();
1266                         Constraint *srcenc=getRetValueEncoding(src, valcas);
1267                         Constraint *storeenc=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, valcas);
1268
1269                         if (srcenc!=NULL && storeenc!=NULL) {
1270                                 Constraint *cond=new Constraint(AND,
1271                                                                                                                                                                 new Constraint(IMPLIES, srcenc->clone(), eq),
1272                                                                                                                                                                 new Constraint(IMPLIES, eq, srcenc));
1273                                 Constraint *cas=new Constraint(IMPLIES, storeenc, cond);
1274                                 ADDCONSTRAINT(cas, "cas");
1275                         } else if (srcenc==NULL) {
1276                                 Constraint *casfail=new Constraint(IMPLIES, storeenc, eq->negate());
1277                                 ADDCONSTRAINT(casfail,"casfail_eq");
1278                         } else {
1279                                 //srcenc must be non-null and store-encoding must be null
1280                                 srcenc->free();
1281                         }
1282                 }
1283                 delete it;
1284                 IntIterator *iit=record->getSet(VC_OLDVALCASINDEX)->iterator();
1285                 while(iit->hasNext()) {
1286                         uint64_t val=iit->next();
1287                         if (!getStoreLoadSet(record)->getValues()->contains(val)) {
1288                                 Constraint *srcenc=getRetValueEncoding(src, val);
1289                                 Constraint *casfail=new Constraint(IMPLIES, srcenc, eq->negate());
1290                                 ADDCONSTRAINT(casfail,"casfailretval");
1291                         }
1292                 }
1293                 delete iit;
1294         }
1295
1296         ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1297         if (depvec==NULL) {
1298                 IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
1299                 uint64_t val=iit->next();
1300                 delete iit;
1301                 Constraint *storeenc=getMemValueEncoding(record, val);
1302                 Constraint *casmemsuc=new Constraint(IMPLIES, eq, storeenc);
1303                 ADDCONSTRAINT(casmemsuc, "casmemsuc");
1304         } else {
1305                 ASSERT(depvec->size()==1);
1306                 EPRecord *src=(*depvec)[0];
1307                 IntIterator *it=record->getStoreSet()->iterator();
1308
1309                 while(it->hasNext()) {
1310                         uint64_t val=it->next();
1311                         Constraint *srcenc=getRetValueEncoding(src, val);
1312                         if (srcenc==NULL) {
1313                                 //this can happen for values that are in the store set because
1314                                 //we re-stored them on a failed CAS
1315                                 continue;
1316                         }
1317                         Constraint *storeenc=getMemValueEncoding(record, val);
1318                         Constraint *storevalue=new Constraint(IMPLIES, new Constraint(AND, eq, srcenc), storeenc);
1319                         ADDCONSTRAINT(storevalue,"casmemsuc");
1320                 }
1321                 delete it;
1322         }
1323         StoreLoadSet *sls=getStoreLoadSet(record);
1324
1325         Constraint *repeatval=generateEquivConstraint(sls->getNumValVars(), sls->getValVars(this, record), sls->getRMWRValVars(this, record));
1326         Constraint *failcas=new Constraint(IMPLIES, eq->negate(), repeatval);
1327         ADDCONSTRAINT(failcas,"casmemfail");
1328
1329         processAddresses(record);
1330 }
1331
1332 void ConstGen::processEXC(EPRecord *record) {
1333         //First do the load
1334         LoadRF * lrf=new LoadRF(record, this);
1335         lrf->genConstraints(this);
1336         delete lrf;
1337
1338         ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1339         if (depvec==NULL) {
1340                 IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
1341                 uint64_t val=iit->next();
1342                 delete iit;
1343                 Constraint *storeenc=getMemValueEncoding(record, val);
1344                 ADDCONSTRAINT(storeenc, "excmemsuc");
1345         } else {
1346                 ASSERT(depvec->size()==1);
1347                 EPRecord *src=(*depvec)[0];
1348                 IntIterator *it=record->getStoreSet()->iterator();
1349
1350                 while(it->hasNext()) {
1351                         uint64_t val=it->next();
1352                         Constraint *srcenc=getRetValueEncoding(src, val);
1353                         Constraint *storeenc=getMemValueEncoding(record, val);
1354                         Constraint *storevalue=new Constraint(IMPLIES, srcenc, storeenc);
1355                         ADDCONSTRAINT(storevalue,"excmemsuc");
1356                 }
1357                 delete it;
1358         }
1359
1360         processAddresses(record);
1361 }
1362
1363 void ConstGen::processAdd(EPRecord *record) {
1364         //First do the load
1365         LoadRF * lrf=new LoadRF(record, this);
1366         lrf->genConstraints(this);
1367         delete lrf;
1368         Constraint *var=getNewVar();
1369         Constraint *newadd=new Constraint(AND, var, getExecutionConstraint(record));
1370         ADDGOAL(record, newadd, "newadd");
1371
1372         ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1373         if (depvec==NULL) {
1374                 IntIterator *valit=record->getSet(VC_BASEINDEX)->iterator();
1375                 uint64_t val=valit->next();
1376                 delete valit;
1377                 IntHashSet *valset=getStoreLoadSet(record)->getValues();
1378                 IntIterator *sis=valset->iterator();
1379                 while(sis->hasNext()) {
1380                         uint64_t memval=sis->next();
1381                         uint64_t sumval=(memval+val)&getmask(record->getLen());
1382
1383                         if (valset->contains(sumval)) {
1384
1385                                 Constraint *loadenc=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, memval);
1386                                 Constraint *storeenc=getMemValueEncoding(record, sumval);
1387                                 Constraint *notvar=var->negate();
1388                                 Constraint *addinputfix=new Constraint(IMPLIES, loadenc, new Constraint(AND, storeenc, notvar));
1389                                 ADDCONSTRAINT(addinputfix, "addinputfix");
1390                         }
1391                 }
1392
1393                 delete sis;
1394         } else {
1395                 ASSERT(depvec->size()==1);
1396                 EPRecord *src=(*depvec)[0];
1397                 IntIterator *it=record->getStoreSet()->iterator();
1398                 IntHashSet *valset=getStoreLoadSet(record)->getValues();
1399
1400                 while(it->hasNext()) {
1401                         uint64_t val=it->next();
1402                         IntIterator *sis=valset->iterator();
1403                         while(sis->hasNext()) {
1404                                 uint64_t memval=sis->next();
1405                                 uint64_t sum=(memval+val)&getmask(record->getLen());
1406                                 if (valset->contains(sum)) {
1407                                         Constraint *srcenc=getRetValueEncoding(src, val);
1408                                         Constraint *loadenc=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, memval);
1409                                         Constraint *storeenc=getMemValueEncoding(record, sum);
1410                                         Constraint *notvar=var->negate();
1411                                         Constraint *addop=new Constraint(IMPLIES, new Constraint(AND, srcenc, loadenc),
1412                                                                                                                                                                                                 new Constraint(AND, notvar, storeenc));
1413                                         ADDCONSTRAINT(addop,"addinputvar");
1414                                 }
1415                         }
1416                         delete sis;
1417                 }
1418                 delete it;
1419         }
1420
1421         processAddresses(record);
1422 }
1423
1424 /** This function ensures that the value of a store's SAT variables
1425                 matches the store's input value.
1426
1427                 TODO: Could optimize the case where the encodings are the same...
1428 */
1429
1430 void ConstGen::processStore(EPRecord *record) {
1431         ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1432         if (depvec==NULL) {
1433                 //We have a hard coded value
1434                 uint64_t val=record->getValue(0)->getValue();
1435                 Constraint *storeenc=getMemValueEncoding(record, val);
1436                 ADDCONSTRAINT(storeenc,"storefix");
1437         } else {
1438                 //We have a value from an input
1439                 ASSERT(depvec->size()==1);
1440                 EPRecord *src=(*depvec)[0];
1441                 IntIterator *it=record->getStoreSet()->iterator();
1442
1443                 while(it->hasNext()) {
1444                         uint64_t val=it->next();
1445                         Constraint *srcenc=getRetValueEncoding(src, val);
1446                         Constraint *storeenc=getMemValueEncoding(record, val);
1447                         Constraint *storevalue=new Constraint(IMPLIES, srcenc, storeenc);
1448                         ADDCONSTRAINT(storevalue,"storevar");
1449                 }
1450                 delete it;
1451         }
1452         processAddresses(record);
1453 }
1454
1455 /** Handle yields by just forbidding them via the SAT formula. */
1456
1457 void ConstGen::processYield(EPRecord *record) {
1458         if (model->params.noyields &&
1459                         record->getBranch()!=NULL) {
1460                 Constraint * noyield=getExecutionConstraint(record)->negate();
1461                 ADDCONSTRAINT(noyield, "noyield");
1462         }
1463 }
1464
1465 void ConstGen::processLoopPhi(EPRecord *record) {
1466         EPRecordIDSet *phiset=record->getPhiLoopTable();
1467         EPRecordIDIterator *rit=phiset->iterator();
1468
1469         while(rit->hasNext()) {
1470                 struct RecordIDPair *rip=rit->next();
1471                 EPRecord *input=rip->idrecord;
1472
1473                 IntIterator * it=record->getSet(VC_BASEINDEX)->iterator();
1474                 while(it->hasNext()) {
1475                         uint64_t value=it->next();
1476                         Constraint * inputencoding=getRetValueEncoding(input, value);
1477                         if (inputencoding==NULL)
1478                                 continue;
1479                         Constraint * branchconstraint=getExecutionConstraint(rip->record);
1480                         Constraint * outputencoding=getRetValueEncoding(record, value);
1481                         Constraint * phiimplication=new Constraint(IMPLIES, new Constraint(AND, inputencoding, branchconstraint), outputencoding);
1482                         ADDCONSTRAINT(phiimplication,"philoop");
1483                 }
1484                 delete it;
1485         }
1486         delete rit;
1487 }
1488
1489 void ConstGen::processPhi(EPRecord *record) {
1490         ModelVector<EPRecord *> * inputs=execution->getRevDependences(record, VC_BASEINDEX);
1491         for(uint i=0;i<inputs->size();i++) {
1492                 EPRecord * input=(*inputs)[i];
1493
1494                 IntIterator * it=record->getSet(VC_BASEINDEX)->iterator();
1495                 while(it->hasNext()) {
1496                         uint64_t value=it->next();
1497                         Constraint * inputencoding=getRetValueEncoding(input, value);
1498                         if (inputencoding==NULL)
1499                                 continue;
1500                         Constraint * branchconstraint=getExecutionConstraint(input);
1501                         Constraint * outputencoding=getRetValueEncoding(record, value);
1502                         Constraint * phiimplication=new Constraint(IMPLIES, new Constraint(AND, inputencoding, branchconstraint), outputencoding);
1503                         ADDCONSTRAINT(phiimplication,"phi");
1504                 }
1505                 delete it;
1506         }
1507 }
1508
1509 void ConstGen::processFunction(EPRecord *record) {
1510         if (record->getLoopPhi()) {
1511                 processLoopPhi(record);
1512                 return;
1513         } else if (record->getPhi()) {
1514                 processPhi(record);
1515                 return;
1516         }
1517
1518         CGoalSet *knownbehaviors=record->completedGoalSet();
1519         CGoalIterator *cit=knownbehaviors->iterator();
1520         uint numinputs=record->getNumFuncInputs();
1521         EPRecord * inputs[numinputs];
1522         for(uint i=0;i<numinputs;i++) {
1523                 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, i+VC_BASEINDEX);
1524                 ASSERT(depvec->size()==1);
1525                 inputs[i]=(*depvec)[0];
1526         }
1527         while(cit->hasNext()) {
1528                 CGoal *goal=cit->next();
1529                 Constraint *carray[numinputs];
1530                 if (record->isSharedGoals()) {
1531                         bool badvalue=false;
1532                         for(uint i=0;i<numinputs;i++) {
1533                                 uint64_t inputval=goal->getValue(i+VC_BASEINDEX);
1534                                 if (!record->getSet(i+VC_BASEINDEX)->contains(inputval)) {
1535                                         badvalue=true;
1536                                         break;
1537                                 }
1538                         }
1539                         if (badvalue)
1540                                 continue;
1541                 }
1542
1543                 /* Build up constraints for each input */
1544                 for(uint i=0;i<numinputs;i++) {
1545                         uint64_t inputval=goal->getValue(i+VC_BASEINDEX);
1546                         Constraint * inputc=getRetValueEncoding(inputs[i], inputval);
1547                         ASSERT(inputc!=NULL);
1548                         carray[i]=inputc;
1549                 }
1550                 Constraint * outputconstraint=getRetValueEncoding(record, goal->getOutput());
1551                 if (numinputs==0) {
1552                         ADDCONSTRAINT(outputconstraint,"functionimpl");
1553                 } else {
1554                         Constraint * functionimplication=new Constraint(IMPLIES, new Constraint(AND, numinputs, carray), outputconstraint);
1555                         ADDCONSTRAINT(functionimplication,"functionimpl");
1556                 }
1557         }
1558         delete cit;
1559
1560         FunctionRecord *fr=functiontable->get(record);
1561         Constraint *goal=fr->getNoValueEncoding();
1562         Constraint *newfunc=new Constraint(AND, goal, getExecutionConstraint(record));
1563         ADDGOAL(record, newfunc, "newfunc");
1564 }
1565
1566 void ConstGen::processEquals(EPRecord *record) {
1567         ASSERT (record->getNumFuncInputs() == 2);
1568         EPRecord * inputs[2];
1569
1570         for(uint i=0;i<2;i++) {
1571                 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, i+VC_BASEINDEX);
1572                 if (depvec==NULL) {
1573                         inputs[i]=NULL;
1574                 } else if (depvec->size()==1) {
1575                         inputs[i]=(*depvec)[0];
1576                 }       else ASSERT(false);
1577         }
1578
1579         //rely on this being a variable
1580         Constraint * outputtrue=getRetValueEncoding(record, 1);
1581         ASSERT(outputtrue->getType()==VAR);
1582
1583         if (inputs[0]!=NULL && inputs[1]!=NULL &&
1584                         (inputs[0]->getType()==LOAD || inputs[0]->getType()==RMW) &&
1585                         (inputs[1]->getType()==LOAD || inputs[1]->getType()==RMW) &&
1586                         (getStoreLoadSet(inputs[0])==getStoreLoadSet(inputs[1]))) {
1587                 StoreLoadSet * sls=getStoreLoadSet(inputs[0]);
1588                 int numvalvars=sls->getNumValVars();
1589                 Constraint **valvar1=(inputs[0]->getType()==RMW)?sls->getRMWRValVars(this, inputs[0]):sls->getValVars(this, inputs[0]);
1590                 Constraint **valvar2=(inputs[1]->getType()==RMW)?sls->getRMWRValVars(this, inputs[1]):sls->getValVars(this, inputs[1]);
1591                 //new test
1592
1593                 Constraint *vars[numvalvars];
1594                 for(int i=0;i<numvalvars;i++) {
1595                         vars[i]=getNewVar();
1596                         Constraint *var1=valvar1[i];
1597                         Constraint *var2=valvar2[i];
1598                         Constraint * array[]={var1, var2->negate(), vars[i]->negate()};
1599                         Constraint * array2[]={var2, var1->negate(), vars[i]->negate()};
1600                         Constraint * a=new Constraint(OR, 3, array);
1601                         ADDCONSTRAINT(a, "equala");
1602                         Constraint * a2=new Constraint(OR, 3, array2);
1603                         ADDCONSTRAINT(a2, "equala2");
1604                         Constraint * arrayb[]={var1, var2, vars[i]};
1605                         Constraint * array2b[]={var2->negate(), var1->negate(), vars[i]};
1606                         Constraint * b=new Constraint(OR, 3, arrayb);
1607                         ADDCONSTRAINT(b, "equalb");
1608                         Constraint *b2=new Constraint(OR, 3, array2b);
1609                         ADDCONSTRAINT(b2, "equalb2");
1610                 }
1611                 ADDCONSTRAINT(new Constraint(IMPLIES, new Constraint(AND, numvalvars, vars), outputtrue),"impequal1");
1612
1613                 ADDCONSTRAINT(new Constraint(IMPLIES, outputtrue, new Constraint(AND, numvalvars, vars)), "impequal2");
1614
1615                 /*
1616
1617                 Constraint * functionimplication=new Constraint(IMPLIES,generateEquivConstraint(numvalvars, valvar1, valvar2), outputtrue);
1618                 ADDCONSTRAINT(functionimplication,"equalsimplspecial");
1619                 Constraint * functionimplicationneg=new Constraint(IMPLIES,outputtrue, generateEquivConstraint(numvalvars, valvar1, valvar2));
1620                 ADDCONSTRAINT(functionimplicationneg,"equalsimplspecialneg");
1621                 */
1622                 return;
1623         }
1624
1625         if (inputs[0]==NULL && inputs[1]==NULL) {
1626                 IntIterator *iit0=record->getSet(VC_BASEINDEX+0)->iterator();
1627                 uint64_t constval=iit0->next();
1628                 delete iit0;
1629                 IntIterator *iit1=record->getSet(VC_BASEINDEX+1)->iterator();
1630                 uint64_t constval2=iit1->next();
1631                 delete iit1;
1632
1633                 if (constval==constval2) {
1634                         ADDCONSTRAINT(outputtrue, "equalsconst");
1635                 } else {
1636                         ADDCONSTRAINT(outputtrue->negate(), "equalsconst");
1637                 }
1638                 return;
1639         }
1640
1641         if (inputs[0]==NULL ||
1642                         inputs[1]==NULL) {
1643                 int nullindex=inputs[0]==NULL?0:1;
1644                 IntIterator *iit=record->getSet(VC_BASEINDEX+nullindex)->iterator();
1645                 uint64_t constval=iit->next();
1646                 delete iit;
1647
1648                 record->getSet(VC_BASEINDEX+nullindex);
1649                 EPRecord *r=inputs[1-nullindex];
1650                 Constraint *l=getRetValueEncoding(r, constval);
1651                 Constraint *functionimplication=new Constraint(IMPLIES, l, outputtrue);
1652                 ADDCONSTRAINT(functionimplication,"equalsimpl");
1653
1654                 Constraint *l2=getRetValueEncoding(r, constval);
1655                 Constraint *functionimplication2=new Constraint(IMPLIES, outputtrue, l2);
1656                 ADDCONSTRAINT(functionimplication2,"equalsimpl");
1657         }
1658
1659         IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
1660         while(iit->hasNext()) {
1661                 uint64_t val1=iit->next();
1662
1663                 IntIterator *iit2=record->getSet(VC_BASEINDEX+1)->iterator();
1664                 while(iit2->hasNext()) {
1665                         uint64_t val2=iit2->next();
1666                         Constraint *l=getRetValueEncoding(inputs[0], val1);
1667                         Constraint *r=getRetValueEncoding(inputs[1], val2);
1668                         Constraint *imp=(val1==val2)?outputtrue:outputtrue->negate();
1669                         Constraint * functionimplication=new Constraint(IMPLIES, new Constraint(AND, l, r), imp);
1670                         ADDCONSTRAINT(functionimplication,"equalsimpl");
1671                 }
1672                 delete iit2;
1673         }
1674         delete iit;
1675 }
1676
1677 #ifdef TSO
1678 void ConstGen::processFence(EPRecord *record) {
1679         //do we already account for the fence?
1680         if (isAlwaysExecuted(record))
1681                 return;
1682         ExecPoint * record_ep=record->getEP();
1683         thread_id_t tid=record_ep->get_tid();
1684         uint thread=id_to_int(tid);
1685         ModelVector<EPRecord *> *tvec=(*threadactions)[thread];
1686         uint size=tvec->size();
1687
1688         EPRecord *prevstore=NULL;
1689         uint i;
1690         for(i=0;i<size;i++) {
1691                 EPRecord *rec=(*tvec)[i];
1692                 if (rec->getType()==STORE) {
1693                         prevstore=rec;
1694                 }
1695                 if (rec == record) {
1696                         i++;
1697                         break;
1698                 }
1699         }
1700         if (prevstore == NULL) {
1701                 return;
1702         }
1703         for(;i<size;i++) {
1704                 EPRecord *rec=(*tvec)[i];
1705                 if (rec->getType()==LOAD) {
1706                         Constraint * condition=getExecutionConstraint(record);
1707                         Constraint * storeload=getOrderConstraint(prevstore, rec);
1708                         Constraint * c=new Constraint(IMPLIES, condition, storeload);
1709                         ADDCONSTRAINT(c, "fence");
1710                         return;
1711                 }
1712         }
1713 }
1714 #endif
1715
1716 void ConstGen::processRecord(EPRecord *record) {
1717         switch (record->getType()) {
1718         case FUNCTION:
1719                 processFunction(record);
1720                 break;
1721         case EQUALS:
1722                 processEquals(record);
1723                 break;
1724         case LOAD:
1725                 processLoad(record);
1726                 break;
1727         case STORE:
1728                 processStore(record);
1729                 break;
1730 #ifdef TSO
1731         case FENCE:
1732                 processFence(record);
1733                 break;
1734 #endif
1735         case RMW:
1736 #ifdef TSO
1737                 processFence(record);
1738 #endif
1739                 if (record->getOp()==ADD) {
1740                         processAdd(record);
1741                 } else if (record->getOp()==CAS) {
1742                         processCAS(record);
1743                 } else if (record->getOp()==EXC) {
1744                         processEXC(record);
1745                 } else
1746                         ASSERT(0);
1747                 break;
1748         case YIELD:
1749                 processYield(record);
1750                 break;
1751         case BRANCHDIR:
1752                 processBranch(record);
1753                 break;
1754         default:
1755                 break;
1756         }
1757 }
1758
1759 void ConstGen::visitRecord(EPRecord *record) {
1760         switch (record->getType()) {
1761         case EQUALS:
1762                 recordExecCond(record);
1763                 insertEquals(record);
1764                 break;
1765         case FUNCTION:
1766                 recordExecCond(record);
1767                 insertFunction(record);
1768                 break;
1769 #ifdef TSO
1770         case FENCE:
1771                 recordExecCond(record);
1772                 insertAction(record);
1773                 break;
1774 #endif
1775         case LOAD:
1776                 recordExecCond(record);
1777                 insertAction(record);
1778                 groupMemoryOperations(record);
1779                 break;
1780         case STORE:
1781                 recordExecCond(record);
1782                 insertAction(record);
1783                 groupMemoryOperations(record);
1784                 break;
1785         case RMW:
1786                 recordExecCond(record);
1787                 insertAction(record);
1788                 groupMemoryOperations(record);
1789                 break;
1790         case BRANCHDIR:
1791                 recordExecCond(record);
1792                 insertBranch(record);
1793                 break;
1794         case LOOPEXIT:
1795                 recordExecCond(record);
1796                 break;
1797         case NONLOCALTRANS:
1798                 recordExecCond(record);
1799                 insertNonLocal(record);
1800                 break;
1801         case LABEL:
1802                 insertLabel(record);
1803                 break;
1804         case YIELD:
1805                 recordExecCond(record);
1806                 break;
1807         default:
1808                 break;
1809         }
1810 }
1811
1812 void ConstGen::recordExecCond(EPRecord *record) {
1813         ExecPoint *eprecord=record->getEP();
1814         EPValue * branchval=record->getBranch();
1815         EPRecord * branch=(branchval==NULL)?NULL:branchval->getRecord();
1816         ExecPoint *epbranch= (branch==NULL) ? NULL : branch->getEP();
1817         RecordSet *srs=NULL;
1818         RecordIterator *sri=nonlocaltrans->iterator();
1819         while(sri->hasNext()) {
1820                 EPRecord *nonlocal=sri->next();
1821                 ExecPoint *epnl=nonlocal->getEP();
1822                 if (epbranch!=NULL) {
1823                         if (epbranch->compare(epnl)==CR_BEFORE) {
1824                                 //branch occurs after non local and thus will subsume condition
1825                                 //branch subsumes this condition
1826                                 continue;
1827                         }
1828                 }
1829                 if (eprecord->compare(epnl)==CR_BEFORE) {
1830                         //record occurs after non-local, so add it to set
1831                         if (srs==NULL)
1832                                 srs=new RecordSet();
1833                         srs->add(nonlocal);
1834                 }
1835         }
1836         delete sri;
1837         if (srs!=NULL)
1838                 execcondtable->put(record, srs);
1839 }
1840
1841 void ConstGen::insertNonLocal(EPRecord *record) {
1842         nonlocaltrans->add(record);
1843 }
1844
1845 void ConstGen::insertLabel(EPRecord *record) {
1846         RecordIterator *sri=nonlocaltrans->iterator();
1847         while(sri->hasNext()) {
1848                 EPRecord *nonlocal=sri->next();
1849                 if (nonlocal->getNextRecord()==record)
1850                         sri->remove();
1851         }
1852
1853         delete sri;
1854 }
1855
1856 void ConstGen::traverseRecord(EPRecord *record, bool initial) {
1857         do {
1858                 if (initial) {
1859                         visitRecord(record);
1860                 } else {
1861                         processRecord(record);
1862                 }
1863                 if (record->getType()==LOOPENTER) {
1864                         workstack->push_back(record->getNextRecord());
1865                         workstack->push_back(record->getChildRecord());
1866                         return;
1867                 }
1868                 if (record->getChildRecord()!=NULL) {
1869                         workstack->push_back(record->getChildRecord());
1870                 }
1871                 if (record->getType()==NONLOCALTRANS) {
1872                         return;
1873                 }
1874                 if (record->getType()==LOOPEXIT) {
1875                         return;
1876                 }
1877                 if (record->getType()==BRANCHDIR) {
1878                         EPRecord *next=record->getNextRecord();
1879                         if (next != NULL)
1880                                 workstack->push_back(next);
1881                         for(uint i=0;i<record->numValues();i++) {
1882                                 EPValue *branchdir=record->getValue(i);
1883
1884                                 //Could have an empty branch, so make sure the branch actually
1885                                 //runs code
1886                                 if (branchdir->getFirstRecord()!=NULL)
1887                                         workstack->push_back(branchdir->getFirstRecord());
1888                         }
1889                         return;
1890                 } else
1891                         record=record->getNextRecord();
1892         } while(record!=NULL);
1893 }
1894
1895 unsigned int RecPairHash(RecPair *rp) {
1896         uintptr_t v=(uintptr_t) rp->epr1;
1897         uintptr_t v2=(uintptr_t) rp->epr2;
1898         uintptr_t x=v^v2;
1899         uintptr_t a=v&v2;
1900         return (uint)((x>>4)^(a));
1901 }
1902
1903 bool RecPairEquals(RecPair *r1, RecPair *r2) {
1904         return ((r1->epr1==r2->epr1)&&(r1->epr2==r2->epr2)) ||
1905                 ((r1->epr1==r2->epr2)&&(r1->epr2==r2->epr1));
1906 }