implement table

1 files changed, 68 insertions, 0 deletions

diff --git a/kernel/memory/paging/table.dats b/kernel/memory/paging/table.dats
new file mode 100644
index 0000000..d5029a7
--- /dev/null
+++ b/kernel/memory/paging/table.dats
@@ -0,0 +1,68 @@
+#define ATS_DYNLOADFLAG 0
+
+#include "kernel/prelude/kernel_prelude.hats"
+
+staload "./table.sats"
+staload "./entry.sats" 
+
+staload "lib/SATS/valid.sats"
+staload "lib/DATS/valid.dats"
+
+// 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]
+in
+  if (contains_flag(entry,PRESENT) && ~contains_flag(entry,HUGE_PAGE)) then
+    let 
+      val next = g1ofg0((Ptr1_to_sz(p) << 9) lor (index << 12))
+    in
+      if next > i2sz(0) then
+        create_valid(sz_to_Ptr1(next))
+      else
+        create_unvalid()
+    end
+  else
+    create_unvalid()
+end
+
+implement set_zero(table) = let 
+  implement array_foreach$fwork<entry_t><void>(entry,v) = set_unused(entry)
+in
+  assertloc(array_foreach<entry_t>(table,i2sz(ENTRY_COUNT)) = i2sz(ENTRY_COUNT))
+end
+
+// UNSAFE: unsafe block
+local
+
+  staload UN = "prelude/SATS/unsafe.sats"
+
+in
+
+  implement get_P4() = @{
+    ptr = $UN.ptr_vtake(ulint_to_Ptr1(0xfffffffffffff000ul)),
+    level = (0u | )
+  }
+
+  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
+  in
+    if is_valid(next) then 
+      let
+        val p = unwrap_valid(next)
+      in
+        create_valid(@{
+          ptr = $UN.ptr_vtake(p),
+          level = ( succ(tp.level.0) | )
+        })
+      end
+    else
+      let
+        val () = destroy_unvalid(next)
+      in
+        create_unvalid()
+      end
+  end
+
+end