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