From: Peizhao Ou Date: Sat, 30 Jan 2016 06:47:34 +0000 (-0800) Subject: edits X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=189207ea1c47667cd77bcd5a41b37ff023a48315;hp=29c06628ef41f45b117aef06330aca37554b65d1 edits --- diff --git a/notes/definition.cc b/notes/definition.cc index bcc01e7..0c5b796 100644 --- a/notes/definition.cc +++ b/notes/definition.cc @@ -32,7 +32,7 @@ typedef set IntSet; /********** More general specification-related types and operations **********/ -#define NewSet new set +#define NewMethodSet new set #define CAT(a, b) CAT_HELPER(a, b) /* Concatenate two symbols for macros! */ #define CAT_HELPER(a, b) a ## b @@ -74,7 +74,7 @@ typedef set IntSet; /* #define Subset(s, subset, condition) \ MethodSet original = s; \ - MethodSet subset = NewSet; \ + MethodSet subset = NewMethodSet; \ ForEach (_M, original) { \ if ((condition)) \ subset->insert(_M); \ @@ -213,7 +213,7 @@ inline MethodSet MakeSet(int count, ...) { 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); @@ -281,7 +281,7 @@ int main() { is2->insert(5); - MethodSet ms = NewSet; + MethodSet ms = NewMethodSet; Method m = new MethodCall; m->interfaceName = "Store"; StateStruct *ss = new StateStruct; diff --git a/notes/nondeterm-spec.txt b/notes/nondeterm-spec.txt index e594157..d1011dc 100644 --- a/notes/nondeterm-spec.txt +++ b/notes/nondeterm-spec.txt @@ -93,13 +93,113 @@ IV. Examples 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*) + +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 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). 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 *prev; // Method calls that are hb right before me set *concurrent; // Method calls that are concurrent with me set *next; // Method calls that are hb right after me