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                         return true;
 988         }
 989         return false;
 990 }
 991
 992 /** This function generates an ordering constraint for two events.  */
 993
 994 void ConstGen::createOrderConstraint(EPRecord *first, EPRecord *second) {
 995         RecPair * rp=new RecPair(first, second);
 996         if (!rpt->contains(rp)) {
 997                 if (orderThread(first, second))
 998                         rp->constraint=&ctrue;
 999                 else if (orderThread(second, first))
1000                         rp->constraint=&cfalse;
1001                 else
1002                         rp->constraint=getNewVar();
1003
1004                 rpt->put(rp, rp);
1005         } else {
1006                 delete rp;
1007         }
1008 }
1009
1010 Constraint * ConstGen::getNewVar() {
1011         Constraint *var;
1012         if (varindex>vars->size()) {
1013                 var=new Constraint(VAR, varindex);
1014                 Constraint *varneg=new Constraint(NOTVAR, varindex);
1015                 var->setNeg(varneg);
1016                 varneg->setNeg(var);
1017                 vars->push_back(var);
1018         } else {
1019                 var=(*vars)[varindex-1];
1020         }
1021         varindex++;
1022         return var;
1023 }
1024
1025 /** Gets an array of new variables.  */
1026
1027 void ConstGen::getArrayNewVars(uint num, Constraint **carray) {
1028         for(uint i=0;i<num;i++)
1029                 carray[i]=getNewVar();
1030 }
1031
1032 StoreLoadSet * ConstGen::getStoreLoadSet(EPRecord *record) {
1033         IntIterator *it=record->getSet(VC_ADDRINDEX)->iterator();
1034         void *addr=(void *)it->next();
1035         delete it;
1036         return storeloadtable->get(addr);
1037 }
1038
1039 /** Returns a constraint that is true if the output of record has the
1040                 given value. */
1041
1042 Constraint * ConstGen::getRetValueEncoding(EPRecord *record, uint64_t value) {
1043         switch(record->getType()) {
1044         case EQUALS:
1045                 return equalstable->get(record)->getValueEncoding(value);
1046         case FUNCTION:
1047                 return functiontable->get(record)->getValueEncoding(value);
1048         case LOAD: {
1049                 return getStoreLoadSet(record)->getValueEncoding(this, record, value);
1050         }
1051         case RMW: {
1052                 return getStoreLoadSet(record)->getRMWRValueEncoding(this, record, value);
1053         }
1054         default:
1055                 ASSERT(false);
1056                 exit(-1);
1057         }
1058 }
1059
1060 Constraint * ConstGen::getMemValueEncoding(EPRecord *record, uint64_t value) {
1061         switch(record->getType()) {
1062         case STORE:
1063                 return getStoreLoadSet(record)->getValueEncoding(this, record, value);
1064         case RMW:
1065                 return getStoreLoadSet(record)->getValueEncoding(this, record, value);
1066         default:
1067                 ASSERT(false);
1068                 exit(-1);
1069         }
1070 }
1071
1072 /** Return true if the execution of record implies the execution of
1073  *      recordsubsumes */
1074
1075 bool ConstGen::subsumesExecutionConstraint(EPRecord *recordsubsumes, EPRecord *record) {
1076         EPValue *branch=record->getBranch();
1077         EPValue *branchsubsumes=recordsubsumes->getBranch();
1078         if (branchsubsumes != NULL) {
1079                 bool branchsubsumed=false;
1080                 while(branch!=NULL) {
1081                         if (branchsubsumes==branch) {
1082                                 branchsubsumed=true;
1083                                 break;
1084                         }
1085                         branch=branch->getRecord()->getBranch();
1086                 }
1087                 if (!branchsubsumed)
1088                         return false;
1089         }
1090         RecordSet *srs=execcondtable->get(recordsubsumes);
1091
1092         if (srs!=NULL) {
1093                 RecordIterator *sri=srs->iterator();
1094                 while(sri->hasNext()) {
1095                         EPRecord *rec=sri->next();
1096
1097                         if (!getOrderConstraint(rec, record)->isTrue()) {
1098                                 delete sri;
1099                                 return false;
1100                         }
1101                 }
1102                 delete sri;
1103         }
1104         return true;
1105 }
1106
1107 Constraint * ConstGen::getExecutionConstraint(EPRecord *record) {
1108         EPValue *branch=record->getBranch();
1109         RecordSet *srs=execcondtable->get(record);
1110         int size=srs==NULL ? 0 : srs->getSize();
1111         if (branch!=NULL)
1112                 size++;
1113
1114         Constraint *array[size];
1115         int index=0;
1116         if (srs!=NULL) {
1117                 RecordIterator *sri=srs->iterator();
1118                 while(sri->hasNext()) {
1119                         EPRecord *rec=sri->next();
1120                         EPValue *recbranch=rec->getBranch();
1121                         BranchRecord *guardbr=branchtable->get(recbranch->getRecord());
1122                         array[index++]=guardbr->getBranch(recbranch)->negate();
1123                 }
1124                 delete sri;
1125         }
1126         if (branch!=NULL) {
1127                 BranchRecord *guardbr=branchtable->get(branch->getRecord());
1128                 array[index++]=guardbr->getBranch(branch);
1129         }
1130         if (index==0)
1131                 return &ctrue;
1132         else if (index==1)
1133                 return array[0];
1134         else
1135                 return new Constraint(AND, index, array);
1136 }
1137
1138 bool ConstGen::isAlwaysExecuted(EPRecord *record) {
1139         EPValue *branch=record->getBranch();
1140         RecordSet *srs=execcondtable->get(record);
1141         int size=srs==NULL ? 0 : srs->getSize();
1142         if (branch!=NULL)
1143                 size++;
1144
1145         return size==0;
1146 }
1147
1148 void ConstGen::insertBranch(EPRecord *record) {
1149         uint numvalue=record->numValues();
1150         /** need one value for new directions */
1151         if (numvalue<record->getLen()) {
1152                 numvalue++;
1153                 if (model->params.noexecyields) {
1154                         incompleteexploredbranch->add(record);
1155                 }
1156         }
1157         /** need extra value to represent that branch wasn't executed. **/
1158         bool alwaysexecuted=isAlwaysExecuted(record);
1159         if (!alwaysexecuted)
1160                 numvalue++;
1161         uint numbits=NUMBITS(numvalue-1);
1162         Constraint *bits[numbits];
1163         getArrayNewVars(numbits, bits);
1164         BranchRecord *br=new BranchRecord(record, numbits, bits, alwaysexecuted);
1165         branchtable->put(record, br);
1166 }
1167
1168 void ConstGen::processBranch(EPRecord *record) {
1169         BranchRecord *br=branchtable->get(record);
1170         if (record->numValues()<record->getLen()) {
1171                 Constraint *goal=br->getNewBranch();
1172                 ADDBRANCHGOAL(record, goal,"newbranch");
1173         }
1174
1175         /** Insert criteria of parent branch going the right way. **/
1176         Constraint *baseconstraint=getExecutionConstraint(record);
1177
1178         if (!isAlwaysExecuted(record)) {
1179                 Constraint *parentbranch=new Constraint(IMPLIES, br->getAnyBranch(), baseconstraint);
1180                 ADDCONSTRAINT(parentbranch, "parentbranch");
1181         }
1182
1183         /** Insert criteria for directions */
1184         ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1185         ASSERT(depvec->size()==1);
1186         EPRecord * val_record=(*depvec)[0];
1187         for(unsigned int i=0;i<record->numValues();i++) {
1188                 EPValue * branchval=record->getValue(i);
1189                 uint64_t val=branchval->getValue();
1190
1191                 if (val==0) {
1192                         Constraint *execconstraint=getExecutionConstraint(record);
1193                         Constraint *br_false=new Constraint(IMPLIES,
1194                                                                                                                                                                         new Constraint(AND, execconstraint,
1195                                                                                                                                                                                                                                  getRetValueEncoding(val_record, val)), br->getBranch(branchval));
1196                         ADDCONSTRAINT(br_false, "br_false");
1197                 } else {
1198                         if (record->getBranchAnyValue()) {
1199                                 if (getRetValueEncoding(val_record, 0)!=NULL) {
1200                                         Constraint *execconstraint=getExecutionConstraint(record);
1201                                         Constraint *br_true1=new Constraint(IMPLIES, new Constraint(AND, getRetValueEncoding(val_record, 0)->negate(),
1202                                                                                                                                                                                                                                                                                         execconstraint),
1203                                                                                                                                                                                         br->getBranch(branchval));
1204                                         ADDCONSTRAINT(br_true1, "br_true1");
1205                                 } else {
1206                                         for(unsigned int j=0;j<val_record->numValues();j++) {
1207                                                 EPValue * epval=val_record->getValue(j);
1208                                                 Constraint *execconstraint=getExecutionConstraint(record);
1209                                                 Constraint *valuematches=getRetValueEncoding(val_record, epval->getValue());
1210                                                 Constraint *br_true2=new Constraint(IMPLIES, new Constraint(AND, execconstraint, valuematches), br->getBranch(branchval));
1211                                                 ADDCONSTRAINT(br_true2, "br_true2");
1212                                         }
1213                                 }
1214                         } else {
1215                                 Constraint *execconstraint=getExecutionConstraint(record);
1216                                 Constraint *br_val=new Constraint(IMPLIES, new Constraint(AND, execconstraint, getRetValueEncoding(val_record, val)), br->getBranch(branchval));
1217                                 ADDCONSTRAINT(br_val, "br_val");
1218                         }
1219                 }
1220         }
1221 }
1222
1223 void ConstGen::insertFunction(EPRecord *record) {
1224         FunctionRecord * fr=new FunctionRecord(this, record);
1225         functiontable->put(record, fr);
1226 }
1227
1228 void ConstGen::insertEquals(EPRecord *record) {
1229         EqualsRecord * fr=new EqualsRecord(this, record);
1230         equalstable->put(record, fr);
1231 }
1232
1233 void ConstGen::processLoad(EPRecord *record) {
1234         LoadRF * lrf=new LoadRF(record, this);
1235         lrf->genConstraints(this);
1236         delete lrf;
1237         processAddresses(record);
1238 }
1239
1240 /** This procedure generates the constraints that set the address
1241                 variables for load/store/rmw operations. */
1242
1243 void ConstGen::processAddresses(EPRecord *record) {
1244         StoreLoadSet *sls=getStoreLoadSet(record);
1245         ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_ADDRINDEX);
1246         if (depvec==NULL) {
1247                 //we have a hard coded address
1248                 const void *addr=record->getValue(0)->getAddr();
1249                 Constraint *addrenc=sls->getAddressEncoding(this, record, addr);
1250                 ADDCONSTRAINT(addrenc,"fixedaddress");
1251         } else {
1252                 //we take as input an address and have to generate implications
1253                 //for each possible input address
1254                 ASSERT(depvec->size()==1);
1255                 EPRecord *src=(*depvec)[0];
1256                 IntIterator *it=record->getSet(VC_ADDRINDEX)->iterator();
1257
1258                 uintptr_t offset=record->getOffset();
1259
1260                 while(it->hasNext()) {
1261                         uint64_t addr=it->next();
1262                         Constraint *srcenc=getRetValueEncoding(src, addr-offset);
1263                         Constraint *addrenc=sls->getAddressEncoding(this, record, (void *) addr);
1264                         Constraint *addrmatch=new Constraint(IMPLIES, srcenc, addrenc);
1265                         ADDCONSTRAINT(addrmatch,"setaddress");
1266                 }
1267                 delete it;
1268         }
1269 }
1270
1271 void ConstGen::processCAS(EPRecord *record) {
1272         //First do the load
1273         LoadRF * lrf=new LoadRF(record, this);
1274         lrf->genConstraints(this);
1275         delete lrf;
1276         //Next see if we are successful
1277         Constraint *eq=getNewVar();
1278         ModelVector<EPRecord *> * depveccas=execution->getRevDependences(record, VC_OLDVALCASINDEX);
1279         if (depveccas==NULL) {
1280                 //Hard coded old value
1281                 IntIterator *iit=record->getSet(VC_OLDVALCASINDEX)->iterator();
1282                 uint64_t valcas=iit->next();
1283                 delete iit;
1284                 Constraint *rmwr=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, valcas);
1285                 if (rmwr==NULL) {
1286                         Constraint *cascond=eq->negate();
1287                         ADDCONSTRAINT(cascond, "cascond");
1288                 } else {
1289                         Constraint *cascond=generateEquivConstraint(eq, rmwr);
1290                         ADDCONSTRAINT(cascond, "cascond");
1291                 }
1292         } else {
1293                 ASSERT(depveccas->size()==1);
1294                 EPRecord *src=(*depveccas)[0];
1295                 IntIterator *it=getStoreLoadSet(record)->getValues()->iterator();
1296
1297                 while(it->hasNext()) {
1298                         uint64_t valcas=it->next();
1299                         Constraint *srcenc=getRetValueEncoding(src, valcas);
1300                         Constraint *storeenc=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, valcas);
1301
1302                         if (srcenc!=NULL && storeenc!=NULL) {
1303                                 Constraint *cond=new Constraint(AND,
1304                                                                                                                                                                 new Constraint(IMPLIES, srcenc->clone(), eq),
1305                                                                                                                                                                 new Constraint(IMPLIES, eq, srcenc));
1306                                 Constraint *cas=new Constraint(IMPLIES, storeenc, cond);
1307                                 ADDCONSTRAINT(cas, "cas");
1308                         } else if (srcenc==NULL) {
1309                                 Constraint *casfail=new Constraint(IMPLIES, storeenc, eq->negate());
1310                                 ADDCONSTRAINT(casfail,"casfail_eq");
1311                         } else {
1312                                 //srcenc must be non-null and store-encoding must be null
1313                                 srcenc->free();
1314                         }
1315                 }
1316                 delete it;
1317                 IntIterator *iit=record->getSet(VC_OLDVALCASINDEX)->iterator();
1318                 while(iit->hasNext()) {
1319                         uint64_t val=iit->next();
1320                         if (!getStoreLoadSet(record)->getValues()->contains(val)) {
1321                                 Constraint *srcenc=getRetValueEncoding(src, val);
1322                                 Constraint *casfail=new Constraint(IMPLIES, srcenc, eq->negate());
1323                                 ADDCONSTRAINT(casfail,"casfailretval");
1324                         }
1325                 }
1326                 delete iit;
1327         }
1328
1329         ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1330         if (depvec==NULL) {
1331                 IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
1332                 uint64_t val=iit->next();
1333                 delete iit;
1334                 Constraint *storeenc=getMemValueEncoding(record, val);
1335                 Constraint *casmemsuc=new Constraint(IMPLIES, eq, storeenc);
1336                 ADDCONSTRAINT(casmemsuc, "casmemsuc");
1337         } else {
1338                 ASSERT(depvec->size()==1);
1339                 EPRecord *src=(*depvec)[0];
1340                 IntIterator *it=record->getStoreSet()->iterator();
1341
1342                 while(it->hasNext()) {
1343                         uint64_t val=it->next();
1344                         Constraint *srcenc=getRetValueEncoding(src, val);
1345                         if (srcenc==NULL) {
1346                                 //this can happen for values that are in the store set because
1347                                 //we re-stored them on a failed CAS
1348                                 continue;
1349                         }
1350                         Constraint *storeenc=getMemValueEncoding(record, val);
1351                         Constraint *storevalue=new Constraint(IMPLIES, new Constraint(AND, eq, srcenc), storeenc);
1352                         ADDCONSTRAINT(storevalue,"casmemsuc");
1353                 }
1354                 delete it;
1355         }
1356         StoreLoadSet *sls=getStoreLoadSet(record);
1357
1358         Constraint *repeatval=generateEquivConstraint(sls->getNumValVars(), sls->getValVars(this, record), sls->getRMWRValVars(this, record));
1359         Constraint *failcas=new Constraint(IMPLIES, eq->negate(), repeatval);
1360         ADDCONSTRAINT(failcas,"casmemfail");
1361
1362         processAddresses(record);
1363 }
1364
1365 void ConstGen::processEXC(EPRecord *record) {
1366         //First do the load
1367         LoadRF * lrf=new LoadRF(record, this);
1368         lrf->genConstraints(this);
1369         delete lrf;
1370
1371         ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1372         if (depvec==NULL) {
1373                 IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
1374                 uint64_t val=iit->next();
1375                 delete iit;
1376                 Constraint *storeenc=getMemValueEncoding(record, val);
1377                 ADDCONSTRAINT(storeenc, "excmemsuc");
1378         } else {
1379                 ASSERT(depvec->size()==1);
1380                 EPRecord *src=(*depvec)[0];
1381                 IntIterator *it=record->getStoreSet()->iterator();
1382
1383                 while(it->hasNext()) {
1384                         uint64_t val=it->next();
1385                         Constraint *srcenc=getRetValueEncoding(src, val);
1386                         Constraint *storeenc=getMemValueEncoding(record, val);
1387                         Constraint *storevalue=new Constraint(IMPLIES, srcenc, storeenc);
1388                         ADDCONSTRAINT(storevalue,"excmemsuc");
1389                 }
1390                 delete it;
1391         }
1392
1393         processAddresses(record);
1394 }
1395
1396 void ConstGen::processAdd(EPRecord *record) {
1397         //First do the load
1398         LoadRF * lrf=new LoadRF(record, this);
1399         lrf->genConstraints(this);
1400         delete lrf;
1401         Constraint *var=getNewVar();
1402         Constraint *newadd=new Constraint(AND, var, getExecutionConstraint(record));
1403         ADDGOAL(record, newadd, "newadd");
1404
1405         ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1406         if (depvec==NULL) {
1407                 IntIterator *valit=record->getSet(VC_BASEINDEX)->iterator();
1408                 uint64_t val=valit->next();
1409                 delete valit;
1410                 IntHashSet *valset=getStoreLoadSet(record)->getValues();
1411                 IntIterator *sis=valset->iterator();
1412                 while(sis->hasNext()) {
1413                         uint64_t memval=sis->next();
1414                         uint64_t sumval=(memval+val)&getmask(record->getLen());
1415
1416                         if (valset->contains(sumval)) {
1417
1418                                 Constraint *loadenc=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, memval);
1419                                 Constraint *storeenc=getMemValueEncoding(record, sumval);
1420                                 Constraint *notvar=var->negate();
1421                                 Constraint *addinputfix=new Constraint(IMPLIES, loadenc, new Constraint(AND, storeenc, notvar));
1422                                 ADDCONSTRAINT(addinputfix, "addinputfix");
1423                         }
1424                 }
1425
1426                 delete sis;
1427         } else {
1428                 ASSERT(depvec->size()==1);
1429                 EPRecord *src=(*depvec)[0];
1430                 IntIterator *it=record->getStoreSet()->iterator();
1431                 IntHashSet *valset=getStoreLoadSet(record)->getValues();
1432
1433                 while(it->hasNext()) {
1434                         uint64_t val=it->next();
1435                         IntIterator *sis=valset->iterator();
1436                         while(sis->hasNext()) {
1437                                 uint64_t memval=sis->next();
1438                                 uint64_t sum=(memval+val)&getmask(record->getLen());
1439                                 if (valset->contains(sum)) {
1440                                         Constraint *srcenc=getRetValueEncoding(src, val);
1441                                         Constraint *loadenc=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, memval);
1442                                         Constraint *storeenc=getMemValueEncoding(record, sum);
1443                                         Constraint *notvar=var->negate();
1444                                         Constraint *addop=new Constraint(IMPLIES, new Constraint(AND, srcenc, loadenc),
1445                                                                                                                                                                          new Constraint(AND, notvar, storeenc));
1446                                         ADDCONSTRAINT(addop,"addinputvar");
1447                                 }
1448                         }
1449                         delete sis;
1450                 }
1451                 delete it;
1452         }
1453
1454         processAddresses(record);
1455 }
1456
1457 /** This function ensures that the value of a store's SAT variables
1458                 matches the store's input value.
1459
1460                 TODO: Could optimize the case where the encodings are the same...
1461  */
1462
1463 void ConstGen::processStore(EPRecord *record) {
1464         ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1465         if (depvec==NULL) {
1466                 //We have a hard coded value
1467                 uint64_t val=record->getValue(0)->getValue();
1468                 Constraint *storeenc=getMemValueEncoding(record, val);
1469                 ADDCONSTRAINT(storeenc,"storefix");
1470         } else {
1471                 //We have a value from an input
1472                 ASSERT(depvec->size()==1);
1473                 EPRecord *src=(*depvec)[0];
1474                 IntIterator *it=record->getStoreSet()->iterator();
1475
1476                 while(it->hasNext()) {
1477                         uint64_t val=it->next();
1478                         Constraint *srcenc=getRetValueEncoding(src, val);
1479                         Constraint *storeenc=getMemValueEncoding(record, val);
1480                         Constraint *storevalue=new Constraint(IMPLIES, srcenc, storeenc);
1481                         ADDCONSTRAINT(storevalue,"storevar");
1482                 }
1483                 delete it;
1484         }
1485         processAddresses(record);
1486 }
1487
1488 /** **/
1489
1490 void ConstGen::computeYieldCond(EPRecord *record) {
1491         ExecPoint *yieldep=record->getEP();
1492         EPRecord *prevyield=NULL;
1493         ExecPoint *prevyieldep=NULL;
1494
1495         for(int i=(int)(yieldlist->size()-1);i>=0;i--) {
1496                 EPRecord *tmpyield=(*yieldlist)[i];
1497                 ExecPoint *tmpep=tmpyield->getEP();
1498                 //Do we have a previous yield operation from the same thread
1499                 if (tmpep->get_tid()==yieldep->get_tid() &&
1500                                 yieldep->compare(tmpep)==CR_BEFORE) {
1501                         //Yes
1502                         prevyield=tmpyield;
1503                         prevyieldep=prevyield->getEP();
1504                         break;
1505                 }
1506         }
1507
1508         yieldlist->push_back(record);
1509
1510         ModelVector<Constraint *> * novel_branches=new ModelVector<Constraint *>();
1511         RecordIterator *sri=incompleteexploredbranch->iterator();
1512         while(sri->hasNext()) {
1513                 EPRecord * unexploredbranch=sri->next();
1514                 ExecPoint * branchep=unexploredbranch->getEP();
1515                 if (branchep->get_tid()!=yieldep->get_tid()) {
1516                         //wrong thread
1517                         continue;
1518                 }
1519
1520                 if (yieldep->compare(branchep)!=CR_BEFORE) {
1521                         //Branch does not occur before yield, so skip
1522                         continue;
1523                 }
1524
1525                 //See if the previous yield already accounts for this branch
1526                 if (prevyield != NULL &&
1527                                 prevyieldep->compare(branchep)==CR_BEFORE) {
1528                         //Branch occurs before previous yield, so we can safely skip this branch
1529                         continue;
1530                 }
1531                 //This is a branch that could prevent this yield from being executed
1532                 BranchRecord *br=branchtable->get(unexploredbranch);
1533                 Constraint * novel_branch=br->getNewBranch();
1534                 novel_branches->push_back(novel_branch);
1535         }
1536
1537         int num_constraints=((prevyield==NULL)?0:1)+novel_branches->size();
1538         Constraint *carray[num_constraints];
1539         int arr_index=0;
1540
1541         if (prevyield!=NULL) {
1542                 carray[arr_index++]=yieldtable->get(prevyield);//get constraint for old yield
1543         }
1544         for(uint i=0;i<novel_branches->size();i++) {
1545                 carray[arr_index++]=(*novel_branches)[i];
1546         }
1547
1548         Constraint *cor=num_constraints!=0?new Constraint(OR, num_constraints, carray):&cfalse;
1549
1550         Constraint *var=getNewVar();
1551         //If the variable is true, then we need to have taken some branch
1552         //ahead of the yield
1553         Constraint *implies=new Constraint(IMPLIES, var, cor);
1554         ADDCONSTRAINT(implies, "possiblebranchnoyield");
1555         yieldtable->put(record, var);
1556
1557         delete novel_branches;
1558         delete sri;
1559 }
1560
1561
1562 /** Handle yields by just forbidding them via the SAT formula. */
1563
1564 void ConstGen::processYield(EPRecord *record) {
1565         if (model->params.noexecyields) {
1566                 computeYieldCond(record);
1567                 Constraint * noexecyield=getExecutionConstraint(record)->negate();
1568                 Constraint * branchaway=yieldtable->get(record);
1569                 Constraint * avoidbranch=new Constraint(OR, noexecyield, branchaway);
1570                 ADDCONSTRAINT(avoidbranch, "noexecyield");
1571         }
1572 }
1573
1574 void ConstGen::processLoopPhi(EPRecord *record) {
1575         EPRecordIDSet *phiset=record->getPhiLoopTable();
1576         EPRecordIDIterator *rit=phiset->iterator();
1577
1578         while(rit->hasNext()) {
1579                 struct RecordIDPair *rip=rit->next();
1580                 EPRecord *input=rip->idrecord;
1581
1582                 IntIterator * it=record->getSet(VC_BASEINDEX)->iterator();
1583                 while(it->hasNext()) {
1584                         uint64_t value=it->next();
1585                         Constraint * inputencoding=getRetValueEncoding(input, value);
1586                         if (inputencoding==NULL)
1587                                 continue;
1588                         Constraint * branchconstraint=getExecutionConstraint(rip->record);
1589                         Constraint * outputencoding=getRetValueEncoding(record, value);
1590                         Constraint * phiimplication=new Constraint(IMPLIES, new Constraint(AND, inputencoding, branchconstraint), outputencoding);
1591                         ADDCONSTRAINT(phiimplication,"philoop");
1592                 }
1593                 delete it;
1594         }
1595         delete rit;
1596 }
1597
1598 void ConstGen::processPhi(EPRecord *record) {
1599         ModelVector<EPRecord *> * inputs=execution->getRevDependences(record, VC_BASEINDEX);
1600         for(uint i=0;i<inputs->size();i++) {
1601                 EPRecord * input=(*inputs)[i];
1602
1603                 IntIterator * it=record->getSet(VC_BASEINDEX)->iterator();
1604                 while(it->hasNext()) {
1605                         uint64_t value=it->next();
1606                         Constraint * inputencoding=getRetValueEncoding(input, value);
1607                         if (inputencoding==NULL)
1608                                 continue;
1609                         Constraint * branchconstraint=getExecutionConstraint(input);
1610                         Constraint * outputencoding=getRetValueEncoding(record, value);
1611                         Constraint * phiimplication=new Constraint(IMPLIES, new Constraint(AND, inputencoding, branchconstraint), outputencoding);
1612                         ADDCONSTRAINT(phiimplication,"phi");
1613                 }
1614                 delete it;
1615         }
1616 }
1617
1618 void ConstGen::processFunction(EPRecord *record) {
1619         if (record->getLoopPhi()) {
1620                 processLoopPhi(record);
1621                 return;
1622         } else if (record->getPhi()) {
1623                 processPhi(record);
1624                 return;
1625         }
1626
1627         CGoalSet *knownbehaviors=record->completedGoalSet();
1628         CGoalIterator *cit=knownbehaviors->iterator();
1629         uint numinputs=record->getNumFuncInputs();
1630         EPRecord * inputs[numinputs];
1631         for(uint i=0;i<numinputs;i++) {
1632                 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, i+VC_BASEINDEX);
1633                 ASSERT(depvec->size()==1);
1634                 inputs[i]=(*depvec)[0];
1635         }
1636         while(cit->hasNext()) {
1637                 CGoal *goal=cit->next();
1638                 Constraint *carray[numinputs];
1639                 if (record->isSharedGoals()) {
1640                         bool badvalue=false;
1641                         for(uint i=0;i<numinputs;i++) {
1642                                 uint64_t inputval=goal->getValue(i+VC_BASEINDEX);
1643                                 if (!record->getSet(i+VC_BASEINDEX)->contains(inputval)) {
1644                                         badvalue=true;
1645                                         break;
1646                                 }
1647                         }
1648                         if (badvalue)
1649                                 continue;
1650                 }
1651
1652                 /* Build up constraints for each input */
1653                 for(uint i=0;i<numinputs;i++) {
1654                         uint64_t inputval=goal->getValue(i+VC_BASEINDEX);
1655                         Constraint * inputc=getRetValueEncoding(inputs[i], inputval);
1656                         ASSERT(inputc!=NULL);
1657                         carray[i]=inputc;
1658                 }
1659                 Constraint * outputconstraint=getRetValueEncoding(record, goal->getOutput());
1660                 if (numinputs==0) {
1661                         ADDCONSTRAINT(outputconstraint,"functionimpl");
1662                 } else {
1663                         Constraint * functionimplication=new Constraint(IMPLIES, new Constraint(AND, numinputs, carray), outputconstraint);
1664                         ADDCONSTRAINT(functionimplication,"functionimpl");
1665                 }
1666         }
1667         delete cit;
1668
1669         FunctionRecord *fr=functiontable->get(record);
1670         Constraint *goal=fr->getNoValueEncoding();
1671         Constraint *newfunc=new Constraint(AND, goal, getExecutionConstraint(record));
1672         ADDGOAL(record, newfunc, "newfunc");
1673 }
1674
1675 void ConstGen::processEquals(EPRecord *record) {
1676         ASSERT (record->getNumFuncInputs() == 2);
1677         EPRecord * inputs[2];
1678
1679         for(uint i=0;i<2;i++) {
1680                 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, i+VC_BASEINDEX);
1681                 if (depvec==NULL) {
1682                         inputs[i]=NULL;
1683                 } else if (depvec->size()==1) {
1684                         inputs[i]=(*depvec)[0];
1685                 }       else ASSERT(false);
1686         }
1687
1688         //rely on this being a variable
1689         Constraint * outputtrue=getRetValueEncoding(record, 1);
1690         ASSERT(outputtrue->getType()==VAR);
1691
1692         if (inputs[0]!=NULL && inputs[1]!=NULL &&
1693                         (inputs[0]->getType()==LOAD || inputs[0]->getType()==RMW) &&
1694                         (inputs[1]->getType()==LOAD || inputs[1]->getType()==RMW) &&
1695                         (getStoreLoadSet(inputs[0])==getStoreLoadSet(inputs[1]))) {
1696                 StoreLoadSet * sls=getStoreLoadSet(inputs[0]);
1697                 int numvalvars=sls->getNumValVars();
1698                 Constraint **valvar1=(inputs[0]->getType()==RMW) ? sls->getRMWRValVars(this, inputs[0]) : sls->getValVars(this, inputs[0]);
1699                 Constraint **valvar2=(inputs[1]->getType()==RMW) ? sls->getRMWRValVars(this, inputs[1]) : sls->getValVars(this, inputs[1]);
1700                 //new test
1701
1702                 Constraint *vars[numvalvars];
1703                 for(int i=0;i<numvalvars;i++) {
1704                         vars[i]=getNewVar();
1705                         Constraint *var1=valvar1[i];
1706                         Constraint *var2=valvar2[i];
1707                         Constraint * array[]={var1, var2->negate(), vars[i]->negate()};
1708                         Constraint * array2[]={var2, var1->negate(), vars[i]->negate()};
1709                         Constraint * a=new Constraint(OR, 3, array);
1710                         ADDCONSTRAINT(a, "equala");
1711                         Constraint * a2=new Constraint(OR, 3, array2);
1712                         ADDCONSTRAINT(a2, "equala2");
1713                         Constraint * arrayb[]={var1, var2, vars[i]};
1714                         Constraint * array2b[]={var2->negate(), var1->negate(), vars[i]};
1715                         Constraint * b=new Constraint(OR, 3, arrayb);
1716                         ADDCONSTRAINT(b, "equalb");
1717                         Constraint *b2=new Constraint(OR, 3, array2b);
1718                         ADDCONSTRAINT(b2, "equalb2");
1719                 }
1720                 ADDCONSTRAINT(new Constraint(IMPLIES, new Constraint(AND, numvalvars, vars), outputtrue),"impequal1");
1721
1722                 ADDCONSTRAINT(new Constraint(IMPLIES, outputtrue, new Constraint(AND, numvalvars, vars)), "impequal2");
1723
1724                 /*
1725
1726                    Constraint * functionimplication=new Constraint(IMPLIES,generateEquivConstraint(numvalvars, valvar1, valvar2), outputtrue);
1727                    ADDCONSTRAINT(functionimplication,"equalsimplspecial");
1728                    Constraint * functionimplicationneg=new Constraint(IMPLIES,outputtrue, generateEquivConstraint(numvalvars, valvar1, valvar2));
1729                    ADDCONSTRAINT(functionimplicationneg,"equalsimplspecialneg");
1730                  */
1731                 return;
1732         }
1733
1734         if (inputs[0]==NULL && inputs[1]==NULL) {
1735                 IntIterator *iit0=record->getSet(VC_BASEINDEX+0)->iterator();
1736                 uint64_t constval=iit0->next();
1737                 delete iit0;
1738                 IntIterator *iit1=record->getSet(VC_BASEINDEX+1)->iterator();
1739                 uint64_t constval2=iit1->next();
1740                 delete iit1;
1741
1742                 if (constval==constval2) {
1743                         ADDCONSTRAINT(outputtrue, "equalsconst");
1744                 } else {
1745                         ADDCONSTRAINT(outputtrue->negate(), "equalsconst");
1746                 }
1747                 return;
1748         }
1749
1750         if (inputs[0]==NULL ||
1751                         inputs[1]==NULL) {
1752                 int nullindex=inputs[0]==NULL ? 0 : 1;
1753                 IntIterator *iit=record->getSet(VC_BASEINDEX+nullindex)->iterator();
1754                 uint64_t constval=iit->next();
1755                 delete iit;
1756
1757                 record->getSet(VC_BASEINDEX+nullindex);
1758                 EPRecord *r=inputs[1-nullindex];
1759                 Constraint *l=getRetValueEncoding(r, constval);
1760                 Constraint *functionimplication=new Constraint(IMPLIES, l, outputtrue);
1761                 ADDCONSTRAINT(functionimplication,"equalsimpl");
1762
1763                 Constraint *l2=getRetValueEncoding(r, constval);
1764                 Constraint *functionimplication2=new Constraint(IMPLIES, outputtrue, l2);
1765                 ADDCONSTRAINT(functionimplication2,"equalsimpl");
1766         }
1767
1768         IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
1769         while(iit->hasNext()) {
1770                 uint64_t val1=iit->next();
1771
1772                 IntIterator *iit2=record->getSet(VC_BASEINDEX+1)->iterator();
1773                 while(iit2->hasNext()) {
1774                         uint64_t val2=iit2->next();
1775                         Constraint *l=getRetValueEncoding(inputs[0], val1);
1776                         Constraint *r=getRetValueEncoding(inputs[1], val2);
1777                         Constraint *imp=(val1==val2) ? outputtrue : outputtrue->negate();
1778                         Constraint * functionimplication=new Constraint(IMPLIES, new Constraint(AND, l, r), imp);
1779                         ADDCONSTRAINT(functionimplication,"equalsimpl");
1780                 }
1781                 delete iit2;
1782         }
1783         delete iit;
1784 }
1785
1786 #ifdef TSO
1787 void ConstGen::processFence(EPRecord *record) {
1788         //do we already account for the fence?
1789         if (isAlwaysExecuted(record))
1790                 return;
1791         ExecPoint * record_ep=record->getEP();
1792         thread_id_t tid=record_ep->get_tid();
1793         uint thread=id_to_int(tid);
1794         ModelVector<EPRecord *> *tvec=(*threadactions)[thread];
1795         uint size=tvec->size();
1796
1797         EPRecord *prevstore=NULL;
1798         uint i;
1799         for(i=0;i<size;i++) {
1800                 EPRecord *rec=(*tvec)[i];
1801                 if (rec->getType()==STORE) {
1802                         prevstore=rec;
1803                 }
1804                 if (rec == record) {
1805                         i++;
1806                         break;
1807                 }
1808         }
1809         if (prevstore == NULL) {
1810                 return;
1811         }
1812         for(;i<size;i++) {
1813                 EPRecord *rec=(*tvec)[i];
1814                 if (rec->getType()==LOAD) {
1815                         Constraint * condition=getExecutionConstraint(record);
1816                         Constraint * storeload=getOrderConstraint(prevstore, rec);
1817                         Constraint * c=new Constraint(IMPLIES, condition, storeload);
1818                         ADDCONSTRAINT(c, "fence");
1819                         return;
1820                 }
1821         }
1822 }
1823 #endif
1824
1825 /** processRecord performs actions on second traversal of event
1826                 graph. */
1827
1828 void ConstGen::processRecord(EPRecord *record) {
1829         switch (record->getType()) {
1830         case FUNCTION:
1831                 processFunction(record);
1832                 break;
1833         case EQUALS:
1834                 processEquals(record);
1835                 break;
1836         case LOAD:
1837                 processLoad(record);
1838                 break;
1839         case STORE:
1840                 processStore(record);
1841                 break;
1842 #ifdef TSO
1843         case FENCE:
1844                 processFence(record);
1845                 break;
1846 #endif
1847         case RMW:
1848 #ifdef TSO
1849                 processFence(record);
1850 #endif
1851                 if (record->getOp()==ADD) {
1852                         processAdd(record);
1853                 } else if (record->getOp()==CAS) {
1854                         processCAS(record);
1855                 } else if (record->getOp()==EXC) {
1856                         processEXC(record);
1857                 } else
1858                         ASSERT(0);
1859                 break;
1860         case YIELD:
1861                 processYield(record);
1862                 break;
1863         case BRANCHDIR:
1864                 processBranch(record);
1865                 break;
1866         default:
1867                 break;
1868         }
1869 }
1870
1871 /** visitRecord performs actions done on first traversal of event
1872  *      graph. */
1873
1874 void ConstGen::visitRecord(EPRecord *record) {
1875         switch (record->getType()) {
1876         case EQUALS:
1877                 recordExecCond(record);
1878                 insertEquals(record);
1879                 break;
1880         case FUNCTION:
1881                 recordExecCond(record);
1882                 insertFunction(record);
1883                 break;
1884 #ifdef TSO
1885         case FENCE:
1886                 recordExecCond(record);
1887                 insertAction(record);
1888                 break;
1889 #endif
1890         case LOAD:
1891                 recordExecCond(record);
1892                 insertAction(record);
1893                 groupMemoryOperations(record);
1894                 break;
1895         case STORE:
1896                 recordExecCond(record);
1897                 insertAction(record);
1898                 groupMemoryOperations(record);
1899                 break;
1900         case RMW:
1901                 recordExecCond(record);
1902                 insertAction(record);
1903                 groupMemoryOperations(record);
1904                 break;
1905         case BRANCHDIR:
1906                 recordExecCond(record);
1907                 insertBranch(record);
1908                 break;
1909         case LOOPEXIT:
1910                 recordExecCond(record);
1911                 break;
1912         case NONLOCALTRANS:
1913                 recordExecCond(record);
1914                 insertNonLocal(record);
1915                 break;
1916         case LABEL:
1917                 insertLabel(record);
1918                 break;
1919         case YIELD:
1920                 recordExecCond(record);
1921                 break;
1922         default:
1923                 break;
1924         }
1925 }
1926
1927 void ConstGen::recordExecCond(EPRecord *record) {
1928         ExecPoint *eprecord=record->getEP();
1929         EPValue * branchval=record->getBranch();
1930         EPRecord * branch=(branchval==NULL) ? NULL : branchval->getRecord();
1931         ExecPoint *epbranch= (branch==NULL) ? NULL : branch->getEP();
1932         RecordSet *srs=NULL;
1933         RecordIterator *sri=nonlocaltrans->iterator();
1934         while(sri->hasNext()) {
1935                 EPRecord *nonlocal=sri->next();
1936                 ExecPoint *epnl=nonlocal->getEP();
1937                 if (epbranch!=NULL) {
1938                         if (epbranch->compare(epnl)==CR_BEFORE) {
1939                                 //branch occurs after non local and thus will subsume condition
1940                                 //branch subsumes this condition
1941                                 continue;
1942                         }
1943                 }
1944                 if (eprecord->compare(epnl)==CR_BEFORE) {
1945                         //record occurs after non-local, so add it to set
1946                         if (srs==NULL)
1947                                 srs=new RecordSet();
1948                         srs->add(nonlocal);
1949                 }
1950         }
1951         delete sri;
1952         if (srs!=NULL)
1953                 execcondtable->put(record, srs);
1954 }
1955
1956 void ConstGen::insertNonLocal(EPRecord *record) {
1957         nonlocaltrans->add(record);
1958 }
1959
1960 void ConstGen::insertLabel(EPRecord *record) {
1961         RecordIterator *sri=nonlocaltrans->iterator();
1962         while(sri->hasNext()) {
1963                 EPRecord *nonlocal=sri->next();
1964                 if (nonlocal->getNextRecord()==record)
1965                         sri->remove();
1966         }
1967
1968         delete sri;
1969 }
1970
1971 void ConstGen::traverseRecord(EPRecord *record, bool initial) {
1972         do {
1973                 if (initial) {
1974                         visitRecord(record);
1975                 } else {
1976                         processRecord(record);
1977                 }
1978                 if (record->getType()==LOOPENTER) {
1979                         if (record->getNextRecord()!=NULL)
1980                                 workstack->push_back(record->getNextRecord());
1981                         workstack->push_back(record->getChildRecord());
1982                         return;
1983                 }
1984                 if (record->getChildRecord()!=NULL) {
1985                         workstack->push_back(record->getChildRecord());
1986                 }
1987                 if (record->getType()==NONLOCALTRANS) {
1988                         return;
1989                 }
1990                 if (record->getType()==YIELD && model->params.noexecyields) {
1991                         return;
1992                 }
1993                 if (record->getType()==LOOPEXIT) {
1994                         return;
1995                 }
1996                 if (record->getType()==BRANCHDIR) {
1997                         EPRecord *next=record->getNextRecord();
1998                         if (next != NULL)
1999                                 workstack->push_back(next);
2000                         for(uint i=0;i<record->numValues();i++) {
2001                                 EPValue *branchdir=record->getValue(i);
2002
2003                                 //Could have an empty branch, so make sure the branch actually
2004                                 //runs code
2005                                 if (branchdir->getFirstRecord()!=NULL)
2006                                         workstack->push_back(branchdir->getFirstRecord());
2007                         }
2008                         return;
2009                 } else
2010                         record=record->getNextRecord();
2011         } while(record!=NULL);
2012 }
2013
2014 unsigned int RecPairHash(RecPair *rp) {
2015         uintptr_t v=(uintptr_t) rp->epr1;
2016         uintptr_t v2=(uintptr_t) rp->epr2;
2017         uintptr_t x=v^v2;
2018         uintptr_t a=v&v2;
2019         return (uint)((x>>4)^(a));
2020 }
2021
2022 bool RecPairEquals(RecPair *r1, RecPair *r2) {
2023         return ((r1->epr1==r2->epr1)&&(r1->epr2==r2->epr2)) ||
2024                                  ((r1->epr1==r2->epr2)&&(r1->epr2==r2->epr1));
2025 }