aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorXander <xander@biltopia.org>2023-07-15 00:31:51 +0200
committerXander <xander@biltopia.org>2023-07-15 00:31:51 +0200
commitab383485291164f7bc78b88787271dd1b85c0d73 (patch)
tree2c94f258cda82214bf1834a56571d3b8487f652c
parent5ad68a0c087d21fa1d0f82bea1550169f1e4c1aa (diff)
downloadats-os-ab383485291164f7bc78b88787271dd1b85c0d73.tar.xz
ats-os-ab383485291164f7bc78b88787271dd1b85c0d73.zip
Boot info memory mapping implementation
-rw-r--r--Makefile2
-rw-r--r--kernel/main.dats25
-rw-r--r--kernel/multiboot.dats62
-rw-r--r--kernel/multiboot.sats34
-rw-r--r--kernel/prelude/DATS/print.dats12
5 files changed, 120 insertions, 15 deletions
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<strptr>(ptr_add<uint8>(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<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
+
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 -<lin,prf> 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)