From 70cca66089896730797a71ba545c7f4e87b12975 Mon Sep 17 00:00:00 2001
From: Xander <xander@biltopia.org>
Date: Sun, 20 Aug 2023 22:57:07 +0200
Subject: implement page

---
 kernel/memory/paging/table.dats | 44 ++++++++++++++++++++++++++++++++++++++---
 1 file changed, 41 insertions(+), 3 deletions(-)

(limited to 'kernel/memory/paging/table.dats')

diff --git a/kernel/memory/paging/table.dats b/kernel/memory/paging/table.dats
index e636c6c..d3bfe93 100644
--- a/kernel/memory/paging/table.dats
+++ b/kernel/memory/paging/table.dats
@@ -28,6 +28,16 @@ in
     create_unvalid()
 end
 
+// Checks if next table exists and returns bool
+fn next_table_exists{n:int|n < 3}(table: !table_t(n),index : sizeLt(ENTRY_COUNT)):<> bool = let
+  val vnext = next_table_address(table,index)
+in
+  if is_valid(vnext) then
+    let val _ = unwrap_valid(vnext) in true end
+  else 
+    (destroy_unvalid(vnext); false)
+end
+
 implement table_get_at(table,i) = let
   val entry = (table.3->[i]) : entry_t
 in
@@ -36,7 +46,8 @@ end
 
 implement table_set_at(table,i,x) = table.3->[i] := x
 
-implement set_zero(table) = let 
+// Set all the entries in the table to unused (zero)
+fn set_zero(table: &Table_t):<!wrt> void = let 
   fun loop{i:nat | i < ENTRY_COUNT}.<ENTRY_COUNT-i>.(i : size_t i,t : !Table_t):<!wrt> void = let 
   in
     set_unused(t.3->[i]);
@@ -54,6 +65,8 @@ local
 
 in
 
+  // TODO: define safe unique ownership for this table
+  // see https://os.phil-opp.com/page-tables/#safety-2
   implement get_P4() =  let
     val (pf,fpf | p) = $UN.ptr_vtake(ulint_to_Ptr1(0xfffffffffffff000ul))
   in
@@ -76,7 +89,32 @@ in
       let
         val () = destroy_unvalid(next)
       in
-        create_unvalid()
-      end;
+        create_unvalid();
+      end
+  end
+
+  implement next_table_create(table,index) = let
+    staload "kernel/memory/frame.sats"
+  in
+    if ~next_table_exists(table,index) then (
+      println!("not exists");
+      assertloc(~contains_flag(table[index],HUGE_PAGE));
+      table[index] := create_entry(allocate_frame(),flags,i2sz(2)) where {
+        var flags = @[entry_flag](PRESENT,WRITABLE)
+      };
+      let 
+        val vnext = next_table(table,index)
+      in
+        if is_valid(vnext) then
+            let var next = unwrap_valid(vnext) in (set_zero(next); create_valid(next)) end
+        else (
+          destroy_unvalid(vnext);
+          create_unvalid()
+        )
+      end
+    ) else 
+      $UN.castvwtp0(next_table(table,index)) //This is safe
   end
+
 end
+
-- 
cgit v1.2.3