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
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
|
$include <elf.sail>
val read_register = "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
// EL1 physical EL2 physical EL3 physical EL1 virtual, EL2 virtual
let CNT_CVAL = [ref CNTP_CVAL_EL0, ref CNTHP_CVAL_EL2, ref CNTPS_CVAL_EL1, ref CNTV_CVAL_EL0, ref CNTHV_CVAL_EL2]
let CNT_TVAL = [ref CNTP_TVAL_EL0, ref CNTHP_TVAL_EL2, ref CNTPS_TVAL_EL1, ref CNTV_TVAL_EL0, ref CNTHV_TVAL_EL2]
let CNT_CTL = [ref CNTP_CTL_EL0, ref CNTHP_CTL_EL2, ref CNTPS_CTL_EL1, ref CNTV_CTL_EL0, ref CNTHV_CTL_EL2 ]
let CNT_CTL = [ref CNTP_CTL_EL0, ref CNTHP_CTL_EL2, ref CNTPS_CTL_EL1, ref CNTV_CTL_EL0, ref CNTHV_CTL_EL2 ]
let CNT_IRQ = [0x0000_000d, 0x0000_000a, 0x0000_03ff, 0x0000_000b, 0x0000_03ff ]
// No IRQ No IRQ?
// SGI Interrupts are 0-15, PPI interrupts are 16-31, so SPI interrupts have an offset of 32.
let SPI_OFFSET = 32
// Simple top level fetch and execute loop.
val fetch_and_execute : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
register cycle_counter : int
function fetch_and_execute () = {
cycle_counter = 0;
while true do {
cycle_counter = cycle_counter + 1;
try {
// Increment the counter
CNTPCT_EL0 = CNTPCT_EL0 + 1;
CNTVCT_EL0 = CNTPCT_EL0 - CNTVOFF_EL2;
// Timer value view for each timer
foreach (timer from 0 to 4) {
let TVAL = CNT_TVAL[timer];
let nextTVAL = read_register(TVAL) - 1;
(*TVAL) = nextTVAL;
if nextTVAL == 0x0000_0000 then {
_IRQPending = true;
AArch64_TakePhysicalIRQException()
}
};
// Handle the Kernel event stream, if enabled by CNTKCTL_EL1[2].
if CNTKCTL_EL1[2] == bitone then {
let mask = LSL(ZeroExtend(0x1, 64), UInt(CNTKCTL_EL1[7 .. 4]));
// Trigger event stream on either rising bit (0-1, bitzero) or falling (1-0, bitone)
let trigger : bool = if CNTKCTL_EL1[3] == bitzero then {
((CNTVCT_EL0 - 1) & mask) == Zeros() & (CNTVCT_EL0 & mask) != Zeros()
} else {
((CNTVCT_EL0 - 1) & mask) != Zeros() & (CNTVCT_EL0 & mask) == Zeros()
};
if trigger & PSTATE.I == bitzero then {
_IRQPending = true;
AArch64_TakePhysicalIRQException()
}
};
// Handle the Hypervisor event stream, if enabled by CNTHCTL_EL2[2].
if CNTHCTL_EL2[2] == bitone then {
let mask = LSL(ZeroExtend(0x1, 64), UInt(CNTHCTL_EL2[7 .. 4]));
// Trigger event stream on either rising bit (0-1, bitzero) or falling (1-0, bitone)
let trigger : bool = if CNTHCTL_EL2[3] == bitzero then {
((CNTPCT_EL0 - 1) & mask) == Zeros() & (CNTPCT_EL0 & mask) != Zeros()
} else {
((CNTPCT_EL0 - 1) & mask) != Zeros() & (CNTPCT_EL0 & mask) == Zeros()
};
if trigger & PSTATE.I == bitzero then {
prerr("[Clock] Tick\n");
_IRQPending = true;
AArch64_TakePhysicalIRQException()
}
};
var prevEL = PSTATE.EL;
var prevI = PSTATE.I;
// Store the old values of the Counter-timer Kernel/Hypervisor Control
// registers, as we want to figure out when they changes.
var prevCNTKCTL_EL1 = CNTKCTL_EL1;
var prevCNTHCTL_EL2 = CNTHCTL_EL2;
if ~(__Sleeping()) then {
// Check for pending interrupts
var interrupt_req : InterruptReq = undefined;
interrupt_req.take_SE = true; interrupt_req.take_vSE = true;
interrupt_req.take_IRQ = true; interrupt_req.take_vIRQ = true;
interrupt_req.take_FIQ = true; interrupt_req.take_vFIQ = true;
var interrupted = false;
try {
interrupted = TakePendingInterrupts(interrupt_req);
if interrupted then {
print("Pending interrupt taken\n");
}
} catch {
_ => {
print("Unhandled exception while pending exceptions\n");
}
};
var ok = true;
if ok then {
try {
__currentInstr = __fetchA64();
__currentInstrLength = 4;
ok = true;
} catch {
Error_ExceptionTaken() => {
print(concat_str("Exception taken during IFetch from PC=", concat_str(HexStr(UInt(aget_PC())), "\n")));
},
_ => {
print("Exiting due to unhandled exception during fetch\n");
exit()
}
};
if ok then {
try {
__PC_changed = false;
ShouldAdvanceIT = (PSTATE.nRW == [bitone]) & (PSTATE.T == [bitone]);
decode(__currentInstr);
} catch {
// note: if supporting AArch32 as well, call _UndefinedFault() instead
Error_Undefined() => try { AArch64_UndefinedFault() } catch { _ => print("Exception during Undefined recovery\n") },
Error_See(_) => try { AArch64_UndefinedFault() } catch { _ => print("Exception during SEE recovery\n") },
Error_ReservedEncoding(_) => try { AArch64_UndefinedFault() } catch { _ => print("Exception during ReservedEncoding recovery\n") },
Error_ExceptionTaken() => {
print(concat_str("ExceptionTaken during Decode/Execute from PC=", concat_str(HexStr(UInt(aget_PC())), concat_str(" opcode=", concat_str(HexStr(UInt(__currentInstr)), "\n")))));
// print(" This might just be a HINT like 0xd50320df\n");
()
},
Error_Implementation_Defined(s) => {
print(concat_str("Ignoring IMPLEMENTATION_DEFINED", concat_str(s, "\n")));
}
}
};
if ~(__PC_changed) then _PC = _PC + __currentInstrLength else ();
if ShouldAdvanceIT then AArch32_ITAdvance() else ();
SSAdvance();
__UpdateSystemCounter(); // should this happen even if sleeping?
}
};
// We want to keep track of what exception level we are in for debugging purposes.
if UInt(prevEL) > UInt(PSTATE.EL) then {
prerr_bits("[Sail] Exception level dropped to: ", PSTATE.EL)
};
if prevI != PSTATE.I then {
prerr_bits("[Sail] PSTATE.I changed to: ", PSTATE.I);
print(concat_str(" at PC=", concat_str(HexStr(UInt(aget_PC())), concat_str(" in cycle=", concat_str(DecStr(cycle_counter), "\n")))));
};
if prevCNTKCTL_EL1 != CNTKCTL_EL1 then {
prerr_bits("[Clock] CNTKCTL_EL1 changed to ", CNTKCTL_EL1);
};
if prevCNTHCTL_EL2 != CNTHCTL_EL2 then {
prerr_bits("[Clock] CNTHCTL_EL2 changed to ", CNTHCTL_EL2);
}
} catch {
Error_See(str) if str == "HINT" => (),
Error_ExceptionTaken(_) => {
// enable_tracing()
()
},
_ => {
prerr("Exiting due to unhandled exception\n");
exit()
}
};
__EndCycle() // advance state of non-sleeping parts of the system
}
}
let COLD_RESET : bool = true
val "load_raw" : (bits(64), string) -> unit
val init : unit -> unit effect {escape, undef, rreg, wreg}
function init() = {
__currentInstrLength = 4;
TakeReset(COLD_RESET);
_PC = CFG_RVBAR;
}
val main : unit -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
function main() = {
init();
fetch_and_execute()
}
|
