Home My Page Projects Code Snippets Project Openings diderot
Summary Activity Tracker Tasks SCM

SCM Repository

[diderot] Annotation of /branches/vis15/src/compiler/cfg-ir/check-ir-fn.sml
ViewVC logotype

Annotation of /branches/vis15/src/compiler/cfg-ir/check-ir-fn.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3937 - (view) (download)

1 : jhr 3475 (* check-ir-fn.sml
2 : jhr 3470 *
3 :     * This code is part of the Diderot Project (http://diderot-language.cs.uchicago.edu)
4 :     *
5 :     * COPYRIGHT (c) 2015 The University of Chicago
6 :     * All rights reserved.
7 :     *
8 : jhr 3475 * Correctness checker for SSA-based IRs.
9 : jhr 3470 *
10 :     * TODO:
11 :     * check that the state variables and method stateOut variables are all defined.
12 :     *)
13 :    
14 :     signature OPERATOR_TY =
15 :     sig
16 :     type rator
17 :     type ty
18 :    
19 :     (* returns the signature of an operator as (rng, dom). *)
20 :     val sigOf : rator -> ty * ty list
21 :    
22 :     (* return the type of a CONS, where the first argument is the annotated type
23 :     * and the second argument is the list of argument types. Returns false if
24 :     * there is a type error.
25 :     *)
26 :     val typeOfCons : ty * ty list -> bool
27 :    
28 : jhr 3937 (* return true if the type is of the specified form *)
29 :     val isBoolTy : ty -> bool
30 :     val isStrandTy : ty -> bool
31 :    
32 : jhr 3470 end
33 :    
34 : jhr 3475 functor CheckIRFn (
35 : jhr 3470
36 : jhr 3475 structure IR : SSA
37 : jhr 3470 structure OpTy : OPERATOR_TY
38 : jhr 3475 where type rator = IR.Op.rator
39 :     where type ty = IR.Ty.ty
40 : jhr 3470
41 :     ) : sig
42 :    
43 :     (* check the program for type errors, etc. The first argument will be used to
44 :     * identify the phase that the check follows and the return result will be true
45 :     * if any errors were detected.
46 :     *)
47 : jhr 3475 val check : string * IR.program -> bool
48 : jhr 3470
49 :     end = struct
50 :    
51 : jhr 3475 structure IR = IR
52 :     structure Ty = IR.Ty
53 :     structure V = IR.Var
54 : jhr 3470 structure VSet = V.Set
55 :    
56 :     (* forward analysis to determine the variables that are available in blocks *)
57 :     structure Avail = ForwardDFAFn (
58 :     struct
59 :    
60 : jhr 3475 structure IR = IR
61 : jhr 3470 type t = VSet.set
62 :    
63 :     val bottom = VSet.empty
64 :    
65 :     fun join inputs = List.foldl VSet.union bottom inputs
66 :    
67 : jhr 3475 fun transfer (input, nd as IR.ND{kind, ...}) = (case kind
68 :     of IR.JOIN{phis, ...} => let
69 : jhr 3470 (* add the lhs of the phi node. We do not remove the rhs variables, since
70 :     * after value numbering, they may have further uses.
71 :     *)
72 :     fun doPhi ((y, _), vs) = VSet.add(vs, y)
73 :     val output = List.foldl doPhi input (!phis)
74 :     in
75 :     output
76 :     end
77 : jhr 3526 | IR.FOREACH{var, phis, ...} => let
78 :     (* add the lhs of the phi node. We do not remove the rhs variables, since
79 :     * after value numbering, they may have further uses.
80 :     *)
81 :     fun doPhi ((y, _), vs) = VSet.add(vs, y)
82 :     val output = List.foldl doPhi input (!phis)
83 :     in
84 :     VSet.add (output, var)
85 :     end
86 : jhr 3475 | IR.ASSIGN{stm=(y, _), ...} => VSet.add(input, y)
87 :     | IR.MASSIGN{stm=(ys, _, _), ...} => VSet.addList(input, ys)
88 : jhr 3470 | _ => input
89 :     (* end case *))
90 :    
91 :     val same = VSet.equal
92 :    
93 :     fun toString vs = let
94 : jhr 3475 fun f (v, []) = [IR.Var.toString v, "}"]
95 :     | f (v, l) = IR.Var.toString v :: "," :: l
96 : jhr 3470 in
97 :     if VSet.isEmpty vs then "{}" else String.concat("{" :: VSet.foldl f [] vs)
98 :     end
99 :    
100 :     end)
101 :    
102 :     datatype token
103 : jhr 3475 = NL | S of string | A of Atom.atom | V of IR.var | VTYS of IR.var list
104 : jhr 3470 | TY of Ty.ty | TYS of Ty.ty list
105 : jhr 3475 | ND of IR.node
106 : jhr 3470
107 :     fun error errBuf toks = let
108 :     fun tok2str NL = "\n ** "
109 :     | tok2str (S s) = s
110 :     | tok2str (A s) = Atom.toString s
111 :     | tok2str (V x) = V.toString x
112 :     | tok2str (VTYS xs) = tok2str(TYS(List.map V.ty xs))
113 :     | tok2str (TY ty) = Ty.toString ty
114 :     | tok2str (TYS []) = "()"
115 :     | tok2str (TYS[ty]) = Ty.toString ty
116 :     | tok2str (TYS tys) = String.concat[
117 :     "(", String.concatWith " * " (List.map Ty.toString tys), ")"
118 :     ]
119 : jhr 3475 | tok2str (ND nd) = IR.Node.toString nd
120 : jhr 3470 in
121 :     errBuf := concat ("**** Error: " :: List.map tok2str toks)
122 :     :: !errBuf
123 :     end
124 :    
125 :     fun checkAssign errFn ((y, rhs), bvs) = let
126 :     (* check a variable use *)
127 :     fun checkVar x = if VSet.member(bvs, x)
128 :     then ()
129 :     else errFn [
130 :     S "variable ", V x, S " is not bound in", NL,
131 : jhr 3475 S(IR.assignToString(y, rhs))
132 : jhr 3470 ]
133 :     fun tyError (ty1, ty2) = errFn [
134 : jhr 3475 S "type mismatch in \"", S(IR.assignToString (y, rhs)), S "\"",
135 : jhr 3470 NL, S "lhs: ", TY ty1, NL, S "rhs: ", TY ty2
136 :     ]
137 :     fun checkTys (ty1, ty2) = if Ty.same(ty1, ty2)
138 :     then ()
139 :     else tyError (ty1, ty2)
140 :     in
141 :     (* check that y is not bound twice *)
142 : jhr 3526 (* FIXME: with loops, this check no longer works (false positives)
143 : jhr 3470 if VSet.member(bvs, y)
144 :     then errFn [
145 :     S "variable ", V y, S " is bound twice in", NL,
146 : jhr 3475 S(IR.assignToString (y, rhs))
147 : jhr 3470 ]
148 :     else ();
149 : jhr 3526 *)
150 : jhr 3470 case rhs
151 : jhr 3475 of IR.GLOBAL x => checkTys(V.ty y, IR.GlobalVar.ty x)
152 : jhr 3846 | IR.STATE(NONE, sv) => checkTys(V.ty y, IR.StateVar.ty sv)
153 :     | IR.STATE(SOME x, sv) => (
154 : jhr 3937 if not(OpTy.isStrandTy(V.ty x))
155 :     then errFn [
156 :     S "expected strand type for ", V x, S ", but found ", TY(V.ty x)
157 :     ]
158 :     else ();
159 : jhr 3846 checkVar x; checkTys(V.ty y, IR.StateVar.ty sv))
160 : jhr 3475 | IR.VAR x => (
161 : jhr 3470 checkVar x;
162 :     checkTys (V.ty y, V.ty x))
163 : jhr 3475 | IR.LIT lit => let
164 : jhr 3470 val ty = (case lit
165 :     of Literal.Int _ => Ty.intTy
166 :     | Literal.Real _ => Ty.realTy
167 :     | Literal.String _ => Ty.StringTy
168 :     | Literal.Bool _ => Ty.BoolTy
169 :     (* end case *))
170 :     in
171 :     checkTys (V.ty y, ty)
172 :     end
173 : jhr 3475 | IR.OP(rator, xs) => let
174 : jhr 3470 val (resTy, argTys) = OpTy.sigOf rator
175 :     in
176 :     List.app checkVar xs;
177 :     checkTys (V.ty y, resTy);
178 :     if ListPair.allEq (fn (x, ty) => Ty.same(V.ty x, ty)) (xs, argTys)
179 :     then ()
180 :     else errFn [
181 : jhr 3475 S "argument type mismatch in \"", S(IR.assignToString (y, rhs)), S "\"",
182 : jhr 3470 NL, S "expected: ", TYS argTys,
183 :     NL, S "found: ", VTYS xs
184 :     ]
185 :     end
186 : jhr 3475 | IR.CONS(xs, ty) => (
187 : jhr 3470 List.app checkVar xs;
188 :     if OpTy.typeOfCons (ty, List.map V.ty xs)
189 :     then checkTys (V.ty y, ty)
190 : jhr 3475 else errFn [S "invalid ", S(IR.assignToString(y, rhs))])
191 :     | IR.SEQ(xs, ty) => (
192 : jhr 3470 List.app checkVar xs;
193 :     (* FIXME: check types of sequence elements *)())
194 : jhr 3475 | IR.EINAPP(ein, xs) => (
195 : jhr 3470 List.app checkVar xs;
196 :     (* FIXME: check ein *)())
197 :     (* end case *);
198 :     VSet.add(bvs, y)
199 :     end
200 :    
201 :     fun checkMAssign errFn (stm as (ys, rator, xs), bvs) = let
202 :     (* check that a lhs variable is not bound twice *)
203 :     fun checkBind y = if VSet.member(bvs, y)
204 :     then errFn [
205 :     S "variable ", V y, S " is bound twice in", NL,
206 : jhr 3475 S(IR.massignToString stm)
207 : jhr 3470 ]
208 :     else ()
209 :     (* check a variable use *)
210 :     fun checkVar x = if VSet.member(bvs, x)
211 :     then ()
212 :     else errFn [
213 :     S "variable ", V x, S " is not bound in", NL,
214 : jhr 3475 S(IR.massignToString stm)
215 : jhr 3470 ]
216 :     fun tyError (ty1, ty2) = errFn [
217 : jhr 3475 S "type mismatch in \"", S(IR.massignToString stm), S "\"",
218 : jhr 3470 NL, S "lhs: ", TY ty1, NL, S "rhs: ", TY ty2
219 :     ]
220 :     in
221 :     (* check that the lhs variables are not bound twice *)
222 :     List.app checkBind ys;
223 :     (* FIXME:
224 :     (* check the types *)
225 :     val (resTys, argTys) = OpTy.sigOf rator
226 :     in
227 :     List.app checkVar xs;
228 :     if ListPair.allEq (fn (y, ty) => Ty.same(V.ty y, ty)) (ys, resTys)
229 :     then ()
230 :     else tyError (V.ty y, resTy);
231 :     if ListPair.allEq (fn (x, ty) => Ty.same(V.ty x, ty)) (xs, argTys)
232 :     then ()
233 :     else errFn [
234 : jhr 3475 S "argument type mismatch in \"", S(IR.massignToString stm), S "\"",
235 : jhr 3470 NL, S "expected: ", TYS argTys,
236 :     NL, S "found: ", VTYS xs
237 :     ]
238 :     end
239 :     *)
240 :     VSet.addList(bvs, ys)
241 :     end
242 :    
243 :     fun checkPhi errFn (nd, bvs, mask) (y, xs) = let
244 :     val ty = V.ty y
245 :     fun chkTy x = if Ty.same(V.ty x, ty)
246 :     then ()
247 :     else errFn [
248 : jhr 3475 S "type mismatch in \"", S(IR.phiToString (y, xs)), S "\"", NL,
249 : jhr 3470 S "typeof(", V y, S "): ", TY ty, NL,
250 :     S "typeof(", V x, S "): ", TY(V.ty x)
251 :     ]
252 :     fun chkRHS ([], []) = ()
253 :     | chkRHS (true::ms, NONE::xs) = chkRHS (ms, xs)
254 :     | chkRHS (false::ms, (SOME x)::xs) = (chkTy x; chkRHS (ms, xs))
255 :     | chkRHS _ = errFn [S "phi/mask mismatch in ", ND nd]
256 :     in
257 :     (* check that y is not bound twice *)
258 :     if VSet.member(bvs, y)
259 :     then errFn [
260 :     S "variable ", V y, S " is bound twice in", NL,
261 : jhr 3475 S(IR.phiToString (y, xs))
262 : jhr 3470 ]
263 :     else ();
264 :     (* check that rhs vars have the correct type *)
265 :     chkRHS (mask, xs)
266 :     end
267 :    
268 : jhr 3485 fun check (phase, prog) = let
269 :     val IR.Program{
270 :     props, consts, inputs, globals,
271 :     constInit, globalInit, strand, create, update
272 :     } = prog
273 : jhr 3470 val errBuf = ref []
274 :     val errFn = error errBuf
275 :     fun final () = (case !errBuf
276 :     of [] => false
277 :     | errs => (
278 : jhr 3676 Log.msg ["********** IR Errors detected after ", phase, " **********\n"];
279 :     List.app (fn msg => Log.msg [msg, "\n"]) (List.rev errs);
280 : jhr 3470 true)
281 :     (* end case *))
282 :     val checkPhi = checkPhi errFn
283 :     val checkAssign = checkAssign errFn
284 :     val checkMAssign = checkMAssign errFn
285 :     fun checkCFG (vs, cfg) = let
286 :     val bvs = VSet.fromList vs
287 :     (* compute the variables available on entry to each block *)
288 :     val nodes = Avail.analyse (bvs, cfg)
289 :     (* check the edges of a node. For each predecessor, the node should appear in the
290 :     * successor list and for each successor, the node should appear in the predecessor
291 :     * list.
292 :     *)
293 :     fun checkEdges nd = let
294 : jhr 3475 fun eqNd nd' = IR.Node.same(nd, nd')
295 :     fun chkPred src = if List.exists eqNd (IR.Node.succs src)
296 : jhr 3470 then ()
297 :     else errFn [
298 :     S "predecessor edge from ", ND nd, S " -> ", ND src,
299 :     S " not matched by successor edge"
300 :     ]
301 : jhr 3475 fun chkSucc dst = if List.exists eqNd (IR.Node.preds dst)
302 : jhr 3470 then ()
303 :     else errFn [
304 :     S "successor edge from ", ND nd, S " -> ", ND dst,
305 :     S " not matched by predecessor edge"
306 :     ]
307 :     in
308 : jhr 3475 List.app chkPred (IR.Node.preds nd);
309 :     List.app chkSucc (IR.Node.succs nd)
310 : jhr 3470 end
311 : jhr 3475 fun checkNd (nd as IR.ND{kind, ...}) = (case kind
312 :     of IR.NULL => errFn [S "unexpected ", ND nd]
313 :     | IR.JOIN{mask, phis, ...} =>
314 : jhr 3470 List.app
315 :     (checkPhi (nd, VSet.union(Avail.inValue nd, bvs), !mask))
316 :     (!phis)
317 : jhr 3937 | IR.COND{cond, ...} => (
318 :     if not(OpTy.isBoolTy(V.ty(!cond)))
319 :     then errFn [
320 :     S "expected bool type for ", V(!cond), S ", but found ",
321 :     TY(V.ty(!cond))
322 :     ]
323 :     else ();
324 : jhr 3536 if VSet.member(Avail.inValue nd, !cond)
325 :     orelse VSet.member(bvs, !cond)
326 : jhr 3470 then ()
327 : jhr 3937 else errFn [S "unbound variable ", V(!cond), S " in conditional"])
328 : jhr 3754 | IR.FOREACH{phis, mask, var, src, bodyExit, ...} => (
329 : jhr 3536 if VSet.member(Avail.inValue nd, !src)
330 :     orelse VSet.member(bvs, !src)
331 : jhr 3473 then ()
332 : jhr 3536 else errFn [S "unbound variable ", V(!src), S " in foreach"];
333 : jhr 3473 List.app
334 :     (checkPhi (nd, VSet.union(Avail.inValue nd, bvs), !mask))
335 : jhr 3754 (!phis);
336 :     case IR.Node.kind(!bodyExit)
337 :     of IR.NEXT{succ, ...} =>
338 :     if IR.Node.same(nd, !succ)
339 :     then ()
340 :     else errFn [
341 :     S "loop's body exit node ", ND(!bodyExit),
342 :     S " does not point back to loop header"
343 :     ]
344 :     | _ => errFn [
345 :     S "bad bodyExit ", ND(!bodyExit), S " for loop ", ND nd
346 :     ]
347 :     (* end case *))
348 :     | IR.NEXT{succ, ...} => (case IR.Node.kind(!succ)
349 :     of IR.FOREACH{bodyExit, ...} =>
350 :     if IR.Node.same(nd, !bodyExit)
351 :     then ()
352 :     else errFn [
353 :     S "next node ", ND nd, S " and loop ", ND(!succ),
354 :     S " do not agree"
355 :     ]
356 :     | _ => errFn [
357 :     S "bad successor ", ND(!succ), S " for loop exit ", ND nd
358 :     ]
359 :     (* end case *))
360 : jhr 3475 | IR.ASSIGN{stm, ...} =>
361 : jhr 3470 ignore (checkAssign (stm, VSet.union(Avail.inValue nd, bvs)))
362 : jhr 3475 | IR.MASSIGN{stm, ...} =>
363 : jhr 3470 ignore (checkMAssign (stm, VSet.union(Avail.inValue nd, bvs)))
364 : jhr 3475 | IR.GASSIGN{lhs, rhs, ...} => let
365 : jhr 3470 val bvs = VSet.union(Avail.inValue nd, bvs)
366 :     in
367 :     if VSet.member(bvs, rhs)
368 :     then ()
369 :     else errFn [
370 :     S "variable ", V rhs, S " is not bound in global assignment ",
371 : jhr 3475 S(IR.GlobalVar.toString lhs)
372 : jhr 3470 ];
373 : jhr 3475 if Ty.same(IR.GlobalVar.ty lhs, V.ty rhs)
374 : jhr 3470 then ()
375 :     else errFn [
376 : jhr 3475 S "type mismatch in \"", S(IR.GlobalVar.toString lhs),
377 : jhr 3470 S " = ", S(V.toString rhs), S "\"",
378 : jhr 3475 NL, S "lhs: ", TY(IR.GlobalVar.ty lhs),
379 : jhr 3470 NL, S "rhs: ", TY(V.ty rhs)
380 :     ]
381 :     end
382 : jhr 3475 | IR.NEW{strand, args, ...} => let
383 : jhr 3470 val bvs = VSet.union(Avail.inValue nd, bvs)
384 :     (* check a variable use *)
385 :     fun checkVar x = if VSet.member(bvs, x)
386 :     then ()
387 :     else errFn [
388 :     S "variable ", V x, S " is not bound in new ",
389 :     S(Atom.toString strand)
390 :     ]
391 :     in
392 :     List.app checkVar args
393 :     end
394 : jhr 3475 | IR.SAVE{lhs, rhs, ...} => let
395 : jhr 3470 val bvs = VSet.union(Avail.inValue nd, bvs)
396 :     in
397 :     if VSet.member(bvs, rhs)
398 :     then ()
399 :     else errFn [
400 :     S "variable ", V rhs, S " is not bound in save ",
401 : jhr 3475 S(IR.StateVar.toString lhs)
402 : jhr 3470 ];
403 : jhr 3475 if Ty.same(IR.StateVar.ty lhs, V.ty rhs)
404 : jhr 3470 then ()
405 :     else errFn [
406 : jhr 3475 S "type mismatch in \"", S(IR.StateVar.toString lhs),
407 : jhr 3470 S " = ", S(V.toString rhs), S "\"",
408 : jhr 3475 NL, S "lhs: ", TY(IR.StateVar.ty lhs),
409 : jhr 3470 NL, S "rhs: ", TY(V.ty rhs)
410 :     ]
411 :     end
412 :     | _ => ()
413 :     (* end case *))
414 :     in
415 :     List.app checkEdges nodes;
416 :     List.app checkNd nodes;
417 :     (* cleanup *)
418 :     Avail.scrub nodes
419 :     end
420 :     (* check a strand definition *)
421 : jhr 3485 fun checkStrand (IR.Strand{name, params, state, stateInit, initM, updateM, stabilizeM}) =
422 :     let
423 : jhr 3470 val nStateVars = List.length state
424 :     val extraVars = params
425 : jhr 3485 fun checkMethod body = checkCFG (extraVars, body)
426 : jhr 3470 (*DEBUG*)handle ex => raise ex
427 :     in
428 :     checkCFG (extraVars, stateInit)
429 :     (*DEBUG*)handle ex => raise ex;
430 : jhr 3485 Option.app checkMethod initM;
431 :     checkMethod updateM;
432 :     Option.app checkMethod stabilizeM
433 : jhr 3470 end
434 :     (* handle exceptions *)
435 :     fun onExn exn =
436 :     errFn (S "uncaught exception: " :: S(exnMessage exn) ::
437 :     List.foldr (fn (s, msg) => NL :: S " raised at " :: S s :: msg)
438 :     [] (SMLofNJ.exnHistory exn))
439 : jhr 3485 fun checkCFG' cfg = (checkCFG ([], cfg) handle ex => onExn ex)
440 : jhr 3470 in
441 :     (* check the input part *)
442 : jhr 3485 checkCFG' constInit;
443 : jhr 3470 (* check the global part *)
444 : jhr 3485 checkCFG' globalInit;
445 :     (* check initial strand creation *)
446 :     case create of IR.Create{dim, code} => checkCFG' code;
447 : jhr 3470 (* check the strands *)
448 : jhr 3485 (checkStrand strand) handle ex => onExn ex;
449 :     (* check the optional global update *)
450 :     Option.app checkCFG' update;
451 : jhr 3470 (* check for errors *)
452 :     final()
453 :     end
454 :    
455 :     end

root@smlnj-gforge.cs.uchicago.edu
ViewVC Help
Powered by ViewVC 1.0.0