aboutsummaryrefslogtreecommitdiff
path: root/kernel/memory/paging/entry.dats
diff options
context:
space:
mode:
authorXander <xander@biltopia.org>2023-08-19 15:04:23 +0200
committerXander <xander@biltopia.org>2023-08-19 15:19:25 +0200
commitfcf755d4f03f6fba974d11307659e2e96f9696e7 (patch)
treea58d9b7b24d6ab4b80f854d6d3905246b37494bd /kernel/memory/paging/entry.dats
parentd177285a761de33b86fcbde72fd718137bfa6f86 (diff)
downloadats-os-fcf755d4f03f6fba974d11307659e2e96f9696e7.tar.xz
ats-os-fcf755d4f03f6fba974d11307659e2e96f9696e7.zip
Implemented entry
Diffstat (limited to 'kernel/memory/paging/entry.dats')
-rw-r--r--kernel/memory/paging/entry.dats52
1 files changed, 52 insertions, 0 deletions
diff --git a/kernel/memory/paging/entry.dats b/kernel/memory/paging/entry.dats
new file mode 100644
index 0000000..7fa97b9
--- /dev/null
+++ b/kernel/memory/paging/entry.dats
@@ -0,0 +1,52 @@
+#define ATS_DYNLOADFLAG 0
+
+#include "kernel/prelude/kernel_prelude.hats"
+
+staload UN = "prelude/SATS/unsafe.sats"
+
+staload "./entry.sats"
+staload FRAME = "kernel/memory/frame.sats"
+staload "lib/SATS/valid.sats"
+staload "lib/DATS/valid.dats"
+
+assume entry_type = uint64
+
+val zero = u2u64(0u)
+
+fn flags2entry{n:nat}(arr : &(@[entry_flag][n]), n: size_t n) : entry_t = let
+ implement array_foreach$fwork<entry_flag><entry_t>(f,k) = k := k lor $UN.cast{entry_t}(1 << (case+ f 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
+ ))
+ var k = g0ofg1(u2u64(0u))
+ val _ = array_foreach_env<entry_flag><entry_t>(arr,n,k)
+in
+ k
+end
+
+implement is_unused(entry) = entry = zero
+implement set_unused(entry) = entry := zero
+
+implement contains_flag(entry,flag) = (flags2entry(flags,i2sz(1)) land entry) != zero where {
+ var flags = @[entry_flag](PRESENT)
+}
+
+implement pointed_frame(entry) =
+ if contains_flag(entry,PRESENT) then
+ create_valid($FRAME.containing_address(u64_to_Ptr0(entry land u2u64(0x000FFFFFFFFFF000u))))
+ else
+ create_unvalid()
+
+implement entry_set(entry,frame,flags,n) = let
+ val x = Ptr0_to_u64($FRAME.start_address(frame))
+in
+ assertloc((x land u2u64(0xFFF0000000000FFFu)) = zero);
+ entry := (x lor flags2entry(flags,n))
+end