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
|
/* PTE attributes, permission checks and updates */
type pteAttribs = bits(8)
/* Reserved PTE bits could be used by extensions on RV64. There are
* no such available bits on RV32, so these bits will be zeros on RV32.
*/
type extPte = bits(10)
bitfield PTE_Bits : pteAttribs = {
D : 7,
A : 6,
G : 5,
U : 4,
X : 3,
W : 2,
R : 1,
V : 0
}
function isPTEPtr(p : pteAttribs, ext : extPte) -> bool = {
let a = Mk_PTE_Bits(p);
a.R() == 0b0 & a.W() == 0b0 & a.X() == 0b0
}
function isInvalidPTE(p : pteAttribs, ext : extPte) -> bool = {
let a = Mk_PTE_Bits(p);
a.V() == 0b0 | (a.W() == 0b1 & a.R() == 0b0)
}
union PTE_Check = {
PTE_Check_Success : ext_ptw,
PTE_Check_Failure : (ext_ptw, ext_ptw_fail)
}
function to_pte_check(b : bool) -> PTE_Check =
if b then PTE_Check_Success(()) else PTE_Check_Failure((), ())
/* For extensions: this function gets the extension-available bits of the PTE in extPte,
* and the accumulated information of the page-table-walk in ext_ptw. It should return
* the updated ext_ptw in both the success and failure cases.
*/
function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits, ext : extPte, ext_ptw : ext_ptw) -> PTE_Check = {
match (ac, priv) {
(Read(_), User) => to_pte_check(p.U() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
(Write(_), User) => to_pte_check(p.U() == 0b1 & p.W() == 0b1),
(ReadWrite(_, _), User) => to_pte_check(p.U() == 0b1 & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
(Execute(), User) => to_pte_check(p.U() == 0b1 & p.X() == 0b1),
(Read(_), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
(Write(_), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & p.W() == 0b1),
(ReadWrite(_, _), Supervisor) => to_pte_check((p.U() == 0b0 | do_sum) & p.W() == 0b1 & (p.R() == 0b1 | (p.X() == 0b1 & mxr))),
(Execute(), Supervisor) => to_pte_check(p.U() == 0b0 & p.X() == 0b1),
(_, Machine) => internal_error("m-mode mem perm check")
}
}
function update_PTE_Bits(p : PTE_Bits, a : AccessType(ext_access_type), ext : extPte) -> option((PTE_Bits, extPte)) = {
let update_d = p.D() == 0b0 & (match a { // dirty-bit
Execute() => false,
Read() => false,
Write(_) => true,
ReadWrite(_,_) => true
});
let update_a = p.A() == 0b0; // accessed-bit
if update_d | update_a then {
let np = update_A(p, 0b1);
let np = if update_d then update_D(np, 0b1) else np;
Some(np, ext)
} else None()
}
|