From e2d7deb82cd25b47cbccda0c48ab39e17c5c536d Mon Sep 17 00:00:00 2001
From: Xander <xander@biltopia.org>
Date: Thu, 17 Aug 2023 21:09:27 +0200
Subject: Started implementing paging

---
 kernel/memory/frame.dats            |  2 +-
 kernel/memory/frame.sats            |  2 ++
 kernel/memory/paging.dats           | 30 ++++++++++++++++++++++++++++++
 kernel/memory/paging.sats           | 33 +++++++++++++++++++++++++++++++++
 kernel/prelude/SATS/safe_casts.sats |  1 +
 kernel/prelude/kernel_prelude.hats  |  1 +
 6 files changed, 68 insertions(+), 1 deletion(-)
 create mode 100644 kernel/memory/paging.dats
 create mode 100644 kernel/memory/paging.sats
 create mode 100644 kernel/prelude/SATS/safe_casts.sats

(limited to 'kernel')

diff --git a/kernel/memory/frame.dats b/kernel/memory/frame.dats
index 2910de5..aa02134 100644
--- a/kernel/memory/frame.dats
+++ b/kernel/memory/frame.dats
@@ -10,7 +10,7 @@ staload "lib/DATS/init.dats"
 
 staload UN = "prelude/SATS/unsafe.sats"
 
-fn containing_address{l:addr}(address : ptr l):<> frame_t = 
+implement containing_address(address) = 
   @{ 
     counter = $UN.cast{size_t}(address) / i2sz(PAGE_SIZE)
   }
diff --git a/kernel/memory/frame.sats b/kernel/memory/frame.sats
index 6ace8f9..dfd422e 100644
--- a/kernel/memory/frame.sats
+++ b/kernel/memory/frame.sats
@@ -15,6 +15,8 @@ typedef frame_allocator_t = @{
   multiboot_end = frame_t
 }
 
+fn containing_address{l:addr}(ptr l):<> frame_t
+
 fn allocate_frame () : frame_t
 fn deallocate_frame () : void
 fn init(kernel_start: Ptr, kernel_end: Ptr, multiboot_start:Ptr, multiboot_end: Ptr) : void
diff --git a/kernel/memory/paging.dats b/kernel/memory/paging.dats
new file mode 100644
index 0000000..9b55624
--- /dev/null
+++ b/kernel/memory/paging.dats
@@ -0,0 +1,30 @@
+#define ATS_DYNLOADFLAG 0
+
+#include "kernel/prelude/kernel_prelude.hats"
+
+staload UN = "prelude/SATS/unsafe.sats"
+
+staload "./paging.sats"
+staload "./frame.sats"
+
+assume entry_type = uint64
+
+val zero = u2uint64(0u)
+
+implement is_unused(entry) = entry = zero
+implement set_unused(entry) = entry := zero
+
+implement flag_contains(entry,flag) = 
+    (entry land $UN.cast{uint64}(1 << (case+ flag of
+      | PRESENT() => 0
+      | WRITABLE() => 1
+      | USER_ACCESSIBLE() => 2
+      | WRITE_THROUGH() => 3
+      | NO_CACHE() => 4
+      | ACCESSED() => 5
+      | DIRTY() => 6
+      | HUGE_PAGE() => 7
+      | GLOBAL() => 8
+      | NO_EXECUTE() => 63
+    ))) != zero
+
diff --git a/kernel/memory/paging.sats b/kernel/memory/paging.sats
new file mode 100644
index 0000000..784f567
--- /dev/null
+++ b/kernel/memory/paging.sats
@@ -0,0 +1,33 @@
+#define ENTRY_COUNT 512
+
+staload "./frame.sats"
+
+abstype paddr_type(l:addr) = ptr(l)
+typedef paddr(l:addr) = paddr_type(l)
+
+abstype vaddr_type(l:addr) = ptr(l)
+typedef vaddr(l:addr) = vaddr_type(l)
+
+abst@ype entry_type = uint64
+typedef entry_t = entry_type
+
+typedef page_t = @{
+  num = size_t
+}
+
+datatype entry_flag = 
+  | PRESENT
+  | WRITABLE
+  | USER_ACCESSIBLE 
+  | WRITE_THROUGH 
+  | NO_CACHE 
+  | ACCESSED 
+  | DIRTY 
+  | HUGE_PAGE 
+  | GLOBAL 
+  | NO_EXECUTE 
+
+fn is_unused(entry_t) : bool
+fn set_unused(&entry_t) : void
+
+fn flag_contains(entry_t,entry_flag) : bool
diff --git a/kernel/prelude/SATS/safe_casts.sats b/kernel/prelude/SATS/safe_casts.sats
new file mode 100644
index 0000000..50a68a8
--- /dev/null
+++ b/kernel/prelude/SATS/safe_casts.sats
@@ -0,0 +1 @@
+castfn u2uint64{v : nat | v <= 0xFFFFFFFFFFFFFFFF}(v : uint v) : uint64 v
diff --git a/kernel/prelude/kernel_prelude.hats b/kernel/prelude/kernel_prelude.hats
index 39e7560..514c2c2 100644
--- a/kernel/prelude/kernel_prelude.hats
+++ b/kernel/prelude/kernel_prelude.hats
@@ -4,6 +4,7 @@
 #include "share/atspre_staload.hats"
 
 staload "./DATS/print.dats"
+staload "./SATS/safe_casts.sats"
 
 #endif
 
-- 
cgit v1.2.3