blob: 7fa97b9edd8283961fb890a200b81d47a37c3dd5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
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
|
