1 2[[case]] # simple file seek 3define = [ 4 {COUNT=132, SKIP=4}, 5 {COUNT=132, SKIP=128}, 6 {COUNT=200, SKIP=10}, 7 {COUNT=200, SKIP=100}, 8 {COUNT=4, SKIP=1}, 9 {COUNT=4, SKIP=2}, 10] 11code = ''' 12 lfs_format(&lfs, &cfg) => 0; 13 lfs_mount(&lfs, &cfg) => 0; 14 lfs_file_open(&lfs, &file, "kitty", 15 LFS_O_WRONLY | LFS_O_CREAT | LFS_O_APPEND) => 0; 16 size = strlen("kittycatcat"); 17 memcpy(buffer, "kittycatcat", size); 18 for (int j = 0; j < COUNT; j++) { 19 lfs_file_write(&lfs, &file, buffer, size); 20 } 21 lfs_file_close(&lfs, &file) => 0; 22 lfs_unmount(&lfs) => 0; 23 24 lfs_mount(&lfs, &cfg) => 0; 25 lfs_file_open(&lfs, &file, "kitty", LFS_O_RDONLY) => 0; 26 27 lfs_soff_t pos = -1; 28 size = strlen("kittycatcat"); 29 for (int i = 0; i < SKIP; i++) { 30 lfs_file_read(&lfs, &file, buffer, size) => size; 31 memcmp(buffer, "kittycatcat", size) => 0; 32 pos = lfs_file_tell(&lfs, &file); 33 } 34 assert(pos >= 0); 35 36 lfs_file_seek(&lfs, &file, pos, LFS_SEEK_SET) => pos; 37 lfs_file_read(&lfs, &file, buffer, size) => size; 38 memcmp(buffer, "kittycatcat", size) => 0; 39 40 lfs_file_rewind(&lfs, &file) => 0; 41 lfs_file_read(&lfs, &file, buffer, size) => size; 42 memcmp(buffer, "kittycatcat", size) => 0; 43 44 lfs_file_seek(&lfs, &file, 0, LFS_SEEK_CUR) => size; 45 lfs_file_read(&lfs, &file, buffer, size) => size; 46 memcmp(buffer, "kittycatcat", size) => 0; 47 48 lfs_file_seek(&lfs, &file, size, LFS_SEEK_CUR) => 3*size; 49 lfs_file_read(&lfs, &file, buffer, size) => size; 50 memcmp(buffer, "kittycatcat", size) => 0; 51 52 lfs_file_seek(&lfs, &file, pos, LFS_SEEK_SET) => pos; 53 lfs_file_read(&lfs, &file, buffer, size) => size; 54 memcmp(buffer, "kittycatcat", size) => 0; 55 56 lfs_file_seek(&lfs, &file, -size, LFS_SEEK_CUR) => pos; 57 lfs_file_read(&lfs, &file, buffer, size) => size; 58 memcmp(buffer, "kittycatcat", size) => 0; 59 60 lfs_file_seek(&lfs, &file, -size, LFS_SEEK_END) >= 0 => 1; 61 lfs_file_read(&lfs, &file, buffer, size) => size; 62 memcmp(buffer, "kittycatcat", size) => 0; 63 64 size = lfs_file_size(&lfs, &file); 65 lfs_file_seek(&lfs, &file, 0, LFS_SEEK_CUR) => size; 66 67 lfs_file_close(&lfs, &file) => 0; 68 lfs_unmount(&lfs) => 0; 69''' 70 71[[case]] # simple file seek and write 72define = [ 73 {COUNT=132, SKIP=4}, 74 {COUNT=132, SKIP=128}, 75 {COUNT=200, SKIP=10}, 76 {COUNT=200, SKIP=100}, 77 {COUNT=4, SKIP=1}, 78 {COUNT=4, SKIP=2}, 79] 80code = ''' 81 lfs_format(&lfs, &cfg) => 0; 82 lfs_mount(&lfs, &cfg) => 0; 83 lfs_file_open(&lfs, &file, "kitty", 84 LFS_O_WRONLY | LFS_O_CREAT | LFS_O_APPEND) => 0; 85 size = strlen("kittycatcat"); 86 memcpy(buffer, "kittycatcat", size); 87 for (int j = 0; j < COUNT; j++) { 88 lfs_file_write(&lfs, &file, buffer, size); 89 } 90 lfs_file_close(&lfs, &file) => 0; 91 lfs_unmount(&lfs) => 0; 92 93 lfs_mount(&lfs, &cfg) => 0; 94 lfs_file_open(&lfs, &file, "kitty", LFS_O_RDWR) => 0; 95 96 lfs_soff_t pos = -1; 97 size = strlen("kittycatcat"); 98 for (int i = 0; i < SKIP; i++) { 99 lfs_file_read(&lfs, &file, buffer, size) => size; 100 memcmp(buffer, "kittycatcat", size) => 0; 101 pos = lfs_file_tell(&lfs, &file); 102 } 103 assert(pos >= 0); 104 105 memcpy(buffer, "doggodogdog", size); 106 lfs_file_seek(&lfs, &file, pos, LFS_SEEK_SET) => pos; 107 lfs_file_write(&lfs, &file, buffer, size) => size; 108 109 lfs_file_seek(&lfs, &file, pos, LFS_SEEK_SET) => pos; 110 lfs_file_read(&lfs, &file, buffer, size) => size; 111 memcmp(buffer, "doggodogdog", size) => 0; 112 113 lfs_file_rewind(&lfs, &file) => 0; 114 lfs_file_read(&lfs, &file, buffer, size) => size; 115 memcmp(buffer, "kittycatcat", size) => 0; 116 117 lfs_file_seek(&lfs, &file, pos, LFS_SEEK_SET) => pos; 118 lfs_file_read(&lfs, &file, buffer, size) => size; 119 memcmp(buffer, "doggodogdog", size) => 0; 120 121 lfs_file_seek(&lfs, &file, -size, LFS_SEEK_END) >= 0 => 1; 122 lfs_file_read(&lfs, &file, buffer, size) => size; 123 memcmp(buffer, "kittycatcat", size) => 0; 124 125 size = lfs_file_size(&lfs, &file); 126 lfs_file_seek(&lfs, &file, 0, LFS_SEEK_CUR) => size; 127 128 lfs_file_close(&lfs, &file) => 0; 129 lfs_unmount(&lfs) => 0; 130''' 131 132[[case]] # boundary seek and writes 133define.COUNT = 132 134define.OFFSETS = '"{512, 1020, 513, 1021, 511, 1019, 1441}"' 135code = ''' 136 lfs_format(&lfs, &cfg) => 0; 137 lfs_mount(&lfs, &cfg) => 0; 138 lfs_file_open(&lfs, &file, "kitty", 139 LFS_O_WRONLY | LFS_O_CREAT | LFS_O_APPEND) => 0; 140 size = strlen("kittycatcat"); 141 memcpy(buffer, "kittycatcat", size); 142 for (int j = 0; j < COUNT; j++) { 143 lfs_file_write(&lfs, &file, buffer, size); 144 } 145 lfs_file_close(&lfs, &file) => 0; 146 lfs_unmount(&lfs) => 0; 147 148 lfs_mount(&lfs, &cfg) => 0; 149 lfs_file_open(&lfs, &file, "kitty", LFS_O_RDWR) => 0; 150 151 size = strlen("hedgehoghog"); 152 const lfs_soff_t offsets[] = OFFSETS; 153 154 for (unsigned i = 0; i < sizeof(offsets) / sizeof(offsets[0]); i++) { 155 lfs_soff_t off = offsets[i]; 156 memcpy(buffer, "hedgehoghog", size); 157 lfs_file_seek(&lfs, &file, off, LFS_SEEK_SET) => off; 158 lfs_file_write(&lfs, &file, buffer, size) => size; 159 lfs_file_seek(&lfs, &file, off, LFS_SEEK_SET) => off; 160 lfs_file_read(&lfs, &file, buffer, size) => size; 161 memcmp(buffer, "hedgehoghog", size) => 0; 162 163 lfs_file_seek(&lfs, &file, 0, LFS_SEEK_SET) => 0; 164 lfs_file_read(&lfs, &file, buffer, size) => size; 165 memcmp(buffer, "kittycatcat", size) => 0; 166 167 lfs_file_seek(&lfs, &file, off, LFS_SEEK_SET) => off; 168 lfs_file_read(&lfs, &file, buffer, size) => size; 169 memcmp(buffer, "hedgehoghog", size) => 0; 170 171 lfs_file_sync(&lfs, &file) => 0; 172 173 lfs_file_seek(&lfs, &file, 0, LFS_SEEK_SET) => 0; 174 lfs_file_read(&lfs, &file, buffer, size) => size; 175 memcmp(buffer, "kittycatcat", size) => 0; 176 177 lfs_file_seek(&lfs, &file, off, LFS_SEEK_SET) => off; 178 lfs_file_read(&lfs, &file, buffer, size) => size; 179 memcmp(buffer, "hedgehoghog", size) => 0; 180 } 181 182 lfs_file_close(&lfs, &file) => 0; 183 lfs_unmount(&lfs) => 0; 184''' 185 186[[case]] # out of bounds seek 187define = [ 188 {COUNT=132, SKIP=4}, 189 {COUNT=132, SKIP=128}, 190 {COUNT=200, SKIP=10}, 191 {COUNT=200, SKIP=100}, 192 {COUNT=4, SKIP=2}, 193 {COUNT=4, SKIP=3}, 194] 195code = ''' 196 lfs_format(&lfs, &cfg) => 0; 197 lfs_mount(&lfs, &cfg) => 0; 198 lfs_file_open(&lfs, &file, "kitty", 199 LFS_O_WRONLY | LFS_O_CREAT | LFS_O_APPEND) => 0; 200 size = strlen("kittycatcat"); 201 memcpy(buffer, "kittycatcat", size); 202 for (int j = 0; j < COUNT; j++) { 203 lfs_file_write(&lfs, &file, buffer, size); 204 } 205 lfs_file_close(&lfs, &file) => 0; 206 lfs_unmount(&lfs) => 0; 207 lfs_mount(&lfs, &cfg) => 0; 208 lfs_file_open(&lfs, &file, "kitty", LFS_O_RDWR) => 0; 209 210 size = strlen("kittycatcat"); 211 lfs_file_size(&lfs, &file) => COUNT*size; 212 lfs_file_seek(&lfs, &file, (COUNT+SKIP)*size, 213 LFS_SEEK_SET) => (COUNT+SKIP)*size; 214 lfs_file_read(&lfs, &file, buffer, size) => 0; 215 216 memcpy(buffer, "porcupineee", size); 217 lfs_file_write(&lfs, &file, buffer, size) => size; 218 219 lfs_file_seek(&lfs, &file, (COUNT+SKIP)*size, 220 LFS_SEEK_SET) => (COUNT+SKIP)*size; 221 lfs_file_read(&lfs, &file, buffer, size) => size; 222 memcmp(buffer, "porcupineee", size) => 0; 223 224 lfs_file_seek(&lfs, &file, COUNT*size, 225 LFS_SEEK_SET) => COUNT*size; 226 lfs_file_read(&lfs, &file, buffer, size) => size; 227 memcmp(buffer, "\0\0\0\0\0\0\0\0\0\0\0", size) => 0; 228 229 lfs_file_seek(&lfs, &file, -((COUNT+SKIP)*size), 230 LFS_SEEK_CUR) => LFS_ERR_INVAL; 231 lfs_file_tell(&lfs, &file) => (COUNT+1)*size; 232 233 lfs_file_seek(&lfs, &file, -((COUNT+2*SKIP)*size), 234 LFS_SEEK_END) => LFS_ERR_INVAL; 235 lfs_file_tell(&lfs, &file) => (COUNT+1)*size; 236 237 lfs_file_close(&lfs, &file) => 0; 238 lfs_unmount(&lfs) => 0; 239''' 240 241[[case]] # inline write and seek 242define.SIZE = [2, 4, 128, 132] 243code = ''' 244 lfs_format(&lfs, &cfg) => 0; 245 lfs_mount(&lfs, &cfg) => 0; 246 lfs_file_open(&lfs, &file, "tinykitty", 247 LFS_O_RDWR | LFS_O_CREAT) => 0; 248 int j = 0; 249 int k = 0; 250 251 memcpy(buffer, "abcdefghijklmnopqrstuvwxyz", 26); 252 for (unsigned i = 0; i < SIZE; i++) { 253 lfs_file_write(&lfs, &file, &buffer[j++ % 26], 1) => 1; 254 lfs_file_tell(&lfs, &file) => i+1; 255 lfs_file_size(&lfs, &file) => i+1; 256 } 257 258 lfs_file_seek(&lfs, &file, 0, LFS_SEEK_SET) => 0; 259 lfs_file_tell(&lfs, &file) => 0; 260 lfs_file_size(&lfs, &file) => SIZE; 261 for (unsigned i = 0; i < SIZE; i++) { 262 uint8_t c; 263 lfs_file_read(&lfs, &file, &c, 1) => 1; 264 c => buffer[k++ % 26]; 265 } 266 267 lfs_file_sync(&lfs, &file) => 0; 268 lfs_file_tell(&lfs, &file) => SIZE; 269 lfs_file_size(&lfs, &file) => SIZE; 270 271 lfs_file_seek(&lfs, &file, 0, LFS_SEEK_SET) => 0; 272 for (unsigned i = 0; i < SIZE; i++) { 273 lfs_file_write(&lfs, &file, &buffer[j++ % 26], 1) => 1; 274 lfs_file_tell(&lfs, &file) => i+1; 275 lfs_file_size(&lfs, &file) => SIZE; 276 lfs_file_sync(&lfs, &file) => 0; 277 lfs_file_tell(&lfs, &file) => i+1; 278 lfs_file_size(&lfs, &file) => SIZE; 279 if (i < SIZE-2) { 280 uint8_t c[3]; 281 lfs_file_seek(&lfs, &file, -1, LFS_SEEK_CUR) => i; 282 lfs_file_read(&lfs, &file, &c, 3) => 3; 283 lfs_file_tell(&lfs, &file) => i+3; 284 lfs_file_size(&lfs, &file) => SIZE; 285 lfs_file_seek(&lfs, &file, i+1, LFS_SEEK_SET) => i+1; 286 lfs_file_tell(&lfs, &file) => i+1; 287 lfs_file_size(&lfs, &file) => SIZE; 288 } 289 } 290 291 lfs_file_seek(&lfs, &file, 0, LFS_SEEK_SET) => 0; 292 lfs_file_tell(&lfs, &file) => 0; 293 lfs_file_size(&lfs, &file) => SIZE; 294 for (unsigned i = 0; i < SIZE; i++) { 295 uint8_t c; 296 lfs_file_read(&lfs, &file, &c, 1) => 1; 297 c => buffer[k++ % 26]; 298 } 299 300 lfs_file_sync(&lfs, &file) => 0; 301 lfs_file_tell(&lfs, &file) => SIZE; 302 lfs_file_size(&lfs, &file) => SIZE; 303 304 lfs_file_close(&lfs, &file) => 0; 305 lfs_unmount(&lfs) => 0; 306''' 307 308[[case]] # file seek and write with power-loss 309# must be power-of-2 for quadratic probing to be exhaustive 310define.COUNT = [4, 64, 128] 311reentrant = true 312code = ''' 313 err = lfs_mount(&lfs, &cfg); 314 if (err) { 315 lfs_format(&lfs, &cfg) => 0; 316 lfs_mount(&lfs, &cfg) => 0; 317 } 318 err = lfs_file_open(&lfs, &file, "kitty", LFS_O_RDONLY); 319 assert(!err || err == LFS_ERR_NOENT); 320 if (!err) { 321 if (lfs_file_size(&lfs, &file) != 0) { 322 lfs_file_size(&lfs, &file) => 11*COUNT; 323 for (int j = 0; j < COUNT; j++) { 324 memset(buffer, 0, 11+1); 325 lfs_file_read(&lfs, &file, buffer, 11) => 11; 326 assert(memcmp(buffer, "kittycatcat", 11) == 0 || 327 memcmp(buffer, "doggodogdog", 11) == 0); 328 } 329 } 330 lfs_file_close(&lfs, &file) => 0; 331 } 332 333 lfs_file_open(&lfs, &file, "kitty", LFS_O_WRONLY | LFS_O_CREAT) => 0; 334 if (lfs_file_size(&lfs, &file) == 0) { 335 for (int j = 0; j < COUNT; j++) { 336 strcpy((char*)buffer, "kittycatcat"); 337 size = strlen((char*)buffer); 338 lfs_file_write(&lfs, &file, buffer, size) => size; 339 } 340 } 341 lfs_file_close(&lfs, &file) => 0; 342 343 strcpy((char*)buffer, "doggodogdog"); 344 size = strlen((char*)buffer); 345 346 lfs_file_open(&lfs, &file, "kitty", LFS_O_RDWR) => 0; 347 lfs_file_size(&lfs, &file) => COUNT*size; 348 // seek and write using quadratic probing to touch all 349 // 11-byte words in the file 350 lfs_off_t off = 0; 351 for (int j = 0; j < COUNT; j++) { 352 off = (5*off + 1) % COUNT; 353 lfs_file_seek(&lfs, &file, off*size, LFS_SEEK_SET) => off*size; 354 lfs_file_read(&lfs, &file, buffer, size) => size; 355 assert(memcmp(buffer, "kittycatcat", size) == 0 || 356 memcmp(buffer, "doggodogdog", size) == 0); 357 if (memcmp(buffer, "doggodogdog", size) != 0) { 358 lfs_file_seek(&lfs, &file, off*size, LFS_SEEK_SET) => off*size; 359 strcpy((char*)buffer, "doggodogdog"); 360 lfs_file_write(&lfs, &file, buffer, size) => size; 361 lfs_file_seek(&lfs, &file, off*size, LFS_SEEK_SET) => off*size; 362 lfs_file_read(&lfs, &file, buffer, size) => size; 363 assert(memcmp(buffer, "doggodogdog", size) == 0); 364 lfs_file_sync(&lfs, &file) => 0; 365 lfs_file_seek(&lfs, &file, off*size, LFS_SEEK_SET) => off*size; 366 lfs_file_read(&lfs, &file, buffer, size) => size; 367 assert(memcmp(buffer, "doggodogdog", size) == 0); 368 } 369 } 370 lfs_file_close(&lfs, &file) => 0; 371 372 lfs_file_open(&lfs, &file, "kitty", LFS_O_RDWR) => 0; 373 lfs_file_size(&lfs, &file) => COUNT*size; 374 for (int j = 0; j < COUNT; j++) { 375 lfs_file_read(&lfs, &file, buffer, size) => size; 376 assert(memcmp(buffer, "doggodogdog", size) == 0); 377 } 378 lfs_file_close(&lfs, &file) => 0; 379 lfs_unmount(&lfs) => 0; 380''' 381