Work around changes in newer versions of glibc

[satcheck.git] / constgen.cc

diff --git a/constgen.cc b/constgen.cc
index 60cceb7a3bb7f9d8dd1de73add4693e80e3b895c..2f3375b23070d0cd9ccde22677440b042b0ca6ac 100644 (file)
--- a/constgen.cc
+++ b/constgen.cc
@@ -192,7 +192,7 @@ bool ConstGen::canReuseEncoding() {
                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 +201,7 @@ bool ConstGen::canReuseEncoding() {
        }
 
        schedulebuilder->buildSchedule(solution);
-       model_free(solution);   
+       model_free(solution);
 
        return true;
 }
@@ -308,7 +308,7 @@ 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);
@@ -318,19 +318,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) {
@@ -348,6 +348,9 @@ void ConstGen::printRecord(EPRecord *record, int file) {
                if (record->getType()==NONLOCALTRANS) {
                        return;
                }
+               if (record->getType()==LOOPEXIT) {
+                       return;
+               }
                if (record->getType()==BRANCHDIR) {
                        EPRecord *next=record->getNextRecord();
                        if (next != NULL)
@@ -359,7 +362,7 @@ void ConstGen::printRecord(EPRecord *record, int file) {
                                //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;
@@ -661,13 +664,13 @@ void ConstGen::genTSOTransOrderConstraints() {
                                        Constraint * storeload=getOrderConstraint(store, rec);
                                        Constraint * earlystoreload=getOrderConstraint(laststore, rec);
                                        Constraint * c=new Constraint(IMPLIES, storeload, earlystoreload);
-                                       ADDCONSTRAINT(c, "earylstore");
+                                       ADDCONSTRAINT(c, "earlystore");
                                }
                                if (lastload != NULL) {
                                        Constraint * storeearlyload=getOrderConstraint(store, lastload);
                                        Constraint * storeload=getOrderConstraint(store, rec);
                                        Constraint * c=new Constraint(IMPLIES, storeearlyload, storeload);
-                                       ADDCONSTRAINT(c, "earylload");
+                                       ADDCONSTRAINT(c, "earlyload");
                                }
                                lastload=rec;
                        }
@@ -743,6 +746,15 @@ void ConstGen::genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVe
                                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
@@ -756,6 +768,16 @@ void ConstGen::genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVe
                                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
@@ -856,7 +878,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;
@@ -1788,6 +1810,9 @@ void ConstGen::visitRecord(EPRecord *record) {
                recordExecCond(record);
                insertBranch(record);
                break;
+       case LOOPEXIT:
+               recordExecCond(record);
+               break;
        case NONLOCALTRANS:
                recordExecCond(record);
                insertNonLocal(record);
@@ -1865,6 +1890,9 @@ void ConstGen::traverseRecord(EPRecord *record, bool initial) {
                if (record->getType()==NONLOCALTRANS) {
                        return;
                }
+               if (record->getType()==LOOPEXIT) {
+                       return;
+               }
                if (record->getType()==BRANCHDIR) {
                        EPRecord *next=record->getNextRecord();
                        if (next != NULL)