13 typedef struct MethodCall {
14 string interfaceName; // The interface label name
15 void *value; // The pointer that points to the struct that have the return
16 // value and the arguments
17 void *localState; // The pointer that points to the struct that represents
19 set<MethodCall*> *prev; // Method calls that are hb right before me
20 set<MethodCall*> *next; // Method calls that are hb right after me
21 set<MethodCall*> *concurrent; // Method calls that are concurrent with me
24 typedef MethodCall *Method;
25 typedef set<Method> *MethodSet;
27 typedef vector<int> IntVector;
28 typedef list<int> IntList;
29 typedef set<int> IntSet;
31 /********** More general specification-related types and operations **********/
33 #define NewSet new set<Method>
35 #define CAT(a, b) CAT_HELPER(a, b) /* Concatenate two symbols for macros! */
36 #define CAT_HELPER(a, b) a ## b
37 #define X(name) CAT(__##name, __LINE__) /* unique variable */
40 The set here is a vector<MethodCall*>* type, or the MethodSet type. And the
41 item would become the MethodCall* type, or the Method type
43 #define ForEach1(item, set) \
45 for (Method item = (set)->size() > 0 ? (*(set))[0] : NULL; \
46 X(i) < (set)->size(); X(i)++, item = X(i) < (set)->size() ? (*(set))[X(i)] : NULL)
48 #define ForEach(item, container) \
49 auto X(_container) = (container); \
50 auto X(iter) = X(_container)->begin(); \
51 for (auto item = *X(iter); X(iter) != X(_container)->end(); item = ((++X(iter)) != \
52 X(_container)->end()) ? *X(iter) : 0)
55 The subset operation is only for the MethodCall set
62 #define LOCAL(field) Local(_M, field)
64 #define VALUE(type, field) Value(_M, type, field)
66 #define Subset(s, subset, condition) \
67 MethodSet original = s; \
68 MethodSet subset = NewSet; \
69 ForEach (_M, original) { \
74 /** General for set, list & vector */
75 #define Size(container) ((container)->size())
77 #define _BelongHelper(type) \
79 inline bool Belong(type<T> *container, T item) { \
80 return std::find(container->begin(), \
81 container->end(), item) != container->end(); \
88 /** General set operations */
90 inline set<T>* Intersect(set<T> *set1, set<T> *set2) {
91 set<T> *res = new set<T>;
92 ForEach (item, set1) {
93 if (Belong(set2, item))
100 inline set<T>* Union(set<T> *s1, set<T> *s2) {
101 set<T> *res = new set<T>(*s1);
108 inline set<T>* Subtract(set<T> *set1, set<T> *set2) {
109 set<T> *res = new set<T>;
110 ForEach (item, set1) {
111 if (!Belong(set2, item))
118 inline void Insert(set<T> *s, T item) { s->insert(item); }
121 inline void Insert(set<T> *s, set<T> *others) {
122 ForEach (item, others)
126 inline MethodSet MakeSet(int count, ...) {
130 va_start (ap, count);
132 for (int i = 0; i < count; i++) {
133 Method item = va_arg (ap, Method);
140 /********** Method call related operations **********/
141 #define Name(method) method->interfaceName
143 #define Local(method, field) ((StateStruct*) method->localState)->field
145 #define Value(method, type, field) ((type*) method->value)->field
147 #define Prev(method) method->prev
148 #define PREV ME->prev
150 #define Next(method) method->next
151 #define NEXT ME->next
153 #define Concurrent(method) method->concurrent
154 #define CONCURRENT ME->concurrent
156 // This auto-generated struct can have different fields according to the read
157 // state declaration. Here it's just a test example
158 typedef struct StateStruct {
162 // These auto-generated struct can have different fields according to the return
163 // value and arguments of the corresponding interface. The struct will have the
164 // same name as the interface name. Here it's just a test example
165 typedef struct Store {
170 typedef struct Load {
176 set<int> *is1 = new set<int>;
177 set<int> *is2 = new set<int>;
179 list<int> *il1 = new list<int>;
180 list<int> *il2 = new list<int>;
192 MethodSet ms = NewSet;
193 Method m = new MethodCall;
194 m->interfaceName = "Store";
195 StateStruct *ss = new StateStruct;
198 Store *st = new Store;
204 m->interfaceName= "Store";
205 ss = new StateStruct;
214 m->interfaceName= "Load";
215 ss = new StateStruct;
223 //Subset(ms, sub, NAME == "Store" && VALUE(Store, val) != 0);
224 Subset(ms, sub, NAME == "Store" && VALUE(Store, val) >= 0 && LOCAL(x) == 0);
226 cout << "Size=" << Size(sub) << endl;