Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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