-
Notifications
You must be signed in to change notification settings - Fork 0
/
list.h
149 lines (133 loc) · 5.34 KB
/
list.h
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
/* originally: ./include/linux/list.h */
/* SPDX-License-Identifier: GPL-2.0 */
#define list_entry(ptr, type, member) \
container_of(ptr, type, member)
#define list_first_entry(ptr, type, member) \
list_entry((ptr)->next, type, member)
static inline int list_empty(const struct list_head *head)
/*@ requires take O = Owned(head) @*/
/*@ ensures take OR = Owned(head) @*/
/*@ ensures O == OR @*/
/*@ ensures return == (((*head).next == head) ? 1 : 0) @*/
{
/* return READ_ONCE(head->next) == head; */
return head->next == head;
}
/* renamed list to llist to avoid clash with CN keyword list */
static inline void INIT_LIST_HEAD(struct list_head *llist)
/*@ requires take O = Owned(llist) @*/
/*@ ensures take OR = Owned(llist) @*/
/*@ ensures (*llist).next == llist; (*llist).prev == llist @*/
{
/* WRITE_ONCE (llist->next, llist); */
llist->next = llist;
llist->prev = llist;
}
static inline bool __list_del_entry_valid(struct list_head *entry)
/*@ ensures return == 1 @*/
{
return true;
}
static inline void __list_del(struct list_head * prev, struct list_head * next)
/*@ requires take O1 = Owned(prev) @*/
/*@ requires take O2 = O_struct_list_head(next, prev != next) @*/
/*@ ensures take O1R = Owned(prev) @*/
/*@ ensures take O2R = O_struct_list_head(next, prev != next) @*/
/*@ ensures (prev == next) || (O2.next == O2R.next) @*/
/*@ ensures (prev == next) || {(*prev).prev} unchanged @*/
/*@ ensures (*prev).next == next @*/
/*@ ensures (prev == next) || (O2R.prev == prev) @*/
/*@ ensures (prev != next) || ((*prev).prev == prev) @*/
{
/*CN*/ if(prev != next);
next->prev = prev;
/* WRITE_ONCE (prev->next, next); */
prev->next = next;
}
static inline void __list_del_entry(struct list_head *entry)
/*@ requires take O1 = Owned(entry) @*/
/*@ requires let prev = (*entry).prev; let next = (*entry).next @*/
/*@ requires take O2 = O_struct_list_head(prev, prev != entry) @*/
/*@ requires take O3 = O_struct_list_head(next, prev != next) @*/
/*@ requires (prev != entry) || (next == entry) @*/
/*@ ensures take O1R = Owned(entry) @*/
/*@ ensures {*entry} unchanged @*/
/*@ ensures take O2R = O_struct_list_head(prev, prev != entry) @*/
/*@ ensures take O3R = O_struct_list_head(next, prev != next) @*/
/*@ ensures (prev == next) || (O3.next == O3R.next) @*/
/*@ ensures (prev == next) || (O2.prev == O2R.prev) @*/
/*@ ensures (prev == entry) || (O2R.next == next) @*/
/*@ ensures (prev == next) || (O3R.prev == prev) @*/
/*@ ensures (prev != next) || ((prev == entry) || (O2R.prev == prev)) @*/
{
/*CN*/ if(entry->prev != entry);
/*CN*/ if(entry->prev != entry->next);
if (!__list_del_entry_valid(entry))
return;
__list_del(entry->prev, entry->next);
}
static inline void list_del_init(struct list_head *entry)
/*@ requires take O1 = Owned(entry) @*/
/*@ requires let prev = (*entry).prev; let next = (*entry).next @*/
/*@ requires take O2 = Owned(prev) @*/
/*@ requires take O3 = O_struct_list_head(next, prev != next) @*/
/*@ requires (*entry).prev != entry @*/
/*@ ensures take O1R = Owned(entry) @*/
/*@ ensures (*entry).prev == entry; (*entry).next == entry @*/
/*@ ensures take O2R = Owned(prev) @*/
/*@ ensures take O3R = O_struct_list_head(next, prev != next) @*/
/*@ ensures (prev == next) || (O3.next == O3R.next) @*/
/*@ ensures (prev == next) || {(*prev).prev} unchanged @*/
/*@ ensures (*prev).next == next @*/
/*@ ensures (prev == next) || (O3R.prev == prev) @*/
/*@ ensures (prev != next) || ((*prev).prev == prev) @*/
{
/*CN*/ if(entry->prev != entry);
/*CN*/ if(entry->prev != entry->next);
__list_del_entry(entry);
INIT_LIST_HEAD(entry);
}
static inline bool __list_add_valid(struct list_head *new,
struct list_head *prev,
struct list_head *next)
/*@ ensures return == 1 @*/
{
return true;
}
static inline void __list_add(struct list_head *new,
struct list_head *prev,
struct list_head *next)
/*@ requires take O1 = Owned(new); take O2 = Owned(prev); take O3 = O_struct_list_head(next, prev != next) @*/
/*@ ensures take O1R = Owned(new); take O2R = Owned(prev); take O3R = O_struct_list_head(next, prev != next) @*/
/*@ ensures (prev == next) || {(*prev).prev} unchanged @*/
/*@ ensures (prev == next) || (O3.next == O3R.next) @*/
/*@ ensures (*prev).next == new @*/
/*@ ensures (prev == next) || (O3R.prev == new) @*/
/*@ ensures (prev != next) || ((*prev).prev == new) @*/
/*@ ensures (*new).next == next; (*new).prev == prev @*/
{
if (!__list_add_valid(new, prev, next))
return;
/*CN*/ if (prev != next);
next->prev = new;
new->next = next;
new->prev = prev;
/* WRITE_ONCE (prev->next, new); */
prev->next = new;
}
static inline void list_add_tail(struct list_head *new, struct list_head *head)
/*@ requires take O1 = Owned(new) @*/
/*@ requires take O2 = Owned(head) @*/
/*@ requires let prev = (*head).prev; let next = head @*/
/*@ requires take O3 = O_struct_list_head(prev, prev != next) @*/
/*@ ensures take O1R = Owned(new); take O2R = Owned(head); take O3R = O_struct_list_head(prev, prev != next) @*/
/*@ ensures (prev == next) || (O3.prev == O3R.prev) @*/
/*@ ensures (prev == next) || {(*head).next} unchanged @*/
/*@ ensures (*head).prev == new @*/
/*@ ensures (prev == next) || (O3R.next == new) @*/
/*@ ensures (prev != next) || ((*head).next == new) @*/
/*@ ensures (*new).next == next; (*new).prev == prev @*/
{
/*CN*/ if (head->prev != head);
__list_add(new, head->prev, head);
}