blob: 76d6c0cb4c1517de643663f0a538051fc021e5c9 (
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
53
54
|
#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)
implement add_flag(entry,f) = entry 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
))
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 _ = $effmask_all(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](flag)
}
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 create_entry(frame,flags,n) = let
val x = Ptr0_to_u64($FRAME.start_address(frame))
in
assertloc((x land u2u64(0xFFF0000000000FFFu)) = zero);
(x lor flags2entry(flags,n))
end
|
