Project

General

Profile

Revision 3b2bd83d src/main_lustre_compiler.ml

View differences:

src/main_lustre_compiler.ml
15 15
open Utils
16 16
open LustreSpec
17 17
open Compiler_common
18
 
19
exception StopPhase1 of program
18 20

  
19
let usage = "Usage: lustrec [options] <source-file>"
21
let usage = "Usage: lustrec [options] \x1b[4msource file\x1b[0m"
20 22

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

  
......
86 88
  end
87 89

  
88 90

  
91
let functional_backend () = 
92
  match !Options.output with
93
  | "horn" | "lustre" | "acsl" -> true
94
  | _ -> false
89 95

  
90
(* compile a .lus source file *)
91
let rec compile_source dirname basename extension =
92

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

  
95
  (* Parsing source *)
96
  let prog = parse_source (dirname ^ "/" ^ basename ^ extension) in
96
(* From prog to prog *)
97
let stage1 prog dirname basename =
98
  (* Removing automata *) 
99
  let prog = expand_automata prog in
97 100

  
98
  (* Removing automata *)
99
  let prog = Automata.expand_decls prog in
100

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

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

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

  
125 128
  (* Typing *)
126 129
  let computed_types_env = type_decls type_env prog in
......
130 133

  
131 134
  (* Generating a .lusi header file only *)
132 135
  if !Options.lusi then
133
    begin
134
      let lusi_ext = extension ^ "i" in
135
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating interface file %s@," (dirname ^ "/" ^ basename ^ lusi_ext));
136
      print_lusi prog dirname basename lusi_ext;
137
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
138
      exit 0
139
    end;
136
    (* We stop here the processing and produce the current prog. It will be
137
       exported as a lusi *)
138
    raise (StopPhase1 prog);
140 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
  *)
141 155
  (* Delay calculus *)
142 156
  (* TO BE DONE LATER (Xavier)
143 157
    if(!Options.delay_calculus)
......
159 173

  
160 174
  (* Compatibility with Lusi *)
161 175
  (* Checking the existence of a lusi (Lustre Interface file) *)
162
  (match !Options.output with
163
    "C" ->
164
      begin
165
        let extension = ".lusi" in
166
        compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension;
167
      end
168
   |_ -> ());
176
  let extension = ".lusi" in
177
  compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension;
169 178

  
170 179
  Typing.uneval_prog_generics prog;
171 180
  Clock_calculus.uneval_prog_generics prog;
......
184 193
	!Options.main_node
185 194
	orig prog type_env clock_env
186 195
    end;
187

  
188
(*Format.eprintf "Inliner.global_inline<<@.%a@.>>@." Printers.pp_prog prog;*)
196
  
189 197
  (* Computes and stores generic calls for each node,
190 198
     only useful for ANSI C90 compliant generic node compilation *)
191 199
  if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
192
  (*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;*)
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;*)
193 203

  
194 204
  (* Normalization phase *)
195 205
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
......
197 207
  if !Options.output = "lustre" then
198 208
    Normalization.unfold_arrow_active := false;
199 209
  let prog = Normalization.normalize_prog prog in
210
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
200 211

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

  
202 226
  (* Checking array accesses *)
203 227
  if !Options.check then
204 228
    begin
205
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. array access checks@,");
229
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking array accesses@,");
206 230
      Access.check_prog prog;
207 231
    end;
208 232

  
233
  prog, dependencies
234

  
235
(* from source to machine code, with optimization *)
236
let stage2 prog =    
209 237
  (* Computation of node equation scheduling. It also breaks dependency cycles
210 238
     and warns about unused input or memory variables *)
211 239
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. scheduling@,");
212 240
  let prog, node_schs = Scheduling.schedule_prog prog in
213
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_warning_unused node_schs);
241
  Log.report ~level:1 (fun fmt -> fprintf fmt "%a"              Scheduling.pp_warning_unused node_schs);
214 242
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs);
215 243
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);
244
  Log.report ~level:5 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_dep_graph node_schs);
216 245
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
217 246

  
218
 (* Optimization of prog:
219
    - Unfold consts
220
    - eliminate trivial expressions
221
 *)
222
  let prog =
223
    if !Options.optimization >= 5 then
224
      begin
225
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. constants elimination@,");
226
	Optimize_prog.prog_unfold_consts prog
227
      end
228
    else
229
      prog
230
  in
247

  
248
  (* TODO Salsa optimize prog: 
249
     - emits warning for programs with pre inside expressions
250
     - make sure each node arguments and memory is bounded by a local annotation
251
     - introduce fresh local variables for each real pure subexpression
252
  *)
231 253
  (* DFS with modular code generation *)
232
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,");
254
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@ ");
233 255
  let machine_code = Machine_code.translate_prog prog node_schs in
234 256

  
235
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
257
  Log.report ~level:4 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
236 258
  (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
237
  machine_code);
259
    machine_code);
238 260

  
239 261
  (* Optimize machine code *)
240 262
  let machine_code =
241 263
    if !Options.optimization >= 4 && !Options.output <> "horn" then
242 264
      begin
243
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 3)@,");
265
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: common sub-expression elimination@,");
244 266
	Optimize_machine.machines_cse machine_code
245 267
      end
246 268
    else
247 269
      machine_code
248 270
  in
249

  
250 271
  (* Optimize machine code *)
251
  let machine_code =
272
  let machine_code, removed_table = 
252 273
    if !Options.optimization >= 2 && !Options.output <> "horn" then
253 274
      begin
254
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 1)@,");
275
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: constants inlining@,");
255 276
	Optimize_machine.machines_unfold (Corelang.get_consts prog) node_schs machine_code
256 277
      end
257 278
    else
258
      machine_code
259
  in
279
      machine_code, IMap.empty
280
  in  
260 281
  (* Optimize machine code *)
261
  let machine_code =
282
  let machine_code = 
262 283
    if !Options.optimization >= 3 && !Options.output <> "horn" then
263 284
      begin
264
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 2)@,");
265
	Optimize_machine.machines_fusion (Optimize_machine.machines_reuse_variables machine_code node_schs)
285
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
286
	let node_schs    = Scheduling.remove_prog_inlined_locals removed_table node_schs in
287
	let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
288
	Optimize_machine.machines_fusion (Optimize_machine.machines_reuse_variables machine_code reuse_tables)
266 289
      end
267 290
    else
268 291
      machine_code
269 292
  in
293
  
294
  (* Salsa optimize machine code *)
295
  (*
296
  let machine_code = 
297
    if !Options.salsa_enabled then
298
      begin
299
	check_main ();
300
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization: optimizing floating-point accuracy with Salsa@,");
301
	(* Selecting float constants for Salsa *)
302
	let constEnv = List.fold_left (
303
	  fun accu c_topdecl ->
304
	    match c_topdecl.top_decl_desc with
305
	    | Const c when Types.is_real_type c.const_type  ->
306
	      (c.const_id, c.const_value) :: accu
307
	    | _ -> accu
308
	) [] (Corelang.get_consts prog) 
309
	in
310
	List.map 
311
	  (Machine_salsa_opt.machine_t2machine_t_optimized_by_salsa constEnv) 
312
	  machine_code 
313
      end
314
    else
315
      machine_code
316
  in
317
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@ "
318
    (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
319
    machine_code);
320
  *)
321
  machine_code
270 322

  
271
  if !Options.optimization >= 2 then
272
    begin
273
      Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
274
	(Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
275
	machine_code);
276
    end;
277 323

  
278
  (* Printing code *)
324
(* printing code *)
325
let stage3 prog machine_code dependencies basename =
279 326
  let basename    =  Filename.basename basename in
280
  let destname = !Options.dest_dir ^ "/" ^ basename in
281
  let _ = match !Options.output with
282
    | "C" ->
283
      begin
284
	  let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *)
285
	  let source_lib_file = destname ^ ".c" in (* Could be changed *)
286
	  let source_main_file = destname ^ "_main.c" in (* Could be changed *)
287
	  let makefile_file = destname ^ ".makefile" in (* Could be changed *)
288
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
289
	  C_backend.translate_to_c
290
	    alloc_header_file source_lib_file source_main_file makefile_file
291
	    basename prog machine_code dependencies
292
	end
293
    | "java" ->
294
      begin
295
	failwith "Sorry, but not yet supported !"
296
    (*let source_file = basename ^ ".java" in
297
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
298
      let source_out = open_out source_file in
299
      let source_fmt = formatter_of_out_channel source_out in
300
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
301
      Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
302
      end
303
    | "horn" ->
304
       begin
305
	let source_file = destname ^ ".smt2" in (* Could be changed *)
306
	let source_out = open_out source_file in
307
	let fmt = formatter_of_out_channel source_out in
308
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
309
        Horn_backend.translate fmt basename prog machine_code;
310
	(* Tracability file if option is activated *)
311
	if !Options.traces then (
312
	let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
313
	let traces_out = open_out traces_file in
314
	let fmt = formatter_of_out_channel traces_out in
315
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
316
	Horn_backend.traces_file fmt basename prog machine_code;
317
	)
318
      end
319
    | "lustre" ->
327
  match !Options.output with
328
    "C" -> 
320 329
      begin
321
	let source_file = destname ^ ".lustrec.lus" in (* Could be changed *)
322
	let source_out = open_out source_file in
323
	let fmt = formatter_of_out_channel source_out in
324
	Printers.pp_prog fmt prog;
325
(*	Lustre_backend.translate fmt basename normalized_prog machine_code *)
326
	()
330
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
331
	C_backend.translate_to_c
332
	  (* alloc_header_file source_lib_file source_main_file makefile_file *)
333
	  basename prog machine_code dependencies
327 334
      end
335
  | "java" ->
336
     begin
337
       (Format.eprintf "internal error: sorry, but not yet supported !"; assert false)
338
     (*let source_file = basename ^ ".java" in
339
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
340
       let source_out = open_out source_file in
341
       let source_fmt = formatter_of_out_channel source_out in
342
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
343
       Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
344
     end
345
  | "horn" ->
346
     begin
347
       let destname = !Options.dest_dir ^ "/" ^ basename in
348
       let source_file = destname ^ ".smt2" in (* Could be changed *)
349
       let source_out = open_out source_file in
350
       let fmt = formatter_of_out_channel source_out in
351
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
352
       Horn_backend.translate fmt basename prog (Machine_code.arrow_machine::machine_code);
353
       (* Tracability file if option is activated *)
354
       if !Options.traces then (
355
	 let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
356
	 let traces_out = open_out traces_file in
357
	 let fmt = formatter_of_out_channel traces_out in
358
         Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
359
	 Horn_backend_traces.traces_file fmt basename prog machine_code;
360
       )
361
     end
362
  | "lustre" ->
363
     begin
364
       let destname = !Options.dest_dir ^ "/" ^ basename in
365
       let source_file = destname ^ ".lustrec.lus" in (* Could be changed *)
366
       let source_out = open_out source_file in
367
       let fmt = formatter_of_out_channel source_out in
368
       Printers.pp_prog fmt prog;
369
       (*	Lustre_backend.translate fmt basename normalized_prog machine_code *)
370
       ()
371
     end
372

  
373
  | _ -> assert false
374

  
375
(* compile a .lus source file *)
376
let rec compile_source dirname basename extension =
377
  let source_name = dirname ^ "/" ^ basename ^ extension in
378

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

  
329
    | _ -> assert false
381
  (* Parsing source *)
382
  let prog = parse_source source_name in
383

  
384
  let prog =
385
    if !Options.mpfr then
386
      Mpfr.mpfr_module::prog
387
    else
388
      prog
389
  in
390
  let prog, dependencies = 
391
    try 
392
      stage1 prog dirname basename
393
    with StopPhase1 prog -> (
394
      if !Options.lusi then
395
	begin
396
	  let lusi_ext = extension ^ "i" in
397
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating interface file %s@," (basename ^ lusi_ext));
398
	  print_lusi prog dirname basename lusi_ext;
399
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
400
	  exit 0
401
	end
402
      else
403
        assert false
404
    )
330 405
  in
331
  begin
332
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done @ @]@.");
333
  (* We stop the process here *)
334
    exit 0
335
  end
406

  
407
  let machine_code = 
408
    stage2 prog 
409
  in
410
  if Scopes.Plugin.show_scopes () then
411
    begin
412
      let all_scopes = Scopes.compute_scopes prog !Options.main_node in
413
      (* Printing scopes *)
414
      if !Options.verbose_level >= 1 then
415
	Format.printf "Possible scopes are:@   ";
416
      Format.printf "@[<v>%a@ @]@.@?" Scopes.print_scopes all_scopes;
417
      exit 0
418
	
419
    end;
420

  
421
  let machine_code = 
422
    if Scopes.Plugin.is_active () then
423
      Scopes.Plugin.process_scopes !Options.main_node prog machine_code
424
    else
425
      machine_code
426
  in
427
  
428
  stage3 prog machine_code dependencies basename;
429
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. done @ @]@.");
430
    (* We stop the process here *)
431
  exit 0
336 432

  
337 433
let compile dirname basename extension =
338 434
  match extension with
......
356 452
    raise (Arg.Bad ("Can only compile *.lusi, *.lus or *.ec files"))
357 453

  
358 454
let _ =
455
  Global.initialize ();
359 456
  Corelang.add_internal_funs ();
360 457
  try
361 458
    Printexc.record_backtrace true;
362
    Arg.parse Options.options anonymous usage
459

  
460
    let options = Options.options @ 
461
      List.flatten (
462
	List.map Options.plugin_opt [
463
	  Scopes.Plugin.name, Scopes.Plugin.activate, Scopes.Plugin.options
464
	]
465
      )
466
    in
467
    
468
    Arg.parse options anonymous usage
363 469
  with
364
  | Parse.Syntax_err _ | Lexer_lustre.Error _
470
  | Parse.Error _
365 471
  | Types.Error (_,_) | Clocks.Error (_,_)
366 472
  | Corelang.Error _ (*| Task_set.Error _*)
367
  | Causality.Cycle _ -> exit 1
473
  | Causality.Error _ -> exit 1
368 474
  | Sys_error msg -> (eprintf "Failure: %s@." msg)
369 475
  | exc -> (Utils.track_exception (); raise exc)
370 476

  

Also available in: Unified diff