/********** More general specification-related types and operations **********/
-#define NewSet new set<Method>
+#define NewMethodSet new set<Method>
#define CAT(a, b) CAT_HELPER(a, b) /* Concatenate two symbols for macros! */
#define CAT_HELPER(a, b) a ## b
/*
#define Subset(s, subset, condition) \
MethodSet original = s; \
- MethodSet subset = NewSet; \
+ MethodSet subset = NewMethodSet; \
ForEach (_M, original) { \
if ((condition)) \
subset->insert(_M); \
MethodSet res;
va_start (ap, count);
- res = NewSet;
+ res = NewMethodSet;
for (int i = 0; i < count; i++) {
Method item = va_arg (ap, Method);
res->insert(item);
is2->insert(5);
- MethodSet ms = NewSet;
+ MethodSet ms = NewMethodSet;
Method m = new MethodCall;
m->interfaceName = "Store";
StateStruct *ss = new StateStruct;
We define a struct called MethodCall to represent the data we would collect and
communicate between the real execution and the checking process.
+
+STATE(field) // A primitive to access the current state in the interface
+ // specification by the name of the field. We can use this as a
+ // lvalue & rvalue ==> "STATE(x) = 1" and "int i = STATE(x)" are
+ // both okay
+
+ // This can also be used to refer to the state of a method item
+ // in the Subset operation (see Subset)
+
+NAME // Used to refer to the name of a method item in the Subset
+ // operation (see Subset)
+
+RET(type) // Used to refer to the return value of a method item in the
+ // Subset operation (see Subset)
+
+ARG(type, arg) // Used to refer to the argument of a method item in the
+ // Subset operation (see Subset)
+
+
+PREV // Represent the set of previous method calls of the current method
+ // call
+
+CONCURRENT // Represent the set of concurrent method calls of the current
+ // method call
+
+NEXT // Represent the set of next method calls of the current method
+ // call
+
+Name(method) // The interface label name of the specific method
+
+State(method, field) // A primitive to access a specific state field of a
+ // specific method. Also used as lvalue and rvalue
+
+Ret(method, type) // The return value of the specific method; type should
+ // be the name of the interface label
+
+Arg(method, type, arg) // The arguement by name of the specific method; type should
+ // be the name of the interface label, and arg should be
+ // the name of the argument
+
+Prev(method) // Represent the set of previous method calls of the
+ // specific method call
+
+Next(method) // Represent the set of next method calls of the specific
+ // method call
+
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+ForEach(item, container) { ... } // Useful iteration primitive
+
+NewMethodSet // Create a new method set (set<MethodCall*>*)
+
+MakeSet(NewSetType, oldset, newset, field); //
+
+Subset(set, condition) // A generic subset operation that takes a condition and
+ // returns all the item for which the boolean guard
+ // holds. The condition can be specified with GUARD or
+ // GeneralGuard shown as follow.
+
+ITEM // Used to refer to the set item in the GeneralGuard shown below
+
+GeneralGuard(type, expression) // Used as a condition for any set<T> type. We
+ // use "ITEM" to refer to a set item. For
+ // example, a subset of positive elements on an
+ // IntSet "s" would be
+ // "Subset(s, GeneralGuard(int, ITEM > 0))"
+
+Guard(expression) // Used specifically for MethodSet(set<MethodCall*>). An
+ // example to extract the subset of method calls in the PREV
+ // set that is a "Store" method and whose state "x" is equal
+ // to "val" and the return value is 5 would be
+ // "Subset(PREV, Guard(STATE(x) == val && NAME == "Store" &&
+ // RET(Store) == 5))"
+
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+
+
+To make things easier, we have the following helper macros.
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+/**
+ 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 CAT(a, b) CAT_HELPER(a, b) /* Concatenate two symbols for macros! */
+#define CAT_HELPER(a, b) a ## b
+#define X(name) CAT(__##name, __LINE__) /* unique variable */
+
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+
*****************************************************************************
typedef struct MethodCall {
string name; // The interface label name
void *value; // The pointer that points to the struct that have the return
// value and the arguments
void *state; // The pointer that points to the struct that represents
- // the (local) state
+ // the state
set<MethodCall*> *prev; // Method calls that are hb right before me
set<MethodCall*> *concurrent; // Method calls that are concurrent with me
set<MethodCall*> *next; // Method calls that are hb right after me
projects / cdsspec-compiler.git / commitdiff