rpt(new RecPairTable()),
numconstraints(0),
goalset(new ModelVector<Constraint *>()),
+ yieldlist(new ModelVector<EPRecord *>()),
goalvararray(NULL),
vars(new ModelVector<Constraint *>()),
branchtable(new BranchTable()),
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)
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;i<storeloadtable->capacity;i++) {
- struct hashlistnode<const void *, StoreLoadSet *> * ptr=& storeloadtable->table[i];
+ struct hashlistnode<const void *, StoreLoadSet *> * ptr=&storeloadtable->table[i];
if (ptr->val != NULL) {
if (ptr->val->removeAddress(ptr->key))
delete ptr->val;
delete storeloadtable->zero->val;
} else
ASSERT(false);
- model_free(storeloadtable -> zero);
+ model_free(storeloadtable->zero);
storeloadtable->zero = NULL;
}
storeloadtable->size = 0;
rpt->resetanddelete();
resetstoreloadtable(storeloadtable);
nonlocaltrans->reset();
+ incompleteexploredbranch->reset();
threadactions->clear();
rectoint->reset();
+ yieldtable->reset();
+ yieldlist->clear();
goalset->clear();
varindex=1;
numconstraints=0;
#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;i<goalset->size();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;
}
schedulebuilder->buildSchedule(solution);
- model_free(solution);
+ model_free(solution);
return true;
}
delete solver;
solver = NULL;
}
-
+
solver=new IncrementalSolver();
traverse(true);
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;i<goalset->size();i++) {
Constraint *var=goalvararray[i];
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()) {
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) {
doPrint(record,file);
if (record->getType()==LOOPENTER) {
- workstack->push_back(record->getNextRecord());
+ if (record->getNextRecord()!=NULL)
+ workstack->push_back(record->getNextRecord());
workstack->push_back(record->getChildRecord());
return;
}
workstack->push_back(next);
for(uint i=0;i<record->numValues();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;
}
/** 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 */
}
}
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();
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);
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))
sri->remove();
}
}
-
+
delete sri;
return srscopy;
}
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();
IntHashSet *addrset=load->getSet(VC_ADDRINDEX);
IntIterator *ait=addrset->iterator();
-
+
while(ait->hasNext()) {
void *addr=(void *)ait->next();
RecordSet *rs=execution->getStoreTable(addr);
}
/** This function merges two recordsets and updates the storeloadtable
- accordingly. */
+ accordingly. */
void ConstGen::mergeSets(StoreLoadSet *to, StoreLoadSet *from) {
RecordIterator * sri=from->iterator();
while (j>0) {
EPRecord *oldrec=(*vector)[--j];
EventType oldrec_t=oldrec->getType();
-
+
if (((oldrec_t == RMW) || (oldrec_t==FENCE)) &&
isAlwaysExecuted(oldrec)) {
return;
#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();
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;t3i<t2vec->size();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;t0i<t1i;t0i++) {
EPRecord *t0rec=(*t1vec)[t0i];
Constraint *c02=getOrderConstraint(t0rec, t2rec);
#ifdef TSO
Constraint *c10=getOrderConstraint(t1rec, t0rec);
+
+ if (!c10->isFalse()) {
+ //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");
- }
+ }
}
}
}
void ConstGen::printConstraint(uint value) {
solver->addClauseLiteral(value);
}
-
+
bool * ConstGen::runSolver() {
int solution=solver->solve();
if (solution == IS_UNSAT) {
} else {
delete solver;
solver=NULL;
- dprintf(2, "INDETER\n");
+ model_print_err("INDETER\n");
model_print("INDETER\n");
exit(-1);
return NULL;
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;
}
EPRecord *join=(*joinvec)[i];
ExecPoint *jp=join->getEP();
if (jp->get_tid()==thr2 &&
- jp->compare(ep2)==CR_AFTER)
+ jp->compare(ep2)==CR_AFTER &&
+ join->getJoinThread() == thr1)
return true;
}
return false;
}
/** 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()) {
RecordIterator *sri=srs->iterator();
while(sri->hasNext()) {
EPRecord *rec=sri->next();
-
+
if (!getOrderConstraint(rec, record)->isTrue()) {
delete sri;
return false;
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++;
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++;
void ConstGen::insertBranch(EPRecord *record) {
uint numvalue=record->numValues();
/** need one value for new directions */
- if (numvalue<record->getLen())
+ if (numvalue<record->getLen()) {
numvalue++;
+ if (model->params.noexecyields) {
+ incompleteexploredbranch->add(record);
+ }
+ }
/** need extra value to represent that branch wasn't executed. **/
bool alwaysexecuted=isAlwaysExecuted(record);
if (!alwaysexecuted)
Constraint *parentbranch=new Constraint(IMPLIES, br->getAnyBranch(), baseconstraint);
ADDCONSTRAINT(parentbranch, "parentbranch");
}
-
+
/** Insert criteria for directions */
ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
ASSERT(depvec->size()==1);
for(unsigned int i=0;i<record->numValues();i++) {
EPValue * branchval=record->getValue(i);
uint64_t val=branchval->getValue();
-
+
if (val==0) {
Constraint *execconstraint=getExecutionConstraint(record);
Constraint *br_false=new Constraint(IMPLIES,
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;j<val_record->numValues();j++) {
}
/** 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);
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);
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);
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);
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);
}
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);
Constraint *var=getNewVar();
Constraint *newadd=new Constraint(AND, var, getExecutionConstraint(record));
ADDGOAL(record, newadd, "newadd");
-
+
ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
if (depvec==NULL) {
IntIterator *valit=record->getSet(VC_BASEINDEX)->iterator();
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");
}
}
}
/** 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<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
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);
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<Constraint *> * novel_branches=new ModelVector<Constraint *>();
+ 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;i<novel_branches->size();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");
}
}
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();
ModelVector<EPRecord *> * inputs=execution->getRevDependences(record, VC_BASEINDEX);
for(uint i=0;i<inputs->size();i++) {
EPRecord * input=(*inputs)[i];
-
+
IntIterator * it=record->getSet(VC_BASEINDEX)->iterator();
while(it->hasNext()) {
uint64_t value=it->next();
void ConstGen::processEquals(EPRecord *record) {
ASSERT (record->getNumFuncInputs() == 2);
EPRecord * inputs[2];
-
+
for(uint i=0;i<2;i++) {
ModelVector<EPRecord *> * 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;i<numvalvars;i++) {
vars[i]=getNewVar();
ADDCONSTRAINT(new Constraint(IMPLIES, outputtrue, new Constraint(AND, numvalvars, vars)), "impequal2");
/*
-
- Constraint * functionimplication=new Constraint(IMPLIES,generateEquivConstraint(numvalvars, valvar1, valvar2), outputtrue);
- ADDCONSTRAINT(functionimplication,"equalsimplspecial");
- Constraint * functionimplicationneg=new Constraint(IMPLIES,outputtrue, generateEquivConstraint(numvalvars, valvar1, valvar2));
- ADDCONSTRAINT(functionimplicationneg,"equalsimplspecialneg");
- */
+
+ Constraint * functionimplication=new Constraint(IMPLIES,generateEquivConstraint(numvalvars, valvar1, valvar2), outputtrue);
+ ADDCONSTRAINT(functionimplication,"equalsimplspecial");
+ Constraint * functionimplicationneg=new Constraint(IMPLIES,outputtrue, generateEquivConstraint(numvalvars, valvar1, valvar2));
+ ADDCONSTRAINT(functionimplicationneg,"equalsimplspecialneg");
+ */
return;
}
if (inputs[0]==NULL && inputs[1]==NULL) {
- IntIterator *iit0=record->getSet(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;
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;
Constraint *l2=getRetValueEncoding(r, constval);
Constraint *functionimplication2=new Constraint(IMPLIES, outputtrue, l2);
ADDCONSTRAINT(functionimplication2,"equalsimpl");
+ return;
}
-
- 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");
}
}
#endif
+/** processRecord performs actions on second traversal of event
+ graph. */
+
void ConstGen::processRecord(EPRecord *record) {
switch (record->getType()) {
case FUNCTION:
case FENCE:
processFence(record);
break;
-#endif
+#endif
case RMW:
#ifdef TSO
processFence(record);
}
}
+/** visitRecord performs actions done on first traversal of event
+ * graph. */
+
void ConstGen::visitRecord(EPRecord *record) {
switch (record->getType()) {
case EQUALS:
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();
processRecord(record);
}
if (record->getType()==LOOPENTER) {
- workstack->push_back(record->getNextRecord());
+ if (record->getNextRecord()!=NULL)
+ workstack->push_back(record->getNextRecord());
workstack->push_back(record->getChildRecord());
return;
}
if (record->getType()==NONLOCALTRANS) {
return;
}
+ if (record->getType()==YIELD && model->params.noexecyields) {
+ return;
+ }
if (record->getType()==LOOPEXIT) {
return;
}
workstack->push_back(next);
for(uint i=0;i<record->numValues();i++) {
EPValue *branchdir=record->getValue(i);
-
+
//Could have an empty branch, so make sure the branch actually
//runs code
if (branchdir->getFirstRecord()!=NULL)
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));
}
projects / satcheck.git / blobdiff