17 typedef MethodCall *Method;
18 typedef set<Method> *MethodSet;
21 string interfaceName; // The interface label name
22 void *value; // The pointer that points to the struct that have the return
23 // value and the arguments
24 void *state; // The pointer that points to the struct that represents
26 MethodSet prev; // Method calls that are hb right before me
27 MethodSet next; // Method calls that are hb right after me
28 MethodSet concurrent; // Method calls that are concurrent with me
30 MethodCall(string name) : MethodCall() { interfaceName = name; }
32 MethodCall() : interfaceName(""), prev(new set<Method>),
33 next(new set<Method>), concurrent(new set<Method>) { }
35 void addPrev(Method m) { prev->insert(m); }
37 void addNext(Method m) { next->insert(m); }
39 void addConcurrent(Method m) { concurrent->insert(m); }
44 typedef vector<int> IntVector;
45 typedef list<int> IntList;
46 typedef set<int> IntSet;
48 typedef vector<double> DoubleVector;
49 typedef list<double> DoubleList;
50 typedef set<double> DoubleSet;
52 /********** More general specification-related types and operations **********/
54 #define NewMethodSet new set<Method>
56 #define CAT(a, b) CAT_HELPER(a, b) /* Concatenate two symbols for macros! */
57 #define CAT_HELPER(a, b) a ## b
58 #define X(name) CAT(__##name, __LINE__) /* unique variable */
61 This is a generic ForEach primitive for all the containers that support
62 using iterator to iterate.
64 #define ForEach(item, container) \
65 auto X(_container) = (container); \
66 auto X(iter) = X(_container)->begin(); \
67 for (auto item = *X(iter); X(iter) != X(_container)->end(); item = ((++X(iter)) != \
68 X(_container)->end()) ? *X(iter) : 0)
71 This is a common macro that is used as a constant for the name of specific
72 variables. We basically have two usage scenario:
73 1. In Subset operation, we allow users to specify a condition to extract a
74 subset. In that condition expression, we provide NAME, RET(type), ARG(type,
75 field) and STATE(field) to access each item's (method call) information.
76 2. In general specification (in pre- & post- conditions and side effects),
77 we would automatically generate an assignment that assign the current
78 MethodCall* pointer to a variable namedd _M. With this, when we access the
79 state of the current method, we use STATE(field) (this is a reference
87 #define STATE(field) State(_M, field)
89 #define VALUE(type, field) Value(_M, type, field)
90 #define RET(type) VALUE(type, RET)
91 #define ARG(type, arg) VALUE(type, arg)
94 #define Subset(s, subset, condition) \
95 MethodSet original = s; \
96 MethodSet subset = NewMethodSet; \
97 ForEach (_M, original) { \
105 This operation is specifically for Method set. For example, when we want to
106 construct an integer set from the state field "x" (which is an
107 integer) of the previous set of method calls (PREV), and the new set goes to
108 "readSet", we would call "MakeSet(int, PREV, readSet, STATE(x));". Then users
109 can use the "readSet" as an integer set (set<int>)
111 #define MakeSet(type, oldset, newset, field) \
112 auto newset = new set<type>; \
113 ForEach (_M, oldset) \
114 newset->insert(field); \
117 We provide a more general subset operation that takes a plain boolean
118 expression on each item (access by the name "ITEM") of the set, and put it
119 into a new set if the boolean expression (Guard) on that item holds. This
120 is used as the second arguments of the Subset operation. An example to
121 extract a subset of positive elements on an IntSet "s" would be "Subset(s,
122 GeneralGuard(int, ITEM > 0))"
124 #define GeneralGuard(type, expression) std::function<bool(type)> ( \
125 [&](type ITEM) -> bool { return (expression);}) \
128 This is a more specific guard designed for the Method (MethodCall*). It
129 basically wrap around the GeneralGuard with the type Method. An example to
130 extract the subset of method calls in the PREV set whose state "x" is equal
131 to "val" would be "Subset(PREV, Guard(STATE(x) == val))"
133 #define Guard(expression) GeneralGuard(Method, expression)
136 A general subset operation that takes a condition and returns all the item
137 for which the boolean guard holds.
139 inline MethodSet Subset(MethodSet original, std::function<bool(Method)> condition) {
140 MethodSet res = new SnapSet<Method>;
141 ForEach (_M, original) {
149 A general set operation that takes a condition and returns if there exists
150 any item for which the boolean guard holds.
153 inline bool HasItem(set<T> *original, std::function<bool(T)> condition) {
154 ForEach (_M, original) {
164 A general sublist operation that takes a condition and returns all the item
165 for which the boolean guard holds in the same order as in the old list.
168 inline list<T>* Sublist(list<T> *original, std::function<bool(T)> condition) {
169 list<T> *res = new list<T>;
170 ForEach (_M, original) {
178 A general subvector operation that takes a condition and returns all the item
179 for which the boolean guard holds in the same order as in the old vector.
182 inline vector<T>* Subvector(vector<T> *original, std::function<bool(T)> condition) {
183 vector<T> *res = new vector<T>;
184 ForEach (_M, original) {
191 /** General for set, list & vector */
192 #define Size(container) ((container)->size())
194 #define _BelongHelper(type) \
196 inline bool Belong(type<T> *container, T item) { \
197 return std::find(container->begin(), \
198 container->end(), item) != container->end(); \
202 _BelongHelper(vector)
205 /** General set operations */
207 inline set<T>* Intersect(set<T> *set1, set<T> *set2) {
208 set<T> *res = new set<T>;
209 ForEach (item, set1) {
210 if (Belong(set2, item))
217 inline set<T>* Union(set<T> *s1, set<T> *s2) {
218 set<T> *res = new set<T>(*s1);
225 inline set<T>* Subtract(set<T> *set1, set<T> *set2) {
226 set<T> *res = new set<T>;
227 ForEach (item, set1) {
228 if (!Belong(set2, item))
235 inline void Insert(set<T> *s, T item) { s->insert(item); }
238 inline void Insert(set<T> *s, set<T> *others) {
239 ForEach (item, others)
244 inline MethodSet MakeSet(int count, ...) {
248 va_start (ap, count);
250 for (int i = 0; i < count; i++) {
251 Method item = va_arg (ap, Method);
259 /********** Method call related operations **********/
260 #define Name(method) method->interfaceName
262 #define State(method, field) ((StateStruct*) method->state)->field
264 #define Value(method, type, field) ((type*) method->value)->field
265 #define Ret(method, type) Value(method, type, RET)
266 #define Arg(method, type, arg) Value(method, type, arg)
268 #define Prev(method) method->prev
269 #define PREV _M->prev
271 #define Next(method) method->next
272 #define NEXT _M->next
274 #define Concurrent(method) method->concurrent
275 #define CONCURRENT _M->concurrent
278 /***************************************************************************/
279 /***************************************************************************/
281 // This auto-generated struct can have different fields according to the read
282 // state declaration. Here it's just a test example
283 typedef struct StateStruct {
287 // These auto-generated struct can have different fields according to the return
288 // value and arguments of the corresponding interface. The struct will have the
289 // same name as the interface name. Here it's just a test example
290 typedef struct Store {
295 typedef struct Load {
301 set<int> *is1 = new set<int>;
302 set<int> *is2 = new set<int>;
304 list<int> *il1 = new list<int>;
305 list<int> *il2 = new list<int>;
317 MethodSet ms = NewMethodSet;
318 Method m = new MethodCall;
319 m->interfaceName = "Store";
320 StateStruct *ss = new StateStruct;
323 Store *st = new Store;
329 m->interfaceName= "Store";
330 ss = new StateStruct;
339 m->interfaceName= "Load";
340 ss = new StateStruct;
348 //MakeSet(int, ms, newis, STATE(x));
349 //cout << "Size=" << Size(newis) << " | val= " << Belong(newis, 2) << endl;
353 cout << "HasItem=" << HasItem(ms, Guard(STATE(x) == x && y == 0)) << endl;
355 //ForEach (i, newis) {
356 //cout << "elem: " << i << endl;
360 //Subset(ms, sub, NAME == "Store" && VALUE(Store, val) != 0);
361 //cout << "Size=" << Size(Subset(ms, Guard(NAME == "Store" && ARG(Store, val)
362 //>= 0 && STATE(x) >= 0 ))) << endl;