15 typedef struct MethodCall {
16 string interfaceName; // The interface label name
17 void *value; // The pointer that points to the struct that have the return
18 // value and the arguments
19 void *state; // The pointer that points to the struct that represents
21 set<MethodCall*> *prev; // Method calls that are hb right before me
22 set<MethodCall*> *next; // Method calls that are hb right after me
23 set<MethodCall*> *concurrent; // Method calls that are concurrent with me
26 typedef MethodCall *Method;
27 typedef set<Method> *MethodSet;
29 typedef vector<int> IntVector;
30 typedef list<int> IntList;
31 typedef set<int> IntSet;
33 /********** More general specification-related types and operations **********/
35 #define NewMethodSet new set<Method>
37 #define CAT(a, b) CAT_HELPER(a, b) /* Concatenate two symbols for macros! */
38 #define CAT_HELPER(a, b) a ## b
39 #define X(name) CAT(__##name, __LINE__) /* unique variable */
42 This is a generic ForEach primitive for all the containers that support
43 using iterator to iterate.
45 #define ForEach(item, container) \
46 auto X(_container) = (container); \
47 auto X(iter) = X(_container)->begin(); \
48 for (auto item = *X(iter); X(iter) != X(_container)->end(); item = ((++X(iter)) != \
49 X(_container)->end()) ? *X(iter) : 0)
52 This is a common macro that is used as a constant for the name of specific
53 variables. We basically have two usage scenario:
54 1. In Subset operation, we allow users to specify a condition to extract a
55 subset. In that condition expression, we provide NAME, RET(type), ARG(type,
56 field) and STATE(field) to access each item's (method call) information.
57 2. In general specification (in pre- & post- conditions and side effects),
58 we would automatically generate an assignment that assign the current
59 MethodCall* pointer to a variable namedd _M. With this, when we access the
60 state of the current method, we use STATE(field) (this is a reference
68 #define STATE(field) State(_M, field)
70 #define VALUE(type, field) Value(_M, type, field)
71 #define RET(type) VALUE(type, RET)
72 #define ARG(type, arg) VALUE(type, arg)
75 #define Subset(s, subset, condition) \
76 MethodSet original = s; \
77 MethodSet subset = NewMethodSet; \
78 ForEach (_M, original) { \
86 This operation is specifically for Method set. For example, when we want to
87 construct an integer set from the state field "x" (which is an
88 integer) of the previous set of method calls (PREV), and the new set goes to
89 "readSet", we would call "MakeSet(int, PREV, readSet, STATE(x));". Then users
90 can use the "readSet" as an integer set (set<int>)
92 #define MakeSet(type, oldset, newset, field) \
93 auto newset = new set<type>; \
94 ForEach (_M, oldset) \
95 newset->insert(field); \
98 We provide a more general subset operation that takes a plain boolean
99 expression on each item (access by the name "ITEM") of the set, and put it
100 into a new set if the boolean expression (Guard) on that item holds. This is
101 used as the second arguments of the Subset operation. An example to extract
102 a subset of positive elements on an IntSet "s" would be "Subset(s,
103 GeneralGuard(int, ITEM > 0))"
105 #define GeneralGuard(type, expression) std::function<bool(type)> ( \
106 [](type ITEM) -> bool { return (expression);}) \
109 This is a more specific guard designed for the Method (MethodCall*). It
110 basically wrap around the GeneralGuard with the type Method. An example to
111 extract the subset of method calls in the PREV set whose state "x" is
112 equal to "val" would be "Subset(PREV, Guard(STATE(x) == val))"
114 #define Guard(expression) GeneralGuard(Method, expression)
117 A general subset operation that takes a condition and returns all the item
118 for which the boolean guard holds.
121 inline set<T>* Subset(set<T> *original, std::function<bool(T)> condition) {
122 set<T> *res = new set<T>;
123 ForEach (_M, original) {
131 A general set operation that takes a condition and returns if there exists
132 any item for which the boolean guard holds.
135 inline bool HasItem(set<T> *original, std::function<bool(T)> condition) {
136 ForEach (_M, original) {
146 A general sublist operation that takes a condition and returns all the item
147 for which the boolean guard holds in the same order as in the old list.
150 inline list<T>* Sublist(list<T> *original, std::function<bool(T)> condition) {
151 list<T> *res = new list<T>;
152 ForEach (_M, original) {
160 A general subvector operation that takes a condition and returns all the item
161 for which the boolean guard holds in the same order as in the old vector.
164 inline vector<T>* Subvector(vector<T> *original, std::function<bool(T)> condition) {
165 vector<T> *res = new vector<T>;
166 ForEach (_M, original) {
173 /** General for set, list & vector */
174 #define Size(container) ((container)->size())
176 #define _BelongHelper(type) \
178 inline bool Belong(type<T> *container, T item) { \
179 return std::find(container->begin(), \
180 container->end(), item) != container->end(); \
184 _BelongHelper(vector)
187 /** General set operations */
189 inline set<T>* Intersect(set<T> *set1, set<T> *set2) {
190 set<T> *res = new set<T>;
191 ForEach (item, set1) {
192 if (Belong(set2, item))
199 inline set<T>* Union(set<T> *s1, set<T> *s2) {
200 set<T> *res = new set<T>(*s1);
207 inline set<T>* Subtract(set<T> *set1, set<T> *set2) {
208 set<T> *res = new set<T>;
209 ForEach (item, set1) {
210 if (!Belong(set2, item))
217 inline void Insert(set<T> *s, T item) { s->insert(item); }
220 inline void Insert(set<T> *s, set<T> *others) {
221 ForEach (item, others)
226 inline MethodSet MakeSet(int count, ...) {
230 va_start (ap, count);
232 for (int i = 0; i < count; i++) {
233 Method item = va_arg (ap, Method);
241 /********** Method call related operations **********/
242 #define Name(method) method->interfaceName
244 #define State(method, field) ((StateStruct*) method->state)->field
246 #define Value(method, type, field) ((type*) method->value)->field
247 #define Ret(method, type) Value(method, type, RET)
248 #define Arg(method, type, arg) Value(method, type, arg)
250 #define Prev(method) method->prev
251 #define PREV _M->prev
253 #define Next(method) method->next
254 #define NEXT _M->next
256 #define Concurrent(method) method->concurrent
257 #define CONCURRENT _M->concurrent
260 /***************************************************************************/
261 /***************************************************************************/
263 // This auto-generated struct can have different fields according to the read
264 // state declaration. Here it's just a test example
265 typedef struct StateStruct {
269 // These auto-generated struct can have different fields according to the return
270 // value and arguments of the corresponding interface. The struct will have the
271 // same name as the interface name. Here it's just a test example
272 typedef struct Store {
277 typedef struct Load {
283 set<int> *is1 = new set<int>;
284 set<int> *is2 = new set<int>;
286 list<int> *il1 = new list<int>;
287 list<int> *il2 = new list<int>;
299 MethodSet ms = NewMethodSet;
300 Method m = new MethodCall;
301 m->interfaceName = "Store";
302 StateStruct *ss = new StateStruct;
305 Store *st = new Store;
311 m->interfaceName= "Store";
312 ss = new StateStruct;
321 m->interfaceName= "Load";
322 ss = new StateStruct;
330 MakeSet(int, ms, newis, STATE(x));
331 //cout << "Size=" << Size(newis) << " | val= " << Belong(newis, 2) << endl;
332 cout << "HasItem=" << HasItem(ms, Guard(STATE(x) == 2)) << endl;
334 //cout << "elem: " << i << endl;
338 //Subset(ms, sub, NAME == "Store" && VALUE(Store, val) != 0);
339 //cout << "Size=" << Size(Subset(ms, Guard(NAME == "Store" && ARG(Store, val)
340 //>= 0 && STATE(x) >= 0 ))) << endl;