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
|
#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_map_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_entry_t>(ptr_add<memory_entry_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) : 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
//----------------------------------------------
|
