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 *localState; // 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 NewSet 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 The set here is a vector<MethodCall*>* type, or the MethodSet type. And the
43 item would become the MethodCall* type, or the Method type
45 #define ForEach1(item, set) \
47 for (Method item = (set)->size() > 0 ? (*(set))[0] : NULL; \
48 X(i) < (set)->size(); X(i)++, item = X(i) < (set)->size() ? (*(set))[X(i)] : NULL)
50 #define ForEach(item, container) \
51 auto X(_container) = (container); \
52 auto X(iter) = X(_container)->begin(); \
53 for (auto item = *X(iter); X(iter) != X(_container)->end(); item = ((++X(iter)) != \
54 X(_container)->end()) ? *X(iter) : 0)
57 The subset operation is only for the MethodCall set
61 This is a common macro that is used as a constant for the name of specific
62 variables. We basically have two usage scenario:
63 1. In Subset operation, we allow users to specify a condition to extract a
64 subset. In that condition expression, we provide NAME, RET(type), ARG(type,
65 field) and LOCAL(field) to access each item's (method call) information.
66 2. In general specification (in pre- & post- conditions and side effects),
67 we would automatically generate an assignment that assign the current
68 MethodCall* pointer to a variable namedd _M. With this, when we access the
69 local state of the current method, we use LOCAL(field) (this is a reference
77 #define LOCAL(field) Local(_M, field)
79 #define VALUE(type, field) Value(_M, type, field)
80 #define RET(type) VALUE(type, RET)
81 #define ARG(type, arg) VALUE(type, arg)
84 #define Subset(s, subset, condition) \
85 MethodSet original = s; \
86 MethodSet subset = NewSet; \
87 ForEach (_M, original) { \
95 This operation is specifically for Method set. For example, when we want to
96 construct an integer set from the local state field "x" (which is an
97 integer) of the previous set of method calls (PREV), and the new set goes to
98 "readSet", we would call "MakeSet(int, PREV, readSet, LOCAL(x));". Then users
99 can use the "readSet" as an integer set (set<int>)
101 #define MakeSet(type, oldset, newset, field) \
102 auto newset = new set<type>; \
103 ForEach (_M, oldset) \
104 newset->insert(field); \
107 We provide a more general subset operation that takes a plain boolean
108 expression on each item (access by the name "ITEM") of the set, and put it
109 into a new set if the boolean expression (Guard) on that item holds. This is
110 used as the second arguments of the Subset operation. An example to extract
111 a subset of positive elements on an IntSet "s" would be "Subset(s,
112 GeneralGuard(int, ITEM > 0))"
114 #define GeneralGuard(type, expression) std::function<bool(type)> ( \
115 [](type ITEM) -> bool { return (expression);}) \
118 This is a more specific guard designed for the Method (MethodCall*). It
119 basically wrap around the GeneralGuard with the type Method. An example to
120 extract the subset of method calls in the PREV set whose local state "x" is
121 equal to "val" would be "Subset(PREV, Guard(Local(x) == val))"
123 #define Guard(expression) GeneralGuard(Method, expression)
126 A general subset operation that takes a condition and returns all the item
127 for which the boolean guard holds.
130 inline set<T>* Subset(set<T> *original, std::function<bool(T)> condition) {
131 set<T> *res = new set<T>;
132 ForEach (_M, original) {
140 A general sublist operation that takes a condition and returns all the item
141 for which the boolean guard holds in the same order as in the old list.
144 inline list<T>* Sublist(list<T> *original, std::function<bool(T)> condition) {
145 list<T> *res = new list<T>;
146 ForEach (_M, original) {
154 A general subvector operation that takes a condition and returns all the item
155 for which the boolean guard holds in the same order as in the old vector.
158 inline vector<T>* Subvector(vector<T> *original, std::function<bool(T)> condition) {
159 vector<T> *res = new vector<T>;
160 ForEach (_M, original) {
167 /** General for set, list & vector */
168 #define Size(container) ((container)->size())
170 #define _BelongHelper(type) \
172 inline bool Belong(type<T> *container, T item) { \
173 return std::find(container->begin(), \
174 container->end(), item) != container->end(); \
178 _BelongHelper(vector)
181 /** General set operations */
183 inline set<T>* Intersect(set<T> *set1, set<T> *set2) {
184 set<T> *res = new set<T>;
185 ForEach (item, set1) {
186 if (Belong(set2, item))
193 inline set<T>* Union(set<T> *s1, set<T> *s2) {
194 set<T> *res = new set<T>(*s1);
201 inline set<T>* Subtract(set<T> *set1, set<T> *set2) {
202 set<T> *res = new set<T>;
203 ForEach (item, set1) {
204 if (!Belong(set2, item))
211 inline void Insert(set<T> *s, T item) { s->insert(item); }
214 inline void Insert(set<T> *s, set<T> *others) {
215 ForEach (item, others)
220 inline MethodSet MakeSet(int count, ...) {
224 va_start (ap, count);
226 for (int i = 0; i < count; i++) {
227 Method item = va_arg (ap, Method);
235 /********** Method call related operations **********/
236 #define Name(method) method->interfaceName
238 #define Local(method, field) ((StateStruct*) method->localState)->field
240 #define Value(method, type, field) ((type*) method->value)->field
241 #define Ret(method, type) Value(method, type, RET)
242 #define Arg(method, type, arg) Value(method, type, arg)
244 #define Prev(method) method->prev
245 #define PREV _M->prev
247 #define Next(method) method->next
248 #define NEXT _M->next
250 #define Concurrent(method) method->concurrent
251 #define CONCURRENT _M->concurrent
253 // This auto-generated struct can have different fields according to the read
254 // state declaration. Here it's just a test example
255 typedef struct StateStruct {
259 // These auto-generated struct can have different fields according to the return
260 // value and arguments of the corresponding interface. The struct will have the
261 // same name as the interface name. Here it's just a test example
262 typedef struct Store {
267 typedef struct Load {
277 set<int> *is1 = new set<int>;
278 set<int> *is2 = new set<int>;
280 list<int> *il1 = new list<int>;
281 list<int> *il2 = new list<int>;
293 MethodSet ms = NewSet;
294 Method m = new MethodCall;
295 m->interfaceName = "Store";
296 StateStruct *ss = new StateStruct;
299 Store *st = new Store;
305 m->interfaceName= "Store";
306 ss = new StateStruct;
315 m->interfaceName= "Load";
316 ss = new StateStruct;
324 MakeSet(int, ms, newis, LOCAL(x));
325 cout << "Size=" << Size(newis) << " | val= " << Belong(newis, 2) << endl;
327 cout << "elem: " << i << endl;
331 //Subset(ms, sub, NAME == "Store" && VALUE(Store, val) != 0);
332 //cout << "Size=" << Size(Subset(ms, Guard(NAME == "Store" && ARG(Store, val)
333 //>= 0 && LOCAL(x) >= 0 ))) << endl;