From 245f24890cd78304cf0fd397dda8e72b0a7fbe6b Mon Sep 17 00:00:00 2001 From: Xander Date: Tue, 8 Aug 2023 22:17:40 +0200 Subject: more refactoring and implemented exec_init --- kernel/bootinfo/multiboot.dats | 172 +++++++++++++++++++++++++---------------- kernel/bootinfo/multiboot.sats | 3 +- kernel/main.dats | 33 ++++---- kernel/prelude/DATS/print.dats | 5 +- lib/DATS/init.dats | 31 +++++--- lib/DATS/panic.dats | 2 +- lib/DATS/writer.dats | 18 ++--- lib/SATS/init.sats | 3 + 8 files changed, 155 insertions(+), 112 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): 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): 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): 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(v) = ( if (total_size > 0u) then ( + v.address := p; v.total_size := total_size; $effmask_ntm(loop(v, ptr_add(p,2))); let prval () = opt_some v in true end) @@ -81,6 +88,36 @@ in exec_void(bootinfo_ref) end + implement get_elf_headers_n() = let + implement exec$fwork(v) = _get_elf_headers_n(v) + in + exec(bootinfo_ref) + end + + implement get_elf_header(n) = let + implement exec$fwork(v) = _get_elf_header(v,n) + in + exec(bootinfo_ref) + end + + implement print_elf_headers() = let + implement exec_void$fwork(v) = _print_elf_headers(v) + in + exec_void(bootinfo_ref) + end + + implement get_kernel_ranges() = let + implement exec$fwork<(Ptr,Ptr)>(v) = _get_kernel_ranges(v) + in + exec<(Ptr,Ptr)>(bootinfo_ref) + end + + implement get_multiboot_ranges() = let + implement exec$fwork<(Ptr0,Ptr0)>(v) = _get_multiboot_ranges(v) + in + exec<(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(ptr_add(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(ptr_add(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} .. (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(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(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} .. (i : size_t i, n : size_t n) : 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(ptr_add(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} .. (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(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(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} .. (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 diff --git a/kernel/main.dats b/kernel/main.dats index 7b7c162..96cfdda 100644 --- a/kernel/main.dats +++ b/kernel/main.dats @@ -13,17 +13,17 @@ staload "lib/SATS/writer.sats" //NOTE: how to make sure ats checks 2 contstraints in one if statement? //TODO: put in seperate utils module (just generic size function) -(* fn kernel_size(kernel_start : Ptr, kernel_end : Ptr) : size_t = let *) -(* extern castfn Ptr12size (a : Ptr1): size_t *) -(* in *) -(* if (kernel_end > the_null_ptr) then *) -(* if (kernel_start > the_null_ptr) then *) -(* Ptr12size(kernel_end) - Ptr12size(kernel_start) *) -(* else *) -(* i2sz(0) *) -(* else *) -(* i2sz(0) *) -(* end *) +fn kernel_size(kernel_start : Ptr, kernel_end : Ptr) : size_t = let + extern castfn Ptr12size (a : Ptr1): size_t +in + if (kernel_end > the_null_ptr) then + if (kernel_start > the_null_ptr) then + Ptr12size(kernel_end) - Ptr12size(kernel_start) + else + i2sz(0) + else + i2sz(0) +end (* fn test(allocptr : !allocptr, bootptr : !bootptr) : void = let *) (* fun loop(i : int) : void = if (i < 160) then( let val _ = allocate_frame(allocptr.0, bootptr.0 | allocptr.2, bootptr.2) in end; loop(succ(i))) *) @@ -37,20 +37,17 @@ extern fun breakpoint() :void = "mac#" extern fun entry(p : Ptr1) : void = "ext#" implement entry(p) = let - - - (* val (kernel_start,kernel_end) = get_kernel_ranges(bootptr) *) + val () = $BOOT.init(p); + val (kernel_start,kernel_end) = $BOOT.get_kernel_ranges() (* val (multiboot_start,multiboot_end) = get_multiboot_ranges(bootptr) *) (* val allocptr = frame_allocator_init(kernel_start,kernel_end,multiboot_start,multiboot_end,bootptr) *) in // Initialize boot info struct - $BOOT.init(p); - clear_screen(); $BOOT.print_memory_mappings(); + $BOOT.print_elf_headers(); - (* print_elf_headers(bootptr); *) - (* println!("Kernel Size: ", kernel_size(kernel_start,kernel_end)); *) + println!("Kernel Size: ", kernel_size(kernel_start,kernel_end)); (* test(allocptr,bootptr); *) (* let *) (* val frame = allocate_frame(allocptr.0, bootptr.0 | allocptr.2, bootptr.2) *) diff --git a/kernel/prelude/DATS/print.dats b/kernel/prelude/DATS/print.dats index ac864ad..c6907a1 100644 --- a/kernel/prelude/DATS/print.dats +++ b/kernel/prelude/DATS/print.dats @@ -4,14 +4,15 @@ staload "lib/SATS/writer.sats" staload "lib/DATS/itoa.dats" +staload "lib/SATS/panic.sats" staload UN = "prelude/SATS/unsafe.sats" extern fun print_newline() : void implement print_newline() = put_string("\n") -extern fun assert_errmsg(b: bool, msg: string) : void -implement assert_errmsg(b,msg) = if (~b) then put_string(msg) +extern fun assert_errmsg(b: bool, string) :<> void +implement assert_errmsg(b,loc) = if (~b) then panic_loc(loc,"Assert fail") extern fun print_int (n : int) : void implement print_int(n) = put_string(itoa(n,10)) diff --git a/lib/DATS/init.dats b/lib/DATS/init.dats index c2ae39d..206dc6f 100644 --- a/lib/DATS/init.dats +++ b/lib/DATS/init.dats @@ -26,7 +26,25 @@ in panic("Not initialized") end -implement{vt} exec_void$fwork (v) = panic("Not overloaded") +//NOTE: lot of duplicate code +implement{vt} exec_init (r) = let + val (vbox pf | p) = ref_get_viewptr{initializable vt}(r) +in + if p->initialized then + let + prval () = opt_unsome p->obj + val () = exec_void$fwork(p->obj) + prval () = opt_some p->obj + in + end + else ( + $effmask_ref(initialize(r)); + if p->initialized then + $effmask_ref(exec_void(r)) + else + panic("Not inialized"); + ) +end implement{vt} {a} exec (r) = let val (vbox pf | p) = ref_get_viewptr{initializable vt}(r) @@ -45,10 +63,6 @@ in ) end -implement{vt} {a} exec$fwork (v) = ( - (panic("Not overloaded")); - $UN.ptr0_get(the_null_ptr) -) implement{vt} initialize (r) = let val (vbox pf | p) = ref_get_viewptr{initializable vt}(r) @@ -59,10 +73,3 @@ in val () = p->initialized := initialize$fwork(p->obj) in end end - -implement{vt} initialize$fwork (v) = let - prval () = opt_none v -in - false -end - diff --git a/lib/DATS/panic.dats b/lib/DATS/panic.dats index 356eda5..fc3122b 100644 --- a/lib/DATS/panic.dats +++ b/lib/DATS/panic.dats @@ -15,7 +15,7 @@ staload UN = "prelude/SATS/unsafe.sats" extern fun halt(): void = "mac#" -implement panic_loc(loc,msg) = ( +implement panic_loc(loc,msg) = $effmask_all( put_string "KERNEL PANIC:\n "; put_string loc; put_string "\n\n "; diff --git a/lib/DATS/writer.dats b/lib/DATS/writer.dats index b8625f4..6a183c1 100644 --- a/lib/DATS/writer.dats +++ b/lib/DATS/writer.dats @@ -96,6 +96,12 @@ in in + implement initialize$fwork(v) = + ( + v := @{position = 0, color_code = code_value(White,Black)}; + let prval() = opt_some v in true end + ) + implement put_string (str : string) : void = let implement exec_void$fwork(v) = let implement string_foreach$fwork (c,env) = put_char(c,env) @@ -103,21 +109,13 @@ in in end in - $effmask_ref(exec_void(writer_ref)) + $effmask_ref(exec_init(writer_ref)) end implement clear_screen() : void = let implement exec_void$fwork(v) = _clear_screen(v) - implement initialize$fwork(v) = - ( - v := @{position = 0, color_code = code_value(White,Black)}; - let prval() = opt_some v in true end - ) in - if not writer_ref->initialized then - initialize(writer_ref); - - exec_void(writer_ref) + exec_init(writer_ref) end end diff --git a/lib/SATS/init.sats b/lib/SATS/init.sats index 69c6c9a..9fe8581 100644 --- a/lib/SATS/init.sats +++ b/lib/SATS/init.sats @@ -6,6 +6,9 @@ fun {vt:viewt@ype} uninitialized (v : opt(vt,false)): initializable vt fun {vt:viewt@ype} exec_void (r: ref(initializable vt)): void fun {vt:viewt@ype} exec_void$fwork (v : &vt): void +// function will also inialize if not yet initalized +fun {vt:viewt@ype} exec_init (r: ref(initializable vt)): void + fun {vt:viewt@ype} {a: t@ype} exec (r: ref(initializable vt)): a fun {vt:viewt@ype} {a: t@ype} exec$fwork (v : &vt): a -- cgit v1.2.3