diff options
Diffstat (limited to 'kernel/bootinfo')
| -rw-r--r-- | kernel/bootinfo/multiboot.dats | 62 | ||||
| -rw-r--r-- | kernel/bootinfo/multiboot.sats | 10 |
2 files changed, 47 insertions, 25 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) + |