diff options
Diffstat (limited to 'kernel/multiboot.dats')
-rw-r--r-- | kernel/multiboot.dats | 62 |
1 files changed, 62 insertions, 0 deletions
diff --git a/kernel/multiboot.dats b/kernel/multiboot.dats new file mode 100644 index 0000000..bc3b552 --- /dev/null +++ b/kernel/multiboot.dats @@ -0,0 +1,62 @@ +#include "./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<uint>(p,4) + ) + | _ => (); + + 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) : size_t + +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 ) + +implement get_memory_mapping(p,n) = let + val size = p.2->memory_map.tag.size + val n_entries = ui2sz (if(size >= 16u) then (size - 16u) / p.2->memory_map.entry_size else 0u) +in + assertloc(n < n_entries); + $UN.ptr0_get<memory_entry_t>(ptr_add<memory_map_t>(p.2->memory_map.entries,n)) +end + |