diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/bootinfo/multiboot.dats | 62 | ||||
| -rw-r--r-- | kernel/bootinfo/multiboot.sats | 10 | ||||
| -rw-r--r-- | kernel/main.dats | 16 | ||||
| -rw-r--r-- | kernel/memory/frame.dats | 57 | ||||
| -rw-r--r-- | kernel/memory/frame.sats | 4 | ||||
| -rw-r--r-- | kernel/prelude/DATS/print.dats | 4 |
6 files changed, 121 insertions, 32 deletions
diff --git a/kernel/bootinfo/multiboot.dats b/kernel/bootinfo/multiboot.dats index 6ea7b00..96d7f84 100644 --- a/kernel/bootinfo/multiboot.dats +++ b/kernel/bootinfo/multiboot.dats @@ -49,24 +49,25 @@ extern castfn ui2sz (n : uint) : [n : nat] size_t n //------------Memory------------------------ -implement get_memory_mappings_n(p) = let - val size = p.2->memory_map.tag.size - val n_entries = (if(size >= 16u) then (size - 16u) / p.2->memory_map.entry_size else 0u) : uint +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) -implement get_memory_mapping(p,n) = ( - assertloc(n < get_memory_mappings_n(p)); - $UN.ptr0_get<memory_area_t>(ptr_add<memory_area_t>(p.2->memory_map.entries,n)) +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)) ) +//TODO: use foreach with fwork to loop through memory maps implement print_memory_mappings(p) = let - val length = get_memory_mappings_n(p) + 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,i) + val entry = get_memory_mapping(p.0 | p.2 ,i) in if (entry.type = 1) then ( print(" Start Address: "); @@ -96,13 +97,37 @@ implement get_elf_header (p,n) = ( $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_bootinfo_ranges(p) = (p.2, 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, min : size_t, max : size_t) : void = let + 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) - val a = $UN.cast{size_t}(header.addr) - val new_min = (if (a < min && header.size != 0) then a else min) : size_t - val new_max = (if (a + header.size > max && header.size != 0) then a + header.size else max) : size_t in print(" addr: "); print_hex(header.addr); @@ -112,20 +137,13 @@ implement print_elf_headers(p) = let println_hex(header.flags); if (i < n - 1) then - loop(p,succ(i),n,new_min,new_max) - else ( - print("Kernel start: "); - print_hex(new_min); - print(" end: "); - print_hex(new_max); - print(" size: "); - println!(new_max - new_min) - ) + loop(p,succ(i),n) + end in if (length > 0) then ( println!("Elf section headers: "); - loop(p,i2sz(0),length,i2sz(0xFFFFFF),i2sz(0))) + 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 3909fdd..963e2e6 100644 --- a/kernel/bootinfo/multiboot.sats +++ b/kernel/bootinfo/multiboot.sats @@ -5,7 +5,7 @@ typedef tag_t = @{ } typedef memory_area_t = @{ - base_addr = Ptr1, // Start of physical address + base_addr = Ptr, // Start of physical address length = [n : nat | n > 0 ] size_t n , // Size of memory region in bytes (64 bits) type = uint, // Variety of address range represented. 1: available RAM, 3: usable memory holding ACPI information, // 4: reserved memory (preserved on hibernation), Other: reserved area @@ -50,10 +50,14 @@ vtypedef bootptr = [l : agz] (boot_info_t@l , boot_info_t@l -<lin,prf> void | p fun boot_info_init(p : Ptr1) : bootptr -fn get_memory_mappings_n (p : !bootptr) : [n:nat] size_t n -fn get_memory_mapping (p : !bootptr, n : size_t) : memory_area_t +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 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_bootinfo_ranges (p : !bootptr) : (ptr,ptr) // (bootinfo start, bootinfo end) + diff --git a/kernel/main.dats b/kernel/main.dats index 94955ee..c57f53d 100644 --- a/kernel/main.dats +++ b/kernel/main.dats @@ -14,8 +14,19 @@ staload UN = "prelude/SATS/unsafe.sats" } %} +//NOTE: how to make sure ats checks 2 contstraints in one if statement? +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 -extern castfn char_arr2string {n:nat} (arr : &(@[char][n])) : string n extern fun breakpoint() :void = "mac#" @@ -25,10 +36,13 @@ implement main(p) = let // Initialize boot info struct val bootptr = boot_info_init(p) + val (kernel_start,kernel_end) = get_kernel_ranges(bootptr) in print_memory_mappings(bootptr); + print_elf_headers(bootptr); + println!("Kernel Size: ", kernel_size(kernel_start,kernel_end)); // Initialize interrupt table idt_init(); diff --git a/kernel/memory/frame.dats b/kernel/memory/frame.dats index 26ff412..8578e8f 100644 --- a/kernel/memory/frame.dats +++ b/kernel/memory/frame.dats @@ -2,6 +2,13 @@ #define ATS_DYNLOADFLAG 0 +macdef invalid_area = @{ + base_addr = the_null_ptr, + length = 1, + type = 0u, + reserved = 0 +} + staload "./frame.sats" staload "kernel/bootinfo/multiboot.sats" @@ -12,19 +19,63 @@ implement containing_address(address) : frame_t = counter = $UN.cast{size_t}(address) / i2sz(PAGE_SIZE) } -fn choose_next_area{l,k : agz}(pf : !frame_allocator_t@l, bf : !boot_info_t @ k | p : ptr l, b : ptr k) : void = let +fn containing_area(area : memory_area_t) : frame_t = containing_address(ptr_add<uint8>(area.base_addr,area.length - i2sz(1))) +//FIX: function doesn't handle no frames left +fn choose_next_area{l,k : agz}(pf : !frame_allocator_t@l, bf : !boot_info_t @ k | p : ptr l, b : ptr k) : void = let + val length = get_memory_mappings_n(bf | b) + val next_free_frame = p->next_free_frame + fun loop {n,i : nat | i < n} {l : agz} .<n-i>. (bf : !boot_info_t @ l | b : ptr l, i : size_t i, n : size_t n) : memory_area_t = let + val entry = get_memory_mapping(bf | b ,i) + val fr = containing_area(entry) + in + if (entry.type = 1 && fr.num >= next_free_frame.num) then + entry + else if (i < n-1) then + loop (bf | b,succ(i),n) + else + entry //TODO: fix + end in + if (length > 0) then //TODO: fix + p->current_area := loop(bf | b, i2sz(0), length); + if (p->current_area.length > 1) then + let + val start_frame = containing_address(p->current_area.base_addr) + in + if (p->next_free_frame.num < start_frame.num) then + p->next_free_frame := start_frame + end end +local + +var frame_allocator : frame_allocator_t + +in + + implement frame_allocator_init() : allocptr = let + extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (frame_allocator_t@l) // takeout proof UNSAFE: + prval (pf, fpf) = __assert (addr@frame_allocator) + val allocator = @{ + next_free_frame = containing_address(the_null_ptr), + current_area = invalid_area + } + in + + (pf, fpf | addr@frame_allocator) + end + +end + implement allocate_frame(pf , bf | p,b) : frame_t = - if (p->current_area.length > 1) then let + if (p->current_area.type != 0u) then let val area = p->current_area val frame = @{ num = p->next_free_frame.num } // last frame of current area - val last_frame_area = containing_address(ptr_add<uint8>(area.base_addr,area.length - i2sz(1))) + val last_frame_area = containing_area(area) in if (frame.num > last_frame_area.num) then ( // all frames of current area are used, switch to next area diff --git a/kernel/memory/frame.sats b/kernel/memory/frame.sats index 441b85a..0d29298 100644 --- a/kernel/memory/frame.sats +++ b/kernel/memory/frame.sats @@ -9,7 +9,6 @@ typedef frame_t = @{ typedef frame_allocator_t = @{ next_free_frame = frame_t, current_area = memory_area_t, - num_areas = size_t, kernel_start = frame_t, kernel_end = frame_t, multiboot_start = frame_t, @@ -19,7 +18,6 @@ typedef frame_allocator_t = @{ vtypedef allocptr = [l : agz] (frame_allocator_t@l , frame_allocator_t@l -<lin,prf> void | ptr l) fn containing_address {l : addr} (address : ptr l) : frame_t - fn allocate_frame {l : agz}{k : agz} (pf : !frame_allocator_t @ l >> frame_allocator_t @ l, bf : !boot_info_t @ k | p : ptr l, b : ptr k) : frame_t - fn deallocate_frame (p : !allocptr) : void +fn frame_allocator_init() : allocptr diff --git a/kernel/prelude/DATS/print.dats b/kernel/prelude/DATS/print.dats index c6cd220..b183da5 100644 --- a/kernel/prelude/DATS/print.dats +++ b/kernel/prelude/DATS/print.dats @@ -34,6 +34,9 @@ implement print_size_t (n) = put_string(itoa($UN.cast{int}(n),10)) extern fun print_uint (n : uint) : void implement print_uint (n) = put_string(itoa($UN.cast{int}(n),10)) +extern fun print_addr (n : Ptr) : void +implement print_addr (n) = put_string(itoa($UN.cast{int}(n),10)) + overload print with put_string of 1 overload print with print_int of 1 overload print with print_uint32 of 1 @@ -42,6 +45,7 @@ overload print with print_uint16 of 1 overload print with print_uint8 of 1 overload print with print_size_t of 1 overload print with print_uint of 1 +overload print with print_addr of 1 extern fun {a : t@ype} println_base {n:nat | n > 1 && n < 33} (n :a, base : int n) : void implement{a} println_base(n,base) = println!(itoa($UN.cast{int}(n), base)) |