implement pageHEADmaster

1 files changed, 8 insertions, 6 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