Line data Source code
1 : #include <linked_list_helper.h>
2 : #include <nondet.h>
3 : #include <proof_allocators.h>
4 : #include <seahorn/seahorn.h>
5 :
6 : // init helper for length <= 2
7 : static inline void init_short_aws_linked_list(struct aws_linked_list *list,
8 21316 : size_t length) {
9 21316 : struct aws_linked_list_node *front;
10 21316 : struct aws_linked_list_node *back;
11 21316 : // initialize
12 21316 : list->head.prev = NULL;
13 21316 : list->tail.next = NULL;
14 21316 : // populate linked list based on nd length
15 21316 : if (length == 0) {
16 13564 : aws_linked_list_attach_after(&list->head, &list->tail, true);
17 13564 : } else if (length == 1) {
18 5678 : front = malloc(sizeof(struct aws_linked_list_node));
19 5678 : aws_linked_list_attach_after(&list->head, front, true);
20 5678 : aws_linked_list_attach_after(front, &list->tail, true);
21 5700 : } else if (length == 2) {
22 2074 : front = malloc(sizeof(struct aws_linked_list_node));
23 2074 : back = malloc(sizeof(struct aws_linked_list_node));
24 2074 : aws_linked_list_attach_after(&list->head, front, true);
25 2074 : aws_linked_list_attach_after(front, back, true);
26 2074 : aws_linked_list_attach_after(back, &list->tail, true);
27 2074 : }
28 21316 : }
29 :
30 1112130 : void init_node(struct aws_linked_list_node *node) {
31 1112130 : assume(node);
32 1112130 : node->next = NULL;
33 1112130 : node->prev = NULL;
34 1112130 : }
35 :
36 : void sea_nd_init_aws_linked_list_from_head(struct aws_linked_list *list,
37 250000 : size_t *length) {
38 250000 : list->head.prev = NULL;
39 250000 : list->tail.next = NULL;
40 250000 :
41 250000 : size_t nd_len = nd_size_t();
42 250000 : *length = nd_len;
43 250000 : if (nd_len <= 2) {
44 2830 : init_short_aws_linked_list(list, nd_len);
45 247170 : } else {
46 247170 : // HEAD <--> front <--> front_next --> nd ... nd <-- TAIL
47 247170 : struct aws_linked_list_node *front =
48 247170 : malloc(sizeof(struct aws_linked_list_node));
49 247170 : init_node(front);
50 247170 : struct aws_linked_list_node *front_next =
51 247170 : malloc(sizeof(struct aws_linked_list_node));
52 247170 : init_node(front_next);
53 247170 : aws_linked_list_attach_after(&list->head, front, true);
54 247170 : aws_linked_list_attach_after(front, front_next, true);
55 247170 : aws_linked_list_attach_after(front_next, &list->tail, false);
56 247170 : }
57 250000 : }
58 :
59 : void sea_nd_init_aws_linked_list_from_tail(struct aws_linked_list *list,
60 250000 : size_t *length) {
61 250000 : list->head.prev = NULL;
62 250000 : list->tail.next = NULL;
63 250000 :
64 250000 : size_t nd_len = nd_size_t();
65 250000 : *length = nd_len;
66 250000 : if (nd_len <= 2) {
67 2518 : init_short_aws_linked_list(list, nd_len);
68 247482 : } else {
69 247482 : // HEAD --> nd ... nd <-- back_prev <--> back <--> TAIL
70 247482 : struct aws_linked_list_node *back =
71 247482 : malloc(sizeof(struct aws_linked_list_node));
72 247482 : init_node(back);
73 247482 : struct aws_linked_list_node *back_prev =
74 247482 : malloc(sizeof(struct aws_linked_list_node));
75 247482 : init_node(back_prev);
76 247482 : aws_linked_list_attach_after(&list->head, back_prev, false);
77 247482 : aws_linked_list_attach_after(back_prev, back, true);
78 247482 : aws_linked_list_attach_after(back, &list->tail, true);
79 247482 : }
80 250000 : }
81 :
82 : void sea_nd_init_aws_linked_list(struct aws_linked_list *list,
83 92355 : size_t *length) {
84 92355 : list->head.prev = NULL;
85 92355 : list->tail.next = NULL;
86 92355 :
87 92355 : size_t nd_len = nd_size_t();
88 92355 : *length = nd_len;
89 92355 : if (nd_len <= 2) {
90 15968 : init_short_aws_linked_list(list, nd_len);
91 15968 : }
92 76387 : else {
93 76387 : // HEAD <--> front --> nd ... nd <-- back <--> TAIL
94 76387 : struct aws_linked_list_node *front =
95 76387 : malloc(sizeof(struct aws_linked_list_node));
96 76387 : init_node(front);
97 76387 : struct aws_linked_list_node *back =
98 76387 : malloc(sizeof(struct aws_linked_list_node));
99 76387 : init_node(back);
100 76387 : aws_linked_list_attach_after(&list->head, front, true);
101 76387 : aws_linked_list_attach_after(front, back, false);
102 76387 : aws_linked_list_attach_after(back, &list->tail, true);
103 76387 : }
104 92355 : }
105 :
106 : bool nodes_prev_equal(struct aws_linked_list_node *node,
107 1152038 : struct saved_aws_linked_list_node *saved) {
108 1152038 : return node == saved->node && node->prev == saved->node_prev;
109 1152038 : }
110 :
111 : bool nodes_next_equal(struct aws_linked_list_node *node,
112 1154863 : struct saved_aws_linked_list_node *saved) {
113 1154863 : return node == saved->node && node->next == saved->node_next;
114 1154863 : }
115 :
116 : bool nodes_equal(struct aws_linked_list_node *node,
117 909536 : struct saved_aws_linked_list_node *saved) {
118 909536 : return nodes_prev_equal(node, saved) && nodes_next_equal(node, saved);
119 909536 : }
120 :
121 : void sea_save_aws_node_to_sea_node(struct aws_linked_list_node *s,
122 1916419 : struct saved_aws_linked_list_node *d) {
123 1916419 : d->node = s;
124 1916419 : d->node_prev = s->prev;
125 1916419 : d->node_next = s->next;
126 1916419 : }
127 :
128 : bool check_tail_unchanged(struct aws_linked_list *list,
129 0 : struct saved_aws_linked_list *saved) {
130 0 : return nodes_equal(&list->tail, &saved->tail);
131 0 : }
132 :
133 : bool is_aws_list_unchanged_to_tail(struct aws_linked_list *list,
134 192382 : struct saved_aws_linked_list *saved) {
135 192382 : if (saved->saved_size == 0) {
136 425 : // if saved size is zero, only check that tail is unchanged
137 425 : return nodes_next_equal(&list->tail, &saved->tail);
138 191957 : } else if (saved->saved_size == 1) {
139 40252 : // if saved size is 1 then check start and tail are unchanged
140 40252 : return nodes_next_equal(saved->save_point, &saved->nodes[0]) &&
141 40252 : nodes_equal(&list->tail, &saved->tail);
142 40252 :
143 190681 : } else if (saved->saved_size == 2) {
144 38284 : // if saved size is 2 then check start, start.next and tail are unchanged
145 38284 : return nodes_next_equal(saved->save_point, &saved->nodes[0]) &&
146 38284 : nodes_equal(saved->save_point->next, &saved->nodes[1]) &&
147 38284 : nodes_equal(&list->tail, &saved->tail);
148 38284 :
149 151491 : } else if (saved->saved_size == 3) {
150 113421 : // we only save a maximum of three nodes since that is the maximum we
151 113421 : // construct concretely are head <--> node1 <--> node2
152 113421 : return nodes_next_equal(saved->save_point, &saved->nodes[0]) &&
153 113421 : nodes_equal(saved->save_point->next, &saved->nodes[1]) &&
154 113421 : nodes_equal(saved->save_point->next->next, &saved->nodes[2]) &&
155 113421 : nodes_equal(&list->tail, &saved->tail);
156 113421 : } else {
157 0 : return false;
158 0 : }
159 192382 : // do nothing here: if condition should be exhaustive
160 192382 : }
161 :
162 : bool is_aws_list_unchanged_to_head(struct aws_linked_list *list,
163 189557 : struct saved_aws_linked_list *saved) {
164 189557 : if (saved->saved_size == 0) {
165 360 : // if saved size is zero, only check that head is unchanged
166 360 : return nodes_prev_equal(&list->head, &saved->head);
167 189197 : } else if (saved->saved_size == 1) {
168 38596 : // if saved size is 1 then check start and head are unchanged
169 38596 : return nodes_prev_equal(saved->save_point, &saved->nodes[0]) &&
170 38596 : nodes_equal(&list->head, &saved->head);
171 38596 : ;
172 150601 : } else if (saved->saved_size == 2) {
173 37946 : // if saved size is 2 then check start, start.prev and head are unchanged
174 37946 : return nodes_prev_equal(saved->save_point, &saved->nodes[0]) &&
175 37946 : nodes_equal(saved->save_point->prev, &saved->nodes[1]) &&
176 37946 : nodes_equal(&list->head, &saved->head);
177 37946 : ;
178 112655 : } else if (saved->saved_size == 3) {
179 112655 : // we only save a maximum of three nodes since that is the maximum we
180 112655 : // construct concretely are node1 <--> node2 <--> tail
181 112655 : return nodes_prev_equal(saved->save_point, &saved->nodes[0]) &&
182 112655 : nodes_equal(saved->save_point->prev, &saved->nodes[1]) &&
183 112655 : nodes_equal(saved->save_point->prev->prev, &saved->nodes[2]) &&
184 112655 : nodes_equal(&list->head, &saved->head);
185 112655 : } else {
186 0 : return false;
187 0 : }
188 189557 : // do nothing here: if condition should be exhaustive
189 189557 : }
190 :
191 : bool is_aws_list_unchanged_full(struct aws_linked_list *list,
192 65886 : struct saved_aws_linked_list *saved) {
193 65886 : if (saved->saved_size == 0)
194 8582 : { /* saved zero nodes */
195 8582 : return saved->head.node_next == saved->tail.node &&
196 8582 : saved->tail.node_prev == saved->head.node;
197 8582 : }
198 57304 : else if (saved->saved_size == 1)
199 4359 : {
200 4359 : // when content consists of one node, only check equality of the node itself
201 4359 : return saved->save_point == saved->save_point_end &&
202 4359 : saved->save_point == saved->nodes[0].node;
203 4359 : }
204 52945 : else if (saved->saved_size == 2)
205 52945 : {
206 52945 : return nodes_next_equal(saved->save_point, &saved->nodes[0]) &&
207 52945 : nodes_prev_equal(saved->save_point_end, &saved->nodes[1]);
208 52945 : }
209 0 : else if (saved->saved_size == 3)
210 0 : {
211 0 : if (nodes_next_equal(saved->save_point, &saved->nodes[0]) &&
212 0 : nodes_prev_equal(saved->save_point_end, &saved->nodes[2]))
213 0 : {
214 0 : if (saved->nodes[1].node == saved->save_point->next)
215 0 : {
216 0 : return nodes_equal(saved->save_point->next, &saved->nodes[1]);
217 0 : }
218 0 : else if (saved->nodes[1].node == saved->save_point_end->prev)
219 0 : {
220 0 : return nodes_equal(saved->save_point_end->prev, &saved->nodes[1]);
221 0 : }
222 0 : else
223 0 : return false;
224 0 : }
225 0 : else
226 0 : return false;
227 0 : }
228 0 : else if (saved->saved_size == 4)
229 0 : {
230 0 : return nodes_next_equal(saved->save_point, &saved->nodes[0]) &&
231 0 : nodes_equal(saved->save_point->next, &saved->nodes[1]) &&
232 0 : nodes_equal(saved->save_point_end->prev, &saved->nodes[2]) &&
233 0 : nodes_prev_equal(saved->save_point_end, &saved->nodes[3]);
234 0 : }
235 0 : else
236 0 : return false;
237 65886 : }
238 :
239 : // iterator function for save*Node
240 378547 : struct aws_linked_list_node *getNext(struct aws_linked_list_node *node) {
241 378547 : return node->next;
242 378547 : }
243 :
244 : // iterator function for save*Node
245 375911 : struct aws_linked_list_node *getPrev(struct aws_linked_list_node *node) {
246 375911 : return node->prev;
247 375911 : }
248 :
249 : void save_one_node(struct aws_linked_list_node *start,
250 83535 : struct saved_aws_linked_list *to_save) {
251 83535 : sea_save_aws_node_to_sea_node(start, &to_save->nodes[0]);
252 83535 : to_save->saved_size = 1;
253 83535 : }
254 : void save_two_nodes(
255 : struct aws_linked_list_node *start, struct saved_aws_linked_list *to_save,
256 76230 : struct aws_linked_list_node *(*next)(struct aws_linked_list_node *)) {
257 76230 : sea_save_aws_node_to_sea_node(start, &to_save->nodes[0]);
258 76230 : sea_save_aws_node_to_sea_node((*next)(start), &to_save->nodes[1]);
259 76230 : to_save->saved_size = 2;
260 76230 : }
261 : void save_three_nodes(
262 : struct aws_linked_list_node *start, struct saved_aws_linked_list *to_save,
263 226076 : struct aws_linked_list_node *(*next)(struct aws_linked_list_node *)) {
264 226076 : sea_save_aws_node_to_sea_node(start, &to_save->nodes[0]);
265 226076 : sea_save_aws_node_to_sea_node((*next)(start), &to_save->nodes[1]);
266 226076 : sea_save_aws_node_to_sea_node((*next)((*next)(start)), &to_save->nodes[2]);
267 226076 : to_save->saved_size = 3;
268 226076 : }
269 : void aws_linked_list_save_to_tail(struct aws_linked_list *list, size_t size,
270 : struct aws_linked_list_node *start,
271 192710 : struct saved_aws_linked_list *to_save) {
272 192710 : sea_save_aws_node_to_sea_node(&list->head, &to_save->head);
273 192710 : sea_save_aws_node_to_sea_node(&list->tail, &to_save->tail);
274 192710 :
275 192710 : to_save->save_point = start;
276 192710 :
277 192710 : if (size == 0) {
278 1907 : // only possibility is to save head or tail.
279 1907 : // Note tail is never saved in nodes[..] array
280 1907 : if (&list->head == start) {
281 1527 : save_one_node(start, to_save);
282 1907 : } else {
283 380 : to_save->saved_size = 0;
284 380 : }
285 190803 : } else if (size == 1) {
286 336 : // either save head, head.next or only head.next
287 336 : if (&list->head == start) {
288 214 : save_two_nodes(start, to_save, getNext);
289 336 : } else if (list->head.next == start) {
290 77 : save_one_node(start, to_save);
291 122 : } else {
292 45 : to_save->saved_size = 0;
293 45 : }
294 190467 : } else if (size > 1) {
295 190467 : // either save
296 190467 : // 1) head, head.next, head.next.next OR
297 190467 : // 2) head.next, head.next.next OR
298 190467 : // 3) head.next.next
299 190467 : if (&list->head == start) {
300 113421 : save_three_nodes(start, to_save, getNext);
301 190467 : } else if (list->head.next == start) {
302 38070 : save_two_nodes(start, to_save, getNext);
303 77046 : } else if (list->head.next->next == start) {
304 38976 : save_one_node(start, to_save);
305 38976 : } else {
306 0 : to_save->saved_size = 0;
307 0 : }
308 190467 : }
309 192710 : }
310 :
311 : void aws_linked_list_save_to_head(struct aws_linked_list *list, size_t size,
312 : struct aws_linked_list_node *start,
313 189557 : struct saved_aws_linked_list *to_save) {
314 189557 : sea_save_aws_node_to_sea_node(&list->head, &to_save->head);
315 189557 : sea_save_aws_node_to_sea_node(&list->tail, &to_save->tail);
316 189557 :
317 189557 : to_save->save_point = start;
318 189557 :
319 189557 : if (size == 0) {
320 1501 : // only possibility is to save tail or head
321 1501 : // Note: head is never saved in nodes[..] array
322 1501 : if (&list->tail == start) {
323 1184 : save_one_node(start, to_save);
324 1501 : } else {
325 317 : to_save->saved_size = 0;
326 317 : }
327 188056 : } else if (size == 1) {
328 320 : // either save (in-order) tail, tail.prev or only tail.prev
329 320 : if (&list->tail == start) {
330 204 : save_two_nodes(start, to_save, getPrev);
331 320 : } else if (list->tail.prev == start) {
332 73 : save_one_node(start, to_save);
333 116 : } else {
334 43 : to_save->saved_size = 0;
335 43 : }
336 187736 : } else if (size > 1) {
337 187736 : // either save (in-order)
338 187736 : // 1) tail, tail.prev, tail.prev.prev OR
339 187736 : // 2) tail.prev, tail.prev.prev OR
340 187736 : // 3) tail.prev.prev
341 187736 : if (&list->tail == start) {
342 112655 : save_three_nodes(start, to_save, getPrev);
343 187736 : } else if (list->tail.prev == start) {
344 37742 : save_two_nodes(start, to_save, getPrev);
345 75081 : } else if (list->tail.prev->prev == start) {
346 37339 : save_one_node(start, to_save);
347 37339 : } else {
348 0 : to_save->saved_size = 0;
349 0 : }
350 187736 : }
351 189557 : }
352 :
353 : void aws_linked_list_save_full(struct aws_linked_list *list, size_t size,
354 : struct aws_linked_list_node *start,
355 : struct aws_linked_list_node *end,
356 : struct saved_aws_linked_list *to_save)
357 65886 : {
358 65886 : sea_save_aws_node_to_sea_node(&list->head, &to_save->head);
359 65886 : sea_save_aws_node_to_sea_node(&list->tail, &to_save->tail);
360 65886 : to_save->save_point = start;
361 65886 : to_save->save_point_end = end;
362 65886 : if (start == end) {
363 4359 : save_one_node(start, to_save);
364 4359 : return;
365 4359 : }
366 61527 : if (size == 0) {
367 8582 : /* only save head and tail */
368 8582 : if (start == &list->head) {
369 0 : save_two_nodes(start, to_save, getNext);
370 8582 : } else {
371 8582 : /* save content when empty */
372 8582 : to_save->saved_size = 0;
373 8582 : }
374 52945 : } else if (size == 1) {
375 0 : /* front nodes: [head, head.next...] or [head.next...] */
376 0 : /* back nodes: [...tail] or same as front nodes */
377 0 : size_t back_nodes_start = 0;
378 0 : if (start == &list->head) {
379 0 : sea_save_aws_node_to_sea_node(&list->head, &to_save->nodes[0]);
380 0 : sea_save_aws_node_to_sea_node(list->head.next, &to_save->nodes[1]);
381 0 : to_save->saved_size = 2;
382 0 : back_nodes_start = 2;
383 0 : } else if (start == list->head.next) {
384 0 : sea_save_aws_node_to_sea_node(list->head.next, &to_save->nodes[0]);
385 0 : to_save->saved_size = 1;
386 0 : back_nodes_start = 1;
387 0 : }
388 0 : /* head.next == tail.prev, so only conditionally add tail */
389 0 : if (end == &list->tail) {
390 0 : sea_save_aws_node_to_sea_node(end, &to_save->nodes[back_nodes_start]);
391 0 : to_save->saved_size += 1;
392 0 : }
393 52945 : } else if (size > 1) {
394 52945 : size_t back_nodes_start = 0;
395 52945 : /* front nodes: [head, head.next...] or [head.next...] */
396 52945 : /* back nodes: [...tail.prev] or [...tail.prev, tail] */
397 52945 : if (start == &list->head) {
398 0 : sea_save_aws_node_to_sea_node(&list->head, &to_save->nodes[0]);
399 0 : sea_save_aws_node_to_sea_node(list->head.next, &to_save->nodes[1]);
400 0 : to_save->saved_size = 2;
401 0 : back_nodes_start = 2;
402 52945 : } else if (start == list->head.next) {
403 52945 : sea_save_aws_node_to_sea_node(list->head.next, &to_save->nodes[0]);
404 52945 : to_save->saved_size = 1;
405 52945 : back_nodes_start = 1;
406 52945 : }
407 52945 : if (end == &list->tail) {
408 0 : sea_save_aws_node_to_sea_node(list->tail.prev, &to_save->nodes[back_nodes_start]);
409 0 : sea_save_aws_node_to_sea_node(&list->tail, &to_save->nodes[back_nodes_start + 1]);
410 0 : to_save->saved_size += 2;
411 52945 : } else if (end == list->tail.prev) {
412 52945 : sea_save_aws_node_to_sea_node(list->tail.prev, &to_save->nodes[back_nodes_start]);
413 52945 : to_save->saved_size += 1;
414 52945 : }
415 52945 : }
416 61527 : }
417 :
418 : void aws_linked_list_attach_after(struct aws_linked_list_node *after,
419 : struct aws_linked_list_node *to_attach,
420 1869771 : bool directly_attached) {
421 1869771 : if (directly_attached) {
422 1313706 : after->next = to_attach;
423 1313706 : to_attach->prev = after;
424 1313706 : } else {
425 556065 : after->next = nd_linked_list_node();
426 556065 : to_attach->prev = nd_linked_list_node();
427 556065 : }
428 1869771 : }
429 :
430 : bool is_aws_linked_list_node_attached_after(
431 : struct aws_linked_list_node *after,
432 422318 : struct aws_linked_list_node *to_attach) {
433 422318 : return after->next == to_attach && to_attach->prev == after;
434 422318 : }
|
