optional implementation of multboot 1

2 files changed, 176 insertions, 141 deletions

diff --git a/kernel/bootinfo/multiboot.dats b/kernel/bootinfo/multiboot.dats
index 9eee595..0653184 100644
--- a/kernel/bootinfo/multiboot.dats
+++ b/kernel/bootinfo/multiboot.dats
@@ -3,150 +3,186 @@
 #define ATS_DYNLOADFLAG 0
 
 staload "./multiboot.sats"
+staload "lib/SATS/init.sats"
+staload "lib/DATS/init.dats"
 staload UN = "prelude/SATS/unsafe.sats"
 
 local
 
-var boot_info : boot_info_t
+  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
 
 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_areas_t>(p); 
-               boot_p->memory_map.entries := ptr_add<uint32>(p,4)
-              )
-      | 9u => (
-               boot_p->elf_tag := $UN.ptr0_get<elf_tag_t>(p);
-               boot_p->elf_tag.headers := ptr_add<uint32>(p,5);
-              )
-      | _ => ();
-
-    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
-
-//------------Memory------------------------
-
-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)
+  local
+    // Static variable
+    var _v : boot_info_t?
+    prval () = opt_none _v
+    var v = uninitialized<boot_info_t>(_v)
+    // Reference to writer
+    val bootinfo_ref = ref_make_viewptr{initializable boot_info_t} (view@v | addr@v)
+  in
 
-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))
-)
+    implement init (p : Ptr1) = let
+      extern castfn unsafe_init(x : &boot_info_t? >> boot_info_t) :<> void
+      val total_size = $UN.ptr0_get<uint>(p)
+
+      fun loop (boot_info : &boot_info_t? >> boot_info_t, p : ptr):<!wrt,!ntm> 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_info.memory_map := $UN.ptr0_get<memory_areas_t>(p); 
+                   boot_info.memory_map.entries := ptr_add<uint32>(p,4)
+                  )
+          | 9u => (
+                   boot_info.elf_tag := $UN.ptr0_get<elf_tag_t>(p);
+                   boot_info.elf_tag.headers := ptr_add<uint32>(p,5);
+                  )
+          | _ => ();
+
+        if (type != 0u) then
+          loop(boot_info,ptr_add<uint8>(p, next))
+        else
+          unsafe_init(boot_info)
+      end
+
+      val (vbox pf | boot_p) = ref_get_viewptr(bootinfo_ref)
+    in
+      if (not boot_p->initialized) then 
+        let
+          prval ()  = opt_unnone boot_p->obj
+          val ()    = boot_p->obj.total_size := total_size
+          val ()    = loop(boot_p->obj, ptr_add<uint32>(p,2))
+          val ()    = boot_p->initialized := true
+          prval ()  = opt_some boot_p->obj
+        in end
+    end
+
+    implement get_memory_mappings_n() = let
+      implement exec$fwork<boot_info_t><size_t>(v,_) = _get_memory_mappings_n(v)
+    in
+      exec<boot_info_t>(bootinfo_ref,i2sz(0))
+    end
+
+    implement get_memory_mapping(n) = let
+      implement exec$fwork<boot_info_t><memory_area_t>(v,_) = _get_memory_mapping(v,n)
+    in
+      exec<boot_info_t><memory_area_t>(bootinfo_ref,invalid_area)
+    end
+
+    implement print_memory_mappings() = let
+      implement exec_void$fwork<boot_info_t>(v) = _print_memory_mappings(v)
+    in
+      exec_void<boot_info_t>(bootinfo_ref)
+    end
 
-//TODO: use foreach with fwork to loop through memory maps
-implement print_memory_mappings(p) = let
-  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.0 | p.2 ,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 (
-    println!("Memory areas:");
-    loop(p,i2sz(0),length))
-  else
-    println!("No memory mappings")
-end
 
-//----------------------------------------------
+  //------------Memory------------------------
 
-//---------------------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
-    )
+  implement _get_memory_mappings_n(boot_info) = let
+    val size = boot_info.memory_map.tag.size 
+    val n_entries = (if(size >= 16u) then (size - 16u) / boot_info.memory_map.entry_size else 0u) : uint
   in
-    if (i < n - 1) then
-      loop(p,succ(i),n,new_min,new_max)
-    else 
-      (new_min,new_max)
+    ui2sz n_entries
   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)
+  implement _get_memory_mapping(boot_info,n) =  (
+    (* assertloc(n < get_memory_mappings_n(pf | p)); *)
+    $UN.ptr0_get<memory_area_t>(ptr_add<memory_area_t>(boot_info.memory_map.entries,n))
+  )
+
+  //TODO: use foreach with fwork to loop through memory maps
+  implement _print_memory_mappings(boot_info) = let
+    val length = _get_memory_mappings_n(boot_info)
+    fun loop {n,i : nat | i < n} .<n-i>. (i : size_t i, n : size_t n):<!wrt> void = let 
+      val entry = _get_memory_mapping(boot_info,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 (succ(i),n)
+    end
   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)
-
+    if (length > 0) then (
+      println!("Memory areas:");
+      loop(i2sz(0),length))
+    else
+      println!("No memory mappings")
   end
-in
-  if (length > 0) then (
-    println!("Elf section headers: ");
-    loop(p,i2sz(0),length))
-  else
-    println!("No elf section headers")
+
 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 *)
+(**)
+(* //---------------------------------------------- *)
+(**)
diff --git a/kernel/bootinfo/multiboot.sats b/kernel/bootinfo/multiboot.sats
index 1a2e6db..cab885a 100644
--- a/kernel/bootinfo/multiboot.sats
+++ b/kernel/bootinfo/multiboot.sats
@@ -45,24 +45,23 @@ typedef boot_info_t = @{
   elf_tag = elf_tag_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 {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 // Print all available memory area's
-
-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_multiboot_ranges (p : !bootptr) : (Ptr0,Ptr0) // (bootinfo start, bootinfo end)
-
 macdef invalid_area = @{
   base_addr = the_null_ptr,
   length = i2sz(1),
   type = 0u,
   reserved = 0u
 }
+
+fun init(p : Ptr1) :void
+
+fn get_memory_mappings_n () : [n:nat] size_t n
+fn get_memory_mapping (n : size_t) : memory_area_t
+fn print_memory_mappings () : void // Print all available memory area's
+
+(* fn get_elf_headers_n () : [n:nat] size_t n *)
+(* fn get_elf_header  (n : size_t) : elf64_shdr_t *)
+(* fn print_elf_headers () : void *)
+(**)
+(* fn get_kernel_ranges () : (Ptr,Ptr) // (kernel start, kernel end) *)
+(* fn get_multiboot_ranges () : (Ptr0,Ptr0) // (bootinfo start, bootinfo end) *)
+