2 files changed, 117 insertions, 0 deletions
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<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) : [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<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/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 -<lin,prf> 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