Project

General

Profile

Revision 45f0f48d src/main_lustre_compiler.ml

View differences:

src/main_lustre_compiler.ml
88 88
  end
89 89

  
90 90

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

  
91 96
(* From prog to prog *)
92 97
let stage1 prog dirname basename =
93 98
  (* Removing automata *) 
......
122 127

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

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

  
......
148 153
  in
149 154
  *)
150 155
  (* Delay calculus *)
151
  (*
156
  (* TO BE DONE LATER (Xavier)
152 157
    if(!Options.delay_calculus)
153 158
    then
154 159
    begin
......
213 218
      end
214 219
    else
215 220
      begin
216
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping FP numbers@,");
221
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping floating-point numbers@,");
217 222
	prog
218 223
      end in
219 224
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
......
221 226
  (* Checking array accesses *)
222 227
  if !Options.check then
223 228
    begin
224
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. array access checks@,");
229
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking array accesses@,");
225 230
      Access.check_prog prog;
226 231
    end;
227 232

  
......
257 262
  let machine_code =
258 263
    if !Options.optimization >= 4 && !Options.output <> "horn" then
259 264
      begin
260
	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@,");
261 266
	Optimize_machine.machines_cse machine_code
262 267
      end
263 268
    else
......
267 272
  let machine_code, removed_table = 
268 273
    if !Options.optimization >= 2 && !Options.output <> "horn" then
269 274
      begin
270
	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@,");
271 276
	Optimize_machine.machines_unfold (Corelang.get_consts prog) node_schs machine_code
272 277
      end
273 278
    else
......
277 282
  let machine_code = 
278 283
    if !Options.optimization >= 3 && !Options.output <> "horn" then
279 284
      begin
280
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 2)@ ");
285
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
281 286
	let node_schs    = Scheduling.remove_prog_inlined_locals removed_table node_schs in
282 287
	let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
283 288
	Optimize_machine.machines_fusion (Optimize_machine.machines_reuse_variables machine_code reuse_tables)
......
292 297
    if !Options.salsa_enabled then
293 298
      begin
294 299
	check_main ();
295
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization (phase 3)@ ");
300
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization: optimizing floating-point accuracy with Salsa@,");
296 301
	(* Selecting float constants for Salsa *)
297 302
	let constEnv = List.fold_left (
298 303
	  fun accu c_topdecl ->
......
348 353
	let source_out = open_out source_file in
349 354
	let fmt = formatter_of_out_channel source_out in
350 355
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
351
        Horn_backend.translate fmt basename prog machine_code;
356
        Horn_backend.translate fmt basename prog (Machine_code.arrow_machine::machine_code);
352 357
	(* Tracability file if option is activated *)
353 358
	if !Options.traces then (
354
	let traces_file = destname ^ ".traces" in (* Could be changed *)
359
	let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
355 360
	let traces_out = open_out traces_file in
356 361
	let fmt = formatter_of_out_channel traces_out in
357 362
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
358
	Horn_backend.traces_file fmt basename prog machine_code;
363
	Horn_backend_traces.traces_file fmt basename prog machine_code;
359 364
	)
360 365
      end
361 366
    | "lustre" ->

Also available in: Unified diff