1 /* Copyright (c) 2015 Regents of the University of California
3 * Author: Brian Demsky <bdemsky@uci.edu>
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.
11 #include "mcexecution.h"
12 #include "constraint.h"
13 #include "branchrecord.h"
14 #include "functionrecord.h"
15 #include "equalsrecord.h"
16 #include "storeloadset.h"
18 #include "schedulebuilder.h"
23 #include "inc_solver.h"
28 gettimeofday(&tv, NULL);
29 return tv.tv_sec*1000000+tv.tv_usec;
32 ConstGen::ConstGen(MCExecution *e) :
33 storeloadtable(new StoreLoadSetHashTable()),
34 loadtable(new LoadHashTable()),
36 workstack(new ModelVector<EPRecord *>()),
37 threadactions(new ModelVector<ModelVector<EPRecord *> *>()),
38 rpt(new RecPairTable()),
40 goalset(new ModelVector<Constraint *>()),
42 vars(new ModelVector<Constraint *>()),
43 branchtable(new BranchTable()),
44 functiontable(new FunctionTable()),
45 equalstable(new EqualsTable()),
46 schedulebuilder(new ScheduleBuilder(e, this)),
47 nonlocaltrans(new RecordSet()),
48 execcondtable(new LoadHashTable()),
50 rectoint(new RecToIntTable()),
53 has_untaken_branches(false)
56 curr_stat=new MC_Stat();
58 curr_stat->was_incremental=false;
59 curr_stat->was_sat=true;
62 stats=new ModelVector<struct MC_Stat *>();
66 ConstGen::~ConstGen() {
70 for(uint i=0;i<vars->size();i++) {
71 Constraint *var=(*vars)[i];
72 Constraint *notvar=var->neg;
77 delete storeloadtable;
87 delete schedulebuilder;
93 void resetstoreloadtable(StoreLoadSetHashTable * storeloadtable) {
94 for(uint i=0;i<storeloadtable->capacity;i++) {
95 struct hashlistnode<const void *, StoreLoadSet *> * ptr=&storeloadtable->table[i];
96 if (ptr->val != NULL) {
97 if (ptr->val->removeAddress(ptr->key))
104 if (storeloadtable->zero != NULL) {
105 if (storeloadtable->zero->val->removeAddress(storeloadtable->zero->key)) {
106 delete storeloadtable->zero->val;
109 model_free(storeloadtable->zero);
110 storeloadtable->zero = NULL;
112 storeloadtable->size = 0;
115 void ConstGen::reset() {
116 for(uint i=0;i<threadactions->size();i++) {
117 delete (*threadactions)[i];
119 if (goalvararray != NULL) {
120 model_free(goalvararray);
123 functiontable->resetanddelete();
124 equalstable->resetanddelete();
125 branchtable->resetanddelete();
126 loadtable->resetanddelete();
127 execcondtable->resetanddelete();
128 rpt->resetanddelete();
129 resetstoreloadtable(storeloadtable);
130 nonlocaltrans->reset();
131 threadactions->clear();
136 has_untaken_branches=false;
139 void ConstGen::translateGoals() {
140 int size=goalset->size();
141 goalvararray=(Constraint **) model_malloc(size*sizeof(Constraint *));
143 for(int i=0;i<size;i++) {
144 Constraint *goal=(*goalset)[i];
145 goalvararray[i]=getNewVar();
146 addConstraint(new Constraint(OR, goalvararray[i]->negate(), goal));
148 Constraint *atleastonegoal=new Constraint(OR, size, goalvararray);
149 ADDCONSTRAINT(atleastonegoal, "atleastonegoal");
152 bool ConstGen::canReuseEncoding() {
155 Constraint *array[goalset->size()];
156 int remaininggoals=0;
158 //Zero out the achieved goals
159 for(uint i=0;i<goalset->size();i++) {
160 Constraint *var=goalvararray[i];
162 array[remaininggoals++]=var;
165 if (remaininggoals == 0)
167 Constraint *atleastonegoal=new Constraint(OR, remaininggoals, array);
168 ADDCONSTRAINT(atleastonegoal, "atleastonegoal");
169 solver->finishedClauses();
170 clock_t start=myclock();
171 bool *solution=runSolver();
172 clock_t finish=myclock();
174 if (curr_stat != NULL)
175 stats->push_back(curr_stat);
176 curr_stat=new MC_Stat();
177 curr_stat->time=finish-start;
178 curr_stat->was_incremental=true;
179 curr_stat->was_sat=(solution!=NULL);
183 model_print("start %lu, finish %lu\n", start,finish);
184 model_print("Incremental time = %12.6f\n", ((double)(finish-start))/1000000);
186 if (solution==NULL) {
190 //Zero out the achieved goals
191 for(uint i=0;i<goalset->size();i++) {
192 Constraint *var=goalvararray[i];
194 if (solution[var->getVar()]) {
195 //if (goalvararray[i] != NULL)
196 //model_print("SAT clearing goal %d.\n", i);
198 goalvararray[i]=NULL;
203 schedulebuilder->buildSchedule(solution);
204 model_free(solution);
209 bool ConstGen::process() {
210 #ifdef DUMP_EVENT_GRAPHS
214 if (solver != NULL) {
219 solver=new IncrementalSolver();
222 genTransOrderConstraints();
224 genTSOTransOrderConstraints();
228 if (goalset->size()==0) {
230 stats->push_back(curr_stat);
231 for(uint i=0;i<stats->size();i++) {
232 struct MC_Stat *s=(*stats)[i];
233 model_print("time=%lld fgoals=%d bgoals=%d incremental=%d sat=%d\n", s->time, s->fgoals, s->bgoals, s->was_incremental, s->was_sat);
236 model_print("No goals, done\n");
242 if (model->params.branches && !has_untaken_branches) {
248 solver->finishedClauses();
250 //Freeze the goal variables
251 for(uint i=0;i<goalset->size();i++) {
252 Constraint *var=goalvararray[i];
253 solver->freeze(var->getVar());
256 clock_t start=myclock();
257 bool *solution=runSolver();
258 clock_t finish=myclock();
260 if (curr_stat != NULL)
261 stats->push_back(curr_stat);
262 curr_stat=new MC_Stat();
263 curr_stat->time=finish-start;
264 curr_stat->was_incremental=false;
265 curr_stat->was_sat=(solution!=NULL);
269 if (solution == NULL) {
270 stats->push_back(curr_stat);
271 for(uint i=0;i<stats->size();i++) {
272 struct MC_Stat *s=(*stats)[i];
273 model_print("time=%lld fgoals=%d bgoals=%d incremental=%d sat=%d\n", s->time, s->fgoals, s->bgoals, s->was_incremental, s->was_sat);
279 model_print("start %lu, finish %lu\n", start,finish);
280 model_print("Initial time = %12.6f\n", ((double)(finish-start))/1000000);
283 if (solution==NULL) {
289 //Zero out the achieved goals
290 for(uint i=0;i<goalset->size();i++) {
291 Constraint *var=goalvararray[i];
293 if (solution[var->getVar()]) {
294 //if (goalvararray[i] != NULL)
295 // model_print("SAT clearing goal %d.\n", i);
296 goalvararray[i]=NULL;
301 schedulebuilder->buildSchedule(solution);
302 model_free(solution);
306 void ConstGen::printEventGraph() {
308 sprintf(buffer, "eventgraph%u.dot",schedule_graph);
310 int file=open(buffer,O_WRONLY|O_CREAT|O_TRUNC, S_IRWXU);
311 model_dprintf(file, "digraph eventgraph {\n");
313 EPRecord *first=execution->getEPRecord(MCID_FIRST);
314 printRecord(first, file);
315 while(!workstack->empty()) {
316 EPRecord *record=workstack->back();
317 workstack->pop_back();
318 printRecord(record, file);
321 model_dprintf(file, "}\n");
325 void ConstGen::doPrint(EPRecord *record, int file) {
326 model_dprintf(file, "%lu[label=\"",(uintptr_t)record);
328 model_dprintf(file, "\"];\n");
329 if (record->getNextRecord()!=NULL)
330 model_dprintf(file, "%lu->%lu;\n", (uintptr_t) record, (uintptr_t) record->getNextRecord());
332 if (record->getChildRecord()!=NULL)
333 model_dprintf(file, "%lu->%lu[color=red];\n", (uintptr_t) record, (uintptr_t) record->getChildRecord());
336 void ConstGen::printRecord(EPRecord *record, int file) {
338 doPrint(record,file);
340 if (record->getType()==LOOPENTER) {
341 workstack->push_back(record->getNextRecord());
342 workstack->push_back(record->getChildRecord());
345 if (record->getChildRecord()!=NULL) {
346 workstack->push_back(record->getChildRecord());
348 if (record->getType()==NONLOCALTRANS) {
351 if (record->getType()==LOOPEXIT) {
354 if (record->getType()==BRANCHDIR) {
355 EPRecord *next=record->getNextRecord();
357 workstack->push_back(next);
358 for(uint i=0;i<record->numValues();i++) {
359 EPValue *branchdir=record->getValue(i);
361 //Could have an empty branch, so make sure the branch actually
363 if (branchdir->getFirstRecord()!=NULL) {
364 workstack->push_back(branchdir->getFirstRecord());
365 model_dprintf(file, "%lu->%lu[color=blue];\n", (uintptr_t) record, (uintptr_t) branchdir->getFirstRecord());
370 record=record->getNextRecord();
371 } while(record!=NULL);
375 /* This function traverses a thread's graph in execution order. */
377 void ConstGen::traverse(bool initial) {
378 EPRecord *first=execution->getEPRecord(MCID_FIRST);
379 traverseRecord(first, initial);
380 while(!workstack->empty()) {
381 EPRecord *record=workstack->back();
382 workstack->pop_back();
383 traverseRecord(record, initial);
387 /** This method looks for all other memory operations that could
388 potentially share a location, and build partitions of memory
389 locations such that all memory locations that can share the same
390 address are in the same group.
392 These memory operations should share an encoding of addresses and
396 void ConstGen::groupMemoryOperations(EPRecord *op) {
397 /** Handle our first address */
398 IntHashSet *addrset=op->getSet(VC_ADDRINDEX);
399 IntIterator *ait=addrset->iterator();
401 void *iaddr=(void *) ait->next();
402 StoreLoadSet *isls=storeloadtable->get(iaddr);
404 isls=new StoreLoadSet();
405 storeloadtable->put(iaddr, isls);
409 while(ait->hasNext()) {
410 void *addr=(void *)ait->next();
411 StoreLoadSet *sls=storeloadtable->get(addr);
413 storeloadtable->put(addr, isls);
414 } else if (sls!=isls) {
416 mergeSets(isls, sls);
423 RecordSet * ConstGen::computeConflictSet(EPRecord *store, EPRecord *load, RecordSet * baseset) {
424 //See if we can determine addresses that store/load may use
425 IntIterator * storeaddr=store->getSet(VC_ADDRINDEX)->iterator();
426 int numaddr=0;void *commonaddr=NULL;
427 while(storeaddr->hasNext()) {
428 void *addr=(void *) storeaddr->next();
429 if (load->getSet(VC_ADDRINDEX)->contains((uint64_t)addr)) {
440 RecordSet *srscopy=baseset->copy();
441 RecordIterator *sri=srscopy->iterator();
442 while(sri->hasNext()) {
443 bool pruneconflictstore=false;
444 EPRecord *conflictstore=sri->next();
445 bool conflictafterstore=getOrderConstraint(store,conflictstore)->isTrue();
446 bool conflictbeforeload=getOrderConstraint(conflictstore,load)->isTrue();
448 if (conflictafterstore) {
449 RecordIterator *sricheck=srscopy->iterator();
450 while(sricheck->hasNext()) {
451 EPRecord *checkstore=sricheck->next();
452 bool checkafterstore=getOrderConstraint(store, checkstore)->isTrue();
453 if (!checkafterstore)
455 bool checkbeforeconflict=getOrderConstraint(checkstore,conflictstore)->isTrue();
456 if (!checkbeforeconflict)
459 //See if the checkstore must store to the relevant address
460 IntHashSet * storeaddr=checkstore->getSet(VC_ADDRINDEX);
462 if (storeaddr->getSize()!=1 || !storeaddr->contains((uint64_t)commonaddr))
466 if (subsumesExecutionConstraint(checkstore, conflictstore)) {
467 pruneconflictstore=true;
474 if (conflictbeforeload && !pruneconflictstore) {
475 RecordIterator *sricheck=srscopy->iterator();
476 while(sricheck->hasNext()) {
477 EPRecord *checkstore=sricheck->next();
479 bool checkafterconflict=getOrderConstraint(conflictstore, checkstore)->isTrue();
480 if (!checkafterconflict)
483 bool checkbeforeload=getOrderConstraint(checkstore, load)->isTrue();
484 if (!checkbeforeload)
487 //See if the checkstore must store to the relevant address
488 IntHashSet * storeaddr=checkstore->getSet(VC_ADDRINDEX);
489 if (storeaddr->getSize()!=1 || !storeaddr->contains((uint64_t)commonaddr))
493 if (subsumesExecutionConstraint(checkstore, conflictstore)) {
494 pruneconflictstore=true;
500 if (pruneconflictstore) {
501 //This store is redundant
511 /** This method returns all stores that a load may read from. */
513 RecordSet * ConstGen::getMayReadFromSet(EPRecord *load) {
514 if (load->getSet(VC_ADDRINDEX)->getSize()==1)
515 return getMayReadFromSetOpt(load);
517 RecordSet *srs=loadtable->get(load);
518 ExecPoint *epload=load->getEP();
519 thread_id_t loadtid=epload->get_tid();
522 loadtable->put(load, srs);
524 IntHashSet *addrset=load->getSet(VC_ADDRINDEX);
525 IntIterator *ait=addrset->iterator();
527 while(ait->hasNext()) {
528 void *addr=(void *)ait->next();
529 RecordSet *rs=execution->getStoreTable(addr);
533 RecordIterator * rit=rs->iterator();
534 while(rit->hasNext()) {
535 EPRecord *rec=rit->next();
536 ExecPoint *epstore=rec->getEP();
537 thread_id_t storetid=epstore->get_tid();
538 if (storetid != loadtid ||
539 epstore->compare(epload) == CR_AFTER)
550 RecordSet * ConstGen::getMayReadFromSetOpt(EPRecord *load) {
551 RecordSet *srs=loadtable->get(load);
552 ExecPoint *epload=load->getEP();
553 thread_id_t loadtid=epload->get_tid();
556 loadtable->put(load, srs);
558 IntHashSet *addrset=load->getSet(VC_ADDRINDEX);
559 IntIterator *ait=addrset->iterator();
560 void *addr=(void *)ait->next();
563 RecordSet *rs=execution->getStoreTable(addr);
564 RecordIterator * rit=rs->iterator();
565 ExecPoint *latest=NULL;
566 while(rit->hasNext()) {
567 EPRecord *store=rit->next();
568 ExecPoint *epstore=store->getEP();
569 thread_id_t storetid=epstore->get_tid();
570 if (storetid == loadtid && isAlwaysExecuted(store) &&
571 store->getSet(VC_ADDRINDEX)->getSize()==1 &&
572 epstore->compare(epload) == CR_AFTER &&
573 (latest==NULL || latest->compare(epstore) == CR_AFTER)) {
579 while(rit->hasNext()) {
580 EPRecord *store=rit->next();
581 ExecPoint *epstore=store->getEP();
582 thread_id_t storetid=epstore->get_tid();
583 if (storetid == loadtid) {
584 if (epstore->compare(epload) == CR_AFTER &&
585 (latest==NULL || epstore->compare(latest) != CR_AFTER))
596 /** This function merges two recordsets and updates the storeloadtable
599 void ConstGen::mergeSets(StoreLoadSet *to, StoreLoadSet *from) {
600 RecordIterator * sri=from->iterator();
601 while(sri->hasNext()) {
602 EPRecord *rec=sri->next();
604 IntHashSet *addrset=rec->getSet(VC_ADDRINDEX);
605 IntIterator *ait=addrset->iterator();
606 while(ait->hasNext()) {
607 void *addr=(void *)ait->next();
608 storeloadtable->put(addr, to);
617 /** This function creates ordering variables between stores and loads
618 * in same thread for TSO. */
620 void ConstGen::insertTSOAction(EPRecord *load) {
621 if (load->getType() != LOAD)
623 ExecPoint *load_ep=load->getEP();
624 thread_id_t tid=load_ep->get_tid();
625 uint thread=id_to_int(tid);
626 ModelVector<EPRecord *> * vector=(*threadactions)[thread];
627 uint j=vector->size()-1;
629 EPRecord *oldrec=(*vector)[--j];
630 EventType oldrec_t=oldrec->getType();
632 if (((oldrec_t == RMW) || (oldrec_t==FENCE)) &&
633 isAlwaysExecuted(oldrec)) {
635 } else if (oldrec_t == STORE) {
636 /* Only generate variables for things that can actually both run */
638 createOrderConstraint(oldrec, load);
643 void ConstGen::genTSOTransOrderConstraints() {
644 for(uint t1=0;t1<threadactions->size();t1++) {
645 ModelVector<EPRecord *> *tvec=(*threadactions)[t1];
646 uint size=tvec->size();
647 EPRecord *laststore=NULL;
648 for(uint store_i=0;store_i<size;store_i++) {
649 EPRecord *store=(*tvec)[store_i];
650 EventType store_t=store->getType();
651 if (store_t != STORE)
653 EPRecord *lastload=NULL;
654 for(uint load_i=store_i+1;load_i<size;load_i++) {
655 EPRecord *rec=(*tvec)[store_i];
656 //Hit fence, don't need more stuff
657 EventType rec_t=rec->getType();
658 if (((rec_t == RMW) || (rec_t == FENCE)) &&
659 isAlwaysExecuted(rec))
663 if (laststore != NULL) {
664 Constraint * storeload=getOrderConstraint(store, rec);
665 Constraint * earlystoreload=getOrderConstraint(laststore, rec);
666 Constraint * c=new Constraint(IMPLIES, storeload, earlystoreload);
667 ADDCONSTRAINT(c, "earlystore");
669 if (lastload != NULL) {
670 Constraint * storeearlyload=getOrderConstraint(store, lastload);
671 Constraint * storeload=getOrderConstraint(store, rec);
672 Constraint * c=new Constraint(IMPLIES, storeearlyload, storeload);
673 ADDCONSTRAINT(c, "earlyload");
683 /** This function creates ordering constraints to implement SC for
684 memory operations. */
686 void ConstGen::insertAction(EPRecord *record) {
687 thread_id_t tid=record->getEP()->get_tid();
688 uint thread=id_to_int(tid);
689 if (threadactions->size()<=thread) {
690 uint oldsize=threadactions->size();
691 threadactions->resize(thread+1);
692 for(;oldsize<=thread;oldsize++) {
693 (*threadactions)[oldsize]=new ModelVector<EPRecord *>();
697 (*threadactions)[thread]->push_back(record);
699 for(uint i=0;i<threadactions->size();i++) {
702 ModelVector<EPRecord *> * vector=(*threadactions)[i];
703 for(uint j=0;j<vector->size();j++) {
704 EPRecord *oldrec=(*vector)[j];
705 createOrderConstraint(oldrec, record);
709 insertTSOAction(record);
713 void ConstGen::genTransOrderConstraints() {
714 for(uint t1=0;t1<threadactions->size();t1++) {
715 ModelVector<EPRecord *> *t1vec=(*threadactions)[t1];
716 for(uint t2=0;t2<t1;t2++) {
717 ModelVector<EPRecord *> *t2vec=(*threadactions)[t2];
718 genTransOrderConstraints(t1vec, t2vec);
719 genTransOrderConstraints(t2vec, t1vec);
720 for(uint t3=0;t3<t2;t3++) {
721 ModelVector<EPRecord *> *t3vec=(*threadactions)[t3];
722 genTransOrderConstraints(t1vec, t2vec, t3vec);
728 void ConstGen::genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVector<EPRecord *> *t2vec) {
729 for(uint t1i=0;t1i<t1vec->size();t1i++) {
730 EPRecord *t1rec=(*t1vec)[t1i];
731 for(uint t2i=0;t2i<t2vec->size();t2i++) {
732 EPRecord *t2rec=(*t2vec)[t2i];
734 /* Note: One only really needs to generate the first constraint
735 in the first loop and the last constraint in the last loop.
736 I tried this and performance suffered on linuxrwlocks and
737 linuxlocks at the current time. BD - August 2014*/
738 Constraint *c21=getOrderConstraint(t2rec, t1rec);
740 /* short circuit for the trivial case */
744 for(uint t3i=t2i+1;t3i<t2vec->size();t3i++) {
745 EPRecord *t3rec=(*t2vec)[t3i];
746 Constraint *c13=getOrderConstraint(t1rec, t3rec);
748 Constraint *c32=getOrderConstraint(t3rec, t2rec);
749 if (!c32->isFalse()) {
750 //Have a store->load that could be reordered, need to generate other constraint
751 Constraint *c12=getOrderConstraint(t1rec, t2rec);
752 Constraint *c23=getOrderConstraint(t2rec, t3rec);
753 Constraint *c31=getOrderConstraint(t3rec, t1rec);
754 Constraint *slarray[] = {c31, c23, c12};
755 Constraint * intradelayedstore=new Constraint(OR, 3, slarray);
756 ADDCONSTRAINT(intradelayedstore, "intradelayedstore");
758 Constraint * array[]={c21, c32, c13};
759 Constraint *intratransorder=new Constraint(OR, 3, array);
761 Constraint *intratransorder=new Constraint(OR, c21, c13);
763 ADDCONSTRAINT(intratransorder,"intratransorder");
766 for(uint t0i=0;t0i<t1i;t0i++) {
767 EPRecord *t0rec=(*t1vec)[t0i];
768 Constraint *c02=getOrderConstraint(t0rec, t2rec);
770 Constraint *c10=getOrderConstraint(t1rec, t0rec);
772 if (!c10->isFalse()) {
773 //Have a store->load that could be reordered, need to generate other constraint
774 Constraint *c01=getOrderConstraint(t0rec, t1rec);
775 Constraint *c12=getOrderConstraint(t1rec, t2rec);
776 Constraint *c20=getOrderConstraint(t2rec, t0rec);
777 Constraint *slarray[] = {c01, c12, c20};
778 Constraint * intradelayedstore=new Constraint(OR, 3, slarray);
779 ADDCONSTRAINT(intradelayedstore, "intradelayedstore");
781 Constraint * array[]={c10, c21, c02};
782 Constraint *intratransorder=new Constraint(OR, 3, array);
784 Constraint *intratransorder=new Constraint(OR, c21, c02);
786 ADDCONSTRAINT(intratransorder,"intratransorder");
793 void ConstGen::genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVector<EPRecord *> *t2vec, ModelVector<EPRecord *> * t3vec) {
794 for(uint t1i=0;t1i<t1vec->size();t1i++) {
795 EPRecord *t1rec=(*t1vec)[t1i];
796 for(uint t2i=0;t2i<t2vec->size();t2i++) {
797 EPRecord *t2rec=(*t2vec)[t2i];
798 for(uint t3i=0;t3i<t3vec->size();t3i++) {
799 EPRecord *t3rec=(*t3vec)[t3i];
800 genTransOrderConstraint(t1rec, t2rec, t3rec);
806 void ConstGen::genTransOrderConstraint(EPRecord *t1rec, EPRecord *t2rec, EPRecord *t3rec) {
807 Constraint *c21=getOrderConstraint(t2rec, t1rec);
808 Constraint *c32=getOrderConstraint(t3rec, t2rec);
809 Constraint *c13=getOrderConstraint(t1rec, t3rec);
810 Constraint * cimpl1[]={c21, c32, c13};
811 Constraint * c1=new Constraint(OR, 3, cimpl1);
812 ADDCONSTRAINT(c1, "intertransorder");
814 Constraint *c12=getOrderConstraint(t1rec, t2rec);
815 Constraint *c23=getOrderConstraint(t2rec, t3rec);
816 Constraint *c31=getOrderConstraint(t3rec, t1rec);
817 Constraint * cimpl2[]={c12, c23, c31};
818 Constraint *c2=new Constraint(OR, 3, cimpl2);
819 ADDCONSTRAINT(c2, "intertransorder");
822 void ConstGen::addGoal(EPRecord *r, Constraint *c) {
823 rectoint->put(r, goalset->size());
824 goalset->push_back(c);
827 void ConstGen::addBranchGoal(EPRecord *r, Constraint *c) {
828 has_untaken_branches=true;
829 rectoint->put(r, goalset->size());
830 goalset->push_back(c);
833 void ConstGen::achievedGoal(EPRecord *r) {
834 if (rectoint->contains(r)) {
835 uint index=rectoint->get(r);
836 //if (goalvararray[index] != NULL)
837 //model_print("Run Clearing goal index %d\n",index);
838 goalvararray[index]=NULL;
842 void ConstGen::addConstraint(Constraint *c) {
843 ModelVector<Constraint *> *vec=c->simplify();
844 for(uint i=0;i<vec->size();i++) {
845 Constraint *simp=(*vec)[i];
846 if (simp->type==TRUE)
848 ASSERT(simp->type!=FALSE);
849 simp->printDIMACS(this);
850 #ifdef VERBOSE_CONSTRAINTS
860 void ConstGen::printNegConstraint(uint value) {
862 solver->addClauseLiteral(val);
865 void ConstGen::printConstraint(uint value) {
866 solver->addClauseLiteral(value);
869 bool * ConstGen::runSolver() {
870 int solution=solver->solve();
871 if (solution == IS_UNSAT) {
873 } else if (solution == IS_SAT) {
874 bool * assignments=(bool *)model_malloc(sizeof(bool)*(varindex+1));
875 for(uint i=0;i<=varindex;i++)
876 assignments[i]=solver->getValue(i);
881 model_print_err("INDETER\n");
882 model_print("INDETER\n");
888 Constraint * ConstGen::getOrderConstraint(EPRecord *first, EPRecord *second) {
890 if (first->getEP()->get_tid()==second->getEP()->get_tid()) {
891 if (first->getEP()->compare(second->getEP())==CR_AFTER)
898 RecPair rp(first, second);
899 RecPair *rpc=rpt->get(&rp);
902 first->getEP()->get_tid()==second->getEP()->get_tid()) {
903 if (first->getEP()->compare(second->getEP())==CR_AFTER)
912 Constraint *c=rpc->constraint;
913 if (rpc->epr1!=first) {
914 //have to flip arguments
921 bool ConstGen::getOrder(EPRecord *first, EPRecord *second, bool * satsolution) {
922 RecPair rp(first, second);
923 RecPair *rpc=rpt->get(&rp);
926 first->getEP()->get_tid()==second->getEP()->get_tid()) {
927 if (first->getEP()->compare(second->getEP())==CR_AFTER)
937 Constraint *c=rpc->constraint;
938 CType type=c->getType();
943 else if (type==FALSE)
946 uint index=c->getVar();
947 order=satsolution[index];
949 if (rpc->epr1==first)
955 /** This function determines whether events first and second are
956 * ordered by start and join operations. */
958 bool ConstGen::orderThread(EPRecord *first, EPRecord *second) {
959 ExecPoint * ep1=first->getEP();
960 ExecPoint * ep2=second->getEP();
961 thread_id_t thr1=ep1->get_tid();
962 thread_id_t thr2=ep2->get_tid();
963 Thread *tr2=execution->get_thread(thr2);
964 EPRecord *thr2start=tr2->getParentRecord();
965 if (thr2start!=NULL) {
966 ExecPoint *epthr2start=thr2start->getEP();
967 if (epthr2start->get_tid()==thr1 &&
968 ep1->compare(epthr2start)==CR_AFTER)
971 ModelVector<EPRecord *> * joinvec=execution->getJoins();
972 for(uint i=0;i<joinvec->size();i++) {
973 EPRecord *join=(*joinvec)[i];
974 ExecPoint *jp=join->getEP();
975 if (jp->get_tid()==thr2 &&
976 jp->compare(ep2)==CR_AFTER)
982 /** This function generates an ordering constraint for two events. */
984 void ConstGen::createOrderConstraint(EPRecord *first, EPRecord *second) {
985 RecPair * rp=new RecPair(first, second);
986 if (!rpt->contains(rp)) {
987 if (orderThread(first, second))
988 rp->constraint=&ctrue;
989 else if (orderThread(second, first))
990 rp->constraint=&cfalse;
992 rp->constraint=getNewVar();
1000 Constraint * ConstGen::getNewVar() {
1002 if (varindex>vars->size()) {
1003 var=new Constraint(VAR, varindex);
1004 Constraint *varneg=new Constraint(NOTVAR, varindex);
1005 var->setNeg(varneg);
1006 varneg->setNeg(var);
1007 vars->push_back(var);
1009 var=(*vars)[varindex-1];
1015 /** Gets an array of new variables. */
1017 void ConstGen::getArrayNewVars(uint num, Constraint **carray) {
1018 for(uint i=0;i<num;i++)
1019 carray[i]=getNewVar();
1022 StoreLoadSet * ConstGen::getStoreLoadSet(EPRecord *record) {
1023 IntIterator *it=record->getSet(VC_ADDRINDEX)->iterator();
1024 void *addr=(void *)it->next();
1026 return storeloadtable->get(addr);
1029 /** Returns a constraint that is true if the output of record has the
1032 Constraint * ConstGen::getRetValueEncoding(EPRecord *record, uint64_t value) {
1033 switch(record->getType()) {
1035 return equalstable->get(record)->getValueEncoding(value);
1037 return functiontable->get(record)->getValueEncoding(value);
1039 return getStoreLoadSet(record)->getValueEncoding(this, record, value);
1042 return getStoreLoadSet(record)->getRMWRValueEncoding(this, record, value);
1050 Constraint * ConstGen::getMemValueEncoding(EPRecord *record, uint64_t value) {
1051 switch(record->getType()) {
1053 return getStoreLoadSet(record)->getValueEncoding(this, record, value);
1055 return getStoreLoadSet(record)->getValueEncoding(this, record, value);
1062 /** Return true if the execution of record implies the execution of
1065 bool ConstGen::subsumesExecutionConstraint(EPRecord *recordsubsumes, EPRecord *record) {
1066 EPValue *branch=record->getBranch();
1067 EPValue *branchsubsumes=recordsubsumes->getBranch();
1068 if (branchsubsumes != NULL) {
1069 bool branchsubsumed=false;
1070 while(branch!=NULL) {
1071 if (branchsubsumes==branch) {
1072 branchsubsumed=true;
1075 branch=branch->getRecord()->getBranch();
1077 if (!branchsubsumed)
1080 RecordSet *srs=execcondtable->get(recordsubsumes);
1083 RecordIterator *sri=srs->iterator();
1084 while(sri->hasNext()) {
1085 EPRecord *rec=sri->next();
1087 if (!getOrderConstraint(rec, record)->isTrue()) {
1097 Constraint * ConstGen::getExecutionConstraint(EPRecord *record) {
1098 EPValue *branch=record->getBranch();
1099 RecordSet *srs=execcondtable->get(record);
1100 int size=srs==NULL ? 0 : srs->getSize();
1104 Constraint *array[size];
1107 RecordIterator *sri=srs->iterator();
1108 while(sri->hasNext()) {
1109 EPRecord *rec=sri->next();
1110 EPValue *recbranch=rec->getBranch();
1111 BranchRecord *guardbr=branchtable->get(recbranch->getRecord());
1112 array[index++]=guardbr->getBranch(recbranch)->negate();
1117 BranchRecord *guardbr=branchtable->get(branch->getRecord());
1118 array[index++]=guardbr->getBranch(branch);
1125 return new Constraint(AND, index, array);
1128 bool ConstGen::isAlwaysExecuted(EPRecord *record) {
1129 EPValue *branch=record->getBranch();
1130 RecordSet *srs=execcondtable->get(record);
1131 int size=srs==NULL ? 0 : srs->getSize();
1138 void ConstGen::insertBranch(EPRecord *record) {
1139 uint numvalue=record->numValues();
1140 /** need one value for new directions */
1141 if (numvalue<record->getLen())
1143 /** need extra value to represent that branch wasn't executed. **/
1144 bool alwaysexecuted=isAlwaysExecuted(record);
1145 if (!alwaysexecuted)
1147 uint numbits=NUMBITS(numvalue-1);
1148 Constraint *bits[numbits];
1149 getArrayNewVars(numbits, bits);
1150 BranchRecord *br=new BranchRecord(record, numbits, bits, alwaysexecuted);
1151 branchtable->put(record, br);
1154 void ConstGen::processBranch(EPRecord *record) {
1155 BranchRecord *br=branchtable->get(record);
1156 if (record->numValues()<record->getLen()) {
1157 Constraint *goal=br->getNewBranch();
1158 ADDBRANCHGOAL(record, goal,"newbranch");
1161 /** Insert criteria of parent branch going the right way. **/
1162 Constraint *baseconstraint=getExecutionConstraint(record);
1164 if (!isAlwaysExecuted(record)) {
1165 Constraint *parentbranch=new Constraint(IMPLIES, br->getAnyBranch(), baseconstraint);
1166 ADDCONSTRAINT(parentbranch, "parentbranch");
1169 /** Insert criteria for directions */
1170 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1171 ASSERT(depvec->size()==1);
1172 EPRecord * val_record=(*depvec)[0];
1173 for(unsigned int i=0;i<record->numValues();i++) {
1174 EPValue * branchval=record->getValue(i);
1175 uint64_t val=branchval->getValue();
1178 Constraint *execconstraint=getExecutionConstraint(record);
1179 Constraint *br_false=new Constraint(IMPLIES,
1180 new Constraint(AND, execconstraint,
1181 getRetValueEncoding(val_record, val)), br->getBranch(branchval));
1182 ADDCONSTRAINT(br_false, "br_false");
1184 if (record->getBranchAnyValue()) {
1185 if (getRetValueEncoding(val_record, 0)!=NULL) {
1186 Constraint *execconstraint=getExecutionConstraint(record);
1187 Constraint *br_true1=new Constraint(IMPLIES, new Constraint(AND, getRetValueEncoding(val_record, 0)->negate(),
1189 br->getBranch(branchval));
1190 ADDCONSTRAINT(br_true1, "br_true1");
1192 for(unsigned int j=0;j<val_record->numValues();j++) {
1193 EPValue * epval=val_record->getValue(j);
1194 Constraint *execconstraint=getExecutionConstraint(record);
1195 Constraint *valuematches=getRetValueEncoding(val_record, epval->getValue());
1196 Constraint *br_true2=new Constraint(IMPLIES, new Constraint(AND, execconstraint, valuematches), br->getBranch(branchval));
1197 ADDCONSTRAINT(br_true2, "br_true2");
1201 Constraint *execconstraint=getExecutionConstraint(record);
1202 Constraint *br_val=new Constraint(IMPLIES, new Constraint(AND, execconstraint, getRetValueEncoding(val_record, val)), br->getBranch(branchval));
1203 ADDCONSTRAINT(br_val, "br_val");
1209 void ConstGen::insertFunction(EPRecord *record) {
1210 FunctionRecord * fr=new FunctionRecord(this, record);
1211 functiontable->put(record, fr);
1214 void ConstGen::insertEquals(EPRecord *record) {
1215 EqualsRecord * fr=new EqualsRecord(this, record);
1216 equalstable->put(record, fr);
1219 void ConstGen::processLoad(EPRecord *record) {
1220 LoadRF * lrf=new LoadRF(record, this);
1221 lrf->genConstraints(this);
1223 processAddresses(record);
1226 /** This procedure generates the constraints that set the address
1227 variables for load/store/rmw operations. */
1229 void ConstGen::processAddresses(EPRecord *record) {
1230 StoreLoadSet *sls=getStoreLoadSet(record);
1231 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_ADDRINDEX);
1233 //we have a hard coded address
1234 const void *addr=record->getValue(0)->getAddr();
1235 Constraint *addrenc=sls->getAddressEncoding(this, record, addr);
1236 ADDCONSTRAINT(addrenc,"fixedaddress");
1238 //we take as input an address and have to generate implications
1239 //for each possible input address
1240 ASSERT(depvec->size()==1);
1241 EPRecord *src=(*depvec)[0];
1242 IntIterator *it=record->getSet(VC_ADDRINDEX)->iterator();
1244 uintptr_t offset=record->getOffset();
1246 while(it->hasNext()) {
1247 uint64_t addr=it->next();
1248 Constraint *srcenc=getRetValueEncoding(src, addr-offset);
1249 Constraint *addrenc=sls->getAddressEncoding(this, record, (void *) addr);
1250 Constraint *addrmatch=new Constraint(IMPLIES, srcenc, addrenc);
1251 ADDCONSTRAINT(addrmatch,"setaddress");
1257 void ConstGen::processCAS(EPRecord *record) {
1259 LoadRF * lrf=new LoadRF(record, this);
1260 lrf->genConstraints(this);
1262 //Next see if we are successful
1263 Constraint *eq=getNewVar();
1264 ModelVector<EPRecord *> * depveccas=execution->getRevDependences(record, VC_OLDVALCASINDEX);
1265 if (depveccas==NULL) {
1266 //Hard coded old value
1267 IntIterator *iit=record->getSet(VC_OLDVALCASINDEX)->iterator();
1268 uint64_t valcas=iit->next();
1270 Constraint *rmwr=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, valcas);
1272 Constraint *cascond=eq->negate();
1273 ADDCONSTRAINT(cascond, "cascond");
1275 Constraint *cascond=generateEquivConstraint(eq, rmwr);
1276 ADDCONSTRAINT(cascond, "cascond");
1279 ASSERT(depveccas->size()==1);
1280 EPRecord *src=(*depveccas)[0];
1281 IntIterator *it=getStoreLoadSet(record)->getValues()->iterator();
1283 while(it->hasNext()) {
1284 uint64_t valcas=it->next();
1285 Constraint *srcenc=getRetValueEncoding(src, valcas);
1286 Constraint *storeenc=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, valcas);
1288 if (srcenc!=NULL && storeenc!=NULL) {
1289 Constraint *cond=new Constraint(AND,
1290 new Constraint(IMPLIES, srcenc->clone(), eq),
1291 new Constraint(IMPLIES, eq, srcenc));
1292 Constraint *cas=new Constraint(IMPLIES, storeenc, cond);
1293 ADDCONSTRAINT(cas, "cas");
1294 } else if (srcenc==NULL) {
1295 Constraint *casfail=new Constraint(IMPLIES, storeenc, eq->negate());
1296 ADDCONSTRAINT(casfail,"casfail_eq");
1298 //srcenc must be non-null and store-encoding must be null
1303 IntIterator *iit=record->getSet(VC_OLDVALCASINDEX)->iterator();
1304 while(iit->hasNext()) {
1305 uint64_t val=iit->next();
1306 if (!getStoreLoadSet(record)->getValues()->contains(val)) {
1307 Constraint *srcenc=getRetValueEncoding(src, val);
1308 Constraint *casfail=new Constraint(IMPLIES, srcenc, eq->negate());
1309 ADDCONSTRAINT(casfail,"casfailretval");
1315 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1317 IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
1318 uint64_t val=iit->next();
1320 Constraint *storeenc=getMemValueEncoding(record, val);
1321 Constraint *casmemsuc=new Constraint(IMPLIES, eq, storeenc);
1322 ADDCONSTRAINT(casmemsuc, "casmemsuc");
1324 ASSERT(depvec->size()==1);
1325 EPRecord *src=(*depvec)[0];
1326 IntIterator *it=record->getStoreSet()->iterator();
1328 while(it->hasNext()) {
1329 uint64_t val=it->next();
1330 Constraint *srcenc=getRetValueEncoding(src, val);
1332 //this can happen for values that are in the store set because
1333 //we re-stored them on a failed CAS
1336 Constraint *storeenc=getMemValueEncoding(record, val);
1337 Constraint *storevalue=new Constraint(IMPLIES, new Constraint(AND, eq, srcenc), storeenc);
1338 ADDCONSTRAINT(storevalue,"casmemsuc");
1342 StoreLoadSet *sls=getStoreLoadSet(record);
1344 Constraint *repeatval=generateEquivConstraint(sls->getNumValVars(), sls->getValVars(this, record), sls->getRMWRValVars(this, record));
1345 Constraint *failcas=new Constraint(IMPLIES, eq->negate(), repeatval);
1346 ADDCONSTRAINT(failcas,"casmemfail");
1348 processAddresses(record);
1351 void ConstGen::processEXC(EPRecord *record) {
1353 LoadRF * lrf=new LoadRF(record, this);
1354 lrf->genConstraints(this);
1357 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1359 IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
1360 uint64_t val=iit->next();
1362 Constraint *storeenc=getMemValueEncoding(record, val);
1363 ADDCONSTRAINT(storeenc, "excmemsuc");
1365 ASSERT(depvec->size()==1);
1366 EPRecord *src=(*depvec)[0];
1367 IntIterator *it=record->getStoreSet()->iterator();
1369 while(it->hasNext()) {
1370 uint64_t val=it->next();
1371 Constraint *srcenc=getRetValueEncoding(src, val);
1372 Constraint *storeenc=getMemValueEncoding(record, val);
1373 Constraint *storevalue=new Constraint(IMPLIES, srcenc, storeenc);
1374 ADDCONSTRAINT(storevalue,"excmemsuc");
1379 processAddresses(record);
1382 void ConstGen::processAdd(EPRecord *record) {
1384 LoadRF * lrf=new LoadRF(record, this);
1385 lrf->genConstraints(this);
1387 Constraint *var=getNewVar();
1388 Constraint *newadd=new Constraint(AND, var, getExecutionConstraint(record));
1389 ADDGOAL(record, newadd, "newadd");
1391 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1393 IntIterator *valit=record->getSet(VC_BASEINDEX)->iterator();
1394 uint64_t val=valit->next();
1396 IntHashSet *valset=getStoreLoadSet(record)->getValues();
1397 IntIterator *sis=valset->iterator();
1398 while(sis->hasNext()) {
1399 uint64_t memval=sis->next();
1400 uint64_t sumval=(memval+val)&getmask(record->getLen());
1402 if (valset->contains(sumval)) {
1404 Constraint *loadenc=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, memval);
1405 Constraint *storeenc=getMemValueEncoding(record, sumval);
1406 Constraint *notvar=var->negate();
1407 Constraint *addinputfix=new Constraint(IMPLIES, loadenc, new Constraint(AND, storeenc, notvar));
1408 ADDCONSTRAINT(addinputfix, "addinputfix");
1414 ASSERT(depvec->size()==1);
1415 EPRecord *src=(*depvec)[0];
1416 IntIterator *it=record->getStoreSet()->iterator();
1417 IntHashSet *valset=getStoreLoadSet(record)->getValues();
1419 while(it->hasNext()) {
1420 uint64_t val=it->next();
1421 IntIterator *sis=valset->iterator();
1422 while(sis->hasNext()) {
1423 uint64_t memval=sis->next();
1424 uint64_t sum=(memval+val)&getmask(record->getLen());
1425 if (valset->contains(sum)) {
1426 Constraint *srcenc=getRetValueEncoding(src, val);
1427 Constraint *loadenc=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, memval);
1428 Constraint *storeenc=getMemValueEncoding(record, sum);
1429 Constraint *notvar=var->negate();
1430 Constraint *addop=new Constraint(IMPLIES, new Constraint(AND, srcenc, loadenc),
1431 new Constraint(AND, notvar, storeenc));
1432 ADDCONSTRAINT(addop,"addinputvar");
1440 processAddresses(record);
1443 /** This function ensures that the value of a store's SAT variables
1444 matches the store's input value.
1446 TODO: Could optimize the case where the encodings are the same...
1449 void ConstGen::processStore(EPRecord *record) {
1450 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1452 //We have a hard coded value
1453 uint64_t val=record->getValue(0)->getValue();
1454 Constraint *storeenc=getMemValueEncoding(record, val);
1455 ADDCONSTRAINT(storeenc,"storefix");
1457 //We have a value from an input
1458 ASSERT(depvec->size()==1);
1459 EPRecord *src=(*depvec)[0];
1460 IntIterator *it=record->getStoreSet()->iterator();
1462 while(it->hasNext()) {
1463 uint64_t val=it->next();
1464 Constraint *srcenc=getRetValueEncoding(src, val);
1465 Constraint *storeenc=getMemValueEncoding(record, val);
1466 Constraint *storevalue=new Constraint(IMPLIES, srcenc, storeenc);
1467 ADDCONSTRAINT(storevalue,"storevar");
1471 processAddresses(record);
1474 /** Handle yields by just forbidding them via the SAT formula. */
1476 void ConstGen::processYield(EPRecord *record) {
1477 if (model->params.noyields &&
1478 record->getBranch()!=NULL) {
1479 Constraint * noyield=getExecutionConstraint(record)->negate();
1480 ADDCONSTRAINT(noyield, "noyield");
1484 void ConstGen::processLoopPhi(EPRecord *record) {
1485 EPRecordIDSet *phiset=record->getPhiLoopTable();
1486 EPRecordIDIterator *rit=phiset->iterator();
1488 while(rit->hasNext()) {
1489 struct RecordIDPair *rip=rit->next();
1490 EPRecord *input=rip->idrecord;
1492 IntIterator * it=record->getSet(VC_BASEINDEX)->iterator();
1493 while(it->hasNext()) {
1494 uint64_t value=it->next();
1495 Constraint * inputencoding=getRetValueEncoding(input, value);
1496 if (inputencoding==NULL)
1498 Constraint * branchconstraint=getExecutionConstraint(rip->record);
1499 Constraint * outputencoding=getRetValueEncoding(record, value);
1500 Constraint * phiimplication=new Constraint(IMPLIES, new Constraint(AND, inputencoding, branchconstraint), outputencoding);
1501 ADDCONSTRAINT(phiimplication,"philoop");
1508 void ConstGen::processPhi(EPRecord *record) {
1509 ModelVector<EPRecord *> * inputs=execution->getRevDependences(record, VC_BASEINDEX);
1510 for(uint i=0;i<inputs->size();i++) {
1511 EPRecord * input=(*inputs)[i];
1513 IntIterator * it=record->getSet(VC_BASEINDEX)->iterator();
1514 while(it->hasNext()) {
1515 uint64_t value=it->next();
1516 Constraint * inputencoding=getRetValueEncoding(input, value);
1517 if (inputencoding==NULL)
1519 Constraint * branchconstraint=getExecutionConstraint(input);
1520 Constraint * outputencoding=getRetValueEncoding(record, value);
1521 Constraint * phiimplication=new Constraint(IMPLIES, new Constraint(AND, inputencoding, branchconstraint), outputencoding);
1522 ADDCONSTRAINT(phiimplication,"phi");
1528 void ConstGen::processFunction(EPRecord *record) {
1529 if (record->getLoopPhi()) {
1530 processLoopPhi(record);
1532 } else if (record->getPhi()) {
1537 CGoalSet *knownbehaviors=record->completedGoalSet();
1538 CGoalIterator *cit=knownbehaviors->iterator();
1539 uint numinputs=record->getNumFuncInputs();
1540 EPRecord * inputs[numinputs];
1541 for(uint i=0;i<numinputs;i++) {
1542 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, i+VC_BASEINDEX);
1543 ASSERT(depvec->size()==1);
1544 inputs[i]=(*depvec)[0];
1546 while(cit->hasNext()) {
1547 CGoal *goal=cit->next();
1548 Constraint *carray[numinputs];
1549 if (record->isSharedGoals()) {
1550 bool badvalue=false;
1551 for(uint i=0;i<numinputs;i++) {
1552 uint64_t inputval=goal->getValue(i+VC_BASEINDEX);
1553 if (!record->getSet(i+VC_BASEINDEX)->contains(inputval)) {
1562 /* Build up constraints for each input */
1563 for(uint i=0;i<numinputs;i++) {
1564 uint64_t inputval=goal->getValue(i+VC_BASEINDEX);
1565 Constraint * inputc=getRetValueEncoding(inputs[i], inputval);
1566 ASSERT(inputc!=NULL);
1569 Constraint * outputconstraint=getRetValueEncoding(record, goal->getOutput());
1571 ADDCONSTRAINT(outputconstraint,"functionimpl");
1573 Constraint * functionimplication=new Constraint(IMPLIES, new Constraint(AND, numinputs, carray), outputconstraint);
1574 ADDCONSTRAINT(functionimplication,"functionimpl");
1579 FunctionRecord *fr=functiontable->get(record);
1580 Constraint *goal=fr->getNoValueEncoding();
1581 Constraint *newfunc=new Constraint(AND, goal, getExecutionConstraint(record));
1582 ADDGOAL(record, newfunc, "newfunc");
1585 void ConstGen::processEquals(EPRecord *record) {
1586 ASSERT (record->getNumFuncInputs() == 2);
1587 EPRecord * inputs[2];
1589 for(uint i=0;i<2;i++) {
1590 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, i+VC_BASEINDEX);
1593 } else if (depvec->size()==1) {
1594 inputs[i]=(*depvec)[0];
1595 } else ASSERT(false);
1598 //rely on this being a variable
1599 Constraint * outputtrue=getRetValueEncoding(record, 1);
1600 ASSERT(outputtrue->getType()==VAR);
1602 if (inputs[0]!=NULL && inputs[1]!=NULL &&
1603 (inputs[0]->getType()==LOAD || inputs[0]->getType()==RMW) &&
1604 (inputs[1]->getType()==LOAD || inputs[1]->getType()==RMW) &&
1605 (getStoreLoadSet(inputs[0])==getStoreLoadSet(inputs[1]))) {
1606 StoreLoadSet * sls=getStoreLoadSet(inputs[0]);
1607 int numvalvars=sls->getNumValVars();
1608 Constraint **valvar1=(inputs[0]->getType()==RMW) ? sls->getRMWRValVars(this, inputs[0]) : sls->getValVars(this, inputs[0]);
1609 Constraint **valvar2=(inputs[1]->getType()==RMW) ? sls->getRMWRValVars(this, inputs[1]) : sls->getValVars(this, inputs[1]);
1612 Constraint *vars[numvalvars];
1613 for(int i=0;i<numvalvars;i++) {
1614 vars[i]=getNewVar();
1615 Constraint *var1=valvar1[i];
1616 Constraint *var2=valvar2[i];
1617 Constraint * array[]={var1, var2->negate(), vars[i]->negate()};
1618 Constraint * array2[]={var2, var1->negate(), vars[i]->negate()};
1619 Constraint * a=new Constraint(OR, 3, array);
1620 ADDCONSTRAINT(a, "equala");
1621 Constraint * a2=new Constraint(OR, 3, array2);
1622 ADDCONSTRAINT(a2, "equala2");
1623 Constraint * arrayb[]={var1, var2, vars[i]};
1624 Constraint * array2b[]={var2->negate(), var1->negate(), vars[i]};
1625 Constraint * b=new Constraint(OR, 3, arrayb);
1626 ADDCONSTRAINT(b, "equalb");
1627 Constraint *b2=new Constraint(OR, 3, array2b);
1628 ADDCONSTRAINT(b2, "equalb2");
1630 ADDCONSTRAINT(new Constraint(IMPLIES, new Constraint(AND, numvalvars, vars), outputtrue),"impequal1");
1632 ADDCONSTRAINT(new Constraint(IMPLIES, outputtrue, new Constraint(AND, numvalvars, vars)), "impequal2");
1636 Constraint * functionimplication=new Constraint(IMPLIES,generateEquivConstraint(numvalvars, valvar1, valvar2), outputtrue);
1637 ADDCONSTRAINT(functionimplication,"equalsimplspecial");
1638 Constraint * functionimplicationneg=new Constraint(IMPLIES,outputtrue, generateEquivConstraint(numvalvars, valvar1, valvar2));
1639 ADDCONSTRAINT(functionimplicationneg,"equalsimplspecialneg");
1644 if (inputs[0]==NULL && inputs[1]==NULL) {
1645 IntIterator *iit0=record->getSet(VC_BASEINDEX+0)->iterator();
1646 uint64_t constval=iit0->next();
1648 IntIterator *iit1=record->getSet(VC_BASEINDEX+1)->iterator();
1649 uint64_t constval2=iit1->next();
1652 if (constval==constval2) {
1653 ADDCONSTRAINT(outputtrue, "equalsconst");
1655 ADDCONSTRAINT(outputtrue->negate(), "equalsconst");
1660 if (inputs[0]==NULL ||
1662 int nullindex=inputs[0]==NULL ? 0 : 1;
1663 IntIterator *iit=record->getSet(VC_BASEINDEX+nullindex)->iterator();
1664 uint64_t constval=iit->next();
1667 record->getSet(VC_BASEINDEX+nullindex);
1668 EPRecord *r=inputs[1-nullindex];
1669 Constraint *l=getRetValueEncoding(r, constval);
1670 Constraint *functionimplication=new Constraint(IMPLIES, l, outputtrue);
1671 ADDCONSTRAINT(functionimplication,"equalsimpl");
1673 Constraint *l2=getRetValueEncoding(r, constval);
1674 Constraint *functionimplication2=new Constraint(IMPLIES, outputtrue, l2);
1675 ADDCONSTRAINT(functionimplication2,"equalsimpl");
1678 IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
1679 while(iit->hasNext()) {
1680 uint64_t val1=iit->next();
1682 IntIterator *iit2=record->getSet(VC_BASEINDEX+1)->iterator();
1683 while(iit2->hasNext()) {
1684 uint64_t val2=iit2->next();
1685 Constraint *l=getRetValueEncoding(inputs[0], val1);
1686 Constraint *r=getRetValueEncoding(inputs[1], val2);
1687 Constraint *imp=(val1==val2) ? outputtrue : outputtrue->negate();
1688 Constraint * functionimplication=new Constraint(IMPLIES, new Constraint(AND, l, r), imp);
1689 ADDCONSTRAINT(functionimplication,"equalsimpl");
1697 void ConstGen::processFence(EPRecord *record) {
1698 //do we already account for the fence?
1699 if (isAlwaysExecuted(record))
1701 ExecPoint * record_ep=record->getEP();
1702 thread_id_t tid=record_ep->get_tid();
1703 uint thread=id_to_int(tid);
1704 ModelVector<EPRecord *> *tvec=(*threadactions)[thread];
1705 uint size=tvec->size();
1707 EPRecord *prevstore=NULL;
1709 for(i=0;i<size;i++) {
1710 EPRecord *rec=(*tvec)[i];
1711 if (rec->getType()==STORE) {
1714 if (rec == record) {
1719 if (prevstore == NULL) {
1723 EPRecord *rec=(*tvec)[i];
1724 if (rec->getType()==LOAD) {
1725 Constraint * condition=getExecutionConstraint(record);
1726 Constraint * storeload=getOrderConstraint(prevstore, rec);
1727 Constraint * c=new Constraint(IMPLIES, condition, storeload);
1728 ADDCONSTRAINT(c, "fence");
1735 void ConstGen::processRecord(EPRecord *record) {
1736 switch (record->getType()) {
1738 processFunction(record);
1741 processEquals(record);
1744 processLoad(record);
1747 processStore(record);
1751 processFence(record);
1756 processFence(record);
1758 if (record->getOp()==ADD) {
1760 } else if (record->getOp()==CAS) {
1762 } else if (record->getOp()==EXC) {
1768 processYield(record);
1771 processBranch(record);
1778 void ConstGen::visitRecord(EPRecord *record) {
1779 switch (record->getType()) {
1781 recordExecCond(record);
1782 insertEquals(record);
1785 recordExecCond(record);
1786 insertFunction(record);
1790 recordExecCond(record);
1791 insertAction(record);
1795 recordExecCond(record);
1796 insertAction(record);
1797 groupMemoryOperations(record);
1800 recordExecCond(record);
1801 insertAction(record);
1802 groupMemoryOperations(record);
1805 recordExecCond(record);
1806 insertAction(record);
1807 groupMemoryOperations(record);
1810 recordExecCond(record);
1811 insertBranch(record);
1814 recordExecCond(record);
1817 recordExecCond(record);
1818 insertNonLocal(record);
1821 insertLabel(record);
1824 recordExecCond(record);
1831 void ConstGen::recordExecCond(EPRecord *record) {
1832 ExecPoint *eprecord=record->getEP();
1833 EPValue * branchval=record->getBranch();
1834 EPRecord * branch=(branchval==NULL) ? NULL : branchval->getRecord();
1835 ExecPoint *epbranch= (branch==NULL) ? NULL : branch->getEP();
1836 RecordSet *srs=NULL;
1837 RecordIterator *sri=nonlocaltrans->iterator();
1838 while(sri->hasNext()) {
1839 EPRecord *nonlocal=sri->next();
1840 ExecPoint *epnl=nonlocal->getEP();
1841 if (epbranch!=NULL) {
1842 if (epbranch->compare(epnl)==CR_BEFORE) {
1843 //branch occurs after non local and thus will subsume condition
1844 //branch subsumes this condition
1848 if (eprecord->compare(epnl)==CR_BEFORE) {
1849 //record occurs after non-local, so add it to set
1851 srs=new RecordSet();
1857 execcondtable->put(record, srs);
1860 void ConstGen::insertNonLocal(EPRecord *record) {
1861 nonlocaltrans->add(record);
1864 void ConstGen::insertLabel(EPRecord *record) {
1865 RecordIterator *sri=nonlocaltrans->iterator();
1866 while(sri->hasNext()) {
1867 EPRecord *nonlocal=sri->next();
1868 if (nonlocal->getNextRecord()==record)
1875 void ConstGen::traverseRecord(EPRecord *record, bool initial) {
1878 visitRecord(record);
1880 processRecord(record);
1882 if (record->getType()==LOOPENTER) {
1883 workstack->push_back(record->getNextRecord());
1884 workstack->push_back(record->getChildRecord());
1887 if (record->getChildRecord()!=NULL) {
1888 workstack->push_back(record->getChildRecord());
1890 if (record->getType()==NONLOCALTRANS) {
1893 if (record->getType()==LOOPEXIT) {
1896 if (record->getType()==BRANCHDIR) {
1897 EPRecord *next=record->getNextRecord();
1899 workstack->push_back(next);
1900 for(uint i=0;i<record->numValues();i++) {
1901 EPValue *branchdir=record->getValue(i);
1903 //Could have an empty branch, so make sure the branch actually
1905 if (branchdir->getFirstRecord()!=NULL)
1906 workstack->push_back(branchdir->getFirstRecord());
1910 record=record->getNextRecord();
1911 } while(record!=NULL);
1914 unsigned int RecPairHash(RecPair *rp) {
1915 uintptr_t v=(uintptr_t) rp->epr1;
1916 uintptr_t v2=(uintptr_t) rp->epr2;
1919 return (uint)((x>>4)^(a));
1922 bool RecPairEquals(RecPair *r1, RecPair *r2) {
1923 return ((r1->epr1==r2->epr1)&&(r1->epr2==r2->epr2)) ||
1924 ((r1->epr1==r2->epr2)&&(r1->epr2==r2->epr1));