1/* this is a -*- c -*- file */
2/*
3 * @TAG(OTHER_BSD)
4 */
5
6/* ********************************************************************
7 *
8 * Copyright (C) 2002, 2003-2004,  Karlsruhe University
9 *   Original authors
10 *
11 * Copyright (C) 2009-2012, NICTA
12 *   Translation to C for verification experiments.
13 *
14 * Description:   very simple kernel memory allocator
15 *
16 * Redistribution and use in source and binary forms, with or without
17 * modification, are permitted provided that the following conditions
18 * are met:
19 * 1. Redistributions of source code must retain the above copyright
20 *    notice, this list of conditions and the following disclaimer.
21 * 2. Redistributions in binary form must reproduce the above copyright
22 *    notice, this list of conditions and the following disclaimer in the
23 *    documentation and/or other materials provided with the distribution.
24 *
25 * THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND
26 * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
27 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
28 * ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE
29 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
30 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
31 * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
32 * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
33 * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
34 * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
35 * SUCH DAMAGE.
36 *
37 ******************************************************************* */
38
39typedef unsigned int u64_t;
40typedef unsigned int u32_t;
41typedef unsigned short u16_t;
42typedef unsigned char u8_t;
43
44typedef signed int s64_t;
45typedef signed int s32_t;
46typedef signed short s16_t;
47typedef signed char s8_t;
48
49typedef u32_t word_t;
50
51
52typedef void* addr_t;
53
54
55word_t *kmem_free_list;
56
57void init (void * start, void * end);
58void free (void * address, word_t size);
59
60void * alloc (word_t size);
61void * alloc_aligned (word_t size, word_t alignement, word_t mask);
62
63
64
65void init(void * start, void * end)
66{
67    kmem_free_list = 0;
68
69    free(start, (word_t)end - (word_t)start);
70
71}
72
73void free(void * address, word_t size)
74{
75    word_t* p;
76    word_t* prev, *curr;
77
78    size = size >= 1024 ? size : 1024;
79
80    /** AUXUPD: "(True,ptr_retyps (unat \<acute>size div unat KMC) (ptr_val \<acute>address))" */
81
82    for (p = (word_t*)address;
83         p < ((word_t*)(((word_t)address) + size - (1024)));
84         p = (word_t*) *p)
85        *p = (word_t) p + (1024);
86
87    for (prev = (word_t*) &kmem_free_list, curr = kmem_free_list;
88         curr && (address > (void *)curr);
89         prev = curr, curr = (word_t*) *curr)
90    ;
91
92    *prev = (word_t) address; *p = (word_t) curr;
93}
94
95
96
97void sep_free(void * address, word_t size)
98{
99    word_t* p;
100    word_t* prev, *curr;
101
102    size = size >= 1024 ? size : 1024;
103
104    /** AUXUPD: "(True,ptr_retyp (ptr_coerce \<acute>address::word32 ptr))" */
105
106    for (p = (word_t*)address;
107         p < ((word_t*)(((word_t)address) + size - (1024)));
108         p = (word_t*) *p)
109      {
110        *p = (word_t) p + (1024);
111        /** AUXUPD: "(True,ptr_retyp (Ptr (ptr_val \<acute>p + 1024)::word32 ptr))" */
112      }
113
114    for (prev = (word_t*) &kmem_free_list, curr = kmem_free_list;
115         curr && (address > (void *)curr);
116         prev = curr, curr = (word_t*) *curr)
117    ;
118
119    *prev = (word_t) address; *p = (word_t) curr;
120}
121
122
123void * alloc(word_t size)
124{
125    word_t* prev;
126    word_t* curr;
127    word_t* tmp;
128    word_t i;
129
130    size = size >= 1024 ? size : 1024;
131
132    for (prev = (word_t*) &kmem_free_list, curr = kmem_free_list;
133         curr;
134         prev = curr, curr = (word_t*) *curr)
135    {
136        if (!((word_t) curr & (size - 1)))
137        {
138            tmp = (word_t*) *curr;
139            for (i = 1; tmp && (i < (size / (1024))); i++)
140            {
141
142                if ((word_t) tmp != ((word_t) curr + (1024)*i))
143                {
144                    tmp = 0;
145                    break;
146                };
147                tmp = (word_t*) *tmp;
148            }
149            if (tmp)
150            {
151
152                *prev = (word_t) tmp;
153
154
155                for (i = 0; i < (size / sizeof(word_t)); i++)
156                    curr[i] = 0;
157
158                return curr;
159            }
160        }
161    }
162
163    return 0;
164}
165
166void * sep_alloc(word_t size)
167{
168    word_t* prev;
169    word_t* curr;
170    word_t* tmp;
171    word_t i;
172
173    size = size >= 1024 ? size : 1024;
174
175    for (prev = (word_t*) &kmem_free_list, curr = kmem_free_list;
176         curr;
177         prev = curr, curr = (word_t*) *curr)
178    {
179        if (!((word_t) curr & (size - 1)))
180        {
181            tmp = (word_t*) *curr;
182            for (i = 1; tmp && (i < (size / (1024))); i++)
183            {
184
185                if ((word_t) tmp != ((word_t) curr + (1024)*i))
186                {
187                    tmp = 0;
188                    break;
189                };
190                tmp = (word_t*) *tmp;
191            }
192            if (tmp)
193            {
194
195                *prev = (word_t) tmp;
196
197
198                for (i = 0; i < (size / sizeof(word_t)); i++)
199                    {
200                    /** AUXUPD: "(ptr_safe (\<acute>curr +\<^sub>p uint \<acute>i) (hrs_htd \<acute>t_hrs),ptr_retyp (\<acute>curr +\<^sub>p uint \<acute>i))"*/
201                    curr[i] = 0;
202                }
203
204                return curr;
205            }
206        }
207    }
208
209    return 0;
210}
211
212void kmalloc_test(word_t size)
213{
214    void *p;
215
216    p = alloc(size);
217
218    if (!p) return;
219
220    free(p, size);
221}
222
223void sep_test(word_t size)
224{
225    void *p;
226
227    p = sep_alloc(size);
228
229    if (!p) return;
230
231    sep_free(p, size);
232}
233
234