Project

General

Profile

« Previous | Next » 

Revision 66359a5e

Added by Pierre-Loïc Garoche about 7 years ago

[general] large modification: added machine types, a second typing phase dealing with machine types (eg uint8)
typing was transformed as a functor and parametrized by basic types (int/real/bool)
it can also be applied multiple times on the same program

View differences:

src/_tags.in
9 9
"plugins/salsa": include
10 10
"plugins/scopes": include
11 11
"plugins/mpfr": include
12
"features/machine_types": include
12 13
"tools/stateflow": include
13 14
"tools/stateflow/common": include
14 15
"tools/stateflow/semantics": include
......
46 47

  
47 48
# Local Variables:
48 49
# mode: conf
49
# End:
50
# End:
src/automata.ml
114 114
let node_vars_of_idents node iset =
115 115
  List.fold_right (fun v res -> if ISet.mem v.var_id iset then v :: res else res) (get_node_vars node) []
116 116

  
117
let mkautomata_state used typedef loc id =
117
let mkautomata_state nodeid used typedef loc id =
118 118
  let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = loc } in
119 119
  let tydec_state id = { ty_dec_desc = Tydec_const id; ty_dec_loc = loc } in
120 120
  let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = loc } in
......
125 125
  let actual_r = mk_new_name used (id ^ "__restart_act") in
126 126
  let actual_s = mk_new_name used (id ^ "__state_act") in
127 127
  {
128
    incoming_r' = mkvar_decl loc (incoming_r', tydec_bool, ckdec_any, false, None);
129
    incoming_s' = mkvar_decl loc (incoming_s', tydec_state typedef.tydef_id, ckdec_any, false, None);
130
    incoming_r = mkvar_decl loc (incoming_r, tydec_bool, ckdec_any, false, None);
131
    incoming_s = mkvar_decl loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false, None);
132
    actual_r = mkvar_decl loc (actual_r  , tydec_bool, ckdec_any, false, None);
133
    actual_s = mkvar_decl loc (actual_s  , tydec_state typedef.tydef_id, ckdec_any, false, None)
128
    incoming_r' = mkvar_decl loc (incoming_r', tydec_bool, ckdec_any, false, None, Some nodeid);
129
    incoming_s' = mkvar_decl loc (incoming_s', tydec_state typedef.tydef_id, ckdec_any, false, None, Some nodeid);
130
    incoming_r = mkvar_decl loc (incoming_r, tydec_bool, ckdec_any, false, None, Some nodeid);
131
    incoming_s = mkvar_decl loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false, None, Some nodeid);
132
    actual_r = mkvar_decl loc (actual_r  , tydec_bool, ckdec_any, false, None, Some nodeid);
133
    actual_s = mkvar_decl loc (actual_s  , tydec_state typedef.tydef_id, ckdec_any, false, None, Some nodeid)
134 134
  }
135 135

  
136 136
let vars_of_aut_state aut_state =
......
225 225

  
226 226
let expand_automata nused used owner typedef node aut =
227 227
  let initial = (List.hd aut.aut_handlers).hand_state in
228
  let aut_state = mkautomata_state used typedef aut.aut_loc aut.aut_id in
228
  let aut_state = mkautomata_state node.node_id used typedef aut.aut_loc aut.aut_id in
229 229
  let unodes = List.map (fun h -> node_of_unless nused used node aut.aut_id aut_state h) aut.aut_handlers in
230 230
  let aunodes = List.map (fun h -> node_of_assign_until nused used node aut.aut_id aut_state h) aut.aut_handlers in
231 231
  let all_outputs = List.fold_left (fun all (outputs, _, _) -> ISet.union outputs all) ISet.empty aunodes in
src/backends/C/c_backend_common.ml
61 61
    var_dec_clock = mkclock Location.dummy_loc Ckdec_any;
62 62
    var_dec_const = false;
63 63
    var_dec_value = None;
64
    var_parent_nodeid = None;
64 65
    var_type = Type_predef.type_arrow (Types.new_var ()) (Types.new_var ());
65 66
    var_clock = Clocks.new_var true;
66 67
    var_loc = loc }
......
124 125
 | Dimension.Dunivar    -> fprintf fmt "'%s" (Utils.name_of_dimension dim.Dimension.dim_id)
125 126

  
126 127
let is_basic_c_type t =
127
  match (Types.repr t).Types.tdesc with
128
  | Types.Tbool | Types.Treal | Types.Tint  -> true
129
  | _                                       -> false
130

  
131
let pp_c_basic_type_desc t_dsec =
132
  match t_dsec with
133
  | Types.Tbool when !Options.cpp  -> "bool"
134
  | Types.Tbool                    -> "_Bool"
135
  | Types.Tint                     -> !Options.int_type
136
  | Types.Treal when !Options.mpfr -> Mpfr.mpfr_t
137
  | Types.Treal                    -> !Options.real_type
138
  | _ -> assert false (* Not a basic C type. Do not handle arrays or pointers *)
128
  Types.is_int_type t || Types.is_real_type t || Types.is_bool_type t
129

  
130
let pp_c_basic_type_desc t_desc =
131
  if Types.is_bool_type t_desc then
132
    if !Options.cpp then "bool" else "_Bool"
133
  else if Types.is_int_type t_desc then !Options.int_type
134
  else if Types.is_real_type t_desc then
135
    if !Options.mpfr then Mpfr.mpfr_t else !Options.real_type
136
  else
137
    assert false (* Not a basic C type. Do not handle arrays or pointers *)
139 138

  
140
let pp_basic_c_type fmt t = fprintf fmt "%s" (pp_c_basic_type_desc (Types.repr t).Types.tdesc)
139
let pp_basic_c_type ?(var_opt=None) fmt t =
140
  match var_opt with
141
  | Some v when Machine_types.is_exportable v ->
142
     Machine_types.pp_c_var_type fmt v
143
  | _ ->
144
     fprintf fmt "%s" (pp_c_basic_type_desc t)
141 145

  
142
let pp_c_type var fmt t =
146
let pp_c_type ?(var_opt=None) var_id fmt t =
143 147
  let rec aux t pp_suffix =
144
    match (Types.repr t).Types.tdesc with
145
    | Types.Tclock t'       -> aux t' pp_suffix
146
    | Types.Tbool | Types.Tint | Types.Treal
147
                            -> fprintf fmt "%a %s%a" pp_basic_c_type t var pp_suffix ()
148
    | Types.Tarray (d, t')  ->
149
      let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
150
      aux t' pp_suffix'
151
    | Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix
152
    | Types.Tconst ty       -> fprintf fmt "%s %s" ty var
153
    | Types.Tarrow (_, _)   -> fprintf fmt "void (*%s)()" var
154
    | _                     -> eprintf "internal error: C_backend_common.pp_c_type %a@." Types.print_ty t; assert false
148
    if is_basic_c_type  t then
149
       fprintf fmt "%a %s%a"
150
	 (pp_basic_c_type ~var_opt) t
151
	 var_id
152
	 pp_suffix ()
153
    else
154
      match (Types.repr t).Types.tdesc with
155
      | Types.Tclock t'       -> aux t' pp_suffix
156
      | Types.Tarray (d, t')  ->
157
	 let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
158
	 aux t' pp_suffix'
159
      | Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix
160
      | Types.Tconst ty       -> fprintf fmt "%s %s" ty var_id
161
      | Types.Tarrow (_, _)   -> fprintf fmt "void (*%s)()" var_id
162
      | _                     -> eprintf "internal error: C_backend_common.pp_c_type %a@." Types.print_ty t; assert false
155 163
  in aux t (fun fmt () -> ())
156 164
(*
157 165
let rec pp_c_initialize fmt t = 
......
241 249
*)
242 250
let pp_c_decl_input_var fmt id =
243 251
  if !Options.ansi && Types.is_address_type id.var_type
244
  then pp_c_type (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type)
245
  else pp_c_type id.var_id fmt id.var_type
252
  then pp_c_type ~var_opt:(Some id) (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type)
253
  else pp_c_type ~var_opt:(Some id) id.var_id fmt id.var_type
246 254

  
247 255
(* Declaration of an output variable:
248 256
   - if its type is scalar, then pass its address
......
252 260
*)
253 261
let pp_c_decl_output_var fmt id =
254 262
  if (not !Options.ansi) && Types.is_address_type id.var_type
255
  then pp_c_type                  id.var_id  fmt id.var_type
256
  else pp_c_type (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type)
263
  then pp_c_type  ~var_opt:(Some id)                  id.var_id  fmt id.var_type
264
  else pp_c_type  ~var_opt:(Some id) (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type)
257 265

  
258 266
(* Declaration of a local/mem variable:
259 267
   - if it's an array/matrix/etc, its size(s) should be
......
264 272
  if id.var_dec_const
265 273
  then
266 274
    Format.fprintf fmt "%a = %a"
267
      (pp_c_type id.var_id) id.var_type
275
      (pp_c_type  ~var_opt:(Some id) id.var_id) id.var_type
268 276
      (pp_c_val "" (pp_c_var_read m)) (get_const_assign m id)
269 277
  else
270 278
    Format.fprintf fmt "%a"
271
      (pp_c_type id.var_id) id.var_type
279
      (pp_c_type  ~var_opt:(Some id) id.var_id) id.var_type
272 280

  
273 281
let pp_c_decl_array_mem self fmt id =
274 282
  fprintf fmt "%a = (%a) (%s->_reg.%s)"
......
409 417
    | _ -> assert false
410 418
  in
411 419
  fprintf fmt "%a %s (@[<v>@[%a@]@,@])"
412
    pp_basic_c_type output.var_type
420
    (pp_basic_c_type ~var_opt:None) output.var_type
413 421
    name
414 422
    (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) inputs
415 423
    
......
650 658
    aux [] fmt (List.hd inputs).value_type
651 659
  end
652 660

  
653

  
654
(*** Common functions for main ***)
661
  (*** Common functions for main ***)
655 662

  
656 663
let print_put_var fmt file_suffix name var_type var_id =
657
  match (Types.unclock_type var_type).Types.tdesc with
658
  | Types.Tint -> fprintf fmt "_put_int(f_out%s, \"%s\", %s)" file_suffix name var_id
659
  | Types.Tbool -> fprintf fmt "_put_bool(f_out%s, \"%s\", %s)" file_suffix name var_id
660
  | Types.Treal when !Options.mpfr -> fprintf fmt "_put_double(f_out%s, \"%s\", mpfr_get_d(%s, %s), %i)" file_suffix name var_id (Mpfr.mpfr_rnd ()) !Options.print_prec_double
661
  | Types.Treal -> fprintf fmt "_put_double(f_out%s, \"%s\", %s, %i)" file_suffix name var_id !Options.print_prec_double
662
  | _ -> Format.eprintf "Impossible to print the _put_xx for type %a@.@?" Types.print_ty var_type; assert false
664
  let unclocked_t = Types.unclock_type var_type in
665
  if Types.is_int_type unclocked_t then
666
    fprintf fmt "_put_int(f_out%s, \"%s\", %s)" file_suffix name var_id
667
  else if Types.is_bool_type unclocked_t then
668
    fprintf fmt "_put_bool(f_out%s, \"%s\", %s)" file_suffix name var_id
669
  else if Types.is_real_type unclocked_t then
670
    if !Options.mpfr then
671
      fprintf fmt "_put_double(f_out%s, \"%s\", mpfr_get_d(%s, %s), %i)" file_suffix name var_id (Mpfr.mpfr_rnd ()) !Options.print_prec_double
672
    else
673
      fprintf fmt "_put_double(f_out%s, \"%s\", %s, %i)" file_suffix name var_id !Options.print_prec_double
674
  else
675
    (Format.eprintf "Impossible to print the _put_xx for type %a@.@?" Types.print_ty var_type; assert false)
676

  
677
      
678
let print_get_inputs fmt m =
679
  let pi fmt (id, v', v) =
680

  
681
    let unclocked_t = Types.unclock_type v.var_type in
682
    if Types.is_int_type unclocked_t then
683
      fprintf fmt "%s = _get_int(f_in%i, \"%s\")" v.var_id id v'.var_id
684
    else if Types.is_bool_type unclocked_t then
685
      fprintf fmt "%s = _get_bool(f_in%i, \"%s\")" v.var_id id v'.var_id
686
    else if Types.is_real_type unclocked_t then
687
      if !Options.mpfr then
688
	fprintf fmt "mpfr_set_d(%s, _get_double(f_in%i, \"%s\"), %i)" v.var_id id v'.var_id (Mpfr.mpfr_prec ())
689
      else
690
	fprintf fmt "%s = _get_double(f_in%i, \"%s\")" v.var_id id v'.var_id
691
    else
692
      begin
693
	Global.main_node := !Options.main_node;
694
	Format.eprintf "Code generation error: %a%a@."
695
	  Error.pp_error_msg Error.Main_wrong_kind
696
	  Location.pp_loc v'.var_loc;
697
	raise (Error (v'.var_loc, Error.Main_wrong_kind))
698
      end
699
  in
700
  Utils.List.iteri2 (fun idx v' v ->
701
    fprintf fmt "@ %a;" pi ((idx+1), v', v);
702
  ) m.mname.node_inputs m.mstep.step_inputs
703

  
663 704

  
664 705
(* Local Variables: *)
665 706
(* compile-command:"make -C ../../.." *)
src/backends/C/c_backend_header.ml
35 35

  
36 36
let print_import_standard fmt =
37 37
  begin
38
    (* if Machine_types.has_machine_type () then *)
39
    (*   begin *)
40
	fprintf fmt "#include <stdint.h>@.";
41
      (* end; *)
38 42
    if !Options.mpfr then
39 43
      begin
40 44
	fprintf fmt "#include <mpfr.h>@."
41 45
      end;
42
  if !Options.cpp then
43
    fprintf fmt "#include \"%s/arrow.hpp\"@.@." arrow_top_decl.top_decl_owner 
44
  else
45
    fprintf fmt "#include \"%s/arrow.h\"@.@." arrow_top_decl.top_decl_owner 
46

  
46
    if !Options.cpp then
47
      fprintf fmt "#include \"%s/arrow.hpp\"@.@." arrow_top_decl.top_decl_owner 
48
    else
49
      fprintf fmt "#include \"%s/arrow.h\"@.@." arrow_top_decl.top_decl_owner 
50
	
47 51
  end
48 52

  
49 53
let rec print_static_val pp_var fmt v =
src/backends/C/c_backend_main.ml
31 31
(*                         Main related functions                                           *)
32 32
(********************************************************************************************)
33 33

  
34
let print_get_inputs fmt m =
35
  let pi fmt (id, v', v) =
36
  match (Types.unclock_type v.var_type).Types.tdesc with
37
    | Types.Tint -> fprintf fmt "%s = _get_int(f_in%i, \"%s\")" v.var_id id v'.var_id
38
    | Types.Tbool -> fprintf fmt "%s = _get_bool(f_in%i, \"%s\")" v.var_id id v'.var_id
39
    | Types.Treal when !Options.mpfr -> fprintf fmt "mpfr_set_d(%s, _get_double(f_in%i, \"%s\"), %i)" v.var_id id v'.var_id (Mpfr.mpfr_prec ())
40
    | Types.Treal -> fprintf fmt "%s = _get_double(f_in%i, \"%s\")" v.var_id id v'.var_id
41
    | _ ->
42
      begin
43
	Global.main_node := !Options.main_node;
44
	Format.eprintf "Code generation error: %a%a@."
45
	  Error.pp_error_msg Error.Main_wrong_kind
46
	  Location.pp_loc v'.var_loc;
47
	raise (Error (v'.var_loc, Error.Main_wrong_kind))
48
      end
49
  in
50
  List.iteri2 (fun idx v' v ->
51
    fprintf fmt "@ %a;" pi ((idx+1), v', v);
52
  ) m.mname.node_inputs m.mstep.step_inputs
53 34

  
54 35
let print_put_outputs fmt m = 
55 36
  let po fmt (id, o', o) =
56 37
    let suff = string_of_int id in
57 38
    print_put_var fmt suff o'.var_id o.var_type o.var_id
58 39
  in
59
  Utils.List.iteri2 (fun idx v' v -> fprintf fmt "@ %a;" po ((idx+1), v', v)) m.mname.node_outputs m.mstep.step_outputs
40
  List.iteri2 (fun idx v' v -> fprintf fmt "@ %a;" po ((idx+1), v', v)) m.mname.node_outputs m.mstep.step_outputs
60 41

  
61 42
let print_main_inout_declaration basename fmt m =
62 43
  let mname = m.mname.node_id in
src/backends/C/c_backend_mauve.ml
43 43
let mauve_default_value v =
44 44
  (* let v_name = v.var_id in *)
45 45

  
46
  let v_type = (Types.repr v.var_type).Types.tdesc in
47
  match v_type with
48
  | Types.Tbool -> "false"
49
  | Types.Tint  -> "0"
50
  | Types.Treal -> "0.0"
51
  | _ -> assert false
46
  if Types.is_bool_type v.var_type then "false"
47
  else if Types.is_int_type v.var_type then "0"
48
  else if Types.is_real_type v.var_type then "0.0"
49
  else assert false
52 50

  
53 51
let print_mauve_default fmt mauve_machine v = 
54 52
  let v_name: string = v.var_id in
......
80 78
  List.iter
81 79
    (fun v ->
82 80
      let v_name = v.var_id in
83
      let v_type = pp_c_basic_type_desc (Types.repr v.var_type).Types.tdesc in
81
      let v_type = pp_c_basic_type_desc v.var_type in
84 82
      fprintf fmt "\tReadPort<%s> & port_%s = mk_readPort<%s>(\"%s\", " v_type v_name v_type v_name;
85 83
      print_mauve_default fmt mauve_machine v;
86 84
      fprintf fmt ");@.";
......
90 88
  List.iter
91 89
    (fun v ->
92 90
      let v_name = v.var_id in
93
      let v_type = pp_c_basic_type_desc (Types.repr v.var_type).Types.tdesc in
91
      let v_type = pp_c_basic_type_desc v.var_type in
94 92
      fprintf fmt "\tWritePort<%s> & port_%s = mk_writePort<%s>(\"%s\");@." v_type v_name v_type v_name;
95 93
    ) mauve_machine.mstep.step_outputs;
96 94

  
......
134 132
  List.iter
135 133
    (fun v ->
136 134
      let v_name = v.var_id in
137
      let v_type = pp_c_basic_type_desc (Types.repr v.var_type).Types.tdesc in
135
      let v_type = pp_c_basic_type_desc v.var_type in
138 136
      fprintf fmt "\t\t%s %s = port_%s.read();@." v_type v_name v_name;
139 137
    ) mauve_machine.mstep.step_inputs;
140 138
  List.iter
141 139
    (fun v ->
142 140
      let v_name = v.var_id in
143
      let v_type = pp_c_basic_type_desc (Types.repr v.var_type).Types.tdesc in
141
      let v_type = pp_c_basic_type_desc v.var_type in
144 142
      fprintf fmt "\t\t%s %s;@." v_type v_name;
145 143
    ) mauve_machine.mstep.step_outputs;
146 144
  print_mauve_step fmt node_name mauve_machine;
src/backends/C/c_backend_src.ml
608 608
  let constants = List.map const_of_top (get_consts prog) in
609 609
  fprintf fmt "@[<v 2>%a {@,static %s init = 0;@,@[<v 2>if (!init) { @,init = 1;@,%a%t%a@]@,}@,return;@]@,}@.@."
610 610
    print_global_init_prototype baseNAME
611
    (pp_c_basic_type_desc Types.Tbool)
611
    (pp_c_basic_type_desc Type_predef.type_bool)
612 612
    (* constants *) 
613 613
    (Utils.fprintf_list ~sep:"@," (pp_const_initialize (pp_c_var_read Machine_code.empty_machine))) constants
614 614
    (Utils.pp_final_char_if_non_empty "@," dependencies)
......
620 620
  let constants = List.map const_of_top (get_consts prog) in
621 621
  fprintf fmt "@[<v 2>%a {@,static %s clear = 0;@,@[<v 2>if (!clear) { @,clear = 1;@,%a%t%a@]@,}@,return;@]@,}@.@."
622 622
    print_global_clear_prototype baseNAME
623
    (pp_c_basic_type_desc Types.Tbool)
623
    (pp_c_basic_type_desc Type_predef.type_bool)
624 624
    (* constants *) 
625 625
    (Utils.fprintf_list ~sep:"@," (pp_const_clear (pp_c_var_read Machine_code.empty_machine))) constants
626 626
    (Utils.pp_final_char_if_non_empty "@," dependencies)
......
666 666
let print_import_standard source_fmt =
667 667
  begin
668 668
    fprintf source_fmt "#include <assert.h>@.";
669
    if Machine_types.has_machine_type () then
670
      begin
671
	fprintf source_fmt "#include <stdint.h>@."
672
      end;
669 673
    if not !Options.static_mem then
670 674
      begin
671 675
	fprintf source_fmt "#include <stdlib.h>@.";
src/backends/EMF/EMF_backend.ml
197 197
	     (reset_name f,
198 198
	      Corelang.mktyp loc Tydec_bool, Corelang.mkclock loc Ckdec_any,
199 199
	      false,
200
	      None,
200 201
	      None) 
201 202
	 in
202 203
	 VSet.add reset_var args_vars
......
365 366
    fprintf fmt "%a" pp_content i;
366 367
    fprintf fmt "@]@]@ }"
367 368
and pp_emf_instrs m fmt instrs = fprintf_list ~sep:",@ " (pp_emf_instr m) fmt instrs
368
       
369

  
370
let pp_emf_annot cpt fmt (key, ee) =
371
  let _ =
372
    fprintf fmt "\"ann%i\": { @[<hov 0>\"key\": [%a],@ \"eexpr\": %a@] }"
373
      !cpt
374
      (fprintf_list ~sep:"," (fun fmt s -> fprintf fmt "\"%s\"" s)) key
375
      pp_emf_eexpr ee
376
  in
377
  incr cpt
378
  
379
let pp_emf_annots cpt fmt annots = fprintf_list ~sep:",@ " (pp_emf_annot cpt) fmt annots.annots
380
let pp_emf_annots_list cpt fmt annots_list = fprintf_list ~sep:",@ " (pp_emf_annots cpt) fmt annots_list
369 381
let pp_machine fmt m =
370 382
  let instrs = (*merge_branches*) m.mstep.step_instrs in
371 383
  try
372 384
    fprintf fmt "@[<v 2>\"%a\": {@ "
373 385
       print_protect (fun fmt -> pp_print_string fmt m.mname.node_id);
374
    fprintf fmt "\"kind\": %t,@ \"inputs\": [%a],@ \"outputs\": [%a],@ \"locals\": [%a],@ "
386
    fprintf fmt "\"kind\": %t,@ "
375 387
      (fun fmt -> if not ( snd (get_stateless_status m) )
376 388
	then fprintf fmt "\"stateful\""
377
	else fprintf fmt "\"stateless\"")
378
      pp_emf_vars_decl m.mstep.step_inputs
379
      pp_emf_vars_decl m.mstep.step_outputs
380
      pp_emf_vars_decl m.mstep.step_locals
381
    ;
389
	else fprintf fmt "\"stateless\"");
390
    fprintf fmt "\"inputs\": [%a],@ "
391
      pp_emf_vars_decl m.mstep.step_inputs;
392
    fprintf fmt "\"outputs\": [%a],@ "
393
      pp_emf_vars_decl m.mstep.step_outputs;
394
    fprintf fmt "\"locals\": [%a],@ "
395
      pp_emf_vars_decl m.mstep.step_locals;
396
    fprintf fmt "\"mems\": [%a],@ "
397
      pp_emf_vars_decl m.mmemory;
398
    
382 399
    fprintf fmt "\"original_name\": \"%s\",@ " m.mname.node_id;
383
    fprintf fmt "\"instrs\": {@[<v 0> %a@]@ }"
400
    fprintf fmt "\"instrs\": {@[<v 0> %a@]@ },@ "
384 401
      (pp_emf_instrs m) instrs;
402
    fprintf fmt "\"annots\": {@[<v 0> %a@]@ }" (pp_emf_annots_list (ref 0)) m.mannot;
385 403
    fprintf fmt "@]@ }"
386 404
  with Unhandled msg -> (
387 405
    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
src/backends/EMF/EMF_common.ml
86 86
      
87 87
   
88 88
     
89
let pp_cst_type c infered_typ fmt =
89
let pp_cst_type fmt c (*infered_typ*) =
90 90
  match c with
91 91
  | Const_tag t ->
92 92
     let typ = (Corelang.typedef_of_top (Hashtbl.find Corelang.tag_table t)) in
......
94 94
       fprintf fmt "bool"
95 95
     else
96 96
       pp_tag_type fmt typ
97
  | Const_int _ -> fprintf fmt "%s" !Options.int_type
98
  | Const_real _ -> fprintf fmt "%s" !Options.real_type
99
  | _ -> Format.eprintf "cst: %a@." Printers.pp_const c; assert false
97
  | Const_int _ -> fprintf fmt "int" (*!Options.int_type*)
98
  | Const_real _ -> fprintf fmt "real" (*!Options.real_type*)
99
  | Const_string _ -> fprintf fmt "string" 
100
  | _ -> eprintf "cst: %a@." Printers.pp_const c; assert false
100 101

  
101 102
let rec pp_infered_type fmt t =
102 103
  let open Types in
104
  if is_bool_type t  then fprintf fmt "bool" else
105
  if is_int_type t then fprintf fmt "int" else (* !Options.int_type *)
106
  if is_real_type t then fprintf fmt "real" else (* !Options.real_type *)
103 107
  match t.tdesc with
104
  | Tint ->
105
     fprintf fmt "%s" !Options.int_type
106
  | Treal ->
107
     fprintf fmt "%s" !Options.real_type
108
  | Tbool ->
109
     fprintf fmt "bool"
110 108
  | Tclock t ->
111 109
     pp_infered_type fmt t
112 110
  | Tstatic (_, t) ->
......
119 117
     pp_tag_type fmt typ
120 118
   | Tlink ty -> 
121 119
       pp_infered_type fmt ty 
122
  | _ -> Format.eprintf "unhandled type: %a@." Types.print_node_ty t; assert false
120
   | _ -> eprintf "unhandled type: %a@." Types.print_node_ty t; assert false
121
     
123 122
let rec pp_concrete_type dec_t infered_t fmt =
124 123
  match dec_t with
125
  | Tydec_int -> fprintf fmt "%s" !Options.int_type
126
  | Tydec_real -> fprintf fmt "%s" !Options.real_type
124
  | Tydec_int -> fprintf fmt "int" (* !Options.int_type *)
125
  | Tydec_real -> fprintf fmt "real" (* !Options.real_type *)
127 126
  (* TODO we could add more concrete types here if they were available in
128 127
     dec_t *)
129 128
  | Tydec_bool -> fprintf fmt "bool"
......
134 133
    pp_tag_type fmt typ
135 134
  )
136 135
  | Tydec_any -> pp_infered_type fmt infered_t 
137
  | _ -> Format.eprintf
136
  | _ -> eprintf
138 137
     "unhandled construct in type printing for EMF backend: %a@."
139 138
     Printers.pp_var_type_dec_desc dec_t; raise (Failure "var")
140 139
       
141 140

  
142
let pp_cst_type fmt v =
141
(*let pp_cst_type fmt v =
143 142
  match v.value_desc with
144 143
  | Cst c-> pp_cst_type c v.value_type fmt (* constants do not have declared type (yet) *)
145 144
  | _ -> assert false
146
     
145
*)
146
       
147 147
let pp_var_type fmt v =
148 148
  try
149
  pp_concrete_type v.var_dec_type.ty_dec_desc v.var_type fmt
150
  with Failure _ -> Format.eprintf "failed var: %a@." Printers.pp_var v; assert false
149
    if Machine_types.is_specified v then
150
      Machine_types.pp_var_type fmt v
151
    else
152
      pp_concrete_type v.var_dec_type.ty_dec_desc v.var_type fmt
153
  with Failure _ -> eprintf "failed var: %a@." Printers.pp_var v; assert false
154
    
151 155
(******** Other print functions *)
152 156
    
153 157
let pp_emf_var_decl fmt v =
......
171 175
  else
172 176
    let const_list = match typ.tydef_desc with Tydec_enum tl -> tl | _ -> assert false in
173 177
    fprintf fmt "%i" (get_idx t const_list)
174
     
175
let pp_emf_cst_or_var fmt v =
176
  match v.value_desc with
177
  | Cst ((Const_tag t) as c)->
178

  
179
let pp_emf_cst fmt c =
180
  match c with
181
  | Const_tag t->
178 182
     let typ = (Corelang.typedef_of_top (Hashtbl.find Corelang.tag_table t)) in
179 183
     if typ.tydef_id = "bool" then (
180 184
       fprintf fmt "{@[\"type\": \"constant\",@ ";
181 185
       fprintf fmt"\"value\": \"%a\",@ "
182 186
	 Printers.pp_const c;
183
       fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type v;
187
       fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type c;
184 188
       fprintf fmt "@]}"
185 189
     )
186 190
     else (
......
188 192
	 pp_tag_id t;
189 193
       fprintf fmt "\"origin_type\": \"%s\",@ \"origin_value\": \"%s\",@ "
190 194
	 typ.tydef_id t;
191
       fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type v;
195
       fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type c;
192 196
       fprintf fmt "@]}"
193 197
     )
194
  | Cst c -> (
198
  | Const_string s ->
199
    fprintf fmt "{@[\"type\": \"constant\",@ \"value\": \"%s\",@ " s;
200
    fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type c;
201
    fprintf fmt "@]}"
202
     
203
  | _ -> (
195 204
    fprintf fmt "{@[\"type\": \"constant\",@ \"value\": \"%a\",@ "
196 205
      Printers.pp_const c;
197
    fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type v;
206
    fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type c;
198 207
    fprintf fmt "@]}"
199 208
  )
209
  
210
  
211
let pp_emf_cst_or_var fmt v =
212
  match v.value_desc with
213
  | Cst c -> pp_emf_cst fmt c
200 214
  | LocalVar v
201 215
  | StateVar v -> (
202 216
    fprintf fmt "{@[\"type\": \"variable\",@ \"value\": \"%a\",@ "
......
205 219
    fprintf fmt "\"datatype\": \"%a\"@ " pp_var_type v;
206 220
    fprintf fmt "@]}"
207 221
  )
208
  | _ -> Format.eprintf "Not of cst or var: %a@." Machine_code.pp_val v ; assert false (* Invalid argument *)
222
  | _ -> eprintf "Not of cst or var: %a@." Machine_code.pp_val v ; assert false (* Invalid argument *)
209 223

  
210 224

  
211 225
let pp_emf_cst_or_var_list =
212 226
  Utils.fprintf_list ~sep:",@ " pp_emf_cst_or_var
213 227

  
228
(* Printer lustre expr and eexpr *)
229
    
230
let rec pp_emf_expr fmt e =
231
  match e.expr_desc with
232
  | Expr_const c -> pp_emf_cst fmt c
233
  | Expr_ident id ->
234
     fprintf fmt "{@[\"type\": \"variable\",@ \"value\": \"%a\",@ "
235
       print_protect (fun fmt -> pp_print_string fmt id);
236
    fprintf fmt "\"datatype\": \"%t\"@ "
237
      (pp_concrete_type
238
	 Tydec_any (* don't know much about that time since it was not
239
		      declared. That may not work with clock constants *)
240
	 e.expr_type
241
      );
242
    fprintf fmt "@]}"
243

  
244
  | Expr_tuple el ->
245
     fprintf fmt "[@[<hov 0>%a@ @]]"
246
       (Utils.fprintf_list ~sep:",@ " pp_emf_expr) el
247
  | _ -> (
248
    Log.report ~level:2
249
      (fun fmt ->
250
	fprintf fmt "Warning: unhandled expression %a in annotation.@ "
251
	  Printers.pp_expr e;
252
	fprintf fmt "Will not be produced in the experted JSON EMF"
253
      );    
254
    fprintf fmt "\"unhandled construct, complain to Ploc\""
255
  )
256
(* Remaining constructs *)  
257
(* | Expr_ite   of expr * expr * expr *)
258
(* | Expr_arrow of expr * expr *)
259
(* | Expr_fby of expr * expr *)
260
(* | Expr_array of expr list *)
261
(* | Expr_access of expr * Dimension.dim_expr *)
262
(* | Expr_power of expr * Dimension.dim_expr *)
263
(* | Expr_pre of expr *)
264
(* | Expr_when of expr * ident * label *)
265
(* | Expr_merge of ident * (label * expr) list *)
266
(* | Expr_appl of call_t *)
267
     
214 268

  
269
let pp_emf_eexpr fmt ee =
270
  fprintf fmt "{@[<hov 0>\"quantifiers\": \"%a\",@ \"qfexpr\": @[%a@]@] }"
271
    (Utils.fprintf_list ~sep:"; " Printers.pp_quantifiers) ee.eexpr_quantifiers
272
    pp_emf_expr ee.eexpr_qfexpr
273
    
274
    
215 275
(* Local Variables: *)
216 276
(* compile-command: "make -C ../.." *)
217 277
(* End: *)
src/backends/Horn/horn_backend_common.ml
19 19
let pp_machine_stateless_name fmt id = fprintf fmt "%s_fun" id
20 20

  
21 21
let rec pp_type fmt t =
22
  if Types.is_bool_type t  then fprintf fmt "Bool" else
23
  if Types.is_int_type t then fprintf fmt "Int" else 
24
  if Types.is_real_type t then fprintf fmt "Real" else 
22 25
  match (Types.repr t).Types.tdesc with
23
  | Types.Tbool           -> fprintf fmt "Bool"
24
  | Types.Tint            -> fprintf fmt "Int"
25
  | Types.Treal           -> fprintf fmt "Real"
26 26
  | Types.Tconst ty       -> pp_print_string fmt ty
27 27
  | Types.Tclock t        -> pp_type fmt t
28 28
  | Types.Tarray(dim,ty)   -> fprintf fmt "(Array Int "; pp_type fmt ty; fprintf fmt ")"
src/backends/Horn/horn_backend_printers.ml
96 96
   for the type integer (arrays).
97 97
*)
98 98
let rec pp_default_val fmt t =
99
  let t = Types.dynamic_type t in
100
  if Types.is_bool_type t  then fprintf fmt "true" else
101
  if Types.is_int_type t then fprintf fmt "0" else 
102
  if Types.is_real_type t then fprintf fmt "0" else 
99 103
  match (Types.dynamic_type t).Types.tdesc with
100
  | Types.Tint -> fprintf fmt "0"
101
  | Types.Treal -> fprintf fmt "0"
102
  | Types.Tbool -> fprintf fmt "true"
103 104
  | Types.Tarray(dim, l) -> (* TODO PL: this strange code has to be (heavily) checked *)
104 105
     let valt = Types.array_element_type t in
105 106
     fprintf fmt "((as const (Array Int %a)) %a)"
src/compiler_common.ml
262 262
  else ()
263 263

  
264 264

  
265

  
265
let update_vdecl_parents_prog prog =
266
  let update_vdecl_parents parent v =
267
    v.var_parent_nodeid <- Some parent
268
  in
269
  List.iter (
270
    fun top -> match top.top_decl_desc with
271
    | Node nd ->
272
       List.iter
273
	 (update_vdecl_parents nd.node_id)
274
	 (nd.node_inputs @ nd.node_outputs @ nd.node_locals )  
275
    | ImportedNode ind -> 
276
       List.iter
277
	 (update_vdecl_parents ind.nodei_id)
278
	 (ind.nodei_inputs @ ind.nodei_outputs )  
279
    | _ -> ()
280
  ) prog
src/compiler_stages.ml
48 48

  
49 49
(* From prog to prog *)
50 50
let stage1 prog dirname basename =
51
  (* Updating parent node information for variables *)
52
  Compiler_common.update_vdecl_parents_prog prog;
53

  
51 54
  (* Removing automata *)
52 55
  let prog = expand_automata prog in
53 56
  Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@,  @[<v 2>@,%a@]@ " Printers.pp_prog prog);
......
83 86
  (* Clock calculus *)
84 87
  let computed_clocks_env = clock_decls clock_env prog in
85 88

  
89
  (* Registering and checking machine types *)
90
  Machine_types.load prog;
91
  
92

  
86 93
  (* Generating a .lusi header file only *)
87 94
  if !Options.lusi then
88 95
    (* We stop here the processing and produce the current prog. It will be
......
131 138
  Typing.uneval_prog_generics prog;
132 139
  Clock_calculus.uneval_prog_generics prog;
133 140

  
141

  
134 142
  if !Options.global_inline && !Options.main_node <> "" && !Options.witnesses then
135 143
    begin
136 144
      let orig = Corelang.copy_prog orig in
......
160 168
    else
161 169
      prog
162 170
  in
163
  
171

  
172

  
173
  (* (\* Registering and checking machine types *\) *)
174
  (* Machine_types.load prog; *)
175

  
164 176
  (* Normalization phase *)
165 177
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
166 178
  let prog = Normalization.normalize_prog ~backend:!Options.output prog in
......
187 199
      Access.check_prog prog;
188 200
    end;
189 201

  
202
  
190 203
  let prog = SortProg.sort_nodes_locals prog in
191 204
  
192 205
  prog, dependencies
206

  
207

  
208
    (* from source to machine code, with optimization *)
209
let stage2 prog =    
210
  (* Computation of node equation scheduling. It also breaks dependency cycles
211
     and warns about unused input or memory variables *)
212
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. @[<v 2>scheduling@ ");
213
  let prog, node_schs =
214
    try 
215
      Scheduling.schedule_prog prog
216
    with Causality.Error _ -> (* Error is not kept. It is recomputed in a more
217
				 systemtic way in AlgebraicLoop module *)
218
      AlgebraicLoop.analyze prog
219
  in
220
  Log.report ~level:1 (fun fmt -> fprintf fmt "%a"              Scheduling.pp_warning_unused node_schs);
221
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs);
222
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);
223
  Log.report ~level:5 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_dep_graph node_schs);
224
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
225
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
226

  
227
  (* TODO Salsa optimize prog: 
228
     - emits warning for programs with pre inside expressions
229
     - make sure each node arguments and memory is bounded by a local annotation
230
     - introduce fresh local variables for each real pure subexpression
231
  *)
232
  (* DFS with modular code generation *)
233
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,");
234
  let machine_code = Machine_code.translate_prog prog node_schs in
235

  
236
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (unoptimized):@ %a@ "Machine_code.pp_machines machine_code);
237

  
238
  (* Optimize machine code *)
239
  Optimize_machine.optimize prog node_schs machine_code
240

  
241

  
242
(* printing code *)
243
let stage3 prog machine_code dependencies basename =
244
  let basename    =  Filename.basename basename in
245
  match !Options.output with
246
    "C" -> 
247
      begin
248
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
249
	C_backend.translate_to_c
250
	  (* alloc_header_file source_lib_file source_main_file makefile_file *)
251
	  basename prog machine_code dependencies
252
      end
253
  | "java" ->
254
     begin
255
       (Format.eprintf "internal error: sorry, but not yet supported !"; assert false)
256
     (*let source_file = basename ^ ".java" in
257
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
258
       let source_out = open_out source_file in
259
       let source_fmt = formatter_of_out_channel source_out in
260
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
261
       Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
262
     end
263
  | "horn" ->
264
     begin
265
       let destname = !Options.dest_dir ^ "/" ^ basename in
266
       let source_file = destname ^ ".smt2" in (* Could be changed *)
267
       let source_out = open_out source_file in
268
       let fmt = formatter_of_out_channel source_out in
269
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
270
       Horn_backend.translate fmt basename prog (Machine_code.arrow_machine::machine_code);
271
       (* Tracability file if option is activated *)
272
       if !Options.traces then (
273
	 let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
274
	 let traces_out = open_out traces_file in
275
	 let fmt = formatter_of_out_channel traces_out in
276
         Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
277
	 Horn_backend_traces.traces_file fmt basename prog machine_code;
278
       )
279
     end
280
  | "lustre" ->
281
     begin
282
       let destname = !Options.dest_dir ^ "/" ^ basename in
283
       let source_file = destname ^ ".lustrec.lus" in (* Could be changed *)
284
       let source_out = open_out source_file in
285
       let fmt = formatter_of_out_channel source_out in
286
       Printers.pp_prog fmt prog;
287
       Format.fprintf fmt "@.@?";
288
       (*	Lustre_backend.translate fmt basename normalized_prog machine_code *)
289
       ()
290
     end
291
  | "emf" ->
292
     begin
293
       let destname = !Options.dest_dir ^ "/" ^ basename in
294
       let source_file = destname ^ ".emf" in (* Could be changed *)
295
       let source_out = open_out source_file in
296
       let fmt = formatter_of_out_channel source_out in
297
       EMF_backend.translate fmt basename prog machine_code;
298
       ()
299
     end
300

  
301
  | _ -> assert false
src/corelang.ml
41 41
let mkclock loc d =
42 42
  { ck_dec_desc = d; ck_dec_loc = loc }
43 43

  
44
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value) =
44
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value, parentid) =
45 45
  assert (value = None || is_const);
46 46
  { var_id = id;
47 47
    var_orig = orig;
......
49 49
    var_dec_clock = ck_dec;
50 50
    var_dec_const = is_const;
51 51
    var_dec_value = value;
52
    var_parent_nodeid = parentid;
52 53
    var_type = Types.new_var ();
53 54
    var_clock = Clocks.new_var true;
54 55
    var_loc = loc }
......
62 63
    expr_annot = None;
63 64
    expr_loc = loc }
64 65

  
65
let var_decl_of_const c =
66
let var_decl_of_const ?(parentid=None) c =
66 67
  { var_id = c.const_id;
67 68
    var_orig = true;
68 69
    var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
69 70
    var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
70 71
    var_dec_const = true;
71 72
    var_dec_value = None;
73
    var_parent_nodeid = parentid;
72 74
    var_type = c.const_type;
73 75
    var_clock = Clocks.new_var false;
74 76
    var_loc = c.const_loc }
......
626 628
  nodei_outputs = nd.node_outputs;
627 629
  nodei_stateless = nd.node_dec_stateless;
628 630
  nodei_spec = nd.node_spec;
631
  (* nodei_annot = nd.node_annot; *)
629 632
  nodei_prototype = None;
630 633
  nodei_in_lib = [];
631 634
 }
......
901 904
  List.map
902 905
    (fun _ -> incr cpt;
903 906
              let name = sprintf "_var_%d" !cpt in
904
              mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false, None))
907
              mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false, None, None))
905 908
    (Types.type_list_of_type ty)
906 909

  
907 910
let mk_internal_node id =
......
920 923
	nodei_outputs = vdecls_of_typ_ck cpt tout;
921 924
	nodei_stateless = Types.get_static_value ty <> None;
922 925
	nodei_spec = spec;
926
	(* nodei_annot = []; *)
923 927
	nodei_prototype = None;
924 928
       	nodei_in_lib = [];
925 929
       })
......
1104 1108

  
1105 1109

  
1106 1110
let copy_var_decl vdecl =
1107
  mkvar_decl vdecl.var_loc ~orig:vdecl.var_orig (vdecl.var_id, vdecl.var_dec_type, vdecl.var_dec_clock, vdecl.var_dec_const, vdecl.var_dec_value)
1111
  mkvar_decl vdecl.var_loc ~orig:vdecl.var_orig (vdecl.var_id, vdecl.var_dec_type, vdecl.var_dec_clock, vdecl.var_dec_const, vdecl.var_dec_value, vdecl.var_parent_nodeid)
1108 1112

  
1109 1113
let copy_const cdecl =
1110 1114
  { cdecl with const_type = Types.new_var () }
src/corelang.mli
20 20

  
21 21
val mktyp: Location.t -> type_dec_desc -> type_dec
22 22
val mkclock: Location.t -> clock_dec_desc -> clock_dec
23
val mkvar_decl: Location.t -> ?orig:bool -> ident * type_dec * clock_dec * bool (* is const *) * expr option (* value *) -> var_decl
24

  
25
val var_decl_of_const: const_desc -> var_decl
23
val mkvar_decl: Location.t -> ?orig:bool ->
24
  ident *
25
    type_dec *
26
    clock_dec *
27
    bool (* is const *) *
28
    expr option (* value *) *
29
    string option (* parent id *)
30
  -> var_decl
31

  
32
val var_decl_of_const: ?parentid:LustreSpec.ident option -> const_desc -> var_decl
26 33
val mkexpr: Location.t ->  expr_desc -> expr
27 34
val mkeq: Location.t -> ident list * expr -> eq
28 35
val mkassert: Location.t -> expr -> assert_t
src/env.ml
27 27
  IMap.mem ident env
28 28

  
29 29
let iter env f = IMap.iter f env
30
let fold = IMap.fold
30 31

  
31 32
(* Merges x and y. In case of conflicting definitions,
32 33
   overwrites definitions in x by definitions in y *)
src/features/machine_types/machine_types.ml
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

  
src/global.ml
1
module Types = Types.Main
2

  
1 3
let type_env : (Types.type_expr Env.t) ref = ref Env.initial
2 4
let clock_env : (Clocks.clock_expr Env.t) ref = ref Env.initial
3 5
let basename = ref ""
src/inliner.ml
137 137
	 { v.var_dec_type  with ty_dec_desc = Corelang.rename_static rename_static v.var_dec_type.ty_dec_desc },
138 138
	 { v.var_dec_clock with ck_dec_desc = Corelang.rename_carrier rename_carrier v.var_dec_clock.ck_dec_desc },
139 139
	 v.var_dec_const,
140
	 Utils.option_map (rename_expr (fun x -> x) rename) v.var_dec_value) in
140
	 Utils.option_map (rename_expr (fun x -> x) rename) v.var_dec_value,
141
	 v.var_parent_nodeid (* we keep the original parent name *)
142
	) in
141 143
    begin
142 144
      (*
143 145
	(try
......
358 360
       {ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
359 361
       {ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
360 362
       false,
361
       None)
363
       None,
364
       None
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff