Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / main_lustre_compiler.ml @ 264a4844

History | View | Annotate | Download (15.5 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 Format
13
open Log
14

    
15
open Utils
16
open LustreSpec
17
open Compiler_common
18
 
19
exception StopPhase1 of program
20

    
21
let usage = "Usage: lustrec [options] \x1b[4msource file\x1b[0m"
22

    
23
let extensions = [".ec"; ".lus"; ".lusi"]
24

    
25
(* print a .lusi header file from a source prog *)
26
let print_lusi prog dirname basename extension =
27
  let header = Lusic.extract_header dirname basename prog in
28
  let header_name = dirname ^ "/" ^ basename ^ extension in
29
  let h_out = open_out header_name in
30
  let h_fmt = formatter_of_out_channel h_out in
31
  begin
32
    Typing.uneval_prog_generics header;
33
    Clock_calculus.uneval_prog_generics header;
34
    Printers.pp_lusi_header h_fmt basename header;
35
    close_out h_out
36
  end
37

    
38
(* compile a .lusi header file *)
39
let compile_header dirname  basename extension =
40
  let destname = !Options.dest_dir ^ "/" ^ basename in
41
  let header_name = basename ^ extension in
42
  let lusic_ext = extension ^ "c" in
43
  begin
44
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
45
    let header = parse_header true (dirname ^ "/" ^ header_name) in
46
    ignore (Modules.load_header ISet.empty header);
47
    ignore (check_top_decls header);
48
    create_dest_dir ();
49
    Log.report ~level:1
50
      (fun fmt -> fprintf fmt ".. generating compiled header file %sc@," (destname ^ extension));
51
    Lusic.write_lusic true header destname lusic_ext;
52
    generate_lusic_header destname lusic_ext;
53
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@ ")
54
  end
55

    
56
(* check whether a source file has a compiled header,
57
   if not, generate the compiled header *)
58
let compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension =
59
  let destname = !Options.dest_dir ^ "/" ^ basename in
60
  let lusic_ext = extension ^ "c" in
61
  let header_name = destname ^ lusic_ext in
62
  begin
63
    if not (Sys.file_exists header_name) then
64
      begin
65
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
66
	Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
67
	Lusic.print_lusic_to_h destname lusic_ext
68
      end
69
    else
70
      let lusic = Lusic.read_lusic destname lusic_ext in
71
      if not lusic.Lusic.from_lusi then
72
	begin
73
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
74
       	  Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
75
	  (*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*)
76
	  Lusic.print_lusic_to_h destname lusic_ext
77
	end
78
      else
79
	begin
80
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
81
	  Modules.check_dependency lusic destname;
82
	  let header = lusic.Lusic.contents in
83
	  let (declared_types_env, declared_clocks_env) = get_envs_from_top_decls header in
84
	  check_compatibility
85
	    (prog, computed_types_env, computed_clocks_env)
86
	    (header, declared_types_env, declared_clocks_env)
87
	end
88
  end
89

    
90

    
91

    
92
let dynamic_checks () =
93
  match !Options.output, !Options.spec with
94
  | "C", "C" -> true
95
  | _ -> false
96
     
97
(* From prog to prog *)
98
let stage1 prog dirname basename =
99
  (* Removing automata *)
100
  let prog = expand_automata prog in
101
  Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@,  @[<v 2>@,%a@]@ " Printers.pp_prog prog);
102

    
103
  (* Importing source *)
104
  let _ = Modules.load_program ISet.empty prog in
105

    
106
  (* Extracting dependencies *)
107
  let dependencies, type_env, clock_env = import_dependencies prog in
108

    
109
  (* Sorting nodes *)
110
  let prog = SortProg.sort prog in
111

    
112
  (* Perform inlining before any analysis *)
113
  let orig, prog =
114
    if !Options.global_inline && !Options.main_node <> "" then
115
      (if !Options.witnesses then prog else []),
116
      Inliner.global_inline basename prog type_env clock_env
117
    else (* if !Option.has_local_inline *)
118
      [],
119
      Inliner.local_inline prog (* type_env clock_env *)
120
  in
121

    
122
  (* Checking stateless/stateful status *)
123
  if Plugins.check_force_stateful () then
124
    force_stateful_decls prog
125
  else
126
    check_stateless_decls prog;
127

    
128
  (* Typing *)
129
  let computed_types_env = type_decls type_env prog in
130

    
131
  (* Clock calculus *)
132
  let computed_clocks_env = clock_decls clock_env prog in
133

    
134
  (* Generating a .lusi header file only *)
135
  if !Options.lusi then
136
    (* We stop here the processing and produce the current prog. It will be
137
       exported as a lusi *)
138
    raise (StopPhase1 prog);
139

    
140
 (* Optimization of prog: 
141
     - Unfold consts 
142
     - eliminate trivial expressions
143
 *)
144
  (*
145
  let prog = 
146
    if !Options.const_unfold || !Options.optimization >= 5 then
147
      begin
148
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. eliminating constants and aliases@,");
149
	Optimize_prog.prog_unfold_consts prog
150
      end
151
    else
152
      prog
153
  in
154
  *)
155
  (* Delay calculus *)
156
  (* TO BE DONE LATER (Xavier)
157
    if(!Options.delay_calculus)
158
    then
159
    begin
160
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. initialisation analysis@?");
161
    try
162
    Delay_calculus.delay_prog Basic_library.delay_env prog
163
    with (Delay.Error (loc,err)) as exc ->
164
    Location.print loc;
165
    eprintf "%a" Delay.pp_error err;
166
    Utils.track_exception ();
167
    raise exc
168
    end;
169
  *)
170

    
171
  (* Creating destination directory if needed *)
172
  create_dest_dir ();
173

    
174
  (* Compatibility with Lusi *)
175
  (* Checking the existence of a lusi (Lustre Interface file) *)
176
  let extension = ".lusi" in
177
  compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension;
178

    
179
  Typing.uneval_prog_generics prog;
180
  Clock_calculus.uneval_prog_generics prog;
181

    
182
  if !Options.global_inline && !Options.main_node <> "" && !Options.witnesses then
183
    begin
184
      let orig = Corelang.copy_prog orig in
185
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating witness file@,");
186
      check_stateless_decls orig;
187
      let _ = Typing.type_prog type_env orig in
188
      let _ = Clock_calculus.clock_prog clock_env orig in
189
      Typing.uneval_prog_generics orig;
190
      Clock_calculus.uneval_prog_generics orig;
191
      Inliner.witness
192
	basename
193
	!Options.main_node
194
	orig prog type_env clock_env
195
    end;
196
  
197
  (* Computes and stores generic calls for each node,
198
     only useful for ANSI C90 compliant generic node compilation *)
199
  if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
200
  (*Hashtbl.iter (fun id td -> match td.Corelang.top_decl_desc with
201
    Corelang.Node nd -> Format.eprintf "%s calls %a" id
202
    Causality.NodeDep.pp_generic_calls nd | _ -> ()) Corelang.node_table;*)
203

    
204
  (* If some backend involving dynamic checks are active, then node annotations become runtime checks *)
205
  let prog =
206
    if dynamic_checks () then
207
      Spec.enforce_spec_prog prog
208
    else
209
      prog
210
  in
211
  
212
  (* Normalization phase *)
213
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
214
  let prog = Normalization.normalize_prog ~backend:!Options.output prog in
215
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
216

    
217
  let prog =
218
    if !Options.mpfr
219
    then
220
      begin
221
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. targetting MPFR library@,");
222
	Mpfr.inject_prog prog
223
      end
224
    else
225
      begin
226
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping floating-point numbers@,");
227
	prog
228
      end in
229
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
230

    
231
  (* Checking array accesses *)
232
  if !Options.check then
233
    begin
234
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking array accesses@,");
235
      Access.check_prog prog;
236
    end;
237

    
238
  prog, dependencies
239

    
240
(* from source to machine code, with optimization *)
241
let stage2 prog =    
242
  (* Computation of node equation scheduling. It also breaks dependency cycles
243
     and warns about unused input or memory variables *)
244
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. @[<v 2>scheduling@ ");
245
  let prog, node_schs =
246
    try 
247
      Scheduling.schedule_prog prog
248
    with Causality.Error _ -> (* Error is not kept. It is recomputed in a more
249
				 systemtic way in AlgebraicLoop module *)
250
      AlgebraicLoop.analyze prog
251
  in
252
  Log.report ~level:1 (fun fmt -> fprintf fmt "%a"              Scheduling.pp_warning_unused node_schs);
253
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs);
254
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);
255
  Log.report ~level:5 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_dep_graph node_schs);
256
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
257
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
258

    
259
  (* TODO Salsa optimize prog: 
260
     - emits warning for programs with pre inside expressions
261
     - make sure each node arguments and memory is bounded by a local annotation
262
     - introduce fresh local variables for each real pure subexpression
263
  *)
264
  (* DFS with modular code generation *)
265
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,");
266
  let machine_code = Machine_code.translate_prog prog node_schs in
267

    
268
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (unoptimized):@ %a@ "Machine_code.pp_machines machine_code);
269

    
270
  (* Optimize machine code *)
271
  Optimize_machine.optimize prog node_schs machine_code
272

    
273

    
274
(* printing code *)
275
let stage3 prog machine_code dependencies basename =
276
  let basename    =  Filename.basename basename in
277
  match !Options.output with
278
    "C" -> 
279
      begin
280
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
281
	C_backend.translate_to_c
282
	  (* alloc_header_file source_lib_file source_main_file makefile_file *)
283
	  basename prog machine_code dependencies
284
      end
285
  | "java" ->
286
     begin
287
       (Format.eprintf "internal error: sorry, but not yet supported !"; assert false)
288
     (*let source_file = basename ^ ".java" in
289
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
290
       let source_out = open_out source_file in
291
       let source_fmt = formatter_of_out_channel source_out in
292
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
293
       Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
294
     end
295
  | "horn" ->
296
     begin
297
       let destname = !Options.dest_dir ^ "/" ^ basename in
298
       let source_file = destname ^ ".smt2" in (* Could be changed *)
299
       let source_out = open_out source_file in
300
       let fmt = formatter_of_out_channel source_out in
301
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
302
       Horn_backend.translate fmt basename prog (Machine_code.arrow_machine::machine_code);
303
       (* Tracability file if option is activated *)
304
       if !Options.traces then (
305
	 let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
306
	 let traces_out = open_out traces_file in
307
	 let fmt = formatter_of_out_channel traces_out in
308
         Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
309
	 Horn_backend_traces.traces_file fmt basename prog machine_code;
310
       )
311
     end
312
  | "lustre" ->
313
     begin
314
       let destname = !Options.dest_dir ^ "/" ^ basename in
315
       let source_file = destname ^ ".lustrec.lus" in (* Could be changed *)
316
       let source_out = open_out source_file in
317
       let fmt = formatter_of_out_channel source_out in
318
       Printers.pp_prog fmt prog;
319
       (*	Lustre_backend.translate fmt basename normalized_prog machine_code *)
320
       ()
321
     end
322
  | "emf" ->
323
     begin
324
       let destname = !Options.dest_dir ^ "/" ^ basename in
325
       let source_file = destname ^ ".emf" in (* Could be changed *)
326
       let source_out = open_out source_file in
327
       let fmt = formatter_of_out_channel source_out in
328
       EMF_backend.translate fmt basename prog machine_code;
329
       ()
330
     end
331

    
332
  | _ -> assert false
333

    
334
(* compile a .lus source file *)
335
let rec compile_source dirname basename extension =
336
  let source_name = dirname ^ "/" ^ basename ^ extension in
337

    
338
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 0>");
339

    
340
  (* Parsing source *)
341
  let prog = parse_source source_name in
342

    
343
  let prog =
344
    if !Options.mpfr then
345
      Mpfr.mpfr_module::prog
346
    else
347
      prog
348
  in
349
  let prog, dependencies = 
350
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 1 : Normalisation@,");
351
    try 
352
      stage1 prog dirname basename
353
    with StopPhase1 prog -> (
354
      if !Options.lusi then
355
	begin
356
	  let lusi_ext = extension ^ "i" in
357
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating interface file %s@ " (basename ^ lusi_ext));
358
	  print_lusi prog dirname basename lusi_ext;
359
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
360
	  exit 0
361
	end
362
      else
363
        assert false
364
    )
365
  in
366
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@,");
367
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. Normalized program:@ %a@ "Printers.pp_prog prog);
368

    
369
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 2 : Machines generation@,");
370

    
371
  let machine_code = 
372
    stage2 prog 
373
  in
374

    
375
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
376
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. Generated machines:@ %a@ "Machine_code.pp_machines machine_code);
377

    
378
  if Scopes.Plugin.show_scopes () then
379
    begin
380
      let all_scopes = Scopes.compute_scopes prog !Options.main_node in
381
      (* Printing scopes *)
382
      if !Options.verbose_level >= 1 then
383
	Format.printf "Possible scopes are:@   ";
384
      Format.printf "@[<v>%a@ @]@ @?" Scopes.print_scopes all_scopes;
385
      exit 0
386
	
387
    end;
388

    
389
  let machine_code = Plugins.refine_machine_code prog machine_code in
390
  
391
  stage3 prog machine_code dependencies basename;
392
  begin
393
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
394
    (* We stop the process here *)
395
    exit 0
396
  end
397

    
398
let compile dirname basename extension =
399
  match extension with
400
  | ".lusi"  -> compile_header dirname basename extension
401
  | ".lus"   -> compile_source dirname basename extension
402
  | _        -> assert false
403

    
404
let anonymous filename =
405
  let ok_ext, ext = List.fold_left
406
    (fun (ok, ext) ext' ->
407
      if not ok && Filename.check_suffix filename ext' then
408
	true, ext'
409
      else
410
	ok, ext)
411
    (false, "") extensions in
412
  if ok_ext then
413
    let dirname = Filename.dirname filename in
414
    let basename = Filename.chop_suffix (Filename.basename filename) ext in
415
    compile dirname basename ext
416
  else
417
    raise (Arg.Bad ("Can only compile *.lusi, *.lus or *.ec files"))
418

    
419
let _ =
420
  Global.initialize ();
421
  Corelang.add_internal_funs ();
422
  try
423
    Printexc.record_backtrace true;
424

    
425
    let options = Options_management.lustrec_options @ (Plugins.options ()) in
426
    
427
    Arg.parse options anonymous usage
428
  with
429
  | Parse.Error _
430
  | Types.Error (_,_) | Clocks.Error (_,_) -> exit 1
431
  | Corelang.Error (_ (* loc *), kind) (*| Task_set.Error _*) -> exit (Error.return_code kind)
432
  (* | Causality.Error _  -> exit (Error.return_code Error.AlgebraicLoop) *)
433
  | Sys_error msg -> (eprintf "Failure: %s@." msg)
434
  | exc -> (track_exception (); raise exc) 
435

    
436
(* Local Variables: *)
437
(* compile-command:"make -C .." *)
438
(* End: *)