diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/bootinfo/multiboot.dats | 24 | ||||
| -rw-r--r-- | kernel/bootinfo/multiboot.sats | 14 | ||||
| -rw-r--r-- | kernel/main.dats | 4 |
3 files changed, 22 insertions, 20 deletions
diff --git a/kernel/bootinfo/multiboot.dats b/kernel/bootinfo/multiboot.dats index 9fe9103..cf72ba7 100644 --- a/kernel/bootinfo/multiboot.dats +++ b/kernel/bootinfo/multiboot.dats @@ -28,9 +28,9 @@ in implement init (p : Ptr1) = let val total_size = g1ofg0($UN.ptr0_get<uint>(p)) - fun loop {n,i : nat | i < n} .<n-i>. (boot_info : &boot_info_t? >> boot_info_t, p : ptr, i: uint i, n: uint n):<!wrt> void = let + fun loop (boot_info : &boot_info_t? >> boot_info_t, p : ptr):<!wrt,!ntm> void = let extern castfn unsafe_init(x : &boot_info_t? >> boot_info_t) :<> void - val type = $UN.ptr0_get<uint>(p) + 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 @@ -45,8 +45,8 @@ in ) | _ => (); - if (i < n - 1u) then - loop(boot_info,ptr_add<uint8>(p, next),succ(i),n) + if (type != 0u) then + loop(boot_info,ptr_add<uint8>(p, next)) else unsafe_init(boot_info) end @@ -54,23 +54,25 @@ in implement initialize$fwork<boot_info_t>(v) = ( if (total_size > 0u) then ( v.total_size := total_size; - loop(v, ptr_add<uint32>(p,2),0u,total_size); + $effmask_ntm(loop(v, ptr_add<uint32>(p,2))); let prval () = opt_some v in true end) else let prval () = opt_none v in false end ) - in end + in + initialize<boot_info_t>(bootinfo_ref) + end implement get_memory_mappings_n() = let - implement exec$fwork<boot_info_t><size_t>(v,_) = _get_memory_mappings_n(v) + implement exec$fwork<boot_info_t><size_t>(v) = _get_memory_mappings_n(v) in - exec<boot_info_t>(bootinfo_ref,i2sz(0)) + exec<boot_info_t><size_t>(bootinfo_ref) end implement get_memory_mapping(n) = let - implement exec$fwork<boot_info_t><memory_area_t>(v,_) = _get_memory_mapping(v,n) + 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) + exec<boot_info_t><memory_area_t>(bootinfo_ref) end implement print_memory_mappings() = let @@ -123,7 +125,7 @@ end //---------------------------------------------- (* //---------------------ELF---------------------- *) -(**) + (* implement get_elf_headers_n(p) = ui2sz p.2->elf_tag.num *) (**) (* implement get_elf_header (p,n) = ( *) diff --git a/kernel/bootinfo/multiboot.sats b/kernel/bootinfo/multiboot.sats index 6be1e73..9a41f29 100644 --- a/kernel/bootinfo/multiboot.sats +++ b/kernel/bootinfo/multiboot.sats @@ -54,14 +54,14 @@ macdef invalid_area = @{ fun init(p : Ptr1) :void -fn get_memory_mappings_n () : [n:nat] size_t n +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_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) *) +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) diff --git a/kernel/main.dats b/kernel/main.dats index 4c7d49a..7b7c162 100644 --- a/kernel/main.dats +++ b/kernel/main.dats @@ -38,13 +38,13 @@ extern fun breakpoint() :void = "mac#" extern fun entry(p : Ptr1) : void = "ext#" implement entry(p) = let - // Initialize boot info struct - val () = $BOOT.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 + // Initialize boot info struct + $BOOT.init(p); clear_screen(); $BOOT.print_memory_mappings(); |