Fix yield bug

[satcheck.git] / schedulebuilder.cc

diff --git a/schedulebuilder.cc b/schedulebuilder.cc
index 4473c74e3a97461d4187f0af61b3e4af581738bd..6cf4b5aae9598963b8e6a86b2fa6cf68c7319b78 100644 (file)
--- a/schedulebuilder.cc
+++ b/schedulebuilder.cc
@@ -13,6 +13,7 @@
 #include "constgen.h"
 #include "branchrecord.h"
 #include "storeloadset.h"
+#include "model.h"
 
 ScheduleBuilder::ScheduleBuilder(MCExecution *_execution, ConstGen *cgen) :
        cg(cgen),
@@ -26,23 +27,27 @@ ScheduleBuilder::~ScheduleBuilder() {
 
 
 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:
                ;
        }
@@ -65,7 +70,7 @@ void ScheduleBuilder::buildSchedule(bool * satsolution) {
                        EPRecord *next=processRecord(record, satsolution);
 #ifdef TSO
                        if (next != NULL) {
-                       
+
                                if (next->getType()==STORE) {
                                        stores[index]->push_back(next);
                                        next=getNextRecord(next);
@@ -86,10 +91,9 @@ void ScheduleBuilder::buildSchedule(bool * satsolution) {
                }
                //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;
@@ -97,7 +101,6 @@ void ScheduleBuilder::buildSchedule(bool * satsolution) {
 #ifdef TSO
                        if (!stores[index]->empty()) {
                                record=stores[index]->front();
-                               
                                if (record!=NULL && (earliest==NULL ||
                                                                                                                 cg->getOrder(record, earliest, satsolution))) {
                                        earliest=record;
@@ -149,7 +152,7 @@ EPRecord * ScheduleBuilder::getNextRecord(EPRecord *record) {
                if (!br->hasNextRecord())
                        next=NULL;
        }
-       
+
        if (next==NULL && record->getBranch()!=NULL) {
                EPValue * epbr=record->getBranch();
                EPRecord *branch=epbr->getRecord();
@@ -190,7 +193,7 @@ EPRecord * ScheduleBuilder::processRecord(EPRecord *record, bool *satsolution) {
        case MERGE:
        case ALLOC:
        case EQUALS:
-       case FUNCTION: 
+       case FUNCTION:
                /* Continue executing */
                break;
        case THREADCREATE:
@@ -208,9 +211,13 @@ EPRecord * ScheduleBuilder::processRecord(EPRecord *record, bool *satsolution) {
                break;
        case NONLOCALTRANS:
                break;
+       case LOOPEXIT:
+               break;
        case LABEL:
                break;
        case YIELD:
+               if (model->params.noexecyields)
+                       return NULL;
                break;
        default:
                ASSERT(0);