lustrec / src / main_lustre_compiler.ml @ 566dbf49
History | View | Annotate | Download (12 KB)
1 | ef34b4ae | xthirioux | (********************************************************************) |
---|---|---|---|
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 Format |
||
13 | open Log |
||
14 | |||
15 | 54d032f5 | xthirioux | open Utils |
16 | ef34b4ae | xthirioux | open LustreSpec |
17 | open Compiler_common |
||
18 | |||
19 | let usage = "Usage: lustrec [options] <source-file>" |
||
20 | |||
21 | let extensions = [".ec"; ".lus"; ".lusi"] |
||
22 | |||
23 | (* print a .lusi header file from a source prog *) |
||
24 | let print_lusi prog basename extension = |
||
25 | let header = Lusic.extract_header basename prog in |
||
26 | let header_name = basename ^ extension in |
||
27 | let h_out = open_out header_name in |
||
28 | let h_fmt = formatter_of_out_channel h_out in |
||
29 | begin |
||
30 | Printers.pp_lusi_header h_fmt basename header; |
||
31 | close_out h_out |
||
32 | end |
||
33 | |||
34 | (* compile a .lusi header file *) |
||
35 | 1e48ef45 | ploc | let compile_header dirname basename extension = |
36 | 9603460e | xthirioux | let destname = !Options.dest_dir ^ "/" ^ basename in |
37 | let header_name = basename ^ extension in |
||
38 | let lusic_ext = extension ^ "c" in |
||
39 | begin |
||
40 | Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>"); |
||
41 | 1e48ef45 | ploc | let header = parse_header true (dirname ^ "/" ^ header_name) in |
42 | 54d032f5 | xthirioux | ignore (Modules.load_header ISet.empty header); |
43 | 9603460e | xthirioux | ignore (check_top_decls header); |
44 | create_dest_dir (); |
||
45 | c7c6ef4c | tkahsai | Log.report ~level:1 |
46 | 1e48ef45 | ploc | (fun fmt -> fprintf fmt ".. generating compiled header file %sc@," (destname ^ extension)); |
47 | 9603460e | xthirioux | Lusic.write_lusic true header destname lusic_ext; |
48 | Lusic.print_lusic_to_h destname lusic_ext; |
||
49 | Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.") |
||
50 | end |
||
51 | ef34b4ae | xthirioux | |
52 | (* check whether a source file has a compiled header, |
||
53 | if not, generate the compiled header *) |
||
54 | let compile_source_to_header prog computed_types_env computed_clocks_env basename extension = |
||
55 | 9603460e | xthirioux | let destname = !Options.dest_dir ^ "/" ^ basename in |
56 | ef34b4ae | xthirioux | let lusic_ext = extension ^ "c" in |
57 | 9603460e | xthirioux | let header_name = destname ^ lusic_ext in |
58 | ef34b4ae | xthirioux | begin |
59 | if not (Sys.file_exists header_name) then |
||
60 | begin |
||
61 | Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name); |
||
62 | 9603460e | xthirioux | Lusic.write_lusic false (Lusic.extract_header basename prog) destname lusic_ext; |
63 | Lusic.print_lusic_to_h destname lusic_ext |
||
64 | ef34b4ae | xthirioux | end |
65 | else |
||
66 | 9603460e | xthirioux | let lusic = Lusic.read_lusic destname lusic_ext in |
67 | ef34b4ae | xthirioux | if not lusic.Lusic.from_lusi then |
68 | begin |
||
69 | Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name); |
||
70 | 9603460e | xthirioux | Lusic.write_lusic false (Lusic.extract_header basename prog) destname lusic_ext; |
71 | ef34b4ae | xthirioux | (*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*) |
72 | 9603460e | xthirioux | Lusic.print_lusic_to_h destname lusic_ext |
73 | ef34b4ae | xthirioux | end |
74 | else |
||
75 | begin |
||
76 | Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name); |
||
77 | let header = lusic.Lusic.contents in |
||
78 | let (declared_types_env, declared_clocks_env) = get_envs_from_top_decls header in |
||
79 | check_compatibility |
||
80 | (prog, computed_types_env, computed_clocks_env) |
||
81 | (header, declared_types_env, declared_clocks_env) |
||
82 | end |
||
83 | end |
||
84 | |||
85 | (* compile a .lus source file *) |
||
86 | 1e48ef45 | ploc | let rec compile_source dirname basename extension = |
87 | b9c40119 | ploc | let source_name = (* dirname ^ "/" ^*) basename ^ extension in |
88 | ef34b4ae | xthirioux | |
89 | Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>"); |
||
90 | |||
91 | 54d032f5 | xthirioux | (* Parsing source *) |
92 | ef34b4ae | xthirioux | let prog = parse_source source_name in |
93 | |||
94 | c7c6ef4c | tkahsai | (* Removing automata *) |
95 | 54d032f5 | xthirioux | let prog = Automata.expand_decls prog in |
96 | |||
97 | (* Importing source *) |
||
98 | let _ = Modules.load_program ISet.empty prog in |
||
99 | |||
100 | ef34b4ae | xthirioux | (* Extracting dependencies *) |
101 | let dependencies, type_env, clock_env = import_dependencies prog in |
||
102 | d5767b5a | xthirioux | |
103 | ef34b4ae | xthirioux | (* Sorting nodes *) |
104 | let prog = SortProg.sort prog in |
||
105 | |||
106 | (* Typing *) |
||
107 | let computed_types_env = type_decls type_env prog in |
||
108 | c7c6ef4c | tkahsai | |
109 | ef34b4ae | xthirioux | (* Clock calculus *) |
110 | let computed_clocks_env = clock_decls clock_env prog in |
||
111 | |||
112 | (* Checking stateless/stateful status *) |
||
113 | check_stateless_decls prog; |
||
114 | |||
115 | (* Generating a .lusi header file only *) |
||
116 | if !Options.lusi then |
||
117 | begin |
||
118 | let lusi_ext = extension ^ "i" in |
||
119 | Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating interface file %s@," (basename ^ lusi_ext)); |
||
120 | print_lusi prog basename lusi_ext; |
||
121 | Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@."); |
||
122 | exit 0 |
||
123 | end; |
||
124 | |||
125 | (* Perform global inlining *) |
||
126 | let prog = |
||
127 | c7c6ef4c | tkahsai | if !Options.global_inline && |
128 | ef34b4ae | xthirioux | (match !Options.main_node with | "" -> false | _ -> true) then |
129 | Inliner.global_inline basename prog type_env clock_env |
||
130 | 566dbf49 | ploc | else (* if !Option.has_local_inline *) |
131 | Inliner.local_inline basename prog type_env clock_env |
||
132 | ef34b4ae | xthirioux | in |
133 | |||
134 | (* Delay calculus *) |
||
135 | 566dbf49 | ploc | (* TO BE DONE LATER (Xavier) |
136 | ef34b4ae | xthirioux | if(!Options.delay_calculus) |
137 | then |
||
138 | begin |
||
139 | Log.report ~level:1 (fun fmt -> fprintf fmt ".. initialisation analysis@?"); |
||
140 | try |
||
141 | Delay_calculus.delay_prog Basic_library.delay_env prog |
||
142 | with (Delay.Error (loc,err)) as exc -> |
||
143 | Location.print loc; |
||
144 | eprintf "%a" Delay.pp_error err; |
||
145 | Utils.track_exception (); |
||
146 | raise exc |
||
147 | end; |
||
148 | *) |
||
149 | 566dbf49 | ploc | |
150 | ef34b4ae | xthirioux | (* Creating destination directory if needed *) |
151 | create_dest_dir (); |
||
152 | |||
153 | (* Compatibility with Lusi *) |
||
154 | (* Checking the existence of a lusi (Lustre Interface file) *) |
||
155 | let extension = ".lusi" in |
||
156 | compile_source_to_header prog computed_types_env computed_clocks_env basename extension; |
||
157 | |||
158 | Typing.uneval_prog_generics prog; |
||
159 | Clock_calculus.uneval_prog_generics prog; |
||
160 | |||
161 | (* Computes and stores generic calls for each node, |
||
162 | only useful for ANSI C90 compliant generic node compilation *) |
||
163 | if !Options.ansi then Causality.NodeDep.compute_generic_calls prog; |
||
164 | (*Hashtbl.iter (fun id td -> match td.Corelang.top_decl_desc with Corelang.Node nd -> Format.eprintf "%s calls %a" id Causality.NodeDep.pp_generic_calls nd | _ -> ()) Corelang.node_table;*) |
||
165 | |||
166 | (* Normalization phase *) |
||
167 | Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,"); |
||
168 | (* Special treatment of arrows in lustre backend. We want to keep them *) |
||
169 | if !Options.output = "lustre" then |
||
170 | Normalization.unfold_arrow_active := false; |
||
171 | let prog = Normalization.normalize_prog prog in |
||
172 | Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog); |
||
173 | (* Checking array accesses *) |
||
174 | if !Options.check then |
||
175 | begin |
||
176 | Log.report ~level:1 (fun fmt -> fprintf fmt ".. array access checks@,"); |
||
177 | Access.check_prog prog; |
||
178 | end; |
||
179 | |||
180 | (* Computation of node equation scheduling. It also breaks dependency cycles |
||
181 | and warns about unused input or memory variables *) |
||
182 | f2b1c245 | ploc | Log.report ~level:1 (fun fmt -> fprintf fmt ".. scheduling@,@?"); |
183 | ef34b4ae | xthirioux | let prog, node_schs = Scheduling.schedule_prog prog in |
184 | df39e35a | xthirioux | Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_warning_unused node_schs); |
185 | ef34b4ae | xthirioux | Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs); |
186 | Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs); |
||
187 | Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog); |
||
188 | |||
189 | c7c6ef4c | tkahsai | (* Optimization of prog: |
190 | - Unfold consts |
||
191 | ef34b4ae | xthirioux | - eliminate trivial expressions |
192 | *) |
||
193 | c7c6ef4c | tkahsai | let prog = |
194 | if !Options.optimization >= 4 then |
||
195 | Optimize_prog.prog_unfold_consts prog |
||
196 | ef34b4ae | xthirioux | else |
197 | prog |
||
198 | in |
||
199 | (* DFS with modular code generation *) |
||
200 | Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,"); |
||
201 | let machine_code = Machine_code.translate_prog prog node_schs in |
||
202 | |||
203 | (* Optimize machine code *) |
||
204 | c7c6ef4c | tkahsai | let machine_code = |
205 | d0b1ec56 | xthirioux | if !Options.optimization >= 2 && !Options.output <> "horn" then |
206 | ef34b4ae | xthirioux | begin |
207 | d0b1ec56 | xthirioux | Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 1)@,"); |
208 | Optimize_machine.machines_unfold (Corelang.get_consts prog) node_schs machine_code |
||
209 | ef34b4ae | xthirioux | end |
210 | else |
||
211 | machine_code |
||
212 | c7c6ef4c | tkahsai | in |
213 | d0b1ec56 | xthirioux | (* Optimize machine code *) |
214 | c7c6ef4c | tkahsai | let machine_code = |
215 | ef34b4ae | xthirioux | if !Options.optimization >= 3 && !Options.output <> "horn" then |
216 | begin |
||
217 | d0b1ec56 | xthirioux | Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 2)@,"); |
218 | Optimize_machine.machines_fusion (Optimize_machine.machines_reuse_variables machine_code node_schs) |
||
219 | ef34b4ae | xthirioux | end |
220 | else |
||
221 | machine_code |
||
222 | in |
||
223 | Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," |
||
224 | (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine) |
||
225 | machine_code); |
||
226 | |||
227 | (* Printing code *) |
||
228 | let basename = Filename.basename basename in |
||
229 | let destname = !Options.dest_dir ^ "/" ^ basename in |
||
230 | let _ = match !Options.output with |
||
231 | c7c6ef4c | tkahsai | "C" -> |
232 | ef34b4ae | xthirioux | begin |
233 | let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *) |
||
234 | let source_lib_file = destname ^ ".c" in (* Could be changed *) |
||
235 | let source_main_file = destname ^ "_main.c" in (* Could be changed *) |
||
236 | let makefile_file = destname ^ ".makefile" in (* Could be changed *) |
||
237 | Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,"); |
||
238 | c7c6ef4c | tkahsai | C_backend.translate_to_c |
239 | ef34b4ae | xthirioux | alloc_header_file source_lib_file source_main_file makefile_file |
240 | basename prog machine_code dependencies |
||
241 | end |
||
242 | | "java" -> |
||
243 | begin |
||
244 | failwith "Sorry, but not yet supported !" |
||
245 | (*let source_file = basename ^ ".java" in |
||
246 | Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file); |
||
247 | let source_out = open_out source_file in |
||
248 | let source_fmt = formatter_of_out_channel source_out in |
||
249 | Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?"); |
||
250 | Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*) |
||
251 | end |
||
252 | | "horn" -> |
||
253 | begin |
||
254 | let source_file = destname ^ ".smt2" in (* Could be changed *) |
||
255 | let source_out = open_out source_file in |
||
256 | let fmt = formatter_of_out_channel source_out in |
||
257 | Horn_backend.translate fmt basename prog machine_code; |
||
258 | (* Tracability file if option is activated *) |
||
259 | ea1c2906 | ploc | if !Options.traces then ( |
260 | 922ed789 | tkahsai | let traces_file = destname ^ ".traces.xml" in (* Could be changed *) |
261 | ef34b4ae | xthirioux | let traces_out = open_out traces_file in |
262 | let fmt = formatter_of_out_channel traces_out in |
||
263 | 922ed789 | tkahsai | Horn_backend.traces_file fmt basename prog machine_code; |
264 | |||
265 | ef34b4ae | xthirioux | ) |
266 | end |
||
267 | c7c6ef4c | tkahsai | | "lustre" -> |
268 | ef34b4ae | xthirioux | begin |
269 | let source_file = destname ^ ".lustrec.lus" in (* Could be changed *) |
||
270 | let source_out = open_out source_file in |
||
271 | let fmt = formatter_of_out_channel source_out in |
||
272 | Printers.pp_prog fmt prog; |
||
273 | (* Lustre_backend.translate fmt basename normalized_prog machine_code *) |
||
274 | () |
||
275 | end |
||
276 | |||
277 | | _ -> assert false |
||
278 | in |
||
279 | begin |
||
280 | Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@."); |
||
281 | (* We stop the process here *) |
||
282 | exit 0 |
||
283 | end |
||
284 | |||
285 | 1e48ef45 | ploc | let compile dirname basename extension = |
286 | ef34b4ae | xthirioux | match extension with |
287 | 1e48ef45 | ploc | | ".lusi" -> compile_header dirname basename extension |
288 | | ".lus" -> compile_source dirname basename extension |
||
289 | ef34b4ae | xthirioux | | _ -> assert false |
290 | |||
291 | let anonymous filename = |
||
292 | c7c6ef4c | tkahsai | let ok_ext, ext = List.fold_left |
293 | (fun (ok, ext) ext' -> |
||
294 | if not ok && Filename.check_suffix filename ext' then |
||
295 | true, ext' |
||
296 | 1e48ef45 | ploc | else |
297 | c7c6ef4c | tkahsai | ok, ext) |
298 | 1e48ef45 | ploc | (false, "") extensions in |
299 | ef34b4ae | xthirioux | if ok_ext then |
300 | 1e48ef45 | ploc | let dirname = Filename.dirname filename in |
301 | 9603460e | xthirioux | let basename = Filename.chop_suffix (Filename.basename filename) ext in |
302 | 1e48ef45 | ploc | compile dirname basename ext |
303 | ef34b4ae | xthirioux | else |
304 | raise (Arg.Bad ("Can only compile *.lusi, *.lus or *.ec files")) |
||
305 | |||
306 | let _ = |
||
307 | Corelang.add_internal_funs (); |
||
308 | try |
||
309 | Printexc.record_backtrace true; |
||
310 | Arg.parse Options.options anonymous usage |
||
311 | with |
||
312 | c7c6ef4c | tkahsai | | Parse.Syntax_err _ | Lexer_lustre.Error _ |
313 | ef34b4ae | xthirioux | | Types.Error (_,_) | Clocks.Error (_,_) |
314 | c7c6ef4c | tkahsai | | Corelang.Error _ (*| Task_set.Error _*) |
315 | ef34b4ae | xthirioux | | Causality.Cycle _ -> exit 1 |
316 | | Sys_error msg -> (eprintf "Failure: %s@." msg) |
||
317 | | exc -> (Utils.track_exception (); raise exc) |
||
318 | |||
319 | (* Local Variables: *) |
||
320 | (* compile-command:"make -C .." *) |
||
321 | (* End: *) |