annotate lab2/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 (* common/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 Tree
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
5 open Print
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
6
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
7 (* |codelab| -- type of code labels *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
8 type codelab = int
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
9
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
10 (* |lastlab| -- last used code label *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
11 let lastlab = ref 0
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
12
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
13 (* |label| -- allocate a code label *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
14 let label () = incr lastlab; !lastlab
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
15
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
16 (* |fLab| -- format a code label for printf *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
17 let fLab n = fMeta "L$" [fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
18
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
19 (* |op| -- type of picoPascal operators *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
20 type op = Plus | Minus | Times | Div | Mod | Eq
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
21 | Uminus | Lt | Gt | Leq | Geq | Neq | And | Or | Not
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
22
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
23 (* |code| -- type of intermediate instructions *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
24 type code =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
25 CONST of int (* Push constant (value) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
26 | GLOBAL of string (* Push global address (name) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
27 | LOCAL of int (* Push local adddress (offset) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
28 | LOADW (* Load word *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
29 | STOREW (* Store word *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
30 | LOADC (* Load character *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
31 | STOREC (* Store character *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
32 | MONOP of op (* Perform unary operation (op) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
33 | BINOP of op (* Perform binary operation (op) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
34 | OFFSET (* Add address and offset *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
35 | LABEL of codelab (* Set code label *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
36 | JUMP of codelab (* Unconditional branch (dest) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
37 | JUMPC of op * codelab (* Conditional branch (op, dest) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
38 | PCALL of int (* Call procedure *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
39 | PCALLW of int (* Proc call with result (nargs) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
40 | RETURNW (* Return from procedure *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
41 | BOUND of int (* Bounds check *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
42 | CASEJUMP of int (* Case jump (num cases) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
43 | CASEARM of int * codelab (* Case value and label *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
44 | PACK (* Pack two values into one *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
45 | UNPACK (* Unpack one value into two *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
46 | DUP
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
47 | POP
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
48
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
49 | LDGW of string (* Load Global Word (name) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
50 | STGW of string (* Store Global Word (name) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
51 | LDLW of int (* Load Local Word (offset) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
52 | STLW of int (* Store Local Word (offset) *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
53 | LDNW of int (* Load word with offset *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
54 | STNW of int (* Store word with offset *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
55
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
56 | LINE of int
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
57 | SEQ of code list
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
58 | NOP
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
59
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
60 (* op_name -- map an operator to its name *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
61 let op_name =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
62 function
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
63 Plus -> "Plus" | Minus -> "Minus" | Times -> "Times"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
64 | Div -> "Div" | Mod -> "Mod" | Eq -> "Eq"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
65 | Uminus -> "Uminus" | Lt -> "Lt" | Gt -> "Gt"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
66 | Leq -> "Leq" | Geq -> "Geq" | Neq -> "Neq"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
67 | And -> "And" | Or -> "Or" | Not -> "Not"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
68
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
69 (* fOp -- format an operator as an instruction *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
70 let fOp w =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
71 (* Avoid the deprecated String.uppercase *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
72 let upc ch =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
73 if ch >= 'a' && ch <= 'z' then Char.chr (Char.code ch - 32) else ch in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
74 fStr (String.map upc (op_name w))
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
75
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
76 (* |fInst| -- format an instruction for |printf| *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
77 let fInst =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
78 function
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
79 CONST x -> fMeta "CONST $" [fNum x]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
80 | GLOBAL a -> fMeta "GLOBAL $" [fStr a]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
81 | LOCAL n -> fMeta "LOCAL $" [fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
82 | LOADW -> fStr "LOADW"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
83 | STOREW -> fStr "STOREW"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
84 | LOADC -> fStr "LOADC"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
85 | STOREC -> fStr "STOREC"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
86 | MONOP w -> fOp w
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
87 | BINOP w -> fOp w
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
88 | OFFSET -> fStr "OFFSET"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
89 | LABEL l -> fMeta "LABEL $" [fLab l]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
90 | JUMP l -> fMeta "JUMP $" [fLab l]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
91 | JUMPC (w, l) -> fMeta "J$ $" [fOp w; fLab l]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
92 | PCALL n -> fMeta "PCALL $" [fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
93 | PCALLW n -> fMeta "PCALLW $" [fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
94 | RETURNW -> fStr "RETURNW"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
95 | BOUND n -> fMeta "BOUND $" [fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
96 | CASEJUMP n -> fMeta "CASEJUMP $" [fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
97 | CASEARM (v, l) -> fMeta "CASEARM $ $" [fNum v; fLab l]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
98 | PACK -> fStr "PACK"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
99 | UNPACK -> fStr "UNPACK"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
100 | DUP -> fStr "DUP 0"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
101 | POP -> fStr "POP 1"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
102 | LDGW a -> fMeta "LDGW $" [fStr a]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
103 | STGW a -> fMeta "STGW $" [fStr a]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
104 | LDLW n -> fMeta "LDLW $" [fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
105 | STLW n -> fMeta "STLW $" [fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
106 | LDNW n -> fMeta "LDNW $" [fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
107 | STNW n -> fMeta "STNW $" [fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
108 | LINE n -> fMeta "LINE $" [fNum n]
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
109 | SEQ _ -> fStr "SEQ ..."
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
110 | NOP -> fStr "NOP"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
111
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
112 let mark_line n ys =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
113 if n = 0 then ys else
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
114 match ys with
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
115 [] | LINE _ :: _ -> ys
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
116 | _ -> LINE n :: ys
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
117
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
118 (* |canon| -- flatten a code sequence *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
119 let canon x =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
120 let rec accum x ys =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
121 match x with
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
122 SEQ xs -> List.fold_right accum xs ys
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
123 | NOP -> ys
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
124 | LINE n ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
125 if n = 0 then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
126 ys
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
127 else begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
128 match ys with
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
129 [] -> ys
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
130 | LINE _ :: _ -> ys
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
131 | _ -> LINE n :: ys
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
132 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
133 | _ -> x :: ys in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
134 SEQ (accum x [])
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
135
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
136
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
137 (* SANITY CHECKS *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
138
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
139 (* The checks implemented here ensure that the value stack is used in a
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
140 consistent way, and that CASEJUMP instructions are followed by the
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
141 correct number of case labels. There are a few assumptions, the main
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
142 one being that backwards jumps leave nothing on the stack. *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
143
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
144 (* Compute pair (a, b) if an instruction pops a values and pushes b *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
145 let delta =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
146 function
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
147 CONST _ | GLOBAL _ | LOCAL _ | LDGW _ | LDLW _ -> (0, 1)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
148 | STGW _ | STLW _ -> (1, 0)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
149 | LOADW | LOADC | LDNW _ -> (1, 1)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
150 | STOREW | STOREC | STNW _ -> (2, 0)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
151 | MONOP _ -> (1, 1)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
152 | BINOP _ | OFFSET -> (2, 1)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
153 | PCALL n -> (n+2, 0)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
154 | PCALLW n -> (n+2, 1)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
155 | RETURNW -> (1, 0)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
156 | BOUND _ -> (2, 1)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
157 | PACK -> (2, 1)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
158 | UNPACK -> (1, 2)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
159 | LINE _ -> (0, 0)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
160 | DUP -> (1, 2)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
161 | POP -> (1, 0)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
162 | i -> failwith (sprintf "delta $" [fInst i])
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
163
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
164 (* Output code and check for basic sanity *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
165 let check_and_output code =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
166 let line = ref 0 in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
167
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
168 (* Output an instruction *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
169 let out =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
170 function
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
171 LINE n ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
172 if n <> 0 && !line <> n then begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
173 printf "! $\n" [fStr (Source.get_line n)];
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
174 line := n
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
175 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
176 | x -> printf "$\n" [fInst x] in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
177
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
178 (* Report failure of sanity checks *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
179 let insane fmt args =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
180 fprintf stderr "WARNING: Code failed sanity checks -- $\n" [fMeta fmt args];
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
181 printf "! *** HERE!\n" [];
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
182 raise Exit in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
183
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
184 (* Map labels to (depth, flag) pairs *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
185 let labdict = Hashtbl.create 50 in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
186
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
187 (* Note the depth at a label and check for consistency *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
188 let note_label lab def d =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
189 try
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
190 let (d1, f) = Hashtbl.find labdict lab in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
191 if d >= 0 && d <> d1 then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
192 insane "inconsistent stack depth ($ <> $) at label $"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
193 [fNum d; fNum d1; fNum lab];
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
194 if def then begin
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
195 if !f then insane "multiply defined label $" [fNum lab];
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
196 f := true
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
197 end;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
198 d1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
199 with Not_found ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
200 (* If this point is after an unconditional jump (d < 0) and
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
201 the label is not defined previously, assume depth 0 *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
202 let d1 = max d 0 in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
203 Hashtbl.add labdict lab (d1, ref def);
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
204 d1 in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
205
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
206 (* Check all mentioned labels have been defined *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
207 let check_labs () =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
208 Hashtbl.iter (fun lab (d, f) ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
209 if not !f then insane "label $ is not defined" [fNum lab]) labdict in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
210
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
211 let tail = ref [] in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
212
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
213 let output () = out (List.hd !tail); tail := List.tl !tail in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
214
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
215 (* Scan an instruction sequence, keeping track of the stack depth *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
216 let rec scan d =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
217 match !tail with
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
218 [] ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
219 if d <> 0 then insane "stack not empty at end" []
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
220 | x :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
221 let need a =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
222 if d < a then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
223 insane "stack underflow at instruction $" [fInst x] in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
224 output ();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
225 begin match x with
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
226 LABEL lab ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
227 scan (note_label lab true d)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
228 | JUMP lab ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
229 unreachable (note_label lab false d)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
230 | JUMPC (_, lab) ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
231 need 2; scan (note_label lab false (d-2))
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
232 | CASEARM (_, _) ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
233 insane "unexpected CASEARM" []
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
234 | CASEJUMP n ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
235 need 1; jumptab n (d-1)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
236 | SEQ _ | NOP ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
237 failwith "sanity2"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
238 | _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
239 let (a, b) = delta x in need a; scan (d-a+b)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
240 end
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
241
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
242 (* Scan a jump table, checking for the correct number of entries *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
243 and jumptab n d =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
244 match !tail with
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
245 CASEARM (_, lab) :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
246 output ();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
247 if n = 0 then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
248 insane "too many CASEARMs after CASEJUMP" [];
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
249 jumptab (n-1) (note_label lab false d)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
250 | _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
251 if n > 0 then
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
252 insane "too few CASEARMs after CASEJUMP" [];
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
253 scan d
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
254
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
255 (* Scan code after an unconditional jump *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
256 and unreachable d =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
257 match !tail with
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
258 [] -> ()
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
259 | LABEL lab :: _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
260 output ();
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
261 scan (note_label lab true (-1))
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
262 | _ ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
263 (* Genuinely unreachable code -- assume stack is empty *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
264 scan 0 in
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
265
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
266 match canon code with
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
267 SEQ xs ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
268 tail := xs;
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
269 (try scan 0; check_labs () with Exit ->
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
270 (* After error, output rest of code without checks *)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
271 List.iter out !tail; exit 1)
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
272 | _ -> failwith "sanity"
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
273
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
274 let output code =
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
275 try check_and_output code with Exit -> exit 1
Mike Spivey <mike@cs.ox.ac.uk>
parents:
diff changeset
276