From e2f3bfc0973c151951531b1715c53d14e8656d92 Mon Sep 17 00:00:00 2001 From: Xander Date: Sat, 15 Jul 2023 18:04:00 +0200 Subject: Print memory mappings --- kernel/bootinfo/multiboot.dats | 83 ++++++++++++++++++++++++++++++++++++++++++ kernel/bootinfo/multiboot.sats | 34 +++++++++++++++++ kernel/main.dats | 24 ++++++------ kernel/multiboot.dats | 62 ------------------------------- kernel/multiboot.sats | 34 ----------------- 5 files changed, 129 insertions(+), 108 deletions(-) create mode 100644 kernel/bootinfo/multiboot.dats create mode 100644 kernel/bootinfo/multiboot.sats delete mode 100644 kernel/multiboot.dats delete mode 100644 kernel/multiboot.sats diff --git a/kernel/bootinfo/multiboot.dats b/kernel/bootinfo/multiboot.dats new file mode 100644 index 0000000..1128352 --- /dev/null +++ b/kernel/bootinfo/multiboot.dats @@ -0,0 +1,83 @@ +#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(p) + + fun loop {l : agz} (pf : !boot_info_t@l | boot_p : ptr l , p : ptr): void = let + val type = $UN.ptr0_get(p) + val size = $UN.ptr0_get(ptr_succ(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(p); + boot_p->memory_map.entries := ptr_add(p,4) + ) + | _ => (); + + if (type != 0u) then + loop(pf | boot_p, ptr_add(p, next)) + end + +in + boot_info.total_size := total_size; + loop(pf | addr@boot_info, ptr_add(p,2)); + + (pf , fpf | addr@boot_info) +end + +end + +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 + 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) = 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(ptr_add(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} .. (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/bootinfo/multiboot.sats b/kernel/bootinfo/multiboot.sats new file mode 100644 index 0000000..0507241 --- /dev/null +++ b/kernel/bootinfo/multiboot.sats @@ -0,0 +1,34 @@ + +typedef tag_t = @{ + type = uint32, // Identifier of tag + size = [n : nat | n >= 8] uint n // Size of tag (not including padding) +} + +typedef memory_entry_t = @{ + base_addr = Ptr1, // Start of physical address + length = uint64, // Size of memory region in bytes + type = uint, // Variety of address range represented. 1: available RAM, 3: usable memory holding ACPI information, + // 4: reserved memory (preserved on hibernation), Other: reserved area + reserved = uint 0 +} + +typedef memory_map_t = @{ + tag = tag_t, + entry_size = [n : nat | n > 0 && n % 8 == 0] uint n, + entry_version = uint, + entries = ptr // Pointer to entries +} + + +typedef boot_info_t = @{ + total_size = uint, // total size of boot information + memory_map = memory_map_t +} + +vtypedef bootptr = [l : agz] (boot_info_t@l , boot_info_t@l - void | ptr l) + +fun boot_info_init(p : Ptr1) : bootptr + +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 diff --git a/kernel/multiboot.dats b/kernel/multiboot.dats deleted file mode 100644 index bc3b552..0000000 --- a/kernel/multiboot.dats +++ /dev/null @@ -1,62 +0,0 @@ -#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(p) - - fun loop {l : agz} (pf : !boot_info_t@l | boot_p : ptr l , p : ptr): void = let - val type = $UN.ptr0_get(p) - val size = $UN.ptr0_get(ptr_succ(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(p); - boot_p->memory_map.entries := ptr_add(p,4) - ) - | _ => (); - - if (type != 0u) then - loop(pf | boot_p, ptr_add(p, next)) - end - -in - boot_info.total_size := total_size; - loop(pf | addr@boot_info, ptr_add(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(ptr_add(p.2->memory_map.entries,n)) -end - diff --git a/kernel/multiboot.sats b/kernel/multiboot.sats deleted file mode 100644 index 9cbc4b4..0000000 --- a/kernel/multiboot.sats +++ /dev/null @@ -1,34 +0,0 @@ - -typedef tag_t = @{ - type = uint32, // Identifier of tag - size = [n : nat | n >= 8] uint n // Size of tag (not including padding) -} - -typedef memory_entry_t = @{ - base_addr = Ptr1, // Start of physical address - length = uint64, // Size of memory region in bytes - type = uint, // Variety of address range represented. 1: available RAM, 3: usable memory holding ACPI information, - // 4: reserved memory (preserved on hibernation), Other: reserved area - reserved = uint 0 -} - -typedef memory_map_t = @{ - tag = tag_t, - entry_size = [n : nat | n > 0 && n % 8 == 0] uint n, - entry_version = uint, - entries = ptr // Pointer to entries -} - - -typedef boot_info_t = @{ - total_size = uint, // total size of boot information - memory_map = memory_map_t -} - -vtypedef bootptr = [l : agz] (boot_info_t@l , boot_info_t@l - void | ptr l) - -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 -- cgit v1.2.3