annotate ppc/keiko.ml @ 0:bfdcc3820b32

Basis
author Mike Spivey <mike@cs.ox.ac.uk>
date Thu, 05 Oct 2017 08:04:15 +0100
parents
children
rev   line source
0
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
1 (* ppc/keiko.ml *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
2 (* Copyright (c) 2017 J. M. Spivey *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
3
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
4 open Print
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
5
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
6 (* |symbol| -- global symbols *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
7 type symbol = string
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
8
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
9 type codelab = int
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
10
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
11 let nolab = -1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
12
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
13 (* |lab| -- last used code label *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
14 let lab = ref 0
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
15
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
16 (* |label| -- allocate a code label *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
17 let label () = incr lab; !lab
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
18
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
19 (* |fLab| -- format a code label for printf *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
20 let fLab n = fMeta "L$" [fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
21
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
22 let nosym = "*nosym*"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
23
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
24 let gensym () = sprintf "g$" [fNum (label ())]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
25
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
26 (* |op| -- type of picoPascal operators *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
27 type op = Plus | Minus | Times | Div | Mod | Eq
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
28 | Uminus | Lt | Gt | Leq | Geq | Neq | And | Or | Not
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
29 | Lsl | Lsr | Asr | BitAnd | BitOr | BitNot
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
30
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
31 (* |code| -- type of intermediate instructions *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
32 type code =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
33 CONST of int (* Constant (value) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
34 | GLOBAL of symbol (* Constant (symbol) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
35 | LOCAL of int (* Local address (offset) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
36 | LOAD of int (* Load (size) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
37 | STORE of int (* Store (size) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
38 | FIXCOPY (* Copy multiple values (size) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
39 | PCALL of int * int (* Call procedure (nparams, rsize) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
40 | RETURN of int (* Procedure return (rsize) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
41 | MONOP of op (* Perform unary operation (op) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
42 | BINOP of op (* Perform binary operation (op) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
43 | OFFSET (* Add address and offset *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
44 | BOUND of int (* Array bound check (line) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
45 | NCHECK of int (* Null pointer check (line) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
46 | ERETURN of int (* Failure to return (line) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
47 | LABEL of codelab (* Set code label *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
48 | JUMP of codelab (* Unconditional branch (dest) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
49 | JUMPC of op * codelab (* Conditional branch (cond, dest) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
50 | JCASE of codelab list (* Jump table *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
51 | LINE of int (* Line number *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
52
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
53 | LDL of int * int (* LDL (n, s) = LOCAL n / LOAD s *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
54 | STL of int * int (* STL (n, s) = LOCAL n / STORE s *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
55 | LDG of symbol * int (* LDG (x, s) = GLOBAL x / LOAD s *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
56 | STG of symbol * int (* STG (x, s) = GLOBAL x / STORE s *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
57 | LDNW of int (* LDNW n = CONST n / OFFSET / LOAD 4 *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
58 | STNW of int (* STNW n = CONST n / OFFSET / STORE 4 *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
59 | LDI of int (* LDI s = CONST s / TIMES / OFFSET / LOAD s *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
60 | STI of int (* STI s = CONST s / TIMES / OFFSET / STORE s *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
61 | JUMPCZ of op * codelab (* Conditional branch with zero (cond, dest) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
62
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
63 | SEQ of code list (* Sequence of other instructions *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
64 | NOP (* Null operation *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
65
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
66 let mark_line n ys =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
67 if n = 0 then ys else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
68 match ys with
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
69 [] | LINE _ :: _ -> ys
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
70 | _ -> LINE n :: ys
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
71
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
72 let canon x =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
73 let rec accum x ys =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
74 match x with
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
75 SEQ xs -> List.fold_right accum xs ys
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
76 | NOP -> ys
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
77 | LINE n -> mark_line n ys
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
78 | _ -> x :: ys in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
79 SEQ (accum x [])
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
80
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
81 let op_name =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
82 function
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
83 Plus -> "PLUS" | Minus -> "MINUS" | Times -> "TIMES"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
84 | Div -> "DIV" | Mod -> "MOD" | Eq -> "EQ"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
85 | Uminus -> "UMINUS" | Lt -> "LT" | Gt -> "GT"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
86 | Leq -> "LEQ" | Geq -> "GEQ" | Neq -> "NEQ"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
87 | And -> "AND" | Or -> "OR" | Not -> "NOT"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
88 | Lsl -> "LSL" | Lsr -> "LSR" | Asr -> "ASR"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
89 | BitAnd -> "BITAND" | BitOr -> "BITOR" | BitNot -> "BITNOT"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
90
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
91 let fOp w = fStr (op_name w)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
92
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
93 let fType =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
94 function 1 -> fStr "C" | 4 -> fStr "W" | s -> fMeta "*$*" [fNum s]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
95
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
96 let fType1 =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
97 function 0 -> fStr "" | 1 -> fStr "W" | s -> fMeta "*$*" [fNum s]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
98
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
99 let fInst =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
100 function
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
101 CONST x -> fMeta "CONST $" [fNum x]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
102 | GLOBAL a -> fMeta "GLOBAL $" [fStr a]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
103 | LOCAL n -> fMeta "LOCAL $" [fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
104 | LOAD s -> fMeta "LOAD$" [fType s]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
105 | STORE s -> fMeta "STORE$" [fType s]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
106 | FIXCOPY -> fStr "FIXCOPY"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
107 | PCALL (n, s) -> fMeta "PCALL$ $" [fType1 s; fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
108 | RETURN s -> fMeta "RETURN$" [fType1 s]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
109 | MONOP w -> fStr (op_name w)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
110 | BINOP w -> fStr (op_name w)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
111 | OFFSET -> fStr "OFFSET"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
112 | BOUND n -> fMeta "BOUND $" [fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
113 | NCHECK n -> fMeta "NCHECK $" [fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
114 | ERETURN n -> fMeta "ERROR E_RETURN $" [fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
115 | LABEL l -> fMeta "LABEL $" [fLab l]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
116 | JUMP l -> fMeta "JUMP $" [fLab l]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
117 | JUMPC (w, l) -> fMeta "J$ $" [fStr (op_name w); fLab l]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
118 | JCASE labs -> fMeta "JCASE $" [fNum (List.length labs)]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
119 | LINE n -> fMeta "LINE $" [fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
120
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
121 | LDL (n, s) -> fMeta "LDL$ $" [fType s; fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
122 | STL (n, s) -> fMeta "STL$ $" [fType s; fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
123 | LDG (x, s) -> fMeta "LDG$ $" [fType s; fStr x]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
124 | STG (x, s) -> fMeta "STG$ $" [fType s; fStr x]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
125 | LDNW n -> fMeta "LDNW $" [fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
126 | STNW n -> fMeta "STNW $" [fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
127 | LDI s -> fMeta "LDI$" [fType s]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
128 | STI s -> fMeta "STI$" [fType s]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
129 | JUMPCZ (w, lab) -> fMeta "J$Z $" [fStr (op_name w); fLab lab]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
130
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
131 | SEQ _ -> fStr "SEQ ..."
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
132 | NOP -> fStr "NOP"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
133
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
134 (* |output| -- output code sequence *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
135 let output code =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
136 let line = ref 0 in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
137 let rec out =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
138 function
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
139 SEQ xs -> List.iter out xs
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
140 | NOP -> ()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
141 | LINE n ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
142 if !line <> n then begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
143 printf "! $\n" [fStr (Source.get_line n)];
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
144 line := n
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
145 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
146 | JCASE labs ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
147 printf "$\n" [fInst (JCASE labs)];
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
148 List.iter (fun lab -> printf "CASEL $\n" [fLab lab]) labs
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
149 | x -> printf "$\n" [fInst x] in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
150 out code
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
151
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
152
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
153 let int_of_bool b = if b then 1 else 0
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
154
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
155 (* |do_monop| -- evaluate unary operators *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
156 let do_monop w x =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
157 match w with
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
158 Uminus -> - x
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
159 | Not -> if x <> 0 then 0 else 1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
160 | BitNot -> lnot x
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
161 | _ -> failwith "do_monop"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
162
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
163 (* |do_binop| -- evaluate binary operators *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
164 let do_binop w x y =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
165 match w with
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
166 Plus -> x + y
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
167 | Minus -> x - y
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
168 | Times -> x * y
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
169 | Div -> x / y
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
170 | Mod -> x mod y
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
171 | Eq -> int_of_bool (x = y)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
172 | Lt -> int_of_bool (x < y)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
173 | Gt -> int_of_bool (x > y)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
174 | Leq -> int_of_bool (x <= y)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
175 | Geq -> int_of_bool (x >= y)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
176 | Neq -> int_of_bool (x <> y)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
177 | And -> if x <> 0 then y else 0
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
178 | Or -> if x <> 0 then 1 else y
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
179 | Lsl -> x lsl y
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
180 | Lsr -> x lsr y
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
181 | Asr -> x asr y
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
182 | BitAnd -> x land y
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
183 | BitOr -> x lor y
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
184 | _ -> failwith (sprintf "do_binop $" [fOp w])
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
185
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
186 (* |negate| -- negation of a comparison *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
187 let negate =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
188 function Eq -> Neq | Neq -> Eq | Lt -> Geq
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
189 | Leq -> Gt | Gt -> Leq | Geq -> Lt
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
190 | _ -> failwith "negate"