Implemented entry

2 files changed, 86 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
diff --git a/kernel/memory/paging/entry.sats b/kernel/memory/paging/entry.sats
new file mode 100644
index 0000000..a7f91ee
--- /dev/null
+++ b/kernel/memory/paging/entry.sats
@@ -0,0 +1,34 @@
+#define ENTRY_COUNT 512
+
+staload "kernel/memory/frame.sats"
+staload "lib/SATS/valid.sats"
+
+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 contains_flag(entry_t,entry_flag) : bool
+fn pointed_frame(entry_t) : Valid frame_t
+
+fn entry_set{n:nat}(&entry_t,frame_t,&(@[entry_flag][n]),size_t n) : void