diff options
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/bootinfo/multiboot.dats (renamed from kernel/multiboot.dats) | 27 | ||||
-rw-r--r-- | kernel/bootinfo/multiboot.sats (renamed from kernel/multiboot.sats) | 6 | ||||
-rw-r--r-- | kernel/main.dats | 24 |
3 files changed, 39 insertions, 18 deletions
diff --git a/kernel/multiboot.dats b/kernel/bootinfo/multiboot.dats index bc3b552..1128352 100644 --- a/kernel/multiboot.dats +++ b/kernel/bootinfo/multiboot.dats @@ -1,4 +1,4 @@ -#include "./prelude/kernel_prelude.hats" +#include "kernel/prelude/kernel_prelude.hats" #define ATS_DYNLOADFLAG 0 @@ -41,7 +41,7 @@ end end -extern castfn ui2sz (n : uint) : size_t +extern castfn ui2sz (n : uint) : [n : nat] size_t n implement get_memory_mappings_n(p) = let val size = p.2->memory_map.tag.size @@ -50,7 +50,7 @@ in ui2sz n_entries end -// TODO: here use optional datatype (fix runtime ) +// TODO: here use optional datatype (fix runtime alloc) implement get_memory_mapping(p,n) = let val size = p.2->memory_map.tag.size @@ -60,3 +60,24 @@ in $UN.ptr0_get<memory_entry_t>(ptr_add<memory_map_t>(p.2->memory_map.entries,n)) end +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 + loop(p,i2sz(0),length) + else + println!("No memory mappings") +end diff --git a/kernel/multiboot.sats b/kernel/bootinfo/multiboot.sats index 9cbc4b4..0507241 100644 --- a/kernel/multiboot.sats +++ b/kernel/bootinfo/multiboot.sats @@ -29,6 +29,6 @@ vtypedef bootptr = [l : agz] (boot_info_t@l , boot_info_t@l -<lin,prf> void | p fun boot_info_init(p : Ptr1) : bootptr -fun get_memory_mappings_n (p : !bootptr) : size_t - -fun get_memory_mapping (p : !bootptr, n : size_t) : memory_entry_t +fn get_memory_mappings_n (p : !bootptr) : [n:nat] size_t n +fn get_memory_mapping (p : !bootptr, n : size_t) : memory_entry_t +fn print_memory_mappings (p : !bootptr) : void diff --git a/kernel/main.dats b/kernel/main.dats index 7e6bfe7..67afb7c 100644 --- a/kernel/main.dats +++ b/kernel/main.dats @@ -3,14 +3,11 @@ #define ATS_DYNLOADFLAG 0 staload "kernel/interrupts/idt.sats" -staload "kernel/multiboot.sats" +staload "kernel/bootinfo/multiboot.sats" staload "lib/SATS/writer.sats" staload UN = "prelude/SATS/unsafe.sats" -extern praxi c (p : ptr) : [l : agz] strptr l -extern prfun eat(p : strptr) : void - %{^ void breakpoint(){ __asm__("int3"); @@ -23,16 +20,13 @@ extern fun breakpoint() :void = "mac#" extern fun main(p : Ptr1) : void = "ext#" implement main(p) = let -in - - clear_screen(); - println!("Start"); + val () = clear_screen() // Initialize boot info struct - let - val bootptr = boot_info_init(p) - prval () = bootptr.1(bootptr.0) - in end; + val bootptr = boot_info_init(p) +in + + print_memory_mappings(bootptr); // Initialize interrupt table idt_init(); @@ -40,6 +34,12 @@ in // Throws breakpoint exception breakpoint(); + println!("End"); + let + prval () = bootptr.1(bootptr.0) + in end + + end |