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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
|
#define ATS_DYNLOADFLAG 0
#include "kernel/prelude/kernel_prelude.hats"
staload "./page.sats"
staload FR = "kernel/memory/frame.sats"
staload "./table.sats"
staload "lib/SATS/valid.sats"
staload "lib/DATS/valid.dats"
datatype table_level =
| Level4
| Level3
| Level2
| Level1
fn start_address(page : page_t) : size_t = page.num * $FR.PAGE_SIZE
fn get_index(page: page_t,n : intLte(3)) = g1ofg0((page.num >> (27 - 9 * n)) land i2sz(511))
//NOTE: huge page handler not implemented
fn translate_page(page: page_t) : Valid $FR.frame_t = let
fun loop{n : nat | n < 3}.<3-n>.(table : table_t n, count : int n) : Valid $FR.frame_t = let
staload "./entry.sats"
val index = get_index(page,count)
in
if index < ENTRY_COUNT then let
val v = next_table(table,index)
in
if is_valid(v) then let
val table_next = unwrap_valid(v)
in
if count < 2 then
loop(table_next,succ(count))
else(
consume(table_next);
frame
) where {
val index = get_index(page,count+1)
val frame = (if index < ENTRY_COUNT then pointed_frame(table_next[index]) else create_unvalid()) : Valid $FR.frame_t
}
end
else (
destroy_unvalid(v);
println!("Unvalid table pointer encountered: ", count);
create_unvalid())
end
else (
consume(table);
println!("Table index too big");
create_unvalid())
end
in
loop(get_P4(),0)
end
implement translate(virtual_addr) = let
val offset = Ptr0_to_sz(virtual_addr) % i2sz($FR.PAGE_SIZE)
val vframe = translate_page(containing_address(virtual_addr))
in
if is_valid(vframe) then let
val frame = unwrap_valid(vframe)
in
create_valid (sz_to_Ptr0(frame.num * $FR.PAGE_SIZE + offset))
end
else (
destroy_unvalid(vframe);
create_unvalid();
)
end
implement containing_address(address) = (
assertloc(address < ulint_to_Ptr0(0x0000800000000000ul) ||
address >= ulint_to_Ptr0(0xFFFF800000000000ul));
@{num = Ptr0_to_sz(address) / i2sz($FR.PAGE_SIZE)}
)
// TODO: implement and_then and or_else for valid (like in rust)
implement map_to{s}(page,frame,flags,size) = let
staload "./entry.sats"
fun loop{n : nat | n < 3}.<3-n>.(table : table_t n, count : int n, flags: &(@[entry_flag][s])) : void = let
staload "lib/SATS/panic.sats"
val index = get_index(page,count)
val () = println!(index)
in
if index < ENTRY_COUNT then let
val v = next_table_create(table,index)
in
if is_valid(v) then let
val table_next = unwrap_valid(v)
in
if count < 2 then
loop(table_next,succ(count),flags)
else let
val index = get_index(page,count+1)
in
if index < ENTRY_COUNT then (
assertloc(is_unused(table_next[index]));
table_next[index] := add_flag(create_entry(frame, flags,size),PRESENT);
);
consume(table_next);
end
end
else (
destroy_unvalid(v);
panic("Could not create table"))
end
else (
consume(table);
println!("Table index too big"))
end
in
loop(get_P4(),0,flags)
end
implement map(page,flags,size) = map_to(page,$FR.allocate_frame(),flags,size)
|
