Revision 66359a5e
Added by Pierre-Loïc Garoche about 7 years ago
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 |
Also available in: Unified diff
[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