X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=constgen.cc;h=e7f8c2d68004928529c2441d2024b0fe7208d85d;hb=40913ce63d171f125117caab249218839fd4b083;hp=cf584646b340ce7d160aba52c1e49e1e8fb797ab;hpb=e3e2836db3e10d5d1b7a262c7b34f247af076b7a;p=satcheck.git diff --git a/constgen.cc b/constgen.cc index cf58464..e7f8c2d 100644 --- a/constgen.cc +++ b/constgen.cc @@ -38,6 +38,7 @@ ConstGen::ConstGen(MCExecution *e) : rpt(new RecPairTable()), numconstraints(0), goalset(new ModelVector()), + yieldlist(new ModelVector()), goalvararray(NULL), vars(new ModelVector()), branchtable(new BranchTable()), @@ -45,9 +46,11 @@ ConstGen::ConstGen(MCExecution *e) : equalstable(new EqualsTable()), schedulebuilder(new ScheduleBuilder(e, this)), nonlocaltrans(new RecordSet()), + incompleteexploredbranch(new RecordSet()), execcondtable(new LoadHashTable()), solver(NULL), rectoint(new RecToIntTable()), + yieldtable(new RecToConsTable()), varindex(1), schedule_graph(0), has_untaken_branches(false) @@ -80,19 +83,22 @@ ConstGen::~ConstGen() { delete threadactions; delete rpt; delete goalset; + delete yieldlist; delete vars; delete branchtable; delete functiontable; delete equalstable; delete schedulebuilder; delete nonlocaltrans; + delete incompleteexploredbranch; delete execcondtable; delete rectoint; + delete yieldtable; } void resetstoreloadtable(StoreLoadSetHashTable * storeloadtable) { for(uint i=0;icapacity;i++) { - struct hashlistnode * ptr=& storeloadtable->table[i]; + struct hashlistnode * ptr=&storeloadtable->table[i]; if (ptr->val != NULL) { if (ptr->val->removeAddress(ptr->key)) delete ptr->val; @@ -106,7 +112,7 @@ void resetstoreloadtable(StoreLoadSetHashTable * storeloadtable) { delete storeloadtable->zero->val; } else ASSERT(false); - model_free(storeloadtable -> zero); + model_free(storeloadtable->zero); storeloadtable->zero = NULL; } storeloadtable->size = 0; @@ -128,8 +134,11 @@ void ConstGen::reset() { rpt->resetanddelete(); resetstoreloadtable(storeloadtable); nonlocaltrans->reset(); + incompleteexploredbranch->reset(); threadactions->clear(); rectoint->reset(); + yieldtable->reset(); + yieldlist->clear(); goalset->clear(); varindex=1; numconstraints=0; @@ -182,17 +191,17 @@ bool ConstGen::canReuseEncoding() { #endif model_print("start %lu, finish %lu\n", start,finish); model_print("Incremental time = %12.6f\n", ((double)(finish-start))/1000000); - + if (solution==NULL) { return false; } - + //Zero out the achieved goals for(uint i=0;isize();i++) { Constraint *var=goalvararray[i]; if (var != NULL) { if (solution[var->getVar()]) { - // if (goalvararray[i] != NULL) + //if (goalvararray[i] != NULL) //model_print("SAT clearing goal %d.\n", i); goalvararray[i]=NULL; @@ -201,7 +210,7 @@ bool ConstGen::canReuseEncoding() { } schedulebuilder->buildSchedule(solution); - model_free(solution); + model_free(solution); return true; } @@ -215,7 +224,7 @@ bool ConstGen::process() { delete solver; solver = NULL; } - + solver=new IncrementalSolver(); traverse(true); @@ -279,13 +288,13 @@ bool ConstGen::process() { model_print("start %lu, finish %lu\n", start,finish); model_print("Initial time = %12.6f\n", ((double)(finish-start))/1000000); - + if (solution==NULL) { delete solver; solver = NULL; return true; } - + //Zero out the achieved goals for(uint i=0;isize();i++) { Constraint *var=goalvararray[i]; @@ -308,8 +317,8 @@ void ConstGen::printEventGraph() { sprintf(buffer, "eventgraph%u.dot",schedule_graph); schedule_graph++; int file=open(buffer,O_WRONLY|O_CREAT|O_TRUNC, S_IRWXU); - dprintf(file, "digraph eventgraph {\n"); - + model_dprintf(file, "digraph eventgraph {\n"); + EPRecord *first=execution->getEPRecord(MCID_FIRST); printRecord(first, file); while(!workstack->empty()) { @@ -318,19 +327,19 @@ void ConstGen::printEventGraph() { printRecord(record, file); } - dprintf(file, "}\n"); + model_dprintf(file, "}\n"); close(file); } void ConstGen::doPrint(EPRecord *record, int file) { - dprintf(file, "%lu[label=\"",(uintptr_t)record); + model_dprintf(file, "%lu[label=\"",(uintptr_t)record); record->print(file); - dprintf(file, "\"];\n"); + model_dprintf(file, "\"];\n"); if (record->getNextRecord()!=NULL) - dprintf(file, "%lu->%lu;\n", (uintptr_t) record, (uintptr_t) record->getNextRecord()); - + model_dprintf(file, "%lu->%lu;\n", (uintptr_t) record, (uintptr_t) record->getNextRecord()); + if (record->getChildRecord()!=NULL) - dprintf(file, "%lu->%lu[color=red];\n", (uintptr_t) record, (uintptr_t) record->getChildRecord()); + model_dprintf(file, "%lu->%lu[color=red];\n", (uintptr_t) record, (uintptr_t) record->getChildRecord()); } void ConstGen::printRecord(EPRecord *record, int file) { @@ -357,12 +366,12 @@ void ConstGen::printRecord(EPRecord *record, int file) { workstack->push_back(next); for(uint i=0;inumValues();i++) { EPValue *branchdir=record->getValue(i); - + //Could have an empty branch, so make sure the branch actually //runs code if (branchdir->getFirstRecord()!=NULL) { workstack->push_back(branchdir->getFirstRecord()); - dprintf(file, "%lu->%lu[color=blue];\n", (uintptr_t) record, (uintptr_t) branchdir->getFirstRecord()); + model_dprintf(file, "%lu->%lu[color=blue];\n", (uintptr_t) record, (uintptr_t) branchdir->getFirstRecord()); } } return; @@ -385,13 +394,13 @@ void ConstGen::traverse(bool initial) { } /** This method looks for all other memory operations that could - potentially share a location, and build partitions of memory - locations such that all memory locations that can share the same - address are in the same group. - - These memory operations should share an encoding of addresses and - values. -*/ + potentially share a location, and build partitions of memory + locations such that all memory locations that can share the same + address are in the same group. + + These memory operations should share an encoding of addresses and + values. + */ void ConstGen::groupMemoryOperations(EPRecord *op) { /** Handle our first address */ @@ -432,18 +441,18 @@ RecordSet * ConstGen::computeConflictSet(EPRecord *store, EPRecord *load, Record } } delete storeaddr; - + ASSERT(numaddr!=0); if (numaddr!=1) return NULL; - + RecordSet *srscopy=baseset->copy(); RecordIterator *sri=srscopy->iterator(); while(sri->hasNext()) { bool pruneconflictstore=false; EPRecord *conflictstore=sri->next(); bool conflictafterstore=getOrderConstraint(store,conflictstore)->isTrue(); - bool conflictbeforeload=getOrderConstraint(conflictstore,load)->isTrue(); + bool conflictbeforeload=getOrderConstraint(conflictstore,load)->isTrue(); if (conflictafterstore) { RecordIterator *sricheck=srscopy->iterator(); @@ -455,7 +464,7 @@ RecordSet * ConstGen::computeConflictSet(EPRecord *store, EPRecord *load, Record bool checkbeforeconflict=getOrderConstraint(checkstore,conflictstore)->isTrue(); if (!checkbeforeconflict) continue; - + //See if the checkstore must store to the relevant address IntHashSet * storeaddr=checkstore->getSet(VC_ADDRINDEX); @@ -483,7 +492,7 @@ RecordSet * ConstGen::computeConflictSet(EPRecord *store, EPRecord *load, Record bool checkbeforeload=getOrderConstraint(checkstore, load)->isTrue(); if (!checkbeforeload) continue; - + //See if the checkstore must store to the relevant address IntHashSet * storeaddr=checkstore->getSet(VC_ADDRINDEX); if (storeaddr->getSize()!=1 || !storeaddr->contains((uint64_t)commonaddr)) @@ -502,7 +511,7 @@ RecordSet * ConstGen::computeConflictSet(EPRecord *store, EPRecord *load, Record sri->remove(); } } - + delete sri; return srscopy; } @@ -513,7 +522,7 @@ RecordSet * ConstGen::computeConflictSet(EPRecord *store, EPRecord *load, Record RecordSet * ConstGen::getMayReadFromSet(EPRecord *load) { if (load->getSet(VC_ADDRINDEX)->getSize()==1) return getMayReadFromSetOpt(load); - + RecordSet *srs=loadtable->get(load); ExecPoint *epload=load->getEP(); thread_id_t loadtid=epload->get_tid(); @@ -523,7 +532,7 @@ RecordSet * ConstGen::getMayReadFromSet(EPRecord *load) { IntHashSet *addrset=load->getSet(VC_ADDRINDEX); IntIterator *ait=addrset->iterator(); - + while(ait->hasNext()) { void *addr=(void *)ait->next(); RecordSet *rs=execution->getStoreTable(addr); @@ -594,7 +603,7 @@ RecordSet * ConstGen::getMayReadFromSetOpt(EPRecord *load) { } /** This function merges two recordsets and updates the storeloadtable - accordingly. */ + accordingly. */ void ConstGen::mergeSets(StoreLoadSet *to, StoreLoadSet *from) { RecordIterator * sri=from->iterator(); @@ -628,7 +637,7 @@ void ConstGen::insertTSOAction(EPRecord *load) { while (j>0) { EPRecord *oldrec=(*vector)[--j]; EventType oldrec_t=oldrec->getType(); - + if (((oldrec_t == RMW) || (oldrec_t==FENCE)) && isAlwaysExecuted(oldrec)) { return; @@ -681,7 +690,7 @@ void ConstGen::genTSOTransOrderConstraints() { #endif /** This function creates ordering constraints to implement SC for - memory operations. */ + memory operations. */ void ConstGen::insertAction(EPRecord *record) { thread_id_t tid=record->getEP()->get_tid(); @@ -732,40 +741,59 @@ void ConstGen::genTransOrderConstraints(ModelVector * t1vec, ModelVe EPRecord *t2rec=(*t2vec)[t2i]; /* Note: One only really needs to generate the first constraint - in the first loop and the last constraint in the last loop. - I tried this and performance suffered on linuxrwlocks and - linuxlocks at the current time. BD - August 2014*/ + in the first loop and the last constraint in the last loop. + I tried this and performance suffered on linuxrwlocks and + linuxlocks at the current time. BD - August 2014*/ Constraint *c21=getOrderConstraint(t2rec, t1rec); /* short circuit for the trivial case */ if (c21->isTrue()) continue; - + for(uint t3i=t2i+1;t3isize();t3i++) { EPRecord *t3rec=(*t2vec)[t3i]; Constraint *c13=getOrderConstraint(t1rec, t3rec); #ifdef TSO Constraint *c32=getOrderConstraint(t3rec, t2rec); + if (!c32->isFalse()) { + //Have a store->load that could be reordered, need to generate other constraint + Constraint *c12=getOrderConstraint(t1rec, t2rec); + Constraint *c23=getOrderConstraint(t2rec, t3rec); + Constraint *c31=getOrderConstraint(t3rec, t1rec); + Constraint *slarray[] = {c31, c23, c12}; + Constraint * intradelayedstore=new Constraint(OR, 3, slarray); + ADDCONSTRAINT(intradelayedstore, "intradelayedstore"); + } Constraint * array[]={c21, c32, c13}; Constraint *intratransorder=new Constraint(OR, 3, array); #else Constraint *intratransorder=new Constraint(OR, c21, c13); #endif ADDCONSTRAINT(intratransorder,"intratransorder"); - } + } for(uint t0i=0;t0iisFalse()) { + //Have a store->load that could be reordered, need to generate other constraint + Constraint *c01=getOrderConstraint(t0rec, t1rec); + Constraint *c12=getOrderConstraint(t1rec, t2rec); + Constraint *c20=getOrderConstraint(t2rec, t0rec); + Constraint *slarray[] = {c01, c12, c20}; + Constraint * intradelayedstore=new Constraint(OR, 3, slarray); + ADDCONSTRAINT(intradelayedstore, "intradelayedstore"); + } Constraint * array[]={c10, c21, c02}; Constraint *intratransorder=new Constraint(OR, 3, array); #else Constraint *intratransorder=new Constraint(OR, c21, c02); #endif ADDCONSTRAINT(intratransorder,"intratransorder"); - } + } } } } @@ -846,7 +874,7 @@ void ConstGen::printNegConstraint(uint value) { void ConstGen::printConstraint(uint value) { solver->addClauseLiteral(value); } - + bool * ConstGen::runSolver() { int solution=solver->solve(); if (solution == IS_UNSAT) { @@ -859,7 +887,7 @@ bool * ConstGen::runSolver() { } else { delete solver; solver=NULL; - dprintf(2, "INDETER\n"); + model_print_err("INDETER\n"); model_print("INDETER\n"); exit(-1); return NULL; @@ -945,7 +973,7 @@ bool ConstGen::orderThread(EPRecord *first, EPRecord *second) { EPRecord *thr2start=tr2->getParentRecord(); if (thr2start!=NULL) { ExecPoint *epthr2start=thr2start->getEP(); - if (epthr2start->get_tid()==thr1 && + if (epthr2start->get_tid()==thr1 && ep1->compare(epthr2start)==CR_AFTER) return true; } @@ -1008,7 +1036,7 @@ StoreLoadSet * ConstGen::getStoreLoadSet(EPRecord *record) { } /** Returns a constraint that is true if the output of record has the - given value. */ + given value. */ Constraint * ConstGen::getRetValueEncoding(EPRecord *record, uint64_t value) { switch(record->getType()) { @@ -1064,7 +1092,7 @@ bool ConstGen::subsumesExecutionConstraint(EPRecord *recordsubsumes, EPRecord *r RecordIterator *sri=srs->iterator(); while(sri->hasNext()) { EPRecord *rec=sri->next(); - + if (!getOrderConstraint(rec, record)->isTrue()) { delete sri; return false; @@ -1078,7 +1106,7 @@ bool ConstGen::subsumesExecutionConstraint(EPRecord *recordsubsumes, EPRecord *r Constraint * ConstGen::getExecutionConstraint(EPRecord *record) { EPValue *branch=record->getBranch(); RecordSet *srs=execcondtable->get(record); - int size=srs==NULL?0:srs->getSize(); + int size=srs==NULL ? 0 : srs->getSize(); if (branch!=NULL) size++; @@ -1109,7 +1137,7 @@ Constraint * ConstGen::getExecutionConstraint(EPRecord *record) { bool ConstGen::isAlwaysExecuted(EPRecord *record) { EPValue *branch=record->getBranch(); RecordSet *srs=execcondtable->get(record); - int size=srs==NULL?0:srs->getSize(); + int size=srs==NULL ? 0 : srs->getSize(); if (branch!=NULL) size++; @@ -1119,8 +1147,12 @@ bool ConstGen::isAlwaysExecuted(EPRecord *record) { void ConstGen::insertBranch(EPRecord *record) { uint numvalue=record->numValues(); /** need one value for new directions */ - if (numvaluegetLen()) + if (numvaluegetLen()) { numvalue++; + if (model->params.noexecyields) { + incompleteexploredbranch->add(record); + } + } /** need extra value to represent that branch wasn't executed. **/ bool alwaysexecuted=isAlwaysExecuted(record); if (!alwaysexecuted) @@ -1146,7 +1178,7 @@ void ConstGen::processBranch(EPRecord *record) { Constraint *parentbranch=new Constraint(IMPLIES, br->getAnyBranch(), baseconstraint); ADDCONSTRAINT(parentbranch, "parentbranch"); } - + /** Insert criteria for directions */ ModelVector * depvec=execution->getRevDependences(record, VC_BASEINDEX); ASSERT(depvec->size()==1); @@ -1154,7 +1186,7 @@ void ConstGen::processBranch(EPRecord *record) { for(unsigned int i=0;inumValues();i++) { EPValue * branchval=record->getValue(i); uint64_t val=branchval->getValue(); - + if (val==0) { Constraint *execconstraint=getExecutionConstraint(record); Constraint *br_false=new Constraint(IMPLIES, @@ -1167,7 +1199,7 @@ void ConstGen::processBranch(EPRecord *record) { Constraint *execconstraint=getExecutionConstraint(record); Constraint *br_true1=new Constraint(IMPLIES, new Constraint(AND, getRetValueEncoding(val_record, 0)->negate(), execconstraint), - br->getBranch(branchval)); + br->getBranch(branchval)); ADDCONSTRAINT(br_true1, "br_true1"); } else { for(unsigned int j=0;jnumValues();j++) { @@ -1205,7 +1237,7 @@ void ConstGen::processLoad(EPRecord *record) { } /** This procedure generates the constraints that set the address - variables for load/store/rmw operations. */ + variables for load/store/rmw operations. */ void ConstGen::processAddresses(EPRecord *record) { StoreLoadSet *sls=getStoreLoadSet(record); @@ -1223,7 +1255,7 @@ void ConstGen::processAddresses(EPRecord *record) { IntIterator *it=record->getSet(VC_ADDRINDEX)->iterator(); uintptr_t offset=record->getOffset(); - + while(it->hasNext()) { uint64_t addr=it->next(); Constraint *srcenc=getRetValueEncoding(src, addr-offset); @@ -1260,7 +1292,7 @@ void ConstGen::processCAS(EPRecord *record) { ASSERT(depveccas->size()==1); EPRecord *src=(*depveccas)[0]; IntIterator *it=getStoreLoadSet(record)->getValues()->iterator(); - + while(it->hasNext()) { uint64_t valcas=it->next(); Constraint *srcenc=getRetValueEncoding(src, valcas); @@ -1305,7 +1337,7 @@ void ConstGen::processCAS(EPRecord *record) { ASSERT(depvec->size()==1); EPRecord *src=(*depvec)[0]; IntIterator *it=record->getStoreSet()->iterator(); - + while(it->hasNext()) { uint64_t val=it->next(); Constraint *srcenc=getRetValueEncoding(src, val); @@ -1321,11 +1353,11 @@ void ConstGen::processCAS(EPRecord *record) { delete it; } StoreLoadSet *sls=getStoreLoadSet(record); - + Constraint *repeatval=generateEquivConstraint(sls->getNumValVars(), sls->getValVars(this, record), sls->getRMWRValVars(this, record)); Constraint *failcas=new Constraint(IMPLIES, eq->negate(), repeatval); ADDCONSTRAINT(failcas,"casmemfail"); - + processAddresses(record); } @@ -1346,7 +1378,7 @@ void ConstGen::processEXC(EPRecord *record) { ASSERT(depvec->size()==1); EPRecord *src=(*depvec)[0]; IntIterator *it=record->getStoreSet()->iterator(); - + while(it->hasNext()) { uint64_t val=it->next(); Constraint *srcenc=getRetValueEncoding(src, val); @@ -1368,7 +1400,7 @@ void ConstGen::processAdd(EPRecord *record) { Constraint *var=getNewVar(); Constraint *newadd=new Constraint(AND, var, getExecutionConstraint(record)); ADDGOAL(record, newadd, "newadd"); - + ModelVector * depvec=execution->getRevDependences(record, VC_BASEINDEX); if (depvec==NULL) { IntIterator *valit=record->getSet(VC_BASEINDEX)->iterator(); @@ -1409,7 +1441,7 @@ void ConstGen::processAdd(EPRecord *record) { Constraint *storeenc=getMemValueEncoding(record, sum); Constraint *notvar=var->negate(); Constraint *addop=new Constraint(IMPLIES, new Constraint(AND, srcenc, loadenc), - new Constraint(AND, notvar, storeenc)); + new Constraint(AND, notvar, storeenc)); ADDCONSTRAINT(addop,"addinputvar"); } } @@ -1422,10 +1454,10 @@ void ConstGen::processAdd(EPRecord *record) { } /** This function ensures that the value of a store's SAT variables - matches the store's input value. + matches the store's input value. - TODO: Could optimize the case where the encodings are the same... -*/ + TODO: Could optimize the case where the encodings are the same... + */ void ConstGen::processStore(EPRecord *record) { ModelVector * depvec=execution->getRevDependences(record, VC_BASEINDEX); @@ -1439,7 +1471,7 @@ void ConstGen::processStore(EPRecord *record) { ASSERT(depvec->size()==1); EPRecord *src=(*depvec)[0]; IntIterator *it=record->getStoreSet()->iterator(); - + while(it->hasNext()) { uint64_t val=it->next(); Constraint *srcenc=getRetValueEncoding(src, val); @@ -1452,13 +1484,89 @@ void ConstGen::processStore(EPRecord *record) { processAddresses(record); } +/** **/ + +void ConstGen::computeYieldCond(EPRecord *record) { + ExecPoint *yieldep=record->getEP(); + EPRecord *prevyield=NULL; + ExecPoint *prevyieldep=NULL; + + for(int i=(int)(yieldlist->size()-1);i>=0;i--) { + EPRecord *tmpyield=(*yieldlist)[i]; + ExecPoint *tmpep=tmpyield->getEP(); + //Do we have a previous yield operation from the same thread + if (tmpep->get_tid()==yieldep->get_tid() && + yieldep->compare(tmpep)==CR_BEFORE) { + //Yes + prevyield=tmpyield; + prevyieldep=prevyield->getEP(); + break; + } + } + + yieldlist->push_back(record); + + ModelVector * novel_branches=new ModelVector(); + RecordIterator *sri=incompleteexploredbranch->iterator(); + while(sri->hasNext()) { + EPRecord * unexploredbranch=sri->next(); + ExecPoint * branchep=unexploredbranch->getEP(); + if (branchep->get_tid()!=yieldep->get_tid()) { + //wrong thread + continue; + } + + if (yieldep->compare(branchep)!=CR_BEFORE) { + //Branch does not occur before yield, so skip + continue; + } + + //See if the previous yield already accounts for this branch + if (prevyield != NULL && + prevyieldep->compare(branchep)==CR_BEFORE) { + //Branch occurs before previous yield, so we can safely skip this branch + continue; + } + //This is a branch that could prevent this yield from being executed + BranchRecord *br=branchtable->get(unexploredbranch); + Constraint * novel_branch=br->getNewBranch(); + novel_branches->push_back(novel_branch); + } + + int num_constraints=((prevyield==NULL)?0:1)+novel_branches->size(); + Constraint *carray[num_constraints]; + int arr_index=0; + + if (prevyield!=NULL) { + carray[arr_index++]=yieldtable->get(prevyield);//get constraint for old yield + } + for(uint i=0;isize();i++) { + carray[arr_index++]=(*novel_branches)[i]; + } + + Constraint *cor=num_constraints!=0?new Constraint(OR, num_constraints, carray):&cfalse; + + Constraint *var=getNewVar(); + //If the variable is true, then we need to have taken some branch + //ahead of the yield + Constraint *implies=new Constraint(IMPLIES, var, cor); + ADDCONSTRAINT(implies, "possiblebranchnoyield"); + yieldtable->put(record, var); + + delete novel_branches; + delete sri; +} + + /** Handle yields by just forbidding them via the SAT formula. */ void ConstGen::processYield(EPRecord *record) { - if (model->params.noyields && - record->getBranch()!=NULL) { - Constraint * noyield=getExecutionConstraint(record)->negate(); - ADDCONSTRAINT(noyield, "noyield"); + if (model->params.noexecyields) { + computeYieldCond(record); + Constraint * noexecyield=getExecutionConstraint(record)->negate(); + Constraint * branchaway=yieldtable->get(record); + Constraint * avoidbranch=new Constraint(OR, noexecyield, branchaway); + ADDCONSTRAINT(avoidbranch, "noexecyield"); } } @@ -1469,7 +1577,7 @@ void ConstGen::processLoopPhi(EPRecord *record) { while(rit->hasNext()) { struct RecordIDPair *rip=rit->next(); EPRecord *input=rip->idrecord; - + IntIterator * it=record->getSet(VC_BASEINDEX)->iterator(); while(it->hasNext()) { uint64_t value=it->next(); @@ -1490,7 +1598,7 @@ void ConstGen::processPhi(EPRecord *record) { ModelVector * inputs=execution->getRevDependences(record, VC_BASEINDEX); for(uint i=0;isize();i++) { EPRecord * input=(*inputs)[i]; - + IntIterator * it=record->getSet(VC_BASEINDEX)->iterator(); while(it->hasNext()) { uint64_t value=it->next(); @@ -1566,30 +1674,30 @@ void ConstGen::processFunction(EPRecord *record) { void ConstGen::processEquals(EPRecord *record) { ASSERT (record->getNumFuncInputs() == 2); EPRecord * inputs[2]; - + for(uint i=0;i<2;i++) { ModelVector * depvec=execution->getRevDependences(record, i+VC_BASEINDEX); if (depvec==NULL) { inputs[i]=NULL; } else if (depvec->size()==1) { inputs[i]=(*depvec)[0]; - } else ASSERT(false); + } else ASSERT(false); } //rely on this being a variable Constraint * outputtrue=getRetValueEncoding(record, 1); ASSERT(outputtrue->getType()==VAR); - + if (inputs[0]!=NULL && inputs[1]!=NULL && (inputs[0]->getType()==LOAD || inputs[0]->getType()==RMW) && (inputs[1]->getType()==LOAD || inputs[1]->getType()==RMW) && (getStoreLoadSet(inputs[0])==getStoreLoadSet(inputs[1]))) { StoreLoadSet * sls=getStoreLoadSet(inputs[0]); int numvalvars=sls->getNumValVars(); - Constraint **valvar1=(inputs[0]->getType()==RMW)?sls->getRMWRValVars(this, inputs[0]):sls->getValVars(this, inputs[0]); - Constraint **valvar2=(inputs[1]->getType()==RMW)?sls->getRMWRValVars(this, inputs[1]):sls->getValVars(this, inputs[1]); + Constraint **valvar1=(inputs[0]->getType()==RMW) ? sls->getRMWRValVars(this, inputs[0]) : sls->getValVars(this, inputs[0]); + Constraint **valvar2=(inputs[1]->getType()==RMW) ? sls->getRMWRValVars(this, inputs[1]) : sls->getValVars(this, inputs[1]); //new test - + Constraint *vars[numvalvars]; for(int i=0;igetSet(VC_BASEINDEX+0)->iterator(); + IntIterator *iit0=record->getSet(VC_BASEINDEX+0)->iterator(); uint64_t constval=iit0->next(); delete iit0; - IntIterator *iit1=record->getSet(VC_BASEINDEX+1)->iterator(); + IntIterator *iit1=record->getSet(VC_BASEINDEX+1)->iterator(); uint64_t constval2=iit1->next(); delete iit1; @@ -1636,12 +1744,12 @@ void ConstGen::processEquals(EPRecord *record) { ADDCONSTRAINT(outputtrue->negate(), "equalsconst"); } return; - } - + } + if (inputs[0]==NULL || inputs[1]==NULL) { - int nullindex=inputs[0]==NULL?0:1; - IntIterator *iit=record->getSet(VC_BASEINDEX+nullindex)->iterator(); + int nullindex=inputs[0]==NULL ? 0 : 1; + IntIterator *iit=record->getSet(VC_BASEINDEX+nullindex)->iterator(); uint64_t constval=iit->next(); delete iit; @@ -1655,17 +1763,17 @@ void ConstGen::processEquals(EPRecord *record) { Constraint *functionimplication2=new Constraint(IMPLIES, outputtrue, l2); ADDCONSTRAINT(functionimplication2,"equalsimpl"); } - - IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator(); + + IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator(); while(iit->hasNext()) { uint64_t val1=iit->next(); - - IntIterator *iit2=record->getSet(VC_BASEINDEX+1)->iterator(); + + IntIterator *iit2=record->getSet(VC_BASEINDEX+1)->iterator(); while(iit2->hasNext()) { uint64_t val2=iit2->next(); Constraint *l=getRetValueEncoding(inputs[0], val1); Constraint *r=getRetValueEncoding(inputs[1], val2); - Constraint *imp=(val1==val2)?outputtrue:outputtrue->negate(); + Constraint *imp=(val1==val2) ? outputtrue : outputtrue->negate(); Constraint * functionimplication=new Constraint(IMPLIES, new Constraint(AND, l, r), imp); ADDCONSTRAINT(functionimplication,"equalsimpl"); } @@ -1713,6 +1821,9 @@ void ConstGen::processFence(EPRecord *record) { } #endif +/** processRecord performs actions on second traversal of event + graph. */ + void ConstGen::processRecord(EPRecord *record) { switch (record->getType()) { case FUNCTION: @@ -1731,7 +1842,7 @@ void ConstGen::processRecord(EPRecord *record) { case FENCE: processFence(record); break; -#endif +#endif case RMW: #ifdef TSO processFence(record); @@ -1756,6 +1867,9 @@ void ConstGen::processRecord(EPRecord *record) { } } +/** visitRecord performs actions done on first traversal of event + * graph. */ + void ConstGen::visitRecord(EPRecord *record) { switch (record->getType()) { case EQUALS: @@ -1812,7 +1926,7 @@ void ConstGen::visitRecord(EPRecord *record) { void ConstGen::recordExecCond(EPRecord *record) { ExecPoint *eprecord=record->getEP(); EPValue * branchval=record->getBranch(); - EPRecord * branch=(branchval==NULL)?NULL:branchval->getRecord(); + EPRecord * branch=(branchval==NULL) ? NULL : branchval->getRecord(); ExecPoint *epbranch= (branch==NULL) ? NULL : branch->getEP(); RecordSet *srs=NULL; RecordIterator *sri=nonlocaltrans->iterator(); @@ -1871,6 +1985,9 @@ void ConstGen::traverseRecord(EPRecord *record, bool initial) { if (record->getType()==NONLOCALTRANS) { return; } + if (record->getType()==YIELD && model->params.noexecyields) { + return; + } if (record->getType()==LOOPEXIT) { return; } @@ -1880,7 +1997,7 @@ void ConstGen::traverseRecord(EPRecord *record, bool initial) { workstack->push_back(next); for(uint i=0;inumValues();i++) { EPValue *branchdir=record->getValue(i); - + //Could have an empty branch, so make sure the branch actually //runs code if (branchdir->getFirstRecord()!=NULL) @@ -1902,5 +2019,5 @@ unsigned int RecPairHash(RecPair *rp) { bool RecPairEquals(RecPair *r1, RecPair *r2) { return ((r1->epr1==r2->epr1)&&(r1->epr2==r2->epr2)) || - ((r1->epr1==r2->epr2)&&(r1->epr2==r2->epr1)); + ((r1->epr1==r2->epr2)&&(r1->epr2==r2->epr1)); }