Project

General

Profile

Download (12.6 KB) Statistics
| Branch: | Tag: | Revision:
1 04257b1e ploc
open Format
2
open Utils
3
open Compiler_common
4 8446bf03 ploc
open Lustre_types
5 f0195e96 ploc
module Mpfr = Lustrec_mpfr
6 04257b1e ploc
7 ad4774b0 ploc
exception StopPhase1 of program_t
8 04257b1e ploc
9
let dynamic_checks () =
10
  match !Options.output, !Options.spec with
11
  | "C", "C" -> true
12
  | _ -> false
13 f20d8ac7 Christophe Garion
14 04257b1e ploc
15
(* check whether a source file has a compiled header, if not, generate the
16
   compiled header *)
17
let compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension =
18
  let destname = !Options.dest_dir ^ "/" ^ basename in
19 217837e2 ploc
  let lusic_ext = ".lusic" in
20 04257b1e ploc
  let header_name = destname ^ lusic_ext in
21
  begin
22 217837e2 ploc
    if (* Generating the lusic file *)
23
      extension = ".lusi" (* because input is a lusi *)
24
      || (extension = ".lus" &&
25
            not (Sys.file_exists header_name))
26
           (* or because it is a lus but not lusic exists *)
27
      || (let lusic = Lusic.read_lusic destname lusic_ext in
28
          not lusic.Lusic.from_lusi)
29
         (* or the lusic exists but is not generated from a lusi, hence it
30
            has te be regenerated *)
31
    then
32 04257b1e ploc
      begin
33
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
34 217837e2 ploc
	Lusic.write_lusic
35
          (extension = ".lusi") (* is it a lusi file ? *)
36
          (if extension = ".lusi" then prog else Lusic.extract_header dirname basename prog)
37
          destname
38
          lusic_ext;
39
        let _ =
40
          match !Options.output with
41
          | "C" -> C_backend_lusic.print_lusic_to_h destname lusic_ext
42
          | _ -> ()
43
        in
44
        ()
45
      end
46
    else (* Lusic exists and is usable. Checking compatibility *)
47
      begin
48
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
49
        let lusic = Lusic.read_lusic destname lusic_ext in
50
        Lusic.check_obsolete lusic destname;
51
	let header = lusic.Lusic.contents in
52
	let (declared_types_env, declared_clocks_env) = Modules.get_envs_from_top_decls header in
53
	check_compatibility
54
	  (prog, computed_types_env, computed_clocks_env)
55
	  (header, declared_types_env, declared_clocks_env)
56 04257b1e ploc
      end
57
  end
58
59
60
(* From prog to prog *)
61 217837e2 ploc
let stage1 params prog dirname basename extension =
62 66359a5e ploc
  (* Updating parent node information for variables *)
63
  Compiler_common.update_vdecl_parents_prog prog;
64
65 04257b1e ploc
  (* Removing automata *)
66
  let prog = expand_automata prog in
67
  Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@,  @[<v 2>@,%a@]@ " Printers.pp_prog prog);
68
69
  (* Importing source *)
70 217837e2 ploc
  let prog, dependencies, (typ_env, clk_env) = Modules.load ~is_header:(extension = ".lusi") prog in
71 5fccce23 ploc
  (* Registering types and clocks for future checks *)
72
  Global.type_env := Env.overwrite !Global.type_env typ_env;
73
  Global.clock_env := Env.overwrite !Global.clock_env clk_env;
74
  
75
  (* (\* Extracting dependencies (and updating Global.(type_env/clock_env) *\)
76
   * let dependencies = import_dependencies prog in *)
77 04257b1e ploc
78
  (* Sorting nodes *)
79
  let prog = SortProg.sort prog in
80 f4cba4b8 ploc
  (* Consolidating contracts *)
81
  let prog = resolve_contracts prog in
82 1fd3d002 ploc
  let prog = SortProg.sort prog in
83
  Log.report ~level:3 (fun fmt ->
84
      Format.fprintf fmt "@[<v 0>Contracts resolved:@ %a@ @]@ " Printers.pp_prog prog);
85 8df40160 ploc
86
  (* Consolidating main node *)
87
  let _ =
88
    match !Options.main_node with
89
    | "" -> ()
90
    | main_node -> (
91
      Global.main_node := main_node;
92
      try
93
        ignore (Corelang.node_from_name main_node)
94
      with Not_found -> (
95
        Format.eprintf "Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
96 04a188ec ploc
        raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
97 8df40160 ploc
    ))
98
  in
99 f4cba4b8 ploc
  
100 04257b1e ploc
  (* Perform inlining before any analysis *)
101
  let orig, prog =
102 8df40160 ploc
    if !Options.global_inline && !Global.main_node <> "" then
103 04257b1e ploc
      (if !Options.witnesses then prog else []),
104 f20d8ac7 Christophe Garion
      Inliner.global_inline basename prog
105 04257b1e ploc
    else (* if !Option.has_local_inline *)
106
      [],
107
      Inliner.local_inline prog (* type_env clock_env *)
108
  in
109
110
  (* Checking stateless/stateful status *)
111
  if Plugins.check_force_stateful () then
112
    force_stateful_decls prog
113
  else
114
    check_stateless_decls prog;
115
116
  (* Typing *)
117 2d27eedd ploc
  Global.type_env := type_decls !Global.type_env prog;
118 04257b1e ploc
119
  (* Clock calculus *)
120 2d27eedd ploc
  Global.clock_env := clock_decls !Global.clock_env prog;
121 04257b1e ploc
122 66359a5e ploc
  (* Registering and checking machine types *)
123 f4050bef ploc
  if Machine_types.is_active then Machine_types.load prog;
124 f20d8ac7 Christophe Garion
125 66359a5e ploc
126 04257b1e ploc
  (* Generating a .lusi header file only *)
127 a0c92fa8 ploc
  if !Options.lusi || !Options.print_nodes then
128 04257b1e ploc
    (* We stop here the processing and produce the current prog. It will be
129
       exported as a lusi *)
130
    raise (StopPhase1 prog);
131
132 f20d8ac7 Christophe Garion
  (* Optimization of prog:
133
     - Unfold consts
134 04257b1e ploc
     - eliminate trivial expressions
135 8df40160 ploc
   *)
136
  
137
  let prog =
138 04257b1e ploc
    if !Options.const_unfold || !Options.optimization >= 5 then
139 8df40160 ploc
      begin
140
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. eliminating constants and aliases@,");
141
        Optimize_prog.prog_unfold_consts prog
142
      end
143 04257b1e ploc
    else
144 8df40160 ploc
      prog
145
  in
146
  
147 04257b1e ploc
  (* Delay calculus *)
148
  (* TO BE DONE LATER (Xavier)
149
     if(!Options.delay_calculus)
150
     then
151
     begin
152
     Log.report ~level:1 (fun fmt -> fprintf fmt ".. initialisation analysis@?");
153
     try
154
     Delay_calculus.delay_prog Basic_library.delay_env prog
155
     with (Delay.Error (loc,err)) as exc ->
156
     Location.print loc;
157
     eprintf "%a" Delay.pp_error err;
158
     Utils.track_exception ();
159
     raise exc
160
     end;
161 8df40160 ploc
   *)
162 04257b1e ploc
163
  (* Creating destination directory if needed *)
164
  create_dest_dir ();
165 8df40160 ploc
  
166 04257b1e ploc
  Typing.uneval_prog_generics prog;
167
  Clock_calculus.uneval_prog_generics prog;
168
169 66359a5e ploc
170 8df40160 ploc
  (* Disabling witness option. Could but reactivated later
171 04257b1e ploc
  if !Options.global_inline && !Options.main_node <> "" && !Options.witnesses then
172
    begin
173
      let orig = Corelang.copy_prog orig in
174
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating witness file@,");
175
      check_stateless_decls orig;
176
      let _ = Typing.type_prog type_env orig in
177
      let _ = Clock_calculus.clock_prog clock_env orig in
178
      Typing.uneval_prog_generics orig;
179
      Clock_calculus.uneval_prog_generics orig;
180
      Inliner.witness
181
	basename
182
	!Options.main_node
183
	orig prog type_env clock_env
184
    end;
185 8df40160 ploc
   *)
186 2d27eedd ploc
187 04257b1e ploc
  (* Computes and stores generic calls for each node,
188
     only useful for ANSI C90 compliant generic node compilation *)
189
  if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
190
  (*Hashtbl.iter (fun id td -> match td.Corelang.top_decl_desc with
191
    Corelang.Node nd -> Format.eprintf "%s calls %a" id
192
    Causality.NodeDep.pp_generic_calls nd | _ -> ()) Corelang.node_table;*)
193
194
  (* If some backend involving dynamic checks are active, then node annotations become runtime checks *)
195
  let prog =
196
    if dynamic_checks () then
197
      Spec.enforce_spec_prog prog
198
    else
199
      prog
200
  in
201 66359a5e ploc
202
203
  (* (\* Registering and checking machine types *\) *)
204
  (* Machine_types.load prog; *)
205
206 04257b1e ploc
  (* Normalization phase *)
207
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
208 ad4774b0 ploc
  let prog = Normalization.normalize_prog params prog in
209 2120af73 ploc
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog_short prog);
210
  Log.report ~level:3  (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
211 59020713 ploc
  
212 684d39e7 ploc
  (* Compatibility with Lusi *)
213
  (* If compiling a lusi, generate the lusic. If this is a lus file, Check the existence of a lusi (Lustre Interface file) *)
214 7a4fd94d ploc
  if !Options.compile_header then
215
    compile_source_to_header
216
      prog !Global.type_env !Global.clock_env dirname basename extension;
217 684d39e7 ploc
218 04257b1e ploc
219
  let prog =
220
    if !Options.mpfr
221
    then
222
      begin
223
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. targetting MPFR library@,");
224
	Mpfr.inject_prog prog
225
      end
226
    else
227
      begin
228
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping floating-point numbers@,");
229
	prog
230
      end in
231 2120af73 ploc
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
232 04257b1e ploc
233
  (* Checking array accesses *)
234
  if !Options.check then
235
    begin
236
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking array accesses@,");
237
      Access.check_prog prog;
238
    end;
239
240 f20d8ac7 Christophe Garion
241 70466917 ploc
  let prog = SortProg.sort_nodes_locals prog in
242 f20d8ac7 Christophe Garion
243 04257b1e ploc
  prog, dependencies
244 66359a5e ploc
245
246
    (* from source to machine code, with optimization *)
247 8df40160 ploc
let stage2 params prog =
248 66359a5e ploc
  (* Computation of node equation scheduling. It also breaks dependency cycles
249
     and warns about unused input or memory variables *)
250
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. @[<v 2>scheduling@ ");
251
  let prog, node_schs =
252 f20d8ac7 Christophe Garion
    try
253 66359a5e ploc
      Scheduling.schedule_prog prog
254
    with Causality.Error _ -> (* Error is not kept. It is recomputed in a more
255
				 systemtic way in AlgebraicLoop module *)
256
      AlgebraicLoop.analyze prog
257
  in
258
  Log.report ~level:1 (fun fmt -> fprintf fmt "%a"              Scheduling.pp_warning_unused node_schs);
259
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs);
260
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);
261
  Log.report ~level:5 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_dep_graph node_schs);
262
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
263
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
264
265 f20d8ac7 Christophe Garion
  (* TODO Salsa optimize prog:
266 66359a5e ploc
     - emits warning for programs with pre inside expressions
267
     - make sure each node arguments and memory is bounded by a local annotation
268
     - introduce fresh local variables for each real pure subexpression
269
  *)
270
  (* DFS with modular code generation *)
271
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,");
272
  let machine_code = Machine_code.translate_prog prog node_schs in
273
274 2863281f ploc
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (unoptimized):@ %a@ " Machine_code_common.pp_machines machine_code);
275 66359a5e ploc
276
  (* Optimize machine code *)
277 8df40160 ploc
  Optimize_machine.optimize params prog node_schs machine_code
278 66359a5e ploc
279
280
(* printing code *)
281 217837e2 ploc
let stage3 prog machine_code dependencies basename extension =
282 66359a5e ploc
  let basename    =  Filename.basename basename in
283 217837e2 ploc
  match !Options.output, extension with
284
    "C", ".lus" -> 
285
     begin
286
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
287
       C_backend.translate_to_c
288
	 (* alloc_header_file source_lib_file source_main_file makefile_file *)
289
	 basename prog machine_code dependencies
290
     end
291
  |  "C", _ -> 
292 66359a5e ploc
      begin
293 217837e2 ploc
      	Log.report ~level:1 (fun fmt -> fprintf fmt ".. no C code generation for lusi@,");
294 66359a5e ploc
      end
295 217837e2 ploc
  | "java", _ ->
296 66359a5e ploc
     begin
297
       (Format.eprintf "internal error: sorry, but not yet supported !"; assert false)
298
     (*let source_file = basename ^ ".java" in
299
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
300
       let source_out = open_out source_file in
301
       let source_fmt = formatter_of_out_channel source_out in
302
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
303
       Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
304
     end
305 e4b630c5 Guillaume DAVY
  | "Ada", _ ->
306 f20d8ac7 Christophe Garion
    begin
307 c419ca44 Guillaume DAVY
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. Ada code generation@.");
308 f20d8ac7 Christophe Garion
      Ada_backend.translate_to_ada
309 e4b630c5 Guillaume DAVY
      basename prog (Machine_code_common.arrow_machine::machine_code) dependencies
310 f20d8ac7 Christophe Garion
    end
311 217837e2 ploc
  | "horn", _ ->
312 66359a5e ploc
     begin
313
       let destname = !Options.dest_dir ^ "/" ^ basename in
314
       let source_file = destname ^ ".smt2" in (* Could be changed *)
315
       let source_out = open_out source_file in
316
       let fmt = formatter_of_out_channel source_out in
317
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
318 2863281f ploc
       Horn_backend.translate fmt basename prog (Machine_code_common.arrow_machine::machine_code);
319 66359a5e ploc
       (* Tracability file if option is activated *)
320
       if !Options.traces then (
321
	 let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
322
	 let traces_out = open_out traces_file in
323
	 let fmt = formatter_of_out_channel traces_out in
324
         Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
325
	 Horn_backend_traces.traces_file fmt basename prog machine_code;
326
       )
327
     end
328 217837e2 ploc
  | "lustre", _ ->
329 66359a5e ploc
     begin
330
       let destname = !Options.dest_dir ^ "/" ^ basename in
331 217837e2 ploc
       let source_file = destname ^ ".lustrec" ^ extension  in (* Could be changed *)
332
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. exporting processed file as %s@," source_file);
333 66359a5e ploc
       let source_out = open_out source_file in
334
       let fmt = formatter_of_out_channel source_out in
335
       Printers.pp_prog fmt prog;
336
       Format.fprintf fmt "@.@?";
337
       (*	Lustre_backend.translate fmt basename normalized_prog machine_code *)
338
       ()
339
     end
340 217837e2 ploc
  | "emf", _ ->
341 66359a5e ploc
     begin
342
       let destname = !Options.dest_dir ^ "/" ^ basename in
343 1fd3d002 ploc
       let source_file = destname ^ ".json" in (* Could be changed *)
344 66359a5e ploc
       let source_out = open_out source_file in
345
       let fmt = formatter_of_out_channel source_out in
346
       EMF_backend.translate fmt basename prog machine_code;
347
       ()
348
     end
349
350
  | _ -> assert false