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
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
|
#include "kernel/prelude/kernel_prelude.hats"
#define ATS_DYNLOADFLAG 0
staload "./multiboot.sats"
staload "lib/SATS/init.sats"
staload "lib/DATS/init.dats"
staload UN = "prelude/SATS/unsafe.sats"
local
extern castfn ui2sz (n : uint) :<> [n : nat] size_t n
extern fn _get_memory_mappings_n(boot_info : !boot_info_t):<> [n:nat] size_t n
extern fn _get_memory_mapping(boot_info : !boot_info_t,n : size_t):<> memory_area_t
extern fn _print_memory_mappings(boot_info : !boot_info_t):<!wrt> void
in
local
// Static variable
var _v : boot_info_t?
prval () = opt_none _v
var v = uninitialized<boot_info_t>(_v)
// Reference to writer
val bootinfo_ref = ref_make_viewptr{initializable boot_info_t} (view@v | addr@v)
in
implement init (p : Ptr1) = let
val total_size = g1ofg0($UN.ptr0_get<uint>(p))
fun loop {n,i : nat | i < n} .<n-i>. (boot_info : &boot_info_t? >> boot_info_t, p : ptr, i: uint i, n: uint n):<!wrt> void = let
extern castfn unsafe_init(x : &boot_info_t? >> boot_info_t) :<> void
val type = $UN.ptr0_get<uint>(p)
val size = $UN.ptr0_get<uint>(ptr_succ<uint>(p))
val next = (if (size % 8u != 0) then size + 8u - (size % 8u) else size) : uint
in
case+ type of
| 6u => (
boot_info.memory_map := $UN.ptr0_get<memory_areas_t>(p);
boot_info.memory_map.entries := ptr_add<uint32>(p,4)
)
| 9u => (
boot_info.elf_tag := $UN.ptr0_get<elf_tag_t>(p);
boot_info.elf_tag.headers := ptr_add<uint32>(p,5);
)
| _ => ();
if (i < n - 1u) then
loop(boot_info,ptr_add<uint8>(p, next),succ(i),n)
else
unsafe_init(boot_info)
end
implement initialize$fwork<boot_info_t>(v) = (
if (total_size > 0u) then (
v.total_size := total_size;
loop(v, ptr_add<uint32>(p,2),0u,total_size);
let prval () = opt_some v in true end)
else
let prval () = opt_none v in false end
)
in end
implement get_memory_mappings_n() = let
implement exec$fwork<boot_info_t><size_t>(v,_) = _get_memory_mappings_n(v)
in
exec<boot_info_t>(bootinfo_ref,i2sz(0))
end
implement get_memory_mapping(n) = let
implement exec$fwork<boot_info_t><memory_area_t>(v,_) = _get_memory_mapping(v,n)
in
exec<boot_info_t><memory_area_t>(bootinfo_ref,invalid_area)
end
implement print_memory_mappings() = let
implement exec_void$fwork<boot_info_t>(v) = _print_memory_mappings(v)
in
exec_void<boot_info_t>(bootinfo_ref)
end
end
//------------Memory------------------------
implement _get_memory_mappings_n(boot_info) = let
val size = boot_info.memory_map.tag.size
val n_entries = (if(size >= 16u) then (size - 16u) / boot_info.memory_map.entry_size else 0u) : uint
in
ui2sz n_entries
end
implement _get_memory_mapping(boot_info,n) = (
(* assertloc(n < get_memory_mappings_n(pf | p)); *)
$UN.ptr0_get<memory_area_t>(ptr_add<memory_area_t>(boot_info.memory_map.entries,n))
)
//TODO: use foreach with fwork to loop through memory maps
implement _print_memory_mappings(boot_info) = let
val length = _get_memory_mappings_n(boot_info)
fun loop {n,i : nat | i < n} .<n-i>. (i : size_t i, n : size_t n):<!wrt> void = let
val entry = _get_memory_mapping(boot_info,i)
in
if (entry.type = 1) then (
print(" Start Address: ");
print_hex(entry.base_addr);
print(", Length: ");
println_hex(entry.length);
);
if (i < n-1) then
loop (succ(i),n)
end
in
if (length > 0) then (
println!("Memory areas:");
loop(i2sz(0),length))
else
println!("No memory mappings")
end
end
//----------------------------------------------
(* //---------------------ELF---------------------- *)
(**)
(* implement get_elf_headers_n(p) = ui2sz p.2->elf_tag.num *)
(**)
(* implement get_elf_header (p,n) = ( *)
(* assertloc(n < get_elf_headers_n(p)); *)
(* $UN.ptr0_get<elf64_shdr_t>(ptr_add<elf64_shdr_t>(p.2->elf_tag.headers,n)) *)
(* ) *)
(**)
(* implement get_kernel_ranges(p) = let *)
(* val length = get_elf_headers_n(p) *)
(* fun loop {n,i : nat | i < n} .<n-i>. (p : !bootptr, i : size_t i,n : size_t n, min : Ptr, max : Ptr) : (Ptr,Ptr) = let *)
(* val header = get_elf_header(p,i) *)
(* val new_min = (if ((header.addr < min || min = the_null_ptr) && header.size != 0) then header.addr else min) *)
(* val end_p = ptr_add<uint8>(header.addr,header.size) *)
(* val new_max = ( *)
(* if (end_p > max && header.size != 0) *)
(* then $UN.cast2Ptr1(end_p) *)
(* else max *)
(* ) *)
(* in *)
(* if (i < n - 1) then *)
(* loop(p,succ(i),n,new_min,new_max) *)
(* else *)
(* (new_min,new_max) *)
(* end *)
(**)
(* in *)
(* if (length > 0) then *)
(* loop(p,i2sz(0),length,the_null_ptr,the_null_ptr) *)
(* else *)
(* (the_null_ptr,the_null_ptr) *)
(* end *)
(**)
(* implement get_multiboot_ranges(p) = (p.2, $UN.cast2Ptr1(ptr_add<uint8>(p.2,p.2->total_size))) *)
(**)
(* implement print_elf_headers(p) = let *)
(* val length = get_elf_headers_n(p) *)
(* fun loop {n,i : nat | i < n} .<n-i>. (p : !bootptr, i : size_t i, n : size_t n) : void = let *)
(* val header = get_elf_header(p,i) *)
(* in *)
(* print(" addr: "); *)
(* print_hex(header.addr); *)
(* print(", size: "); *)
(* print_hex(header.size); *)
(* print(", flags: "); *)
(* println_hex(header.flags); *)
(* *)
(* if (i < n - 1) then *)
(* loop(p,succ(i),n) *)
(**)
(* end *)
(* in *)
(* if (length > 0) then ( *)
(* println!("Elf section headers: "); *)
(* loop(p,i2sz(0),length)) *)
(* else *)
(* println!("No elf section headers") *)
(* end *)
(**)
(* //---------------------------------------------- *)
(**)
|
