lustrec / src / features / machine_types / machine_types.ml @ 3c3414c5
History  View  Annotate  Download (15 KB)
1 
(* Extension du deal with machine types annotation 

2  
3 
In each node, node local annotations can specify the actual type of the 
4 
implementation uintXX, intXX, floatXX ... 
5  
6 
The module provide utility functions to query the model: 
7 
 get_var_machine_type varid nodeid returns the string denoting the actual type 
8  
9 
The actual type is used at different stages of the coompilation 
10 
 early stage: limited typing, ie validity of operation are checked 
11 
 a first version ensures that the actual type is a subtype of the declared/infered ones 
12 
eg uint8 is a valid subtype of int 
13 
 a future implementation could ensures that operations are valid 
14 
 each standard or unspecified operation should be homogeneous : 
15 
op: real > real > real is valid for any same subtype t of real: op: t > t > t 
16 
 specific nodes that explicitely defined subtypes could be used to perform casts 
17 
eg. a int2uint8 (i: int) returns (j: int) with annotations specifying i as int and j as uint8 
18 
 C backend: any print of a typed variable should rely on the actual machine type when provided 
19 
 EMF backend: idem 
20 
 Horn backend: an option could enforce the bounds provided by the machine 
21 
type or implement the cycling behavior for integer subtypes 
22 
 Salsa plugin: the information should be propagated to the plugin. 
23 
One can also imagine that results of the analysis could specify or 
24 
substitute a type by a subtype. Eg. the analysis detects that a float32 is enough for variable z and 
25 
the annotation is added to the node. 
26  
27  
28 
A posisble behavior could be 
29 
 an option to ensure type checking 
30 
 dedicated conversion functions that, in C, would generate cast or calls to simple identity functions (to be inlined) 
31  
32  
33  
34 
TODO 
35 
EMF: rajouter les memoires dans les caracteristiques du node 
36 
gerer les types plus finement: 
37 
propager les types machines aux variables fraiches creees par la normalisation 
38  
39 
*) 
40 
open LustreSpec 
41 

42 
let keyword = ["machine_types"] 
43  
44 
module MT = 
45 
struct 
46  
47 
type int_typ = 
48 
 Tint8_t 
49 
 Tint16_t 
50 
 Tint32_t 
51 
 Tint64_t 
52 
 Tuint8_t 
53 
 Tuint16_t 
54 
 Tuint32_t 
55 
 Tuint64_t 
56  
57 
let pp_int fmt t = 
58 
match t with 
59 
 Tint8_t > Format.fprintf fmt "int8" 
60 
 Tint16_t > Format.fprintf fmt "int16" 
61 
 Tint32_t > Format.fprintf fmt "int32" 
62 
 Tint64_t > Format.fprintf fmt "int64" 
63 
 Tuint8_t > Format.fprintf fmt "uint8" 
64 
 Tuint16_t > Format.fprintf fmt "uint16" 
65 
 Tuint32_t > Format.fprintf fmt "uint32" 
66 
 Tuint64_t > Format.fprintf fmt "uint64" 
67  
68 
let pp_c_int fmt t = 
69 
match t with 
70 
 Tint8_t > Format.fprintf fmt "int8_t" 
71 
 Tint16_t > Format.fprintf fmt "int16_t" 
72 
 Tint32_t > Format.fprintf fmt "int32_t" 
73 
 Tint64_t > Format.fprintf fmt "int64_t" 
74 
 Tuint8_t > Format.fprintf fmt "uint8_t" 
75 
 Tuint16_t > Format.fprintf fmt "uint16_t" 
76 
 Tuint32_t > Format.fprintf fmt "uint32_t" 
77 
 Tuint64_t > Format.fprintf fmt "uint64_t" 
78  
79 
type t = 
80 
 MTint of int_typ option 
81 
 MTreal of string option 
82 
 MTbool 
83 
 MTstring 
84  
85 
open Format 
86 
let pp fmt t = 
87 
match t with 
88 
 MTint None > 
89 
fprintf fmt "int" 
90 
 MTint (Some s) > 
91 
fprintf fmt "%a" pp_int s 
92 
 MTreal None > 
93 
fprintf fmt "real" 
94 
 MTreal (Some s) > 
95 
fprintf fmt "%s" s 
96 
 MTbool > 
97 
fprintf fmt "bool" 
98 
 MTstring > 
99 
fprintf fmt "string" 
100  
101 
let pp_c fmt t = 
102 
match t with 
103 
 MTint (Some s) > 
104 
fprintf fmt "%a" pp_c_int s 
105 
 MTreal (Some s) > 
106 
fprintf fmt "%s" s 
107 
 MTint None 
108 
 MTreal None 
109 
 MTbool 
110 
 MTstring > assert false 
111 

112 

113 
let is_scalar_type t = 
114 
match t with 
115 
 MTbool 
116 
 MTint _ 
117 
 MTreal _ > true 
118 
 _ > false 
119  
120  
121 
let is_numeric_type t = 
122 
match t with 
123 
 MTint _ 
124 
 MTreal _ > true 
125 
 _ > false 
126  
127 
let is_int_type t = match t with MTint _ > true  _ > false 
128 
let is_real_type t = match t with MTreal _ > true  _ > false 
129 
let is_bool_type t = t = MTbool 
130 

131 
let is_dimension_type t = 
132 
match t with 
133 
 MTint _ 
134 
 MTbool > true 
135 
 _ > false 
136  
137 
let type_int_builder = MTint None 
138 
let type_real_builder = MTreal None 
139 
let type_bool_builder = MTbool 
140 
let type_string_builder = MTstring 
141  
142 
let unify _ _ = () 
143 
let is_unifiable b1 b2 = 
144 
match b1, b2 with 
145 
 MTint _ , MTint _ 
146 
 MTreal _, MTreal _ 
147 
 MTstring, MTstring 
148 
 MTbool, MTbool > true 
149 
 _ > false 
150  
151 
let is_exportable b = 
152 
match b with 
153 
 MTstring 
154 
 MTbool 
155 
 MTreal None 
156 
 MTint None > false 
157 
 _ > true 
158 
end 
159  
160 
module MTypes = Types.Make (MT) 
161  
162 
let type_uint8 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tuint8_t))) 
163 
let type_uint16 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tuint16_t))) 
164 
let type_uint32 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tuint32_t))) 
165 
let type_uint64 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tuint64_t))) 
166 
let type_int8 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tint8_t))) 
167 
let type_int16 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tint16_t))) 
168 
let type_int32 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tint32_t))) 
169 
let type_int64 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tint64_t))) 
170  
171 

172 
module ConvTypes = 
173 
struct 
174 
type type_expr = MTypes.type_expr 
175  
176 
let map_type_basic f_basic = 
177 
let rec map_type_basic e = 
178 
{ MTypes.tid = e.Types.tid; 
179 
MTypes.tdesc = map_type_basic_desc (Types.type_desc e) 
180 
} 
181 
and map_type_basic_desc td = 
182 
let mape = map_type_basic in 
183 
match td with 
184 
 Types.Tbasic b > f_basic b 
185 
 Types.Tconst c > MTypes.Tconst c 
186 
 Types.Tenum e > MTypes.Tenum e 
187 
 Types.Tvar > MTypes.Tvar 
188 
 Types.Tunivar > MTypes.Tunivar 
189 

190 
 Types.Tclock te > MTypes.Tclock (mape te) 
191 
 Types.Tarrow (te1, te2) > MTypes.Tarrow (mape te1, mape te2) 
192 
 Types.Ttuple tel > MTypes.Ttuple (List.map mape tel) 
193 
 Types.Tstruct id_te_l > MTypes.Tstruct (List.map (fun (id, te) > id, mape te) id_te_l) 
194 
 Types.Tarray (de, te) > MTypes.Tarray (de, mape te) 
195 
 Types.Tstatic (de, te) > MTypes.Tstatic (de, mape te) 
196 
 Types.Tlink te > MTypes.Tlink (mape te) 
197 
in 
198 
map_type_basic 
199 

200 
let import main_typ = 
201 
let import_basic b = 
202 
if Types.BasicT.is_int_type b then MTypes.type_int else 
203 
if Types.BasicT.is_real_type b then MTypes.type_real else 
204 
if Types.BasicT.is_bool_type b then MTypes.type_bool else 
205 
(Format.eprintf "importing %a with issues!@.@?" Types.print_ty main_typ; assert false) 
206 
in 
207 
map_type_basic import_basic main_typ 
208  
209 

210 
let map_mtype_basic f_basic = 
211 
let rec map_mtype_basic e = 
212 
{ Types.tid = e.MTypes.tid; 
213 
Types.tdesc = map_mtype_basic_desc (MTypes.type_desc e) 
214 
} 
215 
and map_mtype_basic_desc td = 
216 
let mape = map_mtype_basic in 
217 
match td with 
218 
 MTypes.Tbasic b > 
219 
(* Format.eprintf "supposely basic mtype: %a@." MTypes.BasicT.pp b; *) 
220 
f_basic b 
221 
 MTypes.Tconst c > Types.Tconst c 
222 
 MTypes.Tenum e > Types.Tenum e 
223 
 MTypes.Tvar > Types.Tvar 
224 
 MTypes.Tunivar > Types.Tunivar 
225 

226 
 MTypes.Tclock te > Types.Tclock (mape te) 
227 
 MTypes.Tarrow (te1, te2) > Types.Tarrow (mape te1, mape te2) 
228 
 MTypes.Ttuple tel > Types.Ttuple (List.map mape tel) 
229 
 MTypes.Tstruct id_te_l > Types.Tstruct (List.map (fun (id, te) > id, mape te) id_te_l) 
230 
 MTypes.Tarray (de, te) > Types.Tarray (de, mape te) 
231 
 MTypes.Tstatic (de, te) > Types.Tstatic (de, mape te) 
232 
 MTypes.Tlink te > Types.Tlink (mape te) 
233 
in 
234 
map_mtype_basic 
235 

236 
let export machine_type = 
237 
let export_basic b = 
238 
if MTypes.BasicT.is_int_type b then Types.type_int else 
239 
if MTypes.BasicT.is_real_type b then Types.type_real else 
240 
if MTypes.BasicT.is_bool_type b then Types.type_bool else 
241 
( 
242 
Format.eprintf "unhandled basic mtype is %a. Issues while dealing with basic type %a@.@?" MTypes.print_ty machine_type MTypes.BasicT.pp b; 
243 
assert false 
244 
) 
245 
in 
246 
map_mtype_basic export_basic machine_type 
247  
248 
end 
249  
250 
module Typing = Typing.Make (MTypes) (ConvTypes) 
251 

252 
(* Associate to each (node_id, var_id) its machine type *) 
253 
let machine_type_table : (var_decl, MTypes.type_expr) Hashtbl.t = Hashtbl.create 13 
254  
255 
(* Store the node signatures, with machine types when available *) 
256 
let typing_env = ref Env.initial 
257 

258 
let is_specified v = 
259 
(* Format.eprintf "looking for var %a@." Printers.pp_var v; *) 
260 
Hashtbl.mem machine_type_table v 
261  
262 
let pp_table fmt = 
263 
Format.fprintf fmt "@[<v 0>["; 
264 
Hashtbl.iter 
265 
(fun v typ > Format.fprintf fmt "%a > %a,@ " Printers.pp_var v MTypes.print_ty typ ) 
266 
machine_type_table; 
267 
Format.fprintf fmt "@]" 
268  
269 

270 
let get_specified_type v = 
271 
(* Format.eprintf "Looking for variable %a in table [%t]@.@?" *) 
272 
(* Printers.pp_var v *) 
273 
(* pp_table; *) 
274 
Hashtbl.find machine_type_table v 
275  
276 
let is_exportable v = 
277 
is_specified v && ( 
278 
let typ = get_specified_type v in 
279 
match (MTypes.dynamic_type typ).MTypes.tdesc with 
280 
 MTypes.Tbasic b > MT.is_exportable b 
281 
 MTypes.Tconst _ > false (* Enumerated types are not "machine type" customizeable *) 
282 
 _ > assert false (* TODO deal with other constructs *) 
283 
) 
284 
(* could depend on the actual computed type *) 
285  
286 
let type_name typ = 
287 
MTypes.print_ty Format.str_formatter typ; 
288 
Format.flush_str_formatter () 
289  
290 
let pp_var_type fmt v = 
291 
let typ = get_specified_type v in 
292 
MTypes.print_ty fmt typ 
293  
294 
let pp_c_var_type fmt v = 
295 
let typ = get_specified_type v in 
296 
MTypes.print_ty_param MT.pp_c fmt typ 
297 

298 
(************** Checking types ******************) 
299 

300 
let erroneous_annotation loc = 
301 
Format.eprintf "Invalid annotation for machine_type at loc %a@." 
302 
Location.pp_loc loc; 
303 
assert false 
304  
305  
306 
let valid_subtype subtype typ = 
307 
let mismatch subtyp typ = 
308 
Format.eprintf "Subtype mismatch %a vs %a@." MTypes.print_ty subtyp Types.print_ty typ; false 
309 
in 
310 
match (MTypes.dynamic_type subtype).MTypes.tdesc with 
311 
 MTypes.Tconst c > Types.is_const_type typ c 
312 
 MTypes.Tbasic MT.MTint _ > Types.is_int_type typ 
313 
 MTypes.Tbasic MT.MTreal _ > Types.is_real_type typ 
314 
 MTypes.Tbasic MT.MTbool > Types.is_bool_type typ 
315 
 _ > mismatch subtype typ 
316 

317 
let type_of_name name = 
318 
match name with 
319 
 "uint8" > type_uint8 
320 
 "uint16" > type_uint16 
321 
 "uint32" > type_uint32 
322 
 "uint64" > type_uint64 
323 
 "int8" > type_int8 
324 
 "int16" > type_int16 
325 
 "int32" > type_int32 
326 
 "int64" > type_int64 
327 
 _ > assert false (* unknown custom machine type *) 
328 

329 
let register_var var typ = 
330 
(* let typ = type_of_name type_name in *) 
331 
if valid_subtype typ var.var_type then ( 
332 
Hashtbl.add machine_type_table var typ 
333 
) 
334 
else 
335 
erroneous_annotation var.var_loc 
336 

337 
(* let register_var_opt var type_name_opt = *) 
338 
(* match type_name_opt with *) 
339 
(*  None > () *) 
340 
(*  Some type_name > register_var var type_name *) 
341 

342 
(************** Registering annotations ******************) 
343  
344 

345 
let register_node node_id vars annots = 
346 
List.fold_left (fun accu annot > 
347 
let annl = annot.annots in 
348 
List.fold_left (fun accu (kwd, value) > 
349 
if kwd = keyword then 
350 
let expr = value.eexpr_qfexpr in 
351 
match Corelang.expr_list_of_expr expr with 
352 
 [var_id; type_name] > ( 
353 
match var_id.expr_desc, type_name.expr_desc with 
354 
 Expr_ident var_id, Expr_const (Const_string type_name) > 
355 
let var = List.find (fun v > v.var_id = var_id) vars in 
356 
Log.report ~level:2 (fun fmt > 
357 
Format.fprintf fmt "Recorded type %s for variable %a (parent node is %s)@ " 
358 
type_name 
359 
Printers.pp_var var 
360 
(match var.var_parent_nodeid with Some id > id  None > "unknown") 
361 
); 
362 
let typ = type_of_name type_name in 
363 
register_var var typ; 
364 
var::accu 
365 
 _ > erroneous_annotation expr.expr_loc 
366 
) 
367 
 _ > erroneous_annotation expr.expr_loc 
368 
else 
369 
accu 
370 
) accu annl 
371 
) [] annots 
372  
373  
374 
let check_node nd vars = 
375 
(* TODO check that all access to vars are valid *) 
376 
() 
377 

378 
let type_of_vlist vars = 
379 
let tyl = List.map (fun v > if is_specified v then get_specified_type v else 
380 
ConvTypes.import v.var_type 
381 
) vars in 
382 
MTypes.type_of_type_list tyl 
383  
384 

385 
let load prog = 
386 
let init_env = 
387 
Env.fold (fun id typ env > 
388 
Env.add_value env id (ConvTypes.import typ) 
389 
) 
390 
Basic_library.type_env Env.initial in 
391 
let env = 
392 
List.fold_left (fun type_env top > 
393 
match top.top_decl_desc with 
394 
 Node nd > 
395 
(* Format.eprintf "Registeing node %s@." nd.node_id; *) 
396 
let vars = nd.node_inputs @ nd.node_outputs @ nd.node_locals in 
397 
let constrained_vars = register_node nd.node_id vars nd.node_annot in 
398 
check_node nd constrained_vars; 
399  
400 
(* Computing the node type *) 
401 
let ty_ins = type_of_vlist nd.node_inputs in 
402 
let ty_outs = type_of_vlist nd.node_outputs in 
403 
let ty_node = MTypes.new_ty (MTypes.Tarrow (ty_ins,ty_outs)) in 
404 
Typing.generalize ty_node; 
405 
let env = Env.add_value type_env nd.node_id ty_node in 
406 
(* Format.eprintf "Env: %a" (Env.pp_env MTypes.print_ty) env; *) 
407 
env 
408  
409 
 _ > type_env 
410 
(*  ImportedNode ind > *) 
411 
(* let vars = ind.nodei_inputs @ ind.nodei_outputs in *) 
412 
(* register_node ind.nodei_id vars ind.nodei_annot *) 
413 
(*  _ > () TODO: shall we load something for Open statements? *) 
414 
) init_env prog 
415 
in 
416 
typing_env := env 
417  
418 
let type_expr nd expr = 
419 
let init_env = !typing_env in 
420 
(* Format.eprintf "Init env: %a@." (Env.pp_env MTypes.print_ty) init_env; *) 
421 
let init_vars = nd.node_inputs @ nd.node_outputs @ nd.node_locals in 
422 
(* Rebuilding the variables environment from accumulated knowledge *) 
423 
let env,vars = (* First, we add non specified variables *) 
424 
List.fold_left (fun (env, vars) v > 
425 
if not (is_specified v) then 
426 
let env = Env.add_value env v.var_id (ConvTypes.import v.var_type) in 
427 
env, v::vars 
428 
else 
429 
env, vars 
430 
) (init_env, []) init_vars 
431 
in 
432 

433 
(* Then declared ones *) 
434 
let env, vars = 
435 
Hashtbl.fold (fun vdecl machine_type (env, vds) > 
436 
if vdecl.var_parent_nodeid = Some nd.node_id then ( 
437 
(* Format.eprintf "Adding variable %a to the environement@." Printers.pp_var vdecl; *) 
438 
let env = Env.add_value env vdecl.var_id machine_type in 
439 
env, vdecl::vds 
440 
) 
441 
else 
442 
env, vds 
443 
) machine_type_table (env, vars) 
444 
in 
445  
446 

447 
(* Format.eprintf "env with local vars: %a@." (Env.pp_env MTypes.print_ty) env; *) 
448 
(* Format.eprintf "expr = %a@." Printers.pp_expr expr; *) 
449 
(* let res = *) 
450 
Typing.type_expr 
451 
(env,vars) 
452 
false (* not in main node *) 
453 
false (* no a constant *) 
454 
expr 
455 
(* in *) 
456 
(* Format.eprintf "typing ok = %a@." MTypes.print_ty res; *) 
457 
(* res *) 
458 

459 
(* Typing the expression (vars = expr) in node 
460 

461 
*) 
462 
let type_def node vars expr = 
463 
(* Format.eprintf "Typing def %a = %a@.@." *) 
464 
(* (Utils.fprintf_list ~sep:", " Printers.pp_var) vars *) 
465 
(* Printers.pp_expr expr *) 
466 
(* ; *) 
467 
let typ = type_expr node expr in 
468 
(* Format.eprintf "Type is %a. Saving stuff@.@." MTypes.print_ty typ; *) 
469 
let typ = MTypes.type_list_of_type typ in 
470 
List.iter2 register_var vars typ 
471  
472 
let has_machine_type () = 
473 
let annl = Annotations.get_expr_annotations keyword in 
474 
(* Format.eprintf "has _mchine _type annotations: %i@." (List.length annl); *) 
475 
List.length annl > 0 
476 

477 
(* Local Variables: *) 
478 
(* compilecommand:"make C ../.." *) 
479 
(* End: *) 
480 