diff options
Diffstat (limited to 'kernel/bootinfo')
| -rw-r--r-- | kernel/bootinfo/multiboot.dats | 172 | ||||
| -rw-r--r-- | kernel/bootinfo/multiboot.sats | 3 |
2 files changed, 106 insertions, 69 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 |