lustrec / src / features / machine_types / machine_types.ml @ 66359a5e
History  View  Annotate  Download (14.8 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 
 _ > assert false (* TODO deal with other constructs *) 
282 
) 
283 
(* could depend on the actual computed type *) 
284  
285 
let type_name typ = 
286 
MTypes.print_ty Format.str_formatter typ; 
287 
Format.flush_str_formatter () 
288  
289 
let pp_var_type fmt v = 
290 
let typ = get_specified_type v in 
291 
MTypes.print_ty fmt typ 
292  
293 
let pp_c_var_type fmt v = 
294 
let typ = get_specified_type v in 
295 
MTypes.print_ty_param MT.pp_c fmt typ 
296 

297 
(************** Checking types ******************) 
298 

299 
let erroneous_annotation loc = 
300 
Format.eprintf "Invalid annotation for machine_type at loc %a@." 
301 
Location.pp_loc loc; 
302 
assert false 
303  
304  
305 
let valid_subtype subtype typ = 
306 
let mismatch subtyp typ = 
307 
Format.eprintf "Subtype mismatch %a vs %a@." MTypes.print_ty subtyp Types.print_ty typ; false 
308 
in 
309 
match (MTypes.dynamic_type subtype).MTypes.tdesc with 
310 

311 
 MTypes.Tbasic MT.MTint _ > Types.is_int_type typ 
312 
 MTypes.Tbasic MT.MTreal _ > Types.is_real_type typ 
313 
 MTypes.Tbasic MT.MTbool > Types.is_bool_type typ 
314 
 _ > mismatch subtype typ 
315 

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

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

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

341 
(************** Registering annotations ******************) 
342  
343 

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

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

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

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

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

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

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

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