Mainly refactoring

2 files changed, 47 insertions, 25 deletions

diff --git a/kernel/bootinfo/multiboot.dats b/kernel/bootinfo/multiboot.dats
index 6ea7b00..96d7f84 100644
--- a/kernel/bootinfo/multiboot.dats
+++ b/kernel/bootinfo/multiboot.dats
@@ -49,24 +49,25 @@ extern castfn ui2sz (n : uint) : [n : nat] size_t n
 
 //------------Memory------------------------
 
-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
+implement get_memory_mappings_n(pf | p) = let
+  val size = p->memory_map.tag.size 
+  val n_entries = (if(size >= 16u) then (size - 16u) / p->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) =  (
-  assertloc(n < get_memory_mappings_n(p));
-  $UN.ptr0_get<memory_area_t>(ptr_add<memory_area_t>(p.2->memory_map.entries,n))
+implement get_memory_mapping(pf | p,n) =  (
+  assertloc(n < get_memory_mappings_n(pf | p));
+  $UN.ptr0_get<memory_area_t>(ptr_add<memory_area_t>(p->memory_map.entries,n))
 )
 
+//TODO: use foreach with fwork to loop through memory maps
 implement print_memory_mappings(p) = let
-  val length = get_memory_mappings_n(p)
+  val length = get_memory_mappings_n(p.0 | p.2)
   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)
+    val entry = get_memory_mapping(p.0 | p.2 ,i)
   in
     if (entry.type = 1) then (
       print("   Start Address: ");
@@ -96,13 +97,37 @@ implement get_elf_header (p,n) = (
   $UN.ptr0_get<elf64_shdr_t>(ptr_add<elf64_shdr_t>(p.2->elf_tag.headers,n))
 )
 
+implement get_kernel_ranges(p) = let
+  val length = get_elf_headers_n(p)
+  fun loop {n,i : nat | i < n} .<n-i>. (p : !bootptr, i : size_t i,n : size_t n, min : Ptr, max : Ptr) : (Ptr,Ptr) = let
+    val header = get_elf_header(p,i)
+    val new_min = (if ((header.addr < min || min = the_null_ptr) && header.size != 0) then header.addr else min)
+    val end_p = ptr_add<uint8>(header.addr,header.size)
+    val new_max = (
+      if (end_p > max && header.size != 0) 
+        then $UN.cast2Ptr1(end_p) 
+      else max
+    )
+  in
+    if (i < n - 1) then
+      loop(p,succ(i),n,new_min,new_max)
+    else 
+      (new_min,new_max)
+  end
+
+in
+  if (length > 0) then
+    loop(p,i2sz(0),length,the_null_ptr,the_null_ptr)
+  else
+    (the_null_ptr,the_null_ptr)
+end
+
+implement get_bootinfo_ranges(p) = (p.2, ptr_add<uint8>(p.2,p.2->total_size))
+
 implement print_elf_headers(p) = let
   val length = get_elf_headers_n(p)
-  fun loop {n,i : nat | i < n} .<n-i>. (p : !bootptr, i : size_t i, n : size_t n, min : size_t, max : size_t) : void = let
+  fun loop {n,i : nat | i < n} .<n-i>. (p : !bootptr, i : size_t i, n : size_t n) : void = let
     val header = get_elf_header(p,i)
-    val a = $UN.cast{size_t}(header.addr)
-    val new_min = (if (a < min && header.size != 0) then a else min) : size_t
-    val new_max = (if (a + header.size > max && header.size != 0) then a + header.size else max) : size_t
   in
     print("   addr: ");
     print_hex(header.addr);
@@ -112,20 +137,13 @@ implement print_elf_headers(p) = let
     println_hex(header.flags);
       
     if (i < n - 1) then
-      loop(p,succ(i),n,new_min,new_max)
-    else (
-      print("Kernel start: ");
-      print_hex(new_min);
-      print(" end: ");
-      print_hex(new_max);
-      print(" size: ");
-      println!(new_max - new_min)
-    )
+      loop(p,succ(i),n)
+
   end
 in
   if (length > 0) then (
     println!("Elf section headers: ");
-    loop(p,i2sz(0),length,i2sz(0xFFFFFF),i2sz(0)))
+    loop(p,i2sz(0),length))
   else
     println!("No elf section headers")
 end
diff --git a/kernel/bootinfo/multiboot.sats b/kernel/bootinfo/multiboot.sats
index 3909fdd..963e2e6 100644
--- a/kernel/bootinfo/multiboot.sats
+++ b/kernel/bootinfo/multiboot.sats
@@ -5,7 +5,7 @@ typedef tag_t = @{
 }
 
 typedef memory_area_t = @{
-  base_addr = Ptr1, // Start of physical address
+  base_addr = Ptr, // Start of physical address
   length = [n : nat | n > 0 ] size_t n ,  // Size of memory region in bytes (64 bits)
   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
@@ -50,10 +50,14 @@ vtypedef bootptr  = [l : agz] (boot_info_t@l , boot_info_t@l -<lin,prf> void | p
 
 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_area_t
+fn get_memory_mappings_n {l : agz} (pf : !boot_info_t@l | p : ptr l) : [n:nat] size_t n
+fn get_memory_mapping {l:agz} (pf : !boot_info_t @ l | p : ptr l, n : size_t) : memory_area_t
 fn print_memory_mappings (p : !bootptr) : void
 
 fn get_elf_headers_n (p : !bootptr) : [n:nat] size_t n
 fn get_elf_header  (p : !bootptr, n : size_t) : elf64_shdr_t
 fn print_elf_headers (p : !bootptr) : void
+
+fn get_kernel_ranges (p : !bootptr) : (Ptr,Ptr) // (kernel start, kernel end)
+fn get_bootinfo_ranges (p : !bootptr) : (ptr,ptr) // (bootinfo start, bootinfo end)
+