1
|
(********************************************************************)
|
2
|
(* *)
|
3
|
(* The LustreC compiler toolset / The LustreC Development Team *)
|
4
|
(* Copyright 2012 - -- ONERA - CNRS - INPT - ISAE-SUPAERO *)
|
5
|
(* *)
|
6
|
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
|
7
|
(* under the terms of the GNU Lesser General Public License *)
|
8
|
(* version 2.1. *)
|
9
|
(* *)
|
10
|
(********************************************************************)
|
11
|
|
12
|
open Format
|
13
|
open Machine_code_types
|
14
|
open Misc_lustre_function
|
15
|
open Ada_backend_common
|
16
|
|
17
|
let indent_size = 2
|
18
|
|
19
|
(** Log at level 2 a string message with some indentation. @param indent the
|
20
|
indentation level @param info the message **)
|
21
|
let log_str_level_two indent info =
|
22
|
let str_indent = String.make (indent * indent_size) ' ' in
|
23
|
let pp_message fmt = fprintf fmt "%s.. %s@." str_indent info in
|
24
|
Log.report ~level:2 pp_message;
|
25
|
Format.pp_print_flush Format.err_formatter ()
|
26
|
|
27
|
(** Write a new file with formatter @param destname folder where the file shoudl
|
28
|
be created @param pp_filename function printing the filename @param pp_file
|
29
|
function wich pretty print the file @param arg will be given to pp_filename
|
30
|
and pp_file **)
|
31
|
let write_file destname pp_filename pp_file arg =
|
32
|
let path = asprintf "%s%a" destname pp_filename arg in
|
33
|
let out = open_out path in
|
34
|
let fmt = formatter_of_out_channel out in
|
35
|
log_str_level_two 2 ("generating " ^ path);
|
36
|
pp_file fmt arg;
|
37
|
pp_print_flush fmt ();
|
38
|
close_out out
|
39
|
|
40
|
exception CheckFailed of string
|
41
|
(** Exception raised when a machine contains a feature not supported by the Ada
|
42
|
backend*)
|
43
|
|
44
|
(** Check that a machine match the requirement for an Ada compilation : - No
|
45
|
constants. @param machine the machine to test **)
|
46
|
let check machine =
|
47
|
match machine.mconst with
|
48
|
| [] ->
|
49
|
()
|
50
|
| _ ->
|
51
|
raise (CheckFailed "machine.mconst should be void")
|
52
|
|
53
|
let get_typed_submachines machines m =
|
54
|
let instances =
|
55
|
List.filter (fun (id, _) -> not (is_builtin_fun id)) m.mcalls
|
56
|
in
|
57
|
let submachines = List.map (get_machine machines) instances in
|
58
|
List.map2
|
59
|
(fun instance submachine ->
|
60
|
let ident = fst instance in
|
61
|
ident, (get_substitution m ident submachine, submachine))
|
62
|
instances submachines
|
63
|
|
64
|
let extract_contract machines m =
|
65
|
let rec find_submachine_from_ident ident = function
|
66
|
| [] ->
|
67
|
raise Not_found
|
68
|
| h :: _ when h.mname.node_id = ident ->
|
69
|
h
|
70
|
| _ :: t ->
|
71
|
find_submachine_from_ident ident t
|
72
|
in
|
73
|
let extract_ident eexpr =
|
74
|
match eexpr.Lustre_types.eexpr_qfexpr.expr_desc with
|
75
|
| Expr_ident ident ->
|
76
|
ident
|
77
|
| _ ->
|
78
|
assert false
|
79
|
(* | Expr_const cst -> assert false | Expr_tuple exprs -> assert false |
|
80
|
Expr_ite (expr1, expr2, expr3) -> assert false | Expr_arrow (expr1,
|
81
|
expr2) -> assert false | Expr_fby (expr1, expr2) -> assert false |
|
82
|
Expr_array exprs -> assert false | Expr_access (expr1, dim) -> assert
|
83
|
false | Expr_power (expr1, dim) -> assert false | Expr_pre expr -> assert
|
84
|
false | Expr_when (expr,ident,label) -> assert false | Expr_merge (ident,
|
85
|
l) -> assert false | Expr_appl call -> assert false *)
|
86
|
in
|
87
|
match m.mspec.mnode_spec with
|
88
|
| Some (NodeSpec ident) ->
|
89
|
let machine_spec = find_submachine_from_ident ident machines in
|
90
|
let guarantees =
|
91
|
match machine_spec.mspec.mnode_spec with
|
92
|
| Some (Contract contract) ->
|
93
|
assert (contract.consts = []);
|
94
|
assert (contract.locals = []);
|
95
|
assert (contract.stmts = []);
|
96
|
assert (contract.assume = []);
|
97
|
List.map extract_ident contract.guarantees
|
98
|
| _ ->
|
99
|
assert false
|
100
|
in
|
101
|
let opt_machine_spec =
|
102
|
match machine_spec.mstep.step_instrs with
|
103
|
| [] ->
|
104
|
None
|
105
|
| _ ->
|
106
|
Some machine_spec
|
107
|
in
|
108
|
opt_machine_spec, guarantees
|
109
|
| _ ->
|
110
|
None, []
|
111
|
|
112
|
(** Main function of the Ada backend. It calls all the subfunction creating all
|
113
|
the file and fill them with Ada code representing the machines list given.
|
114
|
@param basename name of the lustre file @param prog list of machines to
|
115
|
translate **)
|
116
|
let translate_to_ada basename machines =
|
117
|
(* let module Ads = Ada_backend_ads.Main in
|
118
|
* let module Adb = Ada_backend_adb.Main in
|
119
|
* let module Wrapper = Ada_backend_wrapper.Main in *)
|
120
|
let is_real_machine m =
|
121
|
match m.mspec.mnode_spec with Some (Contract _) -> false | _ -> true
|
122
|
in
|
123
|
|
124
|
let filtered_machines = List.filter is_real_machine machines in
|
125
|
|
126
|
let typed_submachines =
|
127
|
List.map (get_typed_submachines machines) filtered_machines
|
128
|
in
|
129
|
|
130
|
let contracts = List.map (extract_contract machines) filtered_machines in
|
131
|
|
132
|
let _machines = List.combine contracts filtered_machines in
|
133
|
|
134
|
let _machines = List.combine typed_submachines _machines in
|
135
|
|
136
|
let _pp_filename ext fmt (_, (_, machine)) =
|
137
|
pp_machine_filename ext fmt machine
|
138
|
in
|
139
|
|
140
|
(* Extract the main machine if there is one *)
|
141
|
let main_machine =
|
142
|
match !Options.main_node with
|
143
|
| "" ->
|
144
|
None
|
145
|
| main_node -> (
|
146
|
match Machine_code_common.get_machine_opt filtered_machines main_node with
|
147
|
| None ->
|
148
|
Format.eprintf "Ada Code generation error: %a@." Error.pp
|
149
|
Error.Main_not_found;
|
150
|
raise (Error.Error (Location.dummy, Error.Main_not_found))
|
151
|
| Some m ->
|
152
|
Some m)
|
153
|
in
|
154
|
|
155
|
let destname = !Options.dest_dir ^ "/" in
|
156
|
|
157
|
log_str_level_two 1 "Checking machines";
|
158
|
List.iter check machines;
|
159
|
|
160
|
log_str_level_two 1 "Generating ads";
|
161
|
List.iter (write_file destname (_pp_filename "ads") Ada_backend_ads.pp_file) _machines;
|
162
|
|
163
|
log_str_level_two 1 "Generating adb";
|
164
|
List.iter (write_file destname (_pp_filename "adb") Ada_backend_adb.pp_file) _machines;
|
165
|
|
166
|
(* If a main node is given we generate a main adb file and a project file *)
|
167
|
log_str_level_two 1 "Generating wrapper files";
|
168
|
(match main_machine with
|
169
|
| None ->
|
170
|
()
|
171
|
| Some machine ->
|
172
|
write_file destname pp_main_filename Ada_backend_wrapper.pp_main_adb
|
173
|
(*get_typed_submachines filtered_machines machine*)
|
174
|
machine;
|
175
|
write_file destname
|
176
|
(fun fmt _ -> Ada_backend_wrapper.pp_project_name (basename ^ "_exe") fmt)
|
177
|
(Ada_backend_wrapper.pp_project_file filtered_machines basename)
|
178
|
main_machine);
|
179
|
write_file destname Ada_backend_wrapper.pp_project_configuration_name
|
180
|
(fun fmt _ -> Ada_backend_wrapper.pp_project_configuration_file fmt)
|
181
|
basename;
|
182
|
write_file destname
|
183
|
(fun fmt _ -> Ada_backend_wrapper.pp_project_name (basename ^ "_lib") fmt)
|
184
|
(Ada_backend_wrapper.pp_project_file filtered_machines basename)
|
185
|
None
|
186
|
|
187
|
(* Local Variables: *)
|
188
|
(* compile-command:"make -C ../../.." *)
|
189
|
(* End: *)
|