From: bdemsky Date: Thu, 15 Dec 2016 06:29:12 +0000 (-0800) Subject: fix spacing with make tabbing X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satcheck.git;a=commitdiff_plain;h=086658309f67c28dc254b06bda5bafa8c3e191d6 fix spacing with make tabbing --- diff --git a/branchrecord.cc b/branchrecord.cc index e55aa24..c2c07b0 100644 --- a/branchrecord.cc +++ b/branchrecord.cc @@ -54,6 +54,6 @@ int BranchRecord::getBranchValue(bool * array) { } if (!alwaysexecuted) value--; - + return value; } diff --git a/branchrecord.h b/branchrecord.h index aa5e4a2..1cc1152 100644 --- a/branchrecord.h +++ b/branchrecord.h @@ -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 --- a/cgoal.h +++ b/cgoal.h @@ -15,7 +15,7 @@ #include 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); }; diff --git a/change.h b/change.h index f2e0bef..dc539f1 100644 --- 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; diff --git a/cmodelint.cc b/cmodelint.cc index 2c95808..549376a 100644 --- a/cmodelint.cc +++ b/cmodelint.cc @@ -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. */ diff --git a/common.cc b/common.cc index b445ce3..4227122 100644 --- 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 */ diff --git a/common.h b/common.h index 89b59b4..d4d86c6 100644 --- 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__ */ diff --git a/config.h b/config.h index 9efd32e..6ec9b80 100644 --- a/config.h +++ b/config.h @@ -37,11 +37,11 @@ #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() */ diff --git a/constgen.cc b/constgen.cc index 2f3375b..4f4ec3a 100644 --- a/constgen.cc +++ b/constgen.cc @@ -92,7 +92,7 @@ ConstGen::~ConstGen() { void resetstoreloadtable(StoreLoadSetHashTable * storeloadtable) { for(uint i=0;icapacity;i++) { - struct hashlistnode * ptr=& storeloadtable->table[i]; + struct hashlistnode * 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;isize();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;isize();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;inumValues();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 * 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;t3isize();t3i++) { EPRecord *t3rec=(*t2vec)[t3i]; Constraint *c13=getOrderConstraint(t1rec, t3rec); @@ -761,7 +761,7 @@ void ConstGen::genTransOrderConstraints(ModelVector * t1vec, ModelVe Constraint *intratransorder=new Constraint(OR, c21, c13); #endif ADDCONSTRAINT(intratransorder,"intratransorder"); - } + } for(uint t0i=0;t0i * 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 * depvec=execution->getRevDependences(record, VC_BASEINDEX); ASSERT(depvec->size()==1); @@ -1173,7 +1173,7 @@ void ConstGen::processBranch(EPRecord *record) { for(unsigned int i=0;inumValues();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;jnumValues();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 * 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 * 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 * inputs=execution->getRevDependences(record, VC_BASEINDEX); for(uint i=0;isize();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 * 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;igetSet(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;inumValues();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)); } diff --git a/constgen.h b/constgen.h index 68c02e7..8669a7f 100644 --- a/constgen.h +++ b/constgen.h @@ -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; diff --git a/constraint.cc b/constraint.cc index 457eaab..0656a35 100644 --- a/constraint.cc +++ b/constraint.cc @@ -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;jnegate(); + 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::simplify() { } case AND: { Constraint *array[numoperandsorvar]; - + ModelVector *vec=new ModelVector(); for(uint j=0;jnumoperandsorvar;j++) { //copy other elements @@ -413,7 +413,7 @@ Constraint * Constraint::negate() { for(uint i=0;inegate(); } - type=(type==AND)?OR:AND; + type=(type==AND) ? OR : AND; return this; } default: diff --git a/constraint.h b/constraint.h index bf97b31..4bfdd6b 100644 --- a/constraint.h +++ b/constraint.h @@ -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; diff --git a/context.cc b/context.cc index 7081656..56c3acb 100644 --- a/context.cc +++ b/context.cc @@ -33,4 +33,4 @@ int model_swapcontext(ucontext_t *oucp, ucontext_t *ucp) return 0; } -#endif /* MAC */ +#endif/* MAC */ diff --git a/context.h b/context.h index 948d89f..7160f49 100644 --- a/context.h +++ b/context.h @@ -21,13 +21,13 @@ 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__ */ diff --git a/eprecord.cc b/eprecord.cc index a11d2d6..a87167e 100644 --- a/eprecord.cc +++ b/eprecord.cc @@ -191,7 +191,7 @@ void EPRecord::print(int f) { delete it; } - + execpoint->print(f); } diff --git a/eprecord.h b/eprecord.h index 1d5e23a..54069de 100644 --- a/eprecord.h +++ b/eprecord.h @@ -20,18 +20,18 @@ typedef ModelVector 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 EPRecordIDSet; @@ -39,7 +39,7 @@ typedef HashSet 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; diff --git a/epvalue.h b/epvalue.h index 5d3a85b..13ceea8 100644 --- 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; diff --git a/equalsrecord.h b/equalsrecord.h index 14968ba..f5e66a3 100644 --- a/equalsrecord.h +++ b/equalsrecord.h @@ -12,15 +12,15 @@ #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 diff --git a/execpoint.cc b/execpoint.cc index 7b63213..7cfdff5 100644 --- a/execpoint.cc +++ b/execpoint.cc @@ -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=(sizesize)?size:ep->size; + unsigned int minsize=(sizesize) ? size : ep->size; for(unsigned int i=0;ipairarray[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; isize; i++) { + for(unsigned int i=0;isize;i++) { if (e1->pairarray[i]!=e2->pairarray[i]) return false; } diff --git a/execpoint.h b/execpoint.h index 74344ea..74650ed 100644 --- a/execpoint.h +++ b/execpoint.h @@ -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; diff --git a/functionrecord.cc b/functionrecord.cc index a7576b7..f9ff51f 100644 --- a/functionrecord.cc +++ b/functionrecord.cc @@ -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); diff --git a/functionrecord.h b/functionrecord.h index a7ecce8..5db5132 100644 --- a/functionrecord.h +++ b/functionrecord.h @@ -12,16 +12,16 @@ #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 diff --git a/hashset.h b/hashset.h index ecda268..140b85f 100644 --- a/hashset.h +++ b/hashset.h @@ -18,204 +18,204 @@ struct LinkNode { LinkNode<_Key> *next; }; -template +template class HashSet; template, 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, 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 diff --git a/hashtable.h b/hashtable.h index bcc8e70..16744bb 100644 --- a/hashtable.h +++ b/hashtable.h @@ -34,12 +34,12 @@ struct hashlistnode { template inline unsigned int default_hash_function(_Key hash) { - return (unsigned int)(((_KeyInt)hash) >> _Shift); + return (unsigned int)(((_KeyInt)hash) >> _Shift); } template 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, 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 *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 *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 *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 *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__ */ diff --git a/inc_solver.cc b/inc_solver.cc index daeeb1e..97f050c 100644 --- a/inc_solver.cc +++ b/inc_solver.cc @@ -12,153 +12,153 @@ #include 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; } diff --git a/inc_solver.h b/inc_solver.h index d5b7f3c..415dc8d 100644 --- a/inc_solver.h +++ b/inc_solver.h @@ -19,32 +19,32 @@ #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 diff --git a/loadrf.cc b/loadrf.cc index f536c1b..2d5984a 100644 --- 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; diff --git a/loadrf.h b/loadrf.h index 8ef7a19..12d4065 100644 --- a/loadrf.h +++ b/loadrf.h @@ -12,13 +12,13 @@ #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 --- 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(); diff --git a/mcexecution.cc b/mcexecution.cc index 9ea8af6..573b0b2 100644 --- a/mcexecution.cc +++ b/mcexecution.cc @@ -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 *>(); #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 * list=(*storebuffer)[id_to_int(tid)]; return list->empty(); } - + void MCExecution::doStore(thread_id_t tid) { SnapList * 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 *list=(*storebuffer)[tid]; - for(SnapList::reverse_iterator it=list->rbegin(); it != list->rend(); it++) { + for(SnapList::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;ipop(); //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;iget_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()); } - + ModelVector * recvec=revrecorddep->get(&pair); for(uint i=0;isize();i++) { if ((*recvec)[i]==record) diff --git a/mcexecution.h b/mcexecution.h index dca4228..a8c68f7 100644 --- a/mcexecution.h +++ b/mcexecution.h @@ -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 EPRecordSet; typedef HSIterator 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 * joinvec; ModelVector * sharedgoals; ModelVector * sharedfuncrecords; - + MCID currid; MCID id_addr; MCID id_oldvalue; diff --git a/mcschedule.cc b/mcschedule.cc index a86b0ff..f73671f 100644 --- a/mcschedule.cc +++ b/mcschedule.cc @@ -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;iget_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 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); diff --git a/mcschedule.h b/mcschedule.h index d7fb852..185a50f 100644 --- a/mcschedule.h +++ b/mcschedule.h @@ -15,20 +15,20 @@ #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; diff --git a/mcutil.h b/mcutil.h index 9699d7f..dd0f814 100644 --- 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 diff --git a/model.cc b/model.cc index 2ac46b8..506d116 100644 --- 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 --- 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__ */ diff --git a/mymemory.cc b/mymemory.cc index ea65c89..bbddf7e 100644 --- a/mymemory.cc +++ b/mymemory.cc @@ -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 */ diff --git a/mymemory.h b/mymemory.h index 0eca0a3..2bd7663 100644 --- a/mymemory.h +++ b/mymemory.h @@ -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 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 @@ -153,14 +153,14 @@ class ModelAlloc { /** Return that all specializations of this allocator are interchangeable. */ template bool operator ==(const ModelAlloc&, - const ModelAlloc&) throw() { + const ModelAlloc&) throw() { return true; } /** Return that all specializations of this allocator are interchangeable. */ template bool operator!= (const ModelAlloc&, - const ModelAlloc&) throw() { + const ModelAlloc&) throw() { return false; } @@ -176,15 +176,15 @@ bool operator!= (const ModelAlloc&, */ template 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 @@ -245,44 +245,44 @@ class SnapshotAlloc { /** Return that all specializations of this allocator are interchangeable. */ template bool operator ==(const SnapshotAlloc&, - const SnapshotAlloc&) throw() { + const SnapshotAlloc&) throw() { return true; } /** Return that all specializations of this allocator are interchangeable. */ template bool operator!= (const SnapshotAlloc&, - const SnapshotAlloc&) throw() { + const SnapshotAlloc&) 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 */ diff --git a/output.h b/output.h index f8aba6c..3c78875 100644 --- 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__ */ diff --git a/params.h b/params.h index 31e9267..78cedcb 100644 --- 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__ */ diff --git a/planner.cc b/planner.cc index f832fb9..d6cf00c 100644 --- a/planner.cc +++ b/planner.cc @@ -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) { diff --git a/planner.h b/planner.h index 9f35ddd..7ee76f1 100644 --- a/planner.h +++ b/planner.h @@ -20,7 +20,7 @@ typedef HSIteratorgetAddressEncoding(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;indexgetOrder(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: diff --git a/schedulebuilder.h b/schedulebuilder.h index be27aac..7ff4bb5 100644 --- a/schedulebuilder.h +++ b/schedulebuilder.h @@ -13,13 +13,13 @@ #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; diff --git a/snapshot-interface.cc b/snapshot-interface.cc index 4f9a4d5..dd48107 100644 --- a/snapshot-interface.cc +++ b/snapshot-interface.cc @@ -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 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 diff --git a/snapshot-interface.h b/snapshot-interface.h index 7c8516c..dbc6f88 100644 --- a/snapshot-interface.h +++ b/snapshot-interface.h @@ -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); diff --git a/snapshot.cc b/snapshot.cc index d06b887..b754d5b 100644 --- a/snapshot.cc +++ b/snapshot.cc @@ -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); diff --git a/stacktrace.h b/stacktrace.h index f7c451c..e710d11 100644 --- a/stacktrace.h +++ b/stacktrace.h @@ -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__ diff --git a/stl-model.h b/stl-model.h index 85bb311..37aa909 100644 --- a/stl-model.h +++ b/stl-model.h @@ -17,7 +17,7 @@ template 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 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 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 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__ */ diff --git a/storeloadset.h b/storeloadset.h index 45e2465..8dbbbc2 100644 --- a/storeloadset.h +++ b/storeloadset.h @@ -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; diff --git a/threads-model.h b/threads-model.h index 37ab6c9..690d19d 100644 --- a/threads-model.h +++ b/threads-model.h @@ -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__ */ diff --git a/threads.cc b/threads.cc index b7927c4..52b7ca9 100644 --- a/threads.cc +++ b/threads.cc @@ -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; diff --git a/valuerecord.h b/valuerecord.h index 9269223..fdfad21 100644 --- a/valuerecord.h +++ b/valuerecord.h @@ -12,14 +12,14 @@ #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; };