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