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 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 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 = NewSet; \
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 sublist operation that takes a condition and returns all the item
132 for which the boolean guard holds in the same order as in the old list.
135 inline list<T>* Sublist(list<T> *original, std::function<bool(T)> condition) {
136 list<T> *res = new list<T>;
137 ForEach (_M, original) {
145 A general subvector operation that takes a condition and returns all the item
146 for which the boolean guard holds in the same order as in the old vector.
149 inline vector<T>* Subvector(vector<T> *original, std::function<bool(T)> condition) {
150 vector<T> *res = new vector<T>;
151 ForEach (_M, original) {
158 /** General for set, list & vector */
159 #define Size(container) ((container)->size())
161 #define _BelongHelper(type) \
163 inline bool Belong(type<T> *container, T item) { \
164 return std::find(container->begin(), \
165 container->end(), item) != container->end(); \
169 _BelongHelper(vector)
172 /** General set operations */
174 inline set<T>* Intersect(set<T> *set1, set<T> *set2) {
175 set<T> *res = new set<T>;
176 ForEach (item, set1) {
177 if (Belong(set2, item))
184 inline set<T>* Union(set<T> *s1, set<T> *s2) {
185 set<T> *res = new set<T>(*s1);
192 inline set<T>* Subtract(set<T> *set1, set<T> *set2) {
193 set<T> *res = new set<T>;
194 ForEach (item, set1) {
195 if (!Belong(set2, item))
202 inline void Insert(set<T> *s, T item) { s->insert(item); }
205 inline void Insert(set<T> *s, set<T> *others) {
206 ForEach (item, others)
211 inline MethodSet MakeSet(int count, ...) {
215 va_start (ap, count);
217 for (int i = 0; i < count; i++) {
218 Method item = va_arg (ap, Method);
226 /********** Method call related operations **********/
227 #define Name(method) method->interfaceName
229 #define State(method, field) ((StateStruct*) method->state)->field
231 #define Value(method, type, field) ((type*) method->value)->field
232 #define Ret(method, type) Value(method, type, RET)
233 #define Arg(method, type, arg) Value(method, type, arg)
235 #define Prev(method) method->prev
236 #define PREV _M->prev
238 #define Next(method) method->next
239 #define NEXT _M->next
241 #define Concurrent(method) method->concurrent
242 #define CONCURRENT _M->concurrent
245 /***************************************************************************/
246 /***************************************************************************/
248 // This auto-generated struct can have different fields according to the read
249 // state declaration. Here it's just a test example
250 typedef struct StateStruct {
254 // These auto-generated struct can have different fields according to the return
255 // value and arguments of the corresponding interface. The struct will have the
256 // same name as the interface name. Here it's just a test example
257 typedef struct Store {
262 typedef struct Load {
268 set<int> *is1 = new set<int>;
269 set<int> *is2 = new set<int>;
271 list<int> *il1 = new list<int>;
272 list<int> *il2 = new list<int>;
284 MethodSet ms = NewSet;
285 Method m = new MethodCall;
286 m->interfaceName = "Store";
287 StateStruct *ss = new StateStruct;
290 Store *st = new Store;
296 m->interfaceName= "Store";
297 ss = new StateStruct;
306 m->interfaceName= "Load";
307 ss = new StateStruct;
315 MakeSet(int, ms, newis, STATE(x));
316 cout << "Size=" << Size(newis) << " | val= " << Belong(newis, 2) << endl;
318 cout << "elem: " << i << endl;
322 //Subset(ms, sub, NAME == "Store" && VALUE(Store, val) != 0);
323 //cout << "Size=" << Size(Subset(ms, Guard(NAME == "Store" && ARG(Store, val)
324 //>= 0 && STATE(x) >= 0 ))) << endl;