more refactoring and implemented exec_init

1 files changed, 104 insertions, 68 deletions

diff --git a/kernel/bootinfo/multiboot.dats b/kernel/bootinfo/multiboot.dats
index cf72ba7..ff10c40 100644
--- a/kernel/bootinfo/multiboot.dats
+++ b/kernel/bootinfo/multiboot.dats
@@ -9,10 +9,16 @@ staload UN = "prelude/SATS/unsafe.sats"
 
 local
 
+  // Private function
   extern castfn ui2sz (n : uint) :<> [n : nat] size_t n
-  extern fn _get_memory_mappings_n(boot_info : !boot_info_t):<> [n:nat] size_t n
-  extern fn _get_memory_mapping(boot_info : !boot_info_t,n : size_t):<> memory_area_t
-  extern fn _print_memory_mappings(boot_info : !boot_info_t):<!wrt> void
+  extern fn _get_memory_mappings_n(boot_info: !boot_info_t):<> [n:nat] size_t n
+  extern fn _get_memory_mapping(boot_info: !boot_info_t,n : size_t):<> memory_area_t
+  extern fn _print_memory_mappings(boot_info: !boot_info_t):<!wrt> void
+  extern fn _get_elf_headers_n(boot_info: !boot_info_t):<> [n:nat] size_t n
+  extern fn _get_elf_header(boot_info: !boot_info_t, n: size_t):<> elf64_shdr_t
+  extern fn _print_elf_headers(boot_info: !boot_info_t):<!wrt> void
+  extern fn _get_kernel_ranges(boot_info: !boot_info_t):<> (Ptr,Ptr)
+  extern fn _get_multiboot_ranges(boot_info: !boot_info_t):<> (Ptr0,Ptr0)
 
 in
 
@@ -53,6 +59,7 @@ in
 
       implement initialize$fwork<boot_info_t>(v) = (
         if (total_size > 0u) then (
+          v.address := p;
           v.total_size := total_size;
           $effmask_ntm(loop(v, ptr_add<uint32>(p,2)));
           let prval () = opt_some v in true end)
@@ -81,6 +88,36 @@ in
       exec_void<boot_info_t>(bootinfo_ref)
     end
 
+    implement get_elf_headers_n() = let
+      implement exec$fwork<boot_info_t><size_t>(v) = _get_elf_headers_n(v)
+    in
+      exec<boot_info_t><size_t>(bootinfo_ref)
+    end
+
+    implement get_elf_header(n) = let
+      implement exec$fwork<boot_info_t><elf64_shdr_t>(v) = _get_elf_header(v,n)
+    in
+      exec<boot_info_t><elf64_shdr_t>(bootinfo_ref)
+    end
+
+    implement print_elf_headers() = let
+      implement exec_void$fwork<boot_info_t>(v) = _print_elf_headers(v)
+    in
+      exec_void<boot_info_t>(bootinfo_ref)
+    end
+
+    implement get_kernel_ranges() = let
+      implement exec$fwork<boot_info_t><(Ptr,Ptr)>(v) = _get_kernel_ranges(v)
+    in
+      exec<boot_info_t><(Ptr,Ptr)>(bootinfo_ref)
+    end
+
+    implement get_multiboot_ranges() = let
+      implement exec$fwork<boot_info_t><(Ptr0,Ptr0)>(v) = _get_multiboot_ranges(v)
+    in
+      exec<boot_info_t><(Ptr0,Ptr0)>(bootinfo_ref)
+    end
+
   end
 
   //------------Memory------------------------
@@ -93,7 +130,7 @@ in
   end
 
   implement _get_memory_mapping(boot_info,n) =  (
-    (* assertloc(n < get_memory_mappings_n(pf | p)); *)
+    assertloc (n < _get_memory_mappings_n boot_info);
     $UN.ptr0_get<memory_area_t>(ptr_add<memory_area_t>(boot_info.memory_map.entries,n))
   )
 
@@ -120,69 +157,68 @@ in
       println!("No memory mappings")
   end
 
+
+  //----------------------------------------------
+
+  //---------------------ELF----------------------
+
+  implement _get_elf_headers_n(boot_info) = ui2sz boot_info.elf_tag.num
+
+  implement _get_elf_header (boot_info,n) = (
+    assertloc (n < _get_elf_headers_n boot_info);
+    $UN.ptr0_get<elf64_shdr_t>(ptr_add<elf64_shdr_t>(boot_info.elf_tag.headers,n))
+  )
+
+  implement _get_kernel_ranges(boot_info) = let
+    val length = _get_elf_headers_n(boot_info)
+    fun loop {n,i : nat | i < n} .<n-i>. (i : size_t i,n : size_t n, min : Ptr, max : Ptr) :<> (Ptr,Ptr) = let
+      val header = _get_elf_header(boot_info,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(succ(i),n,new_min,new_max)
+      else 
+        (new_min,new_max)
+    end
+
+  in
+    if (length > 0) then
+      loop(i2sz(0),length,the_null_ptr,the_null_ptr)
+    else
+      (the_null_ptr,the_null_ptr)
+  end
+
+  implement _get_multiboot_ranges(boot_info) = (boot_info.address, $UN.cast2Ptr1(ptr_add<uint8>(boot_info.address,boot_info.total_size)))
+
+  implement _print_elf_headers(boot_info) = let
+    val length = _get_elf_headers_n(boot_info)
+    fun loop {n,i : nat | i < n} .<n-i>. (i : size_t i, n : size_t n) :<!wrt> void = let
+      val header = _get_elf_header(boot_info,i)
+    in
+      print("   addr: ");
+      print_hex(header.addr);
+      print(", size: ");
+      print_hex(header.size);
+      print(", flags: ");
+      println_hex(header.flags);
+        
+      if (i < n - 1) then
+        loop(succ(i),n)
+
+    end
+  in
+    if (length > 0) then (
+      println!("Elf section headers: ");
+      loop(i2sz(0),length))
+    else
+      println!("No elf section headers")
+  end
+
 end
 
-//----------------------------------------------
-
-(* //---------------------ELF---------------------- *)
-
-(* implement get_elf_headers_n(p) = ui2sz p.2->elf_tag.num *)
-(**)
-(* implement get_elf_header (p,n) = ( *)
-(*   assertloc(n < get_elf_headers_n(p)); *)
-(*   $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_multiboot_ranges(p) = (p.2, $UN.cast2Ptr1(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) : void = let *)
-(*     val header = get_elf_header(p,i) *)
-(*   in *)
-(*     print("   addr: "); *)
-(*     print_hex(header.addr); *)
-(*     print(", size: "); *)
-(*     print_hex(header.size); *)
-(*     print(", flags: "); *)
-(*     println_hex(header.flags); *)
-(*        *)
-(*     if (i < n - 1) then *)
-(*       loop(p,succ(i),n) *)
-(**)
-(*   end *)
-(* in *)
-(*   if (length > 0) then ( *)
-(*     println!("Elf section headers: "); *)
-(*     loop(p,i2sz(0),length)) *)
-(*   else *)
-(*     println!("No elf section headers") *)
-(* end *)
-(**)
-(* //---------------------------------------------- *)
-(**)