From 70cca66089896730797a71ba545c7f4e87b12975 Mon Sep 17 00:00:00 2001 From: Xander Date: Sun, 20 Aug 2023 22:57:07 +0200 Subject: implement page --- kernel/memory/paging/entry.dats | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'kernel/memory/paging/entry.dats') 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(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(f,k) = k := add_flag(k,f) var k = g0ofg1(u2u64(0u)) - val _ = array_foreach_env(arr,n,k) + val _ = $effmask_all(array_foreach_env(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 -- cgit v1.2.3