diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/bootinfo/multiboot.dats | 2 | ||||
| -rw-r--r-- | kernel/bootinfo/multiboot.sats | 8 | ||||
| -rw-r--r-- | kernel/main.dats | 19 | ||||
| -rw-r--r-- | kernel/memory/frame.dats | 23 | ||||
| -rw-r--r-- | kernel/memory/frame.sats | 2 |
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 |