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
|
#include "kernel/prelude/kernel_prelude.hats"
#define ATS_DYNLOADFLAG 0
staload "./idt.sats"
staload UN = "prelude/SATS/unsafe.sats"
extern typedef "int_frame" = int_frame
//----------------------------------No __attribute__ support in ats---------
%{
__attribute__ ((interrupt))
void default_exception_handler(int_frame *frame){
default_exception_handler2(frame);
}
__attribute__ ((interrupt))
void default_exception_handler_e(int_frame *frame, uint64_t error_code){
default_exception_handler_e2(frame, error_code);
}
__attribute__ ((interrupt))
void default_interrupt_handler(int_frame *frame, uint64_t error_code){
default_interrupt_handler_e2(frame, error_code);
}
__attribute__ ((interrupt))
void default_interrupt_handler_e(int_frame *frame, uint64_t error_code){
default_interrupt_handler_e2(frame, error_code);
}
%}
// DEFAULT HANDLERS, --------------------------------------------------
extern fun default_exception_handler2(frame: &int_frame) : void = "mac#"
implement default_exception_handler2(frame) : void = let
in
println!("DEFAULT EXCEPTION HANDLER - NO ERROR CODE");
end
extern fun default_exception_handler_e2(frame: &int_frame, error_code : uint64) : void = "mac#"
implement default_exception_handler_e2(frame,error_code) = let
in
println!("DEFAULT EXCEPTION HANDLER - WIDTH ERROR CODE");
end
extern fun default_interrupt_handler2(frame: &int_frame) : void = "mac#"
implement default_interrupt_handler2(frame) = let
in
println!("DEFAULT INTERRUPT HANDLER - NO ERROR CODE");
end
extern fun default_interrupt_handler_e2(frame: &int_frame, error_code : uint64) : void = "mac#"
implement default_interrupt_handler_e2(frame,error_code) = let
in
println!("DEFAULT INTERRUPT HANDLER - WIDTH ERROR CODE");
end
//-------------------------------------------------------
var idt : @[idt_entry_t][IDT_MAX_DESCRIPTORS] // The table
var idtr : idtr_t // interrupt descriptor table register instance
fun idt_set_descriptor {n : nat | n < IDT_MAX_DESCRIPTORS} (vector: int n, isr: uint64, flags: uint8) : void = let
extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (@[idt_entry_t][IDT_MAX_DESCRIPTORS]@l) // takeout proof UNSAFE:
prval (pf, fpf) = __assert (addr@(idt))
val x = $UN.cast{uint64}(0xFFFF)
val y = $UN.cast{uint64}(0xFFFFFFF)
val entry = @{
isr_low = $UN.cast(isr land x),
kernel_cs = $UN.cast(0x08),
ist = $UN.cast(0),
attributes = flags,
isr_mid = $UN.cast((isr >> 16) land x),
isr_high = $UN.cast((isr >> 32) land y),
reserved = $UN.cast(0)
}
in
idt[vector] := entry;
let prval () = fpf(pf) in end
end
extern typedef "idtr_t" = idtr_t
%{$
void setup(idtr_t idtr) {
__asm__ volatile ("lidt %0" : : "m"(idtr)); // load the new IDT
}
%}
extern fun setup(idtr : idtr_t) : void = "ext#"
// Setup exception handlers (vector 0-31)
fun setup_exceptions() = let
fun loop {n : nat | n <= 32} (i : int n) : void = if (i < 32) then (
idt_set_descriptor(i,$UN.cast(
case+ i of
| _ when i = 8 || i = 10 || i = 11 || i = 12
|| i = 13 || i = 14 || i = 17 || i = 22 => default_exception_handler_e
| _ => default_exception_handler
),$UN.cast(TRAP_GATE_FLAGS));
loop(i + 1)
)
in
loop(0)
end
// Setup trap interrupts (vector 32-255)
fun setup_interrupts() = let
fun loop {n : nat | n <= IDT_MAX_DESCRIPTORS && n >= 32} (i : int n) : void = if (i < IDT_MAX_DESCRIPTORS - 1) then (
idt_set_descriptor(i,$UN.cast(default_interrupt_handler),$UN.cast(INT_GATE_FLAGS));
loop(i + 1)
)
in
loop(32)
end
implement idt_init() : void = let
extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (idtr_t@l)
prval (pf, fpf) = __assert (addr@(idtr)) // takeout proof UNSAFE:
in
idtr.base := addr@(idt);
idtr.limit := $UN.cast(8 * IDT_MAX_DESCRIPTORS);
setup_exceptions();
setup_interrupts();
setup(idtr);
let prval () = fpf(pf) in end
end
|
