aboutsummaryrefslogtreecommitdiff
path: root/kernel/bootinfo
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/bootinfo')
-rw-r--r--kernel/bootinfo/multiboot.dats24
-rw-r--r--kernel/bootinfo/multiboot.sats14
2 files changed, 20 insertions, 18 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)