notes/definition.cc

   1 #include <iostream>
   2 #include <vector>
   3 #include <list>
   4 #include <string>
   5 #include <iterator>
   6 #include <algorithm>
   7 #include <set>
   8
   9 #include <stdarg.h>
  10
  11 using namespace std;
  12
  13 typedef struct MethodCall {
  14         string interfaceName; // The interface label name
  15         void *value; // The pointer that points to the struct that have the return
  16                                  // value and the arguments
  17         void *localState; // The pointer that points to the struct that represents
  18                                           // the (local) state
  19         set<MethodCall*> *prev; // Method calls that are hb right before me
  20         set<MethodCall*> *next; // Method calls that are hb right after me
  21         set<MethodCall*> *concurrent; // Method calls that are concurrent with me
  22 } MethodCall;
  23
  24 typedef MethodCall *Method;
  25 typedef set<Method> *MethodSet;
  26
  27 typedef vector<int> IntVector;
  28 typedef list<int> IntList;
  29 typedef set<int> IntSet;
  30
  31 /********** More general specification-related types and operations **********/
  32
  33 #define NewSet new set<Method>
  34
  35 #define CAT(a, b) CAT_HELPER(a, b) /* Concatenate two symbols for macros! */
  36 #define CAT_HELPER(a, b) a ## b
  37 #define X(name) CAT(__##name, __LINE__) /* unique variable */
  38
  39 /**
  40         The set here is a vector<MethodCall*>* type, or the MethodSet type. And the
  41         item would become the MethodCall* type, or the Method type
  42 */
  43 #define ForEach1(item, set) \
  44         int X(i) = 0; \
  45         for (Method item = (set)->size() > 0 ? (*(set))[0] : NULL; \
  46                 X(i) < (set)->size(); X(i)++, item = X(i) < (set)->size() ? (*(set))[X(i)] : NULL)
  47
  48 #define ForEach(item, container) \
  49         auto X(_container) = (container); \
  50         auto X(iter) = X(_container)->begin(); \
  51         for (auto item = *X(iter); X(iter) != X(_container)->end(); item = ((++X(iter)) != \
  52                 X(_container)->end()) ? *X(iter) : 0)
  53
  54 /**
  55         The subset operation is only for the MethodCall set
  56 */
  57
  58 #define _M ME
  59
  60 #define NAME Name(_M)
  61
  62 #define LOCAL(field) Local(_M, field)
  63
  64 #define VALUE(type, field) Value(_M, type, field)
  65
  66 #define Subset(s, subset, condition) \
  67         MethodSet original = s; \
  68         MethodSet subset = NewSet; \
  69         ForEach (_M, original) { \
  70                 if ((condition)) \
  71                         subset->insert(_M); \
  72         } \
  73
  74 /** General for set, list & vector */
  75 #define Size(container) ((container)->size())
  76
  77 #define _BelongHelper(type) \
  78         template<class T> \
  79         inline bool Belong(type<T> *container, T item) { \
  80                 return std::find(container->begin(), \
  81                         container->end(), item) != container->end(); \
  82         }
  83
  84 _BelongHelper(set)
  85 _BelongHelper(vector)
  86 _BelongHelper(list)
  87
  88 /** General set operations */
  89 template<class T>
  90 inline set<T>* Intersect(set<T> *set1, set<T> *set2) {
  91         set<T> *res = new set<T>;
  92         ForEach (item, set1) {
  93                 if (Belong(set2, item))
  94                         res->insert(item);
  95         }
  96         return res;
  97 }
  98
  99 template<class T>
 100 inline set<T>* Union(set<T> *s1, set<T> *s2) {
 101         set<T> *res = new set<T>(*s1);
 102         ForEach (item, s2)
 103                 res->insert(item);
 104         return res;
 105 }
 106
 107 template<class T>
 108 inline set<T>* Subtract(set<T> *set1, set<T> *set2) {
 109         set<T> *res = new set<T>;
 110         ForEach (item, set1) {
 111                 if (!Belong(set2, item))
 112                         res->insert(item);
 113         }
 114         return res;
 115 }
 116
 117 template<class T>
 118 inline void Insert(set<T> *s, T item) { s->insert(item); }
 119
 120 template<class T>
 121 inline void Insert(set<T> *s, set<T> *others) {
 122         ForEach (item, others)
 123                 s->insert(item);
 124 }
 125
 126 inline MethodSet MakeSet(int count, ...) {
 127         va_list ap;
 128         MethodSet res;
 129
 130         va_start (ap, count);
 131         res = NewSet;
 132         for (int i = 0; i < count; i++) {
 133                 Method item = va_arg (ap, Method);
 134                 res->insert(item);
 135         }
 136         va_end (ap);
 137         return res;
 138 }
 139
 140 /********** Method call related operations **********/
 141 #define Name(method) method->interfaceName
 142
 143 #define Local(method, field) ((StateStruct*) method->localState)->field
 144
 145 #define Value(method, type, field) ((type*) method->value)->field
 146
 147 #define Prev(method) method->prev
 148 #define PREV ME->prev
 149
 150 #define Next(method) method->next
 151 #define NEXT ME->next
 152
 153 #define Concurrent(method) method->concurrent
 154 #define CONCURRENT  ME->concurrent
 155
 156 // This auto-generated struct can have different fields according to the read
 157 // state declaration. Here it's just a test example
 158 typedef struct StateStruct {
 159         int x;
 160 } StateStruct;
 161
 162 // These auto-generated struct can have different fields according to the return
 163 // value and arguments of the corresponding interface. The struct will have the
 164 // same name as the interface name. Here it's just a test example
 165 typedef struct Store {
 166         int *loc;
 167         int val;
 168 } Store;
 169
 170 typedef struct Load {
 171         int RET;
 172         int *loc;
 173 } Load;
 174
 175 int main() {
 176         set<int> *is1 = new set<int>;
 177         set<int> *is2 = new set<int>;
 178
 179         list<int> *il1 = new list<int>;
 180         list<int> *il2 = new list<int>;
 181
 182         il1->push_back(2);
 183         il1->push_back(3);
 184
 185         is1->insert(1);
 186         is1->insert(3);
 187
 188         is2->insert(4);
 189         is2->insert(5);
 190
 191
 192         MethodSet ms = NewSet;
 193         Method m = new MethodCall;
 194         m->interfaceName = "Store";
 195         StateStruct *ss = new StateStruct;
 196         ss->x = 1;
 197         m->localState = ss;
 198         Store *st = new Store;
 199         st->val = 2;
 200         m->value = st;
 201         ms->insert(m);
 202
 203         m = new MethodCall;
 204         m->interfaceName= "Store";
 205         ss = new StateStruct;
 206         ss->x = 2;
 207         m->localState = ss;
 208         st = new Store;
 209         st->val = 0;
 210         m->value = st;
 211         ms->insert(m);
 212
 213         m = new MethodCall;
 214         m->interfaceName= "Load";
 215         ss = new StateStruct;
 216         ss->x = 0;
 217         m->localState = ss;
 218         Load *ld = new Load;
 219         ld->RET = 2;
 220         m->value = ld;
 221         ms->insert(m);
 222
 223         //Subset(ms, sub, NAME == "Store" && VALUE(Store, val) != 0);
 224         Subset(ms, sub, NAME == "Store" && VALUE(Store, val) >= 0 && LOCAL(x) == 0);
 225
 226         cout << "Size=" << Size(sub) << endl;
 227         return 0;
 228 }