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
|
#include "kernel/prelude/kernel_prelude.hats"
#define ATS_DYNLOADFLAG 0
macdef invalid_area = @{
base_addr = the_null_ptr,
length = 1,
type = 0u,
reserved = 0
}
staload "./frame.sats"
staload "kernel/bootinfo/multiboot.sats"
staload UN = "prelude/SATS/unsafe.sats"
implement containing_address(address) : frame_t =
@{
counter = $UN.cast{size_t}(address) / i2sz(PAGE_SIZE)
}
fn containing_area(area : memory_area_t) : frame_t = containing_address(ptr_add<uint8>(area.base_addr,area.length - i2sz(1)))
//FIX: function doesn't handle no frames left
fn choose_next_area{l,k : agz}(pf : !frame_allocator_t@l, bf : !boot_info_t @ k | p : ptr l, b : ptr k) : void = let
val length = get_memory_mappings_n(bf | b)
val next_free_frame = p->next_free_frame
fun loop {n,i : nat | i < n} {l : agz} .<n-i>. (bf : !boot_info_t @ l | b : ptr l, i : size_t i, n : size_t n) : memory_area_t = let
val entry = get_memory_mapping(bf | b ,i)
val fr = containing_area(entry)
in
if (entry.type = 1 && fr.num >= next_free_frame.num) then
entry
else if (i < n-1) then
loop (bf | b,succ(i),n)
else
entry //TODO: fix
end
in
if (length > 0) then //TODO: fix
p->current_area := loop(bf | b, i2sz(0), length);
if (p->current_area.length > 1) then
let
val start_frame = containing_address(p->current_area.base_addr)
in
if (p->next_free_frame.num < start_frame.num) then
p->next_free_frame := start_frame
end
end
local
var frame_allocator : frame_allocator_t
in
implement frame_allocator_init() : allocptr = let
extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (frame_allocator_t@l) // takeout proof UNSAFE:
prval (pf, fpf) = __assert (addr@frame_allocator)
val allocator = @{
next_free_frame = containing_address(the_null_ptr),
current_area = invalid_area
}
in
(pf, fpf | addr@frame_allocator)
end
end
implement allocate_frame(pf , bf | p,b) : frame_t =
if (p->current_area.type != 0u) then let
val area = p->current_area
val frame = @{ num = p->next_free_frame.num }
// last frame of current area
val last_frame_area = containing_area(area)
in
if (frame.num > last_frame_area.num) then (
// all frames of current area are used, switch to next area
choose_next_area(pf, bf | p,b);
allocate_frame(pf,bf | p,b)
) else if (frame.num > p->kernel_start.num && frame.num <= p->kernel_end.num) then (
// frame is used by kernel
p->next_free_frame := @{num = p->kernel_end.num + 1};
allocate_frame(pf,bf | p,b)
) else if (frame.num > p->multiboot_start.num && frame.num <= p->multiboot_end.num) then (
// frame is used by multiboot info structure
p->next_free_frame := @{num = p->multiboot_end.num + 1};
allocate_frame(pf,bf | p,b)
) else (
// frame is unused, increment `next_free_frame` and return it
p->next_free_frame.num := succ(p->next_free_frame.num);
frame
);
end
else
@{num = i2sz(0)} // No free frames left
implement deallocate_frame(p) : void = let
in
end
|
