lustrec / src / features / machine_types / machine_types.ml @ 95944ba1
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 Lustre_types 
41  
42 
let is_active = false 
43 

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

114 

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

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

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

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

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

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

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

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

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

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

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

300 
(************** Checking types ******************) 
301 

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

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

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

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

344 
(************** Registering annotations ******************) 
345  
346 

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

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

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

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

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

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

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

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