string interfaceName; // The interface label name
void *value; // The pointer that points to the struct that have the return
// value and the arguments
- void *localState; // The pointer that points to the struct that represents
- // the (local) state
+ void *state; // The pointer that points to the struct that represents
+ // the state
set<MethodCall*> *prev; // Method calls that are hb right before me
set<MethodCall*> *next; // Method calls that are hb right after me
set<MethodCall*> *concurrent; // Method calls that are concurrent with me
#define X(name) CAT(__##name, __LINE__) /* unique variable */
/**
- The set here is a vector<MethodCall*>* type, or the MethodSet type. And the
- item would become the MethodCall* type, or the Method type
+ This is a generic ForEach primitive for all the containers that support
+ using iterator to iterate.
*/
-#define ForEach1(item, set) \
- int X(i) = 0; \
- for (Method item = (set)->size() > 0 ? (*(set))[0] : NULL; \
- X(i) < (set)->size(); X(i)++, item = X(i) < (set)->size() ? (*(set))[X(i)] : NULL)
-
#define ForEach(item, container) \
auto X(_container) = (container); \
auto X(iter) = X(_container)->begin(); \
for (auto item = *X(iter); X(iter) != X(_container)->end(); item = ((++X(iter)) != \
X(_container)->end()) ? *X(iter) : 0)
-/**
- 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.
+ field) and STATE(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
+ state of the current method, we use STATE(field) (this is a reference
for read/write).
*/
#define ITEM _M
#define NAME Name(_M)
-#define LOCAL(field) Local(_M, field)
+#define STATE(field) State(_M, field)
#define VALUE(type, field) Value(_M, type, field)
#define RET(type) VALUE(type, RET)
/**
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
+ construct an integer set from the 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
+ "readSet", we would call "MakeSet(int, PREV, readSet, STATE(x));". Then users
can use the "readSet" as an integer set (set<int>)
*/
#define MakeSet(type, oldset, newset, field) \
/**
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))"
+ extract the subset of method calls in the PREV set whose state "x" is
+ equal to "val" would be "Subset(PREV, Guard(STATE(x) == val))"
*/
#define Guard(expression) GeneralGuard(Method, expression)
/********** Method call related operations **********/
#define Name(method) method->interfaceName
-#define Local(method, field) ((StateStruct*) method->localState)->field
+#define State(method, field) ((StateStruct*) method->state)->field
#define Value(method, type, field) ((type*) method->value)->field
#define Ret(method, type) Value(method, type, RET)
#define Concurrent(method) method->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
typedef struct StateStruct {
int *loc;
} Load;
-bool f1(Method m) {
- return true;
-}
-
int main() {
set<int> *is1 = new set<int>;
set<int> *is2 = new set<int>;
m->interfaceName = "Store";
StateStruct *ss = new StateStruct;
ss->x = 1;
- m->localState = ss;
+ m->state = ss;
Store *st = new Store;
st->val = 2;
m->value = st;
m->interfaceName= "Store";
ss = new StateStruct;
ss->x = 2;
- m->localState = ss;
+ m->state = ss;
st = new Store;
st->val = 0;
m->value = st;
m->interfaceName= "Load";
ss = new StateStruct;
ss->x = 0;
- m->localState = ss;
+ m->state = ss;
Load *ld = new Load;
ld->RET = 2;
m->value = ld;
ms->insert(m);
- MakeSet(int, ms, newis, LOCAL(x));
+ MakeSet(int, ms, newis, STATE(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;
+ //>= 0 && STATE(x) >= 0 ))) << endl;
return 0;
}
projects / cdsspec-compiler.git / blobdiff