#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();
void processLoad(EPRecord *record);
void processAddresses(EPRecord *record);
void recordExecCond(EPRecord *record);
-
+ void computeYieldCond(EPRecord *record);
+
/** TSO Specific methods */
#ifdef TSO
void genTSOTransOrderConstraints();
#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;
RecPairTable *rpt;
uint numconstraints;
ModelVector<Constraint *> * goalset;
+ ModelVector<EPRecord *> *yieldlist;
Constraint ** goalvararray;
ModelVector<Constraint *> * vars;
BranchTable * branchtable;
EqualsTable *equalstable;
ScheduleBuilder *schedulebuilder;
RecordSet *nonlocaltrans;
+ RecordSet *incompleteexploredbranch;
LoadHashTable *execcondtable;
IncrementalSolver *solver;
RecToIntTable *rectoint;
+ RecToConsTable *yieldtable;
#ifdef STATS
ModelVector<struct MC_Stat *> * stats;
#endif
};
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;