diff options
Diffstat (limited to 'kernel/bootinfo')
| -rw-r--r-- | kernel/bootinfo/multiboot.dats | 288 | ||||
| -rw-r--r-- | kernel/bootinfo/multiboot.sats | 29 |
2 files changed, 176 insertions, 141 deletions
diff --git a/kernel/bootinfo/multiboot.dats b/kernel/bootinfo/multiboot.dats index 9eee595..0653184 100644 --- a/kernel/bootinfo/multiboot.dats +++ b/kernel/bootinfo/multiboot.dats @@ -3,150 +3,186 @@ #define ATS_DYNLOADFLAG 0 staload "./multiboot.sats" +staload "lib/SATS/init.sats" +staload "lib/DATS/init.dats" staload UN = "prelude/SATS/unsafe.sats" local -var boot_info : boot_info_t + 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 in -implement boot_info_init (p : Ptr1) = let - extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (boot_info_t@l) // takeout proof UNSAFE: - prval (pf, fpf) = __assert (addr@boot_info) - val total_size = $UN.ptr0_get<uint>(p) - - fun loop {l : agz} (pf : !boot_info_t@l | boot_p : ptr l , p : ptr): void = let - 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 - case+ type of - | 6u => ( - boot_p->memory_map := $UN.ptr0_get<memory_areas_t>(p); - boot_p->memory_map.entries := ptr_add<uint32>(p,4) - ) - | 9u => ( - boot_p->elf_tag := $UN.ptr0_get<elf_tag_t>(p); - boot_p->elf_tag.headers := ptr_add<uint32>(p,5); - ) - | _ => (); - - if (type != 0u) then - loop(pf | boot_p, ptr_add<uint8>(p, next)) - end - -in - boot_info.total_size := total_size; - loop(pf | addr@boot_info, ptr_add<uint32>(p,2)); - - (pf , fpf | addr@boot_info) -end - -end - -extern castfn ui2sz (n : uint) :<> [n : nat] size_t n - -//------------Memory------------------------ - -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) + local + // Static variable + var _v : boot_info_t? + prval () = opt_none _v + var v = uninitialized<boot_info_t>(_v) + // Reference to writer + val bootinfo_ref = ref_make_viewptr{initializable boot_info_t} (view@v | addr@v) + in -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)) -) + implement init (p : Ptr1) = let + extern castfn unsafe_init(x : &boot_info_t? >> boot_info_t) :<> void + val total_size = $UN.ptr0_get<uint>(p) + + fun loop (boot_info : &boot_info_t? >> boot_info_t, p : ptr):<!wrt,!ntm> void = let + 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 + case+ type of + | 6u => ( + boot_info.memory_map := $UN.ptr0_get<memory_areas_t>(p); + boot_info.memory_map.entries := ptr_add<uint32>(p,4) + ) + | 9u => ( + boot_info.elf_tag := $UN.ptr0_get<elf_tag_t>(p); + boot_info.elf_tag.headers := ptr_add<uint32>(p,5); + ) + | _ => (); + + if (type != 0u) then + loop(boot_info,ptr_add<uint8>(p, next)) + else + unsafe_init(boot_info) + end + + val (vbox pf | boot_p) = ref_get_viewptr(bootinfo_ref) + in + if (not boot_p->initialized) then + let + prval () = opt_unnone boot_p->obj + val () = boot_p->obj.total_size := total_size + val () = loop(boot_p->obj, ptr_add<uint32>(p,2)) + val () = boot_p->initialized := true + prval () = opt_some boot_p->obj + in end + end + + implement get_memory_mappings_n() = let + implement exec$fwork<boot_info_t><size_t>(v,_) = _get_memory_mappings_n(v) + in + exec<boot_info_t>(bootinfo_ref,i2sz(0)) + end + + implement get_memory_mapping(n) = let + 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) + end + + implement print_memory_mappings() = let + implement exec_void$fwork<boot_info_t>(v) = _print_memory_mappings(v) + in + exec_void<boot_info_t>(bootinfo_ref) + end -//TODO: use foreach with fwork to loop through memory maps -implement print_memory_mappings(p) = let - 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.0 | p.2 ,i) - in - if (entry.type = 1) then ( - print(" Start Address: "); - print_hex(entry.base_addr); - print(", Length: "); - println_hex(entry.length); - ); - if (i < n-1) then - loop (p,succ(i),n) end -in - if (length > 0) then ( - println!("Memory areas:"); - loop(p,i2sz(0),length)) - else - println!("No memory mappings") -end -//---------------------------------------------- + //------------Memory------------------------ -//---------------------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 - ) + implement _get_memory_mappings_n(boot_info) = let + val size = boot_info.memory_map.tag.size + val n_entries = (if(size >= 16u) then (size - 16u) / boot_info.memory_map.entry_size else 0u) : uint in - if (i < n - 1) then - loop(p,succ(i),n,new_min,new_max) - else - (new_min,new_max) + ui2sz n_entries 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) + implement _get_memory_mapping(boot_info,n) = ( + (* assertloc(n < get_memory_mappings_n(pf | p)); *) + $UN.ptr0_get<memory_area_t>(ptr_add<memory_area_t>(boot_info.memory_map.entries,n)) + ) + + //TODO: use foreach with fwork to loop through memory maps + implement _print_memory_mappings(boot_info) = let + val length = _get_memory_mappings_n(boot_info) + fun loop {n,i : nat | i < n} .<n-i>. (i : size_t i, n : size_t n):<!wrt> void = let + val entry = _get_memory_mapping(boot_info,i) + in + if (entry.type = 1) then ( + print(" Start Address: "); + print_hex(entry.base_addr); + print(", Length: "); + println_hex(entry.length); + ); + if (i < n-1) then + loop (succ(i),n) + end 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) - + if (length > 0) then ( + println!("Memory areas:"); + loop(i2sz(0),length)) + else + println!("No memory mappings") end -in - if (length > 0) then ( - println!("Elf section headers: "); - loop(p,i2sz(0),length)) - else - println!("No elf section headers") + 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 1a2e6db..cab885a 100644 --- a/kernel/bootinfo/multiboot.sats +++ b/kernel/bootinfo/multiboot.sats @@ -45,24 +45,23 @@ typedef boot_info_t = @{ elf_tag = elf_tag_t } -vtypedef bootptr = [l : agz] (boot_info_t@l , boot_info_t@l -<lin,prf> void | ptr l) - -fun boot_info_init(p : Ptr1) : bootptr - -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 // Print all available memory area's - -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_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 } + +fun init(p : Ptr1) :void + +fn get_memory_mappings_n () : [n:nat] size_t n +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) *) + |