From: Peizhao Ou Date: Thu, 28 Jan 2016 11:20:26 +0000 (-0800) Subject: edits X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=bf88290ca3ad6dc68caefb4ebe4a67d42baeeeef;ds=sidebyside edits --- diff --git a/notes/definition.cc b/notes/definition.cc index 51fdd81..46fdc84 100644 --- a/notes/definition.cc +++ b/notes/definition.cc @@ -2,6 +2,8 @@ #include #include #include +#include +#include using namespace std; @@ -19,16 +21,137 @@ typedef struct MethodCall { typedef MethodCall *Method; typedef vector *MethodSet; +typedef vector IntList; + #define NewSet new vector +#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* 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; } diff --git a/notes/nondeterm-spec.txt b/notes/nondeterm-spec.txt index 7eee23d..f86c661 100644 --- a/notes/nondeterm-spec.txt +++ b/notes/nondeterm-spec.txt @@ -241,6 +241,55 @@ inline vector* Subset(vector *set, string name) { } 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 @@ -264,16 +313,13 @@ inline vector* Subset(vector *set, string name) { @PreCondition: // Auto generated code // MethodCall *ME = ((SomeTypeConversion) info)->method; - // vector PREV = Me->prev; - // vector NEXT = Me->next; - // vector 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: @@ -317,17 +363,15 @@ void enq(queue_t *q, int val); // 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; }