diff options
| author | Xander <xander@biltopia.org> | 2023-07-28 22:30:45 +0200 |
|---|---|---|
| committer | Xander <xander@biltopia.org> | 2023-07-28 22:30:45 +0200 |
| commit | 272a40095e7c3f694f010d074ab54b326730009e (patch) | |
| tree | 79d186dc52267a710c25b87e33fec8380d2ac83c | |
| parent | b78762c92afee705e618f29f89897db8b45df3dd (diff) | |
| download | ats-os-272a40095e7c3f694f010d074ab54b326730009e.tar.xz ats-os-272a40095e7c3f694f010d074ab54b326730009e.zip | |
Some work
| -rw-r--r-- | kernel/bootinfo/multiboot.dats | 30 | ||||
| -rw-r--r-- | kernel/bootinfo/multiboot.sats | 2 | ||||
| -rw-r--r-- | lib/SATS/init.sats | 1 |
3 files changed, 15 insertions, 18 deletions
diff --git a/kernel/bootinfo/multiboot.dats b/kernel/bootinfo/multiboot.dats index 0653184..9fe9103 100644 --- a/kernel/bootinfo/multiboot.dats +++ b/kernel/bootinfo/multiboot.dats @@ -26,10 +26,10 @@ in in 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) + val total_size = g1ofg0($UN.ptr0_get<uint>(p)) - fun loop (boot_info : &boot_info_t? >> boot_info_t, p : ptr):<!wrt,!ntm> void = let + 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 + extern castfn unsafe_init(x : &boot_info_t? >> boot_info_t) :<> void 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 @@ -45,23 +45,21 @@ in ) | _ => (); - if (type != 0u) then - loop(boot_info,ptr_add<uint8>(p, next)) + if (i < n - 1u) then + loop(boot_info,ptr_add<uint8>(p, next),succ(i),n) 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 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); + let prval () = opt_some v in true end) + else + let prval () = opt_none v in false end + ) + in end implement get_memory_mappings_n() = let implement exec$fwork<boot_info_t><size_t>(v,_) = _get_memory_mappings_n(v) diff --git a/kernel/bootinfo/multiboot.sats b/kernel/bootinfo/multiboot.sats index cab885a..6be1e73 100644 --- a/kernel/bootinfo/multiboot.sats +++ b/kernel/bootinfo/multiboot.sats @@ -40,7 +40,7 @@ typedef elf64_shdr_t = @{ } typedef boot_info_t = @{ - total_size = uint, // total size of boot information + total_size = [n : int | n > 0] uint n, // total size of boot information memory_map = memory_areas_t, elf_tag = elf_tag_t } diff --git a/lib/SATS/init.sats b/lib/SATS/init.sats index 8219de1..9261ca9 100644 --- a/lib/SATS/init.sats +++ b/lib/SATS/init.sats @@ -11,4 +11,3 @@ fun {vt:viewt@ype} {a: t@ype} exec$fwork (v : &vt, default: a):<!wrt> a fun {vt:viewt@ype} initialize (r: ref(initializable vt)):<!ref,!wrt> void fun {vt:viewt@ype} initialize$fwork (v: &vt? >> opt(vt,success)):<!wrt> #[success : bool] bool success - |