void neatPrint(EPRecord *r, ConstGen *cgen, bool *satsolution) {
- StoreLoadSet * sls=cgen->getStoreLoadSet(r);
r->print();
- model_print("address=%p ", sls->getAddressEncoding(cgen, r, satsolution));
switch(r->getType()) {
case LOAD: {
- model_print("rd=%lu ", sls->getValueEncoding(cgen, r, satsolution));
+ StoreLoadSet * sls=cgen->getStoreLoadSet(r);
+ model_print("address=%p ", sls->getAddressEncoding(cgen, r, satsolution));
+ model_print("rd=%llu ", sls->getValueEncoding(cgen, r, satsolution));
}
- break;
+ break;
case STORE: {
- model_print("wr=%lu ", sls->getValueEncoding(cgen, r, satsolution));
-
+ StoreLoadSet * sls=cgen->getStoreLoadSet(r);
+ model_print("address=%p ", sls->getAddressEncoding(cgen, r, satsolution));
+ model_print("wr=%llu ", sls->getValueEncoding(cgen, r, satsolution));
}
- break;
+ break;
case RMW: {
- model_print("rd=%lu ", sls->getRMWRValueEncoding(cgen, r, satsolution));
- model_print("wr=%lu ", sls->getValueEncoding(cgen, r, satsolution));
+ StoreLoadSet * sls=cgen->getStoreLoadSet(r);
+ model_print("address=%p ", sls->getAddressEncoding(cgen, r, satsolution));
+ model_print("rd=%llu ", sls->getRMWRValueEncoding(cgen, r, satsolution));
+ model_print("wr=%llu ", sls->getValueEncoding(cgen, r, satsolution));
}
+ break;
default:
;
}
EPRecord *next=processRecord(record, satsolution);
#ifdef TSO
if (next != NULL) {
-
+
if (next->getType()==STORE) {
stores[index]->push_back(next);
next=getNextRecord(next);
}
//Now we have just memory operations, find the first one...make it go first
EPRecord *earliest=NULL;
-
for(uint index=0;index<threads.size();index++) {
EPRecord *record=threads[index];
-
+
if (record!=NULL && (earliest==NULL ||
cg->getOrder(record, earliest, satsolution))) {
earliest=record;
#ifdef TSO
if (!stores[index]->empty()) {
record=stores[index]->front();
-
if (record!=NULL && (earliest==NULL ||
cg->getOrder(record, earliest, satsolution))) {
earliest=record;
if (!br->hasNextRecord())
next=NULL;
}
-
+
if (next==NULL && record->getBranch()!=NULL) {
EPValue * epbr=record->getBranch();
EPRecord *branch=epbr->getRecord();
case MERGE:
case ALLOC:
case EQUALS:
- case FUNCTION:
+ case FUNCTION:
/* Continue executing */
break;
case THREADCREATE:
break;
case NONLOCALTRANS:
break;
+ case LOOPEXIT:
+ break;
case LABEL:
break;
case YIELD: