From: bdemsky <bdemsky@uci.edu>
Date: Thu, 15 Dec 2016 06:29:12 +0000 (-0800)
Subject: fix spacing with make tabbing
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=086658309f67c28dc254b06bda5bafa8c3e191d6;p=satcheck.git
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 <stdint.h>
class CGoal {
- public:
+public:
CGoal(unsigned int num, uint64_t *vals);
~CGoal();
unsigned int getNum() {return num;}
@@ -25,12 +25,12 @@ class CGoal {
void print();
MEMALLOC;
- private:
+private:
uint64_t * valarray;
uint64_t outputvalue;
unsigned int num;
unsigned int hash;
-
+
friend bool CGoalEquals(CGoal *cg1, CGoal *cg2);
friend unsigned int CGoalHash(CGoal *cg);
};
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;i<storeloadtable->capacity;i++) {
- struct hashlistnode<const void *, StoreLoadSet *> * ptr=& storeloadtable->table[i];
+ struct hashlistnode<const void *, StoreLoadSet *> * ptr=&storeloadtable->table[i];
if (ptr->val != NULL) {
if (ptr->val->removeAddress(ptr->key))
delete ptr->val;
@@ -106,7 +106,7 @@ void resetstoreloadtable(StoreLoadSetHashTable * storeloadtable) {
delete storeloadtable->zero->val;
} else
ASSERT(false);
- model_free(storeloadtable -> zero);
+ model_free(storeloadtable->zero);
storeloadtable->zero = NULL;
}
storeloadtable->size = 0;
@@ -182,11 +182,11 @@ bool ConstGen::canReuseEncoding() {
#endif
model_print("start %lu, finish %lu\n", start,finish);
model_print("Incremental time = %12.6f\n", ((double)(finish-start))/1000000);
-
+
if (solution==NULL) {
return false;
}
-
+
//Zero out the achieved goals
for(uint i=0;i<goalset->size();i++) {
Constraint *var=goalvararray[i];
@@ -215,7 +215,7 @@ bool ConstGen::process() {
delete solver;
solver = NULL;
}
-
+
solver=new IncrementalSolver();
traverse(true);
@@ -279,13 +279,13 @@ bool ConstGen::process() {
model_print("start %lu, finish %lu\n", start,finish);
model_print("Initial time = %12.6f\n", ((double)(finish-start))/1000000);
-
+
if (solution==NULL) {
delete solver;
solver = NULL;
return true;
}
-
+
//Zero out the achieved goals
for(uint i=0;i<goalset->size();i++) {
Constraint *var=goalvararray[i];
@@ -309,7 +309,7 @@ void ConstGen::printEventGraph() {
schedule_graph++;
int file=open(buffer,O_WRONLY|O_CREAT|O_TRUNC, S_IRWXU);
model_dprintf(file, "digraph eventgraph {\n");
-
+
EPRecord *first=execution->getEPRecord(MCID_FIRST);
printRecord(first, file);
while(!workstack->empty()) {
@@ -328,7 +328,7 @@ void ConstGen::doPrint(EPRecord *record, int file) {
model_dprintf(file, "\"];\n");
if (record->getNextRecord()!=NULL)
model_dprintf(file, "%lu->%lu;\n", (uintptr_t) record, (uintptr_t) record->getNextRecord());
-
+
if (record->getChildRecord()!=NULL)
model_dprintf(file, "%lu->%lu[color=red];\n", (uintptr_t) record, (uintptr_t) record->getChildRecord());
}
@@ -357,7 +357,7 @@ void ConstGen::printRecord(EPRecord *record, int file) {
workstack->push_back(next);
for(uint i=0;i<record->numValues();i++) {
EPValue *branchdir=record->getValue(i);
-
+
//Could have an empty branch, so make sure the branch actually
//runs code
if (branchdir->getFirstRecord()!=NULL) {
@@ -385,13 +385,13 @@ void ConstGen::traverse(bool initial) {
}
/** This method looks for all other memory operations that could
- potentially share a location, and build partitions of memory
- locations such that all memory locations that can share the same
- address are in the same group.
-
- These memory operations should share an encoding of addresses and
- values.
-*/
+ potentially share a location, and build partitions of memory
+ locations such that all memory locations that can share the same
+ address are in the same group.
+
+ These memory operations should share an encoding of addresses and
+ values.
+ */
void ConstGen::groupMemoryOperations(EPRecord *op) {
/** Handle our first address */
@@ -432,18 +432,18 @@ RecordSet * ConstGen::computeConflictSet(EPRecord *store, EPRecord *load, Record
}
}
delete storeaddr;
-
+
ASSERT(numaddr!=0);
if (numaddr!=1)
return NULL;
-
+
RecordSet *srscopy=baseset->copy();
RecordIterator *sri=srscopy->iterator();
while(sri->hasNext()) {
bool pruneconflictstore=false;
EPRecord *conflictstore=sri->next();
bool conflictafterstore=getOrderConstraint(store,conflictstore)->isTrue();
- bool conflictbeforeload=getOrderConstraint(conflictstore,load)->isTrue();
+ bool conflictbeforeload=getOrderConstraint(conflictstore,load)->isTrue();
if (conflictafterstore) {
RecordIterator *sricheck=srscopy->iterator();
@@ -455,7 +455,7 @@ RecordSet * ConstGen::computeConflictSet(EPRecord *store, EPRecord *load, Record
bool checkbeforeconflict=getOrderConstraint(checkstore,conflictstore)->isTrue();
if (!checkbeforeconflict)
continue;
-
+
//See if the checkstore must store to the relevant address
IntHashSet * storeaddr=checkstore->getSet(VC_ADDRINDEX);
@@ -483,7 +483,7 @@ RecordSet * ConstGen::computeConflictSet(EPRecord *store, EPRecord *load, Record
bool checkbeforeload=getOrderConstraint(checkstore, load)->isTrue();
if (!checkbeforeload)
continue;
-
+
//See if the checkstore must store to the relevant address
IntHashSet * storeaddr=checkstore->getSet(VC_ADDRINDEX);
if (storeaddr->getSize()!=1 || !storeaddr->contains((uint64_t)commonaddr))
@@ -502,7 +502,7 @@ RecordSet * ConstGen::computeConflictSet(EPRecord *store, EPRecord *load, Record
sri->remove();
}
}
-
+
delete sri;
return srscopy;
}
@@ -513,7 +513,7 @@ RecordSet * ConstGen::computeConflictSet(EPRecord *store, EPRecord *load, Record
RecordSet * ConstGen::getMayReadFromSet(EPRecord *load) {
if (load->getSet(VC_ADDRINDEX)->getSize()==1)
return getMayReadFromSetOpt(load);
-
+
RecordSet *srs=loadtable->get(load);
ExecPoint *epload=load->getEP();
thread_id_t loadtid=epload->get_tid();
@@ -523,7 +523,7 @@ RecordSet * ConstGen::getMayReadFromSet(EPRecord *load) {
IntHashSet *addrset=load->getSet(VC_ADDRINDEX);
IntIterator *ait=addrset->iterator();
-
+
while(ait->hasNext()) {
void *addr=(void *)ait->next();
RecordSet *rs=execution->getStoreTable(addr);
@@ -594,7 +594,7 @@ RecordSet * ConstGen::getMayReadFromSetOpt(EPRecord *load) {
}
/** This function merges two recordsets and updates the storeloadtable
- accordingly. */
+ accordingly. */
void ConstGen::mergeSets(StoreLoadSet *to, StoreLoadSet *from) {
RecordIterator * sri=from->iterator();
@@ -628,7 +628,7 @@ void ConstGen::insertTSOAction(EPRecord *load) {
while (j>0) {
EPRecord *oldrec=(*vector)[--j];
EventType oldrec_t=oldrec->getType();
-
+
if (((oldrec_t == RMW) || (oldrec_t==FENCE)) &&
isAlwaysExecuted(oldrec)) {
return;
@@ -681,7 +681,7 @@ void ConstGen::genTSOTransOrderConstraints() {
#endif
/** This function creates ordering constraints to implement SC for
- memory operations. */
+ memory operations. */
void ConstGen::insertAction(EPRecord *record) {
thread_id_t tid=record->getEP()->get_tid();
@@ -732,15 +732,15 @@ void ConstGen::genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVe
EPRecord *t2rec=(*t2vec)[t2i];
/* Note: One only really needs to generate the first constraint
- in the first loop and the last constraint in the last loop.
- I tried this and performance suffered on linuxrwlocks and
- linuxlocks at the current time. BD - August 2014*/
+ in the first loop and the last constraint in the last loop.
+ I tried this and performance suffered on linuxrwlocks and
+ linuxlocks at the current time. BD - August 2014*/
Constraint *c21=getOrderConstraint(t2rec, t1rec);
/* short circuit for the trivial case */
if (c21->isTrue())
continue;
-
+
for(uint t3i=t2i+1;t3i<t2vec->size();t3i++) {
EPRecord *t3rec=(*t2vec)[t3i];
Constraint *c13=getOrderConstraint(t1rec, t3rec);
@@ -761,7 +761,7 @@ void ConstGen::genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVe
Constraint *intratransorder=new Constraint(OR, c21, c13);
#endif
ADDCONSTRAINT(intratransorder,"intratransorder");
- }
+ }
for(uint t0i=0;t0i<t1i;t0i++) {
EPRecord *t0rec=(*t1vec)[t0i];
@@ -784,7 +784,7 @@ void ConstGen::genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVe
Constraint *intratransorder=new Constraint(OR, c21, c02);
#endif
ADDCONSTRAINT(intratransorder,"intratransorder");
- }
+ }
}
}
}
@@ -865,7 +865,7 @@ void ConstGen::printNegConstraint(uint value) {
void ConstGen::printConstraint(uint value) {
solver->addClauseLiteral(value);
}
-
+
bool * ConstGen::runSolver() {
int solution=solver->solve();
if (solution == IS_UNSAT) {
@@ -964,7 +964,7 @@ bool ConstGen::orderThread(EPRecord *first, EPRecord *second) {
EPRecord *thr2start=tr2->getParentRecord();
if (thr2start!=NULL) {
ExecPoint *epthr2start=thr2start->getEP();
- if (epthr2start->get_tid()==thr1 &&
+ if (epthr2start->get_tid()==thr1 &&
ep1->compare(epthr2start)==CR_AFTER)
return true;
}
@@ -1027,7 +1027,7 @@ StoreLoadSet * ConstGen::getStoreLoadSet(EPRecord *record) {
}
/** Returns a constraint that is true if the output of record has the
- given value. */
+ given value. */
Constraint * ConstGen::getRetValueEncoding(EPRecord *record, uint64_t value) {
switch(record->getType()) {
@@ -1083,7 +1083,7 @@ bool ConstGen::subsumesExecutionConstraint(EPRecord *recordsubsumes, EPRecord *r
RecordIterator *sri=srs->iterator();
while(sri->hasNext()) {
EPRecord *rec=sri->next();
-
+
if (!getOrderConstraint(rec, record)->isTrue()) {
delete sri;
return false;
@@ -1097,7 +1097,7 @@ bool ConstGen::subsumesExecutionConstraint(EPRecord *recordsubsumes, EPRecord *r
Constraint * ConstGen::getExecutionConstraint(EPRecord *record) {
EPValue *branch=record->getBranch();
RecordSet *srs=execcondtable->get(record);
- int size=srs==NULL?0:srs->getSize();
+ int size=srs==NULL ? 0 : srs->getSize();
if (branch!=NULL)
size++;
@@ -1128,7 +1128,7 @@ Constraint * ConstGen::getExecutionConstraint(EPRecord *record) {
bool ConstGen::isAlwaysExecuted(EPRecord *record) {
EPValue *branch=record->getBranch();
RecordSet *srs=execcondtable->get(record);
- int size=srs==NULL?0:srs->getSize();
+ int size=srs==NULL ? 0 : srs->getSize();
if (branch!=NULL)
size++;
@@ -1165,7 +1165,7 @@ void ConstGen::processBranch(EPRecord *record) {
Constraint *parentbranch=new Constraint(IMPLIES, br->getAnyBranch(), baseconstraint);
ADDCONSTRAINT(parentbranch, "parentbranch");
}
-
+
/** Insert criteria for directions */
ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
ASSERT(depvec->size()==1);
@@ -1173,7 +1173,7 @@ void ConstGen::processBranch(EPRecord *record) {
for(unsigned int i=0;i<record->numValues();i++) {
EPValue * branchval=record->getValue(i);
uint64_t val=branchval->getValue();
-
+
if (val==0) {
Constraint *execconstraint=getExecutionConstraint(record);
Constraint *br_false=new Constraint(IMPLIES,
@@ -1186,7 +1186,7 @@ void ConstGen::processBranch(EPRecord *record) {
Constraint *execconstraint=getExecutionConstraint(record);
Constraint *br_true1=new Constraint(IMPLIES, new Constraint(AND, getRetValueEncoding(val_record, 0)->negate(),
execconstraint),
- br->getBranch(branchval));
+ br->getBranch(branchval));
ADDCONSTRAINT(br_true1, "br_true1");
} else {
for(unsigned int j=0;j<val_record->numValues();j++) {
@@ -1224,7 +1224,7 @@ void ConstGen::processLoad(EPRecord *record) {
}
/** This procedure generates the constraints that set the address
- variables for load/store/rmw operations. */
+ variables for load/store/rmw operations. */
void ConstGen::processAddresses(EPRecord *record) {
StoreLoadSet *sls=getStoreLoadSet(record);
@@ -1242,7 +1242,7 @@ void ConstGen::processAddresses(EPRecord *record) {
IntIterator *it=record->getSet(VC_ADDRINDEX)->iterator();
uintptr_t offset=record->getOffset();
-
+
while(it->hasNext()) {
uint64_t addr=it->next();
Constraint *srcenc=getRetValueEncoding(src, addr-offset);
@@ -1279,7 +1279,7 @@ void ConstGen::processCAS(EPRecord *record) {
ASSERT(depveccas->size()==1);
EPRecord *src=(*depveccas)[0];
IntIterator *it=getStoreLoadSet(record)->getValues()->iterator();
-
+
while(it->hasNext()) {
uint64_t valcas=it->next();
Constraint *srcenc=getRetValueEncoding(src, valcas);
@@ -1324,7 +1324,7 @@ void ConstGen::processCAS(EPRecord *record) {
ASSERT(depvec->size()==1);
EPRecord *src=(*depvec)[0];
IntIterator *it=record->getStoreSet()->iterator();
-
+
while(it->hasNext()) {
uint64_t val=it->next();
Constraint *srcenc=getRetValueEncoding(src, val);
@@ -1340,11 +1340,11 @@ void ConstGen::processCAS(EPRecord *record) {
delete it;
}
StoreLoadSet *sls=getStoreLoadSet(record);
-
+
Constraint *repeatval=generateEquivConstraint(sls->getNumValVars(), sls->getValVars(this, record), sls->getRMWRValVars(this, record));
Constraint *failcas=new Constraint(IMPLIES, eq->negate(), repeatval);
ADDCONSTRAINT(failcas,"casmemfail");
-
+
processAddresses(record);
}
@@ -1365,7 +1365,7 @@ void ConstGen::processEXC(EPRecord *record) {
ASSERT(depvec->size()==1);
EPRecord *src=(*depvec)[0];
IntIterator *it=record->getStoreSet()->iterator();
-
+
while(it->hasNext()) {
uint64_t val=it->next();
Constraint *srcenc=getRetValueEncoding(src, val);
@@ -1387,7 +1387,7 @@ void ConstGen::processAdd(EPRecord *record) {
Constraint *var=getNewVar();
Constraint *newadd=new Constraint(AND, var, getExecutionConstraint(record));
ADDGOAL(record, newadd, "newadd");
-
+
ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
if (depvec==NULL) {
IntIterator *valit=record->getSet(VC_BASEINDEX)->iterator();
@@ -1428,7 +1428,7 @@ void ConstGen::processAdd(EPRecord *record) {
Constraint *storeenc=getMemValueEncoding(record, sum);
Constraint *notvar=var->negate();
Constraint *addop=new Constraint(IMPLIES, new Constraint(AND, srcenc, loadenc),
- new Constraint(AND, notvar, storeenc));
+ new Constraint(AND, notvar, storeenc));
ADDCONSTRAINT(addop,"addinputvar");
}
}
@@ -1441,10 +1441,10 @@ void ConstGen::processAdd(EPRecord *record) {
}
/** This function ensures that the value of a store's SAT variables
- matches the store's input value.
+ matches the store's input value.
- TODO: Could optimize the case where the encodings are the same...
-*/
+ TODO: Could optimize the case where the encodings are the same...
+ */
void ConstGen::processStore(EPRecord *record) {
ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
@@ -1458,7 +1458,7 @@ void ConstGen::processStore(EPRecord *record) {
ASSERT(depvec->size()==1);
EPRecord *src=(*depvec)[0];
IntIterator *it=record->getStoreSet()->iterator();
-
+
while(it->hasNext()) {
uint64_t val=it->next();
Constraint *srcenc=getRetValueEncoding(src, val);
@@ -1488,7 +1488,7 @@ void ConstGen::processLoopPhi(EPRecord *record) {
while(rit->hasNext()) {
struct RecordIDPair *rip=rit->next();
EPRecord *input=rip->idrecord;
-
+
IntIterator * it=record->getSet(VC_BASEINDEX)->iterator();
while(it->hasNext()) {
uint64_t value=it->next();
@@ -1509,7 +1509,7 @@ void ConstGen::processPhi(EPRecord *record) {
ModelVector<EPRecord *> * inputs=execution->getRevDependences(record, VC_BASEINDEX);
for(uint i=0;i<inputs->size();i++) {
EPRecord * input=(*inputs)[i];
-
+
IntIterator * it=record->getSet(VC_BASEINDEX)->iterator();
while(it->hasNext()) {
uint64_t value=it->next();
@@ -1585,30 +1585,30 @@ void ConstGen::processFunction(EPRecord *record) {
void ConstGen::processEquals(EPRecord *record) {
ASSERT (record->getNumFuncInputs() == 2);
EPRecord * inputs[2];
-
+
for(uint i=0;i<2;i++) {
ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, i+VC_BASEINDEX);
if (depvec==NULL) {
inputs[i]=NULL;
} else if (depvec->size()==1) {
inputs[i]=(*depvec)[0];
- } else ASSERT(false);
+ } else ASSERT(false);
}
//rely on this being a variable
Constraint * outputtrue=getRetValueEncoding(record, 1);
ASSERT(outputtrue->getType()==VAR);
-
+
if (inputs[0]!=NULL && inputs[1]!=NULL &&
(inputs[0]->getType()==LOAD || inputs[0]->getType()==RMW) &&
(inputs[1]->getType()==LOAD || inputs[1]->getType()==RMW) &&
(getStoreLoadSet(inputs[0])==getStoreLoadSet(inputs[1]))) {
StoreLoadSet * sls=getStoreLoadSet(inputs[0]);
int numvalvars=sls->getNumValVars();
- Constraint **valvar1=(inputs[0]->getType()==RMW)?sls->getRMWRValVars(this, inputs[0]):sls->getValVars(this, inputs[0]);
- Constraint **valvar2=(inputs[1]->getType()==RMW)?sls->getRMWRValVars(this, inputs[1]):sls->getValVars(this, inputs[1]);
+ Constraint **valvar1=(inputs[0]->getType()==RMW) ? sls->getRMWRValVars(this, inputs[0]) : sls->getValVars(this, inputs[0]);
+ Constraint **valvar2=(inputs[1]->getType()==RMW) ? sls->getRMWRValVars(this, inputs[1]) : sls->getValVars(this, inputs[1]);
//new test
-
+
Constraint *vars[numvalvars];
for(int i=0;i<numvalvars;i++) {
vars[i]=getNewVar();
@@ -1632,20 +1632,20 @@ void ConstGen::processEquals(EPRecord *record) {
ADDCONSTRAINT(new Constraint(IMPLIES, outputtrue, new Constraint(AND, numvalvars, vars)), "impequal2");
/*
-
- Constraint * functionimplication=new Constraint(IMPLIES,generateEquivConstraint(numvalvars, valvar1, valvar2), outputtrue);
- ADDCONSTRAINT(functionimplication,"equalsimplspecial");
- Constraint * functionimplicationneg=new Constraint(IMPLIES,outputtrue, generateEquivConstraint(numvalvars, valvar1, valvar2));
- ADDCONSTRAINT(functionimplicationneg,"equalsimplspecialneg");
- */
+
+ Constraint * functionimplication=new Constraint(IMPLIES,generateEquivConstraint(numvalvars, valvar1, valvar2), outputtrue);
+ ADDCONSTRAINT(functionimplication,"equalsimplspecial");
+ Constraint * functionimplicationneg=new Constraint(IMPLIES,outputtrue, generateEquivConstraint(numvalvars, valvar1, valvar2));
+ ADDCONSTRAINT(functionimplicationneg,"equalsimplspecialneg");
+ */
return;
}
if (inputs[0]==NULL && inputs[1]==NULL) {
- IntIterator *iit0=record->getSet(VC_BASEINDEX+0)->iterator();
+ IntIterator *iit0=record->getSet(VC_BASEINDEX+0)->iterator();
uint64_t constval=iit0->next();
delete iit0;
- IntIterator *iit1=record->getSet(VC_BASEINDEX+1)->iterator();
+ IntIterator *iit1=record->getSet(VC_BASEINDEX+1)->iterator();
uint64_t constval2=iit1->next();
delete iit1;
@@ -1655,12 +1655,12 @@ void ConstGen::processEquals(EPRecord *record) {
ADDCONSTRAINT(outputtrue->negate(), "equalsconst");
}
return;
- }
-
+ }
+
if (inputs[0]==NULL ||
inputs[1]==NULL) {
- int nullindex=inputs[0]==NULL?0:1;
- IntIterator *iit=record->getSet(VC_BASEINDEX+nullindex)->iterator();
+ int nullindex=inputs[0]==NULL ? 0 : 1;
+ IntIterator *iit=record->getSet(VC_BASEINDEX+nullindex)->iterator();
uint64_t constval=iit->next();
delete iit;
@@ -1674,17 +1674,17 @@ void ConstGen::processEquals(EPRecord *record) {
Constraint *functionimplication2=new Constraint(IMPLIES, outputtrue, l2);
ADDCONSTRAINT(functionimplication2,"equalsimpl");
}
-
- IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
+
+ IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
while(iit->hasNext()) {
uint64_t val1=iit->next();
-
- IntIterator *iit2=record->getSet(VC_BASEINDEX+1)->iterator();
+
+ IntIterator *iit2=record->getSet(VC_BASEINDEX+1)->iterator();
while(iit2->hasNext()) {
uint64_t val2=iit2->next();
Constraint *l=getRetValueEncoding(inputs[0], val1);
Constraint *r=getRetValueEncoding(inputs[1], val2);
- Constraint *imp=(val1==val2)?outputtrue:outputtrue->negate();
+ Constraint *imp=(val1==val2) ? outputtrue : outputtrue->negate();
Constraint * functionimplication=new Constraint(IMPLIES, new Constraint(AND, l, r), imp);
ADDCONSTRAINT(functionimplication,"equalsimpl");
}
@@ -1750,7 +1750,7 @@ void ConstGen::processRecord(EPRecord *record) {
case FENCE:
processFence(record);
break;
-#endif
+#endif
case RMW:
#ifdef TSO
processFence(record);
@@ -1831,7 +1831,7 @@ void ConstGen::visitRecord(EPRecord *record) {
void ConstGen::recordExecCond(EPRecord *record) {
ExecPoint *eprecord=record->getEP();
EPValue * branchval=record->getBranch();
- EPRecord * branch=(branchval==NULL)?NULL:branchval->getRecord();
+ EPRecord * branch=(branchval==NULL) ? NULL : branchval->getRecord();
ExecPoint *epbranch= (branch==NULL) ? NULL : branch->getEP();
RecordSet *srs=NULL;
RecordIterator *sri=nonlocaltrans->iterator();
@@ -1899,7 +1899,7 @@ void ConstGen::traverseRecord(EPRecord *record, bool initial) {
workstack->push_back(next);
for(uint i=0;i<record->numValues();i++) {
EPValue *branchdir=record->getValue(i);
-
+
//Could have an empty branch, so make sure the branch actually
//runs code
if (branchdir->getFirstRecord()!=NULL)
@@ -1921,5 +1921,5 @@ unsigned int RecPairHash(RecPair *rp) {
bool RecPairEquals(RecPair *r1, RecPair *r2) {
return ((r1->epr1==r2->epr1)&&(r1->epr2==r2->epr2)) ||
- ((r1->epr1==r2->epr2)&&(r1->epr2==r2->epr1));
+ ((r1->epr1==r2->epr2)&&(r1->epr2==r2->epr1));
}
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;j<numvars;j++) {
- carray[j]=((value&1)==1)?vars[j]:vars[j]->negate();
+ carray[j]=((value&1)==1) ? vars[j] : vars[j]->negate();
value=value>>1;
}
@@ -220,7 +220,7 @@ Constraint * generateLTConstraint(ConstGen *cg, uint numvars, Constraint ** vars
}
andarray[andi++]=new Constraint(OR, ori, orarray);
- value=value+(1<<(__builtin_ctz(value)));//flip the last one
+ value=value+(1<<(__builtin_ctz(value))); //flip the last one
}
}
@@ -345,7 +345,7 @@ ModelVector<Constraint *> * Constraint::simplify() {
}
case AND: {
Constraint *array[numoperandsorvar];
-
+
ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
for(uint j=0;j<c->numoperandsorvar;j++) {
//copy other elements
@@ -413,7 +413,7 @@ Constraint * Constraint::negate() {
for(uint i=0;i<numoperandsorvar;i++) {
operands[i]=operands[i]->negate();
}
- type=(type==AND)?OR:AND;
+ type=(type==AND) ? OR : AND;
return this;
}
default:
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<EPValue *> ValueVector;
const char * eventToStr(EventType event);
struct RecordIDPair {
- EPRecord *record;
+ EPRecord *record;
EPRecord *idrecord;
};
inline unsigned int RIDP_hash_function(struct RecordIDPair * pair) {
- return (unsigned int)(((uintptr_t)pair->record) >> 4) ^ ((uintptr_t)pair->idrecord);
+ return (unsigned int)(((uintptr_t)pair->record) >> 4) ^ ((uintptr_t)pair->idrecord);
}
inline bool RIDP_equals(struct RecordIDPair * key1, struct RecordIDPair * key2) {
if (key1==NULL)
return key1==key2;
- return key1->record == key2->record && key1->idrecord == key2->idrecord;
+ return key1->record == key2->record && key1->idrecord == key2->idrecord;
}
typedef HashSet<struct RecordIDPair *, uintptr_t, 0, model_malloc, model_calloc, model_free, RIDP_hash_function, RIDP_equals> EPRecordIDSet;
@@ -39,7 +39,7 @@ typedef HashSet<struct RecordIDPair *, uintptr_t, 0, model_malloc, model_calloc,
typedef HSIterator<struct RecordIDPair *, uintptr_t, 0, model_malloc, model_calloc, model_free, RIDP_hash_function, RIDP_equals> EPRecordIDIterator;
class EPRecord {
- public:
+public:
EPRecord(EventType event, ExecPoint *execpoint, EPValue *branch, uintptr_t _offset, unsigned int numinputs,uint len, bool anyvalue = false);
~EPRecord();
ExecPoint * getEP() {return execpoint;}
@@ -83,8 +83,8 @@ class EPRecord {
bool isSharedGoals() {return func_shares_goalset;}
uintptr_t getOffset() {return offset;}
MEMALLOC;
-
- private:
+
+private:
ValueVector * valuevector;
ExecPoint * execpoint;
CGoalSet *completed;
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=(size<ep->size)?size:ep->size;
+ unsigned int minsize=(size<ep->size) ? size : ep->size;
for(unsigned int i=0;i<minsize;i+=2) {
ASSERT(pairarray[i]==ep->pairarray[i]);
if (pairarray[i+1]!=ep->pairarray[i+1]) {
@@ -122,7 +122,7 @@ bool ExecPointEquals(ExecPoint *e1, ExecPoint * e2) {
return e2==NULL;
if (e1->tid != e2->tid || e1->size != e2->size || e1->hashvalue != e2->hashvalue)
return false;
- for(unsigned int i=0; i<e1->size; i++) {
+ for(unsigned int i=0;i<e1->size;i++) {
if (e1->pairarray[i]!=e2->pairarray[i])
return false;
}
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<typename _Key, typename _KeyInt, int _Shift, void *
-(* _malloc)(size_t), void * (* _calloc)(size_t, size_t), void (*_free)(void *), unsigned int (*hash_function
-)(_Key), bool (*equals)(_Key, _Key)>
+template<typename _Key, typename _KeyInt, int _Shift, void *
+ (* _malloc)(size_t), void * (* _calloc)(size_t, size_t), void (*_free)(void *), unsigned int (*hash_function
+ )(_Key), bool (*equals)(_Key, _Key)>
class HashSet;
template<typename _Key, typename _KeyInt, int _Shift, void * (* _malloc)(size_t), void * (* _calloc)(size_t, size_t), void (*_free)(void *), unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = default_equals<_Key> >
class HSIterator {
- public:
- HSIterator(LinkNode<_Key> *_curr, HashSet <_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * _set) :
- curr(_curr),
- set(_set)
- {
- }
-
- /** Override: new operator */
- void * operator new(size_t size) {
- return _malloc(size);
- }
-
- /** Override: delete operator */
- void operator delete(void *p, size_t size) {
- _free(p);
- }
-
- /** Override: new[] operator */
- void * operator new[](size_t size) {
- return _malloc(size);
- }
-
- /** Override: delete[] operator */
- void operator delete[](void *p, size_t size) {
- _free(p);
- }
-
- bool hasNext() {
- return curr!=NULL;
- }
-
- _Key next() {
- _Key k=curr->key;
- last=curr;
- curr=curr->next;
- return k;
- }
-
- _Key currKey() {
- return last->key;
- }
-
- void remove() {
- _Key k=last->key;
- set->remove(k);
- }
-
- private:
- LinkNode<_Key> *curr;
- LinkNode<_Key> *last;
- HashSet <_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * set;
+public:
+ HSIterator(LinkNode<_Key> *_curr, HashSet <_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * _set) :
+ curr(_curr),
+ set(_set)
+ {
+ }
+
+ /** Override: new operator */
+ void * operator new(size_t size) {
+ return _malloc(size);
+ }
+
+ /** Override: delete operator */
+ void operator delete(void *p, size_t size) {
+ _free(p);
+ }
+
+ /** Override: new[] operator */
+ void * operator new[](size_t size) {
+ return _malloc(size);
+ }
+
+ /** Override: delete[] operator */
+ void operator delete[](void *p, size_t size) {
+ _free(p);
+ }
+
+ bool hasNext() {
+ return curr!=NULL;
+ }
+
+ _Key next() {
+ _Key k=curr->key;
+ last=curr;
+ curr=curr->next;
+ return k;
+ }
+
+ _Key currKey() {
+ return last->key;
+ }
+
+ void remove() {
+ _Key k=last->key;
+ set->remove(k);
+ }
+
+private:
+ LinkNode<_Key> *curr;
+ LinkNode<_Key> *last;
+ HashSet <_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * set;
};
template<typename _Key, typename _KeyInt, int _Shift = 0, void * (* _malloc)(size_t) = snapshot_malloc, void * (* _calloc)(size_t, size_t) = snapshot_calloc, void (*_free)(void *) = snapshot_free, unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = default_equals<_Key> >
class HashSet {
- public:
- HashSet(unsigned int initialcapacity = 16, double factor = 0.5) :
- table(new HashTable<_Key, LinkNode<_Key> *, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals>(initialcapacity, factor)),
- list(NULL),
- tail(NULL)
- {
- }
-
- /** @brief Hashset destructor */
- ~HashSet() {
- LinkNode<_Key> *tmp=list;
- while(tmp!=NULL) {
- LinkNode<_Key> *tmpnext=tmp->next;
- _free(tmp);
- tmp=tmpnext;
- }
- delete table;
- }
-
- HashSet<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * copy() {
- HashSet<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> *copy=new HashSet<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals>(table->getCapacity(), table->getLoadFactor());
- HSIterator<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * it=iterator();
- while(it->hasNext())
- copy->add(it->next());
- delete it;
- return copy;
- }
-
- void reset() {
- LinkNode<_Key> *tmp=list;
- while(tmp!=NULL) {
- LinkNode<_Key> *tmpnext=tmp->next;
- _free(tmp);
- tmp=tmpnext;
- }
- list=tail=NULL;
- table->reset();
- }
-
- /** @brief Adds a new key to the hashset. Returns false if the key
- * is already present. */
-
- bool add(_Key key) {
- LinkNode<_Key> * val=table->get(key);
- if (val==NULL) {
- LinkNode<_Key> * newnode=(LinkNode<_Key> *) _malloc(sizeof(struct LinkNode<_Key>));
- newnode->prev=tail;
- newnode->next=NULL;
- newnode->key=key;
- if (tail!=NULL)
- tail->next=newnode;
- else
- list=newnode;
- tail=newnode;
- table->put(key, newnode);
- return true;
- } else
- return false;
- }
-
- /** @brief Gets the original key corresponding to this one from the
- * hashset. Returns NULL if not present. */
-
- _Key get(_Key key) {
- LinkNode<_Key> * val=table->get(key);
- if (val!=NULL)
- return val->key;
- else
- return NULL;
- }
-
- _Key getFirstKey() {
- return list->key;
- }
-
- bool contains(_Key key) {
- return table->get(key)!=NULL;
- }
-
- bool remove(_Key key) {
- LinkNode<_Key> * oldlinknode;
- oldlinknode=table->get(key);
- if (oldlinknode==NULL) {
- return false;
- }
- table->remove(key);
-
- //remove link node from the list
- if (oldlinknode->prev==NULL)
- list=oldlinknode->next;
- else
- oldlinknode->prev->next=oldlinknode->next;
- if (oldlinknode->next!=NULL)
- oldlinknode->next->prev=oldlinknode->prev;
- else
- tail=oldlinknode->prev;
- _free(oldlinknode);
- return true;
- }
-
- unsigned int getSize() {
- return table->getSize();
- }
-
- bool isEmpty() {
- return getSize()==0;
- }
-
-
-
- HSIterator<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * iterator() {
- return new HSIterator<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals>(list, this);
- }
-
- /** Override: new operator */
- void * operator new(size_t size) {
- return _malloc(size);
- }
-
- /** Override: delete operator */
- void operator delete(void *p, size_t size) {
- _free(p);
- }
-
- /** Override: new[] operator */
- void * operator new[](size_t size) {
- return _malloc(size);
- }
-
- /** Override: delete[] operator */
- void operator delete[](void *p, size_t size) {
- _free(p);
- }
- private:
- HashTable<_Key, LinkNode<_Key>*, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * table;
- LinkNode<_Key> *list;
- LinkNode<_Key> *tail;
+public:
+ HashSet(unsigned int initialcapacity = 16, double factor = 0.5) :
+ table(new HashTable<_Key, LinkNode<_Key> *, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals>(initialcapacity, factor)),
+ list(NULL),
+ tail(NULL)
+ {
+ }
+
+ /** @brief Hashset destructor */
+ ~HashSet() {
+ LinkNode<_Key> *tmp=list;
+ while(tmp!=NULL) {
+ LinkNode<_Key> *tmpnext=tmp->next;
+ _free(tmp);
+ tmp=tmpnext;
+ }
+ delete table;
+ }
+
+ HashSet<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * copy() {
+ HashSet<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> *copy=new HashSet<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals>(table->getCapacity(), table->getLoadFactor());
+ HSIterator<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * it=iterator();
+ while(it->hasNext())
+ copy->add(it->next());
+ delete it;
+ return copy;
+ }
+
+ void reset() {
+ LinkNode<_Key> *tmp=list;
+ while(tmp!=NULL) {
+ LinkNode<_Key> *tmpnext=tmp->next;
+ _free(tmp);
+ tmp=tmpnext;
+ }
+ list=tail=NULL;
+ table->reset();
+ }
+
+ /** @brief Adds a new key to the hashset. Returns false if the key
+ * is already present. */
+
+ bool add(_Key key) {
+ LinkNode<_Key> * val=table->get(key);
+ if (val==NULL) {
+ LinkNode<_Key> * newnode=(LinkNode<_Key> *)_malloc(sizeof(struct LinkNode<_Key>));
+ newnode->prev=tail;
+ newnode->next=NULL;
+ newnode->key=key;
+ if (tail!=NULL)
+ tail->next=newnode;
+ else
+ list=newnode;
+ tail=newnode;
+ table->put(key, newnode);
+ return true;
+ } else
+ return false;
+ }
+
+ /** @brief Gets the original key corresponding to this one from the
+ * hashset. Returns NULL if not present. */
+
+ _Key get(_Key key) {
+ LinkNode<_Key> * val=table->get(key);
+ if (val!=NULL)
+ return val->key;
+ else
+ return NULL;
+ }
+
+ _Key getFirstKey() {
+ return list->key;
+ }
+
+ bool contains(_Key key) {
+ return table->get(key)!=NULL;
+ }
+
+ bool remove(_Key key) {
+ LinkNode<_Key> * oldlinknode;
+ oldlinknode=table->get(key);
+ if (oldlinknode==NULL) {
+ return false;
+ }
+ table->remove(key);
+
+ //remove link node from the list
+ if (oldlinknode->prev==NULL)
+ list=oldlinknode->next;
+ else
+ oldlinknode->prev->next=oldlinknode->next;
+ if (oldlinknode->next!=NULL)
+ oldlinknode->next->prev=oldlinknode->prev;
+ else
+ tail=oldlinknode->prev;
+ _free(oldlinknode);
+ return true;
+ }
+
+ unsigned int getSize() {
+ return table->getSize();
+ }
+
+ bool isEmpty() {
+ return getSize()==0;
+ }
+
+
+
+ HSIterator<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * iterator() {
+ return new HSIterator<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals>(list, this);
+ }
+
+ /** Override: new operator */
+ void * operator new(size_t size) {
+ return _malloc(size);
+ }
+
+ /** Override: delete operator */
+ void operator delete(void *p, size_t size) {
+ _free(p);
+ }
+
+ /** Override: new[] operator */
+ void * operator new[](size_t size) {
+ return _malloc(size);
+ }
+
+ /** Override: delete[] operator */
+ void operator delete[](void *p, size_t size) {
+ _free(p);
+ }
+private:
+ HashTable<_Key, LinkNode<_Key>*, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * table;
+ LinkNode<_Key> *list;
+ LinkNode<_Key> *tail;
};
#endif
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<typename _Key, int _Shift, typename _KeyInt>
inline unsigned int default_hash_function(_Key hash) {
- return (unsigned int)(((_KeyInt)hash) >> _Shift);
+ return (unsigned int)(((_KeyInt)hash) >> _Shift);
}
template<typename _Key>
inline bool default_equals(_Key key1, _Key key2) {
- return key1 == key2;
+ return key1 == key2;
}
/**
@@ -64,7 +64,7 @@ inline bool default_equals(_Key key1, _Key key2) {
*/
template<typename _Key, typename _Val, typename _KeyInt, int _Shift = 0, void * (* _malloc)(size_t) = snapshot_malloc, void * (* _calloc)(size_t, size_t) = snapshot_calloc, void (*_free)(void *) = snapshot_free, unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = default_equals<_Key> >
class HashTable {
- public:
+public:
/**
* @brief Hash table constructor
* @param initialcapacity Sets the initial capacity of the hash table.
@@ -81,7 +81,7 @@ class HashTable {
capacitymask = initialcapacity - 1;
threshold = (unsigned int)(initialcapacity * loadfactor);
- size = 0; // Initial number of elements in the hash
+ size = 0; // Initial number of elements in the hash
}
/** @brief Hash table destructor */
@@ -121,46 +121,46 @@ class HashTable {
size = 0;
}
- void resetanddelete() {
- for(unsigned int i=0;i<capacity;i++) {
- struct hashlistnode<_Key, _Val> *bin = &table[i];
- if (bin->key != NULL) {
- bin->key = NULL;
- if (bin->val != NULL) {
- delete bin->val;
- bin->val = NULL;
- }
- }
- }
- if (zero) {
- if (zero->val != NULL)
- delete zero->val;
- _free(zero);
- zero = NULL;
- }
- size = 0;
- }
-
- void resetandfree() {
- for(unsigned int i=0;i<capacity;i++) {
- struct hashlistnode<_Key, _Val> *bin = &table[i];
- if (bin->key != NULL) {
- bin->key = NULL;
- if (bin->val != NULL) {
- _free(bin->val);
- bin->val = NULL;
- }
- }
- }
- if (zero) {
- if (zero->val != NULL)
- _free(zero->val);
- _free(zero);
- zero = NULL;
- }
- size = 0;
- }
-
+ void resetanddelete() {
+ for(unsigned int i=0;i<capacity;i++) {
+ struct hashlistnode<_Key, _Val> *bin = &table[i];
+ if (bin->key != NULL) {
+ bin->key = NULL;
+ if (bin->val != NULL) {
+ delete bin->val;
+ bin->val = NULL;
+ }
+ }
+ }
+ if (zero) {
+ if (zero->val != NULL)
+ delete zero->val;
+ _free(zero);
+ zero = NULL;
+ }
+ size = 0;
+ }
+
+ void resetandfree() {
+ for(unsigned int i=0;i<capacity;i++) {
+ struct hashlistnode<_Key, _Val> *bin = &table[i];
+ if (bin->key != NULL) {
+ bin->key = NULL;
+ if (bin->val != NULL) {
+ _free(bin->val);
+ bin->val = NULL;
+ }
+ }
+ }
+ if (zero) {
+ if (zero->val != NULL)
+ _free(zero->val);
+ _free(zero);
+ zero = NULL;
+ }
+ size = 0;
+ }
+
/**
* @brief Put a key/value pair into the table
* @param key The key for the new value; must not be 0 or NULL
@@ -182,7 +182,7 @@ class HashTable {
resize(capacity << 1);
struct hashlistnode<_Key, _Val> *search;
-
+
unsigned int index = hash_function(key);
do {
index &= capacitymask;
@@ -227,8 +227,8 @@ class HashTable {
if (!search->val)
break;
} else
- if (equals(search->key, key))
- return search->val;
+ if (equals(search->key, key))
+ return search->val;
index++;
index &= capacitymask;
if (index==oindex)
@@ -258,7 +258,7 @@ class HashTable {
}
}
-
+
unsigned int index = hash_function(key);
do {
index &= capacitymask;
@@ -267,23 +267,23 @@ class HashTable {
if (!search->val)
break;
} else
- if (equals(search->key, key)) {
- _Val v=search->val;
- //empty out this bin
- search->val=(_Val) 1;
- search->key=0;
- size--;
- return v;
- }
+ if (equals(search->key, key)) {
+ _Val v=search->val;
+ //empty out this bin
+ search->val=(_Val) 1;
+ search->key=0;
+ size--;
+ return v;
+ }
index++;
} while (true);
return (_Val)0;
}
- unsigned int getSize() const {
+ unsigned int getSize() const {
return size;
}
-
+
/**
* @brief Check whether the table contains a value for the given key
@@ -306,8 +306,8 @@ class HashTable {
if (!search->val)
break;
} else
- if (equals(search->key, key))
- return true;
+ if (equals(search->key, key))
+ return true;
index++;
} while (true);
return false;
@@ -327,7 +327,7 @@ class HashTable {
exit(EXIT_FAILURE);
}
- table = newtable; // Update the global hashtable upon resize()
+ table = newtable; // Update the global hashtable upon resize()
capacity = newsize;
capacitymask = newsize - 1;
@@ -335,7 +335,7 @@ class HashTable {
struct hashlistnode<_Key, _Val> *bin = &oldtable[0];
struct hashlistnode<_Key, _Val> *lastbin = &oldtable[oldcapacity];
- for (; bin < lastbin; bin++) {
+ for (;bin < lastbin;bin++) {
_Key key = bin->key;
struct hashlistnode<_Key, _Val> *search;
@@ -353,18 +353,18 @@ class HashTable {
search->val = bin->val;
}
- _free(oldtable); // Free the memory of the old hash table
+ _free(oldtable); // Free the memory of the old hash table
}
- double getLoadFactor() {return loadfactor;}
- unsigned int getCapacity() {return capacity;}
- struct hashlistnode<_Key, _Val> *table;
- struct hashlistnode<_Key, _Val> *zero;
- unsigned int capacity;
+ double getLoadFactor() {return loadfactor;}
+ unsigned int getCapacity() {return capacity;}
+ struct hashlistnode<_Key, _Val> *table;
+ struct hashlistnode<_Key, _Val> *zero;
+ unsigned int capacity;
unsigned int size;
- private:
+private:
unsigned int capacitymask;
unsigned int threshold;
- double loadfactor;
+ double loadfactor;
};
-#endif /* __HASHTABLE_H__ */
+#endif/* __HASHTABLE_H__ */
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 <fcntl.h>
IncrementalSolver::IncrementalSolver() :
- buffer((int *)model_malloc(sizeof(int)*IS_BUFFERSIZE)),
- solution(NULL),
- solutionsize(0),
- offset(0)
+ buffer((int *)model_malloc(sizeof(int)*IS_BUFFERSIZE)),
+ solution(NULL),
+ solutionsize(0),
+ offset(0)
{
- createSolver();
+ createSolver();
}
IncrementalSolver::~IncrementalSolver() {
- killSolver();
- model_free(buffer);
+ killSolver();
+ model_free(buffer);
if (solution != NULL)
model_free(solution);
}
void IncrementalSolver::reset() {
- killSolver();
- offset = 0;
- createSolver();
+ killSolver();
+ offset = 0;
+ createSolver();
}
void IncrementalSolver::addClauseLiteral(int literal) {
- buffer[offset++]=literal;
- if (offset==IS_BUFFERSIZE) {
- flushBuffer();
- }
+ buffer[offset++]=literal;
+ if (offset==IS_BUFFERSIZE) {
+ flushBuffer();
+ }
}
void IncrementalSolver::finishedClauses() {
- addClauseLiteral(0);
+ addClauseLiteral(0);
}
void IncrementalSolver::freeze(int variable) {
- addClauseLiteral(IS_FREEZE);
- addClauseLiteral(variable);
+ addClauseLiteral(IS_FREEZE);
+ addClauseLiteral(variable);
}
int IncrementalSolver::solve() {
- //add an empty clause
+ //add an empty clause
startSolve();
return getSolution();
}
-
+
void IncrementalSolver::startSolve() {
addClauseLiteral(IS_RUNSOLVER);
- flushBuffer();
+ flushBuffer();
}
int IncrementalSolver::getSolution() {
int result=readIntSolver();
- if (result == IS_SAT) {
- int numVars=readIntSolver();
- if (numVars > solutionsize) {
- if (solution != NULL)
- model_free(solution);
- solution = (int *) model_malloc((numVars+1)*sizeof(int));
+ if (result == IS_SAT) {
+ int numVars=readIntSolver();
+ if (numVars > solutionsize) {
+ if (solution != NULL)
+ model_free(solution);
+ solution = (int *) model_malloc((numVars+1)*sizeof(int));
solution[0] = 0;
- }
- readSolver(&solution[1], numVars * sizeof(int));
- }
- return result;
+ }
+ readSolver(&solution[1], numVars * sizeof(int));
+ }
+ return result;
}
int IncrementalSolver::readIntSolver() {
- int value;
- readSolver(&value, 4);
- return value;
+ int value;
+ readSolver(&value, 4);
+ return value;
}
void IncrementalSolver::readSolver(void * tmp, ssize_t size) {
- char *result = (char *) tmp;
- ssize_t bytestoread=size;
- ssize_t bytesread=0;
- do {
- ssize_t n=read(from_solver_fd, &((char *)result)[bytesread], bytestoread);
- if (n == -1) {
- model_print("Read failure\n");
- exit(-1);
- }
- bytestoread -= n;
- bytesread += n;
- } while(bytestoread != 0);
+ char *result = (char *) tmp;
+ ssize_t bytestoread=size;
+ ssize_t bytesread=0;
+ do {
+ ssize_t n=read(from_solver_fd, &((char *)result)[bytesread], bytestoread);
+ if (n == -1) {
+ model_print("Read failure\n");
+ exit(-1);
+ }
+ bytestoread -= n;
+ bytesread += n;
+ } while(bytestoread != 0);
}
bool IncrementalSolver::getValue(int variable) {
- return solution[variable];
+ return solution[variable];
}
void IncrementalSolver::createSolver() {
- int to_pipe[2];
- int from_pipe[2];
- if (pipe(to_pipe) || pipe(from_pipe)) {
- model_print("Error creating pipe.\n");
- exit(-1);
- }
- if ((solver_pid = fork()) == -1) {
- model_print("Error forking.\n");
- exit(-1);
- }
- if (solver_pid == 0) {
- //Solver process
- close(to_pipe[1]);
- close(from_pipe[0]);
+ int to_pipe[2];
+ int from_pipe[2];
+ if (pipe(to_pipe) || pipe(from_pipe)) {
+ model_print("Error creating pipe.\n");
+ exit(-1);
+ }
+ if ((solver_pid = fork()) == -1) {
+ model_print("Error forking.\n");
+ exit(-1);
+ }
+ if (solver_pid == 0) {
+ //Solver process
+ close(to_pipe[1]);
+ close(from_pipe[0]);
int fd=open("log_file", O_WRONLY|O_CREAT|O_TRUNC, S_IRWXU);
-
- if ((dup2(to_pipe[0], 0) == -1) ||
- (dup2(from_pipe[1], IS_OUT_FD) == -1) ||
+
+ if ((dup2(to_pipe[0], 0) == -1) ||
+ (dup2(from_pipe[1], IS_OUT_FD) == -1) ||
(dup2(fd, 1) == -1)) {
- model_print("Error duplicating pipes\n");
- }
+ model_print("Error duplicating pipes\n");
+ }
// setsid();
- execlp(SATSOLVER, SATSOLVER, NULL);
- model_print("execlp Failed\n");
+ execlp(SATSOLVER, SATSOLVER, NULL);
+ model_print("execlp Failed\n");
close(fd);
- } else {
- //Our process
- to_solver_fd = to_pipe[1];
- from_solver_fd = from_pipe[0];
- close(to_pipe[0]);
- close(from_pipe[1]);
- }
+ } else {
+ //Our process
+ to_solver_fd = to_pipe[1];
+ from_solver_fd = from_pipe[0];
+ close(to_pipe[0]);
+ close(from_pipe[1]);
+ }
}
void IncrementalSolver::killSolver() {
- close(to_solver_fd);
- close(from_solver_fd);
- //Stop the solver
- if (solver_pid > 0) {
+ close(to_solver_fd);
+ close(from_solver_fd);
+ //Stop the solver
+ if (solver_pid > 0) {
int status;
- kill(solver_pid, SIGKILL);
+ kill(solver_pid, SIGKILL);
waitpid(solver_pid, &status, 0);
}
}
void IncrementalSolver::flushBuffer() {
- ssize_t bytestowrite=sizeof(int)*offset;
- ssize_t byteswritten=0;
- do {
- ssize_t n=write(to_solver_fd, &((char *)buffer)[byteswritten], bytestowrite);
- if (n == -1) {
- perror("Write failure\n");
- model_print("to_solver_fd=%d\n",to_solver_fd);
- exit(-1);
- }
- bytestowrite -= n;
- byteswritten += n;
- } while(bytestowrite != 0);
- offset = 0;
+ ssize_t bytestowrite=sizeof(int)*offset;
+ ssize_t byteswritten=0;
+ do {
+ ssize_t n=write(to_solver_fd, &((char *)buffer)[byteswritten], bytestowrite);
+ if (n == -1) {
+ perror("Write failure\n");
+ model_print("to_solver_fd=%d\n",to_solver_fd);
+ exit(-1);
+ }
+ bytestowrite -= n;
+ byteswritten += n;
+ } while(bytestowrite != 0);
+ offset = 0;
}
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<SnapList<EPValue *> *>();
#endif
@@ -217,7 +217,7 @@ uint64_t MCExecution::rmw(enum atomicop op, void *addr, uint len, uint64_t currv
model_print("\n");
}
- int num_mcids=(op==ADD)?1:2;
+ int num_mcids=(op==ADD) ? 1 : 2;
EPRecord * record=getOrCreateCurrRecord(RMW, NULL, id_addr_offset, VC_RMWOUTINDEX-VC_RFINDEX, len, false);
record->setRMW(op);
@@ -307,7 +307,7 @@ bool MCExecution::isEmptyStoreBuffer(thread_id_t tid) {
SnapList<EPValue *> * list=(*storebuffer)[id_to_int(tid)];
return list->empty();
}
-
+
void MCExecution::doStore(thread_id_t tid) {
SnapList<EPValue *> * list=(*storebuffer)[id_to_int(tid)];
EPValue * epval=list->front();
@@ -326,7 +326,7 @@ void MCExecution::doStore(EPValue *epval) {
model_print("flushing %d bytes *(%p) = %lu", len, addr, val);
currexecpoint->print();
model_print("\n");
- }
+ }
switch(len) {
case 1:
(*(uint8_t *)addr) = (uint8_t)val;
@@ -358,11 +358,11 @@ void MCExecution::fence() {
#endif
/** @brief EPValue is the corresponding epvalue object.
- For loads rf is the store we read from.
- For loads or stores, addr is the MCID for the provided address.
- numids is the number of MCID's we take in.
- We then list that number of MCIDs for everything we depend on.
-*/
+ For loads rf is the store we read from.
+ For loads or stores, addr is the MCID for the provided address.
+ numids is the number of MCID's we take in.
+ We then list that number of MCIDs for everything we depend on.
+ */
void MCExecution::recordContext(EPValue * epv, MCID rf, MCID addr, int numids, MCID *mcids) {
EPRecord *currrecord=epv->getRecord();
@@ -403,7 +403,7 @@ void MCExecution::store(void *addr, uint64_t val, int len) {
break;
}
#endif
-
+
if (DBG_ENABLED()) {
model_print("STORE *%p=%lu ", addr, val);
currexecpoint->print();
@@ -471,7 +471,7 @@ uint64_t MCExecution::load(const void *addr, int len) {
bool found=false;
uint tid=id_to_int(currexecpoint->get_tid());
SnapList<EPValue *> *list=(*storebuffer)[tid];
- for(SnapList<EPValue *>::reverse_iterator it=list->rbegin(); it != list->rend(); it++) {
+ for(SnapList<EPValue *>::reverse_iterator it=list->rbegin();it != list->rend();it++) {
EPValue *epval=*it;
const void *epaddr=epval->getAddr();
if (epaddr == addr) {
@@ -513,7 +513,7 @@ uint64_t MCExecution::load(const void *addr, int len) {
break;
}
#endif
-
+
if (DBG_ENABLED()) {
model_print("%lu(mid=%u)=LOAD %p ", val, id_retval, addr);
currexecpoint->print();
@@ -571,7 +571,7 @@ MCID MCExecution::branchDir(MCID dirid, int direction, int numdirs, bool anyvalu
}
/** @brief Processes a merge with a previous branch. mcid gives the
- branch we merged. */
+ branch we merged. */
void MCExecution::merge(MCID mcid) {
EPValue * epvalue=getEPValue(mcid);
@@ -583,7 +583,7 @@ void MCExecution::merge(MCID mcid) {
for(int i=0;i<curr_length-orig_length;i++)
currexecpoint->pop();
//increment top
- currexecpoint->incrementTop();
+ currexecpoint->incrementTop();
//now we can create the merge point
if (DBG_ENABLED()) {
model_print("MERGE mid=%u", mcid);
@@ -603,7 +603,7 @@ MCID MCExecution::phi(MCID input) {
MCID mcids[]={input};
recordContext(epvalue, MCID_NODEP, MCID_NODEP, 1, mcids);
-
+
MCID fnmcid=getNextMCID();
ASSERT(EPList->size()==fnmcid);
EPList->push_back(epvalue);
@@ -632,7 +632,7 @@ MCID MCExecution::loop_phi(MCID input) {
*p=rip;
phiset->add(p);
}
-
+
MCID fnmcid=getNextMCID();
ASSERT(EPList->size()==fnmcid);
EPList->push_back(epvalue);
@@ -704,7 +704,7 @@ MCID MCExecution::function(uint functionidentifier, int len, uint64_t val, uint
val=val&getmask(len);
EPValue * epvalue=getEPValue(record, NULL, NULL, val, len);
recordContext(epvalue, MCID_NODEP, MCID_NODEP, numids, mcids);
-
+
uint64_t valarray[numids+VC_BASEINDEX];
for(uint i=0;i<VC_BASEINDEX;i++) {
valarray[i]=0;
@@ -744,7 +744,7 @@ MCID MCExecution::function(uint functionidentifier, int len, uint64_t val, uint
delete rit;
}
}
-
+
return fnmcid;
}
@@ -785,8 +785,8 @@ void MCExecution::set_current_thread(Thread *t) {
(*CurrBranchList)[oldtid]=currbranch;
}
curr_thread=t;
- currexecpoint=(t==NULL)?NULL:(*ExecPointList)[id_to_int(t->get_id())];
- currbranch=(t==NULL)?NULL:(*CurrBranchList)[id_to_int(t->get_id())];
+ currexecpoint=(t==NULL) ? NULL : (*ExecPointList)[id_to_int(t->get_id())];
+ currbranch=(t==NULL) ? NULL : (*CurrBranchList)[id_to_int(t->get_id())];
}
void MCExecution::threadStart(EPRecord *parent) {
@@ -827,7 +827,7 @@ void MCExecution::threadJoin(Thread *blocking) {
void MCExecution::threadFinish() {
Thread *th = get_current_thread();
/* Wake up any joining threads */
- for (unsigned int i = 0; i < get_num_threads(); i++) {
+ for (unsigned int i = 0;i < get_num_threads();i++) {
Thread *waiting = get_thread(int_to_id(i));
if (waiting->waiting_on() == th) {
waiting->set_waiting(NULL);
@@ -870,14 +870,14 @@ void * MCExecution::alloc(size_t size) {
void MCExecution::enterLoop() {
EPRecord * record=getOrCreateCurrRecord(LOOPENTER, NULL, 0, 0, 8, false);
-
+
//push the loop iteration counter
currexecpoint->push(EP_LOOP,0);
//push the curr iteration statement counter
currexecpoint->push(EP_COUNTER,0);
EPRecord * lpstartrecord=getOrCreateCurrRecord(LOOPSTART, NULL, 0, 0, 8, false);
record->setChildRecord(lpstartrecord);
-
+
currexecpoint->incrementTop();
if (DBG_ENABLED()) {
model_print("ENLOOP ");
@@ -894,7 +894,7 @@ void MCExecution::exitLoop() {
/* Record last statement */
uint tid=id_to_int(currexecpoint->get_tid());
-
+
if (!currexecpoint->directInLoop()) {
breakstate=getOrCreateCurrRecord(NONLOCALTRANS, NULL, 0, 0, 8, false);
currexecpoint->incrementTop();
@@ -902,10 +902,10 @@ void MCExecution::exitLoop() {
breakstate=getOrCreateCurrRecord(LOOPEXIT, NULL, 0, 0, 8, false);
currexecpoint->incrementTop();
}
-
+
/* Get Last Record */
- EPRecord *lastrecord=(currbranch==NULL)?(*alwaysexecuted)[tid]:currbranch->lastrecord;
-
+ EPRecord *lastrecord=(currbranch==NULL) ? (*alwaysexecuted)[tid] : currbranch->lastrecord;
+
/* Remember last record as loop exit for this execution. */
if (lastloopexit->size()<=tid) {
lastloopexit->resize(tid+1);
@@ -991,17 +991,17 @@ void MCExecution::addRecordDepTable(EPRecord *record, EPRecord *deprecord, unsig
struct RecordIntPair pair={deprecord, index};
if (!set->contains(&pair)) {
- struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));
+ struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));
*p=pair;
set->add(p);
}
if (!revrecorddep->contains(&pair)) {
- struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));
+ struct RecordIntPair *p=(struct RecordIntPair *)model_malloc(sizeof(struct RecordIntPair));
*p=pair;
revrecorddep->put(p, new ModelVector<EPRecord *>());
}
-
+
ModelVector<EPRecord *> * recvec=revrecorddep->get(&pair);
for(uint i=0;i<recvec->size();i++) {
if ((*recvec)[i]==record)
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<struct RecordIntPair *, uintptr_t, 0, model_malloc, model_calloc, model_free, RP_hash_function, RP_equals> EPRecordSet;
typedef HSIterator<struct RecordIntPair *, uintptr_t, 0, model_malloc, model_calloc, model_free, RP_hash_function, RP_equals> EPRecordIterator;
@@ -45,12 +45,12 @@ struct MCExecution_snapshot {
MCExecution_snapshot();
~MCExecution_snapshot();
unsigned int next_thread_id;
-
+
SNAPSHOTALLOC;
};
class MCExecution {
- public:
+public:
MCExecution();
~MCExecution();
EPRecord * getOrCreateCurrRecord(EventType et, bool * isNew, uintptr_t offset, unsigned int numinputs, uint len, bool br_anyvalue);
@@ -60,7 +60,7 @@ class MCExecution {
MCID nextRMW(MCID addr, uintptr_t offset, MCID oldval, MCID valarg);
void store(void *addr, uint64_t val, int len);
uint64_t load(const void *addr, int len);
- uint64_t rmw(enum atomicop op, void *addr, uint size, uint64_t currval, uint64_t oldval, uint64_t valarg);
+ uint64_t rmw(enum atomicop op, void *addr, uint size, uint64_t currval, uint64_t oldval, uint64_t valarg);
void reset();
MCID branchDir(MCID dir, int direction, int numdirs, bool anyvalue);
void merge(MCID mcid);
@@ -117,9 +117,9 @@ class MCExecution {
void evalGoal(EPRecord *record, CGoal *goal);
void dumpExecution();
EPRecord * getRecord(ExecPoint * ep) {return EPTable->get(ep);}
-
+
MEMALLOC;
- private:
+private:
EPHashTable * EPTable;
EPValueHashTable * EPValueTable;
MemHashTable *memtable;
@@ -135,7 +135,7 @@ class MCExecution {
ExecPoint * currexecpoint;
MCScheduler * scheduler;
Planner * planner;
- struct MCExecution_snapshot * const snap_fields;
+ struct MCExecution_snapshot * const snap_fields;
Thread * curr_thread;
EPValue *currbranch;
EPRecordDepHashTable *eprecorddep;
@@ -145,7 +145,7 @@ class MCExecution {
ModelVector<EPRecord *> * joinvec;
ModelVector<CGoalSet *> * sharedgoals;
ModelVector<RecordSet *> * sharedfuncrecords;
-
+
MCID currid;
MCID id_addr;
MCID id_oldvalue;
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;i<execution->get_num_threads();i++,tid=(tid+1)%execution->get_num_threads()) {
//don't try to schedule finished threads
if (execution->get_thread(int_to_id(tid))->is_complete())
@@ -152,7 +152,7 @@ void MCScheduler::reset() {
}
}
#endif
-
+
Thread *next_thread=execution->get_thread(int_to_id(tid));
if (next_thread->is_complete())
next_thread=NULL;
@@ -185,7 +185,7 @@ bool MCScheduler::checkSet(unsigned int tid, ModelVector<ModelVector<WaitPair* >
CompareResult compare=stoppoint->compare(current);
if (compare==CR_EQUALS) {
//hit stop point
- ExecPoint *waitpoint=nextwp->getWait();
+ ExecPoint *waitpoint=nextwp->getWait();
thread_id_t waittid=waitpoint->get_tid();
ExecPoint *waitthread=execution->get_execpoint(waittid);
CompareResult comparewt=waitthread->compare(waitpoint);
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 T>
class ModelAlloc {
- public:
+public:
// type definitions
- typedef T value_type;
+ typedef T value_type;
typedef T* pointer;
typedef const T* const_pointer;
typedef T& reference;
typedef const T& const_reference;
- typedef size_t size_type;
- typedef size_t difference_type;
+ typedef size_t size_type;
+ typedef size_t difference_type;
// rebind allocator to type U
template <class U>
@@ -153,14 +153,14 @@ class ModelAlloc {
/** Return that all specializations of this allocator are interchangeable. */
template <class T1, class T2>
bool operator ==(const ModelAlloc<T1>&,
- const ModelAlloc<T2>&) throw() {
+ const ModelAlloc<T2>&) throw() {
return true;
}
/** Return that all specializations of this allocator are interchangeable. */
template <class T1, class T2>
bool operator!= (const ModelAlloc<T1>&,
- const ModelAlloc<T2>&) throw() {
+ const ModelAlloc<T2>&) throw() {
return false;
}
@@ -176,15 +176,15 @@ bool operator!= (const ModelAlloc<T1>&,
*/
template <class T>
class SnapshotAlloc {
- public:
+public:
// type definitions
- typedef T value_type;
+ typedef T value_type;
typedef T* pointer;
typedef const T* const_pointer;
typedef T& reference;
typedef const T& const_reference;
- typedef size_t size_type;
- typedef size_t difference_type;
+ typedef size_t size_type;
+ typedef size_t difference_type;
// rebind allocator to type U
template <class U>
@@ -245,44 +245,44 @@ class SnapshotAlloc {
/** Return that all specializations of this allocator are interchangeable. */
template <class T1, class T2>
bool operator ==(const SnapshotAlloc<T1>&,
- const SnapshotAlloc<T2>&) throw() {
+ const SnapshotAlloc<T2>&) throw() {
return true;
}
/** Return that all specializations of this allocator are interchangeable. */
template <class T1, class T2>
bool operator!= (const SnapshotAlloc<T1>&,
- const SnapshotAlloc<T2>&) throw() {
+ const SnapshotAlloc<T2>&) throw() {
return false;
}
#ifdef __cplusplus
extern "C" {
#endif
- typedef void * mspace;
- extern void * mspace_malloc(mspace msp, size_t bytes);
- extern void mspace_free(mspace msp, void* mem);
- extern void * mspace_realloc(mspace msp, void* mem, size_t newsize);
- extern void * mspace_calloc(mspace msp, size_t n_elements, size_t elem_size);
- extern mspace create_mspace_with_base(void* base, size_t capacity, int locked);
- extern mspace create_mspace(size_t capacity, int locked);
-
- struct snapshot_heap_data {
- void *allocation_ptr;
- void *top_ptr;
- };
+typedef void * mspace;
+extern void * mspace_malloc(mspace msp, size_t bytes);
+extern void mspace_free(mspace msp, void* mem);
+extern void * mspace_realloc(mspace msp, void* mem, size_t newsize);
+extern void * mspace_calloc(mspace msp, size_t n_elements, size_t elem_size);
+extern mspace create_mspace_with_base(void* base, size_t capacity, int locked);
+extern mspace create_mspace(size_t capacity, int locked);
+
+struct snapshot_heap_data {
+ void *allocation_ptr;
+ void *top_ptr;
+};
- extern struct snapshot_heap_data * snapshot_struct;
+extern struct snapshot_heap_data * snapshot_struct;
#if USE_MPROTECT_SNAPSHOT
- extern void * user_snapshot_space;
- extern mspace thread_snapshot_space;
+extern void * user_snapshot_space;
+extern mspace thread_snapshot_space;
#endif
- extern mspace model_snapshot_space;
+extern mspace model_snapshot_space;
#ifdef __cplusplus
-}; /* end of extern "C" */
+}; /* end of extern "C" */
#endif
-#endif /* _MY_MEMORY_H */
+#endif/* _MY_MEMORY_H */
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 HSIterator<MCChange *, intptr_t, 0, model_malloc, model_calloc, model_fr
enum PlanResult {NOSCHEDULE, SCHEDULED};
class Planner {
- public:
+public:
Planner(MCExecution * e);
~Planner();
bool is_finished();
@@ -35,7 +35,7 @@ class Planner {
bool checkConstGraph(EPRecord *record, uint64_t val);
void registerValue(EPRecord *record, uint64_t val, unsigned int index);
ConstGen * getConstGen() {return cgen;}
-
+
MEMALLOC;
private:
diff --git a/schedulebuilder.cc b/schedulebuilder.cc
index cc17b1e..9e7d3de 100644
--- a/schedulebuilder.cc
+++ b/schedulebuilder.cc
@@ -33,20 +33,20 @@ void neatPrint(EPRecord *r, ConstGen *cgen, bool *satsolution) {
model_print("address=%p ", sls->getAddressEncoding(cgen, r, satsolution));
model_print("rd=%lu ", sls->getValueEncoding(cgen, r, satsolution));
}
- break;
+ break;
case STORE: {
StoreLoadSet * sls=cgen->getStoreLoadSet(r);
model_print("address=%p ", sls->getAddressEncoding(cgen, r, satsolution));
model_print("wr=%lu ", sls->getValueEncoding(cgen, r, satsolution));
}
- break;
+ break;
case RMW: {
StoreLoadSet * sls=cgen->getStoreLoadSet(r);
model_print("address=%p ", sls->getAddressEncoding(cgen, r, satsolution));
model_print("rd=%lu ", sls->getRMWRValueEncoding(cgen, r, satsolution));
model_print("wr=%lu ", sls->getValueEncoding(cgen, r, satsolution));
}
- break;
+ break;
default:
;
}
@@ -69,7 +69,7 @@ void ScheduleBuilder::buildSchedule(bool * satsolution) {
EPRecord *next=processRecord(record, satsolution);
#ifdef TSO
if (next != NULL) {
-
+
if (next->getType()==STORE) {
stores[index]->push_back(next);
next=getNextRecord(next);
@@ -92,7 +92,7 @@ void ScheduleBuilder::buildSchedule(bool * satsolution) {
EPRecord *earliest=NULL;
for(uint index=0;index<threads.size();index++) {
EPRecord *record=threads[index];
-
+
if (record!=NULL && (earliest==NULL ||
cg->getOrder(record, earliest, satsolution))) {
earliest=record;
@@ -151,7 +151,7 @@ EPRecord * ScheduleBuilder::getNextRecord(EPRecord *record) {
if (!br->hasNextRecord())
next=NULL;
}
-
+
if (next==NULL && record->getBranch()!=NULL) {
EPValue * epbr=record->getBranch();
EPRecord *branch=epbr->getRecord();
@@ -192,7 +192,7 @@ EPRecord * ScheduleBuilder::processRecord(EPRecord *record, bool *satsolution) {
case MERGE:
case ALLOC:
case EQUALS:
- case FUNCTION:
+ case FUNCTION:
/* Continue executing */
break;
case THREADCREATE:
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<struct snapshot_entry> stack;
};
@@ -164,7 +164,7 @@ static void SnapshotGlobalSegments()
int SnapshotStack::backTrackBeforeStep(int seqindex)
{
int i;
- for (i = (int)stack.size() - 1; i >= 0; i++)
+ for (i = (int)stack.size() - 1;i >= 0;i++)
if (stack[i].index <= seqindex)
break;
else
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<typename _Tp>
class ModelList : public std::list<_Tp, ModelAlloc<_Tp> >
{
- public:
+public:
typedef std::list< _Tp, ModelAlloc<_Tp> > list;
ModelList() :
@@ -28,13 +28,13 @@ class ModelList : public std::list<_Tp, ModelAlloc<_Tp> >
list(n, val)
{ }
- MEMALLOC;
+ MEMALLOC;
};
template<typename _Tp>
class SnapList : public std::list<_Tp, SnapshotAlloc<_Tp> >
{
- public:
+public:
typedef std::list<_Tp, SnapshotAlloc<_Tp> > list;
SnapList() :
@@ -51,7 +51,7 @@ class SnapList : public std::list<_Tp, SnapshotAlloc<_Tp> >
template<typename _Tp>
class ModelVector : public std::vector<_Tp, ModelAlloc<_Tp> >
{
- public:
+public:
typedef std::vector< _Tp, ModelAlloc<_Tp> > vector;
ModelVector() :
@@ -62,13 +62,13 @@ class ModelVector : public std::vector<_Tp, ModelAlloc<_Tp> >
vector(n, val)
{ }
- MEMALLOC;
+ MEMALLOC;
};
template<typename _Tp>
class SnapVector : public std::vector<_Tp, SnapshotAlloc<_Tp> >
{
- public:
+public:
typedef std::vector< _Tp, SnapshotAlloc<_Tp> > vector;
SnapVector() :
@@ -82,4 +82,4 @@ class SnapVector : public std::vector<_Tp, SnapshotAlloc<_Tp> >
SNAPSHOTALLOC;
};
-#endif /* __STL_MODEL_H__ */
+#endif/* __STL_MODEL_H__ */
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;
};