source: libcfa/src/containers/list.hfa@ f90d10f

ADT arm-eh ast-experimental enum forall-pointer-decay jacob/cs343-translation new-ast new-ast-unique-expr pthread-emulation qualifiedEnum
Last change on this file since f90d10f was 4d741e9, checked in by Michael Brooks <mlbrooks@…>, 5 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.