#include <algorithm>
#include <set>
+#include <functional>
+
#include <stdarg.h>
using namespace std;
The subset operation is only for the MethodCall set
*/
+/**
+ This is a common macro that is used as a constant for the name of specific
+ variables. We basically have two usage scenario:
+ 1. In Subset operation, we allow users to specify a condition to extract a
+ subset. In that condition expression, we provide NAME, RET(type), ARG(type,
+ field) and LOCAL(field) to access each item's (method call) information.
+ 2. In general specification (in pre- & post- conditions and side effects),
+ we would automatically generate an assignment that assign the current
+ MethodCall* pointer to a variable namedd _M. With this, when we access the
+ local state of the current method, we use LOCAL(field) (this is a reference
+ for read/write).
+*/
+#define ITEM _M
#define _M ME
#define NAME Name(_M)
#define LOCAL(field) Local(_M, field)
#define VALUE(type, field) Value(_M, type, field)
+#define RET(type) VALUE(type, RET)
+#define ARG(type, arg) VALUE(type, arg)
+/*
#define Subset(s, subset, condition) \
MethodSet original = s; \
MethodSet subset = NewSet; \
if ((condition)) \
subset->insert(_M); \
} \
+*/
+
+
+/**
+ This operation is specifically for Method set. For example, when we want to
+ construct an integer set from the local state field "x" (which is an
+ integer) of the previous set of method calls (PREV), and the new set goes to
+ "readSet", we would call "MakeSet(int, PREV, readSet, LOCAL(x));". Then users
+ can use the "readSet" as an integer set (set<int>)
+*/
+#define MakeSet(type, oldset, newset, field) \
+ auto newset = new set<type>; \
+ ForEach (_M, oldset) \
+ newset->insert(field); \
+
+/**
+ We provide a more general subset operation that takes a plain boolean
+ expression on each item (access by the name "ITEM") of the set, and put it
+ into a new set if the boolean expression (Guard) on that item holds. This is
+ used as the second arguments of the Subset operation. An example to extract
+ a subset of positive elements on an IntSet "s" would be "Subset(s,
+ GeneralGuard(int, ITEM > 0))"
+*/
+#define GeneralGuard(type, expression) std::function<bool(type)> ( \
+ [](type ITEM) -> bool { return (expression);}) \
+
+/**
+ This is a more specific guard designed for the Method (MethodCall*). It
+ basically wrap around the GeneralGuard with the type Method. An example to
+ extract the subset of method calls in the PREV set whose local state "x" is
+ equal to "val" would be "Subset(PREV, Guard(Local(x) == val))"
+*/
+#define Guard(expression) GeneralGuard(Method, expression)
+
+/**
+ A general subset operation that takes a condition and returns all the item
+ for which the boolean guard holds.
+*/
+template <class T>
+inline set<T>* Subset(set<T> *original, std::function<bool(T)> condition) {
+ set<T> *res = new set<T>;
+ ForEach (_M, original) {
+ if (condition(_M))
+ res->insert(_M);
+ }
+ return res;
+}
+
+/**
+ A general sublist operation that takes a condition and returns all the item
+ for which the boolean guard holds in the same order as in the old list.
+*/
+template <class T>
+inline list<T>* Sublist(list<T> *original, std::function<bool(T)> condition) {
+ list<T> *res = new list<T>;
+ ForEach (_M, original) {
+ if (condition(_M))
+ res->push_back(_M);
+ }
+ return res;
+}
+
+/**
+ A general subvector operation that takes a condition and returns all the item
+ for which the boolean guard holds in the same order as in the old vector.
+*/
+template <class T>
+inline vector<T>* Subvector(vector<T> *original, std::function<bool(T)> condition) {
+ vector<T> *res = new vector<T>;
+ ForEach (_M, original) {
+ if (condition(_M))
+ res->push_back(_M);
+ }
+ return res;
+}
/** General for set, list & vector */
#define Size(container) ((container)->size())
s->insert(item);
}
+/*
inline MethodSet MakeSet(int count, ...) {
va_list ap;
MethodSet res;
va_end (ap);
return res;
}
+*/
/********** Method call related operations **********/
#define Name(method) method->interfaceName
#define Local(method, field) ((StateStruct*) method->localState)->field
#define Value(method, type, field) ((type*) method->value)->field
+#define Ret(method, type) Value(method, type, RET)
+#define Arg(method, type, arg) Value(method, type, arg)
#define Prev(method) method->prev
-#define PREV ME->prev
+#define PREV _M->prev
#define Next(method) method->next
-#define NEXT ME->next
+#define NEXT _M->next
#define Concurrent(method) method->concurrent
-#define CONCURRENT ME->concurrent
+#define CONCURRENT _M->concurrent
// This auto-generated struct can have different fields according to the read
// state declaration. Here it's just a test example
int *loc;
} Load;
+bool f1(Method m) {
+ return true;
+}
+
int main() {
set<int> *is1 = new set<int>;
set<int> *is2 = new set<int>;
ld->RET = 2;
m->value = ld;
ms->insert(m);
-
- //Subset(ms, sub, NAME == "Store" && VALUE(Store, val) != 0);
- Subset(ms, sub, NAME == "Store" && VALUE(Store, val) >= 0 && LOCAL(x) == 0);
- cout << "Size=" << Size(sub) << endl;
+ MakeSet(int, ms, newis, LOCAL(x));
+ cout << "Size=" << Size(newis) << " | val= " << Belong(newis, 2) << endl;
+ ForEach (i, newis) {
+ cout << "elem: " << i << endl;
+ }
+
+
+ //Subset(ms, sub, NAME == "Store" && VALUE(Store, val) != 0);
+ //cout << "Size=" << Size(Subset(ms, Guard(NAME == "Store" && ARG(Store, val)
+ //>= 0 && LOCAL(x) >= 0 ))) << endl;
return 0;
}
@Interface: Load
@PreCondition:
- Subset(PREV, subset, LOCAL(x) == RET);
- return Size(subset) > 0;
+ Size(Subset(PREV, LOCAL(x) == RET)) > 0;
@SideEffect: LOCAL(x) = RET;
int load(int *loc);
*********************************************
-
-TODO:We want subset operation by the equality and inequality of the interface
-name, a specific (or combined) state and a specific (or combined) of the value
-(RET & arguments)
-
-// 1.1 Subset(set, name) --> to get a subset of method calls by name
-inline vector<MethodCall*>* Subset(vector<MethodCall*> *set, string name) {
- vector<MethodCall*> _subset = new vector<MethodCall*>;
- for (int i = 0; i < set->size(); i++) {
- MethodCall *_m = (*set)[i];
- if (_m->interfaceName == name)
- _subset->push_back(_m);
- }
- return _subset;
-}
+// 1.1 Subset(set, guard) --> to get a subset of method calls by a boolean
+// expression; This takes advantage of C++11 std::function features and C macros.
// 1.2 Size(set) --> to get the size of a method set
#define Size(set) set->size()
// 3. Value(method, type, field)
#define Value(method, type, field) ((type*) method->value)->field
+3.1 Return
+#define Ret(method, type) Value(method, type, RET)
+3.2 Arguments
+#define Arg(method, type, arg) Value(method, type, arg)
+
// 4. Name(mehtod)
#defien Lable(method) method->interfaceName
// Auto generated code
// MethodCall *ME = ((SomeTypeConversion) info)->method;
- Subset(Prev, readSet1, LOCAL(x) == RET);
- if (Size(readSet1) > 0) return true;
- Subset(Concurrent, readSet2, NAME == "Store" && VALUE(Store, val) == RET);
- return Size(readSet2) > 0;
+ int count = Size(Subset(Prev, LOCAL(x) == RET))
+ + Size(Subset(CONCURRENT, NAME == "Store" && ARG(Store, val) == RET))
+ return count > 0;
@SideEffect: LOCAL(x) = RET;
int load(int *loc);
// Otherwise check there must be other concurrent dequeuers
ForEach (item, Local(q)) {
// Check there's some concurrent dequeuer for this item
- Subset(CONCURRENT, concurSet, NAME == "Deq" && VALUE(Deq, RET) &&
- *VALUE(Deq, res) == item);
- if (Size(concurSet) == 0) return false;
+ if (Size(Subset(CONCURRENT, NAME == "Deq" && RET(Deq) &&
+ *ARG(Deq, res) == item)) == 0) return false;
}
return true;
} else { // Check the global queue state