From ab383485291164f7bc78b88787271dd1b85c0d73 Mon Sep 17 00:00:00 2001 From: Xander Date: Sat, 15 Jul 2023 00:31:51 +0200 Subject: Boot info memory mapping implementation --- Makefile | 2 +- kernel/main.dats | 25 ++++++++--------- kernel/multiboot.dats | 62 ++++++++++++++++++++++++++++++++++++++++++ kernel/multiboot.sats | 34 +++++++++++++++++++++++ kernel/prelude/DATS/print.dats | 12 ++++++++ 5 files changed, 120 insertions(+), 15 deletions(-) create mode 100644 kernel/multiboot.dats create mode 100644 kernel/multiboot.sats diff --git a/Makefile b/Makefile index 19bca78..f56a430 100644 --- a/Makefile +++ b/Makefile @@ -22,7 +22,7 @@ CLFAGS_ATS := CFLAGS_ATS += -D_ATS_CCOMP_RUNTIME_NONE_ CFLAGS_ATS += -D_ATS_CCOMP_EXCEPTION_NONE_ -CFLAGS=-ffreestanding -mcmodel=large -mno-red-zone -mgeneral-regs-only -m64 -fpack-struct +CFLAGS=-ffreestanding -mcmodel=large -mno-red-zone -mgeneral-regs-only -m64 -fpack-struct -fno-stack-protector .PHONY: all clean run iso diff --git a/kernel/main.dats b/kernel/main.dats index b35387f..7e6bfe7 100644 --- a/kernel/main.dats +++ b/kernel/main.dats @@ -3,10 +3,14 @@ #define ATS_DYNLOADFLAG 0 staload "kernel/interrupts/idt.sats" +staload "kernel/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"); @@ -17,25 +21,18 @@ extern castfn char_arr2string {n:nat} (arr : &(@[char][n])) : string n extern fun breakpoint() :void = "mac#" -extern fun main(p : ptr) : void = "ext#" +extern fun main(p : Ptr1) : void = "ext#" implement main(p) = let - prval size = $UN.ptr0_get(ptr_add(p, - 8 + - 16 + - 16 + - 4 + 4 - (* 16 + *) - (* 8 + *) - (* 32 + *) - (* 16 + 24 + 24 + 24 + 24 + 24 + 48 + // memory map *) - (* 792 + // elf *) - (* 4 + 4 + 4 *) - )) in clear_screen(); println!("Start"); - (* println!(size); *) + + // Initialize boot info struct + let + val bootptr = boot_info_init(p) + prval () = bootptr.1(bootptr.0) + in end; // Initialize interrupt table idt_init(); 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(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 new file mode 100644 index 0000000..9cbc4b4 --- /dev/null +++ b/kernel/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 + +fun get_memory_mappings_n (p : !bootptr) : size_t + +fun get_memory_mapping (p : !bootptr, n : size_t) : memory_entry_t diff --git a/kernel/prelude/DATS/print.dats b/kernel/prelude/DATS/print.dats index 0b5c38a..c6cd220 100644 --- a/kernel/prelude/DATS/print.dats +++ b/kernel/prelude/DATS/print.dats @@ -28,15 +28,27 @@ implement print_uint8 (n) = put_string(itoa($UN.cast{int}(n),10)) extern fun print_uint64 (n : uint64) : void implement print_uint64 (n) = put_string(itoa($UN.cast{int}(n),10)) +extern fun print_size_t (n : size_t) : void +implement print_size_t (n) = put_string(itoa($UN.cast{int}(n),10)) + +extern fun print_uint (n : uint) : void +implement print_uint (n) = put_string(itoa($UN.cast{int}(n),10)) + overload print with put_string of 1 overload print with print_int of 1 overload print with print_uint32 of 1 overload print with print_uint64 of 1 overload print with print_uint16 of 1 overload print with print_uint8 of 1 +overload print with print_size_t of 1 +overload print with print_uint of 1 extern fun {a : t@ype} println_base {n:nat | n > 1 && n < 33} (n :a, base : int n) : void implement{a} println_base(n,base) = println!(itoa($UN.cast{int}(n), base)) +extern fun {a : t@ype} print_base {n:nat | n > 1 && n < 33} (n :a, base : int n) : void +implement{a} print_base(n,base) = put_string(itoa($UN.cast{int}(n), base)) + macdef println_hex(s) = (put_string "0x"; println_base(,(s), 16)) +macdef print_hex(s) = (put_string "0x"; print_base(,(s), 16)) macdef assertloc(tf) = assert_errmsg (,(tf), $mylocation) -- cgit v1.2.3