#include <vector>
#include <string>
#include <iterator>
+#include <algorithm>
+#include <set>
using namespace std;
typedef MethodCall *Method;
typedef vector<Method> *MethodSet;
+typedef vector<int> IntList;
+
#define NewSet new vector<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++,
+ 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)
+
+inline MethodSet Subset(MethodSet set, string name) {
+ MethodSet _subset = NewSet;
+ ForEach (_m, set) {
+ if (_m->interfaceName == name)
+ _subset->push_back(_m);
+ }
+ return _subset;
+}
+
+#define Size(set) (set->size())
+
+#define Belong(set, method) (std::find(set->begin(), set->end(), method) \
+ != set->end())
+
+inline MethodSet Intersect(MethodSet set1, MethodSet set2) {
+ MethodSet res = NewSet;
+ ForEach (m, set1) {
+ if (Belong(set2, m))
+ res->push_back(m);
+ }
+ return res;
+}
+
+inline MethodSet Union(MethodSet set1, MethodSet set2) {
+ MethodSet res = NewSet(*set1);
+ ForEach (m, set2) {
+ if (!Belong(set1, m))
+ res->push_back(m);
+ }
+ return res;
+}
+
+inline MethodSet Subtract(MethodSet set1, MethodSet set2) {
+ MethodSet res = NewSet;
+ ForEach (m, set1) {
+ if (!Belong(set2, m))
+ res->push_back(m);
+ }
+ return res;
+}
+
+inline bool Insert(MethodSet set, Method m) {
+ if (Belong(set, m))
+ return false;
+ else {
+ set->push_back(m);
+ return true;
+ }
+}
+
+inline MethodSet MakeSet(int count, ...) {
+ va_list ap;
+ MethodSet res;
+
+ va_start (ap, count);
+ res = NewSet;
+ for (int i = 0; i < count; i++) {
+ Method m = va_arg (ap, Method);
+ if (!Belong(res, m))
+ res->push_back(m);
+ }
+ va_end (ap);
+ return res;
+}
+
+
+#define Local(method, field) ((StateStruct*) method->localState)->field
+
+#define Value(method, type, field) ((type*) method->value)->field
+
+#define Label(method) method->interfaceName
+
+#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 {
+ IntList *list;
+} 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() {
+ Method ME = NULL;
+ MethodSet set = NewSet;
+ ForEach (m, Subset(set, "Store")) {
+ IntList *l = Local(m, list);
+ int ret = Value(m, Load, RET);
+ string name = Label(m);
+ }
+ ForEach (m, Prev(ME)) {
+
+ }
+
+ int size = Size(PREV);
+ bool flag = Belong(CONCURRENT, ME);
+ flag = Belong(MakeSet(3, ME, ME, ME), ME);
return 0;
}
}
return _subset;
}
+
+// 1.2 Size(set) --> to get the size of a method set
+#define Size(set) set->size()
+
+// 1.3 Belong(set, method) --> whether method belongs to set
+#define Belong(set, method) std::find(set->begin(), set->end(), method) != set->end()
+
+// 1.4 Intersect(set1, set2) --> the intersection of two method sets
+inline MethodSet Intersect(MethodSet set1, MethodSet set2) {
+ MethodSet res = NewSet;
+ ForEach (m, set1) {
+ if (Belong(set2, m))
+ res->push_back(m);
+ }
+ return res;
+}
+
+// 1.5 Union(set1, set2) --> the union of two method sets
+inline MethodSet Union(MethodSet set1, MethodSet set2) {
+ MethodSet res = NewSet(set1);
+ ForEach (m, set2) {
+ if (!Belong(set1, m))
+ res->push_back(m);
+ }
+ return res;
+}
+
+// 1.6 Insert(set, method) --> add a method to the set
+inline bool Insert(MethodSet set, Method m) {
+ if (Belong(set, m))
+ return false;
+ else {
+ set->push_back(m);
+ return true;
+ }
+}
+
+// 1.7 Subtract(set1, set2) --> subtract set2 from set1
+inline MethodSet Subtract(MethodSet set1, MethodSet set2) {
+ MethodSet res = NewSet;
+ ForEach (m, set1) {
+ if (!Belong(set2, m))
+ res->push_back(m);
+ }
+ return res;
+}
+
+// 1.8 MakeSet(count, ...) --> Make a set from the arguments
+
// 2. Local(method, field)
#define Local(method, field) ((StateStruct*) method->localState)->field
@PreCondition:
// Auto generated code
// MethodCall *ME = ((SomeTypeConversion) info)->method;
- // vector<MethodCall*> PREV = Me->prev;
- // vector<MethodCall*> NEXT = Me->next;
- // vector<MethodCall*> CONCURRENT = Me->concurrent;
IntegerSet prevSet, concurSet;
ForEach(m, PREV) {
- prevSet.add(LOCAL(m, x));
+ prevSet->insert(LOCAL(m, x));
}
- ForEach (m, CONCURRENT("STORE")) {
- concurSet->add(m.val);
+ ForEach (m, Subset(CONCURRENT, "STORE")) {
+ concurSet->insert(Value(m, STORE, val));
}
return prevSet->contains(RET) || concurSet->contains(RET);
@SideEffect:
// dequeue them
if (!RET) {
// Local state is empty
- if (Local.q->size() == 0)
- return true;
+ if (Local.q->size() == 0) return true;
// Otherwise check there must be other concurrent dequeuers
for (int i = 0; i < Local.q->size(); i++) {
int item = (*Local.q)[i];
// Check there's some concurrent dequeuer for this item
bool flag = false;
- for (m in CONCURRENT("Deq")) {
- if (m.RET) {
- if (*m.res == item) flag = true;
- }
+ ForEach (m, Subset(CONCURRENT, "Deq")) {
+ if (Value(m, Deq, RET) && *Value(m, Deq, res) == item)
+ flag = true;
}
if (!flag) return false;
}
projects / cdsspec-compiler.git / commitdiff