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
124
125
126
127
128
129
130
131
|
#include "kernel/prelude/kernel_prelude.hats"
#define ATS_DYNLOADFLAG 0
staload "./frame.sats"
staload "kernel/bootinfo/multiboot.sats"
staload "lib/SATS/init.sats"
staload UN = "prelude/SATS/unsafe.sats"
assume frame_allocator = frame_allocator_t
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{k : agz}(bf : !boot_info_t @ k | b : ptr k, allocator : &frame_allocator_t) :<!wrt> void = let
val length = get_memory_mappings_n(bf | b)
val next_free_frame = allocator.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
allocator.current_area := loop(bf | b, i2sz(0), length);
if (allocator.current_area.length > 1) then
let
val start_frame = containing_address(allocator.current_area.base_addr)
in
if (allocator.next_free_frame.num < start_frame.num) then
allocator.next_free_frame := start_frame
end
end
local
var allocator_static : frame_allocator_t?
prval () = opt_none allocator_static
var allocator = uninitialized<frame_allocator_t>(allocator_static)
val allocator_ref = ref_make_viewptr{initializable frame_allocator_t} (view@allocator | addr@allocator)
in
implement frame_allocator_init(kernel_start, kernel_end, multiboot_start, multiboot_end, b) : void = let
val allocator = @{
next_free_frame = containing_address(the_null_ptr),
current_area = invalid_area,
kernel_start = containing_address(kernel_start),
kernel_end = containing_address(kernel_end),
multiboot_start = containing_address(multiboot_start),
multiboot_end = containing_address(multiboot_end)
} : frame_allocator_t
val (vbox pf | p) = ref_get_viewptr(allocator_ref)
in
if not p->initialized then let
prval () = opt_unnone p->obj
in
p->obj := allocator;
p->initialized := true;
(* choose_next_area(b.0 | b.2, !p); *)
let prval () = opt_some p->obj in end;
end
end
implement allocate_frame(bf | b) : frame_t = let
val (vbox pf | p) = ref_get_viewptr(allocator_ref)
in
if p->initialized then let
(* var allocator = p->obj *)
prval () = opt_unsome p->obj
in
(* if (allocator.current_area.type != 0u) then let *)
(* val area = allocator.current_area *)
(* val frame = @{ num = allocator.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(bf | b, allocator); *)
(* let prval () = opt_some allocator in end; *)
(* allocate_frame(bf | b) *)
(* ) else if (frame.num >= allocator.kernel_start.num && frame.num <= allocator.kernel_end.num) then ( *)
(* // frame is used by kernel *)
(* allocator.next_free_frame := @{num = allocator.kernel_end.num + 1}; *)
(* let prval () = opt_some allocator in end; *)
(* allocate_frame(bf | b) *)
(* ) else if (frame.num >= allocator.multiboot_start.num && frame.num <= allocator.multiboot_end.num) then ( *)
(* // frame is used by multiboot info structure *)
(* allocator.next_free_frame := @{num = allocator.multiboot_end.num + 1}; *)
(* let prval () = opt_some allocator in end; *)
(* allocate_frame(bf | b) *)
(* ) else ( *)
(* // frame is unused, increment `next_free_frame` and return it *)
(* allocator.next_free_frame.num := succ(allocator.next_free_frame.num); *)
(* let prval () = opt_some allocator in end; *)
(* frame *)
(* ); *)
(* end *)
(* else *)
(* let prval () = opt_some allocator in end; *)
(* @{num = i2sz(0)} // No free frames left *)
let prval () = opt_some p->obj in end;
@{num = i2sz(0)}
end
else
@{num = i2sz(0)} // No free frames left
end
end
implement deallocate_frame(p) : void = let
in
end
|
