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 *>()),
41 yieldlist(new ModelVector<EPRecord *>()),
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()),
52 rectoint(new RecToIntTable()),
53 yieldtable(new RecToConsTable()),
56 has_untaken_branches(false)
59 curr_stat=new MC_Stat();
61 curr_stat->was_incremental=false;
62 curr_stat->was_sat=true;
65 stats=new ModelVector<struct MC_Stat *>();
69 ConstGen::~ConstGen() {
73 for(uint i=0;i<vars->size();i++) {
74 Constraint *var=(*vars)[i];
75 Constraint *notvar=var->neg;
80 delete storeloadtable;
91 delete schedulebuilder;
93 delete incompleteexploredbranch;
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))
110 if (storeloadtable->zero != NULL) {
111 if (storeloadtable->zero->val->removeAddress(storeloadtable->zero->key)) {
112 delete storeloadtable->zero->val;
115 model_free(storeloadtable->zero);
116 storeloadtable->zero = NULL;
118 storeloadtable->size = 0;
121 void ConstGen::reset() {
122 for(uint i=0;i<threadactions->size();i++) {
123 delete (*threadactions)[i];
125 if (goalvararray != NULL) {
126 model_free(goalvararray);
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();
145 has_untaken_branches=false;
148 void ConstGen::translateGoals() {
149 int size=goalset->size();
150 goalvararray=(Constraint **) model_malloc(size*sizeof(Constraint *));
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));
157 Constraint *atleastonegoal=new Constraint(OR, size, goalvararray);
158 ADDCONSTRAINT(atleastonegoal, "atleastonegoal");
161 bool ConstGen::canReuseEncoding() {
164 Constraint *array[goalset->size()];
165 int remaininggoals=0;
167 //Zero out the achieved goals
168 for(uint i=0;i<goalset->size();i++) {
169 Constraint *var=goalvararray[i];
171 array[remaininggoals++]=var;
174 if (remaininggoals == 0)
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();
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);
192 model_print("start %lu, finish %lu\n", start,finish);
193 model_print("Incremental time = %12.6f\n", ((double)(finish-start))/1000000);
195 if (solution==NULL) {
199 //Zero out the achieved goals
200 for(uint i=0;i<goalset->size();i++) {
201 Constraint *var=goalvararray[i];
203 if (solution[var->getVar()]) {
204 //if (goalvararray[i] != NULL)
205 //model_print("SAT clearing goal %d.\n", i);
207 goalvararray[i]=NULL;
212 schedulebuilder->buildSchedule(solution);
213 model_free(solution);
218 bool ConstGen::process() {
219 #ifdef DUMP_EVENT_GRAPHS
223 if (solver != NULL) {
228 solver=new IncrementalSolver();
231 genTransOrderConstraints();
233 genTSOTransOrderConstraints();
237 if (goalset->size()==0) {
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);
245 model_print("No goals, done\n");
251 if (model->params.branches && !has_untaken_branches) {
257 solver->finishedClauses();
259 //Freeze the goal variables
260 for(uint i=0;i<goalset->size();i++) {
261 Constraint *var=goalvararray[i];
262 solver->freeze(var->getVar());
265 clock_t start=myclock();
266 bool *solution=runSolver();
267 clock_t finish=myclock();
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);
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);
288 model_print("start %lu, finish %lu\n", start,finish);
289 model_print("Initial time = %12.6f\n", ((double)(finish-start))/1000000);
292 if (solution==NULL) {
298 //Zero out the achieved goals
299 for(uint i=0;i<goalset->size();i++) {
300 Constraint *var=goalvararray[i];
302 if (solution[var->getVar()]) {
303 //if (goalvararray[i] != NULL)
304 // model_print("SAT clearing goal %d.\n", i);
305 goalvararray[i]=NULL;
310 schedulebuilder->buildSchedule(solution);
311 model_free(solution);
315 void ConstGen::printEventGraph() {
317 sprintf(buffer, "eventgraph%u.dot",schedule_graph);
319 int file=open(buffer,O_WRONLY|O_CREAT|O_TRUNC, S_IRWXU);
320 model_dprintf(file, "digraph eventgraph {\n");
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);
330 model_dprintf(file, "}\n");
334 void ConstGen::doPrint(EPRecord *record, int file) {
335 model_dprintf(file, "%lu[label=\"",(uintptr_t)record);
337 model_dprintf(file, "\"];\n");
338 if (record->getNextRecord()!=NULL)
339 model_dprintf(file, "%lu->%lu;\n", (uintptr_t) record, (uintptr_t) record->getNextRecord());
341 if (record->getChildRecord()!=NULL)
342 model_dprintf(file, "%lu->%lu[color=red];\n", (uintptr_t) record, (uintptr_t) record->getChildRecord());
345 void ConstGen::printRecord(EPRecord *record, int file) {
347 doPrint(record,file);
349 if (record->getType()==LOOPENTER) {
350 if (record->getNextRecord()!=NULL)
351 workstack->push_back(record->getNextRecord());
352 workstack->push_back(record->getChildRecord());
355 if (record->getChildRecord()!=NULL) {
356 workstack->push_back(record->getChildRecord());
358 if (record->getType()==NONLOCALTRANS) {
361 if (record->getType()==LOOPEXIT) {
364 if (record->getType()==BRANCHDIR) {
365 EPRecord *next=record->getNextRecord();
367 workstack->push_back(next);
368 for(uint i=0;i<record->numValues();i++) {
369 EPValue *branchdir=record->getValue(i);
371 //Could have an empty branch, so make sure the branch actually
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());
380 record=record->getNextRecord();
381 } while(record!=NULL);
385 /* This function traverses a thread's graph in execution order. */
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);
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.
402 These memory operations should share an encoding of addresses and
406 void ConstGen::groupMemoryOperations(EPRecord *op) {
407 /** Handle our first address */
408 IntHashSet *addrset=op->getSet(VC_ADDRINDEX);
409 IntIterator *ait=addrset->iterator();
411 void *iaddr=(void *) ait->next();
412 StoreLoadSet *isls=storeloadtable->get(iaddr);
414 isls=new StoreLoadSet();
415 storeloadtable->put(iaddr, isls);
419 while(ait->hasNext()) {
420 void *addr=(void *)ait->next();
421 StoreLoadSet *sls=storeloadtable->get(addr);
423 storeloadtable->put(addr, isls);
424 } else if (sls!=isls) {
426 mergeSets(isls, sls);
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)) {
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();
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)
465 bool checkbeforeconflict=getOrderConstraint(checkstore,conflictstore)->isTrue();
466 if (!checkbeforeconflict)
469 //See if the checkstore must store to the relevant address
470 IntHashSet * storeaddr=checkstore->getSet(VC_ADDRINDEX);
472 if (storeaddr->getSize()!=1 || !storeaddr->contains((uint64_t)commonaddr))
476 if (subsumesExecutionConstraint(checkstore, conflictstore)) {
477 pruneconflictstore=true;
484 if (conflictbeforeload && !pruneconflictstore) {
485 RecordIterator *sricheck=srscopy->iterator();
486 while(sricheck->hasNext()) {
487 EPRecord *checkstore=sricheck->next();
489 bool checkafterconflict=getOrderConstraint(conflictstore, checkstore)->isTrue();
490 if (!checkafterconflict)
493 bool checkbeforeload=getOrderConstraint(checkstore, load)->isTrue();
494 if (!checkbeforeload)
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))
503 if (subsumesExecutionConstraint(checkstore, conflictstore)) {
504 pruneconflictstore=true;
510 if (pruneconflictstore) {
511 //This store is redundant
521 /** This method returns all stores that a load may read from. */
523 RecordSet * ConstGen::getMayReadFromSet(EPRecord *load) {
524 if (load->getSet(VC_ADDRINDEX)->getSize()==1)
525 return getMayReadFromSetOpt(load);
527 RecordSet *srs=loadtable->get(load);
528 ExecPoint *epload=load->getEP();
529 thread_id_t loadtid=epload->get_tid();
532 loadtable->put(load, srs);
534 IntHashSet *addrset=load->getSet(VC_ADDRINDEX);
535 IntIterator *ait=addrset->iterator();
537 while(ait->hasNext()) {
538 void *addr=(void *)ait->next();
539 RecordSet *rs=execution->getStoreTable(addr);
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)
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();
566 loadtable->put(load, srs);
568 IntHashSet *addrset=load->getSet(VC_ADDRINDEX);
569 IntIterator *ait=addrset->iterator();
570 void *addr=(void *)ait->next();
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)) {
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))
606 /** This function merges two recordsets and updates the storeloadtable
609 void ConstGen::mergeSets(StoreLoadSet *to, StoreLoadSet *from) {
610 RecordIterator * sri=from->iterator();
611 while(sri->hasNext()) {
612 EPRecord *rec=sri->next();
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);
627 /** This function creates ordering variables between stores and loads
628 * in same thread for TSO. */
630 void ConstGen::insertTSOAction(EPRecord *load) {
631 if (load->getType() != LOAD)
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;
639 EPRecord *oldrec=(*vector)[--j];
640 EventType oldrec_t=oldrec->getType();
642 if (((oldrec_t == RMW) || (oldrec_t==FENCE)) &&
643 isAlwaysExecuted(oldrec)) {
645 } else if (oldrec_t == STORE) {
646 /* Only generate variables for things that can actually both run */
648 createOrderConstraint(oldrec, load);
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)
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))
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");
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");
693 /** This function creates ordering constraints to implement SC for
694 memory operations. */
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 *>();
707 (*threadactions)[thread]->push_back(record);
709 for(uint i=0;i<threadactions->size();i++) {
712 ModelVector<EPRecord *> * vector=(*threadactions)[i];
713 for(uint j=0;j<vector->size();j++) {
714 EPRecord *oldrec=(*vector)[j];
715 createOrderConstraint(oldrec, record);
719 insertTSOAction(record);
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);
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];
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);
750 /* short circuit for the trivial case */
754 for(uint t3i=t2i+1;t3i<t2vec->size();t3i++) {
755 EPRecord *t3rec=(*t2vec)[t3i];
756 Constraint *c13=getOrderConstraint(t1rec, t3rec);
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");
768 Constraint * array[]={c21, c32, c13};
769 Constraint *intratransorder=new Constraint(OR, 3, array);
771 Constraint *intratransorder=new Constraint(OR, c21, c13);
773 ADDCONSTRAINT(intratransorder,"intratransorder");
776 for(uint t0i=0;t0i<t1i;t0i++) {
777 EPRecord *t0rec=(*t1vec)[t0i];
778 Constraint *c02=getOrderConstraint(t0rec, t2rec);
780 Constraint *c10=getOrderConstraint(t1rec, t0rec);
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");
791 Constraint * array[]={c10, c21, c02};
792 Constraint *intratransorder=new Constraint(OR, 3, array);
794 Constraint *intratransorder=new Constraint(OR, c21, c02);
796 ADDCONSTRAINT(intratransorder,"intratransorder");
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);
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");
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");
832 void ConstGen::addGoal(EPRecord *r, Constraint *c) {
833 rectoint->put(r, goalset->size());
834 goalset->push_back(c);
837 void ConstGen::addBranchGoal(EPRecord *r, Constraint *c) {
838 has_untaken_branches=true;
839 rectoint->put(r, goalset->size());
840 goalset->push_back(c);
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;
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)
858 ASSERT(simp->type!=FALSE);
859 simp->printDIMACS(this);
860 #ifdef VERBOSE_CONSTRAINTS
870 void ConstGen::printNegConstraint(uint value) {
872 solver->addClauseLiteral(val);
875 void ConstGen::printConstraint(uint value) {
876 solver->addClauseLiteral(value);
879 bool * ConstGen::runSolver() {
880 int solution=solver->solve();
881 if (solution == IS_UNSAT) {
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);
891 model_print_err("INDETER\n");
892 model_print("INDETER\n");
898 Constraint * ConstGen::getOrderConstraint(EPRecord *first, EPRecord *second) {
900 if (first->getEP()->get_tid()==second->getEP()->get_tid()) {
901 if (first->getEP()->compare(second->getEP())==CR_AFTER)
908 RecPair rp(first, second);
909 RecPair *rpc=rpt->get(&rp);
912 first->getEP()->get_tid()==second->getEP()->get_tid()) {
913 if (first->getEP()->compare(second->getEP())==CR_AFTER)
922 Constraint *c=rpc->constraint;
923 if (rpc->epr1!=first) {
924 //have to flip arguments
931 bool ConstGen::getOrder(EPRecord *first, EPRecord *second, bool * satsolution) {
932 RecPair rp(first, second);
933 RecPair *rpc=rpt->get(&rp);
936 first->getEP()->get_tid()==second->getEP()->get_tid()) {
937 if (first->getEP()->compare(second->getEP())==CR_AFTER)
947 Constraint *c=rpc->constraint;
948 CType type=c->getType();
953 else if (type==FALSE)
956 uint index=c->getVar();
957 order=satsolution[index];
959 if (rpc->epr1==first)
965 /** This function determines whether events first and second are
966 * ordered by start and join operations. */
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)
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)
992 /** This function generates an ordering constraint for two events. */
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;
1002 rp->constraint=getNewVar();
1010 Constraint * ConstGen::getNewVar() {
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);
1019 var=(*vars)[varindex-1];
1025 /** Gets an array of new variables. */
1027 void ConstGen::getArrayNewVars(uint num, Constraint **carray) {
1028 for(uint i=0;i<num;i++)
1029 carray[i]=getNewVar();
1032 StoreLoadSet * ConstGen::getStoreLoadSet(EPRecord *record) {
1033 IntIterator *it=record->getSet(VC_ADDRINDEX)->iterator();
1034 void *addr=(void *)it->next();
1036 return storeloadtable->get(addr);
1039 /** Returns a constraint that is true if the output of record has the
1042 Constraint * ConstGen::getRetValueEncoding(EPRecord *record, uint64_t value) {
1043 switch(record->getType()) {
1045 return equalstable->get(record)->getValueEncoding(value);
1047 return functiontable->get(record)->getValueEncoding(value);
1049 return getStoreLoadSet(record)->getValueEncoding(this, record, value);
1052 return getStoreLoadSet(record)->getRMWRValueEncoding(this, record, value);
1060 Constraint * ConstGen::getMemValueEncoding(EPRecord *record, uint64_t value) {
1061 switch(record->getType()) {
1063 return getStoreLoadSet(record)->getValueEncoding(this, record, value);
1065 return getStoreLoadSet(record)->getValueEncoding(this, record, value);
1072 /** Return true if the execution of record implies the execution of
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;
1085 branch=branch->getRecord()->getBranch();
1087 if (!branchsubsumed)
1090 RecordSet *srs=execcondtable->get(recordsubsumes);
1093 RecordIterator *sri=srs->iterator();
1094 while(sri->hasNext()) {
1095 EPRecord *rec=sri->next();
1097 if (!getOrderConstraint(rec, record)->isTrue()) {
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();
1114 Constraint *array[size];
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();
1127 BranchRecord *guardbr=branchtable->get(branch->getRecord());
1128 array[index++]=guardbr->getBranch(branch);
1135 return new Constraint(AND, index, array);
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();
1148 void ConstGen::insertBranch(EPRecord *record) {
1149 uint numvalue=record->numValues();
1150 /** need one value for new directions */
1151 if (numvalue<record->getLen()) {
1153 if (model->params.noexecyields) {
1154 incompleteexploredbranch->add(record);
1157 /** need extra value to represent that branch wasn't executed. **/
1158 bool alwaysexecuted=isAlwaysExecuted(record);
1159 if (!alwaysexecuted)
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);
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");
1175 /** Insert criteria of parent branch going the right way. **/
1176 Constraint *baseconstraint=getExecutionConstraint(record);
1178 if (!isAlwaysExecuted(record)) {
1179 Constraint *parentbranch=new Constraint(IMPLIES, br->getAnyBranch(), baseconstraint);
1180 ADDCONSTRAINT(parentbranch, "parentbranch");
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();
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");
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(),
1203 br->getBranch(branchval));
1204 ADDCONSTRAINT(br_true1, "br_true1");
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");
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");
1223 void ConstGen::insertFunction(EPRecord *record) {
1224 FunctionRecord * fr=new FunctionRecord(this, record);
1225 functiontable->put(record, fr);
1228 void ConstGen::insertEquals(EPRecord *record) {
1229 EqualsRecord * fr=new EqualsRecord(this, record);
1230 equalstable->put(record, fr);
1233 void ConstGen::processLoad(EPRecord *record) {
1234 LoadRF * lrf=new LoadRF(record, this);
1235 lrf->genConstraints(this);
1237 processAddresses(record);
1240 /** This procedure generates the constraints that set the address
1241 variables for load/store/rmw operations. */
1243 void ConstGen::processAddresses(EPRecord *record) {
1244 StoreLoadSet *sls=getStoreLoadSet(record);
1245 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_ADDRINDEX);
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");
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();
1258 uintptr_t offset=record->getOffset();
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");
1271 void ConstGen::processCAS(EPRecord *record) {
1273 LoadRF * lrf=new LoadRF(record, this);
1274 lrf->genConstraints(this);
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();
1284 Constraint *rmwr=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, valcas);
1286 Constraint *cascond=eq->negate();
1287 ADDCONSTRAINT(cascond, "cascond");
1289 Constraint *cascond=generateEquivConstraint(eq, rmwr);
1290 ADDCONSTRAINT(cascond, "cascond");
1293 ASSERT(depveccas->size()==1);
1294 EPRecord *src=(*depveccas)[0];
1295 IntIterator *it=getStoreLoadSet(record)->getValues()->iterator();
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);
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");
1312 //srcenc must be non-null and store-encoding must be null
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");
1329 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1331 IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
1332 uint64_t val=iit->next();
1334 Constraint *storeenc=getMemValueEncoding(record, val);
1335 Constraint *casmemsuc=new Constraint(IMPLIES, eq, storeenc);
1336 ADDCONSTRAINT(casmemsuc, "casmemsuc");
1338 ASSERT(depvec->size()==1);
1339 EPRecord *src=(*depvec)[0];
1340 IntIterator *it=record->getStoreSet()->iterator();
1342 while(it->hasNext()) {
1343 uint64_t val=it->next();
1344 Constraint *srcenc=getRetValueEncoding(src, val);
1346 //this can happen for values that are in the store set because
1347 //we re-stored them on a failed CAS
1350 Constraint *storeenc=getMemValueEncoding(record, val);
1351 Constraint *storevalue=new Constraint(IMPLIES, new Constraint(AND, eq, srcenc), storeenc);
1352 ADDCONSTRAINT(storevalue,"casmemsuc");
1356 StoreLoadSet *sls=getStoreLoadSet(record);
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");
1362 processAddresses(record);
1365 void ConstGen::processEXC(EPRecord *record) {
1367 LoadRF * lrf=new LoadRF(record, this);
1368 lrf->genConstraints(this);
1371 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1373 IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
1374 uint64_t val=iit->next();
1376 Constraint *storeenc=getMemValueEncoding(record, val);
1377 ADDCONSTRAINT(storeenc, "excmemsuc");
1379 ASSERT(depvec->size()==1);
1380 EPRecord *src=(*depvec)[0];
1381 IntIterator *it=record->getStoreSet()->iterator();
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");
1393 processAddresses(record);
1396 void ConstGen::processAdd(EPRecord *record) {
1398 LoadRF * lrf=new LoadRF(record, this);
1399 lrf->genConstraints(this);
1401 Constraint *var=getNewVar();
1402 Constraint *newadd=new Constraint(AND, var, getExecutionConstraint(record));
1403 ADDGOAL(record, newadd, "newadd");
1405 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1407 IntIterator *valit=record->getSet(VC_BASEINDEX)->iterator();
1408 uint64_t val=valit->next();
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());
1416 if (valset->contains(sumval)) {
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");
1428 ASSERT(depvec->size()==1);
1429 EPRecord *src=(*depvec)[0];
1430 IntIterator *it=record->getStoreSet()->iterator();
1431 IntHashSet *valset=getStoreLoadSet(record)->getValues();
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");
1454 processAddresses(record);
1457 /** This function ensures that the value of a store's SAT variables
1458 matches the store's input value.
1460 TODO: Could optimize the case where the encodings are the same...
1463 void ConstGen::processStore(EPRecord *record) {
1464 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
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");
1471 //We have a value from an input
1472 ASSERT(depvec->size()==1);
1473 EPRecord *src=(*depvec)[0];
1474 IntIterator *it=record->getStoreSet()->iterator();
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");
1485 processAddresses(record);
1490 void ConstGen::computeYieldCond(EPRecord *record) {
1491 ExecPoint *yieldep=record->getEP();
1492 EPRecord *prevyield=NULL;
1493 ExecPoint *prevyieldep=NULL;
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) {
1503 prevyieldep=prevyield->getEP();
1508 yieldlist->push_back(record);
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()) {
1520 if (yieldep->compare(branchep)!=CR_BEFORE) {
1521 //Branch does not occur before yield, so skip
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
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);
1537 int num_constraints=((prevyield==NULL)?0:1)+novel_branches->size();
1538 Constraint *carray[num_constraints];
1541 if (prevyield!=NULL) {
1542 carray[arr_index++]=yieldtable->get(prevyield);//get constraint for old yield
1544 for(uint i=0;i<novel_branches->size();i++) {
1545 carray[arr_index++]=(*novel_branches)[i];
1548 Constraint *cor=num_constraints!=0?new Constraint(OR, num_constraints, carray):&cfalse;
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);
1557 delete novel_branches;
1562 /** Handle yields by just forbidding them via the SAT formula. */
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");
1574 void ConstGen::processLoopPhi(EPRecord *record) {
1575 EPRecordIDSet *phiset=record->getPhiLoopTable();
1576 EPRecordIDIterator *rit=phiset->iterator();
1578 while(rit->hasNext()) {
1579 struct RecordIDPair *rip=rit->next();
1580 EPRecord *input=rip->idrecord;
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)
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");
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];
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)
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");
1618 void ConstGen::processFunction(EPRecord *record) {
1619 if (record->getLoopPhi()) {
1620 processLoopPhi(record);
1622 } else if (record->getPhi()) {
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];
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)) {
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);
1659 Constraint * outputconstraint=getRetValueEncoding(record, goal->getOutput());
1661 ADDCONSTRAINT(outputconstraint,"functionimpl");
1663 Constraint * functionimplication=new Constraint(IMPLIES, new Constraint(AND, numinputs, carray), outputconstraint);
1664 ADDCONSTRAINT(functionimplication,"functionimpl");
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");
1675 void ConstGen::processEquals(EPRecord *record) {
1676 ASSERT (record->getNumFuncInputs() == 2);
1677 EPRecord * inputs[2];
1679 for(uint i=0;i<2;i++) {
1680 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, i+VC_BASEINDEX);
1683 } else if (depvec->size()==1) {
1684 inputs[i]=(*depvec)[0];
1685 } else ASSERT(false);
1688 //rely on this being a variable
1689 Constraint * outputtrue=getRetValueEncoding(record, 1);
1690 ASSERT(outputtrue->getType()==VAR);
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]);
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");
1720 ADDCONSTRAINT(new Constraint(IMPLIES, new Constraint(AND, numvalvars, vars), outputtrue),"impequal1");
1722 ADDCONSTRAINT(new Constraint(IMPLIES, outputtrue, new Constraint(AND, numvalvars, vars)), "impequal2");
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");
1734 if (inputs[0]==NULL && inputs[1]==NULL) {
1735 IntIterator *iit0=record->getSet(VC_BASEINDEX+0)->iterator();
1736 uint64_t constval=iit0->next();
1738 IntIterator *iit1=record->getSet(VC_BASEINDEX+1)->iterator();
1739 uint64_t constval2=iit1->next();
1742 if (constval==constval2) {
1743 ADDCONSTRAINT(outputtrue, "equalsconst");
1745 ADDCONSTRAINT(outputtrue->negate(), "equalsconst");
1750 if (inputs[0]==NULL ||
1752 int nullindex=inputs[0]==NULL ? 0 : 1;
1753 IntIterator *iit=record->getSet(VC_BASEINDEX+nullindex)->iterator();
1754 uint64_t constval=iit->next();
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");
1763 Constraint *l2=getRetValueEncoding(r, constval);
1764 Constraint *functionimplication2=new Constraint(IMPLIES, outputtrue, l2);
1765 ADDCONSTRAINT(functionimplication2,"equalsimpl");
1768 IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
1769 while(iit->hasNext()) {
1770 uint64_t val1=iit->next();
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");
1787 void ConstGen::processFence(EPRecord *record) {
1788 //do we already account for the fence?
1789 if (isAlwaysExecuted(record))
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();
1797 EPRecord *prevstore=NULL;
1799 for(i=0;i<size;i++) {
1800 EPRecord *rec=(*tvec)[i];
1801 if (rec->getType()==STORE) {
1804 if (rec == record) {
1809 if (prevstore == NULL) {
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");
1825 /** processRecord performs actions on second traversal of event
1828 void ConstGen::processRecord(EPRecord *record) {
1829 switch (record->getType()) {
1831 processFunction(record);
1834 processEquals(record);
1837 processLoad(record);
1840 processStore(record);
1844 processFence(record);
1849 processFence(record);
1851 if (record->getOp()==ADD) {
1853 } else if (record->getOp()==CAS) {
1855 } else if (record->getOp()==EXC) {
1861 processYield(record);
1864 processBranch(record);
1871 /** visitRecord performs actions done on first traversal of event
1874 void ConstGen::visitRecord(EPRecord *record) {
1875 switch (record->getType()) {
1877 recordExecCond(record);
1878 insertEquals(record);
1881 recordExecCond(record);
1882 insertFunction(record);
1886 recordExecCond(record);
1887 insertAction(record);
1891 recordExecCond(record);
1892 insertAction(record);
1893 groupMemoryOperations(record);
1896 recordExecCond(record);
1897 insertAction(record);
1898 groupMemoryOperations(record);
1901 recordExecCond(record);
1902 insertAction(record);
1903 groupMemoryOperations(record);
1906 recordExecCond(record);
1907 insertBranch(record);
1910 recordExecCond(record);
1913 recordExecCond(record);
1914 insertNonLocal(record);
1917 insertLabel(record);
1920 recordExecCond(record);
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
1944 if (eprecord->compare(epnl)==CR_BEFORE) {
1945 //record occurs after non-local, so add it to set
1947 srs=new RecordSet();
1953 execcondtable->put(record, srs);
1956 void ConstGen::insertNonLocal(EPRecord *record) {
1957 nonlocaltrans->add(record);
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)
1971 void ConstGen::traverseRecord(EPRecord *record, bool initial) {
1974 visitRecord(record);
1976 processRecord(record);
1978 if (record->getType()==LOOPENTER) {
1979 if (record->getNextRecord()!=NULL)
1980 workstack->push_back(record->getNextRecord());
1981 workstack->push_back(record->getChildRecord());
1984 if (record->getChildRecord()!=NULL) {
1985 workstack->push_back(record->getChildRecord());
1987 if (record->getType()==NONLOCALTRANS) {
1990 if (record->getType()==YIELD && model->params.noexecyields) {
1993 if (record->getType()==LOOPEXIT) {
1996 if (record->getType()==BRANCHDIR) {
1997 EPRecord *next=record->getNextRecord();
1999 workstack->push_back(next);
2000 for(uint i=0;i<record->numValues();i++) {
2001 EPValue *branchdir=record->getValue(i);
2003 //Could have an empty branch, so make sure the branch actually
2005 if (branchdir->getFirstRecord()!=NULL)
2006 workstack->push_back(branchdir->getFirstRecord());
2010 record=record->getNextRecord();
2011 } while(record!=NULL);
2014 unsigned int RecPairHash(RecPair *rp) {
2015 uintptr_t v=(uintptr_t) rp->epr1;
2016 uintptr_t v2=(uintptr_t) rp->epr2;
2019 return (uint)((x>>4)^(a));
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));