From 7fce269442cb37810a14d088ea4a61d040ec3066 Mon Sep 17 00:00:00 2001
From: Xander <xander@biltopia.org>
Date: Sun, 20 Aug 2023 14:15:29 +0200
Subject: Rewrite table

---
 kernel/memory/paging/table.dats | 54 ++++++++++++++++++++++++++---------------
 1 file changed, 34 insertions(+), 20 deletions(-)

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

diff --git a/kernel/memory/paging/table.dats b/kernel/memory/paging/table.dats
index d5029a7..e636c6c 100644
--- a/kernel/memory/paging/table.dats
+++ b/kernel/memory/paging/table.dats
@@ -8,13 +8,16 @@ staload "./entry.sats"
 staload "lib/SATS/valid.sats"
 staload "lib/DATS/valid.dats"
 
+assume table_t(c:int) = tablePtr1 c
+
+
 // Calculate table address of next table based on current table and index: P4->P3->P2->P1
-fn next_table_address{l:agz}(pf : !table_t@l | p : ptr(l), index : sizeLt(ENTRY_COUNT)) : Valid Ptr1 = let
-  val entry = p->[index]
+fn next_table_address{n:int|n < 3}(table : !table_t(n), index : sizeLt(ENTRY_COUNT)):<> Valid Ptr1 = let
+  val entry = table_get_at(table,index)
 in
   if (contains_flag(entry,PRESENT) && ~contains_flag(entry,HUGE_PAGE)) then
     let 
-      val next = g1ofg0((Ptr1_to_sz(p) << 9) lor (index << 12))
+      val next = g1ofg0((Ptr1_to_sz(table.3) << 9) lor (index << 12))
     in
       if next > i2sz(0) then
         create_valid(sz_to_Ptr1(next))
@@ -25,10 +28,23 @@ in
     create_unvalid()
 end
 
+implement table_get_at(table,i) = let
+  val entry = (table.3->[i]) : entry_t
+in
+  entry
+end
+
+implement table_set_at(table,i,x) = table.3->[i] := x
+
 implement set_zero(table) = let 
-  implement array_foreach$fwork<entry_t><void>(entry,v) = set_unused(entry)
+  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]);
+    if i < ENTRY_COUNT - 1 then
+      loop(succ(i),t)
+  end
 in
-  assertloc(array_foreach<entry_t>(table,i2sz(ENTRY_COUNT)) = i2sz(ENTRY_COUNT))
+  loop(i2sz(0),table)
 end
 
 // UNSAFE: unsafe block
@@ -38,31 +54,29 @@ local
 
 in
 
-  implement get_P4() = @{
-    ptr = $UN.ptr_vtake(ulint_to_Ptr1(0xfffffffffffff000ul)),
-    level = (0u | )
-  }
+  implement get_P4() =  let
+    val (pf,fpf | p) = $UN.ptr_vtake(ulint_to_Ptr1(0xfffffffffffff000ul))
+  in
+    (pf,fpf,0u | p)
+  end
 
-  implement next_table(tp,index) = let
-    val k = tp.ptr
-    val next = next_table_address(k.0 | k.2,index)
-    prval () = k.1 k.0
+  implement next_table(table,index) = let
+    val next = next_table_address(table,index)
+    prval level = table.2
   in
+    consume(table);
     if is_valid(next) then 
       let
-        val p = unwrap_valid(next)
+        val t = unwrap_valid(next)
+        val (pf, fpf | p) = $UN.ptr_vtake(t)
       in
-        create_valid(@{
-          ptr = $UN.ptr_vtake(p),
-          level = ( succ(tp.level.0) | )
-        })
+       create_valid ((pf,fpf, succ(level) | p))
       end
     else
       let
         val () = destroy_unvalid(next)
       in
         create_unvalid()
-      end
+      end;
   end
-
 end
-- 
cgit v1.2.3