}
if (!alwaysexecuted)
value--;
-
+
return value;
}
#include "classlist.h"
class BranchRecord {
- public:
+public:
BranchRecord(EPRecord *record, uint numvars, Constraint **vars, bool isalwaysexecuted);
~BranchRecord();
Constraint * getAnyBranch();
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
#include <stdint.h>
class CGoal {
- public:
+public:
CGoal(unsigned int num, uint64_t *vals);
~CGoal();
unsigned int getNum() {return num;}
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);
};
#include "eprecord.h"
class MCChange {
- public:
+public:
MCChange(EPRecord *record, uint64_t _val, unsigned int _index);
~MCChange();
EPRecord *getRecord() {return record;}
void print();
MEMALLOC;
- private:
+private:
EPRecord *record;
uint64_t val;
unsigned int index;
/** Performs a read action.*/
uint64_t model_read_action(void * obj, memory_order ord) {
- return -1;
+ return -1;
}
/** Performs a write action.*/
* a write.
*/
uint64_t model_rmwr_action(void *obj, memory_order ord) {
- return -1;
+ return -1;
}
/** Performs the write part of a RMW action. */
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)
#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
{
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 */
model_print("---- END PROGRAM OUTPUT ----\n");
}
-#endif /* ! CONFIG_DEBUG */
+#endif/* ! CONFIG_DEBUG */
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
#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__ */
#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() */
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;
delete storeloadtable->zero->val;
} else
ASSERT(false);
- model_free(storeloadtable -> zero);
+ model_free(storeloadtable->zero);
storeloadtable->zero = NULL;
}
storeloadtable->size = 0;
#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];
delete solver;
solver = NULL;
}
-
+
solver=new IncrementalSolver();
traverse(true);
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];
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()) {
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());
}
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) {
}
/** 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 */
}
}
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();
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);
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))
sri->remove();
}
}
-
+
delete sri;
return srscopy;
}
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();
IntHashSet *addrset=load->getSet(VC_ADDRINDEX);
IntIterator *ait=addrset->iterator();
-
+
while(ait->hasNext()) {
void *addr=(void *)ait->next();
RecordSet *rs=execution->getStoreTable(addr);
}
/** This function merges two recordsets and updates the storeloadtable
- accordingly. */
+ accordingly. */
void ConstGen::mergeSets(StoreLoadSet *to, StoreLoadSet *from) {
RecordIterator * sri=from->iterator();
while (j>0) {
EPRecord *oldrec=(*vector)[--j];
EventType oldrec_t=oldrec->getType();
-
+
if (((oldrec_t == RMW) || (oldrec_t==FENCE)) &&
isAlwaysExecuted(oldrec)) {
return;
#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();
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);
Constraint *intratransorder=new Constraint(OR, c21, c13);
#endif
ADDCONSTRAINT(intratransorder,"intratransorder");
- }
+ }
for(uint t0i=0;t0i<t1i;t0i++) {
EPRecord *t0rec=(*t1vec)[t0i];
Constraint *intratransorder=new Constraint(OR, c21, c02);
#endif
ADDCONSTRAINT(intratransorder,"intratransorder");
- }
+ }
}
}
}
void ConstGen::printConstraint(uint value) {
solver->addClauseLiteral(value);
}
-
+
bool * ConstGen::runSolver() {
int solution=solver->solve();
if (solution == IS_UNSAT) {
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;
}
}
/** 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()) {
RecordIterator *sri=srs->iterator();
while(sri->hasNext()) {
EPRecord *rec=sri->next();
-
+
if (!getOrderConstraint(rec, record)->isTrue()) {
delete sri;
return false;
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++;
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++;
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);
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,
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++) {
}
/** 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);
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);
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);
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);
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);
}
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);
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();
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");
}
}
}
/** 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);
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);
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();
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();
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();
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;
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;
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");
}
case FENCE:
processFence(record);
break;
-#endif
+#endif
case RMW:
#ifdef TSO
processFence(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();
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)
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));
}
#endif
class ConstGen {
- public:
+public:
ConstGen(MCExecution *e);
~ConstGen();
bool process();
#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();
#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);
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;
};
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;
{
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;
}
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)
{
model_print(" v ");
}
operands[i]->print();
- }
+ }
model_print(")");
break;
case VAR:
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;
}
}
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
}
}
}
case AND: {
Constraint *array[numoperandsorvar];
-
+
ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
for(uint j=0;j<c->numoperandsorvar;j++) {
//copy other elements
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:
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);
Constraint *negate();
MEMALLOC;
- private:
+private:
CType type;
uint numoperandsorvar;
Constraint ** operands;
return 0;
}
-#endif /* MAC */
+#endif/* MAC */
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__ */
delete it;
}
-
+
execpoint->print(f);
}
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;
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;}
bool isSharedGoals() {return func_shares_goalset;}
uintptr_t getOffset() {return offset;}
MEMALLOC;
-
- private:
+
+private:
ValueVector * valuevector;
ExecPoint * execpoint;
CGoalSet *completed;
#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;}
EPRecord *firstrecord;
EPRecord *lastrecord;
EPRecord * getRecord() {return record;}
-
+
MEMALLOC;
- private:
+private:
ExecPoint * execpoint;
EPRecord *record;
const void *addr;
#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
}
/** 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]) {
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;
}
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();
void print();
void print(int f);
MEMALLOC;
- private:
+private:
unsigned int length;
unsigned int size;
execcount_t * pairarray;
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);
#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
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
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;
}
/**
*/
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.
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 */
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
resize(capacity << 1);
struct hashlistnode<_Key, _Val> *search;
-
+
unsigned int index = hash_function(key);
do {
index &= capacitymask;
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)
}
}
-
+
unsigned int index = hash_function(key);
do {
index &= capacitymask;
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
if (!search->val)
break;
} else
- if (equals(search->key, key))
- return true;
+ if (equals(search->key, key))
+ return true;
index++;
} while (true);
return false;
exit(EXIT_FAILURE);
}
- table = newtable; // Update the global hashtable upon resize()
+ table = newtable; // Update the global hashtable upon resize()
capacity = newsize;
capacitymask = newsize - 1;
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;
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__ */
#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;
}
#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
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();
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;
//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();
continue;
}
#else
- Constraint * conflictbeforeload=cg->getOrderConstraint(conflictstore, load);
+ Constraint * conflictbeforeload=cg->getOrderConstraint(conflictstore, load);
if (conflictbeforeload->isFalse()) {
storebeforeconflict->freerec();
continue;
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;
#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;
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);
}
{"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;
case 'v':
params->verbose = optarg ? atoi(optarg) : 1;
break;
- default: /* '?' */
+ default: /* '?' */
error = true;
break;
}
* 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();
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
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);
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();
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;
#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();
break;
}
#endif
-
+
if (DBG_ENABLED()) {
model_print("STORE *%p=%lu ", addr, val);
currexecpoint->print();
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) {
break;
}
#endif
-
+
if (DBG_ENABLED()) {
model_print("%lu(mid=%u)=LOAD %p ", val, id_retval, addr);
currexecpoint->print();
}
/** @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);
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);
MCID mcids[]={input};
recordContext(epvalue, MCID_NODEP, MCID_NODEP, 1, mcids);
-
+
MCID fnmcid=getNextMCID();
ASSERT(EPList->size()==fnmcid);
EPList->push_back(epvalue);
*p=rip;
phiset->add(p);
}
-
+
MCID fnmcid=getNextMCID();
ASSERT(EPList->size()==fnmcid);
EPList->push_back(epvalue);
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;
delete rit;
}
}
-
+
return fnmcid;
}
(*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) {
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);
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 ");
/* Record last statement */
uint tid=id_to_int(currexecpoint->get_tid());
-
+
if (!currexecpoint->directInLoop()) {
breakstate=getOrCreateCurrRecord(NONLOCALTRANS, NULL, 0, 0, 8, false);
currexecpoint->incrementTop();
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);
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)
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;
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);
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);
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;
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;
ModelVector<EPRecord *> * joinvec;
ModelVector<CGoalSet *> * sharedgoals;
ModelVector<RecordSet *> * sharedfuncrecords;
-
+
MCID currid;
MCID id_addr;
MCID id_oldvalue;
- 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;
#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())
}
}
#endif
-
+
Thread *next_thread=execution->get_thread(int_to_id(tid));
if (next_thread->is_complete())
next_thread=NULL;
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);
#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; }
void setNewFlag();
MEMALLOC;
- private:
+private:
unsigned int waitsetlen;
ucontext_t system_context;
MCExecution *execution;
}
-#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
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);
#include "params.h"
class MC {
- public:
+public:
MC(struct model_params params);
~MC();
MCExecution * get_execution() const { return execution; }
const model_params params;
MEMALLOC;
- private:
+private:
MCExecution *execution;
void run_execution();
};
extern MC *model;
-#endif /* __MODEL_H__ */
+#endif/* __MODEL_H__ */
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;
}
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)
free(ptr);
}
-#endif /* !USE_MPROTECT_SNAPSHOT */
+#endif/* !USE_MPROTECT_SNAPSHOT */
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; \
}
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; \
}
*/
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>
/** 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;
}
*/
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>
/** 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 */
void redirect_output();
void clear_program_output();
void print_program_output();
-#endif /* ! CONFIG_DEBUG */
+#endif/* ! CONFIG_DEBUG */
-#endif /* __OUTPUT_H__ */
+#endif/* __OUTPUT_H__ */
/** @brief Only explore branches. */
bool branches;
-
+
/** @brief Command-line argument count to pass to user program */
int argc;
char **argv;
};
-#endif /* __PARAMS_H__ */
+#endif/* __PARAMS_H__ */
void Planner::plan() {
DEBUG("Planning\n");
e->get_scheduler()->reset();
-
+
if (!cgen->canReuseEncoding()) {
processChanges();
cgen->reset();
}
/** 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();
}
/** 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()) {
}
/** 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();
/** This function pushes a new store value to all loads that share an
- address. */
+ address. */
void Planner::processNewStoreValue(MCChange *change) {
EPRecord *store=change->getRecord();
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) {
//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()) {
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) {
enum PlanResult {NOSCHEDULE, SCHEDULED};
class Planner {
- public:
+public:
Planner(MCExecution * e);
~Planner();
bool is_finished();
bool checkConstGraph(EPRecord *record, uint64_t val);
void registerValue(EPRecord *record, uint64_t val, unsigned int index);
ConstGen * getConstGen() {return cgen;}
-
+
MEMALLOC;
private:
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:
;
}
EPRecord *next=processRecord(record, satsolution);
#ifdef TSO
if (next != NULL) {
-
+
if (next->getType()==STORE) {
stores[index]->push_back(next);
next=getNextRecord(next);
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;
if (!br->hasNextRecord())
next=NULL;
}
-
+
if (next==NULL && record->getBranch()!=NULL) {
EPValue * epbr=record->getBranch();
EPRecord *branch=epbr->getRecord();
case MERGE:
case ALLOC:
case EQUALS:
- case FUNCTION:
+ case FUNCTION:
/* Continue executing */
break;
case THREADCREATE:
#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;
};
class SnapshotStack {
- public:
+public:
int backTrackBeforeStep(int seq_index);
void snapshotStep(int seq_index);
MEMALLOC;
- private:
+private:
ModelVector<struct snapshot_entry> stack;
};
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
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);
/* 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
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;
};
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);
}
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;
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);
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();
}
}
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");
{
#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;
#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));
}
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
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;
* @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;
}
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();
/* 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);
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 */
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);
// 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 == '+')
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.
print_stacktrace(fileno(out), max_frames);
}
-#endif // __STACKTRACE_H__
+#endif// __STACKTRACE_H__
template<typename _Tp>
class ModelList : public std::list<_Tp, ModelAlloc<_Tp> >
{
- public:
+public:
typedef std::list< _Tp, ModelAlloc<_Tp> > list;
ModelList() :
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() :
template<typename _Tp>
class ModelVector : public std::vector<_Tp, ModelAlloc<_Tp> >
{
- public:
+public:
typedef std::vector< _Tp, ModelAlloc<_Tp> > vector;
ModelVector() :
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() :
SNAPSHOTALLOC;
};
-#endif /* __STL_MODEL_H__ */
+#endif/* __STL_MODEL_H__ */
#include "stl-model.h"
class StoreLoadSet {
- public:
+public:
StoreLoadSet();
~StoreLoadSet();
void add(EPRecord *op);
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;
/** @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();
Thread_free(p);
}
EPRecord * getParentRecord() {return parentrecord;}
- private:
+private:
int create_context();
/** @brief The parent Thread which created this Thread */
return id;
}
-#endif /* __THREADS_MODEL_H__ */
+#endif/* __THREADS_MODEL_H__ */
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));
*/
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;
#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;
};
projects / satcheck.git / commitdiff