aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/bootinfo/multiboot.dats172
-rw-r--r--kernel/bootinfo/multiboot.sats3
-rw-r--r--kernel/main.dats33
-rw-r--r--kernel/prelude/DATS/print.dats5
4 files changed, 124 insertions, 89 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):<!wrt> 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):<!wrt> 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):<!wrt> 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<boot_info_t>(v) = (
if (total_size > 0u) then (
+ v.address := p;
v.total_size := total_size;
$effmask_ntm(loop(v, ptr_add<uint32>(p,2)));
let prval () = opt_some v in true end)
@@ -81,6 +88,36 @@ in
exec_void<boot_info_t>(bootinfo_ref)
end
+ implement get_elf_headers_n() = let
+ implement exec$fwork<boot_info_t><size_t>(v) = _get_elf_headers_n(v)
+ in
+ exec<boot_info_t><size_t>(bootinfo_ref)
+ end
+
+ implement get_elf_header(n) = let
+ implement exec$fwork<boot_info_t><elf64_shdr_t>(v) = _get_elf_header(v,n)
+ in
+ exec<boot_info_t><elf64_shdr_t>(bootinfo_ref)
+ end
+
+ implement print_elf_headers() = let
+ implement exec_void$fwork<boot_info_t>(v) = _print_elf_headers(v)
+ in
+ exec_void<boot_info_t>(bootinfo_ref)
+ end
+
+ implement get_kernel_ranges() = let
+ implement exec$fwork<boot_info_t><(Ptr,Ptr)>(v) = _get_kernel_ranges(v)
+ in
+ exec<boot_info_t><(Ptr,Ptr)>(bootinfo_ref)
+ end
+
+ implement get_multiboot_ranges() = let
+ implement exec$fwork<boot_info_t><(Ptr0,Ptr0)>(v) = _get_multiboot_ranges(v)
+ in
+ exec<boot_info_t><(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<memory_area_t>(ptr_add<memory_area_t>(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<elf64_shdr_t>(ptr_add<elf64_shdr_t>(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} .<n-i>. (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<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(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<uint8>(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} .<n-i>. (i : size_t i, n : size_t n) :<!wrt> 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<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 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() :<!wrt> void
implement print_newline() = put_string("\n")
-extern fun assert_errmsg(b: bool, msg: string) :<!wrt> 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) :<!wrt> void
implement print_int(n) = put_string(itoa(n,10))
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 09:33:47 +0000