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