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 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         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 = NewSet; \
  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 sublist operation that takes a condition and returns all the item
 132         for which the boolean guard holds in the same order as in the old list.
 133 */
 134 template <class T>
 135 inline list<T>* Sublist(list<T> *original, std::function<bool(T)> condition) {
 136         list<T> *res = new list<T>;
 137         ForEach (_M, original) {
 138                 if (condition(_M))
 139                         res->push_back(_M);
 140         }
 141         return res;
 142 }
 143
 144 /**
 145         A general subvector operation that takes a condition and returns all the item
 146         for which the boolean guard holds in the same order as in the old vector.
 147 */
 148 template <class T>
 149 inline vector<T>* Subvector(vector<T> *original, std::function<bool(T)> condition) {
 150         vector<T> *res = new vector<T>;
 151         ForEach (_M, original) {
 152                 if (condition(_M))
 153                         res->push_back(_M);
 154         }
 155         return res;
 156 }
 157
 158 /** General for set, list & vector */
 159 #define Size(container) ((container)->size())
 160
 161 #define _BelongHelper(type) \
 162         template<class T> \
 163         inline bool Belong(type<T> *container, T item) { \
 164                 return std::find(container->begin(), \
 165                         container->end(), item) != container->end(); \
 166         }
 167
 168 _BelongHelper(set)
 169 _BelongHelper(vector)
 170 _BelongHelper(list)
 171
 172 /** General set operations */
 173 template<class T>
 174 inline set<T>* Intersect(set<T> *set1, set<T> *set2) {
 175         set<T> *res = new set<T>;
 176         ForEach (item, set1) {
 177                 if (Belong(set2, item))
 178                         res->insert(item);
 179         }
 180         return res;
 181 }
 182
 183 template<class T>
 184 inline set<T>* Union(set<T> *s1, set<T> *s2) {
 185         set<T> *res = new set<T>(*s1);
 186         ForEach (item, s2)
 187                 res->insert(item);
 188         return res;
 189 }
 190
 191 template<class T>
 192 inline set<T>* Subtract(set<T> *set1, set<T> *set2) {
 193         set<T> *res = new set<T>;
 194         ForEach (item, set1) {
 195                 if (!Belong(set2, item))
 196                         res->insert(item);
 197         }
 198         return res;
 199 }
 200
 201 template<class T>
 202 inline void Insert(set<T> *s, T item) { s->insert(item); }
 203
 204 template<class T>
 205 inline void Insert(set<T> *s, set<T> *others) {
 206         ForEach (item, others)
 207                 s->insert(item);
 208 }
 209
 210 /*
 211 inline MethodSet MakeSet(int count, ...) {
 212         va_list ap;
 213         MethodSet res;
 214
 215         va_start (ap, count);
 216         res = NewSet;
 217         for (int i = 0; i < count; i++) {
 218                 Method item = va_arg (ap, Method);
 219                 res->insert(item);
 220         }
 221         va_end (ap);
 222         return res;
 223 }
 224 */
 225
 226 /********** Method call related operations **********/
 227 #define Name(method) method->interfaceName
 228
 229 #define State(method, field) ((StateStruct*) method->state)->field
 230
 231 #define Value(method, type, field) ((type*) method->value)->field
 232 #define Ret(method, type) Value(method, type, RET)
 233 #define Arg(method, type, arg) Value(method, type, arg)
 234
 235 #define Prev(method) method->prev
 236 #define PREV _M->prev
 237
 238 #define Next(method) method->next
 239 #define NEXT _M->next
 240
 241 #define Concurrent(method) method->concurrent
 242 #define CONCURRENT  _M->concurrent
 243
 244
 245 /***************************************************************************/
 246 /***************************************************************************/
 247
 248 // This auto-generated struct can have different fields according to the read
 249 // state declaration. Here it's just a test example
 250 typedef struct StateStruct {
 251         int x;
 252 } StateStruct;
 253
 254 // These auto-generated struct can have different fields according to the return
 255 // value and arguments of the corresponding interface. The struct will have the
 256 // same name as the interface name. Here it's just a test example
 257 typedef struct Store {
 258         int *loc;
 259         int val;
 260 } Store;
 261
 262 typedef struct Load {
 263         int RET;
 264         int *loc;
 265 } Load;
 266
 267 int main() {
 268         set<int> *is1 = new set<int>;
 269         set<int> *is2 = new set<int>;
 270
 271         list<int> *il1 = new list<int>;
 272         list<int> *il2 = new list<int>;
 273
 274         il1->push_back(2);
 275         il1->push_back(3);
 276
 277         is1->insert(1);
 278         is1->insert(3);
 279
 280         is2->insert(4);
 281         is2->insert(5);
 282
 283
 284         MethodSet ms = NewSet;
 285         Method m = new MethodCall;
 286         m->interfaceName = "Store";
 287         StateStruct *ss = new StateStruct;
 288         ss->x = 1;
 289         m->state = ss;
 290         Store *st = new Store;
 291         st->val = 2;
 292         m->value = st;
 293         ms->insert(m);
 294
 295         m = new MethodCall;
 296         m->interfaceName= "Store";
 297         ss = new StateStruct;
 298         ss->x = 2;
 299         m->state = ss;
 300         st = new Store;
 301         st->val = 0;
 302         m->value = st;
 303         ms->insert(m);
 304
 305         m = new MethodCall;
 306         m->interfaceName= "Load";
 307         ss = new StateStruct;
 308         ss->x = 0;
 309         m->state = ss;
 310         Load *ld = new Load;
 311         ld->RET = 2;
 312         m->value = ld;
 313         ms->insert(m);
 314
 315         MakeSet(int, ms, newis, STATE(x));
 316         cout << "Size=" << Size(newis) << " | val= " << Belong(newis, 2) << endl;
 317         ForEach (i, newis) {
 318                 cout << "elem: " << i << endl;
 319         }
 320
 321
 322         //Subset(ms, sub, NAME == "Store" && VALUE(Store, val) != 0);
 323         //cout << "Size=" << Size(Subset(ms, Guard(NAME == "Store" && ARG(Store, val)
 324                 //>= 0 && STATE(x) >= 0 ))) << endl;
 325         return 0;
 326 }