implement pageHEADmaster

6 files changed, 191 insertions, 15 deletions

diff --git a/kernel/memory/paging/entry.dats b/kernel/memory/paging/entry.dats
index 7fa97b9..76d6c0c 100644
--- a/kernel/memory/paging/entry.dats
+++ b/kernel/memory/paging/entry.dats
@@ -13,8 +13,7 @@ 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 
+implement add_flag(entry,f) = entry lor $UN.cast{entry_t}(1 << (case+ f of 
       | PRESENT() => 0
       | WRITABLE() => 1
       | USER_ACCESSIBLE() => 2
@@ -25,8 +24,11 @@ fn flags2entry{n:nat}(arr : &(@[entry_flag][n]), n: size_t n) : entry_t = let
       | GLOBAL() => 8
       | NO_EXECUTE() => 63
   ))
+
+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 := add_flag(k,f)
   var k = g0ofg1(u2u64(0u))
-  val _ = array_foreach_env<entry_flag><entry_t>(arr,n,k)
+  val _ = $effmask_all(array_foreach_env<entry_flag><entry_t>(arr,n,k))
 in
   k
 end
@@ -35,7 +37,7 @@ 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)
+  var flags = @[entry_flag](flag)
 }
 
 implement pointed_frame(entry) = 
@@ -44,9 +46,9 @@ implement pointed_frame(entry) =
   else
     create_unvalid()
 
-implement entry_set(entry,frame,flags,n) = let
+implement create_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))
+  (x lor flags2entry(flags,n))
 end
diff --git a/kernel/memory/paging/entry.sats b/kernel/memory/paging/entry.sats
index 17a9f72..fc20a20 100644
--- a/kernel/memory/paging/entry.sats
+++ b/kernel/memory/paging/entry.sats
@@ -1,5 +1,6 @@
 staload "kernel/memory/frame.sats"
 staload "lib/SATS/valid.sats"
+staload "lib/DATS/valid.dats"
 
 abst@ype entry_type = uint64
 typedef entry_t = entry_type
@@ -22,4 +23,5 @@ fn set_unused(&entry_t) :<!wrt> 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
+fn add_flag(entry_t,entry_flag) : entry_t
+fn create_entry{s:nat}(frame_t,&(@[entry_flag][s]),size_t s) : entry_t
diff --git a/kernel/memory/paging/page.dats b/kernel/memory/paging/page.dats
new file mode 100644
index 0000000..2880c18
--- /dev/null
+++ b/kernel/memory/paging/page.dats
@@ -0,0 +1,117 @@
+#define ATS_DYNLOADFLAG 0
+
+#include "kernel/prelude/kernel_prelude.hats"
+
+staload "./page.sats"
+staload FR = "kernel/memory/frame.sats"
+staload "./table.sats"
+
+staload "lib/SATS/valid.sats"
+staload "lib/DATS/valid.dats"
+
+datatype table_level = 
+  | Level4
+  | Level3
+  | Level2
+  | Level1
+
+fn start_address(page : page_t) : size_t = page.num * $FR.PAGE_SIZE
+
+fn get_index(page: page_t,n : intLte(3)) = g1ofg0((page.num >> (27 - 9 * n)) land i2sz(511))
+
+//NOTE: huge page handler not implemented
+fn translate_page(page: page_t) : Valid $FR.frame_t = let
+  fun loop{n : nat | n < 3}.<3-n>.(table : table_t n, count : int n) : Valid $FR.frame_t = let
+    staload "./entry.sats"
+    val index = get_index(page,count)
+  in
+    if index < ENTRY_COUNT then let
+        val v = next_table(table,index)
+      in
+        if is_valid(v) then let
+            val table_next = unwrap_valid(v)
+          in
+            if count < 2 then
+              loop(table_next,succ(count))
+            else(
+              consume(table_next);
+              frame
+            ) where {
+                val index = get_index(page,count+1)
+                val frame = (if index < ENTRY_COUNT then pointed_frame(table_next[index]) else create_unvalid()) : Valid $FR.frame_t
+              }
+          end
+        else (
+          destroy_unvalid(v);
+          println!("Unvalid table pointer encountered: ", count); 
+          create_unvalid())
+      end
+    else (
+      consume(table);
+      println!("Table index too big");
+      create_unvalid())
+  end
+in
+  loop(get_P4(),0)
+end
+
+implement translate(virtual_addr) = let
+  val offset = Ptr0_to_sz(virtual_addr) % i2sz($FR.PAGE_SIZE)
+  val vframe = translate_page(containing_address(virtual_addr))
+in
+  if is_valid(vframe) then let
+      val frame = unwrap_valid(vframe)
+    in
+      create_valid (sz_to_Ptr0(frame.num * $FR.PAGE_SIZE + offset))
+    end
+  else (
+    destroy_unvalid(vframe);
+    create_unvalid();
+  )
+end
+
+implement containing_address(address) = (
+  assertloc(address < ulint_to_Ptr0(0x0000800000000000ul) ||
+            address >= ulint_to_Ptr0(0xFFFF800000000000ul));
+  @{num = Ptr0_to_sz(address) / i2sz($FR.PAGE_SIZE)}
+)
+
+// TODO: implement and_then and or_else for valid (like in rust)
+implement map_to{s}(page,frame,flags,size) = let
+  staload "./entry.sats"
+  fun loop{n : nat | n < 3}.<3-n>.(table : table_t n, count : int n, flags: &(@[entry_flag][s])) : void = let
+    staload "lib/SATS/panic.sats"
+    val index = get_index(page,count)
+    val () = println!(index)
+  in
+    if index < ENTRY_COUNT then let
+        val v = next_table_create(table,index)
+      in
+        if is_valid(v) then let
+            val table_next = unwrap_valid(v)
+          in
+            if count < 2 then
+              loop(table_next,succ(count),flags)
+            else let
+                val index = get_index(page,count+1)
+              in
+                if index < ENTRY_COUNT then (
+                  assertloc(is_unused(table_next[index]));
+                  table_next[index] := add_flag(create_entry(frame, flags,size),PRESENT);
+                );
+                consume(table_next);
+              end
+          end
+        else (
+          destroy_unvalid(v);
+          panic("Could not create table"))
+      end
+    else (
+      consume(table);
+      println!("Table index too big"))
+  end
+in
+  loop(get_P4(),0,flags)
+end
+
+implement map(page,flags,size) = map_to(page,$FR.allocate_frame(),flags,size)
diff --git a/kernel/memory/paging/page.sats b/kernel/memory/paging/page.sats
new file mode 100644
index 0000000..1de50c6
--- /dev/null
+++ b/kernel/memory/paging/page.sats
@@ -0,0 +1,18 @@
+staload FRAME = "kernel/memory/frame.sats"
+
+staload "lib/SATS/valid.sats"
+staload "./entry.sats"
+
+typedef vaddr = Ptr0
+
+typedef page_t = @{
+  num = size_t
+}
+
+fn translate(vaddr) : Valid $FRAME.paddr
+
+fn containing_address(vaddr) : page_t
+
+fn map_to{n:nat}(page_t,$FRAME.frame_t,&(@[entry_flag][n]),size : size_t n): void
+
+fn map{n:nat}(page_t,&(@[entry_flag][n]),size : size_t n) : void
diff --git a/kernel/memory/paging/table.dats b/kernel/memory/paging/table.dats
index e636c6c..d3bfe93 100644
--- a/kernel/memory/paging/table.dats
+++ b/kernel/memory/paging/table.dats
@@ -28,6 +28,16 @@ in
     create_unvalid()
 end
 
+// Checks if next table exists and returns bool
+fn next_table_exists{n:int|n < 3}(table: !table_t(n),index : sizeLt(ENTRY_COUNT)):<> bool = let
+  val vnext = next_table_address(table,index)
+in
+  if is_valid(vnext) then
+    let val _ = unwrap_valid(vnext) in true end
+  else 
+    (destroy_unvalid(vnext); false)
+end
+
 implement table_get_at(table,i) = let
   val entry = (table.3->[i]) : entry_t
 in
@@ -36,7 +46,8 @@ end
 
 implement table_set_at(table,i,x) = table.3->[i] := x
 
-implement set_zero(table) = let 
+// Set all the entries in the table to unused (zero)
+fn set_zero(table: &Table_t):<!wrt> void = let 
   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]);
@@ -54,6 +65,8 @@ local
 
 in
 
+  // TODO: define safe unique ownership for this table
+  // see https://os.phil-opp.com/page-tables/#safety-2
   implement get_P4() =  let
     val (pf,fpf | p) = $UN.ptr_vtake(ulint_to_Ptr1(0xfffffffffffff000ul))
   in
@@ -76,7 +89,32 @@ in
       let
         val () = destroy_unvalid(next)
       in
-        create_unvalid()
-      end;
+        create_unvalid();
+      end
+  end
+
+  implement next_table_create(table,index) = let
+    staload "kernel/memory/frame.sats"
+  in
+    if ~next_table_exists(table,index) then (
+      println!("not exists");
+      assertloc(~contains_flag(table[index],HUGE_PAGE));
+      table[index] := create_entry(allocate_frame(),flags,i2sz(2)) where {
+        var flags = @[entry_flag](PRESENT,WRITABLE)
+      };
+      let 
+        val vnext = next_table(table,index)
+      in
+        if is_valid(vnext) then
+            let var next = unwrap_valid(vnext) in (set_zero(next); create_valid(next)) end
+        else (
+          destroy_unvalid(vnext);
+          create_unvalid()
+        )
+      end
+    ) else 
+      $UN.castvwtp0(next_table(table,index)) //This is safe
   end
+
 end
+
diff --git a/kernel/memory/paging/table.sats b/kernel/memory/paging/table.sats
index 491b77e..6b8e188 100644
--- a/kernel/memory/paging/table.sats
+++ b/kernel/memory/paging/table.sats
@@ -17,11 +17,10 @@ fun table_set_at{n:int}(table: !table_t(n), i: sizeLt(ENTRY_COUNT), x: entry_t):
 overload [] with table_get_at
 overload [] with table_set_at
 
-// Set all the entries in the table to unused (zero)
-fn set_zero(&Table_t):<!wrt> void
-
 castfn consume(Table_t): void
 
-fun get_P4() : table_t 0
+fn get_P4() : table_t 0
+
+fn next_table{n : nat | n < 3}(table_t n, index : sizeLt(ENTRY_COUNT)) : Valid (table_t (n+1))
 
-fun next_table{n : nat | n < 3}(table_t n, sizeLt(ENTRY_COUNT)) : Valid (table_t (n+1))
+fn next_table_create{n : nat | n < 3}(table_t n, index : sizeLt(ENTRY_COUNT)) : Valid (table_t (n+1))