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-il-fn.sml
ViewVC logotype

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3470 - (view) (download)

1 : jhr 3470 (* check-il-fn.sml
2 :     *
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 :     * Correctness checker for SSA-based ILs.
9 :     *
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 :     end
29 :    
30 :     functor CheckILFn (
31 :    
32 :     structure IL : SSA
33 :     structure OpTy : OPERATOR_TY
34 :     where type rator = IL.Op.rator
35 :     where type ty = IL.Ty.ty
36 :    
37 :     ) : sig
38 :    
39 :     (* check the program for type errors, etc. The first argument will be used to
40 :     * identify the phase that the check follows and the return result will be true
41 :     * if any errors were detected.
42 :     *)
43 :     val check : string * IL.program -> bool
44 :    
45 :     end = struct
46 :    
47 :     structure IL = IL
48 :     structure Ty = IL.Ty
49 :     structure V = IL.Var
50 :     structure VSet = V.Set
51 :    
52 :     (* forward analysis to determine the variables that are available in blocks *)
53 :     structure Avail = ForwardDFAFn (
54 :     struct
55 :    
56 :     structure IL = IL
57 :     type t = VSet.set
58 :    
59 :     val bottom = VSet.empty
60 :    
61 :     fun join inputs = List.foldl VSet.union bottom inputs
62 :    
63 :     fun transfer (input, nd as IL.ND{kind, ...}) = (case kind
64 :     of IL.JOIN{phis, ...} => let
65 :     (* add the lhs of the phi node. We do not remove the rhs variables, since
66 :     * after value numbering, they may have further uses.
67 :     *)
68 :     fun doPhi ((y, _), vs) = VSet.add(vs, y)
69 :     val output = List.foldl doPhi input (!phis)
70 :     in
71 :     output
72 :     end
73 :     | IL.ASSIGN{stm=(y, _), ...} => VSet.add(input, y)
74 :     | IL.MASSIGN{stm=(ys, _, _), ...} => VSet.addList(input, ys)
75 :     | _ => input
76 :     (* end case *))
77 :    
78 :     val same = VSet.equal
79 :    
80 :     fun toString vs = let
81 :     fun f (v, []) = [IL.Var.toString v, "}"]
82 :     | f (v, l) = IL.Var.toString v :: "," :: l
83 :     in
84 :     if VSet.isEmpty vs then "{}" else String.concat("{" :: VSet.foldl f [] vs)
85 :     end
86 :    
87 :     end)
88 :    
89 :     datatype token
90 :     = NL | S of string | A of Atom.atom | V of IL.var | VTYS of IL.var list
91 :     | TY of Ty.ty | TYS of Ty.ty list
92 :     | ND of IL.node
93 :    
94 :     fun error errBuf toks = let
95 :     fun tok2str NL = "\n ** "
96 :     | tok2str (S s) = s
97 :     | tok2str (A s) = Atom.toString s
98 :     | tok2str (V x) = V.toString x
99 :     | tok2str (VTYS xs) = tok2str(TYS(List.map V.ty xs))
100 :     | tok2str (TY ty) = Ty.toString ty
101 :     | tok2str (TYS []) = "()"
102 :     | tok2str (TYS[ty]) = Ty.toString ty
103 :     | tok2str (TYS tys) = String.concat[
104 :     "(", String.concatWith " * " (List.map Ty.toString tys), ")"
105 :     ]
106 :     | tok2str (ND nd) = IL.Node.toString nd
107 :     in
108 :     errBuf := concat ("**** Error: " :: List.map tok2str toks)
109 :     :: !errBuf
110 :     end
111 :    
112 :     fun checkAssign errFn ((y, rhs), bvs) = let
113 :     (* check a variable use *)
114 :     fun checkVar x = if VSet.member(bvs, x)
115 :     then ()
116 :     else errFn [
117 :     S "variable ", V x, S " is not bound in", NL,
118 :     S(IL.assignToString(y, rhs))
119 :     ]
120 :     fun tyError (ty1, ty2) = errFn [
121 :     S "type mismatch in \"", S(IL.assignToString (y, rhs)), S "\"",
122 :     NL, S "lhs: ", TY ty1, NL, S "rhs: ", TY ty2
123 :     ]
124 :     fun checkTys (ty1, ty2) = if Ty.same(ty1, ty2)
125 :     then ()
126 :     else tyError (ty1, ty2)
127 :     in
128 :     (* check that y is not bound twice *)
129 :     if VSet.member(bvs, y)
130 :     then errFn [
131 :     S "variable ", V y, S " is bound twice in", NL,
132 :     S(IL.assignToString (y, rhs))
133 :     ]
134 :     else ();
135 :     case rhs
136 :     of IL.GLOBAL x => checkTys(V.ty y, IL.GlobalVar.ty x)
137 :     | IL.STATE x => checkTys(V.ty y, IL.StateVar.ty x)
138 :     | IL.VAR x => (
139 :     checkVar x;
140 :     checkTys (V.ty y, V.ty x))
141 :     | IL.LIT lit => let
142 :     val ty = (case lit
143 :     of Literal.Int _ => Ty.intTy
144 :     | Literal.Real _ => Ty.realTy
145 :     | Literal.String _ => Ty.StringTy
146 :     | Literal.Bool _ => Ty.BoolTy
147 :     (* end case *))
148 :     in
149 :     checkTys (V.ty y, ty)
150 :     end
151 :     | IL.OP(rator, xs) => let
152 :     val (resTy, argTys) = OpTy.sigOf rator
153 :     in
154 :     List.app checkVar xs;
155 :     checkTys (V.ty y, resTy);
156 :     if ListPair.allEq (fn (x, ty) => Ty.same(V.ty x, ty)) (xs, argTys)
157 :     then ()
158 :     else errFn [
159 :     S "argument type mismatch in \"", S(IL.assignToString (y, rhs)), S "\"",
160 :     NL, S "expected: ", TYS argTys,
161 :     NL, S "found: ", VTYS xs
162 :     ]
163 :     end
164 :     | IL.CONS(xs, ty) => (
165 :     List.app checkVar xs;
166 :     if OpTy.typeOfCons (ty, List.map V.ty xs)
167 :     then checkTys (V.ty y, ty)
168 :     else errFn [S "invalid ", S(IL.assignToString(y, rhs))])
169 :     | IL.SEQ(xs, ty) => (
170 :     List.app checkVar xs;
171 :     (* FIXME: check types of sequence elements *)())
172 :     | IL.EINAPP(ein, xs) => (
173 :     List.app checkVar xs;
174 :     (* FIXME: check ein *)())
175 :     (* end case *);
176 :     VSet.add(bvs, y)
177 :     end
178 :    
179 :     fun checkMAssign errFn (stm as (ys, rator, xs), bvs) = let
180 :     (* check that a lhs variable is not bound twice *)
181 :     fun checkBind y = if VSet.member(bvs, y)
182 :     then errFn [
183 :     S "variable ", V y, S " is bound twice in", NL,
184 :     S(IL.massignToString stm)
185 :     ]
186 :     else ()
187 :     (* check a variable use *)
188 :     fun checkVar x = if VSet.member(bvs, x)
189 :     then ()
190 :     else errFn [
191 :     S "variable ", V x, S " is not bound in", NL,
192 :     S(IL.massignToString stm)
193 :     ]
194 :     fun tyError (ty1, ty2) = errFn [
195 :     S "type mismatch in \"", S(IL.massignToString stm), S "\"",
196 :     NL, S "lhs: ", TY ty1, NL, S "rhs: ", TY ty2
197 :     ]
198 :     in
199 :     (* check that the lhs variables are not bound twice *)
200 :     List.app checkBind ys;
201 :     (* FIXME:
202 :     (* check the types *)
203 :     val (resTys, argTys) = OpTy.sigOf rator
204 :     in
205 :     List.app checkVar xs;
206 :     if ListPair.allEq (fn (y, ty) => Ty.same(V.ty y, ty)) (ys, resTys)
207 :     then ()
208 :     else tyError (V.ty y, resTy);
209 :     if ListPair.allEq (fn (x, ty) => Ty.same(V.ty x, ty)) (xs, argTys)
210 :     then ()
211 :     else errFn [
212 :     S "argument type mismatch in \"", S(IL.massignToString stm), S "\"",
213 :     NL, S "expected: ", TYS argTys,
214 :     NL, S "found: ", VTYS xs
215 :     ]
216 :     end
217 :     *)
218 :     VSet.addList(bvs, ys)
219 :     end
220 :    
221 :     fun checkPhi errFn (nd, bvs, mask) (y, xs) = let
222 :     val ty = V.ty y
223 :     fun chkTy x = if Ty.same(V.ty x, ty)
224 :     then ()
225 :     else errFn [
226 :     S "type mismatch in \"", S(IL.phiToString (y, xs)), S "\"", NL,
227 :     S "typeof(", V y, S "): ", TY ty, NL,
228 :     S "typeof(", V x, S "): ", TY(V.ty x)
229 :     ]
230 :     fun chkRHS ([], []) = ()
231 :     | chkRHS (true::ms, NONE::xs) = chkRHS (ms, xs)
232 :     | chkRHS (false::ms, (SOME x)::xs) = (chkTy x; chkRHS (ms, xs))
233 :     | chkRHS _ = errFn [S "phi/mask mismatch in ", ND nd]
234 :     in
235 :     (* check that y is not bound twice *)
236 :     if VSet.member(bvs, y)
237 :     then errFn [
238 :     S "variable ", V y, S " is bound twice in", NL,
239 :     S(IL.phiToString (y, xs))
240 :     ]
241 :     else ();
242 :     (* check that rhs vars have the correct type *)
243 :     chkRHS (mask, xs)
244 :     end
245 :    
246 :     fun check (phase, IL.Program{globals, props, inputInit, globalInit, initially, strands}) = let
247 :     val errBuf = ref []
248 :     val errFn = error errBuf
249 :     fun final () = (case !errBuf
250 :     of [] => false
251 :     | errs => (
252 :     Log.msg(concat["********** IL Errors detected after ", phase, " **********\n"]);
253 :     List.app (fn msg => Log.msg(msg ^ "\n")) (List.rev errs);
254 :     true)
255 :     (* end case *))
256 :     val checkPhi = checkPhi errFn
257 :     val checkAssign = checkAssign errFn
258 :     val checkMAssign = checkMAssign errFn
259 :     fun checkCFG (vs, cfg) = let
260 :     val bvs = VSet.fromList vs
261 :     (* compute the variables available on entry to each block *)
262 :     val nodes = Avail.analyse (bvs, cfg)
263 :     (* check the edges of a node. For each predecessor, the node should appear in the
264 :     * successor list and for each successor, the node should appear in the predecessor
265 :     * list.
266 :     *)
267 :     fun checkEdges nd = let
268 :     fun eqNd nd' = IL.Node.same(nd, nd')
269 :     fun chkPred src = if List.exists eqNd (IL.Node.succs src)
270 :     then ()
271 :     else errFn [
272 :     S "predecessor edge from ", ND nd, S " -> ", ND src,
273 :     S " not matched by successor edge"
274 :     ]
275 :     fun chkSucc dst = if List.exists eqNd (IL.Node.preds dst)
276 :     then ()
277 :     else errFn [
278 :     S "successor edge from ", ND nd, S " -> ", ND dst,
279 :     S " not matched by predecessor edge"
280 :     ]
281 :     in
282 :     List.app chkPred (IL.Node.preds nd);
283 :     List.app chkSucc (IL.Node.succs nd)
284 :     end
285 :     fun checkNd (nd as IL.ND{kind, ...}) = (case kind
286 :     of IL.NULL => errFn [S "unexpected ", ND nd]
287 :     | IL.JOIN{mask, phis, ...} =>
288 :     List.app
289 :     (checkPhi (nd, VSet.union(Avail.inValue nd, bvs), !mask))
290 :     (!phis)
291 :     | IL.COND{cond, ...} =>
292 :     if VSet.member(Avail.inValue nd, cond)
293 :     orelse VSet.member(bvs, cond)
294 :     then ()
295 :     else errFn [S "unbound variable ", V cond, S " in conditional"]
296 :     | IL.ASSIGN{stm, ...} =>
297 :     ignore (checkAssign (stm, VSet.union(Avail.inValue nd, bvs)))
298 :     | IL.MASSIGN{stm, ...} =>
299 :     ignore (checkMAssign (stm, VSet.union(Avail.inValue nd, bvs)))
300 :     | IL.GASSIGN{lhs, rhs, ...} => let
301 :     val bvs = VSet.union(Avail.inValue nd, bvs)
302 :     in
303 :     if VSet.member(bvs, rhs)
304 :     then ()
305 :     else errFn [
306 :     S "variable ", V rhs, S " is not bound in global assignment ",
307 :     S(IL.GlobalVar.toString lhs)
308 :     ];
309 :     if Ty.same(IL.GlobalVar.ty lhs, V.ty rhs)
310 :     then ()
311 :     else errFn [
312 :     S "type mismatch in \"", S(IL.GlobalVar.toString lhs),
313 :     S " = ", S(V.toString rhs), S "\"",
314 :     NL, S "lhs: ", TY(IL.GlobalVar.ty lhs),
315 :     NL, S "rhs: ", TY(V.ty rhs)
316 :     ]
317 :     end
318 :     | IL.NEW{strand, args, ...} => let
319 :     val bvs = VSet.union(Avail.inValue nd, bvs)
320 :     (* check a variable use *)
321 :     fun checkVar x = if VSet.member(bvs, x)
322 :     then ()
323 :     else errFn [
324 :     S "variable ", V x, S " is not bound in new ",
325 :     S(Atom.toString strand)
326 :     ]
327 :     in
328 :     List.app checkVar args
329 :     end
330 :     | IL.SAVE{lhs, rhs, ...} => let
331 :     val bvs = VSet.union(Avail.inValue nd, bvs)
332 :     in
333 :     if VSet.member(bvs, rhs)
334 :     then ()
335 :     else errFn [
336 :     S "variable ", V rhs, S " is not bound in save ",
337 :     S(IL.StateVar.toString lhs)
338 :     ];
339 :     if Ty.same(IL.StateVar.ty lhs, V.ty rhs)
340 :     then ()
341 :     else errFn [
342 :     S "type mismatch in \"", S(IL.StateVar.toString lhs),
343 :     S " = ", S(V.toString rhs), S "\"",
344 :     NL, S "lhs: ", TY(IL.StateVar.ty lhs),
345 :     NL, S "rhs: ", TY(V.ty rhs)
346 :     ]
347 :     end
348 :     | _ => ()
349 :     (* end case *))
350 :     in
351 :     List.app checkEdges nodes;
352 :     List.app checkNd nodes;
353 :     (* cleanup *)
354 :     Avail.scrub nodes
355 :     end
356 :     (* check a strand definition *)
357 :     fun checkStrand (IL.Strand{name, params, state, stateInit, methods}) = let
358 :     val nStateVars = List.length state
359 :     val extraVars = params
360 :     fun checkMethod (IL.Method{name, body, ...}) = checkCFG (extraVars, body)
361 :     (*DEBUG*)handle ex => raise ex
362 :     in
363 :     checkCFG (extraVars, stateInit)
364 :     (*DEBUG*)handle ex => raise ex;
365 :     List.app checkMethod methods
366 :     end
367 :     (* handle exceptions *)
368 :     fun onExn exn =
369 :     errFn (S "uncaught exception: " :: S(exnMessage exn) ::
370 :     List.foldr (fn (s, msg) => NL :: S " raised at " :: S s :: msg)
371 :     [] (SMLofNJ.exnHistory exn))
372 :     in
373 :     (* check the input part *)
374 :     checkCFG ([], inputInit) handle ex => onExn ex;
375 :     (* check the global part *)
376 :     checkCFG ([], globalInit) handle ex => onExn ex;
377 :     (* FIXME: need to check initially *)
378 :     (* check the strands *)
379 :     (List.app checkStrand strands) handle ex => onExn ex;
380 :     (* check for errors *)
381 :     final()
382 :     end
383 :    
384 :     end

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