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
|
#include "kernel/kernel_prelude.hats"
#define ATS_DYNLOADFLAG 0
staload "./idt.sats"
staload UN = "prelude/SATS/unsafe.sats"
%{
__attribute__ ((interrupt))
%}
// Default exception handler
fun default_exception_handler(frame: &int_frame) : void = let
in
println!("DEFAULT EXCEPTION HANDLER - NO ERROR CODE");
end
%{
__attribute__ ((interrupt))
%}
// Default exception handler (with error code)
fun default_exception_handler_e(frame: &int_frame, error_code : uint64) : void = let
in
println!("DEFAULT EXCEPTION HANDLER - ERROR CODE")
end
var idt : @[idt_entry_t][256] // The table
var idtr : idtr_t // interrupt descriptor table register instance
fun idt_set_descriptor {l:addr} {n : nat | n < 256} (vector: int n, isr: (&int_frame) -> void, flags: uint8) : void = let
extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (@[idt_entry_t][256]@l)
prval (pf, fpf) = __assert (addr@(idt))
val x = $UN.cast{uint64}(0xFFFF)
val y = $UN.cast{uint64}(0xFFFFFFF)
val entry = @{
isr_low = $UN.cast($UN.cast{uint64}(isr) land x),
kernel_cs = $UN.cast(0x08),
ist = $UN.cast(0),
attributes = flags,
isr_mid = $UN.cast(($UN.cast{uint64}(isr) >> 16) land x),
isr_high = $UN.cast(($UN.cast{uint64}(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#"
implement idt_init() : void = let
extern praxi __assert{l:addr} (ptr: ptr (l)): vtakeout0 (idtr_t@l)
prval (pf, fpf) = __assert (addr@(idtr))
fun loop {n : nat | n <= 32} (i : int n) : void = if (i < 32) then (idt_set_descriptor(i,default_exception_handler,$UN.cast(TRAP_GATE_FLAGS)); loop(i + 1))
in
idtr.base := addr@(idt);
idtr.limit := $UN.cast{uint16}(8 * 256);
loop(0);
setup(idtr);
let prval () = fpf(pf) in end
end
|
