diff options
Diffstat (limited to 'kernel/memory/paging/entry.dats')
| -rw-r--r-- | kernel/memory/paging/entry.dats | 14 |
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 |