constgen.cc

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