lustrec / src / compiler_common.ml @ f4cba4b8
History | View | Annotate | Download (13.3 KB)
1 |
(********************************************************************) |
---|---|
2 |
(* *) |
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
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 Utils |
13 |
open Format |
14 |
open Lustre_types |
15 |
open Corelang |
16 |
|
17 |
let check_main () = |
18 |
if !Options.main_node = "" then |
19 |
begin |
20 |
eprintf "Code generation error: %a@." Error.pp_error_msg Error.No_main_specified; |
21 |
raise (Error (Location.dummy_loc, Error.No_main_specified)) |
22 |
end |
23 |
|
24 |
let create_dest_dir () = |
25 |
begin |
26 |
if not (Sys.file_exists !Options.dest_dir) then |
27 |
begin |
28 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. creating destination directory@ "); |
29 |
Unix.mkdir !Options.dest_dir (Unix.stat ".").Unix.st_perm |
30 |
end; |
31 |
if (Unix.stat !Options.dest_dir).Unix.st_kind <> Unix.S_DIR then |
32 |
begin |
33 |
eprintf "Failure: destination %s is not a directory.@.@." !Options.dest_dir; |
34 |
exit 1 |
35 |
end |
36 |
end |
37 |
|
38 |
(* Loading Lus/Lusi file and filling type tables with parsed |
39 |
functions/nodes *) |
40 |
let parse filename extension = |
41 |
Location.set_input filename; |
42 |
let f_in = open_in filename in |
43 |
let lexbuf = Lexing.from_channel f_in in |
44 |
Location.init lexbuf filename; |
45 |
(* Parsing *) |
46 |
let prog = |
47 |
try |
48 |
match extension with |
49 |
".lusi" -> |
50 |
Log.report ~level:1 |
51 |
(fun fmt -> fprintf fmt ".. parsing header file %s@ " filename); |
52 |
Parse.header Parser_lustre.header Lexer_lustre.token lexbuf |
53 |
| ".lus" -> |
54 |
Log.report ~level:1 |
55 |
(fun fmt -> fprintf fmt ".. parsing source file %s@ " filename); |
56 |
Parse.prog Parser_lustre.prog Lexer_lustre.token lexbuf |
57 |
| _ -> assert false |
58 |
with |
59 |
| (Parse.Error err) as exc -> |
60 |
Parse.report_error err; |
61 |
raise exc |
62 |
| Corelang.Error (loc, err) as exc -> ( |
63 |
eprintf "Parsing error: %a%a@." |
64 |
Error.pp_error_msg err |
65 |
Location.pp_loc loc; |
66 |
raise exc |
67 |
) |
68 |
in |
69 |
close_in f_in; |
70 |
prog |
71 |
|
72 |
|
73 |
let expand_automata decls = |
74 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. expanding automata@ "); |
75 |
try |
76 |
Automata.expand_decls decls |
77 |
with (Corelang.Error (loc, err)) as exc -> |
78 |
eprintf "Automata error: %a%a@." |
79 |
Error.pp_error_msg err |
80 |
Location.pp_loc loc; |
81 |
raise exc |
82 |
|
83 |
let check_stateless_decls decls = |
84 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking stateless/stateful status@ "); |
85 |
try |
86 |
Stateless.check_prog decls |
87 |
with (Stateless.Error (loc, err)) as exc -> |
88 |
eprintf "Stateless status error: %a%a@." |
89 |
Stateless.pp_error err |
90 |
Location.pp_loc loc; |
91 |
raise exc |
92 |
|
93 |
let force_stateful_decls decls = |
94 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. forcing stateful status@ "); |
95 |
try |
96 |
Stateless.force_prog decls |
97 |
with (Stateless.Error (loc, err)) as exc -> |
98 |
eprintf "Stateless status error: %a%a@." |
99 |
Stateless.pp_error err |
100 |
Location.pp_loc loc; |
101 |
raise exc |
102 |
|
103 |
let type_decls env decls = |
104 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. typing@ "); |
105 |
let new_env = |
106 |
begin |
107 |
try |
108 |
Typing.type_prog env decls |
109 |
with (Types.Error (loc,err)) as exc -> |
110 |
eprintf "Typing error: %a%a@." |
111 |
Types.pp_error err |
112 |
Location.pp_loc loc; |
113 |
raise exc |
114 |
end |
115 |
in |
116 |
if !Options.print_types || !Options.verbose_level > 2 then |
117 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2> %a@]@ " Corelang.pp_prog_type decls); |
118 |
new_env |
119 |
|
120 |
let clock_decls env decls = |
121 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. clock calculus@ "); |
122 |
let new_env = |
123 |
begin |
124 |
try |
125 |
Clock_calculus.clock_prog env decls |
126 |
with (Clocks.Error (loc,err)) as exc -> |
127 |
eprintf "Clock calculus error: %a%a@." Clocks.pp_error err Location.pp_loc loc; |
128 |
raise exc |
129 |
end |
130 |
in |
131 |
if !Options.print_clocks || !Options.verbose_level > 2 then |
132 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2> %a@]@ " Corelang.pp_prog_clock decls); |
133 |
new_env |
134 |
|
135 |
(* Typing/Clocking with an empty env *) |
136 |
let check_top_decls header = |
137 |
let new_tenv = type_decls Basic_library.type_env header in (* Typing *) |
138 |
let new_cenv = clock_decls Basic_library.clock_env header in (* Clock calculus *) |
139 |
header, new_tenv, new_cenv |
140 |
|
141 |
|
142 |
(* |
143 |
List.fold_right |
144 |
(fun top_decl (ty_env, ck_env) -> |
145 |
match top_decl.top_decl_desc with |
146 |
| Node nd -> (Env.add_value ty_env nd.node_id nd.node_type, |
147 |
Env.add_value ck_env nd.node_id nd.node_clock) |
148 |
| ImportedNode ind -> (Env.add_value ty_env ind.nodei_id ind.nodei_type, |
149 |
Env.add_value ck_env ind.nodei_id ind.nodei_clock) |
150 |
| Const c -> get_envs_from_const c (ty_env, ck_env) |
151 |
| TypeDef _ -> List.fold_left (fun envs top -> consts_of_enum_type top_decl |
152 |
| Open _ -> (ty_env, ck_env)) |
153 |
header |
154 |
(Env.initial, Env.initial) |
155 |
*) |
156 |
|
157 |
|
158 |
|
159 |
|
160 |
let check_compatibility (prog, computed_types_env, computed_clocks_env) (header, declared_types_env, declared_clocks_env) = |
161 |
try |
162 |
(* checking defined types are compatible with declared types*) |
163 |
Typing.check_typedef_compat header; |
164 |
|
165 |
(* checking type compatibility with computed types*) |
166 |
Typing.check_env_compat header declared_types_env computed_types_env; |
167 |
|
168 |
(* checking clocks compatibility with computed clocks*) |
169 |
Clock_calculus.check_env_compat header declared_clocks_env computed_clocks_env; |
170 |
|
171 |
(* checking stateless status compatibility *) |
172 |
Stateless.check_compat header |
173 |
with |
174 |
| (Types.Error (loc,err)) as exc -> |
175 |
eprintf "Type mismatch between computed type and declared type in lustre interface file: %a%a@." |
176 |
Types.pp_error err |
177 |
Location.pp_loc loc; |
178 |
raise exc |
179 |
| Clocks.Error (loc, err) as exc -> |
180 |
eprintf "Clock mismatch between computed clock and declared clock in lustre interface file: %a%a@." |
181 |
Clocks.pp_error err |
182 |
Location.pp_loc loc; |
183 |
raise exc |
184 |
| Stateless.Error (loc, err) as exc -> |
185 |
eprintf "Stateless status mismatch between defined status and declared status in lustre interface file: %a%a@." |
186 |
Stateless.pp_error err |
187 |
Location.pp_loc loc; |
188 |
raise exc |
189 |
|
190 |
(* Process each node/imported node and introduce the associated contract node *) |
191 |
let resolve_contracts prog = |
192 |
(* Bind a fresh node with a new name according to existing nodes and freshly binded contract node. Clean the contract to remove the stmts *) |
193 |
let process_contract new_contracts prog c = |
194 |
(* Resolve first the imports *) |
195 |
let stmts, locals, c = |
196 |
List.fold_left ( |
197 |
fun (stmts, locals, c) import -> |
198 |
(* Search for contract in prog. |
199 |
The node have to be processed already. Otherwise raise an error. |
200 |
Each stmts in injected with a fresh name |
201 |
Inputs are renamed and associated to the expression in1 |
202 |
Same thing for outputs. |
203 |
|
204 |
Last the contracts elements are replaced with the renamed vars and merged with c contract. |
205 |
*) |
206 |
let name = import.import_nodeid in |
207 |
assert false; (* TODO: we do not handle imports yet. The |
208 |
algorithm is sketched below *) |
209 |
(* |
210 |
try |
211 |
let imp_nd = xxx in (* Get the contract node in prog *) |
212 |
(* checking that it's actually a (processed) contract *) |
213 |
let imp_c = |
214 |
match imp_nd.node_spec with |
215 |
Some (Contract imp_c) -> |
216 |
if imp_c.imports = [] then |
217 |
imp_c |
218 |
else |
219 |
assert false (* should be processed *) |
220 |
| _ -> assert false (* should be a contract *) |
221 |
in |
222 |
(* Preparing vars: renaming them *) |
223 |
let imp_in = rename imp_nd.node_inputs in |
224 |
let imp_out = rename imp_nd.node_outputs in |
225 |
let imp_locals = rename imp_nd.node_locals in |
226 |
let locals = imp_in@imp_out@imp_locals@locals in |
227 |
(* Assinging in and out *) |
228 |
let in_assigns = |
229 |
xxx imp_in = import.inputs |
230 |
in |
231 |
let out_assigns = |
232 |
xxx imp_out = import.outputs |
233 |
in |
234 |
let stmts = stmts @ (rename imp_nd.stmts) in |
235 |
let imp_c = rename imp_c in |
236 |
let c = merge_contracts c imp_c in |
237 |
stmts, locals, c |
238 |
with Not_found -> raise (Error.Unbound_symbol ("contract " ^ name)) |
239 |
|
240 |
*) |
241 |
) ([], c.consts@c.locals, c) c.imports |
242 |
in |
243 |
(* Other contract elements will be normalized later *) |
244 |
let c = { c with |
245 |
locals = []; |
246 |
consts = []; |
247 |
stmts = []; |
248 |
imports = [] |
249 |
} |
250 |
in |
251 |
stmts, locals, c |
252 |
|
253 |
in |
254 |
let process_contract_new_node accu_contracts prog top = |
255 |
let id, spec, inputs, outputs = |
256 |
match top.top_decl_desc with |
257 |
| Node nd -> nd.node_id, nd.node_spec, nd.node_inputs, nd.node_outputs |
258 |
| ImportedNode ind -> ind.nodei_id, ind.nodei_spec, ind.nodei_inputs, ind.nodei_outputs |
259 |
| _ -> assert false |
260 |
in |
261 |
let stmts, locals, c = |
262 |
match spec with |
263 |
| None | Some (NodeSpec _) -> assert false |
264 |
| Some (Contract c) -> |
265 |
process_contract accu_contracts prog c |
266 |
in |
267 |
(* Create a fresh name *) |
268 |
let used v = List.exists (fun top -> |
269 |
match top.top_decl_desc with |
270 |
| Node _ |
271 |
| ImportedNode _ -> |
272 |
(node_name top) = v |
273 |
| _ -> false |
274 |
) (accu_contracts@prog) |
275 |
in |
276 |
let new_nd_id = mk_new_name used (id ^ "_coco") in |
277 |
let new_nd = |
278 |
mktop_decl |
279 |
c.spec_loc |
280 |
top.top_decl_owner |
281 |
top.top_decl_itf |
282 |
(Node { |
283 |
node_id = new_nd_id; |
284 |
node_type = Types.new_var (); |
285 |
node_clock = Clocks.new_var true; |
286 |
node_inputs = inputs; |
287 |
node_outputs = outputs; |
288 |
node_locals = locals; |
289 |
node_gencalls = []; |
290 |
node_checks = []; |
291 |
node_asserts = []; |
292 |
node_stmts = stmts; |
293 |
node_dec_stateless = false; |
294 |
node_stateless = None; |
295 |
node_spec = Some (Contract c); |
296 |
node_annot = []; |
297 |
node_iscontract = true; |
298 |
}) in |
299 |
new_nd |
300 |
in |
301 |
(* Processing nodes in order. Should have been sorted by now |
302 |
|
303 |
Each top level contract is processed: stmts pushed in node |
304 |
|
305 |
Each regular imported node or node associated with a contract is |
306 |
replaced with a simplidfied contract and its contract is bound to |
307 |
a fresh node. |
308 |
|
309 |
*) |
310 |
let new_contracts, prog = |
311 |
List.fold_left |
312 |
( |
313 |
fun (accu_contracts, accu_nodes) top -> |
314 |
match top.top_decl_desc with |
315 |
|
316 |
| Node nd when nd.node_iscontract -> ( |
317 |
match nd.node_spec with |
318 |
| None | Some (NodeSpec _) -> assert false |
319 |
| Some (Contract c) -> |
320 |
let stmts, locals, c = process_contract accu_contracts prog c in |
321 |
let nd = |
322 |
{ nd with |
323 |
node_locals = nd.node_locals @ locals; |
324 |
node_stmts = nd.node_stmts @ stmts; |
325 |
node_spec = Some (Contract c); |
326 |
} |
327 |
in |
328 |
{ top with top_decl_desc = Node nd }::accu_contracts, |
329 |
accu_nodes |
330 |
|
331 |
) |
332 |
| Node nd -> ( |
333 |
match nd.node_spec with |
334 |
| None -> accu_contracts, top::accu_nodes (* A boring node: no contract *) |
335 |
| Some (NodeSpec id) -> (* shall not happen, its too early *) |
336 |
assert false |
337 |
| Some (Contract c) -> (* A contract: processing it *) |
338 |
(* we bind a fresh node *) |
339 |
let new_nd = process_contract_new_node accu_contracts prog top in |
340 |
Format.eprintf "Creating new contract node %s@." (node_name new_nd); |
341 |
let nd = { nd with node_spec = (Some (NodeSpec (node_name new_nd))) } in |
342 |
new_nd::accu_contracts, |
343 |
{ top with top_decl_desc = Node nd }::accu_nodes |
344 |
|
345 |
) |
346 |
|
347 |
| ImportedNode ind -> ( (* Similar treatment for imported nodes *) |
348 |
match ind.nodei_spec with |
349 |
None -> accu_contracts, top::accu_nodes (* A boring node: no contract *) |
350 |
| Some (NodeSpec id) -> (* shall not happen, its too early *) |
351 |
assert false |
352 |
| Some (Contract c) -> (* A contract: processing it *) |
353 |
(* we bind a fresh node *) |
354 |
let new_nd = process_contract_new_node accu_contracts prog top in |
355 |
let ind = { ind with nodei_spec = (Some (NodeSpec (node_name new_nd))) } in |
356 |
new_nd::accu_contracts, |
357 |
{ top with top_decl_desc = ImportedNode ind }::accu_nodes |
358 |
) |
359 |
| _ -> accu_contracts, top::accu_nodes |
360 |
) ([],[]) prog |
361 |
in |
362 |
(List.rev new_contracts) @ (List.rev prog) |
363 |
|
364 |
|
365 |
|
366 |
let track_exception () = |
367 |
if !Options.track_exceptions |
368 |
then (Printexc.print_backtrace stdout; flush stdout) |
369 |
else () |
370 |
|
371 |
|
372 |
let update_vdecl_parents_prog prog = |
373 |
let update_vdecl_parents parent v = |
374 |
v.var_parent_nodeid <- Some parent |
375 |
in |
376 |
List.iter ( |
377 |
fun top -> match top.top_decl_desc with |
378 |
| Node nd -> |
379 |
List.iter |
380 |
(update_vdecl_parents nd.node_id) |
381 |
(nd.node_inputs @ nd.node_outputs @ nd.node_locals ) |
382 |
| ImportedNode ind -> |
383 |
List.iter |
384 |
(update_vdecl_parents ind.nodei_id) |
385 |
(ind.nodei_inputs @ ind.nodei_outputs ) |
386 |
| _ -> () |
387 |
) prog |