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
|
/*
File: pnext.c
Copyright (C) 2009 Christophe GRENIER <grenier@cgsecurity.org>
This software is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License along
with this program; if not, write the Free Software Foundation, Inc., 51
Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*/
#ifndef _PNEXT_H
#define _PNEXT_H
/* #define DEBUG_GET_NEXT_SECTOR */
/*@
@ requires \valid_read(list_search_space);
@ requires \valid(current_search_space);
@ requires \valid(offset);
@ requires \separated(list_search_space, current_search_space, offset);
@ assigns *current_search_space, *offset;
@*/
static
#ifndef DEBUG_GET_NEXT_SECTOR
inline
#endif
void get_next_header(const alloc_data_t *list_search_space, alloc_data_t **current_search_space, uint64_t *offset)
{
#ifdef DEBUG_GET_NEXT_SECTOR
log_trace(" get_next_header %llu (%llu-%llu)\n",
(unsigned long long)((*offset)/512),
(unsigned long long)((*current_search_space)->start/512),
(unsigned long long)((*current_search_space)->end)/512);
#endif
if((*current_search_space) != list_search_space)
*current_search_space=td_list_entry((*current_search_space)->list.next, alloc_data_t, list);
*offset=(*current_search_space)->start;
}
/*@
@ requires \valid_read(list_search_space);
@ requires \valid(current_search_space);
@ requires \valid(offset);
@ requires \separated(list_search_space, current_search_space, offset);
@ assigns *current_search_space, *offset;
@*/
static
#ifndef DEBUG_GET_NEXT_SECTOR
inline
#endif
void get_next_sector(const alloc_data_t *list_search_space, alloc_data_t **current_search_space, uint64_t *offset, const unsigned int blocksize)
{
#ifdef DEBUG_GET_NEXT_SECTOR
log_debug(" get_next_sector %llu (%llu-%llu)\n",
(unsigned long long)((*offset)/512),
(unsigned long long)((*current_search_space)->start/512),
(unsigned long long)((*current_search_space)->end)/512);
#endif
if((*current_search_space) == list_search_space)
{
return ;
}
#ifdef DEBUG_GET_NEXT_SECTOR
if(! ((*current_search_space)->start <= *offset && (*offset)<=(*current_search_space)->end))
{
log_critical("BUG: get_next_sector stop everything %llu (%llu-%llu)\n",
(unsigned long long)((*offset)/512),
(unsigned long long)((*current_search_space)->start/512),
(unsigned long long)((*current_search_space)->end/512));
log_flush();
log_close();
exit(1);
}
#endif
if((*offset)+blocksize <= (*current_search_space)->end)
*offset+=blocksize;
else
get_next_header(list_search_space, current_search_space, offset);
}
/*@
@ requires \valid_read(list_search_space);
@ requires \valid(current_search_space);
@ requires \valid(offset);
@ requires \separated(list_search_space, current_search_space, offset);
@ assigns *current_search_space, *offset;
@*/
static inline void get_prev_header(const alloc_data_t *list_search_space, alloc_data_t **current_search_space, uint64_t *offset, const unsigned int blocksize)
{
if((*current_search_space) != list_search_space)
*current_search_space=td_list_entry((*current_search_space)->list.prev, alloc_data_t, list);
*offset=(*current_search_space)->end + 1 - blocksize;
}
/*@
@ requires \valid_read(list_search_space);
@ requires \valid(current_search_space);
@ requires \valid(offset);
@ requires \separated(list_search_space, current_search_space, offset);
@ assigns *current_search_space, *offset;
@*/
static inline void get_prev_sector(const alloc_data_t *list_search_space, alloc_data_t **current_search_space, uint64_t *offset, const unsigned int blocksize)
{
if((*current_search_space) == list_search_space)
{
return ;
}
if((*offset) >= (*current_search_space)->start + blocksize)
*offset-=blocksize;
else
get_prev_header(list_search_space, current_search_space, offset, blocksize);
}
#endif
|
