Mainly refactoring

6 files changed, 121 insertions, 32 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)
+
diff --git a/kernel/main.dats b/kernel/main.dats
index 94955ee..c57f53d 100644
--- a/kernel/main.dats
+++ b/kernel/main.dats
@@ -14,8 +14,19 @@ staload UN = "prelude/SATS/unsafe.sats"
   }
 %}
 
+//NOTE: how to make sure ats checks 2 contstraints in one if statement?
+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
 
-extern castfn char_arr2string {n:nat} (arr : &(@[char][n])) : string n
 
 extern fun breakpoint() :void  = "mac#"
 
@@ -25,10 +36,13 @@ implement  main(p) = let
 
   // Initialize boot info struct
   val bootptr = boot_info_init(p) 
+  val (kernel_start,kernel_end) = get_kernel_ranges(bootptr)
 in
 
   print_memory_mappings(bootptr);
+
   print_elf_headers(bootptr);
+  println!("Kernel Size: ", kernel_size(kernel_start,kernel_end));
 
   // Initialize interrupt table
   idt_init();
diff --git a/kernel/memory/frame.dats b/kernel/memory/frame.dats
index 26ff412..8578e8f 100644
--- a/kernel/memory/frame.dats
+++ b/kernel/memory/frame.dats
@@ -2,6 +2,13 @@
 
 #define ATS_DYNLOADFLAG 0
 
+macdef invalid_area = @{
+  base_addr = the_null_ptr,
+  length = 1,
+  type = 0u,
+  reserved = 0
+}
+
 staload "./frame.sats"
 staload "kernel/bootinfo/multiboot.sats"
 
@@ -12,19 +19,63 @@ implement containing_address(address) : frame_t =
     counter = $UN.cast{size_t}(address) / i2sz(PAGE_SIZE)
   }
 
-fn choose_next_area{l,k : agz}(pf : !frame_allocator_t@l, bf : !boot_info_t @ k | p : ptr l, b : ptr k) : void = let 
+fn containing_area(area : memory_area_t) : frame_t = containing_address(ptr_add<uint8>(area.base_addr,area.length - i2sz(1)))
 
+//FIX: function doesn't handle no frames left
+fn choose_next_area{l,k : agz}(pf : !frame_allocator_t@l, bf : !boot_info_t @ k | p : ptr l, b : ptr k) : void = let 
+  val length = get_memory_mappings_n(bf | b)
+  val next_free_frame = p->next_free_frame
+  fun loop {n,i : nat | i < n} {l : agz} .<n-i>. (bf : !boot_info_t @ l | b : ptr l, i : size_t i, n : size_t n) : memory_area_t = let 
+    val entry = get_memory_mapping(bf | b ,i)
+    val fr = containing_area(entry)
+  in
+    if (entry.type = 1 && fr.num >= next_free_frame.num) then
+      entry
+    else if (i < n-1) then
+      loop (bf | b,succ(i),n)
+    else
+      entry //TODO: fix
+  end
 in 
+  if (length > 0) then //TODO: fix
+    p->current_area := loop(bf | b, i2sz(0), length);
 
+  if (p->current_area.length > 1) then
+    let
+      val start_frame = containing_address(p->current_area.base_addr)
+    in
+      if (p->next_free_frame.num < start_frame.num) then
+        p->next_free_frame := start_frame
+    end
 end 
 
+local
+
+var frame_allocator : frame_allocator_t
+
+in
+
+  implement frame_allocator_init() : allocptr = let
+    extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (frame_allocator_t@l) // takeout proof  UNSAFE:
+    prval (pf, fpf) = __assert (addr@frame_allocator) 
+    val allocator = @{ 
+      next_free_frame = containing_address(the_null_ptr),
+      current_area = invalid_area
+    }
+  in
+
+    (pf, fpf | addr@frame_allocator)
+  end
+
+end
+
 implement allocate_frame(pf , bf | p,b) : frame_t = 
-  if (p->current_area.length > 1) then  let
+  if (p->current_area.type != 0u) then  let
       val area = p->current_area
       val frame = @{ num = p->next_free_frame.num }
 
       // last frame of current area
-      val last_frame_area = containing_address(ptr_add<uint8>(area.base_addr,area.length - i2sz(1)))
+      val last_frame_area = containing_area(area)
     in
       if (frame.num > last_frame_area.num) then (
         // all frames of current area are used, switch to next area
diff --git a/kernel/memory/frame.sats b/kernel/memory/frame.sats
index 441b85a..0d29298 100644
--- a/kernel/memory/frame.sats
+++ b/kernel/memory/frame.sats
@@ -9,7 +9,6 @@ typedef frame_t = @{
 typedef frame_allocator_t = @{
   next_free_frame = frame_t,
   current_area = memory_area_t,
-  num_areas = size_t,
   kernel_start = frame_t,
   kernel_end = frame_t,
   multiboot_start = frame_t,
@@ -19,7 +18,6 @@ typedef frame_allocator_t = @{
 vtypedef allocptr  = [l : agz] (frame_allocator_t@l , frame_allocator_t@l -<lin,prf> void | ptr l)
 
 fn containing_address {l : addr} (address : ptr l) : frame_t
-
 fn allocate_frame {l : agz}{k : agz} (pf : !frame_allocator_t @ l >> frame_allocator_t @ l, bf : !boot_info_t @ k | p : ptr l, b : ptr k) : frame_t
- 
 fn deallocate_frame (p : !allocptr) : void
+fn frame_allocator_init() : allocptr
diff --git a/kernel/prelude/DATS/print.dats b/kernel/prelude/DATS/print.dats
index c6cd220..b183da5 100644
--- a/kernel/prelude/DATS/print.dats
+++ b/kernel/prelude/DATS/print.dats
@@ -34,6 +34,9 @@ implement print_size_t (n) = put_string(itoa($UN.cast{int}(n),10))
 extern fun print_uint (n : uint) : void
 implement print_uint (n) = put_string(itoa($UN.cast{int}(n),10))
 
+extern fun print_addr (n : Ptr) : void
+implement print_addr (n) = put_string(itoa($UN.cast{int}(n),10))
+
 overload print with put_string of 1
 overload print with print_int of 1
 overload print with print_uint32 of 1
@@ -42,6 +45,7 @@ overload print with print_uint16 of 1
 overload print with print_uint8 of 1
 overload print with print_size_t of 1
 overload print with print_uint of 1
+overload print with print_addr of 1
 
 extern fun {a : t@ype}  println_base {n:nat | n > 1 && n < 33} (n :a, base : int n) : void
 implement{a} println_base(n,base) = println!(itoa($UN.cast{int}(n), base))