1 /* Copyright (c) 2015 Regents of the University of California
3 * Author: Brian Demsky <bdemsky@uci.edu>
5 * This program is free software; you can redistribute it and/or
6 * modify it under the terms of the GNU General Public License
7 * version 2 as published by the Free Software Foundation.
12 #include "classlist.h"
13 #include "stl-model.h"
16 #ifdef VERBOSE_CONSTRAINTS
17 #define ADDCONSTRAINT(cn, str) do {Constraint *c=cn; model_print("%s ",str);c->print();model_print("\n");addConstraint(c);} while(0);
18 #define ADDCONSTRAINT2(cg, cn, str) do {Constraint *c=cn; model_print("%s ",str);c->print();model_print("\n");cg->addConstraint(c);} while(0);
20 #define ADDGOAL(r, cn, str) do {Constraint *c=cn; model_print("%s ",str);c->print();model_print("\n");addGoal(r, c);} while(0);
21 #define ADDBRANCHGOAL(r, cn, str) do {Constraint *c=cn; model_print("%s ",str);c->print();model_print("\n");addBranchGoal(r, c);} while(0);
24 #define ADDCONSTRAINT(cn, store) addConstraint(cn);
25 #define ADDCONSTRAINT2(cg, cn, store) cg->addConstraint(cn);
27 #define ADDGOAL(r, cn, store) addGoal(r, cn);
28 #define ADDBRANCHGOAL(r, cn, store) addBranchGoal(r, cn);
31 unsigned int RecPairHash(RecPair *rp);
32 bool RecPairEquals(RecPair *r1, RecPair *r2);
33 typedef HashTable<RecPair *, RecPair *, uintptr_t, 0, model_malloc, model_calloc, model_free, RecPairHash, RecPairEquals> RecPairTable;
35 typedef HashTable<EPRecord *, uint, uintptr_t, 0, model_malloc, model_calloc, model_free> RecToIntTable;
50 ConstGen(MCExecution *e);
54 bool canReuseEncoding();
55 Constraint * getNewVar();
56 void getArrayNewVars(uint num, Constraint **);
57 RecordSet * computeConflictSet(EPRecord *store, EPRecord *load, RecordSet *baseset);
58 RecordSet * getMayReadFromSet(EPRecord *load);
59 RecordSet * getMayReadFromSetOpt(EPRecord *load);
60 void addConstraint(Constraint *c);
62 StoreLoadSet * getStoreLoadSet(EPRecord *op);
63 Constraint * getOrderConstraint(EPRecord *first, EPRecord *second);
64 Constraint * getExecutionConstraint(EPRecord *record);
65 bool isAlwaysExecuted(EPRecord *record);
66 BranchRecord * getBranchRecord(EPRecord *branch) {return branchtable->get(branch);}
67 bool getOrder(EPRecord *first, EPRecord *second, bool * satsolution);
68 void printConstraint(uint value);
69 void printNegConstraint(uint value);
70 void achievedGoal(EPRecord *record);
77 Constraint * getRetValueEncoding(EPRecord *record, uint64_t value);
78 Constraint * getMemValueEncoding(EPRecord *record, uint64_t value);
79 bool subsumesExecutionConstraint(EPRecord *recordsubsumes, EPRecord *record);
81 void addBranchGoal(EPRecord *, Constraint *c);
82 void addGoal(EPRecord *, Constraint *c);
83 void translateGoals();
85 /** Methods to print execution graph .*/
86 void printEventGraph();
87 void printRecord(EPRecord *record, int file);
88 void doPrint(EPRecord *record, int file);
90 /** Methods to traverse execution graph .*/
91 void traverse(bool initial);
92 void traverseRecord(EPRecord *record, bool initial);
94 /** Methods for initially visit records */
95 void visitRecord(EPRecord *record);
96 void insertAction(EPRecord *record);
97 void insertFunction(EPRecord *record);
98 void insertEquals(EPRecord *record);
99 void insertBranch(EPRecord *record);
100 void insertNonLocal(EPRecord *record);
101 void insertLabel(EPRecord *record);
103 /** Methods for second pass over records */
104 void processRecord(EPRecord *record);
105 void processYield(EPRecord *record);
106 void processFunction(EPRecord *record);
107 void processEquals(EPRecord *record);
108 void processLoopPhi(EPRecord *record);
109 void processPhi(EPRecord *record);
110 void processCAS(EPRecord *record);
111 void processEXC(EPRecord *record);
112 void processAdd(EPRecord *record);
113 void processStore(EPRecord *record);
114 void processBranch(EPRecord *record);
115 void processLoad(EPRecord *record);
116 void processAddresses(EPRecord *record);
117 void recordExecCond(EPRecord *record);
119 /** TSO Specific methods */
121 void genTSOTransOrderConstraints();
122 void insertTSOAction(EPRecord *record);
123 void processFence(EPRecord *record);
126 /** These functions build closed groups of memory operations that
127 can store/load from each other. */
128 void groupMemoryOperations(EPRecord *op);
129 void mergeSets(StoreLoadSet *to, StoreLoadSet *from);
131 bool orderThread(EPRecord *first, EPRecord *second);
132 void createOrderConstraint(EPRecord *r1, EPRecord *r2);
133 void genTransOrderConstraints();
134 void genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVector<EPRecord *> *t2vec, ModelVector<EPRecord *> * t3vec);
135 void genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVector<EPRecord *> *t2vec);
136 void genTransOrderConstraint(EPRecord *t1rec, EPRecord *t2rec, EPRecord *t3rec);
138 /** The hashtable maps an address to the closure set of
139 memory operations that may touch that address. */
140 StoreLoadSetHashTable *storeloadtable;
141 /** This hashtable maps a load to all of the stores it may read
143 LoadHashTable *loadtable;
145 MCExecution *execution;
146 ModelVector<EPRecord *> * workstack;
147 ModelVector<ModelVector<EPRecord *> *> * threadactions;
150 ModelVector<Constraint *> * goalset;
151 Constraint ** goalvararray;
152 ModelVector<Constraint *> * vars;
153 BranchTable * branchtable;
154 FunctionTable *functiontable;
155 EqualsTable *equalstable;
156 ScheduleBuilder *schedulebuilder;
157 RecordSet *nonlocaltrans;
158 LoadHashTable *execcondtable;
159 IncrementalSolver *solver;
160 RecToIntTable *rectoint;
162 ModelVector<struct MC_Stat *> * stats;
166 bool has_untaken_branches;
171 RecPair(EPRecord *r1, EPRecord *r2) :
178 Constraint *constraint;