Project

General

Profile

Download (18 KB) Statistics
| Branch: | Tag: | Revision:
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
  let do_generate_lusic, lusic_opt =
63
    if not (Sys.file_exists header_name) then
64
      true, None
65
    else
66
      let lusic = Lusic.read_lusic destname lusic_ext in
67
      not lusic.Lusic.from_lusi, Some lusic
68
  in
69
  if do_generate_lusic then
70
    begin
71
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
72
      Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
73
      generate_lusic_header destname lusic_ext
74
    end
75
  else
76
    begin
77
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
78
      let lusic = desome lusic_opt in
79
      Modules.check_dependency lusic destname;
80
      let header = lusic.Lusic.contents in
81
      let (declared_types_env, declared_clocks_env) = get_envs_from_top_decls header in
82
      check_compatibility
83
	(prog, computed_types_env, computed_clocks_env)
84
	(header, declared_types_env, declared_clocks_env)
85
    end
86
      
87
      
88
      
89
      (* begin *)
90
      (* 	if not (Sys.file_exists header_name) then *)
91
      (* 	  begin *)
92
      (* 	    Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name); *)
93
      (* 	    Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext; *)
94
      (* 	    Lusic.print_lusic_to_h destname lusic_ext *)
95
      (* 	  end *)
96
      (* 	else *)
97
      (* 	  let lusic = Lusic.read_lusic destname lusic_ext in *)
98
      (* 	  if not lusic.Lusic.from_lusi then *)
99
      (* 	    begin *)
100
      (* 	      Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name); *)
101
      (*  	      Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext; *)
102
      (* 	      (\*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*\) *)
103
      (* 	      Lusic.print_lusic_to_h destname lusic_ext *)
104
      (* 	    end *)
105
      (* 	  else *)
106
      (* 	    begin *)
107
      (* 	      Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name); *)
108
      (* 	      Modules.check_dependency lusic destname; *)
109
      (* 	      let header = lusic.Lusic.contents in *)
110
      (* 	      let (declared_types_env, declared_clocks_env) = get_envs_from_top_decls header in *)
111
      (* 	      check_compatibility *)
112
      (* 		(prog, computed_types_env, computed_clocks_env) *)
113
      (* 		(header, declared_types_env, declared_clocks_env) *)
114
      (* 	    end *)
115
      (* end *)
116

    
117

    
118

    
119
let dynamic_checks () =
120
  match !Options.output, !Options.spec with
121
  | "C", "C" -> true
122
  | _ -> false
123
     
124
(* From prog to prog *)
125
let stage1 prog dirname basename =
126
  (* Removing automata *) 
127
  let prog = expand_automata prog in
128

    
129
  Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@.@[<v 2>@ %a@]@," Printers.pp_prog prog);
130

    
131
  (* Importing source *)
132
  let _ = Modules.load_program ISet.empty prog in
133

    
134
  (* Extracting dependencies *)
135
  let dependencies, type_env, clock_env = import_dependencies prog in
136

    
137
  (* Sorting nodes *)
138
  let prog = SortProg.sort prog in
139

    
140
  (* Perform inlining before any analysis *)
141
  let orig, prog =
142
    if !Options.global_inline && !Options.main_node <> "" then
143
      (if !Options.witnesses then prog else []),
144
      Inliner.global_inline basename prog type_env clock_env
145
    else (* if !Option.has_local_inline *)
146
      [],
147
      Inliner.local_inline basename prog type_env clock_env
148
  in
149

    
150
  (* Checking stateless/stateful status *)
151
  if Plugins.check_force_stateful () then
152
    force_stateful_decls prog
153
  else
154
    check_stateless_decls prog;
155

    
156
  (* Typing *)
157
  let computed_types_env = type_decls type_env prog in
158

    
159
  (* Clock calculus *)
160
  let computed_clocks_env = clock_decls clock_env prog in
161

    
162
  (* Generating a .lusi header file only *)
163
  if !Options.lusi then
164
    (* We stop here the processing and produce the current prog. It will be
165
       exported as a lusi *)
166
    raise (StopPhase1 prog);
167

    
168
 (* Optimization of prog: 
169
     - Unfold consts 
170
     - eliminate trivial expressions
171
 *)
172
  (*
173
  let prog = 
174
    if !Options.const_unfold || !Options.optimization >= 5 then
175
      begin
176
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. eliminating constants and aliases@,");
177
	Optimize_prog.prog_unfold_consts prog
178
      end
179
    else
180
      prog
181
  in
182
  *)
183
  (* Delay calculus *)
184
  (* TO BE DONE LATER (Xavier)
185
    if(!Options.delay_calculus)
186
    then
187
    begin
188
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. initialisation analysis@?");
189
    try
190
    Delay_calculus.delay_prog Basic_library.delay_env prog
191
    with (Delay.Error (loc,err)) as exc ->
192
    Location.print loc;
193
    eprintf "%a" Delay.pp_error err;
194
    Utils.track_exception ();
195
    raise exc
196
    end;
197
  *)
198

    
199
  (* Creating destination directory if needed *)
200
  create_dest_dir ();
201

    
202
  (* Compatibility with Lusi *)
203
  (* Checking the existence of a lusi (Lustre Interface file) *)
204
  let extension = ".lusi" in
205
  compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension;
206

    
207
  Typing.uneval_prog_generics prog;
208
  Clock_calculus.uneval_prog_generics prog;
209

    
210
  
211
  if !Options.global_inline && !Options.main_node <> "" && !Options.witnesses then
212
    begin
213
      let orig = Corelang.copy_prog orig in
214
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating witness file@,");
215
      check_stateless_decls orig;
216
      let _ = Typing.type_prog type_env orig in
217
      let _ = Clock_calculus.clock_prog clock_env orig in
218
      Typing.uneval_prog_generics orig;
219
      Clock_calculus.uneval_prog_generics orig;
220
      Inliner.witness
221
	basename
222
	!Options.main_node
223
	orig prog type_env clock_env
224
    end;
225
  
226
  (* Computes and stores generic calls for each node,
227
     only useful for ANSI C90 compliant generic node compilation *)
228
  if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
229
  (*Hashtbl.iter (fun id td -> match td.Corelang.top_decl_desc with
230
    Corelang.Node nd -> Format.eprintf "%s calls %a" id
231
    Causality.NodeDep.pp_generic_calls nd | _ -> ()) Corelang.node_table;*)
232

    
233
  (* If some backend involving dynamic checks are active, then node annotations become runtime checks *)
234
  let prog =
235
    if dynamic_checks () then
236
      Spec.enforce_spec_prog prog
237
    else
238
      prog
239
  in
240
  
241
  (* Normalization phase *)
242
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
243
  (* Special treatment of arrows in lustre backend. We want to keep them *)
244
  if !Options.output = "lustre" then
245
    Normalization_common.unfold_arrow_active := false;
246
  let prog = Normalization.normalize_prog prog in
247
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
248

    
249
  let prog =
250
    if !Options.mpfr
251
    then
252
      begin
253
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. targetting MPFR library@,");
254
	Mpfr.inject_prog prog
255
      end
256
    else
257
      begin
258
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping floating-point numbers@,");
259
	prog
260
      end in
261
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
262

    
263
  (* Checking array accesses *)
264
  if !Options.check then
265
    begin
266
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking array accesses@,");
267
      Access.check_prog prog;
268
    end;
269

    
270
  prog, dependencies
271

    
272
(* from source to machine code, with optimization *)
273
let stage2 prog =    
274
  (* Computation of node equation scheduling. It also breaks dependency cycles
275
     and warns about unused input or memory variables *)
276
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. scheduling@,");
277
  let prog, node_schs = Scheduling.schedule_prog prog in
278
  Log.report ~level:1 (fun fmt -> fprintf fmt "%a"              Scheduling.pp_warning_unused node_schs);
279
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs);
280
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);
281
  Log.report ~level:5 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_dep_graph node_schs);
282
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
283

    
284

    
285
  (* TODO Salsa optimize prog: 
286
     - emits warning for programs with pre inside expressions
287
     - make sure each node arguments and memory is bounded by a local annotation
288
     - introduce fresh local variables for each real pure subexpression
289
  *)
290
  (* DFS with modular code generation *)
291
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@ ");
292
  let machine_code = Machine_code.translate_prog prog node_schs in
293

    
294
   (* Optimize machine code *)
295
  let machine_code =
296
    if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then
297
      begin
298
	Log.report ~level:1 
299
	  (fun fmt -> fprintf fmt ".. machines optimization: sub-expression elimination@,");
300
	Optimize_machine.machines_cse machine_code
301
      end
302
    else
303
      machine_code
304
  in
305
  (* Optimize machine code *)
306
  let machine_code, removed_table = 
307
    if !Options.optimization >= 2 (*&& !Options.output <> "horn"*) then
308
      begin
309
	Log.report ~level:1 (fun fmt -> fprintf fmt 
310
    ".. machines optimization: const. inlining (partial eval. with const)@,");
311
	Optimize_machine.machines_unfold (Corelang.get_consts prog) node_schs machine_code
312
      end
313
    else
314
      machine_code, IMap.empty
315
  in  
316
  (* Optimize machine code *)
317
  let machine_code =
318
    if !Options.optimization >= 3 && not (Corelang.functional_backend ()) then
319
      begin
320
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
321
	let node_schs    = Scheduling.remove_prog_inlined_locals removed_table node_schs in
322
	let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
323
	Optimize_machine.machines_fusion (Optimize_machine.machines_reuse_variables machine_code reuse_tables)
324
      end
325
    else
326
      machine_code
327
  in
328
  
329
  (* Salsa optimize machine code *)
330
  (*
331
  let machine_code = 
332
    if !Options.salsa_enabled then
333
      begin
334
	check_main ();
335
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization: optimizing floating-point accuracy with Salsa@,");
336
	(* Selecting float constants for Salsa *)
337
	let constEnv = List.fold_left (
338
	  fun accu c_topdecl ->
339
	    match c_topdecl.top_decl_desc with
340
	    | Const c when Types.is_real_type c.const_type  ->
341
	      (c.const_id, c.const_value) :: accu
342
	    | _ -> accu
343
	) [] (Corelang.get_consts prog) 
344
	in
345
	List.map 
346
	  (Machine_salsa_opt.machine_t2machine_t_optimized_by_salsa constEnv) 
347
	  machine_code 
348
      end
349
    else
350
      machine_code
351
  in
352
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@ "
353
    (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
354
    machine_code);
355
  *)
356
  machine_code
357

    
358

    
359
(* printing code *)
360
let stage3 prog machine_code dependencies basename =
361
  let basename    =  Filename.basename basename in
362
  match !Options.output with
363
    "C" -> 
364
      begin
365
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
366
	C_backend.translate_to_c
367
	  (* alloc_header_file source_lib_file source_main_file makefile_file *)
368
	  basename prog machine_code dependencies
369
      end
370
  | "java" ->
371
     begin
372
       (Format.eprintf "internal error: sorry, but not yet supported !"; assert false)
373
     (*let source_file = basename ^ ".java" in
374
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
375
       let source_out = open_out source_file in
376
       let source_fmt = formatter_of_out_channel source_out in
377
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
378
       Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
379
     end
380
  | "horn" ->
381
     begin
382
       let destname = !Options.dest_dir ^ "/" ^ basename in
383
       let source_file = destname ^ ".smt2" in (* Could be changed *)
384
       let source_out = open_out source_file in
385
       let fmt = formatter_of_out_channel source_out in
386
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
387
       Horn_backend.translate fmt basename prog (Machine_code.arrow_machine::machine_code);
388
       (* Tracability file if option is activated *)
389
       if !Options.traces then (
390
	 let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
391
	 let traces_out = open_out traces_file in
392
	 let fmt = formatter_of_out_channel traces_out in
393
         Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
394
	 Horn_backend_traces.traces_file fmt basename prog machine_code;
395
       )
396
     end
397
  | "lustre" ->
398
     begin
399
       let destname = !Options.dest_dir ^ "/" ^ basename in
400
       let source_file = destname ^ ".lustrec.lus" in (* Could be changed *)
401
       let source_out = open_out source_file in
402
       let fmt = formatter_of_out_channel source_out in
403
       Printers.pp_prog fmt prog;
404
       (*	Lustre_backend.translate fmt basename normalized_prog machine_code *)
405
       ()
406
     end
407
  | "emf" ->
408
     begin
409
       let destname = !Options.dest_dir ^ "/" ^ basename in
410
       let source_file = destname ^ ".emf" in (* Could be changed *)
411
       let source_out = open_out source_file in
412
       let fmt = formatter_of_out_channel source_out in
413
       EMF_backend.translate fmt prog machine_code;
414
       ()
415
     end
416

    
417
  | _ -> assert false
418

    
419
(* compile a .lus source file *)
420
let rec compile_source dirname basename extension =
421
  let source_name = dirname ^ "/" ^ basename ^ extension in
422

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

    
425
  (* Parsing source *)
426
  let prog = parse_source source_name in
427

    
428
  let prog =
429
    if !Options.mpfr then
430
      Mpfr.mpfr_module::prog
431
    else
432
      prog
433
  in
434
  let prog, dependencies = 
435
    try 
436
      stage1 prog dirname basename
437
    with StopPhase1 prog -> (
438
      if !Options.lusi then
439
	begin
440
	  let lusi_ext = extension ^ "i" in
441
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating interface file %s@," (basename ^ lusi_ext));
442
	  print_lusi prog dirname basename lusi_ext;
443
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
444
	  exit 0
445
	end
446
      else
447
        assert false
448
    )
449
  in
450

    
451
  let machine_code = 
452
    stage2 prog 
453
  in
454
  if Scopes.Plugin.show_scopes () then
455
    begin
456
      let all_scopes = Scopes.compute_scopes prog !Options.main_node in
457
      (* Printing scopes *)
458
      if !Options.verbose_level >= 1 then
459
	Format.printf "Possible scopes are:@   ";
460
      Format.printf "@[<v>%a@ @]@.@?" Scopes.print_scopes all_scopes;
461
      exit 0
462
	
463
    end;
464

    
465
  let machine_code = Plugins.refine_machine_code prog machine_code in
466
  
467
  stage3 prog machine_code dependencies basename;
468
  begin
469
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
470
    (* We stop the process here *)
471
    exit 0
472
  end
473

    
474
let compile dirname basename extension =
475
  match extension with
476
  | ".lusi"  -> compile_header dirname basename extension
477
  | ".lus"   -> compile_source dirname basename extension
478
  | _        -> assert false
479

    
480
let anonymous filename =
481
  let ok_ext, ext = List.fold_left
482
    (fun (ok, ext) ext' ->
483
      if not ok && Filename.check_suffix filename ext' then
484
	true, ext'
485
      else
486
	ok, ext)
487
    (false, "") extensions in
488
  if ok_ext then
489
    let dirname = Filename.dirname filename in
490
    let basename = Filename.chop_suffix (Filename.basename filename) ext in
491
    compile dirname basename ext
492
  else
493
    raise (Arg.Bad ("Can only compile *.lusi, *.lus or *.ec files"))
494

    
495
let _ =
496
  Global.initialize ();
497
  Corelang.add_internal_funs ();
498
  try
499
    Printexc.record_backtrace true;
500

    
501
    let options = Options.lustrec_options @ (Plugins.options ()) in
502
    
503
    Arg.parse options anonymous usage
504
  with
505
  | Parse.Error _
506
  | Types.Error (_,_) | Clocks.Error (_,_)
507
  | Corelang.Error _ (*| Task_set.Error _*)
508
  | Causality.Error _ -> exit 1
509
  | Sys_error msg -> (eprintf "Failure: %s@." msg)
510
  | exc -> (Utils.track_exception (); raise exc)
511

    
512
(* Local Variables: *)
513
(* compile-command:"make -C .." *)
514
(* End: *)
(33-33/62)