#include <iostream>
#include <vector>
+#include <list>
#include <string>
#include <iterator>
+#include <algorithm>
+#include <set>
+
+#include <stdarg.h>
using namespace std;
// value and the arguments
void *localState; // The pointer that points to the struct that represents
// the (local) state
- vector<MethodCall*> *prev; // Method calls that are hb right before me
- vector<MethodCall*> *next; // Method calls that are hb right after me
- vector<MethodCall*> *concurrent; // Method calls that are concurrent with me
+ set<MethodCall*> *prev; // Method calls that are hb right before me
+ set<MethodCall*> *next; // Method calls that are hb right after me
+ set<MethodCall*> *concurrent; // Method calls that are concurrent with me
} MethodCall;
typedef MethodCall *Method;
-typedef vector<Method> *MethodSet;
+typedef set<Method> *MethodSet;
+
+typedef vector<int> IntVector;
+typedef list<int> IntList;
+typedef set<int> IntSet;
+
+/********** More general specification-related types and operations **********/
-#define NewSet new vector<Method>
+#define NewSet new set<Method>
+
+#define CAT(a, b) CAT_HELPER(a, b) /* Concatenate two symbols for macros! */
+#define CAT_HELPER(a, b) a ## b
+#define X(name) CAT(__##name, __LINE__) /* unique variable */
/**
The set here is a vector<MethodCall*>* type, or the MethodSet type. And the
item would become the MethodCall* type, or the Method type
*/
-#define ForEach(item, set) \
- for (int i = 0, Method item = (set)->size() > 0 ? (*(set))[0] : NULL; \
- i < (set)->size(); i++,
+#define ForEach1(item, set) \
+ int X(i) = 0; \
+ for (Method item = (set)->size() > 0 ? (*(set))[0] : NULL; \
+ X(i) < (set)->size(); X(i)++, item = X(i) < (set)->size() ? (*(set))[X(i)] : NULL)
+
+#define ForEach(item, container) \
+ auto X(_container) = (container); \
+ auto X(iter) = X(_container)->begin(); \
+ for (auto item = *X(iter); X(iter) != X(_container)->end(); item = ((++X(iter)) != \
+ X(_container)->end()) ? *X(iter) : 0)
+
+/**
+ The subset operation is only for the MethodCall set
+*/
+
+#define _M ME
+
+#define NAME Name(_M)
+
+#define LOCAL(field) Local(_M, field)
+
+#define VALUE(type, field) Value(_M, type, field)
+
+#define Subset(s, subset, condition) \
+ MethodSet original = s; \
+ MethodSet subset = NewSet; \
+ ForEach (_M, original) { \
+ if ((condition)) \
+ subset->insert(_M); \
+ } \
+
+/** General for set, list & vector */
+#define Size(container) ((container)->size())
+
+#define _BelongHelper(type) \
+ template<class T> \
+ inline bool Belong(type<T> *container, T item) { \
+ return std::find(container->begin(), \
+ container->end(), item) != container->end(); \
+ }
+
+_BelongHelper(set)
+_BelongHelper(vector)
+_BelongHelper(list)
+
+/** General set operations */
+template<class T>
+inline set<T>* Intersect(set<T> *set1, set<T> *set2) {
+ set<T> *res = new set<T>;
+ ForEach (item, set1) {
+ if (Belong(set2, item))
+ res->insert(item);
+ }
+ return res;
+}
+
+template<class T>
+inline set<T>* Union(set<T> *s1, set<T> *s2) {
+ set<T> *res = new set<T>(*s1);
+ ForEach (item, s2)
+ res->insert(item);
+ return res;
+}
+
+template<class T>
+inline set<T>* Subtract(set<T> *set1, set<T> *set2) {
+ set<T> *res = new set<T>;
+ ForEach (item, set1) {
+ if (!Belong(set2, item))
+ res->insert(item);
+ }
+ return res;
+}
+
+template<class T>
+inline void Insert(set<T> *s, T item) { s->insert(item); }
+
+template<class T>
+inline void Insert(set<T> *s, set<T> *others) {
+ ForEach (item, others)
+ s->insert(item);
+}
+
+inline MethodSet MakeSet(int count, ...) {
+ va_list ap;
+ MethodSet res;
+
+ va_start (ap, count);
+ res = NewSet;
+ for (int i = 0; i < count; i++) {
+ Method item = va_arg (ap, Method);
+ res->insert(item);
+ }
+ va_end (ap);
+ return res;
+}
+
+/********** Method call related operations **********/
+#define Name(method) method->interfaceName
+
+#define Local(method, field) ((StateStruct*) method->localState)->field
+
+#define Value(method, type, field) ((type*) method->value)->field
+
+#define Prev(method) method->prev
+#define PREV ME->prev
+
+#define Next(method) method->next
+#define NEXT ME->next
+
+#define Concurrent(method) method->concurrent
+#define CONCURRENT ME->concurrent
+
+// This auto-generated struct can have different fields according to the read
+// state declaration. Here it's just a test example
+typedef struct StateStruct {
+ int x;
+} StateStruct;
+
+// These auto-generated struct can have different fields according to the return
+// value and arguments of the corresponding interface. The struct will have the
+// same name as the interface name. Here it's just a test example
+typedef struct Store {
+ int *loc;
+ int val;
+} Store;
+
+typedef struct Load {
+ int RET;
+ int *loc;
+} Load;
int main() {
+ set<int> *is1 = new set<int>;
+ set<int> *is2 = new set<int>;
+
+ list<int> *il1 = new list<int>;
+ list<int> *il2 = new list<int>;
+
+ il1->push_back(2);
+ il1->push_back(3);
+
+ is1->insert(1);
+ is1->insert(3);
+
+ is2->insert(4);
+ is2->insert(5);
+
+
+ MethodSet ms = NewSet;
+ Method m = new MethodCall;
+ m->interfaceName = "Store";
+ StateStruct *ss = new StateStruct;
+ ss->x = 1;
+ m->localState = ss;
+ Store *st = new Store;
+ st->val = 2;
+ m->value = st;
+ ms->insert(m);
+
+ m = new MethodCall;
+ m->interfaceName= "Store";
+ ss = new StateStruct;
+ ss->x = 2;
+ m->localState = ss;
+ st = new Store;
+ st->val = 0;
+ m->value = st;
+ ms->insert(m);
+
+ m = new MethodCall;
+ m->interfaceName= "Load";
+ ss = new StateStruct;
+ ss->x = 0;
+ m->localState = ss;
+ Load *ld = new Load;
+ ld->RET = 2;
+ m->value = ld;
+ ms->insert(m);
+
+ //Subset(ms, sub, NAME == "Store" && VALUE(Store, val) != 0);
+ Subset(ms, sub, NAME == "Store" && VALUE(Store, val) >= 0 && LOCAL(x) == 0);
+
+ cout << "Size=" << Size(sub) << endl;
return 0;
}