diff options
author | Xander <xander@biltopia.org> | 2023-08-20 22:57:07 +0200 |
---|---|---|
committer | Xander <xander@biltopia.org> | 2023-08-20 23:03:17 +0200 |
commit | 70cca66089896730797a71ba545c7f4e87b12975 (patch) | |
tree | 167a22d505b32bf80bd8b432833e12a74a98941b /kernel/memory/paging/page.dats | |
parent | 7fce269442cb37810a14d088ea4a61d040ec3066 (diff) | |
download | ats-os-master.tar.xz ats-os-master.zip |
Diffstat (limited to 'kernel/memory/paging/page.dats')
-rw-r--r-- | kernel/memory/paging/page.dats | 117 |
1 files changed, 117 insertions, 0 deletions
diff --git a/kernel/memory/paging/page.dats b/kernel/memory/paging/page.dats new file mode 100644 index 0000000..2880c18 --- /dev/null +++ b/kernel/memory/paging/page.dats @@ -0,0 +1,117 @@ +#define ATS_DYNLOADFLAG 0 + +#include "kernel/prelude/kernel_prelude.hats" + +staload "./page.sats" +staload FR = "kernel/memory/frame.sats" +staload "./table.sats" + +staload "lib/SATS/valid.sats" +staload "lib/DATS/valid.dats" + +datatype table_level = + | Level4 + | Level3 + | Level2 + | Level1 + +fn start_address(page : page_t) : size_t = page.num * $FR.PAGE_SIZE + +fn get_index(page: page_t,n : intLte(3)) = g1ofg0((page.num >> (27 - 9 * n)) land i2sz(511)) + +//NOTE: huge page handler not implemented +fn translate_page(page: page_t) : Valid $FR.frame_t = let + fun loop{n : nat | n < 3}.<3-n>.(table : table_t n, count : int n) : Valid $FR.frame_t = let + staload "./entry.sats" + val index = get_index(page,count) + in + if index < ENTRY_COUNT then let + val v = next_table(table,index) + in + if is_valid(v) then let + val table_next = unwrap_valid(v) + in + if count < 2 then + loop(table_next,succ(count)) + else( + consume(table_next); + frame + ) where { + val index = get_index(page,count+1) + val frame = (if index < ENTRY_COUNT then pointed_frame(table_next[index]) else create_unvalid()) : Valid $FR.frame_t + } + end + else ( + destroy_unvalid(v); + println!("Unvalid table pointer encountered: ", count); + create_unvalid()) + end + else ( + consume(table); + println!("Table index too big"); + create_unvalid()) + end +in + loop(get_P4(),0) +end + +implement translate(virtual_addr) = let + val offset = Ptr0_to_sz(virtual_addr) % i2sz($FR.PAGE_SIZE) + val vframe = translate_page(containing_address(virtual_addr)) +in + if is_valid(vframe) then let + val frame = unwrap_valid(vframe) + in + create_valid (sz_to_Ptr0(frame.num * $FR.PAGE_SIZE + offset)) + end + else ( + destroy_unvalid(vframe); + create_unvalid(); + ) +end + +implement containing_address(address) = ( + assertloc(address < ulint_to_Ptr0(0x0000800000000000ul) || + address >= ulint_to_Ptr0(0xFFFF800000000000ul)); + @{num = Ptr0_to_sz(address) / i2sz($FR.PAGE_SIZE)} +) + +// TODO: implement and_then and or_else for valid (like in rust) +implement map_to{s}(page,frame,flags,size) = let + staload "./entry.sats" + fun loop{n : nat | n < 3}.<3-n>.(table : table_t n, count : int n, flags: &(@[entry_flag][s])) : void = let + staload "lib/SATS/panic.sats" + val index = get_index(page,count) + val () = println!(index) + in + if index < ENTRY_COUNT then let + val v = next_table_create(table,index) + in + if is_valid(v) then let + val table_next = unwrap_valid(v) + in + if count < 2 then + loop(table_next,succ(count),flags) + else let + val index = get_index(page,count+1) + in + if index < ENTRY_COUNT then ( + assertloc(is_unused(table_next[index])); + table_next[index] := add_flag(create_entry(frame, flags,size),PRESENT); + ); + consume(table_next); + end + end + else ( + destroy_unvalid(v); + panic("Could not create table")) + end + else ( + consume(table); + println!("Table index too big")) + end +in + loop(get_P4(),0,flags) +end + +implement map(page,flags,size) = map_to(page,$FR.allocate_frame(),flags,size) |