Need to allow for one spare encoding for the non-executed case with no suitable stores.

[satcheck.git] / loadrf.cc

diff --git a/loadrf.cc b/loadrf.cc
index 1b9c551b01d3887dda68605651465dbbf86405f5..52a08fb0b162de198c037c3853eecd38e2fb2278 100644 (file)
--- a/loadrf.cc
+++ b/loadrf.cc
@@ -18,7 +18,7 @@
 LoadRF::LoadRF(EPRecord *_load, ConstGen *cg) : load(_load) {
        RecordSet *mrfSet=cg->getMayReadFromSet(load);
        uint numstores=mrfSet->getSize();
-       numvars=NUMBITS(numstores-1);
+       numvars=NUMBITS(numstores); 
        vars=(Constraint **)model_malloc(numvars*sizeof(Constraint *));
        cg->getArrayNewVars(numvars, vars);
 }
@@ -33,7 +33,7 @@ void LoadRF::genConstraints(ConstGen *cg) {
        StoreLoadSet * sls=cg->getStoreLoadSet(load);
        uint numvalvars=sls->getNumValVars();
        uint numaddrvars=sls->getNumAddrVars();
-       Constraint ** loadvalvars=(load->getType()==RMW)?sls->getRMWRValVars(cg, load):sls->getValVars(cg, load);
+       Constraint ** loadvalvars=(load->getType()==RMW) ? sls->getRMWRValVars(cg, load) : sls->getValVars(cg, load);
        Constraint ** loadaddrvars=sls->getAddrVars(cg, load);
 
        RecordIterator *sri=mrfSet->iterator();
@@ -42,7 +42,7 @@ void LoadRF::genConstraints(ConstGen *cg) {
                Constraint ** storevalvars=sls->getValVars(cg, store);
 
 
-               Constraint *rfconst=(numvars==0)?&ctrue:generateConstraint(numvars, vars, storeindex);
+               Constraint *rfconst=(numvars==0) ? &ctrue : generateConstraint(numvars, vars, storeindex);
                //if we read from a store, it should happen before us
 #ifdef TSO
                Constraint *storebeforeload;
@@ -76,7 +76,7 @@ void LoadRF::genConstraints(ConstGen *cg) {
                //ordered between the load and store
 
                RecordSet *conflictSet=cg->computeConflictSet(store, load, mrfSet);
-               RecordIterator *sit=conflictSet!=NULL?conflictSet->iterator():mrfSet->iterator();
+               RecordIterator *sit=conflictSet!=NULL ? conflictSet->iterator() : mrfSet->iterator();
 
                while(sit->hasNext()) {
                        EPRecord *conflictstore=sit->next();
@@ -84,21 +84,37 @@ void LoadRF::genConstraints(ConstGen *cg) {
                        Constraint * storebeforeconflict=cg->getOrderConstraint(store, conflictstore);
                        if (storebeforeconflict->isFalse())
                                continue;
-                       Constraint * conflictbeforeload=cg->getOrderConstraint(conflictstore, load);    
+#ifdef TSO
+                       //Have to cover the same thread case
+                       Constraint *conflictbeforeload;
+                       if (conflictstore->getEP()->get_tid()==load->getEP()->get_tid()) {
+                               if (conflictstore->getEP()->compare(load->getEP())==CR_AFTER)
+                                       conflictbeforeload=&ctrue;
+                               else
+                                       conflictbeforeload=&cfalse;
+                       } else {
+                               conflictbeforeload=cg->getOrderConstraint(conflictstore, load);
+                       }
                        if (conflictbeforeload->isFalse()) {
                                storebeforeconflict->freerec();
                                continue;
                        }
-
+#else
+                       Constraint * conflictbeforeload=cg->getOrderConstraint(conflictstore, load);
+                       if (conflictbeforeload->isFalse()) {
+                               storebeforeconflict->freerec();
+                               continue;
+                       }
+#endif
                        rfconst=generateConstraint(numvars, vars, storeindex);
                        Constraint *array[]={storebeforeconflict,
                                                                                                         conflictbeforeload,
                                                                                                         rfconst,
                                                                                                         cg->getExecutionConstraint(conflictstore)};
-                       Constraint *confstore=new Constraint(IMPLIES, 
+                       Constraint *confstore=new Constraint(IMPLIES,
                                                                                                                                                                         new Constraint(AND, 4, array),
                                                                                                                                                                         generateEquivConstraint(numaddrvars, loadaddrvars, confstoreaddrvars)->negate());
-                       
+
                        ADDCONSTRAINT2(cg, confstore, "confstore");
                }
                delete sit;