Working frame allocator but VERY ugly code

5 files changed, 37 insertions, 17 deletions

diff --git a/kernel/bootinfo/multiboot.dats b/kernel/bootinfo/multiboot.dats
index 96d7f84..4df903e 100644
--- a/kernel/bootinfo/multiboot.dats
+++ b/kernel/bootinfo/multiboot.dats
@@ -122,7 +122,7 @@ in
     (the_null_ptr,the_null_ptr)
 end
 
-implement get_bootinfo_ranges(p) = (p.2, ptr_add<uint8>(p.2,p.2->total_size))
+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)
diff --git a/kernel/bootinfo/multiboot.sats b/kernel/bootinfo/multiboot.sats
index 963e2e6..0a0dce8 100644
--- a/kernel/bootinfo/multiboot.sats
+++ b/kernel/bootinfo/multiboot.sats
@@ -59,5 +59,11 @@ 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)
+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
+}
diff --git a/kernel/main.dats b/kernel/main.dats
index c57f53d..ecbbb40 100644
--- a/kernel/main.dats
+++ b/kernel/main.dats
@@ -4,10 +4,9 @@
 
 staload "kernel/interrupts/idt.sats"
 staload "kernel/bootinfo/multiboot.sats"
+staload "kernel/memory/frame.sats"
 staload "lib/SATS/writer.sats"
 
-staload UN = "prelude/SATS/unsafe.sats"
-
 %{^
   void breakpoint(){ 
     __asm__("int3");
@@ -15,6 +14,7 @@ staload UN = "prelude/SATS/unsafe.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
@@ -27,6 +27,12 @@ in
     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)))
+in
+  loop(0)
+end
+
 
 extern fun breakpoint() :void  = "mac#"
 
@@ -37,12 +43,20 @@ implement  main(p) = let
   // Initialize boot info struct
   val bootptr = boot_info_init(p) 
   val (kernel_start,kernel_end) = get_kernel_ranges(bootptr)
+  val (multiboot_start,multiboot_end) = get_multiboot_ranges(bootptr)
+  val allocptr = frame_allocator_init(kernel_start,kernel_end,multiboot_start,multiboot_end,bootptr)
 in
 
   print_memory_mappings(bootptr);
 
   print_elf_headers(bootptr);
   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)
+  in 
+    println!(frame.num)
+  end;
 
   // Initialize interrupt table
   idt_init();
@@ -55,6 +69,7 @@ in
 
   let
     prval () = bootptr.1(bootptr.0)
+    prval () = allocptr.1(allocptr.0)
   in end
 
 
diff --git a/kernel/memory/frame.dats b/kernel/memory/frame.dats
index 8578e8f..b1d86af 100644
--- a/kernel/memory/frame.dats
+++ b/kernel/memory/frame.dats
@@ -2,18 +2,12 @@
 
 #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"
 
 staload UN = "prelude/SATS/unsafe.sats"
 
+
 implement containing_address(address) : frame_t = 
   @{ 
     counter = $UN.cast{size_t}(address) / i2sz(PAGE_SIZE)
@@ -55,15 +49,20 @@ var frame_allocator : frame_allocator_t
 
 in
 
-  implement frame_allocator_init() : allocptr = let
+  implement frame_allocator_init(kernel_start, kernel_end, multiboot_start, multiboot_end, b) : 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
+      current_area = invalid_area,
+      kernel_start = containing_address(kernel_start),
+      kernel_end = containing_address(kernel_end),
+      multiboot_start = containing_address(multiboot_start),
+      multiboot_end = containing_address(multiboot_end)
     }
   in
-
+    frame_allocator := allocator;
+    choose_next_area(pf,b.0 | addr@frame_allocator, b.2);
     (pf, fpf | addr@frame_allocator)
   end
 
@@ -81,11 +80,11 @@ implement allocate_frame(pf , bf | p,b) : frame_t =
         // all frames of current area are used, switch to next area
         choose_next_area(pf, bf | p,b);
         allocate_frame(pf,bf | p,b)
-      ) else if (frame.num > p->kernel_start.num && frame.num <= p->kernel_end.num) then (
+      ) else if (frame.num >= p->kernel_start.num && frame.num <= p->kernel_end.num) then (
         // frame is used by kernel
         p->next_free_frame := @{num = p->kernel_end.num + 1};
         allocate_frame(pf,bf | p,b)
-      ) else if (frame.num > p->multiboot_start.num && frame.num <= p->multiboot_end.num) then (
+      ) else if (frame.num >= p->multiboot_start.num && frame.num <= p->multiboot_end.num) then (
         // frame is used by multiboot info structure
         p->next_free_frame := @{num = p->multiboot_end.num + 1};
         allocate_frame(pf,bf | p,b)
diff --git a/kernel/memory/frame.sats b/kernel/memory/frame.sats
index 0d29298..d965567 100644
--- a/kernel/memory/frame.sats
+++ b/kernel/memory/frame.sats
@@ -20,4 +20,4 @@ vtypedef allocptr  = [l : agz] (frame_allocator_t@l , frame_allocator_t@l -<lin,
 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
+fn frame_allocator_init(kernel_start: Ptr, kernel_end: Ptr, multiboot_start:Ptr, multiboot_end: Ptr, b : !bootptr) : allocptr