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