source: libcfa/src/containers/list.hfa @ 856fe3e

ADTarm-ehast-experimentalenumforall-pointer-decayjacob/cs343-translationnew-astnew-ast-unique-exprpthread-emulationqualifiedEnum
Last change on this file since 856fe3e was 4d741e9, checked in by Michael Brooks <mlbrooks@…>, 4 years ago

Strengthened test and fixed a bug on dlist.

The test acceptance criteria are now stricter with white- and black-box checks added. New white-box checking, borrowed from alarm's linked-list verify ensures that headed lists reach last when traversed starting from first, and vice-versa. New black-box checking ensures the link from an ending element to the head sentinel is intact.

The bug was that element insertion at an end of a headed list broke the new black-box criterion. The new white-box criterion was never violated in the current test cases, but early work at integrating this list with the alarm system exercised such a break.

Both checks behind the new test criteria are packaged as a verify routine for user code to invoke.
  • Property mode set to 100644
File size: 9.3 KB
Line 
1//
2// Cforall Version 1.0.0 Copyright (C) 2020 University of Waterloo
3//
4// The contents of this file are covered under the licence agreement in the
5// file "LICENCE" distributed with Cforall.
6//
7// list -- lets a user-defined stuct form intrusive linked lists
8//
9// Author           : Michael Brooks
10// Created On       : Wed Apr 22 18:00:00 2020
11// Last Modified By : Michael Brooks
12// Last Modified On : Wed Apr 22 18:00:00 2020
13// Update Count     : 1
14//
15
16#include <assert.h>
17
18#define __DLISTED_MGD_COMMON(ELEM, NODE, LINKS_FLD) \
19static inline ELEM& $tempcv_n2e(NODE &node) { \
20        return node; \
21} \
22\
23static inline NODE& $tempcv_e2n(ELEM &node) { \
24        return node; \
25} \
26\
27static inline ELEM & ?`prev(NODE &node) { \
28    $dlinks(ELEM) & ls = node.LINKS_FLD; \
29        $mgd_link(ELEM) * l = &ls.prev; \
30        ELEM * e = l->elem; \
31        return *e; \
32} \
33\
34static inline ELEM & ?`next(NODE &node) { \
35    $dlinks(ELEM) & ls = node.LINKS_FLD; \
36        $mgd_link(ELEM) * l = &ls.next; \
37        ELEM * e = l->elem; \
38        return *e; \
39} \
40\
41static inline $mgd_link(ELEM) & $prev_link(NODE &node) { \
42    $dlinks(ELEM) & ls = node.LINKS_FLD; \
43        $mgd_link(ELEM) * l = &ls.prev; \
44        return *l; \
45} \
46\
47static inline $mgd_link(ELEM) & $next_link(NODE &node) { \
48    $dlinks(ELEM) & ls = node.LINKS_FLD; \
49        $mgd_link(ELEM) * l = &ls.next; \
50        return *l; \
51}
52
53#define __DLISTED_MGD_JUSTEXPL(STRUCT, IN_THELIST, STRUCT_IN_THELIST) \
54struct STRUCT_IN_THELIST { \
55        inline STRUCT; \
56}; \
57\
58void ?{}(STRUCT_IN_THELIST &) = void; \
59\
60static inline STRUCT_IN_THELIST& ?`IN_THELIST(STRUCT &this) { \
61        return (STRUCT_IN_THELIST&)this; \
62}
63
64#define __DLISTED_MGD_JUSTIMPL(STRUCT)
65
66forall( dtype tE ) {
67        struct $mgd_link {
68                tE *elem;
69                void *terminator;
70                _Bool is_terminator;
71                // will collapse to single pointer with tag bit
72        };
73        static inline void ?{}( $mgd_link(tE) &this, tE* elem ) {
74                (this.elem){ elem };
75                (this.terminator){ 0p };
76                (this.is_terminator){ 0 };
77        }
78        static inline void ?{}( $mgd_link(tE) &this, void * terminator ) {
79                (this.elem){ 0p };
80                (this.terminator){ terminator };
81                (this.is_terminator){ 1 };
82        }
83        forall ( otype tInit | { void ?{}( $mgd_link(tE) &, tInit); } )
84        static inline void ?=?( $mgd_link(tE) &this, tInit i ) {
85                ^?{}( this );
86                ?{}( this, i );
87        }
88        struct $dlinks {
89                // containing item is not listed
90                // iff
91                // links have (elem == 0p && terminator == 0p)
92                $mgd_link(tE) next;
93                $mgd_link(tE) prev;
94        };
95        static inline void ?{}( $dlinks(tE) &this ) {
96                (this.next){ (tE *)0p };
97                (this.prev){ (tE *)0p };
98        }
99}
100
101#define DLISTED_MGD_EXPL_IN(STRUCT, LIST_SUF) \
102  $dlinks(STRUCT) $links_ ## LIST_SUF;
103
104#define DLISTED_MGD_EXPL_OUT(STRUCT, LIST_SUF) \
105  __DLISTED_MGD_JUSTEXPL(STRUCT, in_##LIST_SUF, STRUCT ## _in_ ## LIST_SUF) \
106  __DLISTED_MGD_COMMON(STRUCT, STRUCT##_in_##LIST_SUF,  $links_ ## LIST_SUF)
107
108#define DLISTED_MGD_IMPL_IN(STRUCT) \
109  $dlinks(STRUCT) $links;
110
111#define DLISTED_MGD_IMPL_OUT(STRUCT) \
112  __DLISTED_MGD_JUSTIMPL(STRUCT) \
113  __DLISTED_MGD_COMMON(STRUCT, STRUCT, $links)
114
115trait $dlistable(dtype Tnode, dtype Telem) {
116        $mgd_link(Telem) & $prev_link(Tnode &);
117        $mgd_link(Telem) & $next_link(Tnode &);
118        Telem& $tempcv_n2e(Tnode &);
119        Tnode& $tempcv_e2n(Telem &);
120};
121
122forall (dtype Tnode, dtype Telem | $dlistable(Tnode, Telem)) {
123
124        // implemented as a sentinel item in an underlying cicrular list
125        // theList.$links.next is first
126        // theList.$links.prev is last
127        // note this allocation preserves prev-next composition as an identity
128        struct dlist {
129                $dlinks(Telem) $links;
130        };
131
132        // an empty dlist
133        // links refer to self, making a tight circle
134        static inline void ?{}( dlist(Tnode, Telem) & this ) {
135                $mgd_link(Telem) selfRef = (void *) &this;
136                ( this.$links ) { selfRef, selfRef };
137        }
138
139        static inline Telem & ?`first( dlist(Tnode, Telem) &l ) {
140                return * l.$links.next.elem;
141        }
142
143        static inline Telem & ?`last( dlist(Tnode, Telem) &l ) {
144                return * l.$links.prev.elem;
145        }
146
147        #if !defined(NDEBUG) && (defined(__CFA_DEBUG__) || defined(__CFA_VERIFY__))
148        static bool $validate_fwd( dlist(Tnode, Telem) & this ) {
149                Tnode * it = & $tempcv_e2n( this`first );
150                if (!it) return (& this`last == 0p);
151
152                while( $next_link(*it).elem ) {
153                        it = & $tempcv_e2n( * $next_link(*it).elem );
154                }
155
156                return ( it == & $tempcv_e2n( this`last ) ) &&
157                           ( $next_link(*it).is_terminator ) &&
158                           ( ((dlist(Tnode, Telem)*)$next_link(*it).terminator) == &this );
159        }
160        static bool $validate_rev( dlist(Tnode, Telem) & this ) {
161                Tnode * it = & $tempcv_e2n( this`last );
162                if (!it) return (& this`first == 0p);
163
164                while( $prev_link(*it).elem ) {
165                        it = & $tempcv_e2n( * $prev_link(*it).elem );
166                }
167
168                return ( it == & $tempcv_e2n( this`first ) ) &&
169                           ( $prev_link(*it).is_terminator ) &&
170                           ( ((dlist(Tnode, Telem)*)$prev_link(*it).terminator) == &this );
171        }
172        static bool validate( dlist(Tnode, Telem) & this ) {
173                return $validate_fwd(this) && $validate_rev(this);
174        }
175        #endif
176
177        static inline void insert_after(Tnode &list_pos, Telem &to_insert) {
178                assert (&list_pos != 0p);
179                assert (&to_insert != 0p);
180                Tnode &singleton_to_insert = $tempcv_e2n(to_insert);
181                assert($prev_link(singleton_to_insert).elem == 0p);
182                assert($next_link(singleton_to_insert).elem == 0p);
183                $prev_link(singleton_to_insert) = & $tempcv_n2e(list_pos);
184                $next_link(singleton_to_insert) = $next_link(list_pos);
185                if ($next_link(list_pos).is_terminator) {
186                        dlist(Tnode, Telem) *list = $next_link(list_pos).terminator;
187                        $dlinks(Telem) *list_links = & list->$links;
188                        $mgd_link(Telem) *list_last = & list_links->prev;
189                        *list_last = &to_insert;
190                } else {
191                        Telem *list_pos_next = $next_link(list_pos).elem;
192                        if (list_pos_next) {
193                                Tnode & lpn_inlist = $tempcv_e2n(*list_pos_next);
194                                $prev_link(lpn_inlist) = &to_insert;
195                        }
196                }
197                $next_link(list_pos) = &to_insert;
198        }
199
200        static inline void insert_before(Tnode &list_pos, Telem &to_insert) {
201                assert (&list_pos != 0p);
202                assert (&to_insert != 0p);
203                Tnode &singleton_to_insert = $tempcv_e2n(to_insert);
204                assert($prev_link(singleton_to_insert).elem == 0p);
205                assert($next_link(singleton_to_insert).elem == 0p);
206                $next_link(singleton_to_insert) = & $tempcv_n2e(list_pos);
207                $prev_link(singleton_to_insert) = $prev_link(list_pos);
208                if ($prev_link(list_pos).is_terminator) {
209                        dlist(Tnode, Telem) *list = $prev_link(list_pos).terminator;
210                        $dlinks(Telem) *list_links = & list->$links;
211                        $mgd_link(Telem) *list_first = & list_links->next;
212                        *list_first = &to_insert;
213                } else {
214                        Telem *list_pos_prev = $prev_link(list_pos).elem;
215                        if (list_pos_prev) {
216                                Tnode & lpp_inlist = $tempcv_e2n(*list_pos_prev);
217                                $next_link(lpp_inlist) = &to_insert;
218                        }
219                }
220                $prev_link(list_pos) = &to_insert;
221        }
222
223    static inline void insert_first(dlist(Tnode, Telem) &list, Telem &to_insert) {
224                assert (&list != 0p);
225                assert (&to_insert != 0p);
226                Tnode &singleton_to_insert = $tempcv_e2n(to_insert);
227                assert($prev_link(singleton_to_insert).elem == 0p);
228                assert($next_link(singleton_to_insert).elem == 0p);
229
230                $prev_link(singleton_to_insert) = (void*) &list;
231                $next_link(singleton_to_insert) = list.$links.next;
232
233                $dlinks(Telem) *listLinks = & list.$links;
234                if (listLinks->next.is_terminator) {
235                        $mgd_link(Telem) * listPrevReference = & listLinks->prev;
236                        *listPrevReference = &to_insert;
237                } else {
238                        Tnode & next_inlist = $tempcv_e2n(*list.$links.next.elem);
239                        $prev_link(next_inlist) = &to_insert;
240                }
241                $mgd_link(Telem) * listNextReference = & listLinks->next;
242                *listNextReference = &to_insert;
243        }
244
245    static inline void insert_last(dlist(Tnode, Telem) &list, Telem &to_insert) {
246                assert (&list != 0p);
247                assert (&to_insert != 0p);
248                Tnode &singleton_to_insert = $tempcv_e2n(to_insert);
249                assert($next_link(singleton_to_insert).elem == 0p);
250                assert($prev_link(singleton_to_insert).elem == 0p);
251
252                $next_link(singleton_to_insert) = (void*) &list;
253                $prev_link(singleton_to_insert) = list.$links.prev;
254
255                $dlinks(Telem) *listLinks = & list.$links;
256                if (listLinks->prev.is_terminator) {
257                        $mgd_link(Telem) * listNextReference = & listLinks->next;
258                        *listNextReference = &to_insert;
259                } else {
260                        Tnode & prev_inlist = $tempcv_e2n(*list.$links.prev.elem);
261                        $next_link(prev_inlist) = &to_insert;
262                }
263                $mgd_link(Telem) * listPrevReference = & listLinks->prev;
264                *listPrevReference = &to_insert;
265        }
266
267    static inline void remove(Tnode &list_pos) {
268                assert( &list_pos != 0p );
269
270                $mgd_link(Telem) &incoming_from_prev = *0p;
271                $mgd_link(Telem) &incoming_from_next = *0p;
272
273                if ( $prev_link(list_pos).is_terminator ) {
274                        dlist(Tnode, Telem) * tgt_before = $prev_link(list_pos).terminator;
275                        $dlinks(Telem) * links_before = & tgt_before->$links;
276                        &incoming_from_prev = & links_before->next;
277                } else if ($prev_link(list_pos).elem) {
278                        Telem * tgt_before = $prev_link(list_pos).elem;
279                        Tnode & list_pos_before = $tempcv_e2n(*tgt_before);
280                        &incoming_from_prev = & $next_link(list_pos_before);
281                }
282
283                if ( $next_link(list_pos).is_terminator ) {
284                        dlist(Tnode, Telem) * tgt_after = $next_link(list_pos).terminator;
285                        $dlinks(Telem) * links_after = & tgt_after->$links;
286                        &incoming_from_next = & links_after->prev;
287                } else if ($next_link(list_pos).elem) {
288                        Telem * tgt_after  = $next_link(list_pos).elem;
289                        Tnode & list_pos_after  = $tempcv_e2n(*tgt_after );
290                        &incoming_from_next = & $prev_link(list_pos_after );
291                }
292
293                if (& incoming_from_prev) {
294                        incoming_from_prev = $next_link(list_pos);
295                }
296                if (& incoming_from_next) {
297                        incoming_from_next = $prev_link(list_pos);
298                }
299
300                $next_link(list_pos) = (Telem*) 0p;
301                $prev_link(list_pos) = (Telem*) 0p;
302        }
303}
304
Note: See TracBrowser for help on using the repository browser.