Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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
(* compile-command:"make -C ../.." *)
480
(* End: *)
481