constgen.cc

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