more refactoring and implemented exec_init

8 files changed, 155 insertions, 112 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 *)
-(**)
-(* //---------------------------------------------- *)
-(**)
diff --git a/kernel/bootinfo/multiboot.sats b/kernel/bootinfo/multiboot.sats
index 9a41f29..16be379 100644
--- a/kernel/bootinfo/multiboot.sats
+++ b/kernel/bootinfo/multiboot.sats
@@ -40,6 +40,7 @@ typedef elf64_shdr_t = @{
 }
 
 typedef boot_info_t = @{
+  address = Ptr1,
   total_size = [n : int | n > 0] uint n,    // total size of boot information 
   memory_map = memory_areas_t,
   elf_tag = elf_tag_t
@@ -58,7 +59,7 @@ fn get_memory_mappings_n () : size_t
 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_headers_n () : size_t
 fn get_elf_header  (n : size_t) : elf64_shdr_t
 fn print_elf_headers () : void
 
diff --git a/kernel/main.dats b/kernel/main.dats
index 7b7c162..96cfdda 100644
--- a/kernel/main.dats
+++ b/kernel/main.dats
@@ -13,17 +13,17 @@ staload "lib/SATS/writer.sats"
 
 //NOTE: how to make sure ats checks 2 contstraints in one if statement?
 //TODO: put in seperate utils module (just generic size function)
-(* fn kernel_size(kernel_start : Ptr, kernel_end : Ptr) : size_t = let *)
-(*   extern castfn Ptr12size (a : Ptr1): size_t *)
-(* in *)
-(*   if (kernel_end > the_null_ptr) then  *)
-(*     if (kernel_start > the_null_ptr) then *)
-(*       Ptr12size(kernel_end) - Ptr12size(kernel_start) *)
-(*     else *)
-(*       i2sz(0) *)
-(*   else *)
-(*     i2sz(0) *)
-(* end *)
+fn kernel_size(kernel_start : Ptr, kernel_end : Ptr) : size_t = let
+  extern castfn Ptr12size (a : Ptr1): size_t
+in
+  if (kernel_end > the_null_ptr) then 
+    if (kernel_start > the_null_ptr) then
+      Ptr12size(kernel_end) - Ptr12size(kernel_start)
+    else
+      i2sz(0)
+  else
+    i2sz(0)
+end
 
 (* fn test(allocptr : !allocptr, bootptr : !bootptr) : void = let *)
 (*   fun loop(i : int) : void = if (i < 160) then( let val _ = allocate_frame(allocptr.0, bootptr.0 | allocptr.2, bootptr.2) in end; loop(succ(i))) *)
@@ -37,20 +37,17 @@ extern fun breakpoint() :void  = "mac#"
 
 extern fun entry(p : Ptr1) : void = "ext#"
 implement  entry(p) = let
-
-
-  (* val (kernel_start,kernel_end) = get_kernel_ranges(bootptr) *)
+  val () =  $BOOT.init(p);
+  val (kernel_start,kernel_end) = $BOOT.get_kernel_ranges()
   (* val (multiboot_start,multiboot_end) = get_multiboot_ranges(bootptr) *)
   (* val allocptr = frame_allocator_init(kernel_start,kernel_end,multiboot_start,multiboot_end,bootptr) *)
 in
   // Initialize boot info struct
-  $BOOT.init(p);
 
-  clear_screen();
   $BOOT.print_memory_mappings();
+  $BOOT.print_elf_headers();
 
-  (* print_elf_headers(bootptr); *)
-  (* println!("Kernel Size: ", kernel_size(kernel_start,kernel_end)); *)
+  println!("Kernel Size: ", kernel_size(kernel_start,kernel_end));
   (* test(allocptr,bootptr); *)
   (* let *)
   (*   val frame = allocate_frame(allocptr.0, bootptr.0 | allocptr.2, bootptr.2) *)
diff --git a/kernel/prelude/DATS/print.dats b/kernel/prelude/DATS/print.dats
index ac864ad..c6907a1 100644
--- a/kernel/prelude/DATS/print.dats
+++ b/kernel/prelude/DATS/print.dats
@@ -4,14 +4,15 @@
 
 staload "lib/SATS/writer.sats"
 staload "lib/DATS/itoa.dats"
+staload "lib/SATS/panic.sats"
 
 staload UN = "prelude/SATS/unsafe.sats"
 
 extern fun print_newline() :<!wrt> void
 implement print_newline() = put_string("\n")
 
-extern fun assert_errmsg(b: bool, msg: string) :<!wrt> void
-implement assert_errmsg(b,msg) = if (~b) then put_string(msg)
+extern fun assert_errmsg(b: bool, string) :<> void
+implement assert_errmsg(b,loc) = if (~b) then panic_loc(loc,"Assert fail")
 
 extern fun print_int  (n : int) :<!wrt> void 
 implement print_int(n) = put_string(itoa(n,10))
diff --git a/lib/DATS/init.dats b/lib/DATS/init.dats
index c2ae39d..206dc6f 100644
--- a/lib/DATS/init.dats
+++ b/lib/DATS/init.dats
@@ -26,7 +26,25 @@ in
     panic("Not initialized")
 end
 
-implement{vt} exec_void$fwork (v) = panic("Not overloaded")
+//NOTE: lot of duplicate code
+implement{vt} exec_init (r) = let
+  val (vbox pf | p) = ref_get_viewptr{initializable vt}(r)
+in
+  if p->initialized then
+    let
+      prval () = opt_unsome p->obj
+      val () = exec_void$fwork<vt>(p->obj)
+      prval () = opt_some  p->obj
+    in
+    end
+  else (
+    $effmask_ref(initialize<vt>(r));
+    if p->initialized then 
+      $effmask_ref(exec_void<vt>(r))
+    else
+      panic("Not inialized");
+  )
+end
 
 implement{vt} {a} exec (r) = let
   val (vbox pf | p) = ref_get_viewptr{initializable vt}(r)
@@ -45,10 +63,6 @@ in
   )
 end
 
-implement{vt} {a} exec$fwork (v) = (
-  (panic("Not overloaded")); 
-  $UN.ptr0_get<a>(the_null_ptr)
-)
 
 implement{vt} initialize (r) = let
   val (vbox pf | p) = ref_get_viewptr{initializable vt}(r)
@@ -59,10 +73,3 @@ in
       val () = p->initialized := initialize$fwork(p->obj)
     in end
 end
-
-implement{vt} initialize$fwork (v) = let
-  prval () = opt_none v
-in
-  false
-end
-
diff --git a/lib/DATS/panic.dats b/lib/DATS/panic.dats
index 356eda5..fc3122b 100644
--- a/lib/DATS/panic.dats
+++ b/lib/DATS/panic.dats
@@ -15,7 +15,7 @@ staload UN = "prelude/SATS/unsafe.sats"
 
 extern fun halt():<!ntm> void = "mac#"
 
-implement panic_loc(loc,msg) = (
+implement panic_loc(loc,msg) = $effmask_all(
   put_string "KERNEL PANIC:\n   ";
   put_string loc;
   put_string "\n\n    ";
diff --git a/lib/DATS/writer.dats b/lib/DATS/writer.dats
index b8625f4..6a183c1 100644
--- a/lib/DATS/writer.dats
+++ b/lib/DATS/writer.dats
@@ -96,6 +96,12 @@ in
 
   in
 
+    implement initialize$fwork<writer_t>(v) =
+        (
+          v := @{position = 0, color_code = code_value(White,Black)}; 
+          let prval() = opt_some v in true end
+        )
+
     implement put_string (str : string) : void = let
       implement exec_void$fwork<writer_t>(v) = let 
         implement string_foreach$fwork<writer_t> (c,env) = put_char(c,env)
@@ -103,21 +109,13 @@ in
       in 
       end
     in  
-      $effmask_ref(exec_void<writer_t>(writer_ref))
+      $effmask_ref(exec_init<writer_t>(writer_ref))
     end
 
     implement clear_screen() : void = let
       implement exec_void$fwork<writer_t>(v) = _clear_screen(v)
-      implement initialize$fwork<writer_t>(v) =
-        (
-          v := @{position = 0, color_code = code_value(White,Black)}; 
-          let prval() = opt_some v in true end
-        )
     in
-      if not writer_ref->initialized then
-        initialize<writer_t>(writer_ref);
-      
-      exec_void<writer_t>(writer_ref)
+      exec_init<writer_t>(writer_ref)
     end
 
   end
diff --git a/lib/SATS/init.sats b/lib/SATS/init.sats
index 69c6c9a..9fe8581 100644
--- a/lib/SATS/init.sats
+++ b/lib/SATS/init.sats
@@ -6,6 +6,9 @@ fun {vt:viewt@ype} uninitialized (v : opt(vt,false)): initializable vt
 fun {vt:viewt@ype} exec_void (r: ref(initializable vt)):<!refwrt> void
 fun {vt:viewt@ype} exec_void$fwork (v : &vt):<!wrt> void
 
+// function will also inialize if not yet initalized
+fun {vt:viewt@ype} exec_init (r: ref(initializable vt)):<!refwrt> void
+
 fun {vt:viewt@ype} {a: t@ype} exec  (r: ref(initializable vt)):<!refwrt> a
 fun {vt:viewt@ype} {a: t@ype}  exec$fwork (v : &vt):<!wrt> a