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 <functional>
  10
  11 #include <stdarg.h>
  12
  13 using namespace std;
  14
  15 typedef struct MethodCall {
  16         string interfaceName; // The interface label name
  17         void *value; // The pointer that points to the struct that have the return
  18                                  // value and the arguments
  19         void *localState; // The pointer that points to the struct that represents
  20                                           // the (local) state
  21         set<MethodCall*> *prev; // Method calls that are hb right before me
  22         set<MethodCall*> *next; // Method calls that are hb right after me
  23         set<MethodCall*> *concurrent; // Method calls that are concurrent with me
  24 } MethodCall;
  25
  26 typedef MethodCall *Method;
  27 typedef set<Method> *MethodSet;
  28
  29 typedef vector<int> IntVector;
  30 typedef list<int> IntList;
  31 typedef set<int> IntSet;
  32
  33 /********** More general specification-related types and operations **********/
  34
  35 #define NewSet new set<Method>
  36
  37 #define CAT(a, b) CAT_HELPER(a, b) /* Concatenate two symbols for macros! */
  38 #define CAT_HELPER(a, b) a ## b
  39 #define X(name) CAT(__##name, __LINE__) /* unique variable */
  40
  41 /**
  42         The set here is a vector<MethodCall*>* type, or the MethodSet type. And the
  43         item would become the MethodCall* type, or the Method type
  44 */
  45 #define ForEach1(item, set) \
  46         int X(i) = 0; \
  47         for (Method item = (set)->size() > 0 ? (*(set))[0] : NULL; \
  48                 X(i) < (set)->size(); X(i)++, item = X(i) < (set)->size() ? (*(set))[X(i)] : NULL)
  49
  50 #define ForEach(item, container) \
  51         auto X(_container) = (container); \
  52         auto X(iter) = X(_container)->begin(); \
  53         for (auto item = *X(iter); X(iter) != X(_container)->end(); item = ((++X(iter)) != \
  54                 X(_container)->end()) ? *X(iter) : 0)
  55
  56 /**
  57         The subset operation is only for the MethodCall set
  58 */
  59
  60 /**
  61         This is a common macro that is used as a constant for the name of specific
  62         variables. We basically have two usage scenario:
  63         1. In Subset operation, we allow users to specify a condition to extract a
  64         subset. In that condition expression, we provide NAME, RET(type), ARG(type,
  65         field) and LOCAL(field) to access each item's (method call) information.
  66         2. In general specification (in pre- & post- conditions and side effects),
  67         we would automatically generate an assignment that assign the current
  68         MethodCall* pointer to a variable namedd _M. With this, when we access the
  69         local state of the current method, we use LOCAL(field) (this is a reference
  70         for read/write).
  71 */
  72 #define ITEM _M
  73 #define _M ME
  74
  75 #define NAME Name(_M)
  76
  77 #define LOCAL(field) Local(_M, field)
  78
  79 #define VALUE(type, field) Value(_M, type, field)
  80 #define RET(type) VALUE(type, RET)
  81 #define ARG(type, arg) VALUE(type, arg)
  82
  83 /*
  84 #define Subset(s, subset, condition) \
  85         MethodSet original = s; \
  86         MethodSet subset = NewSet; \
  87         ForEach (_M, original) { \
  88                 if ((condition)) \
  89                         subset->insert(_M); \
  90         } \
  91 */
  92
  93
  94 /**
  95         This operation is specifically for Method set. For example, when we want to
  96         construct an integer set from the local state field "x" (which is an
  97         integer) of the previous set of method calls (PREV), and the new set goes to
  98         "readSet", we would call "MakeSet(int, PREV, readSet, LOCAL(x));". Then users
  99         can use the "readSet" as an integer set (set<int>)
 100 */
 101 #define MakeSet(type, oldset, newset, field) \
 102         auto newset = new set<type>; \
 103         ForEach (_M, oldset) \
 104                 newset->insert(field); \
 105
 106 /**
 107         We provide a more general subset operation that takes a plain boolean
 108         expression on each item (access by the name "ITEM") of the set, and put it
 109         into a new set if the boolean expression (Guard) on that item holds. This is
 110         used as the second arguments of the Subset operation. An example to extract
 111         a subset of positive elements on an IntSet "s" would be "Subset(s,
 112         GeneralGuard(int, ITEM > 0))"
 113 */
 114 #define GeneralGuard(type, expression)  std::function<bool(type)> ( \
 115         [](type ITEM) -> bool { return (expression);}) \
 116
 117 /**
 118         This is a more specific guard designed for the Method (MethodCall*). It
 119         basically wrap around the GeneralGuard with the type Method. An example to
 120         extract the subset of method calls in the PREV set whose local state "x" is
 121         equal to "val" would be "Subset(PREV, Guard(Local(x) == val))"
 122 */
 123 #define Guard(expression) GeneralGuard(Method, expression)
 124
 125 /**
 126         A general subset operation that takes a condition and returns all the item
 127         for which the boolean guard holds.
 128 */
 129 template <class T>
 130 inline set<T>* Subset(set<T> *original, std::function<bool(T)> condition) {
 131         set<T> *res = new set<T>;
 132         ForEach (_M, original) {
 133                 if (condition(_M))
 134                         res->insert(_M);
 135         }
 136         return res;
 137 }
 138
 139 /**
 140         A general sublist operation that takes a condition and returns all the item
 141         for which the boolean guard holds in the same order as in the old list.
 142 */
 143 template <class T>
 144 inline list<T>* Sublist(list<T> *original, std::function<bool(T)> condition) {
 145         list<T> *res = new list<T>;
 146         ForEach (_M, original) {
 147                 if (condition(_M))
 148                         res->push_back(_M);
 149         }
 150         return res;
 151 }
 152
 153 /**
 154         A general subvector operation that takes a condition and returns all the item
 155         for which the boolean guard holds in the same order as in the old vector.
 156 */
 157 template <class T>
 158 inline vector<T>* Subvector(vector<T> *original, std::function<bool(T)> condition) {
 159         vector<T> *res = new vector<T>;
 160         ForEach (_M, original) {
 161                 if (condition(_M))
 162                         res->push_back(_M);
 163         }
 164         return res;
 165 }
 166
 167 /** General for set, list & vector */
 168 #define Size(container) ((container)->size())
 169
 170 #define _BelongHelper(type) \
 171         template<class T> \
 172         inline bool Belong(type<T> *container, T item) { \
 173                 return std::find(container->begin(), \
 174                         container->end(), item) != container->end(); \
 175         }
 176
 177 _BelongHelper(set)
 178 _BelongHelper(vector)
 179 _BelongHelper(list)
 180
 181 /** General set operations */
 182 template<class T>
 183 inline set<T>* Intersect(set<T> *set1, set<T> *set2) {
 184         set<T> *res = new set<T>;
 185         ForEach (item, set1) {
 186                 if (Belong(set2, item))
 187                         res->insert(item);
 188         }
 189         return res;
 190 }
 191
 192 template<class T>
 193 inline set<T>* Union(set<T> *s1, set<T> *s2) {
 194         set<T> *res = new set<T>(*s1);
 195         ForEach (item, s2)
 196                 res->insert(item);
 197         return res;
 198 }
 199
 200 template<class T>
 201 inline set<T>* Subtract(set<T> *set1, set<T> *set2) {
 202         set<T> *res = new set<T>;
 203         ForEach (item, set1) {
 204                 if (!Belong(set2, item))
 205                         res->insert(item);
 206         }
 207         return res;
 208 }
 209
 210 template<class T>
 211 inline void Insert(set<T> *s, T item) { s->insert(item); }
 212
 213 template<class T>
 214 inline void Insert(set<T> *s, set<T> *others) {
 215         ForEach (item, others)
 216                 s->insert(item);
 217 }
 218
 219 /*
 220 inline MethodSet MakeSet(int count, ...) {
 221         va_list ap;
 222         MethodSet res;
 223
 224         va_start (ap, count);
 225         res = NewSet;
 226         for (int i = 0; i < count; i++) {
 227                 Method item = va_arg (ap, Method);
 228                 res->insert(item);
 229         }
 230         va_end (ap);
 231         return res;
 232 }
 233 */
 234
 235 /********** Method call related operations **********/
 236 #define Name(method) method->interfaceName
 237
 238 #define Local(method, field) ((StateStruct*) method->localState)->field
 239
 240 #define Value(method, type, field) ((type*) method->value)->field
 241 #define Ret(method, type) Value(method, type, RET)
 242 #define Arg(method, type, arg) Value(method, type, arg)
 243
 244 #define Prev(method) method->prev
 245 #define PREV _M->prev
 246
 247 #define Next(method) method->next
 248 #define NEXT _M->next
 249
 250 #define Concurrent(method) method->concurrent
 251 #define CONCURRENT  _M->concurrent
 252
 253 // This auto-generated struct can have different fields according to the read
 254 // state declaration. Here it's just a test example
 255 typedef struct StateStruct {
 256         int x;
 257 } StateStruct;
 258
 259 // These auto-generated struct can have different fields according to the return
 260 // value and arguments of the corresponding interface. The struct will have the
 261 // same name as the interface name. Here it's just a test example
 262 typedef struct Store {
 263         int *loc;
 264         int val;
 265 } Store;
 266
 267 typedef struct Load {
 268         int RET;
 269         int *loc;
 270 } Load;
 271
 272 bool f1(Method m) {
 273         return true;
 274 }
 275
 276 int main() {
 277         set<int> *is1 = new set<int>;
 278         set<int> *is2 = new set<int>;
 279
 280         list<int> *il1 = new list<int>;
 281         list<int> *il2 = new list<int>;
 282
 283         il1->push_back(2);
 284         il1->push_back(3);
 285
 286         is1->insert(1);
 287         is1->insert(3);
 288
 289         is2->insert(4);
 290         is2->insert(5);
 291
 292
 293         MethodSet ms = NewSet;
 294         Method m = new MethodCall;
 295         m->interfaceName = "Store";
 296         StateStruct *ss = new StateStruct;
 297         ss->x = 1;
 298         m->localState = ss;
 299         Store *st = new Store;
 300         st->val = 2;
 301         m->value = st;
 302         ms->insert(m);
 303
 304         m = new MethodCall;
 305         m->interfaceName= "Store";
 306         ss = new StateStruct;
 307         ss->x = 2;
 308         m->localState = ss;
 309         st = new Store;
 310         st->val = 0;
 311         m->value = st;
 312         ms->insert(m);
 313
 314         m = new MethodCall;
 315         m->interfaceName= "Load";
 316         ss = new StateStruct;
 317         ss->x = 0;
 318         m->localState = ss;
 319         Load *ld = new Load;
 320         ld->RET = 2;
 321         m->value = ld;
 322         ms->insert(m);
 323
 324         MakeSet(int, ms, newis, LOCAL(x));
 325         cout << "Size=" << Size(newis) << " | val= " << Belong(newis, 2) << endl;
 326         ForEach (i, newis) {
 327                 cout << "elem: " << i << endl;
 328         }
 329
 330
 331         //Subset(ms, sub, NAME == "Store" && VALUE(Store, val) != 0);
 332         //cout << "Size=" << Size(Subset(ms, Guard(NAME == "Store" && ARG(Store, val)
 333                 //>= 0 && LOCAL(x) >= 0 ))) << endl;
 334         return 0;
 335 }