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
118
119
120
121
122
123
124
125
126
127
128
|
(*========================================================================*)
(* *)
(* Copyright (c) 2015-2017 Robert M. Norton *)
(* Copyright (c) 2015-2017 Kathyrn Gray *)
(* All rights reserved. *)
(* *)
(* This software was developed by the University of Cambridge Computer *)
(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *)
(* (REMS) project, funded by EPSRC grant EP/K008528/1. *)
(* *)
(* Redistribution and use in source and binary forms, with or without *)
(* modification, are permitted provided that the following conditions *)
(* are met: *)
(* 1. Redistributions of source code must retain the above copyright *)
(* notice, this list of conditions and the following disclaimer. *)
(* 2. Redistributions in binary form must reproduce the above copyright *)
(* notice, this list of conditions and the following disclaimer in *)
(* the documentation and/or other materials provided with the *)
(* distribution. *)
(* *)
(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *)
(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *)
(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *)
(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *)
(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *)
(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *)
(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *)
(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *)
(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *)
(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *)
(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *)
(* SUCH DAMAGE. *)
(*========================================================================*)
function bool tlbEntryMatch(r, vpn2, asid, (TLBEntry) entry) =
let entryValid = entry.valid in
let entryR = entry.r in
let entryMask = entry.pagemask in
let entryVPN = entry.vpn2 in
let entryASID = entry.asid in
let entryG = entry.g in
(entryValid &
(r == entryR) &
((vpn2 & ~(EXTZ(entryMask))) == ((entryVPN) & ~(EXTZ(entryMask)))) &
((asid == (entryASID)) | (entryG)))
function option<TLBIndexT> tlbSearch((bit[64]) VAddr) =
let r = (VAddr[63..62]) in
let vpn2 = (VAddr[39..13]) in
let asid = TLBEntryHi.ASID in {
foreach (idx from 0 to 63) {
if(tlbEntryMatch(r, vpn2, asid, (TLBEntries[idx]))) then
return (Some ((TLBIndexT) idx))
};
None
}
function (bit[64], bool) TLBTranslate2 ((bit[64]) vAddr, (MemAccessType) accessType) = {
let idx = tlbSearch(vAddr) in
switch(idx) {
case (Some(idx)) ->
let entry = (TLBEntries[idx]) in
let entryMask = entry.pagemask in
let evenOddBit = switch(entryMask) {
case 0x0000 -> 12
case 0x0003 -> 14
case 0x000f -> 16
case 0x003f -> 18
case 0x00ff -> 20
case 0x03ff -> 22
case 0x0fff -> 24
case 0x3fff -> 26
case 0xffff -> 28
case _ -> undefined
} in
let isOdd = (vAddr[evenOddBit]) in
let (caps, capl, (bit[24])pfn, d, v) = if (isOdd) then
(entry.caps1, entry.capl1, entry.pfn1, entry.d1, entry.v1)
else
(entry.caps0, entry.capl0, entry.pfn0, entry.d0, entry.v0) in
if (~(v)) then
(SignalExceptionTLB(if (accessType == StoreData) then XTLBInvS else XTLBInvL, vAddr))
else if ((accessType == StoreData) & ~(d)) then
(SignalExceptionTLB(TLBMod, vAddr))
else
(EXTZ(pfn[23..((evenOddBit)-(12))] : vAddr[((evenOddBit)-(1)) .. 0]),
if (accessType == StoreData) then caps else capl)
case None -> (SignalExceptionTLB(
if (accessType == StoreData) then XTLBRefillS else XTLBRefillL, vAddr))
}
}
(* perform TLB translation. bool is CHERI specific TLB bits noStoreCap/suppressTag *)
function (bit[64], bool) TLBTranslateC ((bit[64]) vAddr, (MemAccessType) accessType) =
{
let currentAccessLevel = getAccessLevel() in
let compat32 = (vAddr[61..31] == 0b1111111111111111111111111111111) in
let (requiredLevel, addr) = switch(vAddr[63..62]) {
case 0b11 -> switch(compat32, vAddr[30..29]) { (* xkseg *)
case (true, 0b11) -> (Kernel, None) (* kseg3 mapped 32-bit compat *)
case (true, 0b10) -> (Supervisor, None) (* sseg mapped 32-bit compat *)
case (true, 0b01) -> (Kernel, Some(EXTZ(vAddr[28..0]))) (* kseg1 unmapped uncached 32-bit compat *)
case (true, 0b00) -> (Kernel, Some(EXTZ(vAddr[28..0]))) (* kseg0 unmapped cached 32-bit compat *)
case (_, _) -> (Kernel, None) (* xkseg mapped *)
}
case 0b10 -> (Kernel, Some(EXTZ(vAddr[58..0]))) (* xkphys bits 61-59 are cache mode (ignored) *)
case 0b01 -> (Supervisor, None) (* xsseg - supervisor mapped *)
case 0b00 -> (User, None) (* xuseg - user mapped *)
} in
if ((int_of_accessLevel(currentAccessLevel)) < (int_of_accessLevel(requiredLevel))) then
(SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
else
let (pa, c) = switch(addr) {
case (Some(a)) -> (a, false)
case None -> if ((~(compat32)) & (unsigned(vAddr[61..0]) > MAX_VA)) then
(SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
else
TLBTranslate2(vAddr, accessType)
}
in if (unsigned(pa) > MAX_PA) then
(SignalExceptionBadAddr(if (accessType == StoreData) then AdES else AdEL, vAddr))
else
(pa, c)
}
function (bit[64]) TLBTranslate ((bit[64]) vAddr, (MemAccessType) accessType) =
let (addr, c) = TLBTranslateC(vAddr, accessType) in addr
|
