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