fix spacing with make tabbing
authorbdemsky <bdemsky@uci.edu>
Thu, 15 Dec 2016 06:29:12 +0000 (22:29 -0800)
committerbdemsky <bdemsky@uci.edu>
Thu, 15 Dec 2016 06:29:12 +0000 (22:29 -0800)
53 files changed:
branchrecord.cc
branchrecord.h
cgoal.h
change.h
cmodelint.cc
common.cc
common.h
config.h
constgen.cc
constgen.h
constraint.cc
constraint.h
context.cc
context.h
eprecord.cc
eprecord.h
epvalue.h
equalsrecord.h
execpoint.cc
execpoint.h
functionrecord.cc
functionrecord.h
hashset.h
hashtable.h
inc_solver.cc
inc_solver.h
loadrf.cc
loadrf.h
main.cc
mcexecution.cc
mcexecution.h
mcschedule.cc
mcschedule.h
mcutil.h
model.cc
model.h
mymemory.cc
mymemory.h
output.h
params.h
planner.cc
planner.h
schedulebuilder.cc
schedulebuilder.h
snapshot-interface.cc
snapshot-interface.h
snapshot.cc
stacktrace.h
stl-model.h
storeloadset.h
threads-model.h
threads.cc
valuerecord.h

index e55aa24..c2c07b0 100644 (file)
@@ -54,6 +54,6 @@ int BranchRecord::getBranchValue(bool * array) {
        }
        if (!alwaysexecuted)
                value--;
-       
+
        return value;
 }
index aa5e4a2..1cc1152 100644 (file)
@@ -12,7 +12,7 @@
 #include "classlist.h"
 
 class BranchRecord {
- public:
+public:
        BranchRecord(EPRecord *record, uint numvars, Constraint **vars, bool isalwaysexecuted);
        ~BranchRecord();
        Constraint * getAnyBranch();
@@ -22,12 +22,12 @@ class BranchRecord {
        int numDirections() {return numdirections;}
        bool hasNextRecord() {return hasNext;}
        MEMALLOC;
- private:
-  EPRecord *branch;
+private:
+       EPRecord *branch;
        bool hasNext;
-  uint numvars;
+       uint numvars;
        uint numdirections;
        bool alwaysexecuted;
-  Constraint **vars;
+       Constraint **vars;
 };
 #endif
diff --git a/cgoal.h b/cgoal.h
index 3374062..e04fc4e 100644 (file)
--- a/cgoal.h
+++ b/cgoal.h
@@ -15,7 +15,7 @@
 #include <stdint.h>
 
 class CGoal {
- public:
+public:
        CGoal(unsigned int num, uint64_t *vals);
        ~CGoal();
        unsigned int getNum() {return num;}
@@ -25,12 +25,12 @@ class CGoal {
        void print();
 
        MEMALLOC;
- private:
+private:
        uint64_t * valarray;
        uint64_t outputvalue;
        unsigned int num;
        unsigned int hash;
-       
+
        friend bool CGoalEquals(CGoal *cg1, CGoal *cg2);
        friend unsigned int CGoalHash(CGoal *cg);
 };
index f2e0bef..dc539f1 100644 (file)
--- a/change.h
+++ b/change.h
@@ -15,7 +15,7 @@
 #include "eprecord.h"
 
 class MCChange {
- public:
+public:
        MCChange(EPRecord *record, uint64_t _val, unsigned int _index);
        ~MCChange();
        EPRecord *getRecord() {return record;}
@@ -29,7 +29,7 @@ class MCChange {
        void print();
        MEMALLOC;
 
- private:
+private:
        EPRecord *record;
        uint64_t val;
        unsigned int index;
index 2c95808..549376a 100644 (file)
@@ -13,7 +13,7 @@
 
 /** Performs a read action.*/
 uint64_t model_read_action(void * obj, memory_order ord) {
-  return -1;
+       return -1;
 }
 
 /** Performs a write action.*/
@@ -30,7 +30,7 @@ void model_init_action(void * obj, uint64_t val) {
  * a write.
  */
 uint64_t model_rmwr_action(void *obj, memory_order ord) {
-  return -1;
+       return -1;
 }
 
 /** Performs the write part of a RMW action. */
index b445ce3..4227122 100644 (file)
--- a/common.cc
+++ b/common.cc
@@ -43,11 +43,11 @@ void print_trace(void)
 
        model_print("\nDumping stack trace (%d frames):\n", size);
 
-       for (i = 0; i < size; i++)
+       for (i = 0;i < size;i++)
                model_print("\t%s\n", strings[i]);
 
        free(strings);
-#endif /* CONFIG_STACKTRACE */
+#endif/* CONFIG_STACKTRACE */
 }
 
 void assert_hook(void)
@@ -65,7 +65,7 @@ void model_assert(bool expr, const char *file, int line)
 
 #ifndef CONFIG_DEBUG
 
-static int fd_user_out; /**< @brief File descriptor from which to read user program output */
+static int fd_user_out;        /**< @brief File descriptor from which to read user program output */
 
 /**
  * @brief Setup output redirecting
@@ -147,7 +147,7 @@ void clear_program_output()
 {
        fflush(stdout);
        char buf[200];
-       while (read_to_buf(fd_user_out, buf, sizeof(buf)));
+       while (read_to_buf(fd_user_out, buf, sizeof(buf))) ;
 }
 
 /** @brief Print out any pending program output */
@@ -178,4 +178,4 @@ void print_program_output()
 
        model_print("---- END PROGRAM OUTPUT   ----\n");
 }
-#endif /* ! CONFIG_DEBUG */
+#endif/* ! CONFIG_DEBUG */
index 89b59b4..d4d86c6 100644 (file)
--- a/common.h
+++ b/common.h
@@ -21,16 +21,16 @@ extern int model_out;
 extern int model_err;
 extern int switch_alloc;
 
-#define model_dprintf(fd, fmt, ...) do { switch_alloc = 1; dprintf(fd, fmt, ##__VA_ARGS__); switch_alloc = 0; } while (0)
+#define model_dprintf(fd, fmt, ...) do { switch_alloc = 1; dprintf(fd, fmt, ## __VA_ARGS__); switch_alloc = 0; } while (0)
 
-#define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ##__VA_ARGS__); } while (0)
+#define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ## __VA_ARGS__); } while (0)
 
-#define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ##__VA_ARGS__); } while (0)
+#define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0)
 
 
 
 #ifdef CONFIG_DEBUG
-#define DEBUG(fmt, ...) do { model_print("*** %15s:%-4d %25s() *** " fmt, __FILE__, __LINE__, __func__, ##__VA_ARGS__); } while (0)
+#define DEBUG(fmt, ...) do { model_print("*** %15s:%-4d %25s() *** " fmt, __FILE__, __LINE__, __func__, ## __VA_ARGS__); } while (0)
 #define DBG() DEBUG("\n")
 #define DBG_ENABLED() (1)
 #else
@@ -43,20 +43,20 @@ void assert_hook(void);
 
 #ifdef CONFIG_ASSERT
 #define ASSERT(expr) \
-do { \
-       if (!(expr)) { \
-               fprintf(stderr, "Error: assertion failed in %s at line %d\n", __FILE__, __LINE__); \
-               /* print_trace(); // Trace printing may cause dynamic memory allocation */ \
-               assert_hook();                           \
-               exit(EXIT_FAILURE); \
-       } \
-} while (0)
+       do { \
+               if (!(expr)) { \
+                       fprintf(stderr, "Error: assertion failed in %s at line %d\n", __FILE__, __LINE__); \
+                       /* print_trace(); // Trace printing may cause dynamic memory allocation */ \
+                       assert_hook();                           \
+                       exit(EXIT_FAILURE); \
+               } \
+       } while (0)
 #else
 #define ASSERT(expr) \
        do { } while (0)
-#endif /* CONFIG_ASSERT */
+#endif/* CONFIG_ASSERT */
 
 #define error_msg(...) fprintf(stderr, "Error: " __VA_ARGS__)
 
 void print_trace(void);
-#endif /* __COMMON_H__ */
+#endif/* __COMMON_H__ */
index 9efd32e..6ec9b80 100644 (file)
--- a/config.h
+++ b/config.h
 #else
 #define BIT48 0
 #endif
-#endif /* BIT48 */
+#endif/* BIT48 */
 
 /** Snapshotting configurables */
 
-/** 
+/**
  * If USE_MPROTECT_SNAPSHOT=2, then snapshot by tuned mmap() algorithm
  * If USE_MPROTECT_SNAPSHOT=1, then snapshot by using mmap() and mprotect()
  * If USE_MPROTECT_SNAPSHOT=0, then snapshot by using fork() */
index 2f3375b..4f4ec3a 100644 (file)
@@ -92,7 +92,7 @@ ConstGen::~ConstGen() {
 
 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;
@@ -106,7 +106,7 @@ void resetstoreloadtable(StoreLoadSetHashTable * storeloadtable) {
                        delete storeloadtable->zero->val;
                } else
                        ASSERT(false);
-               model_free(storeloadtable -> zero);
+               model_free(storeloadtable->zero);
                storeloadtable->zero = NULL;
        }
        storeloadtable->size = 0;
@@ -182,11 +182,11 @@ bool ConstGen::canReuseEncoding() {
 #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];
@@ -215,7 +215,7 @@ bool ConstGen::process() {
                delete solver;
                solver = NULL;
        }
-       
+
        solver=new IncrementalSolver();
 
        traverse(true);
@@ -279,13 +279,13 @@ bool ConstGen::process() {
        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];
@@ -309,7 +309,7 @@ void ConstGen::printEventGraph() {
        schedule_graph++;
        int file=open(buffer,O_WRONLY|O_CREAT|O_TRUNC, S_IRWXU);
        model_dprintf(file, "digraph eventgraph {\n");
-       
+
        EPRecord *first=execution->getEPRecord(MCID_FIRST);
        printRecord(first, file);
        while(!workstack->empty()) {
@@ -328,7 +328,7 @@ void ConstGen::doPrint(EPRecord *record, int file) {
        model_dprintf(file, "\"];\n");
        if (record->getNextRecord()!=NULL)
                model_dprintf(file, "%lu->%lu;\n", (uintptr_t) record, (uintptr_t) record->getNextRecord());
-       
+
        if (record->getChildRecord()!=NULL)
                model_dprintf(file, "%lu->%lu[color=red];\n", (uintptr_t) record, (uintptr_t) record->getChildRecord());
 }
@@ -357,7 +357,7 @@ void ConstGen::printRecord(EPRecord *record, int file) {
                                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) {
@@ -385,13 +385,13 @@ void ConstGen::traverse(bool initial) {
 }
 
 /** 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 */
@@ -432,18 +432,18 @@ RecordSet * ConstGen::computeConflictSet(EPRecord *store, EPRecord *load, Record
                }
        }
        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();
@@ -455,7 +455,7 @@ RecordSet * ConstGen::computeConflictSet(EPRecord *store, EPRecord *load, Record
                                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);
 
@@ -483,7 +483,7 @@ RecordSet * ConstGen::computeConflictSet(EPRecord *store, EPRecord *load, Record
                                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))
@@ -502,7 +502,7 @@ RecordSet * ConstGen::computeConflictSet(EPRecord *store, EPRecord *load, Record
                        sri->remove();
                }
        }
-       
+
        delete sri;
        return srscopy;
 }
@@ -513,7 +513,7 @@ RecordSet * ConstGen::computeConflictSet(EPRecord *store, EPRecord *load, Record
 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();
@@ -523,7 +523,7 @@ RecordSet * ConstGen::getMayReadFromSet(EPRecord *load) {
 
                IntHashSet *addrset=load->getSet(VC_ADDRINDEX);
                IntIterator *ait=addrset->iterator();
-               
+
                while(ait->hasNext()) {
                        void *addr=(void *)ait->next();
                        RecordSet *rs=execution->getStoreTable(addr);
@@ -594,7 +594,7 @@ RecordSet * ConstGen::getMayReadFromSetOpt(EPRecord *load) {
 }
 
 /** This function merges two recordsets and updates the storeloadtable
-               accordingly. */
+                accordingly. */
 
 void ConstGen::mergeSets(StoreLoadSet *to, StoreLoadSet *from) {
        RecordIterator * sri=from->iterator();
@@ -628,7 +628,7 @@ void ConstGen::insertTSOAction(EPRecord *load) {
        while (j>0) {
                EPRecord *oldrec=(*vector)[--j];
                EventType oldrec_t=oldrec->getType();
-               
+
                if (((oldrec_t == RMW) || (oldrec_t==FENCE)) &&
                                isAlwaysExecuted(oldrec)) {
                        return;
@@ -681,7 +681,7 @@ void ConstGen::genTSOTransOrderConstraints() {
 #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();
@@ -732,15 +732,15 @@ void ConstGen::genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVe
                        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);
@@ -761,7 +761,7 @@ void ConstGen::genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVe
                                Constraint *intratransorder=new Constraint(OR, c21, c13);
 #endif
                                ADDCONSTRAINT(intratransorder,"intratransorder");
-               }
+                       }
 
                        for(uint t0i=0;t0i<t1i;t0i++) {
                                EPRecord *t0rec=(*t1vec)[t0i];
@@ -784,7 +784,7 @@ void ConstGen::genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVe
                                Constraint *intratransorder=new Constraint(OR, c21, c02);
 #endif
                                ADDCONSTRAINT(intratransorder,"intratransorder");
-               }
+                       }
                }
        }
 }
@@ -865,7 +865,7 @@ void ConstGen::printNegConstraint(uint value) {
 void ConstGen::printConstraint(uint value) {
        solver->addClauseLiteral(value);
 }
-       
+
 bool * ConstGen::runSolver() {
        int solution=solver->solve();
        if (solution == IS_UNSAT) {
@@ -964,7 +964,7 @@ bool ConstGen::orderThread(EPRecord *first, EPRecord *second) {
        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;
        }
@@ -1027,7 +1027,7 @@ StoreLoadSet * ConstGen::getStoreLoadSet(EPRecord *record) {
 }
 
 /** 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()) {
@@ -1083,7 +1083,7 @@ bool ConstGen::subsumesExecutionConstraint(EPRecord *recordsubsumes, EPRecord *r
                RecordIterator *sri=srs->iterator();
                while(sri->hasNext()) {
                        EPRecord *rec=sri->next();
-               
+
                        if (!getOrderConstraint(rec, record)->isTrue()) {
                                delete sri;
                                return false;
@@ -1097,7 +1097,7 @@ bool ConstGen::subsumesExecutionConstraint(EPRecord *recordsubsumes, EPRecord *r
 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++;
 
@@ -1128,7 +1128,7 @@ Constraint * ConstGen::getExecutionConstraint(EPRecord *record) {
 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++;
 
@@ -1165,7 +1165,7 @@ void ConstGen::processBranch(EPRecord *record) {
                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);
@@ -1173,7 +1173,7 @@ void ConstGen::processBranch(EPRecord *record) {
        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,
@@ -1186,7 +1186,7 @@ void ConstGen::processBranch(EPRecord *record) {
                                        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++) {
@@ -1224,7 +1224,7 @@ void ConstGen::processLoad(EPRecord *record) {
 }
 
 /** 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);
@@ -1242,7 +1242,7 @@ void ConstGen::processAddresses(EPRecord *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);
@@ -1279,7 +1279,7 @@ void ConstGen::processCAS(EPRecord *record) {
                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);
@@ -1324,7 +1324,7 @@ void ConstGen::processCAS(EPRecord *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);
@@ -1340,11 +1340,11 @@ void ConstGen::processCAS(EPRecord *record) {
                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);
 }
 
@@ -1365,7 +1365,7 @@ void ConstGen::processEXC(EPRecord *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);
@@ -1387,7 +1387,7 @@ void ConstGen::processAdd(EPRecord *record) {
        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();
@@ -1428,7 +1428,7 @@ void ConstGen::processAdd(EPRecord *record) {
                                        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");
                                }
                        }
@@ -1441,10 +1441,10 @@ void ConstGen::processAdd(EPRecord *record) {
 }
 
 /** 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);
@@ -1458,7 +1458,7 @@ void ConstGen::processStore(EPRecord *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);
@@ -1488,7 +1488,7 @@ void ConstGen::processLoopPhi(EPRecord *record) {
        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();
@@ -1509,7 +1509,7 @@ void ConstGen::processPhi(EPRecord *record) {
        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();
@@ -1585,30 +1585,30 @@ void ConstGen::processFunction(EPRecord *record) {
 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();
@@ -1632,20 +1632,20 @@ void ConstGen::processEquals(EPRecord *record) {
                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;
 
@@ -1655,12 +1655,12 @@ void ConstGen::processEquals(EPRecord *record) {
                        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;
 
@@ -1674,17 +1674,17 @@ void ConstGen::processEquals(EPRecord *record) {
                Constraint *functionimplication2=new Constraint(IMPLIES, outputtrue, l2);
                ADDCONSTRAINT(functionimplication2,"equalsimpl");
        }
-       
-       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");
                }
@@ -1750,7 +1750,7 @@ void ConstGen::processRecord(EPRecord *record) {
        case FENCE:
                processFence(record);
                break;
-#endif         
+#endif
        case RMW:
 #ifdef TSO
                processFence(record);
@@ -1831,7 +1831,7 @@ void ConstGen::visitRecord(EPRecord *record) {
 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();
@@ -1899,7 +1899,7 @@ void ConstGen::traverseRecord(EPRecord *record, bool initial) {
                                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)
@@ -1921,5 +1921,5 @@ unsigned int RecPairHash(RecPair *rp) {
 
 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));
 }
index 68c02e7..8669a7f 100644 (file)
@@ -46,7 +46,7 @@ struct MC_Stat {
 #endif
 
 class ConstGen {
- public:
+public:
        ConstGen(MCExecution *e);
        ~ConstGen();
        bool process();
@@ -71,13 +71,13 @@ class ConstGen {
 #ifdef STATS
        MC_Stat *curr_stat;
 #endif
-       
+
        MEMALLOC;
- private:
+private:
        Constraint * getRetValueEncoding(EPRecord *record, uint64_t value);
        Constraint * getMemValueEncoding(EPRecord *record, uint64_t value);
        bool subsumesExecutionConstraint(EPRecord *recordsubsumes, EPRecord *record);
-       
+
        void addBranchGoal(EPRecord *, Constraint *c);
        void addGoal(EPRecord *, Constraint *c);
        void translateGoals();
@@ -124,7 +124,7 @@ class ConstGen {
 #endif
 
        /** These functions build closed groups of memory operations that
-                       can store/load from each other. */
+                       can store/load from each other. */
        void groupMemoryOperations(EPRecord *op);
        void mergeSets(StoreLoadSet *to, StoreLoadSet *from);
 
@@ -136,10 +136,10 @@ class ConstGen {
        void genTransOrderConstraint(EPRecord *t1rec, EPRecord *t2rec, EPRecord *t3rec);
 
        /** The hashtable maps an address to the closure set of
-                       memory operations that may touch that address. */
+                       memory operations that may touch that address. */
        StoreLoadSetHashTable *storeloadtable;
        /** This hashtable maps a load to all of the stores it may read
-                       from. */
+                       from. */
        LoadHashTable *loadtable;
 
        MCExecution *execution;
@@ -167,11 +167,11 @@ class ConstGen {
 };
 
 class RecPair {
- public:
- RecPair(EPRecord *r1, EPRecord *r2) :
-       epr1(r1),
-       epr2(r2),
-       constraint(NULL) {
+public:
      RecPair(EPRecord *r1, EPRecord *r2) :
+               epr1(r1),
+               epr2(r2),
+               constraint(NULL) {
        }
        EPRecord *epr1;
        EPRecord *epr2;
index 457eaab..0656a35 100644 (file)
@@ -22,11 +22,11 @@ Constraint::Constraint(CType t, Constraint *l, Constraint *r) :
 {
        ASSERT(l!=NULL);
        //if (type==IMPLIES) {
-               //type=OR;
+       //type=OR;
        //      operands[0]=l->negate();
-               //      } else {
-               operands[0]=l;
-               //      }
+       //      } else {
+       operands[0]=l;
+       //      }
        operands[1]=r;
 }
 
@@ -45,20 +45,20 @@ Constraint::Constraint(CType t, uint num, Constraint **array) :
        operands((Constraint **)model_malloc(num*sizeof(Constraint *))),
        neg(NULL)
 {
-  memcpy(operands, array, num*sizeof(Constraint *));
+       memcpy(operands, array, num*sizeof(Constraint *));
 }
 
 Constraint::Constraint(CType t) :
        type(t),
-  numoperandsorvar(0xffffffff),
-  operands(NULL),
+       numoperandsorvar(0xffffffff),
+       operands(NULL),
        neg(NULL)
 {
 }
 
 Constraint::Constraint(CType t, uint v) :
        type(t),
-  numoperandsorvar(v),
+       numoperandsorvar(v),
        operands(NULL),
        neg(NULL)
 {
@@ -153,7 +153,7 @@ void Constraint::print() {
                                        model_print(" v ");
                        }
                        operands[i]->print();
-    }
+               }
                model_print(")");
                break;
        case VAR:
@@ -193,7 +193,7 @@ Constraint * Constraint::clone() {
 Constraint * generateConstraint(uint numvars, Constraint ** vars, uint value) {
        Constraint *carray[numvars];
        for(uint j=0;j<numvars;j++) {
-               carray[j]=((value&1)==1)?vars[j]:vars[j]->negate();
+               carray[j]=((value&1)==1) ? vars[j] : vars[j]->negate();
                value=value>>1;
        }
 
@@ -220,7 +220,7 @@ Constraint * generateLTConstraint(ConstGen *cg, uint numvars, Constraint ** vars
                }
                andarray[andi++]=new Constraint(OR, ori, orarray);
 
-               value=value+(1<<(__builtin_ctz(value)));//flip the last one
+               value=value+(1<<(__builtin_ctz(value)));                                                //flip the last one
        }
 }
 
@@ -345,7 +345,7 @@ ModelVector<Constraint *> * Constraint::simplify() {
                        }
                        case AND: {
                                Constraint *array[numoperandsorvar];
-                               
+
                                ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
                                for(uint j=0;j<c->numoperandsorvar;j++) {
                                        //copy other elements
@@ -413,7 +413,7 @@ Constraint * Constraint::negate() {
                for(uint i=0;i<numoperandsorvar;i++) {
                        operands[i]=operands[i]->negate();
                }
-               type=(type==AND)?OR:AND;
+               type=(type==AND) ? OR : AND;
                return this;
        }
        default:
index bf97b31..4bfdd6b 100644 (file)
@@ -19,7 +19,7 @@ enum ConstraintType {
 typedef enum ConstraintType CType;
 
 class Constraint {
- public:
+public:
        Constraint(CType t, Constraint *l, Constraint *r);
        Constraint(CType t, Constraint *l);
        Constraint(CType t, uint num, Constraint ** array);
@@ -40,7 +40,7 @@ class Constraint {
        Constraint *negate();
 
        MEMALLOC;
- private:
+private:
        CType type;
        uint numoperandsorvar;
        Constraint ** operands;
index 7081656..56c3acb 100644 (file)
@@ -33,4 +33,4 @@ int model_swapcontext(ucontext_t *oucp, ucontext_t *ucp)
        return 0;
 }
 
-#endif /* MAC */
+#endif/* MAC */
index 948d89f..7160f49 100644 (file)
--- a/context.h
+++ b/context.h
 
 int model_swapcontext(ucontext_t *oucp, ucontext_t *ucp);
 
-#else /* !MAC */
+#else  /* !MAC */
 
 static inline int model_swapcontext(ucontext_t *oucp, ucontext_t *ucp)
 {
        return swapcontext(oucp, ucp);
 }
 
-#endif /* !MAC */
+#endif/* !MAC */
 
-#endif /* __CONTEXT_H__ */
+#endif/* __CONTEXT_H__ */
index a11d2d6..a87167e 100644 (file)
@@ -191,7 +191,7 @@ void EPRecord::print(int f) {
                delete it;
        }
 
-       
+
        execpoint->print(f);
 }
 
index 1d5e23a..54069de 100644 (file)
 typedef ModelVector<EPValue *> ValueVector;
 const char * eventToStr(EventType event);
 struct RecordIDPair {
-       EPRecord *record;
+       EPRecord *record;
        EPRecord *idrecord;
 };
 
 inline unsigned int RIDP_hash_function(struct RecordIDPair * pair) {
-  return (unsigned int)(((uintptr_t)pair->record) >> 4) ^ ((uintptr_t)pair->idrecord);
+       return (unsigned int)(((uintptr_t)pair->record) >> 4) ^ ((uintptr_t)pair->idrecord);
 }
 
 inline bool RIDP_equals(struct RecordIDPair * key1, struct RecordIDPair * key2) {
        if (key1==NULL)
                return key1==key2;
-  return key1->record == key2->record && key1->idrecord == key2->idrecord;
+       return key1->record == key2->record && key1->idrecord == key2->idrecord;
 }
 
 typedef HashSet<struct RecordIDPair *, uintptr_t, 0, model_malloc, model_calloc, model_free, RIDP_hash_function, RIDP_equals> EPRecordIDSet;
@@ -39,7 +39,7 @@ typedef HashSet<struct RecordIDPair *, uintptr_t, 0, model_malloc, model_calloc,
 typedef HSIterator<struct RecordIDPair *, uintptr_t, 0, model_malloc, model_calloc, model_free, RIDP_hash_function, RIDP_equals> EPRecordIDIterator;
 
 class EPRecord {
- public:
+public:
        EPRecord(EventType event, ExecPoint *execpoint, EPValue *branch, uintptr_t _offset, unsigned int numinputs,uint len,  bool anyvalue = false);
        ~EPRecord();
        ExecPoint * getEP() {return execpoint;}
@@ -83,8 +83,8 @@ class EPRecord {
        bool isSharedGoals() {return func_shares_goalset;}
        uintptr_t getOffset() {return offset;}
        MEMALLOC;
-               
- private:
+
+private:
        ValueVector * valuevector;
        ExecPoint * execpoint;
        CGoalSet *completed;
index 5d3a85b..13ceea8 100644 (file)
--- a/epvalue.h
+++ b/epvalue.h
@@ -23,7 +23,7 @@
 #define VC_FUNCOUTINDEX 1
 
 class EPValue {
- public:
+public:
        EPValue(ExecPoint *, EPRecord *, const void *addr, uint64_t value, int len);
        ~EPValue();
        uint64_t getValue() {return value;}
@@ -34,9 +34,9 @@ class EPValue {
        EPRecord *firstrecord;
        EPRecord *lastrecord;
        EPRecord * getRecord() {return record;}
-       
+
        MEMALLOC;
- private:
+private:
        ExecPoint * execpoint;
        EPRecord *record;
        const void *addr;
index 14968ba..f5e66a3 100644 (file)
 #include "classlist.h"
 
 class EqualsRecord {
- public:
+public:
        EqualsRecord(ConstGen *cg, EPRecord *func);
        ~EqualsRecord();
        Constraint * getValueEncoding(uint64_t val);
        EPRecord *getRecord() {return equals;}
 
        MEMALLOC;
- private:
+private:
        EPRecord *equals;
-  Constraint *vars;
+       Constraint *vars;
 };
 #endif
index 7b63213..7cfdff5 100644 (file)
@@ -43,15 +43,15 @@ void ExecPoint::reset() {
 }
 
 /** Return CR_AFTER means that ep occurs after this.
-               Return CR_BEFORE means tha te occurs before this.
-               Return CR_EQUALS means that they are the same point.
-               Return CR_INCOMPARABLE means that they are not comparable.
-*/
+                Return CR_BEFORE means tha te occurs before this.
+                Return CR_EQUALS means that they are the same point.
+                Return CR_INCOMPARABLE means that they are not comparable.
+ */
 
 CompareResult ExecPoint::compare(const ExecPoint * ep) const {
        if (this==ep)
                return CR_EQUALS;
-       unsigned int minsize=(size<ep->size)?size:ep->size;
+       unsigned int minsize=(size<ep->size) ? size : ep->size;
        for(unsigned int i=0;i<minsize;i+=2) {
                ASSERT(pairarray[i]==ep->pairarray[i]);
                if (pairarray[i+1]!=ep->pairarray[i+1]) {
@@ -122,7 +122,7 @@ bool ExecPointEquals(ExecPoint *e1, ExecPoint * e2) {
                return e2==NULL;
        if (e1->tid != e2->tid || e1->size != e2->size || e1->hashvalue != e2->hashvalue)
                return false;
-       for(unsigned int i=0; i<e1->size; i++) {
+       for(unsigned int i=0;i<e1->size;i++) {
                if (e1->pairarray[i]!=e2->pairarray[i])
                        return false;
        }
index 74344ea..74650ed 100644 (file)
@@ -21,7 +21,7 @@ enum ExecPointType {EP_BRANCH, EP_COUNTER, EP_LOOP};
 enum CompareResult {CR_BEFORE, CR_AFTER, CR_EQUALS, CR_INCOMPARABLE};
 
 class ExecPoint {
- public:
+public:
        ExecPoint(int length, thread_id_t thread_id);
        ExecPoint(ExecPoint * e);
        ~ExecPoint();
@@ -40,7 +40,7 @@ class ExecPoint {
        void print();
        void print(int f);
        MEMALLOC;
- private:
+private:
        unsigned int length;
        unsigned int size;
        execcount_t * pairarray;
index a7576b7..f9ff51f 100644 (file)
@@ -20,7 +20,7 @@ FunctionRecord::FunctionRecord(ConstGen *cg, EPRecord *func) : function(func) {
                cg->getArrayNewVars(numvars, vars);
        } else {
                uint numvals=function->getSet(VC_FUNCOUTINDEX)->getSize();
-               numvals++;//allow for new combinations in sat formulas
+               numvals++;                                              //allow for new combinations in sat formulas
                numvars=NUMBITS(numvals-1);
                vars=(Constraint **)model_malloc(numvars*sizeof(Constraint *));
                cg->getArrayNewVars(numvars, vars);
index a7ecce8..5db5132 100644 (file)
 #include "classlist.h"
 
 class FunctionRecord {
- public:
+public:
        FunctionRecord(ConstGen *cg, EPRecord *func);
        ~FunctionRecord();
        Constraint * getValueEncoding(uint64_t val);
        Constraint * getNoValueEncoding();
 
        MEMALLOC;
- private:
+private:
        EPRecord *function;
-  Constraint **vars;
+       Constraint **vars;
        uint numvars;
 };
 #endif
index ecda268..140b85f 100644 (file)
--- a/hashset.h
+++ b/hashset.h
@@ -18,204 +18,204 @@ struct LinkNode {
        LinkNode<_Key> *next;
 };
 
-template<typename _Key, typename _KeyInt, int _Shift, void * 
-(* _malloc)(size_t), void * (* _calloc)(size_t, size_t), void (*_free)(void *), unsigned int (*hash_function
-)(_Key), bool (*equals)(_Key, _Key)>
+template<typename _Key, typename _KeyInt, int _Shift, void *
+                                (* _malloc)(size_t), void * (* _calloc)(size_t, size_t), void (*_free)(void *), unsigned int (*hash_function
+                                                                                                                                                                                                                                                                                                                                                                                                                        )(_Key), bool (*equals)(_Key, _Key)>
 class HashSet;
 
 template<typename _Key, typename _KeyInt, int _Shift, void * (* _malloc)(size_t), void * (* _calloc)(size_t, size_t), void (*_free)(void *), unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = default_equals<_Key> >
 class HSIterator {
- public:
- HSIterator(LinkNode<_Key> *_curr, HashSet <_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * _set) :
-       curr(_curr),
-       set(_set) 
- {
- }
-
- /** Override: new operator */
- void * operator new(size_t size) {
-        return _malloc(size);
- }
- /** Override: delete operator */
- void operator delete(void *p, size_t size) {
-        _free(p);
- }
- /** Override: new[] operator */
- void * operator new[](size_t size) {
-        return _malloc(size);
- }
-
- /** Override: delete[] operator */
- void operator delete[](void *p, size_t size) {
-        _free(p);
- }
- bool hasNext() {
-        return curr!=NULL;
- }
-
- _Key next() {
-        _Key k=curr->key;
-        last=curr;
-        curr=curr->next;
-        return k;
- }
-
- _Key currKey() {
-        return last->key;
- }
-
- void remove() {
-        _Key k=last->key;
-        set->remove(k);
- }
-
- private:
- LinkNode<_Key> *curr;
- LinkNode<_Key> *last;
- HashSet <_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * set;
+public:
      HSIterator(LinkNode<_Key> *_curr, HashSet <_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * _set) :
+               curr(_curr),
+               set(_set)
      {
      }
+
      /** Override: new operator */
      void * operator new(size_t size) {
+               return _malloc(size);
      }
+
      /** Override: delete operator */
      void operator delete(void *p, size_t size) {
+               _free(p);
      }
+
      /** Override: new[] operator */
      void * operator new[](size_t size) {
+               return _malloc(size);
      }
+
      /** Override: delete[] operator */
      void operator delete[](void *p, size_t size) {
+               _free(p);
      }
+
      bool hasNext() {
+               return curr!=NULL;
      }
+
      _Key next() {
+               _Key k=curr->key;
+               last=curr;
+               curr=curr->next;
+               return k;
      }
+
      _Key currKey() {
+               return last->key;
      }
+
      void remove() {
+               _Key k=last->key;
+               set->remove(k);
      }
+
+private:
      LinkNode<_Key> *curr;
      LinkNode<_Key> *last;
      HashSet <_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * set;
 };
 
 template<typename _Key, typename _KeyInt, int _Shift = 0, void * (* _malloc)(size_t) = snapshot_malloc, void * (* _calloc)(size_t, size_t) = snapshot_calloc, void (*_free)(void *) = snapshot_free, unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = default_equals<_Key> >
 class HashSet {
- public:
- HashSet(unsigned int initialcapacity = 16, double factor = 0.5) :
- table(new HashTable<_Key, LinkNode<_Key> *, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals>(initialcapacity, factor)),
- list(NULL),
- tail(NULL)
- {
- }
-       
- /** @brief Hashset destructor */
- ~HashSet() {
-        LinkNode<_Key> *tmp=list;
-        while(tmp!=NULL) {
-                LinkNode<_Key> *tmpnext=tmp->next;
-                _free(tmp);
-                tmp=tmpnext;
-        }
-        delete table;
- }
-
- HashSet<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * copy() {
-        HashSet<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> *copy=new HashSet<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals>(table->getCapacity(), table->getLoadFactor());
-        HSIterator<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * it=iterator();
-        while(it->hasNext())
-                copy->add(it->next());
-        delete it;
-        return copy;
- }
- void reset() {
-        LinkNode<_Key> *tmp=list;
-        while(tmp!=NULL) {
-                LinkNode<_Key> *tmpnext=tmp->next;
-                _free(tmp);
-                tmp=tmpnext;
-        }
-        list=tail=NULL;
-        table->reset();
- }
-
- /** @brief Adds a new key to the hashset.  Returns false if the key
-       *  is already present. */
-
- bool add(_Key key) {
-        LinkNode<_Key> * val=table->get(key);
-        if (val==NULL) {
-                LinkNode<_Key> * newnode=(LinkNode<_Key> *) _malloc(sizeof(struct LinkNode<_Key>));
-                newnode->prev=tail;
-                newnode->next=NULL;
-                newnode->key=key;
-                if (tail!=NULL)
-                        tail->next=newnode;
-                else
-                        list=newnode;
-                tail=newnode;
-                table->put(key, newnode);
-                return true;
-        } else
-                return false;
- }
-
- /** @brief Gets the original key corresponding to this one from the
-       *  hashset.  Returns NULL if not present. */
-
- _Key get(_Key key) {
-        LinkNode<_Key> * val=table->get(key);
-        if (val!=NULL) 
-                return val->key;
-        else
-                return NULL;
- }
-
- _Key getFirstKey() {
-        return list->key;
- }
-
- bool contains(_Key key) {
-        return table->get(key)!=NULL;
- }
-
- bool remove(_Key key) {
-        LinkNode<_Key> * oldlinknode;
-        oldlinknode=table->get(key);
-        if (oldlinknode==NULL) {
-                return false;
-        }
-        table->remove(key);
-        
-        //remove link node from the list
-        if (oldlinknode->prev==NULL)
-                list=oldlinknode->next;
-        else
-                oldlinknode->prev->next=oldlinknode->next;
-        if (oldlinknode->next!=NULL)
-                oldlinknode->next->prev=oldlinknode->prev;
-        else
-                tail=oldlinknode->prev;
-                        _free(oldlinknode);
-        return true;
- }
-
- unsigned int getSize() {
-        return table->getSize();
- }
-
- bool isEmpty() {
-        return getSize()==0;
- }
-
- HSIterator<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * iterator() {
-        return new HSIterator<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals>(list, this);
- }
-
- /** Override: new operator */
- void * operator new(size_t size) {
-        return _malloc(size);
- }
- /** Override: delete operator */
- void operator delete(void *p, size_t size) {
-        _free(p);
- }
- /** Override: new[] operator */
- void * operator new[](size_t size) {
-        return _malloc(size);
- }
-
- /** Override: delete[] operator */
- void operator delete[](void *p, size_t size) {
-        _free(p);
- }
- private:
- HashTable<_Key, LinkNode<_Key>*, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * table;
- LinkNode<_Key> *list;
- LinkNode<_Key> *tail;
+public:
      HashSet(unsigned int initialcapacity = 16, double factor = 0.5) :
              table(new HashTable<_Key, LinkNode<_Key> *, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals>(initialcapacity, factor)),
              list(NULL),
              tail(NULL)
      {
      }
+
      /** @brief Hashset destructor */
      ~HashSet() {
+               LinkNode<_Key> *tmp=list;
+               while(tmp!=NULL) {
+                       LinkNode<_Key> *tmpnext=tmp->next;
+                       _free(tmp);
+                       tmp=tmpnext;
+               }
+               delete table;
      }
+
      HashSet<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * copy() {
+               HashSet<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> *copy=new HashSet<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals>(table->getCapacity(), table->getLoadFactor());
+               HSIterator<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * it=iterator();
+               while(it->hasNext())
+                       copy->add(it->next());
+               delete it;
+               return copy;
      }
+
      void reset() {
+               LinkNode<_Key> *tmp=list;
+               while(tmp!=NULL) {
+                       LinkNode<_Key> *tmpnext=tmp->next;
+                       _free(tmp);
+                       tmp=tmpnext;
+               }
+               list=tail=NULL;
+               table->reset();
      }
+
      /** @brief Adds a new key to the hashset.  Returns false if the key
+        *  is already present. */
+
      bool add(_Key key) {
+               LinkNode<_Key> * val=table->get(key);
+               if (val==NULL) {
+                       LinkNode<_Key> * newnode=(LinkNode<_Key> *)_malloc(sizeof(struct LinkNode<_Key>));
+                       newnode->prev=tail;
+                       newnode->next=NULL;
+                       newnode->key=key;
+                       if (tail!=NULL)
+                               tail->next=newnode;
+                       else
+                               list=newnode;
+                       tail=newnode;
+                       table->put(key, newnode);
+                       return true;
+               } else
+                       return false;
      }
+
      /** @brief Gets the original key corresponding to this one from the
+        *  hashset.  Returns NULL if not present. */
+
      _Key get(_Key key) {
+               LinkNode<_Key> * val=table->get(key);
+               if (val!=NULL)
+                       return val->key;
+               else
+                       return NULL;
      }
+
      _Key getFirstKey() {
+               return list->key;
      }
+
      bool contains(_Key key) {
+               return table->get(key)!=NULL;
      }
+
      bool remove(_Key key) {
+               LinkNode<_Key> * oldlinknode;
+               oldlinknode=table->get(key);
+               if (oldlinknode==NULL) {
+                       return false;
+               }
+               table->remove(key);
+
+               //remove link node from the list
+               if (oldlinknode->prev==NULL)
+                       list=oldlinknode->next;
+               else
+                       oldlinknode->prev->next=oldlinknode->next;
+               if (oldlinknode->next!=NULL)
+                       oldlinknode->next->prev=oldlinknode->prev;
+               else
+                       tail=oldlinknode->prev;
+               _free(oldlinknode);
+               return true;
      }
+
      unsigned int getSize() {
+               return table->getSize();
      }
+
      bool isEmpty() {
+               return getSize()==0;
      }
+
+
+
      HSIterator<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * iterator() {
+               return new HSIterator<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals>(list, this);
      }
+
      /** Override: new operator */
      void * operator new(size_t size) {
+               return _malloc(size);
      }
+
      /** Override: delete operator */
      void operator delete(void *p, size_t size) {
+               _free(p);
      }
+
      /** Override: new[] operator */
      void * operator new[](size_t size) {
+               return _malloc(size);
      }
+
      /** Override: delete[] operator */
      void operator delete[](void *p, size_t size) {
+               _free(p);
      }
+private:
      HashTable<_Key, LinkNode<_Key>*, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * table;
      LinkNode<_Key> *list;
      LinkNode<_Key> *tail;
 };
 #endif
index bcc8e70..16744bb 100644 (file)
@@ -34,12 +34,12 @@ struct hashlistnode {
 
 template<typename _Key, int _Shift, typename _KeyInt>
 inline unsigned int default_hash_function(_Key hash) {
-  return (unsigned int)(((_KeyInt)hash) >> _Shift);
+       return (unsigned int)(((_KeyInt)hash) >> _Shift);
 }
 
 template<typename _Key>
 inline bool default_equals(_Key key1, _Key key2) {
-  return key1 == key2;
+       return key1 == key2;
 }
 
 /**
@@ -64,7 +64,7 @@ inline bool default_equals(_Key key1, _Key key2) {
  */
 template<typename _Key, typename _Val, typename _KeyInt, int _Shift = 0, void * (* _malloc)(size_t) = snapshot_malloc, void * (* _calloc)(size_t, size_t) = snapshot_calloc, void (*_free)(void *) = snapshot_free, unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = default_equals<_Key> >
 class HashTable {
- public:
+public:
        /**
         * @brief Hash table constructor
         * @param initialcapacity Sets the initial capacity of the hash table.
@@ -81,7 +81,7 @@ class HashTable {
                capacitymask = initialcapacity - 1;
 
                threshold = (unsigned int)(initialcapacity * loadfactor);
-               size = 0; // Initial number of elements in the hash
+               size = 0;                                                       // Initial number of elements in the hash
        }
 
        /** @brief Hash table destructor */
@@ -121,46 +121,46 @@ class HashTable {
                size = 0;
        }
 
- void resetanddelete() {
-        for(unsigned int i=0;i<capacity;i++) {
-                struct hashlistnode<_Key, _Val> *bin = &table[i];
-                if (bin->key != NULL) {
-                        bin->key = NULL;
-                        if (bin->val != NULL) {
-                                delete bin->val;
-                                bin->val = NULL;
-                        }
-                }
-        }
-        if (zero) {
-                if (zero->val != NULL)
-                        delete zero->val;
-                _free(zero);
-                zero = NULL;
-        }
-        size = 0;
- }
-
-  void resetandfree() {
-        for(unsigned int i=0;i<capacity;i++) {
-                struct hashlistnode<_Key, _Val> *bin = &table[i];
-                if (bin->key != NULL) {
-                        bin->key = NULL;
-                        if (bin->val != NULL) {
-                                _free(bin->val);
-                                bin->val = NULL;
-                        }
-                }
-        }
-        if (zero) {
-                if (zero->val != NULL)
-                        _free(zero->val);
-                _free(zero);
-                zero = NULL;
-        }
-        size = 0;
- }
      void resetanddelete() {
+               for(unsigned int i=0;i<capacity;i++) {
+                       struct hashlistnode<_Key, _Val> *bin = &table[i];
+                       if (bin->key != NULL) {
+                               bin->key = NULL;
+                               if (bin->val != NULL) {
+                                       delete bin->val;
+                                       bin->val = NULL;
+                               }
+                       }
+               }
+               if (zero) {
+                       if (zero->val != NULL)
+                               delete zero->val;
+                       _free(zero);
+                       zero = NULL;
+               }
+               size = 0;
      }
+
+       void resetandfree() {
+               for(unsigned int i=0;i<capacity;i++) {
+                       struct hashlistnode<_Key, _Val> *bin = &table[i];
+                       if (bin->key != NULL) {
+                               bin->key = NULL;
+                               if (bin->val != NULL) {
+                                       _free(bin->val);
+                                       bin->val = NULL;
+                               }
+                       }
+               }
+               if (zero) {
+                       if (zero->val != NULL)
+                               _free(zero->val);
+                       _free(zero);
+                       zero = NULL;
+               }
+               size = 0;
      }
+
        /**
         * @brief Put a key/value pair into the table
         * @param key The key for the new value; must not be 0 or NULL
@@ -182,7 +182,7 @@ class HashTable {
                        resize(capacity << 1);
 
                struct hashlistnode<_Key, _Val> *search;
-               
+
                unsigned int index = hash_function(key);
                do {
                        index &= capacitymask;
@@ -227,8 +227,8 @@ class HashTable {
                                if (!search->val)
                                        break;
                        } else
-                               if (equals(search->key, key))
-                                       return search->val;
+                       if (equals(search->key, key))
+                               return search->val;
                        index++;
                        index &= capacitymask;
                        if (index==oindex)
@@ -258,7 +258,7 @@ class HashTable {
                        }
                }
 
-               
+
                unsigned int index = hash_function(key);
                do {
                        index &= capacitymask;
@@ -267,23 +267,23 @@ class HashTable {
                                if (!search->val)
                                        break;
                        } else
-                               if (equals(search->key, key)) {
-                                       _Val v=search->val;
-                                       //empty out this bin
-                                       search->val=(_Val) 1;
-                                       search->key=0;
-                                       size--;
-                                       return v;
-                               }
+                       if (equals(search->key, key)) {
+                               _Val v=search->val;
+                               //empty out this bin
+                               search->val=(_Val) 1;
+                               search->key=0;
+                               size--;
+                               return v;
+                       }
                        index++;
                } while (true);
                return (_Val)0;
        }
 
-  unsigned int getSize() const {
+       unsigned int getSize() const {
                return size;
        }
+
 
        /**
         * @brief Check whether the table contains a value for the given key
@@ -306,8 +306,8 @@ class HashTable {
                                if (!search->val)
                                        break;
                        } else
-                               if (equals(search->key, key))
-                                       return true;
+                       if (equals(search->key, key))
+                               return true;
                        index++;
                } while (true);
                return false;
@@ -327,7 +327,7 @@ class HashTable {
                        exit(EXIT_FAILURE);
                }
 
-               table = newtable;          // Update the global hashtable upon resize()
+               table = newtable;                                                                                       // Update the global hashtable upon resize()
                capacity = newsize;
                capacitymask = newsize - 1;
 
@@ -335,7 +335,7 @@ class HashTable {
 
                struct hashlistnode<_Key, _Val> *bin = &oldtable[0];
                struct hashlistnode<_Key, _Val> *lastbin = &oldtable[oldcapacity];
-               for (; bin < lastbin; bin++) {
+               for (;bin < lastbin;bin++) {
                        _Key key = bin->key;
 
                        struct hashlistnode<_Key, _Val> *search;
@@ -353,18 +353,18 @@ class HashTable {
                        search->val = bin->val;
                }
 
-               _free(oldtable);            // Free the memory of the old hash table
+               _free(oldtable);                                                                                                // Free the memory of the old hash table
        }
-  double getLoadFactor() {return loadfactor;}
-  unsigned int getCapacity() {return capacity;}
-  struct hashlistnode<_Key, _Val> *table;
-  struct hashlistnode<_Key, _Val> *zero;
-  unsigned int capacity;
+       double getLoadFactor() {return loadfactor;}
+       unsigned int getCapacity() {return capacity;}
+       struct hashlistnode<_Key, _Val> *table;
+       struct hashlistnode<_Key, _Val> *zero;
+       unsigned int capacity;
        unsigned int size;
- private:
+private:
        unsigned int capacitymask;
        unsigned int threshold;
-  double loadfactor;
+       double loadfactor;
 };
 
-#endif /* __HASHTABLE_H__ */
+#endif/* __HASHTABLE_H__ */
index daeeb1e..97f050c 100644 (file)
 #include <fcntl.h>
 
 IncrementalSolver::IncrementalSolver() :
-  buffer((int *)model_malloc(sizeof(int)*IS_BUFFERSIZE)),
-  solution(NULL),
-  solutionsize(0),
-  offset(0)
+       buffer((int *)model_malloc(sizeof(int)*IS_BUFFERSIZE)),
+       solution(NULL),
+       solutionsize(0),
+       offset(0)
 {
-  createSolver();
+       createSolver();
 }
 
 IncrementalSolver::~IncrementalSolver() {
-  killSolver();
-  model_free(buffer);
+       killSolver();
+       model_free(buffer);
        if (solution != NULL)
                model_free(solution);
 }
 
 void IncrementalSolver::reset() {
-  killSolver();
-  offset = 0;
-  createSolver();
+       killSolver();
+       offset = 0;
+       createSolver();
 }
 
 void IncrementalSolver::addClauseLiteral(int literal) {
-  buffer[offset++]=literal;
-  if (offset==IS_BUFFERSIZE) {
-    flushBuffer();
-  }
+       buffer[offset++]=literal;
+       if (offset==IS_BUFFERSIZE) {
+               flushBuffer();
+       }
 }
 
 void IncrementalSolver::finishedClauses() {
-  addClauseLiteral(0);
+       addClauseLiteral(0);
 }
 
 void IncrementalSolver::freeze(int variable) {
-  addClauseLiteral(IS_FREEZE);
-  addClauseLiteral(variable);
+       addClauseLiteral(IS_FREEZE);
+       addClauseLiteral(variable);
 }
 
 int IncrementalSolver::solve() {
-  //add an empty clause
+       //add an empty clause
        startSolve();
        return getSolution();
 }
 
-       
+
 void IncrementalSolver::startSolve() {
        addClauseLiteral(IS_RUNSOLVER);
-  flushBuffer();
+       flushBuffer();
 }
 
 int IncrementalSolver::getSolution() {
        int result=readIntSolver();
-  if (result == IS_SAT) {
-    int numVars=readIntSolver();
-    if (numVars > solutionsize) {
-      if (solution != NULL)
-        model_free(solution);
-      solution = (int *) model_malloc((numVars+1)*sizeof(int));
+       if (result == IS_SAT) {
+               int numVars=readIntSolver();
+               if (numVars > solutionsize) {
+                       if (solution != NULL)
+                               model_free(solution);
+                       solution = (int *) model_malloc((numVars+1)*sizeof(int));
                        solution[0] = 0;
-    }
-    readSolver(&solution[1], numVars * sizeof(int));
-  }
-  return result;
+               }
+               readSolver(&solution[1], numVars * sizeof(int));
+       }
+       return result;
 }
 
 int IncrementalSolver::readIntSolver() {
-  int value;
-  readSolver(&value, 4);
-  return value;
+       int value;
+       readSolver(&value, 4);
+       return value;
 }
 
 void IncrementalSolver::readSolver(void * tmp, ssize_t size) {
-  char *result = (char *) tmp;
-  ssize_t bytestoread=size;
-  ssize_t bytesread=0;
-  do {
-    ssize_t n=read(from_solver_fd, &((char *)result)[bytesread], bytestoread);
-    if (n == -1) {
-      model_print("Read failure\n");
-      exit(-1);
-    }
-    bytestoread -= n;
-    bytesread += n;
-  } while(bytestoread != 0);
+       char *result = (char *) tmp;
+       ssize_t bytestoread=size;
+       ssize_t bytesread=0;
+       do {
+               ssize_t n=read(from_solver_fd, &((char *)result)[bytesread], bytestoread);
+               if (n == -1) {
+                       model_print("Read failure\n");
+                       exit(-1);
+               }
+               bytestoread -= n;
+               bytesread += n;
+       } while(bytestoread != 0);
 }
 
 bool IncrementalSolver::getValue(int variable) {
-  return solution[variable];
+       return solution[variable];
 }
 
 void IncrementalSolver::createSolver() {
-  int to_pipe[2];
-  int from_pipe[2];
-  if (pipe(to_pipe) || pipe(from_pipe)) {
-    model_print("Error creating pipe.\n");
-    exit(-1);
-  }
-  if ((solver_pid = fork()) == -1) {
-    model_print("Error forking.\n");
-    exit(-1);
-  }
-  if (solver_pid == 0) {
-    //Solver process
-    close(to_pipe[1]);
-    close(from_pipe[0]);
+       int to_pipe[2];
+       int from_pipe[2];
+       if (pipe(to_pipe) || pipe(from_pipe)) {
+               model_print("Error creating pipe.\n");
+               exit(-1);
+       }
+       if ((solver_pid = fork()) == -1) {
+               model_print("Error forking.\n");
+               exit(-1);
+       }
+       if (solver_pid == 0) {
+               //Solver process
+               close(to_pipe[1]);
+               close(from_pipe[0]);
                int fd=open("log_file", O_WRONLY|O_CREAT|O_TRUNC, S_IRWXU);
-               
-    if ((dup2(to_pipe[0], 0) == -1) ||
-        (dup2(from_pipe[1], IS_OUT_FD) == -1) ||
+
+               if ((dup2(to_pipe[0], 0) == -1) ||
+                               (dup2(from_pipe[1], IS_OUT_FD) == -1) ||
                                (dup2(fd, 1) == -1)) {
-      model_print("Error duplicating pipes\n");
-    }
+                       model_print("Error duplicating pipes\n");
+               }
                //    setsid();
-    execlp(SATSOLVER, SATSOLVER, NULL);
-    model_print("execlp Failed\n");
+               execlp(SATSOLVER, SATSOLVER, NULL);
+               model_print("execlp Failed\n");
                close(fd);
-  } else {
-    //Our process
-    to_solver_fd = to_pipe[1];
-    from_solver_fd = from_pipe[0];
-    close(to_pipe[0]);
-    close(from_pipe[1]);
-  }
+       } else {
+               //Our process
+               to_solver_fd = to_pipe[1];
+               from_solver_fd = from_pipe[0];
+               close(to_pipe[0]);
+               close(from_pipe[1]);
+       }
 }
 
 void IncrementalSolver::killSolver() {
-  close(to_solver_fd);
-  close(from_solver_fd);
-  //Stop the solver
-  if (solver_pid > 0) {
+       close(to_solver_fd);
+       close(from_solver_fd);
+       //Stop the solver
+       if (solver_pid > 0) {
                int status;
-    kill(solver_pid, SIGKILL);
+               kill(solver_pid, SIGKILL);
                waitpid(solver_pid, &status, 0);
        }
 }
 
 void IncrementalSolver::flushBuffer() {
-  ssize_t bytestowrite=sizeof(int)*offset;
-  ssize_t byteswritten=0;
-  do {
-    ssize_t n=write(to_solver_fd, &((char *)buffer)[byteswritten], bytestowrite);
-    if (n == -1) {
-      perror("Write failure\n");
-      model_print("to_solver_fd=%d\n",to_solver_fd);
-      exit(-1);
-    }
-    bytestowrite -= n;
-    byteswritten += n;
-  } while(bytestowrite != 0);
-  offset = 0;
+       ssize_t bytestowrite=sizeof(int)*offset;
+       ssize_t byteswritten=0;
+       do {
+               ssize_t n=write(to_solver_fd, &((char *)buffer)[byteswritten], bytestowrite);
+               if (n == -1) {
+                       perror("Write failure\n");
+                       model_print("to_solver_fd=%d\n",to_solver_fd);
+                       exit(-1);
+               }
+               bytestowrite -= n;
+               byteswritten += n;
+       } while(bytestowrite != 0);
+       offset = 0;
 }
index d5b7f3c..415dc8d 100644 (file)
 #include "classlist.h"
 
 class IncrementalSolver {
- public:
-  IncrementalSolver();
-  ~IncrementalSolver();
-  void addClauseLiteral(int literal);
-  void finishedClauses();
-  void freeze(int variable);
-  int solve();
+public:
+       IncrementalSolver();
+       ~IncrementalSolver();
+       void addClauseLiteral(int literal);
+       void finishedClauses();
+       void freeze(int variable);
+       int solve();
        void startSolve();
        int getSolution();
 
        bool getValue(int variable);
-  void reset();
+       void reset();
        MEMALLOC;
-       
- private:
-  void createSolver();
-  void killSolver();
-  void flushBuffer();
-  int readIntSolver();
-  void readSolver(void * buffer, ssize_t size);
-  int * buffer;
-  int * solution;
-  int solutionsize;
-  int offset;
-  pid_t solver_pid;
-  int to_solver_fd;
-  int from_solver_fd;
+
+private:
+       void createSolver();
+       void killSolver();
+       void flushBuffer();
+       int readIntSolver();
+       void readSolver(void * buffer, ssize_t size);
+       int * buffer;
+       int * solution;
+       int solutionsize;
+       int offset;
+       pid_t solver_pid;
+       int to_solver_fd;
+       int from_solver_fd;
 };
 #endif
index f536c1b..2d5984a 100644 (file)
--- a/loadrf.cc
+++ b/loadrf.cc
@@ -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();
@@ -100,7 +100,7 @@ void LoadRF::genConstraints(ConstGen *cg) {
                                continue;
                        }
 #else
-                       Constraint * conflictbeforeload=cg->getOrderConstraint(conflictstore, load);    
+                       Constraint * conflictbeforeload=cg->getOrderConstraint(conflictstore, load);
                        if (conflictbeforeload->isFalse()) {
                                storebeforeconflict->freerec();
                                continue;
@@ -111,10 +111,10 @@ void LoadRF::genConstraints(ConstGen *cg) {
                                                                                                         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;
index 8ef7a19..12d4065 100644 (file)
--- a/loadrf.h
+++ b/loadrf.h
 #include "classlist.h"
 
 class LoadRF {
- public:
+public:
        LoadRF(EPRecord *_load, ConstGen *cg);
        ~LoadRF();
        void genConstraints(ConstGen *cg);
 
        MEMALLOC;
- private:
+private:
        EPRecord *load;
        uint numvars;
        Constraint ** vars;
diff --git a/main.cc b/main.cc
index 9060af5..48ec61f 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -37,12 +37,12 @@ static void print_usage(const char *program_name, struct model_params *params)
        param_defaults(params);
 
        model_print(
-                                                       "Model-checker options:\n"
-                                                       "-h, --help                  Display this help message and exit\n"
-                                                       "-Y, --avoidyields           Fairness support by not executing yields\n"
-                                                       "-b, --branches              Only explore all branches\n"
-                                                       "-v[NUM], --verbose[=NUM]    Print verbose execution information. NUM is optional:\n"
-                                                       " --                         Program arguments follow.\n\n");
+               "Model-checker options:\n"
+               "-h, --help                  Display this help message and exit\n"
+               "-Y, --avoidyields           Fairness support by not executing yields\n"
+               "-b, --branches              Only explore all branches\n"
+               "-v[NUM], --verbose[=NUM]    Print verbose execution information. NUM is optional:\n"
+               " --                         Program arguments follow.\n\n");
        exit(EXIT_SUCCESS);
 }
 
@@ -54,7 +54,7 @@ static void parse_options(struct model_params *params, int argc, char **argv)
                {"avoidyields", no_argument, NULL, 'Y'},
                {"branches", no_argument, NULL, 'b'},
                {"verbose", optional_argument, NULL, 'v'},
-               {0, 0, 0, 0} /* Terminator */
+               {0, 0, 0, 0}                                            /* Terminator */
        };
        int opt, longindex;
        bool error = false;
@@ -72,7 +72,7 @@ static void parse_options(struct model_params *params, int argc, char **argv)
                case 'v':
                        params->verbose = optarg ? atoi(optarg) : 1;
                        break;
-               default: /* '?' */
+               default:                                                /* '?' */
                        error = true;
                        break;
                }
@@ -131,12 +131,12 @@ int main(int argc, char **argv)
         * called, it allocated internal buffers.  We can't easily snapshot
         * libc since we also use it.
         */
-       
+
        printf("SATCheck\n"
                                 "Copyright (c) 2016 Regents of the University of California. All rights reserved.\n"
                                 "Distributed under the GPLv2\n"
                                 "Written by Brian Demsky and Patrick Lam\n\n");
-       
+
        /* Configure output redirection for the model-checker */
        redirect_output();
 
index 9ea8af6..573b0b2 100644 (file)
@@ -55,7 +55,7 @@ MCExecution::MCExecution() :
        currid(MCID_INIT),
        schedule_graph(0)
 {
-       EPList->push_back(NULL);//avoid using MCID of 0
+       EPList->push_back(NULL);                        //avoid using MCID of 0
 #ifdef TSO
        storebuffer = new SnapVector<SnapList<EPValue *> *>();
 #endif
@@ -217,7 +217,7 @@ uint64_t MCExecution::rmw(enum atomicop op, void *addr, uint len, uint64_t currv
                model_print("\n");
        }
 
-       int num_mcids=(op==ADD)?1:2;
+       int num_mcids=(op==ADD) ? 1 : 2;
        EPRecord * record=getOrCreateCurrRecord(RMW, NULL, id_addr_offset, VC_RMWOUTINDEX-VC_RFINDEX, len, false);
        record->setRMW(op);
 
@@ -307,7 +307,7 @@ bool MCExecution::isEmptyStoreBuffer(thread_id_t tid) {
        SnapList<EPValue *> * list=(*storebuffer)[id_to_int(tid)];
        return list->empty();
 }
-               
+
 void MCExecution::doStore(thread_id_t tid) {
        SnapList<EPValue *> * list=(*storebuffer)[id_to_int(tid)];
        EPValue * epval=list->front();
@@ -326,7 +326,7 @@ void MCExecution::doStore(EPValue *epval) {
                model_print("flushing %d bytes *(%p) = %lu", len, addr, val);
                currexecpoint->print();
                model_print("\n");
-       }       
+       }
        switch(len) {
        case 1:
                (*(uint8_t *)addr) = (uint8_t)val;
@@ -358,11 +358,11 @@ void MCExecution::fence() {
 #endif
 
 /** @brief EPValue is the corresponding epvalue object.
-               For loads rf is the store we read from.
-               For loads or stores, addr is the MCID for the provided address.
-               numids is the number of MCID's we take in.
-               We then list that number of MCIDs for everything we depend on.
-*/
+                For loads rf is the store we read from.
+                For loads or stores, addr is the MCID for the provided address.
+                numids is the number of MCID's we take in.
+                We then list that number of MCIDs for everything we depend on.
+ */
 
 void MCExecution::recordContext(EPValue * epv, MCID rf, MCID addr, int numids, MCID *mcids) {
        EPRecord *currrecord=epv->getRecord();
@@ -403,7 +403,7 @@ void MCExecution::store(void *addr, uint64_t val, int len) {
                break;
        }
 #endif
-       
+
        if (DBG_ENABLED()) {
                model_print("STORE *%p=%lu ", addr, val);
                currexecpoint->print();
@@ -471,7 +471,7 @@ uint64_t MCExecution::load(const void *addr, int len) {
        bool found=false;
        uint tid=id_to_int(currexecpoint->get_tid());
        SnapList<EPValue *> *list=(*storebuffer)[tid];
-       for(SnapList<EPValue *>::reverse_iterator it=list->rbegin(); it != list->rend(); it++) {
+       for(SnapList<EPValue *>::reverse_iterator it=list->rbegin();it != list->rend();it++) {
                EPValue *epval=*it;
                const void *epaddr=epval->getAddr();
                if (epaddr == addr) {
@@ -513,7 +513,7 @@ uint64_t MCExecution::load(const void *addr, int len) {
                break;
        }
 #endif
-       
+
        if (DBG_ENABLED()) {
                model_print("%lu(mid=%u)=LOAD %p ", val, id_retval, addr);
                currexecpoint->print();
@@ -571,7 +571,7 @@ MCID MCExecution::branchDir(MCID dirid, int direction, int numdirs, bool anyvalu
 }
 
 /** @brief Processes a merge with a previous branch.  mcid gives the
-               branch we merged. */
+                branch we merged. */
 
 void MCExecution::merge(MCID mcid) {
        EPValue * epvalue=getEPValue(mcid);
@@ -583,7 +583,7 @@ void MCExecution::merge(MCID mcid) {
        for(int i=0;i<curr_length-orig_length;i++)
                currexecpoint->pop();
        //increment top
-       currexecpoint->incrementTop();  
+       currexecpoint->incrementTop();
        //now we can create the merge point
        if (DBG_ENABLED()) {
                model_print("MERGE mid=%u", mcid);
@@ -603,7 +603,7 @@ MCID MCExecution::phi(MCID input) {
 
        MCID mcids[]={input};
        recordContext(epvalue, MCID_NODEP, MCID_NODEP, 1, mcids);
-       
+
        MCID fnmcid=getNextMCID();
        ASSERT(EPList->size()==fnmcid);
        EPList->push_back(epvalue);
@@ -632,7 +632,7 @@ MCID MCExecution::loop_phi(MCID input) {
                *p=rip;
                phiset->add(p);
        }
-       
+
        MCID fnmcid=getNextMCID();
        ASSERT(EPList->size()==fnmcid);
        EPList->push_back(epvalue);
@@ -704,7 +704,7 @@ MCID MCExecution::function(uint functionidentifier, int len, uint64_t val, uint
        val=val&getmask(len);
        EPValue * epvalue=getEPValue(record, NULL, NULL, val, len);
        recordContext(epvalue, MCID_NODEP, MCID_NODEP, numids, mcids);
-       
+
        uint64_t valarray[numids+VC_BASEINDEX];
        for(uint i=0;i<VC_BASEINDEX;i++) {
                valarray[i]=0;
@@ -744,7 +744,7 @@ MCID MCExecution::function(uint functionidentifier, int len, uint64_t val, uint
                        delete rit;
                }
        }
-       
+
        return fnmcid;
 }
 
@@ -785,8 +785,8 @@ void MCExecution::set_current_thread(Thread *t) {
                (*CurrBranchList)[oldtid]=currbranch;
        }
        curr_thread=t;
-       currexecpoint=(t==NULL)?NULL:(*ExecPointList)[id_to_int(t->get_id())];
-       currbranch=(t==NULL)?NULL:(*CurrBranchList)[id_to_int(t->get_id())];
+       currexecpoint=(t==NULL) ? NULL : (*ExecPointList)[id_to_int(t->get_id())];
+       currbranch=(t==NULL) ? NULL : (*CurrBranchList)[id_to_int(t->get_id())];
 }
 
 void MCExecution::threadStart(EPRecord *parent) {
@@ -827,7 +827,7 @@ void MCExecution::threadJoin(Thread *blocking) {
 void MCExecution::threadFinish() {
        Thread *th = get_current_thread();
        /* Wake up any joining threads */
-       for (unsigned int i = 0; i < get_num_threads(); i++) {
+       for (unsigned int i = 0;i < get_num_threads();i++) {
                Thread *waiting = get_thread(int_to_id(i));
                if (waiting->waiting_on() == th) {
                        waiting->set_waiting(NULL);
@@ -870,14 +870,14 @@ void * MCExecution::alloc(size_t size) {
 
 void MCExecution::enterLoop() {
        EPRecord * record=getOrCreateCurrRecord(LOOPENTER, NULL, 0, 0, 8, false);
-       
+
        //push the loop iteration counter
        currexecpoint->push(EP_LOOP,0);
        //push the curr iteration statement counter
        currexecpoint->push(EP_COUNTER,0);
        EPRecord * lpstartrecord=getOrCreateCurrRecord(LOOPSTART, NULL, 0, 0, 8, false);
        record->setChildRecord(lpstartrecord);
-       
+
        currexecpoint->incrementTop();
        if (DBG_ENABLED()) {
                model_print("ENLOOP ");
@@ -894,7 +894,7 @@ void MCExecution::exitLoop() {
 
        /* Record last statement */
        uint tid=id_to_int(currexecpoint->get_tid());
-       
+
        if (!currexecpoint->directInLoop()) {
                breakstate=getOrCreateCurrRecord(NONLOCALTRANS, NULL, 0, 0, 8, false);
                currexecpoint->incrementTop();
@@ -902,10 +902,10 @@ void MCExecution::exitLoop() {
                breakstate=getOrCreateCurrRecord(LOOPEXIT, NULL, 0, 0, 8, false);
                currexecpoint->incrementTop();
        }
-       
+
        /* Get Last Record */
-       EPRecord *lastrecord=(currbranch==NULL)?(*alwaysexecuted)[tid]:currbranch->lastrecord;
-       
+       EPRecord *lastrecord=(currbranch==NULL) ? (*alwaysexecuted)[tid] : currbranch->lastrecord;
+
        /* Remember last record as loop exit for this execution.  */
        if (lastloopexit->size()<=tid) {
                lastloopexit->resize(tid+1);
@@ -991,17 +991,17 @@ void MCExecution::addRecordDepTable(EPRecord *record, EPRecord *deprecord, unsig
        struct RecordIntPair pair={deprecord, index};
 
        if (!set->contains(&pair)) {
-               struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));             
+               struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));
                *p=pair;
                set->add(p);
        }
 
        if (!revrecorddep->contains(&pair)) {
-               struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));             
+               struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));
                *p=pair;
                revrecorddep->put(p, new ModelVector<EPRecord *>());
        }
-       
+
        ModelVector<EPRecord *> * recvec=revrecorddep->get(&pair);
        for(uint i=0;i<recvec->size();i++) {
                if ((*recvec)[i]==record)
index dca4228..a8c68f7 100644 (file)
@@ -29,12 +29,12 @@ struct RecordIntPair {
        unsigned int index;
 };
 inline unsigned int RP_hash_function(struct RecordIntPair * pair) {
-  return (unsigned int)(((uintptr_t)pair->record) >> 4) ^ pair->index;
+       return (unsigned int)(((uintptr_t)pair->record) >> 4) ^ pair->index;
 }
 inline bool RP_equals(struct RecordIntPair * key1, struct RecordIntPair * key2) {
        if (key1==NULL)
                return key1==key2;
-  return key1->record == key2->record && key1->index == key2->index;
+       return key1->record == key2->record && key1->index == key2->index;
 }
 typedef HashSet<struct RecordIntPair *, uintptr_t, 0, model_malloc, model_calloc, model_free, RP_hash_function, RP_equals> EPRecordSet;
 typedef HSIterator<struct RecordIntPair *, uintptr_t, 0, model_malloc, model_calloc, model_free, RP_hash_function, RP_equals> EPRecordIterator;
@@ -45,12 +45,12 @@ struct MCExecution_snapshot {
        MCExecution_snapshot();
        ~MCExecution_snapshot();
        unsigned int next_thread_id;
-       
+
        SNAPSHOTALLOC;
 };
 
 class MCExecution {
- public:
+public:
        MCExecution();
        ~MCExecution();
        EPRecord * getOrCreateCurrRecord(EventType et, bool * isNew, uintptr_t offset, unsigned int numinputs, uint len, bool br_anyvalue);
@@ -60,7 +60,7 @@ class MCExecution {
        MCID nextRMW(MCID addr, uintptr_t offset, MCID oldval, MCID valarg);
        void store(void *addr, uint64_t val, int len);
        uint64_t load(const void *addr, int len);
-       uint64_t rmw(enum atomicop op, void *addr, uint size, uint64_t currval, uint64_t oldval, uint64_t valarg); 
+       uint64_t rmw(enum atomicop op, void *addr, uint size, uint64_t currval, uint64_t oldval, uint64_t valarg);
        void reset();
        MCID branchDir(MCID dir, int direction, int numdirs, bool anyvalue);
        void merge(MCID mcid);
@@ -117,9 +117,9 @@ class MCExecution {
        void evalGoal(EPRecord *record, CGoal *goal);
        void dumpExecution();
        EPRecord * getRecord(ExecPoint * ep) {return EPTable->get(ep);}
-       
+
        MEMALLOC;
- private:
+private:
        EPHashTable * EPTable;
        EPValueHashTable * EPValueTable;
        MemHashTable *memtable;
@@ -135,7 +135,7 @@ class MCExecution {
        ExecPoint * currexecpoint;
        MCScheduler * scheduler;
        Planner * planner;
-       struct MCExecution_snapshot * const snap_fields;  
+       struct MCExecution_snapshot * const snap_fields;
        Thread * curr_thread;
        EPValue *currbranch;
        EPRecordDepHashTable *eprecorddep;
@@ -145,7 +145,7 @@ class MCExecution {
        ModelVector<EPRecord *> * joinvec;
        ModelVector<CGoalSet *> * sharedgoals;
        ModelVector<RecordSet *> * sharedfuncrecords;
-       
+
        MCID currid;
        MCID id_addr;
        MCID id_oldvalue;
index a86b0ff..f73671f 100644 (file)
@@ -113,10 +113,10 @@ void MCScheduler::reset() {
 
 
 
- void MCScheduler::check_preempt() {
+void MCScheduler::check_preempt() {
        Thread *t=execution->get_current_thread();
 #ifdef TSO
- restart_search:
+restart_search:
        //start at the next thread
        unsigned int tid=id_to_int(t->get_id());
        bool storebuffer=true;
@@ -142,7 +142,7 @@ void MCScheduler::reset() {
 #else
        //start at the next thread
        unsigned int tid=(id_to_int(t->get_id())+1)%execution->get_num_threads();
-       
+
        for(unsigned int i=0;i<execution->get_num_threads();i++,tid=(tid+1)%execution->get_num_threads()) {
                //don't try to schedule finished threads
                if (execution->get_thread(int_to_id(tid))->is_complete())
@@ -152,7 +152,7 @@ void MCScheduler::reset() {
                }
        }
 #endif
-       
+
        Thread *next_thread=execution->get_thread(int_to_id(tid));
        if (next_thread->is_complete())
                next_thread=NULL;
@@ -185,7 +185,7 @@ bool MCScheduler::checkSet(unsigned int tid, ModelVector<ModelVector<WaitPair* >
                        CompareResult compare=stoppoint->compare(current);
                        if (compare==CR_EQUALS) {
                                //hit stop point
-                               ExecPoint *waitpoint=nextwp->getWait();         
+                               ExecPoint *waitpoint=nextwp->getWait();
                                thread_id_t waittid=waitpoint->get_tid();
                                ExecPoint *waitthread=execution->get_execpoint(waittid);
                                CompareResult comparewt=waitthread->compare(waitpoint);
index d7fb852..185a50f 100644 (file)
 #include "stl-model.h"
 
 class WaitPair {
- public:
+public:
        WaitPair(ExecPoint * stoppoint, ExecPoint * waitpoint);
        ~WaitPair();
        ExecPoint * getStop();
        ExecPoint * getWait();
 
        MEMALLOC;
- private:
+private:
        ExecPoint *stop_point;
        ExecPoint *wait_point;
 };
 
 class MCScheduler {
- public:
+public:
        MCScheduler(MCExecution * e);
        ~MCScheduler();
        ucontext_t * get_system_context() { return &system_context; }
@@ -44,7 +44,7 @@ class MCScheduler {
        void setNewFlag();
 
        MEMALLOC;
- private:
+private:
        unsigned int waitsetlen;
        ucontext_t system_context;
        MCExecution *execution;
index 9699d7f..dd0f814 100644 (file)
--- a/mcutil.h
+++ b/mcutil.h
@@ -29,6 +29,6 @@ static inline uint64_t getmask(uint len) {
 }
 
 
-#define NUMBITS(x) ((x==0)?0:8*sizeof(x)-__builtin_clz(x))
+#define NUMBITS(x) ((x==0) ? 0 : 8*sizeof(x)-__builtin_clz(x))
 
 #endif
index 2ac46b8..506d116 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -30,7 +30,7 @@ void user_main_wrapper(void *) {
        user_main(model->params.argc, model->params.argv);
 }
 
-/** Implements the main loop for model checking test case 
+/** Implements the main loop for model checking test case
  */
 void MC::check() {
        snapshot_record(0);
diff --git a/model.h b/model.h
index f977117..bf4a085 100644 (file)
--- a/model.h
+++ b/model.h
@@ -24,7 +24,7 @@
 #include "params.h"
 
 class MC {
- public:
+public:
        MC(struct model_params params);
        ~MC();
        MCExecution * get_execution() const { return execution; }
@@ -33,7 +33,7 @@ class MC {
        const model_params params;
 
        MEMALLOC;
- private:
+private:
        MCExecution *execution;
        void run_execution();
 
@@ -41,4 +41,4 @@ class MC {
 };
 
 extern MC *model;
-#endif /* __MODEL_H__ */
+#endif/* __MODEL_H__ */
index ea65c89..bbddf7e 100644 (file)
@@ -212,7 +212,7 @@ void * real_user_malloc(size_t size)
        size=(size+7)&~((size_t)7);
        void *tmp = snapshot_struct->allocation_ptr;
        snapshot_struct->allocation_ptr = (void *)((char *) snapshot_struct->allocation_ptr +size);
-       
+
        ASSERT(snapshot_struct->allocation_ptr <= snapshot_struct->top_ptr);
        return tmp;
 }
@@ -307,7 +307,7 @@ void operator delete[](void *p, size_t size)
        free(p);
 }
 
-#else /* !USE_MPROTECT_SNAPSHOT */
+#else  /* !USE_MPROTECT_SNAPSHOT */
 
 /** @brief Snapshotting allocation function for use by the Thread class only */
 void * Thread_malloc(size_t size)
@@ -321,4 +321,4 @@ void Thread_free(void *ptr)
        free(ptr);
 }
 
-#endif /* !USE_MPROTECT_SNAPSHOT */
+#endif/* !USE_MPROTECT_SNAPSHOT */
index 0eca0a3..2bd7663 100644 (file)
@@ -33,7 +33,7 @@
        void operator delete[](void *p, size_t size) { \
                model_free(p); \
        } \
-       void * operator new(size_t size, void *p) { /* placement new */ \
+       void * operator new(size_t size, void *p) {                             /* placement new */ \
                return p; \
        }
 
@@ -52,7 +52,7 @@
        void operator delete[](void *p, size_t size) { \
                snapshot_free(p); \
        } \
-       void * operator new(size_t size, void *p) { /* placement new */ \
+       void * operator new(size_t size, void *p) {                             /* placement new */ \
                return p; \
        }
 
@@ -84,15 +84,15 @@ void Thread_free(void *ptr);
  */
 template <class T>
 class ModelAlloc {
- public:
+public:
        // type definitions
-       typedef T        value_type;
+       typedef T value_type;
        typedef T*       pointer;
        typedef const T* const_pointer;
        typedef T&       reference;
        typedef const T& const_reference;
-       typedef size_t   size_type;
-       typedef size_t   difference_type;
+       typedef size_t size_type;
+       typedef size_t difference_type;
 
        // rebind allocator to type U
        template <class U>
@@ -153,14 +153,14 @@ class ModelAlloc {
 /** Return that all specializations of this allocator are interchangeable. */
 template <class T1, class T2>
 bool operator ==(const ModelAlloc<T1>&,
-               const ModelAlloc<T2>&) throw() {
+                                                                const ModelAlloc<T2>&) throw() {
        return true;
 }
 
 /** Return that all specializations of this allocator are interchangeable. */
 template <class T1, class T2>
 bool operator!= (const ModelAlloc<T1>&,
-               const ModelAlloc<T2>&) throw() {
+                                                                const ModelAlloc<T2>&) throw() {
        return false;
 }
 
@@ -176,15 +176,15 @@ bool operator!= (const ModelAlloc<T1>&,
  */
 template <class T>
 class SnapshotAlloc {
- public:
+public:
        // type definitions
-       typedef T        value_type;
+       typedef T value_type;
        typedef T*       pointer;
        typedef const T* const_pointer;
        typedef T&       reference;
        typedef const T& const_reference;
-       typedef size_t   size_type;
-       typedef size_t   difference_type;
+       typedef size_t size_type;
+       typedef size_t difference_type;
 
        // rebind allocator to type U
        template <class U>
@@ -245,44 +245,44 @@ class SnapshotAlloc {
 /** Return that all specializations of this allocator are interchangeable. */
 template <class T1, class T2>
 bool operator ==(const SnapshotAlloc<T1>&,
-               const SnapshotAlloc<T2>&) throw() {
+                                                                const SnapshotAlloc<T2>&) throw() {
        return true;
 }
 
 /** Return that all specializations of this allocator are interchangeable. */
 template <class T1, class T2>
 bool operator!= (const SnapshotAlloc<T1>&,
-               const SnapshotAlloc<T2>&) throw() {
+                                                                const SnapshotAlloc<T2>&) throw() {
        return false;
 }
 
 #ifdef __cplusplus
 extern "C" {
 #endif
-       typedef void * mspace;
-       extern void * mspace_malloc(mspace msp, size_t bytes);
-       extern void mspace_free(mspace msp, void* mem);
-       extern void * mspace_realloc(mspace msp, void* mem, size_t newsize);
-       extern void * mspace_calloc(mspace msp, size_t n_elements, size_t elem_size);
-       extern mspace create_mspace_with_base(void* base, size_t capacity, int locked);
-       extern mspace create_mspace(size_t capacity, int locked);
-
-       struct snapshot_heap_data {
-               void *allocation_ptr;
-               void *top_ptr;
-       };
+typedef void * mspace;
+extern void * mspace_malloc(mspace msp, size_t bytes);
+extern void mspace_free(mspace msp, void* mem);
+extern void * mspace_realloc(mspace msp, void* mem, size_t newsize);
+extern void * mspace_calloc(mspace msp, size_t n_elements, size_t elem_size);
+extern mspace create_mspace_with_base(void* base, size_t capacity, int locked);
+extern mspace create_mspace(size_t capacity, int locked);
+
+struct snapshot_heap_data {
+       void *allocation_ptr;
+       void *top_ptr;
+};
 
-       extern struct snapshot_heap_data * snapshot_struct;
+extern struct snapshot_heap_data * snapshot_struct;
 
 #if USE_MPROTECT_SNAPSHOT
-       extern void * user_snapshot_space;
-       extern mspace thread_snapshot_space;
+extern void * user_snapshot_space;
+extern mspace thread_snapshot_space;
 #endif
 
-       extern mspace model_snapshot_space;
+extern mspace model_snapshot_space;
 
 #ifdef __cplusplus
-};  /* end of extern "C" */
+};     /* end of extern "C" */
 #endif
 
-#endif /* _MY_MEMORY_H */
+#endif/* _MY_MEMORY_H */
index f8aba6c..3c78875 100644 (file)
--- a/output.h
+++ b/output.h
@@ -24,6 +24,6 @@ static inline void print_program_output() { }
 void redirect_output();
 void clear_program_output();
 void print_program_output();
-#endif /* ! CONFIG_DEBUG */
+#endif/* ! CONFIG_DEBUG */
 
-#endif /* __OUTPUT_H__ */
+#endif/* __OUTPUT_H__ */
index 31e9267..78cedcb 100644 (file)
--- a/params.h
+++ b/params.h
@@ -23,7 +23,7 @@ struct model_params {
 
        /** @brief Only explore branches. */
        bool branches;
-       
+
        /** @brief Command-line argument count to pass to user program */
        int argc;
 
@@ -31,4 +31,4 @@ struct model_params {
        char **argv;
 };
 
-#endif /* __PARAMS_H__ */
+#endif/* __PARAMS_H__ */
index f832fb9..d6cf00c 100644 (file)
@@ -36,7 +36,7 @@ bool Planner::is_finished() {
 void Planner::plan() {
        DEBUG("Planning\n");
        e->get_scheduler()->reset();
-       
+
        if (!cgen->canReuseEncoding()) {
                processChanges();
                cgen->reset();
@@ -137,8 +137,8 @@ void Planner::processStore(MCChange * change) {
 }
 
 /** This function propagate news values that a function or add
-               operation may generate.
-*/
+                operation may generate.
+ */
 
 void Planner::processNewReturnValue(MCChange *change) {
        EPRecord *record=change->getRecord();
@@ -154,15 +154,15 @@ void Planner::processNewReturnValue(MCChange *change) {
 }
 
 /** This function registers a new address for a load operation.  We
-               iterate over all stores to that new address and grab their values
-               and propagate them.
-*/
+                iterate over all stores to that new address and grab their values
+                and propagate them.
+ */
 
 void Planner::processNewLoadAddress(MCChange *change) {
        EPRecord *load=change->getRecord();
        void *addr=(void *)change->getValue();
        RecordSet *storeset=e->getStoreTable(addr);
-       if (storeset == NULL) 
+       if (storeset == NULL)
                return;
        RecordIterator *rit=storeset->iterator();
        while(rit->hasNext()) {
@@ -182,13 +182,13 @@ void Planner::processNewLoadAddress(MCChange *change) {
 }
 
 /** This function processes a new address for a store.  We push our
-               values to all loads from that address. */
+                values to all loads from that address. */
 
 void Planner::processNewStoreAddress(MCChange *change) {
        EPRecord *store=change->getRecord();
        void *addr=(void *)change->getValue();
        RecordSet *rset=e->getLoadTable(addr);
-       if (rset == NULL) 
+       if (rset == NULL)
                return;
        RecordIterator *rit=rset->iterator();
        IntHashSet *valset=store->getStoreSet();
@@ -209,7 +209,7 @@ void Planner::processNewStoreAddress(MCChange *change) {
 
 
 /** This function pushes a new store value to all loads that share an
-               address. */
+                address. */
 
 void Planner::processNewStoreValue(MCChange *change) {
        EPRecord *store=change->getRecord();
@@ -268,7 +268,7 @@ void Planner::registerBranchValue(EPRecord *record, uint64_t val, unsigned int i
 void Planner::registerLoadValue(EPRecord *record, uint64_t val, unsigned int index) {
        if (index==VC_ADDRINDEX)
                val+=record->getOffset();
-       
+
        bool is_new=record->getSet(index)->add(val);
        if (is_new) {
                switch(index) {
@@ -324,13 +324,13 @@ void Planner::doRMWNewAddrChange(EPRecord *record, uint64_t val) {
        //propagate our value to new loads
        MCChange * change=new MCChange(record, val, VC_ADDRINDEX);
        addChange(change);
-       
+
        //look at new stores and update our read from set
        RecordSet *storeset=e->getStoreTable((void *)val);
        RecordIterator *rit=storeset->iterator();
        while(rit->hasNext()) {
                EPRecord *store=rit->next();
-               
+
                if (e->compatibleStoreLoad(store, record)) {
                        IntIterator * it=store->getStoreSet()->iterator();
                        while(it->hasNext()) {
@@ -388,10 +388,10 @@ void Planner::registerStoreValue(EPRecord *record, uint64_t val, unsigned int in
                val+=record->getOffset();
 
        bool is_new=record->getSet(index)->add(val);
-       
+
        if (index==VC_ADDRINDEX) {
                if (is_new)
-                       e->addStoreTable((void *)val, record);          
+                       e->addStoreTable((void *)val, record);
                MCChange * change=new MCChange(record, val, index);
                addChange(change);
        } else if (index==VC_BASEINDEX) {
index 9f35ddd..7ee76f1 100644 (file)
--- a/planner.h
+++ b/planner.h
@@ -20,7 +20,7 @@ typedef HSIterator<MCChange *, intptr_t, 0, model_malloc, model_calloc, model_fr
 enum PlanResult {NOSCHEDULE, SCHEDULED};
 
 class Planner {
- public:
+public:
        Planner(MCExecution * e);
        ~Planner();
        bool is_finished();
@@ -35,7 +35,7 @@ class Planner {
        bool checkConstGraph(EPRecord *record, uint64_t val);
        void registerValue(EPRecord *record, uint64_t val, unsigned int index);
        ConstGen * getConstGen() {return cgen;}
-       
+
        MEMALLOC;
 
 private:
index cc17b1e..9e7d3de 100644 (file)
@@ -33,20 +33,20 @@ void neatPrint(EPRecord *r, ConstGen *cgen, bool *satsolution) {
                model_print("address=%p ",  sls->getAddressEncoding(cgen, r, satsolution));
                model_print("rd=%lu ", sls->getValueEncoding(cgen, r, satsolution));
        }
-               break;
+       break;
        case STORE: {
                StoreLoadSet * sls=cgen->getStoreLoadSet(r);
                model_print("address=%p ",  sls->getAddressEncoding(cgen, r, satsolution));
                model_print("wr=%lu ", sls->getValueEncoding(cgen, r, satsolution));
        }
-               break;
+       break;
        case RMW: {
                StoreLoadSet * sls=cgen->getStoreLoadSet(r);
                model_print("address=%p ",  sls->getAddressEncoding(cgen, r, satsolution));
                model_print("rd=%lu ", sls->getRMWRValueEncoding(cgen, r, satsolution));
                model_print("wr=%lu ", sls->getValueEncoding(cgen, r, satsolution));
        }
-               break;
+       break;
        default:
                ;
        }
@@ -69,7 +69,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);
@@ -92,7 +92,7 @@ void ScheduleBuilder::buildSchedule(bool * satsolution) {
                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;
@@ -151,7 +151,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();
@@ -192,7 +192,7 @@ EPRecord * ScheduleBuilder::processRecord(EPRecord *record, bool *satsolution) {
        case MERGE:
        case ALLOC:
        case EQUALS:
-       case FUNCTION: 
+       case FUNCTION:
                /* Continue executing */
                break;
        case THREADCREATE:
index be27aac..7ff4bb5 100644 (file)
 #include "stl-model.h"
 
 class ScheduleBuilder {
- public:
+public:
        ScheduleBuilder(MCExecution *_execution, ConstGen *cgen);
        ~ScheduleBuilder();
        void buildSchedule(bool *satsolution);
 
        SNAPSHOTALLOC;
- private:
+private:
        EPRecord * getNextRecord(EPRecord *record);
        EPRecord * processRecord(EPRecord *record, bool * satsolution);
        ConstGen * cg;
index 4f9a4d5..dd48107 100644 (file)
@@ -32,12 +32,12 @@ struct snapshot_entry {
 };
 
 class SnapshotStack {
- public:
+public:
        int backTrackBeforeStep(int seq_index);
        void snapshotStep(int seq_index);
 
        MEMALLOC;
- private:
+private:
        ModelVector<struct snapshot_entry> stack;
 };
 
@@ -164,7 +164,7 @@ static void SnapshotGlobalSegments()
 int SnapshotStack::backTrackBeforeStep(int seqindex)
 {
        int i;
-       for (i = (int)stack.size() - 1; i >= 0; i++)
+       for (i = (int)stack.size() - 1;i >= 0;i++)
                if (stack[i].index <= seqindex)
                        break;
                else
index 7c8516c..dbc6f88 100644 (file)
@@ -19,8 +19,8 @@ typedef unsigned int snapshot_id;
 
 typedef void (*VoidFuncPtr)();
 void snapshot_system_init(unsigned int numbackingpages,
-               unsigned int numsnapshots, unsigned int nummemoryregions,
-               unsigned int numheappages, VoidFuncPtr entryPoint);
+                                                                                                       unsigned int numsnapshots, unsigned int nummemoryregions,
+                                                                                                       unsigned int numheappages, VoidFuncPtr entryPoint);
 
 void snapshot_stack_init();
 void snapshot_record(int seq_index);
index d06b887..b754d5b 100644 (file)
@@ -49,8 +49,8 @@ struct BackingPageRecord {
 
 /* Struct for each memory region */
 struct MemoryRegion {
-       void *basePtr; // base of memory region
-       int sizeInPages; // size of memory region in pages
+       void *basePtr;                  // base of memory region
+       int sizeInPages;                        // size of memory region in pages
 };
 
 /** ReturnPageAlignedAddress returns a page aligned address for the
@@ -66,19 +66,19 @@ struct mprot_snapshotter {
        mprot_snapshotter(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions);
        ~mprot_snapshotter();
 
-       struct MemoryRegion *regionsToSnapShot; //This pointer references an array of memory regions to snapshot
-       snapshot_page_t *backingStore; //This pointer references an array of snapshotpage's that form the backing store
-       void *backingStoreBasePtr; //This pointer references an array of snapshotpage's that form the backing store
-       struct BackingPageRecord *backingRecords; //This pointer references an array of backingpagerecord's (same number of elements as backingstore
-       struct SnapShotRecord *snapShots; //This pointer references the snapshot array
+       struct MemoryRegion *regionsToSnapShot;                         //This pointer references an array of memory regions to snapshot
+       snapshot_page_t *backingStore;                  //This pointer references an array of snapshotpage's that form the backing store
+       void *backingStoreBasePtr;                      //This pointer references an array of snapshotpage's that form the backing store
+       struct BackingPageRecord *backingRecords;                               //This pointer references an array of backingpagerecord's (same number of elements as backingstore
+       struct SnapShotRecord *snapShots;                               //This pointer references the snapshot array
 
-       unsigned int lastSnapShot; //Stores the next snapshot record we should use
-       unsigned int lastBackingPage; //Stores the next backingpage we should use
-       unsigned int lastRegion; //Stores the next memory region to be used
+       unsigned int lastSnapShot;                      //Stores the next snapshot record we should use
+       unsigned int lastBackingPage;                           //Stores the next backingpage we should use
+       unsigned int lastRegion;                        //Stores the next memory region to be used
 
-       unsigned int maxRegions; //Stores the max number of memory regions we support
-       unsigned int maxBackingPages; //Stores the total number of backing pages
-       unsigned int maxSnapShots; //Stores the total number of snapshots we allow
+       unsigned int maxRegions;                        //Stores the max number of memory regions we support
+       unsigned int maxBackingPages;                           //Stores the total number of backing pages
+       unsigned int maxSnapShots;                      //Stores the total number of snapshots we allow
 
        MEMALLOC;
 };
@@ -117,13 +117,13 @@ static void mprot_handle_pf(int sig, siginfo_t *si, void *unused)
        if (si->si_code == SEGV_MAPERR) {
                model_print("Segmentation fault at %p\n", si->si_addr);
                model_print("For debugging, place breakpoint at: %s:%d\n",
-                               __FILE__, __LINE__);
+                                                               __FILE__, __LINE__);
                // print_trace(); // Trace printing may cause dynamic memory allocation
                exit(EXIT_FAILURE);
        }
        void* addr = ReturnPageAlignedAddress(si->si_addr);
 
-       unsigned int backingpage = mprot_snap->lastBackingPage++; //Could run out of pages...
+       unsigned int backingpage = mprot_snap->lastBackingPage++;                               //Could run out of pages...
        if (backingpage == mprot_snap->maxBackingPages) {
                model_print("Out of backing pages at %p\n", si->si_addr);
                exit(EXIT_FAILURE);
@@ -141,8 +141,8 @@ static void mprot_handle_pf(int sig, siginfo_t *si, void *unused)
 }
 
 static void mprot_snapshot_init(unsigned int numbackingpages,
-               unsigned int numsnapshots, unsigned int nummemoryregions,
-               unsigned int numheappages, VoidFuncPtr entryPoint)
+                                                                                                                               unsigned int numsnapshots, unsigned int nummemoryregions,
+                                                                                                                               unsigned int numheappages, VoidFuncPtr entryPoint)
 {
        /* Setup a stack for our signal handler....  */
        stack_t ss;
@@ -176,14 +176,14 @@ static void mprot_snapshot_init(unsigned int numbackingpages,
        memset(&si, 0, sizeof(si));
        si.si_addr = ss.ss_sp;
        mprot_handle_pf(SIGSEGV, &si, NULL);
-       mprot_snap->lastBackingPage--; //remove the fake page we copied
+       mprot_snap->lastBackingPage--;                  //remove the fake page we copied
+
 
-       
        void *basemySpace = model_malloc((numheappages -32 + 1) * PAGESIZE);
        void *pagealignedbase = PageAlignAddressUpward(basemySpace);
        user_snapshot_space = pagealignedbase;
        snapshot_add_memory_region(pagealignedbase, numheappages-32);
-       
+
        void *basethreadSpace = model_malloc(33 * PAGESIZE);
        pagealignedbase = PageAlignAddressUpward(basethreadSpace);
        thread_snapshot_space = create_mspace_with_base(pagealignedbase, 32 * PAGESIZE, 1);
@@ -197,7 +197,7 @@ static void mprot_snapshot_init(unsigned int numbackingpages,
        snapshot_struct = (struct snapshot_heap_data *) model_malloc(sizeof(struct snapshot_heap_data));
        snapshot_struct->allocation_ptr=user_snapshot_space;
        snapshot_struct->top_ptr=(void *)(((char *)user_snapshot_space)+((numheappages-32)*PAGESIZE));
-       
+
        entryPoint();
 }
 
@@ -210,15 +210,15 @@ static void mprot_add_to_snapshot(void *addr, unsigned int numPages)
        }
 
        DEBUG("snapshot region %p-%p (%u page%s)\n",
-                       addr, (char *)addr + numPages * PAGESIZE, numPages,
-                       numPages > 1 ? "s" : "");
+                               addr, (char *)addr + numPages * PAGESIZE, numPages,
+                               numPages > 1 ? "s" : "");
        mprot_snap->regionsToSnapShot[memoryregion].basePtr = addr;
        mprot_snap->regionsToSnapShot[memoryregion].sizeInPages = numPages;
 }
 
 static snapshot_id mprot_take_snapshot()
 {
-       for (unsigned int region = 0; region < mprot_snap->lastRegion; region++) {
+       for (unsigned int region = 0;region < mprot_snap->lastRegion;region++) {
                if (mprotect(mprot_snap->regionsToSnapShot[region].basePtr, mprot_snap->regionsToSnapShot[region].sizeInPages * sizeof(snapshot_page_t), PROT_READ) == -1) {
                        perror("mprotect");
                        model_print("Failed to mprotect inside of takeSnapShot\n");
@@ -239,7 +239,7 @@ static void mprot_roll_back(snapshot_id theID)
 {
 #if USE_MPROTECT_SNAPSHOT == 2
        if (mprot_snap->lastSnapShot == (theID + 1)) {
-               for (unsigned int page = mprot_snap->snapShots[theID].firstBackingPage; page < mprot_snap->lastBackingPage; page++) {
+               for (unsigned int page = mprot_snap->snapShots[theID].firstBackingPage;page < mprot_snap->lastBackingPage;page++) {
                        memcpy(mprot_snap->backingRecords[page].basePtrOfPage, &mprot_snap->backingStore[page], sizeof(snapshot_page_t));
                }
                return;
@@ -247,14 +247,14 @@ static void mprot_roll_back(snapshot_id theID)
 #endif
 
        HashTable< void *, bool, uintptr_t, 4, model_malloc, model_calloc, model_free> duplicateMap;
-       for (unsigned int region = 0; region < mprot_snap->lastRegion; region++) {
+       for (unsigned int region = 0;region < mprot_snap->lastRegion;region++) {
                if (mprotect(mprot_snap->regionsToSnapShot[region].basePtr, mprot_snap->regionsToSnapShot[region].sizeInPages * sizeof(snapshot_page_t), PROT_READ | PROT_WRITE) == -1) {
                        perror("mprotect");
                        model_print("Failed to mprotect inside of takeSnapShot\n");
                        exit(EXIT_FAILURE);
                }
        }
-       for (unsigned int page = mprot_snap->snapShots[theID].firstBackingPage; page < mprot_snap->lastBackingPage; page++) {
+       for (unsigned int page = mprot_snap->snapShots[theID].firstBackingPage;page < mprot_snap->lastBackingPage;page++) {
                if (!duplicateMap.contains(mprot_snap->backingRecords[page].basePtrOfPage)) {
                        duplicateMap.put(mprot_snap->backingRecords[page].basePtrOfPage, true);
                        memcpy(mprot_snap->backingRecords[page].basePtrOfPage, &mprot_snap->backingStore[page], sizeof(snapshot_page_t));
@@ -262,13 +262,13 @@ static void mprot_roll_back(snapshot_id theID)
        }
        mprot_snap->lastSnapShot = theID;
        mprot_snap->lastBackingPage = mprot_snap->snapShots[theID].firstBackingPage;
-       mprot_take_snapshot(); //Make sure current snapshot is still good...All later ones are cleared
+       mprot_take_snapshot();                  //Make sure current snapshot is still good...All later ones are cleared
 }
 
-#else /* !USE_MPROTECT_SNAPSHOT */
+#else  /* !USE_MPROTECT_SNAPSHOT */
 
-#define SHARED_MEMORY_DEFAULT  (100 * ((size_t)1 << 20)) // 100mb for the shared memory
-#define STACK_SIZE_DEFAULT      (((size_t)1 << 20) * 20)  // 20 mb out of the above 100 mb for my stack
+#define SHARED_MEMORY_DEFAULT  (100 * ((size_t)1 << 20))// 100mb for the shared memory
+#define STACK_SIZE_DEFAULT      (((size_t)1 << 20) * 20)       // 20 mb out of the above 100 mb for my stack
 
 struct fork_snapshotter {
        /** @brief Pointer to the shared (non-snapshot) memory heap base
@@ -308,19 +308,19 @@ struct fork_snapshotter {
 static struct fork_snapshotter *fork_snap = NULL;
 
 /** @statics
-*   These variables are necessary because the stack is shared region and
-*   there exists a race between all processes executing the same function.
-*   To avoid the problem above, we require variables allocated in 'safe' regions.
-*   The bug was actually observed with the forkID, these variables below are
-*   used to indicate the various contexts to which to switch to.
-*
-*   @private_ctxt: the context which is internal to the current process. Used
-*   for running the internal snapshot/rollback loop.
-*   @exit_ctxt: a special context used just for exiting from a process (so we
-*   can use swapcontext() instead of setcontext() + hacks)
-*   @snapshotid: it is a running counter for the various forked processes
-*   snapshotid. it is incremented and set in a persistently shared record
-*/
+ *   These variables are necessary because the stack is shared region and
+ *   there exists a race between all processes executing the same function.
+ *   To avoid the problem above, we require variables allocated in 'safe' regions.
+ *   The bug was actually observed with the forkID, these variables below are
+ *   used to indicate the various contexts to which to switch to.
+ *
+ *   @private_ctxt: the context which is internal to the current process. Used
+ *   for running the internal snapshot/rollback loop.
+ *   @exit_ctxt: a special context used just for exiting from a process (so we
+ *   can use swapcontext() instead of setcontext() + hacks)
+ *   @snapshotid: it is a running counter for the various forked processes
+ *   snapshotid. it is incremented and set in a persistently shared record
+ */
 static ucontext_t private_ctxt;
 static ucontext_t exit_ctxt;
 static snapshot_id snapshotid = 0;
@@ -333,7 +333,7 @@ static snapshot_id snapshotid = 0;
  * @param func The entry point function for the context
  */
 static void create_context(ucontext_t *ctxt, void *stack, size_t stacksize,
-               void (*func)(void))
+                                                                                                        void (*func)(void))
 {
        getcontext(ctxt);
        ctxt->uc_stack.ss_sp = stack;
@@ -380,8 +380,8 @@ mspace create_shared_mspace()
 }
 
 static void fork_snapshot_init(unsigned int numbackingpages,
-               unsigned int numsnapshots, unsigned int nummemoryregions,
-               unsigned int numheappages, VoidFuncPtr entryPoint)
+                                                                                                                        unsigned int numsnapshots, unsigned int nummemoryregions,
+                                                                                                                        unsigned int numheappages, VoidFuncPtr entryPoint)
 {
        if (!fork_snap)
                createSharedMemory();
@@ -396,7 +396,7 @@ static void fork_snapshot_init(unsigned int numbackingpages,
 
        /* setup the shared-stack context */
        create_context(&fork_snap->shared_ctxt, fork_snap->mStackBase,
-                       STACK_SIZE_DEFAULT, entryPoint);
+                                                                STACK_SIZE_DEFAULT, entryPoint);
        /* switch to a new entryPoint context, on a new stack */
        model_swapcontext(&private_ctxt, &fork_snap->shared_ctxt);
 
@@ -412,7 +412,7 @@ static void fork_snapshot_init(unsigned int numbackingpages,
                        setcontext(&fork_snap->shared_ctxt);
                } else {
                        DEBUG("parent PID: %d, child PID: %d, snapshot ID: %d\n",
-                               getpid(), forkedID, snapshotid);
+                                               getpid(), forkedID, snapshotid);
 
                        while (waitpid(forkedID, NULL, 0) < 0) {
                                /* waitpid() may be interrupted */
@@ -443,15 +443,15 @@ static void fork_roll_back(snapshot_id theID)
        fork_snap->mIDToRollback = -1;
 }
 
-#endif /* !USE_MPROTECT_SNAPSHOT */
+#endif/* !USE_MPROTECT_SNAPSHOT */
 
 /**
  * @brief Initializes the snapshot system
  * @param entryPoint the function that should run the program.
  */
 void snapshot_system_init(unsigned int numbackingpages,
-               unsigned int numsnapshots, unsigned int nummemoryregions,
-               unsigned int numheappages, VoidFuncPtr entryPoint)
+                                                                                                       unsigned int numsnapshots, unsigned int nummemoryregions,
+                                                                                                       unsigned int numheappages, VoidFuncPtr entryPoint)
 {
 #if USE_MPROTECT_SNAPSHOT
        mprot_snapshot_init(numbackingpages, numsnapshots, nummemoryregions, numheappages, entryPoint);
index f7c451c..e710d11 100644 (file)
@@ -38,12 +38,12 @@ static inline void print_stacktrace(int fd = STDERR_FILENO, unsigned int max_fra
 
        // iterate over the returned symbol lines. skip the first, it is the
        // address of this function.
-       for (int i = 1; i < addrlen; i++) {
+       for (int i = 1;i < addrlen;i++) {
                char *begin_name = 0, *begin_offset = 0, *end_offset = 0;
 
                // find parentheses and +address offset surrounding the mangled name:
                // ./module(function+0x15c) [0x8048a6d]
-               for (char *p = symbollist[i]; *p; ++p) {
+               for (char *p = symbollist[i];*p;++p) {
                        if (*p == '(')
                                begin_name = p;
                        else if (*p == '+')
@@ -67,14 +67,14 @@ static inline void print_stacktrace(int fd = STDERR_FILENO, unsigned int max_fra
                        char* ret = abi::__cxa_demangle(begin_name,
                                                                                                                                                        funcname, &funcnamesize, &status);
                        if (status == 0) {
-                               funcname = ret; // use possibly realloc()-ed string
+                               funcname = ret;                                                                                                 // use possibly realloc()-ed string
                                model_dprintf(fd, "  %s : %s+%s\n",
-                                                               symbollist[i], funcname, begin_offset);
+                                                                                       symbollist[i], funcname, begin_offset);
                        } else {
                                // demangling failed. Output function name as a C function with
                                // no arguments.
                                model_dprintf(fd, "  %s : %s()+%s\n",
-                                                               symbollist[i], begin_name, begin_offset);
+                                                                                       symbollist[i], begin_name, begin_offset);
                        }
                } else {
                        // couldn't parse the line? print the whole line.
@@ -91,4 +91,4 @@ static inline void print_stacktrace(FILE *out, unsigned int max_frames = 63)
        print_stacktrace(fileno(out), max_frames);
 }
 
-#endif // __STACKTRACE_H__
+#endif// __STACKTRACE_H__
index 85bb311..37aa909 100644 (file)
@@ -17,7 +17,7 @@
 template<typename _Tp>
 class ModelList : public std::list<_Tp, ModelAlloc<_Tp> >
 {
- public:
+public:
        typedef std::list< _Tp, ModelAlloc<_Tp> > list;
 
        ModelList() :
@@ -28,13 +28,13 @@ class ModelList : public std::list<_Tp, ModelAlloc<_Tp> >
                list(n, val)
        { }
 
-               MEMALLOC;
+       MEMALLOC;
 };
 
 template<typename _Tp>
 class SnapList : public std::list<_Tp, SnapshotAlloc<_Tp> >
 {
- public:
+public:
        typedef std::list<_Tp, SnapshotAlloc<_Tp> > list;
 
        SnapList() :
@@ -51,7 +51,7 @@ class SnapList : public std::list<_Tp, SnapshotAlloc<_Tp> >
 template<typename _Tp>
 class ModelVector : public std::vector<_Tp, ModelAlloc<_Tp> >
 {
- public:
+public:
        typedef std::vector< _Tp, ModelAlloc<_Tp> > vector;
 
        ModelVector() :
@@ -62,13 +62,13 @@ class ModelVector : public std::vector<_Tp, ModelAlloc<_Tp> >
                vector(n, val)
        { }
 
-               MEMALLOC;
+       MEMALLOC;
 };
 
 template<typename _Tp>
 class SnapVector : public std::vector<_Tp, SnapshotAlloc<_Tp> >
 {
- public:
+public:
        typedef std::vector< _Tp, SnapshotAlloc<_Tp> > vector;
 
        SnapVector() :
@@ -82,4 +82,4 @@ class SnapVector : public std::vector<_Tp, SnapshotAlloc<_Tp> >
        SNAPSHOTALLOC;
 };
 
-#endif /* __STL_MODEL_H__ */
+#endif/* __STL_MODEL_H__ */
index 45e2465..8dbbbc2 100644 (file)
@@ -13,7 +13,7 @@
 #include "stl-model.h"
 
 class StoreLoadSet {
- public:
+public:
        StoreLoadSet();
        ~StoreLoadSet();
        void add(EPRecord *op);
@@ -32,9 +32,9 @@ class StoreLoadSet {
        Constraint ** getRMWRValVars(ConstGen *cg, EPRecord * op);
        IntHashSet * getValues() {return &values;}
        bool removeAddress(const void *addr) {addresses.remove((uint64_t)addr);return addresses.isEmpty();}
-       
+
        MEMALLOC;
- private:
+private:
        void genEncoding();
        RecordSet storeloadset;
        IntHashSet addresses;
index 37ab6c9..690d19d 100644 (file)
@@ -48,7 +48,7 @@ typedef enum thread_state {
 
 /** @brief A Thread is created for each user-space thread */
 class Thread {
- public:
+public:
        Thread(thread_id_t tid);
        Thread(thread_id_t tid, thrd_t *t, void (*func)(void *), void *a, Thread *parent, EPRecord *r);
        ~Thread();
@@ -98,7 +98,7 @@ class Thread {
                Thread_free(p);
        }
        EPRecord * getParentRecord() {return parentrecord;}
- private:
+private:
        int create_context();
 
        /** @brief The parent Thread which created this Thread */
@@ -144,4 +144,4 @@ static inline int id_to_int(thread_id_t id)
        return id;
 }
 
-#endif /* __THREADS_MODEL_H__ */
+#endif/* __THREADS_MODEL_H__ */
index b7927c4..52b7ca9 100644 (file)
@@ -109,7 +109,7 @@ Thread::Thread(thread_id_t tid) :
        user_thread(NULL),
        waiting(NULL),
        id(tid),
-       state(THREAD_READY), /* Thread is always ready? */
+       state(THREAD_READY),                    /* Thread is always ready? */
        model_thread(true)
 {
        memset(&context, 0, sizeof(context));
@@ -189,7 +189,7 @@ void Thread::set_waiting(Thread *th) {
  */
 bool Thread::is_waiting_on(const Thread *t) {
        Thread *wait;
-       for (wait = waiting_on(); wait != NULL; wait = wait->waiting_on())
+       for (wait = waiting_on();wait != NULL;wait = wait->waiting_on())
                if (wait == t)
                        return true;
        return false;
index 9269223..fdfad21 100644 (file)
 #include "classlist.h"
 
 class ValueRecord {
- public:
+public:
        ValueRecord(IntHashSet *set);
-  ~ValueRecord();
-  Constraint * getValueEncoding(Constraint **vars, uint64_t value);
+       ~ValueRecord();
+       Constraint * getValueEncoding(Constraint **vars, uint64_t value);
        uint64_t getValue(Constraint **vars, bool *satsolution);
        uint getNumVars() {return numvars;}
        MEMALLOC;
- private:
+private:
        IntHashSet *set;
        uint numvars;
 };