aboutsummaryrefslogtreecommitdiff
path: root/kernel/memory/paging/page.dats
diff options
context:
space:
mode:
authorXander <xander@biltopia.org>2023-08-20 22:57:07 +0200
committerXander <xander@biltopia.org>2023-08-20 23:03:17 +0200
commit70cca66089896730797a71ba545c7f4e87b12975 (patch)
tree167a22d505b32bf80bd8b432833e12a74a98941b /kernel/memory/paging/page.dats
parent7fce269442cb37810a14d088ea4a61d040ec3066 (diff)
downloadats-os-70cca66089896730797a71ba545c7f4e87b12975.tar.xz
ats-os-70cca66089896730797a71ba545c7f4e87b12975.zip
implement pageHEADmaster
Diffstat (limited to 'kernel/memory/paging/page.dats')
-rw-r--r--kernel/memory/paging/page.dats117
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)