comparison ppc/check.ml @ 0:bfdcc3820b32

Basis
author Mike Spivey <mike@cs.ox.ac.uk>
date Thu, 05 Oct 2017 08:04:15 +0100
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 0:bfdcc3820b32
1 (* ppc/check.ml *)
2 (* Copyright (c) 2017 J. M. Spivey *)
3
4 open Keiko
5 open Tree
6 open Dict
7 open Print
8 open Lexer
9 open Mach
10
11 (* EXPRESSIONS *)
12
13 (* Two global variables to save passing parameters everywhere *)
14 let level = ref 0
15 let return_type = ref voidtype
16
17 let err_line = ref 1
18
19 exception Sem_error of string * Print.arg list * int
20
21 let sem_error fmt args =
22 raise (Sem_error (fmt, args, !err_line))
23
24 let expr_fail () = sem_error "type error in expression" []
25
26 (* |lookup_def| -- find definition of a name, give error if none *)
27 let lookup_def x env =
28 err_line := x.x_line;
29 try
30 let d = lookup x.x_name env in
31 x.x_def <- Some d; d
32 with Not_found ->
33 sem_error "$ is not declared" [fId x.x_name]
34
35 (* |add_def| -- add definition to envmt, give error if already declared *)
36 let add_def d env =
37 try define d env with
38 Exit -> sem_error "$ is already declared" [fId d.d_tag]
39
40 (* |check_monop| -- check application of unary operator *)
41 let check_monop w t =
42 match w with
43 Uminus ->
44 if not (same_type t integer) then expr_fail ();
45 integer
46 | Not ->
47 if not (same_type t boolean) then expr_fail ();
48 boolean
49 | _ -> failwith "bad monop"
50
51 (* |check_binop| -- check application of binary operator *)
52 let check_binop w t1 t2 =
53 match w with
54 Plus | Minus | Times | Div | Mod ->
55 if not (same_type t1 integer && same_type t2 integer) then
56 expr_fail ();
57 integer
58 | Eq | Lt | Gt | Leq | Geq | Neq ->
59 if not (scalar t1) || not (same_type t1 t2) then expr_fail ();
60 boolean
61 | And | Or ->
62 if not (same_type t1 boolean && same_type t2 boolean) then
63 expr_fail ();
64 boolean
65 | _ -> failwith "bad binop"
66
67 (* |try_monop| -- propagate constant through unary operation *)
68 let try_monop w =
69 function
70 Some x -> Some (do_monop w x)
71 | None -> None
72
73 (* |try_binop| -- propagate constant through unary operation *)
74 let try_binop w v1 v2 =
75 match (v1, v2) with
76 (Some x1, Some x2) -> Some (do_binop w x1 x2)
77 | _ -> None
78
79 (* |has_value| -- check if object is suitable for use in expressions *)
80 let has_value d =
81 match d.d_kind with
82 ConstDef _ | VarDef | CParamDef | VParamDef | StringDef -> true
83 | _ -> false
84
85 (* |check_var| -- check that expression denotes a variable *)
86 let rec check_var e =
87 match e.e_guts with
88 Variable x ->
89 let d = get_def x in
90 begin
91 match d.d_kind with
92 VarDef | VParamDef | CParamDef -> ()
93 | _ ->
94 sem_error "$ is not a variable" [fId x.x_name]
95 end
96 | Sub (a, i) -> check_var a
97 | Select (r, x) -> check_var r
98 | Deref p -> ()
99 | _ -> sem_error "a variable is needed here" []
100
101 (* |check_expr| -- check and annotate an expression, return its type *)
102 let rec check_expr e env =
103 let t = expr_type e env in
104 e.e_type <- t; t
105
106 (* |expr_type| -- return type of expression *)
107 and expr_type e env =
108 match e.e_guts with
109 Variable x ->
110 let d = lookup_def x env in
111 if not (has_value d) then
112 sem_error "$ is not a variable" [fId x.x_name];
113 begin
114 match d.d_kind with
115 ConstDef v ->
116 e.e_value <- Some v
117 | _ -> ()
118 end;
119 d.d_type
120 | Sub (e1, e2) ->
121 let t1 = check_expr e1 env
122 and t2 = check_expr e2 env in
123 if not (same_type t2 integer) then
124 sem_error "subscript is not an integer" [];
125 begin
126 match t1.t_guts with
127 ArrayType (upb, u1) -> u1
128 | _ -> sem_error "subscripting a non-array" []
129 end
130 | Select (e1, x) ->
131 let t1 = check_expr e1 env in
132 err_line := x.x_line;
133 begin
134 match t1.t_guts with
135 RecordType fields ->
136 let d = try find_def x.x_name fields
137 with Not_found ->
138 sem_error "selecting non-existent field" [] in
139 x.x_def <- Some d; d.d_type
140 | _ -> sem_error "selecting from a non-record" []
141 end
142 | Deref e1 ->
143 let t1 = check_expr e1 env in
144 begin
145 match t1.t_guts with
146 PointerType u -> !u
147 | _ -> sem_error "dereferencing a non-pointer" []
148 end
149 | Constant (n, t) -> e.e_value <- Some n; t
150 | String (lab, n) -> row n character
151 | Nil -> e.e_value <- Some 0; addrtype
152 | FuncCall (p, args) ->
153 let v = ref None in
154 let t1 = check_funcall p args env v in
155 if same_type t1 voidtype then
156 sem_error "$ does not return a result" [fId p.x_name];
157 e.e_value <- !v; t1
158 | Monop (w, e1) ->
159 let t = check_monop w (check_expr e1 env) in
160 e.e_value <- try_monop w e1.e_value;
161 t
162 | Binop (w, e1, e2) ->
163 let t = check_binop w (check_expr e1 env) (check_expr e2 env) in
164 e.e_value <- try_binop w e1.e_value e2.e_value;
165 t
166
167 (* |check_funcall| -- check a function or procedure call *)
168 and check_funcall f args env v =
169 let d = lookup_def f env in
170 match d.d_kind with
171 LibDef q ->
172 check_libcall q args env v; d.d_type
173 | ProcDef | PParamDef ->
174 let p = get_proc d.d_type in
175 check_args p.p_fparams args env;
176 p.p_result
177 | _ -> sem_error "$ is not a procedure" [fId f.x_name]
178
179 (* |check_args| -- match formal and actual parameters *)
180 and check_args formals args env =
181 try List.iter2 (fun f a -> check_arg f a env) formals args with
182 Invalid_argument _ ->
183 sem_error "wrong number of arguments" []
184
185 (* |check_arg| -- check one (formal, actual) parameter pair *)
186 and check_arg formal arg env =
187 match formal.d_kind with
188 CParamDef | VParamDef ->
189 let t1 = check_expr arg env in
190 if not (same_type formal.d_type t1) then
191 sem_error "argument has wrong type" [];
192 if formal.d_kind = VParamDef then
193 check_var arg
194 | PParamDef ->
195 let pf = get_proc formal.d_type in
196 let x = (match arg.e_guts with Variable x -> x
197 | _ -> sem_error "procedure argument must be a proc name" []) in
198 let actual = lookup_def x env in
199 begin
200 match actual.d_kind with
201 ProcDef | PParamDef ->
202 let pa = get_proc actual.d_type in
203 if not (match_args pf.p_fparams pa.p_fparams) then
204 sem_error "argument lists don't match" [];
205 if not (same_type pf.p_result pa.p_result) then
206 sem_error "result types don't match" []
207 | _ ->
208 sem_error "argument $ is not a procedure" [fId x.x_name]
209 end
210 | _ -> failwith "bad formal"
211
212 (* |check_libcall| -- check call to a library procedure *)
213 and check_libcall q args env v =
214 (* |q.q_nargs = -1| if the lib proc has a variable number of arguments;
215 otherwise it is the number of arguments. |q.q_argtypes = []| if the
216 argument types can vary; otherwise it is a list of arg types. *)
217 if q.q_nargs >= 0 && List.length args <> q.q_nargs then
218 sem_error "wrong number of arguments for $" [fLibId q.q_id];
219 if q.q_argtypes <> [] then begin
220 let check t e =
221 if not (same_type t (check_expr e env)) then
222 sem_error "argument of $ has wrong type" [fLibId q.q_id] in
223 List.iter2 check q.q_argtypes args
224 end;
225 match q.q_id with
226 ChrFun ->
227 let e1 = List.hd args in
228 v := e1.e_value
229 | OrdFun ->
230 let e1 = List.hd args in
231 let t1 = check_expr e1 env in
232 if not (discrete t1) then
233 sem_error "ord expects an argument of a discrete type" [];
234 v := e1.e_value
235 | PrintString ->
236 let t1 = check_expr (List.hd args) env in
237 if not (is_string t1) then
238 sem_error "print_string expects a string" []
239 | ReadChar ->
240 check_var (List.hd args)
241 | NewProc ->
242 let t1 = check_expr (List.hd args) env in
243 if not (is_pointer t1) then
244 sem_error "parameter of new must be a pointer" [];
245 check_var (List.hd args)
246 | ArgvProc ->
247 let t1 = check_expr (List.nth args 0) env
248 and t2 = check_expr (List.nth args 1) env in
249 if not (same_type t1 integer) || not (is_string t2) then
250 sem_error "type error in parameters of argv" [];
251 check_var (List.nth args 1)
252 | OpenIn ->
253 let t1 = check_expr (List.nth args 0) env in
254 if not (is_string t1) then
255 sem_error "parameter of open_in is not a string" []
256 | _ -> ()
257
258 (* |check_const| -- check an expression with constant value *)
259 let check_const e env =
260 let t = check_expr e env in
261 match e.e_value with
262 Some v -> (t, v)
263 | None -> sem_error "constant expected" []
264
265
266 (* STATEMENTS *)
267
268 (* check_dupcases -- check for duplicate case labels *)
269 let check_dupcases vs =
270 let rec chk =
271 function
272 [] | [_] -> ()
273 | x :: (y :: ys as rest) ->
274 if x = y then sem_error "duplicate case label" [];
275 chk rest in
276 chk (List.sort compare vs)
277
278 (* |check_stmt| -- check and annotate a statement *)
279 let rec check_stmt s env =
280 err_line := s.s_line;
281 match s.s_guts with
282 Skip -> ()
283 | Seq ss ->
284 List.iter (fun s1 -> check_stmt s1 env) ss
285 | Assign (lhs, rhs) ->
286 let lt = check_expr lhs env
287 and rt = check_expr rhs env in
288 check_var lhs;
289 if not (same_type lt rt) then
290 sem_error "type mismatch in assignment" []
291 | ProcCall (p, args) ->
292 let rt = check_funcall p args env (ref None) in
293 if rt <> voidtype then
294 sem_error "$ returns a result" [fId p.x_name]
295 | Return res ->
296 if !level = 0 then
297 sem_error "return statement not allowed in main program" [];
298 begin
299 match res with
300 Some e ->
301 if same_type !return_type voidtype then
302 sem_error "procedure must not return a result" [];
303 let t = check_expr e env in
304 if not (same_type t !return_type) then
305 sem_error "type mismatch in return statement" []
306 | None ->
307 if not (same_type !return_type voidtype) then
308 sem_error "function must return a result" []
309 end
310 | IfStmt (cond, thenpt, elsept) ->
311 let ct = check_expr cond env in
312 if not (same_type ct boolean) then
313 sem_error "test in if statement must be a boolean" [];
314 check_stmt thenpt env;
315 check_stmt elsept env
316 | WhileStmt (cond, body) ->
317 let ct = check_expr cond env in
318 if not (same_type ct boolean) then
319 sem_error "type mismatch in while statement" [];
320 check_stmt body env
321 | RepeatStmt (body, test) ->
322 check_stmt body env;
323 let ct = check_expr test env in
324 if not (same_type ct boolean) then
325 sem_error "type mismatch in repeat statement" []
326 | ForStmt (var, lo, hi, body) ->
327 let vt = check_expr var env in
328 let lot = check_expr lo env in
329 let hit = check_expr hi env in
330 if not (same_type vt integer) || not (same_type lot integer)
331 || not (same_type hit integer) then
332 sem_error "type mismatch in for statement" [];
333 check_var var;
334 check_stmt body env
335 | CaseStmt (sel, arms, deflt) ->
336 let st = check_expr sel env in
337 if not (scalar st) then
338 sem_error "expression in case statement must be scalar" [];
339
340 let check_arm (lab, body) =
341 let (t1, v) = check_const lab env in
342 if not (same_type t1 st) then
343 sem_error "case label has wrong type" [];
344 check_stmt body env; v in
345
346 let vs = List.map check_arm arms in
347 check_dupcases vs;
348 check_stmt deflt env
349
350
351 (* TYPES AND DECLARATIONS *)
352
353 let make_def x k t =
354 { d_tag = x; d_kind = k; d_type = t; d_level = !level; d_addr = Nowhere }
355
356 (* |lookup_typename| -- find a named type in the environment *)
357 let lookup_typename x env =
358 let d = lookup_def x env in
359 match d.d_kind with
360 (TypeDef | HoleDef _) -> d
361 | _ -> sem_error "$ is not a type" [fId x.x_name]
362
363 (* |align| -- increase offset to next multiple of alignment *)
364 let align alignment offset =
365 let margin = !offset mod alignment in
366 if margin <> 0 then offset := !offset - margin + alignment
367
368 (* upward_alloc -- allocate objects upward in memory *)
369 let upward_alloc size d =
370 let r = d.d_type.t_rep in
371 align r.r_align size;
372 let addr = !size in
373 size := !size + r.r_size;
374 d.d_addr <- Local addr
375
376 (* local_alloc -- allocate locals downward in memory *)
377 let local_alloc size d =
378 let r = d.d_type.t_rep in
379 align r.r_align size;
380 size := !size + r.r_size;
381 d.d_addr <- Local (local_base - !size)
382
383 (* param_alloc -- allocate space for formal parameter *)
384 let param_alloc pcount d =
385 let s = param_rep.r_size in
386 match d.d_kind with
387 CParamDef | VParamDef ->
388 d.d_addr <- Local (param_base + s * !pcount);
389 incr pcount
390 | PParamDef ->
391 d.d_addr <- Local (param_base + s * !pcount);
392 pcount := !pcount + 2
393 | _ -> failwith "param_alloc"
394
395 (* |global_alloc| -- allocate label for global variable *)
396 let global_alloc d =
397 d.d_addr <- Global (sprintf "_$" [fId d.d_tag])
398
399 (* |check_typexpr| -- check a type expression, returning the ptype *)
400 let rec check_typexpr env =
401 function
402 TypeName x ->
403 let d = lookup_typename x env in
404 if d.d_kind = TypeDef then d.d_type
405 else sem_error "$ is used before its definition" [fId x.x_name]
406 | Array (upb, value) ->
407 let (t1, v1) = check_const upb env
408 and t2 = check_typexpr env value in
409 if not (same_type t1 integer) then
410 sem_error "upper bound must be an integer" [];
411 row v1 t2
412 | Record fields ->
413 let size = ref 0 in
414 let env' =
415 check_decls fields (upward_alloc size) (new_block env) in
416 let defs = top_block env' in
417 let r = { r_size = !size; r_align = max_align } in
418 mk_type (RecordType defs) r
419 | Pointer te ->
420 let t =
421 match te with
422 TypeName x ->
423 let d = lookup_typename x env in
424 begin
425 match d.d_kind with
426 TypeDef -> ref d.d_type
427 | HoleDef h -> h
428 | _ -> failwith "pointer"
429 end
430 | _ -> ref (check_typexpr env te) in
431 mk_type (PointerType t) addr_rep
432
433 (* |check_decl| -- check a declaration and add it to the environment *)
434 and check_decl d alloc env =
435 (* All types of declaration are mixed together in the AST *)
436 match d with
437 ConstDecl (x, e) ->
438 begin
439 match e.e_guts with
440 String (lab, n) ->
441 let t = row n character in
442 let d = make_def x StringDef t in
443 d.d_addr <- Global lab;
444 add_def d env
445 | _ ->
446 let (t, v) = check_const e env in
447 add_def (make_def x (ConstDef v) t) env
448 end
449 | VarDecl (kind, xs, te) ->
450 let t = check_typexpr env te in
451 let def x env =
452 let d = make_def x kind t in
453 alloc d; add_def d env in
454 Util.accum def xs env
455 | TypeDecl tds ->
456 let tds' =
457 List.map (function (x, te) -> (x, te, ref voidtype)) tds in
458 let add_hole (x, te, h) e =
459 add_def (make_def x (HoleDef h) voidtype) e in
460 let env1 = Util.accum add_hole tds' env in
461 let redefine (x, te, h) e =
462 let t = check_typexpr e te in
463 h := t; replace (make_def x TypeDef t) e in
464 Util.accum redefine tds' env1
465 | ProcDecl (Heading (x, _, _) as heading, body) ->
466 let t = check_heading heading env in
467 let d = make_def x.x_name ProcDef t in
468 d.d_addr <- Global (sprintf "_$" [fId d.d_tag]);
469 x.x_def <- Some d; add_def d env
470 | PParamDecl (Heading (x, _, _) as heading) ->
471 let t = check_heading heading env in
472 let d = make_def x.x_name PParamDef t in
473 alloc d; add_def d env
474
475 (* |check_heading| -- process a procedure heading into a procedure type *)
476 and check_heading (Heading (x, fparams, result)) env =
477 err_line := x.x_line;
478 incr level;
479 let pcount = ref 0 in
480 let env' = check_decls fparams (param_alloc pcount) (new_block env) in
481 let defs = top_block env' in
482 decr level;
483 let rt = (match result with
484 Some t -> check_typexpr env t | None -> voidtype) in
485 if not (same_type rt voidtype) && not (scalar rt) then
486 sem_error "return type must be scalar" [];
487 let pt = { p_fparams = defs; p_pcount = !pcount; p_result = rt } in
488 mk_type (ProcType pt) proc_rep
489
490 (* |check_decls| -- check a sequence of declarations *)
491 and check_decls ds alloc env =
492 Util.accum (fun d -> check_decl d alloc) ds env
493
494 (* |check_block| -- check a local block *)
495 let rec check_block rt env (Block (ds, ss, fsize, nregv)) =
496 let env' =
497 check_decls ds (local_alloc fsize) (new_block env) in
498 check_bodies env' ds;
499 return_type := rt;
500 check_stmt ss env';
501 align max_align fsize
502
503 (* |check_bodies| -- check bodies of procedure declarations *)
504 and check_bodies env ds =
505 let check =
506 function
507 ProcDecl (Heading(x, _, _), body) ->
508 let d = get_def x in
509 let p = get_proc d.d_type in
510 let env' = add_block p.p_fparams env in
511 incr level;
512 check_block p.p_result env' body;
513 decr level
514 | _ -> () in
515 List.iter check ds
516
517
518 (* INITIAL ENVIRONMENT *)
519
520 let defn (x, k, t) env =
521 let d = { d_tag = intern x; d_kind = k; d_type = t;
522 d_level = 0; d_addr = Nowhere } in
523 define d env
524
525 let libproc i n ts =
526 LibDef { q_id = i; q_nargs = n; q_argtypes = ts }
527
528 let operator op ts =
529 libproc (Operator op) (List.length ts) ts
530
531 let init_env =
532 Util.accum defn
533 [ ("integer", TypeDef, integer);
534 ("char", TypeDef, character);
535 ("boolean", TypeDef, boolean);
536 ("true", ConstDef 1, boolean);
537 ("false", ConstDef 0, boolean);
538 ("chr", libproc ChrFun 1 [integer], character);
539 ("ord", libproc OrdFun 1 [], integer);
540 ("print_num", libproc PrintNum 1 [integer], voidtype);
541 ("print_char", libproc PrintChar 1 [character], voidtype);
542 ("print_string", libproc PrintString 1 [], voidtype);
543 ("open_in", libproc OpenIn 1 [], boolean);
544 ("close_in", libproc CloseIn 0 [], voidtype);
545 ("newline", libproc NewLine 0 [], voidtype);
546 ("read_char", libproc ReadChar 1 [character], voidtype);
547 ("exit", libproc ExitProc 1 [integer], voidtype);
548 ("new", libproc NewProc 1 [], voidtype);
549 ("argc", libproc ArgcFun 0 [], integer);
550 ("argv", libproc ArgvProc 2 [], voidtype);
551 ("lsl", operator Lsl [integer; integer], integer);
552 ("lsr", operator Lsr [integer; integer], integer);
553 ("asr", operator Asr [integer; integer], integer);
554 ("bitand", operator BitAnd [integer; integer], integer);
555 ("bitor", operator BitOr [integer; integer], integer);
556 ("bitnot", operator BitNot [integer], integer)] empty
557
558 (* |annotate| -- annotate the whole program *)
559 let annotate (Prog (Block (globals, ss, _, _), glodefs)) =
560 level := 0;
561 let env = check_decls globals global_alloc (new_block init_env) in
562 check_bodies env globals;
563 return_type := voidtype;
564 check_stmt ss env;
565 glodefs := top_block env