Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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