edits

diff --git a/notes/definition.cc b/notes/definition.cc
index 457b6094cfbe5ce6c16d8adb6db729944c9759b4..054ff89afe8b4e3d91b18900ab3a836debde9d7d 100644 (file)
--- a/notes/definition.cc
+++ b/notes/definition.cc
@@ -6,6 +6,8 @@
 #include <algorithm>
 #include <set>
 
 #include <algorithm>
 #include <set>
 

+#include <functional>
+

 #include <stdarg.h>
 
 using namespace std;
 #include <stdarg.h>
 
 using namespace std;


@@ -55,6 +57,19 @@ typedef set<int> IntSet;
        The subset operation is only for the MethodCall set
 */
 
        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 _M ME
 
 #define NAME Name(_M)


@@ -62,7 +77,10 @@ typedef set<int> IntSet;
 #define LOCAL(field) Local(_M, field)
 
 #define VALUE(type, field) Value(_M, type, field)
 #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; \
 #define Subset(s, subset, condition) \
        MethodSet original = s; \
        MethodSet subset = NewSet; \


@@ -70,6 +88,81 @@ typedef set<int> IntSet;
                if ((condition)) \
                        subset->insert(_M); \
        } \
                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())
 
 /** General for set, list & vector */
 #define Size(container) ((container)->size())


@@ -123,6 +216,7 @@ inline void Insert(set<T> *s, set<T> *others) {
                s->insert(item);
 }
 
                s->insert(item);
 }
 

+/*

 inline MethodSet MakeSet(int count, ...) {
        va_list ap;
        MethodSet res;
 inline MethodSet MakeSet(int count, ...) {
        va_list ap;
        MethodSet res;


@@ -136,6 +230,7 @@ inline MethodSet MakeSet(int count, ...) {
        va_end (ap);
        return res;
 }
        va_end (ap);
        return res;
 }

+*/

 
 /********** Method call related operations **********/
 #define Name(method) method->interfaceName
 
 /********** Method call related operations **********/
 #define Name(method) method->interfaceName


@@ -143,15 +238,17 @@ inline MethodSet MakeSet(int count, ...) {
 #define Local(method, field) ((StateStruct*) method->localState)->field
 
 #define Value(method, type, field) ((type*) method->value)->field
 #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(method) method->prev

-#define PREV ME->prev
+#define PREV _M->prev

 
 #define Next(method) method->next
 
 #define Next(method) method->next

-#define NEXT ME->next
+#define NEXT _M->next

 
 #define Concurrent(method) method->concurrent
 
 #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
 
 // This auto-generated struct can have different fields according to the read
 // state declaration. Here it's just a test example


@@ -172,6 +269,10 @@ typedef struct Load {
        int *loc;
 } Load;
 
        int *loc;
 } Load;
 

+bool f1(Method m) {
+       return true;
+}
+

 int main() {
        set<int> *is1 = new set<int>;
        set<int> *is2 = new set<int>;
 int main() {
        set<int> *is1 = new set<int>;
        set<int> *is2 = new set<int>;


@@ -219,10 +320,16 @@ int main() {
        ld->RET = 2;
        m->value = ld;
        ms->insert(m);
        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;
 }
        return 0;
 }

diff --git a/notes/nondeterm-spec.txt b/notes/nondeterm-spec.txt
index e6dfb057017406083b79491b2aa0fff21693f634..8dca63c150e5efe831f2b5b35d5e175a32aac9f9 100644 (file)
--- a/notes/nondeterm-spec.txt
+++ b/notes/nondeterm-spec.txt
@@ -161,8 +161,7 @@ void store(int *loc, int val);
 
 @Interface: Load
 @PreCondition:
 
 @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);
 
 @SideEffect: LOCAL(x) = RET;
 int load(int *loc);
 


@@ -214,21 +213,8 @@ interface label name.
 
 
 *********************************************
 
 
 *********************************************

-
-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()
 
 // 1.2 Size(set) --> to get the size of a method set
 #define Size(set) set->size()


@@ -284,6 +270,11 @@ inline MethodSet Subtract(MethodSet set1, MethodSet set2) {
 
 // 3. Value(method, type, field)
 #define Value(method, type, field) ((type*) method->value)->field
 
 // 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
 
 // 4. Name(mehtod)
 #defien Lable(method) method->interfaceName


@@ -312,10 +303,9 @@ void store(int *loc, int val);
        // Auto generated code
        // MethodCall *ME = ((SomeTypeConversion) info)->method;
        
        // 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);
 
 @SideEffect: LOCAL(x) = RET;
 int load(int *loc);
 


@@ -359,9 +349,8 @@ void enq(queue_t *q, int val);
                // Otherwise check there must be other concurrent dequeuers
                ForEach (item, Local(q)) {
                        // Check there's some concurrent dequeuer for this item
                // 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
                }
                return true;
        } else { // Check the global queue state