blob: 84a8bf49880f34c9e5f8eb5cffa12f77fef841cd (
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
|
#define ATS_DYNLOADFLAG 0
#include "kernel/prelude/kernel_prelude.hats"
staload UN = "prelude/SATS/unsafe.sats"
staload "./paging.sats"
staload "./frame.sats"
staload "lib/SATS/valid.sats"
assume entry_type = uint64
val zero = u2uint64(0u)
implement is_unused(entry) = entry = zero
implement set_unused(entry) = entry := zero
implement flag_contains(entry,flag) =
(entry land $UN.cast{uint64}(1 << (case+ flag 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
))) != zero
(* implement test() = let *)
(* in *)
(* (5,true) *)
(* end *)
|
