blob: d5029a7a2b9e8100284a82afd08964475a77ff87 (
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
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
#define ATS_DYNLOADFLAG 0
#include "kernel/prelude/kernel_prelude.hats"
staload "./table.sats"
staload "./entry.sats"
staload "lib/SATS/valid.sats"
staload "lib/DATS/valid.dats"
// Calculate table address of next table based on current table and index: P4->P3->P2->P1
fn next_table_address{l:agz}(pf : !table_t@l | p : ptr(l), index : sizeLt(ENTRY_COUNT)) : Valid Ptr1 = let
val entry = p->[index]
in
if (contains_flag(entry,PRESENT) && ~contains_flag(entry,HUGE_PAGE)) then
let
val next = g1ofg0((Ptr1_to_sz(p) << 9) lor (index << 12))
in
if next > i2sz(0) then
create_valid(sz_to_Ptr1(next))
else
create_unvalid()
end
else
create_unvalid()
end
implement set_zero(table) = let
implement array_foreach$fwork<entry_t><void>(entry,v) = set_unused(entry)
in
assertloc(array_foreach<entry_t>(table,i2sz(ENTRY_COUNT)) = i2sz(ENTRY_COUNT))
end
// UNSAFE: unsafe block
local
staload UN = "prelude/SATS/unsafe.sats"
in
implement get_P4() = @{
ptr = $UN.ptr_vtake(ulint_to_Ptr1(0xfffffffffffff000ul)),
level = (0u | )
}
implement next_table(tp,index) = let
val k = tp.ptr
val next = next_table_address(k.0 | k.2,index)
prval () = k.1 k.0
in
if is_valid(next) then
let
val p = unwrap_valid(next)
in
create_valid(@{
ptr = $UN.ptr_vtake(p),
level = ( succ(tp.level.0) | )
})
end
else
let
val () = destroy_unvalid(next)
in
create_unvalid()
end
end
end
|
