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
|
#include "kernel/prelude/kernel_prelude.hats"
#define ATS_DYNLOADFLAG 0
staload "./multiboot.sats"
staload UN = "prelude/SATS/unsafe.sats"
local
var boot_info : boot_info_t
in
implement boot_info_init (p : Ptr1) = let
extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (boot_info_t@l) // takeout proof UNSAFE:
prval (pf, fpf) = __assert (addr@boot_info)
val total_size = $UN.ptr0_get<uint>(p)
fun loop {l : agz} (pf : !boot_info_t@l | boot_p : ptr l , p : ptr): void = let
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_p->memory_map := $UN.ptr0_get<memory_areas_t>(p);
boot_p->memory_map.entries := ptr_add<uint32>(p,4)
)
| 9u => (
boot_p->elf_tag := $UN.ptr0_get<elf_tag_t>(p);
boot_p->elf_tag.headers := ptr_add<uint32>(p,5);
)
| _ => ();
if (type != 0u) then
loop(pf | boot_p, ptr_add<uint8>(p, next))
end
in
boot_info.total_size := total_size;
loop(pf | addr@boot_info, ptr_add<uint32>(p,2));
(pf , fpf | addr@boot_info)
end
end
extern castfn ui2sz (n : uint) : [n : nat] size_t n
//------------Memory------------------------
implement get_memory_mappings_n(p) = let
val size = p.2->memory_map.tag.size
val n_entries = (if(size >= 16u) then (size - 16u) / p.2->memory_map.entry_size else 0u) : uint
in
ui2sz n_entries
end
// TODO: here use optional datatype (fix runtime alloc)
implement get_memory_mapping(p,n) = (
assertloc(n < get_memory_mappings_n(p));
$UN.ptr0_get<memory_area_t>(ptr_add<memory_area_t>(p.2->memory_map.entries,n))
)
implement print_memory_mappings(p) = let
val length = get_memory_mappings_n(p)
fun loop {n,i : nat | i < n} .<n-i>. (p : !bootptr, i : size_t i, n : size_t n) : void = let
val entry = get_memory_mapping(p,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 (p,succ(i),n)
end
in
if (length > 0) then (
println!("Memory areas:");
loop(p,i2sz(0),length))
else
println!("No memory mappings")
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 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, min : size_t, max : size_t) : void = let
val header = get_elf_header(p,i)
val a = $UN.cast{size_t}(header.addr)
val new_min = (if (a < min && header.size != 0) then a else min) : size_t
val new_max = (if (a + header.size > max && header.size != 0) then a + header.size else max) : size_t
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,new_min,new_max)
else (
print("Kernel start: ");
print_hex(new_min);
print(" end: ");
print_hex(new_max);
print(" size: ");
println!(new_max - new_min)
)
end
in
if (length > 0) then (
println!("Elf section headers: ");
loop(p,i2sz(0),length,i2sz(0xFFFFFF),i2sz(0)))
else
println!("No elf section headers")
end
//----------------------------------------------
|
