Project

General

Profile

Revision 13507742

View differences:

src/backends/backends.ml
1 1
(* Backend-specific options *)
2 2
let join_guards = ref true
3 3

  
4
let setup s =
5
  match s with
6
  | "emf" ->
7
     join_guards := true; (* guards should not be joined, in order to have only
8
			      if c then x = e1 else x = e2 to ease
9
			      reconstruction of flows. *)
10
    Options.optimization := 0; (* Optimization=0 prevents expression
11
				  elimination. This simplifies largely the
12
				  association of lustre expression to
13
				  instructions *)
4
let setup () =
5
  match !Options.output with
6
  (* | "emf" -> *)
7
  (*    join_guards := true; (\* guards should not be joined, in order to have only *)
8
  (* 			      if c then x = e1 else x = e2 to ease *)
9
  (* 			      reconstruction of flows. *\) *)
10
  (*   Options.optimization := 0; (\* Optimization=0 prevents expression *)
11
  (* 				  elimination. This simplifies largely the *)
12
  (* 				  association of lustre expression to *)
13
  (* 				  instructions *\) *)
14 14
  | _ -> ()
15 15

  
16
let is_functional () = 
17
  match !Options.output with
18
  | "horn" | "lustre" | "acsl" | "emf" -> true
19
  | _ -> false
20

  
21
  
16 22
(* Local Variables: *)
17 23
(* compile-command: "make -k -C .." *)
18 24
(* End: *)
src/corelang.ml
1065 1065
let copy_prog top_list =
1066 1066
  List.map copy_top top_list
1067 1067

  
1068
let functional_backend () = 
1069
  match !Options.output with
1070
  | "horn" | "lustre" | "acsl" -> true
1071
  | _ -> false
1072

  
1073 1068
(* Local Variables: *)
1074 1069
(* compile-command:"make -C .." *)
1075 1070
(* End: *)
src/corelang.mli
144 144
val update_expr_annot: ident -> expr -> expr_annot -> expr
145 145
(* val mkpredef_call: Location.t -> ident -> eexpr list -> eexpr*)
146 146

  
147
val functional_backend: unit -> bool
148 147
(* Local Variables: *)
149 148
(* compile-command:"make -C .." *)
150 149
(* End: *)
src/machine_code.ml
602 602
     to be declared for each assert *)
603 603
  let new_locals, assert_instrs, nd_node_asserts =
604 604
    let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
605
    if Corelang.functional_backend () then
605
    if Backends.is_functional () then
606 606
      [], [], exprl  
607 607
    else (* Each assert(e) is associated to a fresh variable v and declared as
608 608
	    v=e; assert (v); *)
src/main_lustre_compiler.ml
262 262
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (unoptimized):@ %a@ "Machine_code.pp_machines machine_code);
263 263

  
264 264
  (* Optimize machine code *)
265
  let machine_code =
266
    if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then
267
      begin
268
	Log.report ~level:1 
269
	  (fun fmt -> fprintf fmt ".. machines optimization: sub-expression elimination@,");
270
	let machine_code = Optimize_machine.machines_cse machine_code in
271
	Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (sub-expr elim):@ %a@ "Machine_code.pp_machines machine_code);
272
	machine_code
273
      end
274
    else
275
      machine_code
276
  in
277
  (* Optimize machine code *)
278
  let machine_code, removed_table = 
279
    if !Options.optimization >= 2 (*&& !Options.output <> "horn"*) then
280
      begin
281
	Log.report ~level:1 (fun fmt -> fprintf fmt 
282
	  ".. machines optimization: const. inlining (partial eval. with const)@,");
283
	let machine_code, removed_table = Optimize_machine.machines_unfold (Corelang.get_consts prog) node_schs machine_code in
284
	Log.report ~level:3 (fun fmt -> fprintf fmt "\t@[Eliminated constants: @[%a@]@]@ "
285
	  (pp_imap Optimize_machine.pp_elim) removed_table);
286
	Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (const inlining):@ %a@ "Machine_code.pp_machines machine_code);	
287
	machine_code, removed_table
288
      end
289
    else
290
      machine_code, IMap.empty
291
  in  
292
  (* Optimize machine code *)
293
  let machine_code =
294
    if !Options.optimization >= 3 && not (Corelang.functional_backend ()) then
295
      begin
296
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
297
	let node_schs    = Scheduling.remove_prog_inlined_locals removed_table node_schs in
298
	let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
299
	Optimize_machine.machines_fusion (Optimize_machine.machines_reuse_variables machine_code reuse_tables)
300
      end
301
    else
302
      machine_code
303
  in
304
  
305
  (* Salsa optimize machine code *)
306
  (*
307
  let machine_code = 
308
    if !Options.salsa_enabled then
309
      begin
310
	check_main ();
311
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization: optimizing floating-point accuracy with Salsa@,");
312
	(* Selecting float constants for Salsa *)
313
	let constEnv = List.fold_left (
314
	  fun accu c_topdecl ->
315
	    match c_topdecl.top_decl_desc with
316
	    | Const c when Types.is_real_type c.const_type  ->
317
	      (c.const_id, c.const_value) :: accu
318
	    | _ -> accu
319
	) [] (Corelang.get_consts prog) 
320
	in
321
	List.map 
322
	  (Machine_salsa_opt.machine_t2machine_t_optimized_by_salsa constEnv) 
323
	  machine_code 
324
      end
325
    else
326
      machine_code
327
  in
328
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@ "
329
    (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
330
    machine_code);
331
  *)
332
  machine_code
265
  Optimize_machine.optimize prog node_schs machine_code
333 266

  
334 267

  
335 268
(* printing code *)
src/optimize_machine.ml
567 567
let machines_fusion prog =
568 568
  List.map machine_fusion prog
569 569

  
570

  
571
(*** Main function ***)
572
    
573
let optimize prog node_schs machine_code =
574
  let machine_code =
575
    if !Options.optimization >= 4 (* && !Options.output <> "horn" *) then
576
      begin
577
	Log.report ~level:1 
578
	  (fun fmt -> Format.fprintf fmt ".. machines optimization: sub-expression elimination@,");
579
	let machine_code = machines_cse machine_code in
580
	Log.report ~level:3 (fun fmt -> Format.fprintf fmt ".. generated machines (sub-expr elim):@ %a@ "Machine_code.pp_machines machine_code);
581
	machine_code
582
      end
583
    else
584
      machine_code
585
  in
586
  (* Optimize machine code *)
587
  let machine_code, removed_table = 
588
    if !Options.optimization >= 2 && !Options.output <> "emf" (*&& !Options.output <> "horn"*) then
589
      begin
590
	Log.report ~level:1 (fun fmt -> Format.fprintf fmt 
591
	  ".. machines optimization: const. inlining (partial eval. with const)@,");
592
	let machine_code, removed_table = machines_unfold (Corelang.get_consts prog) node_schs machine_code in
593
	Log.report ~level:3 (fun fmt -> Format.fprintf fmt "\t@[Eliminated constants: @[%a@]@]@ "
594
	  (pp_imap pp_elim) removed_table);
595
	Log.report ~level:3 (fun fmt -> Format.fprintf fmt ".. generated machines (const inlining):@ %a@ "Machine_code.pp_machines machine_code);	
596
	machine_code, removed_table
597
      end
598
    else
599
      machine_code, IMap.empty
600
  in  
601
  (* Optimize machine code *)
602
  let machine_code =
603
    if !Options.optimization >= 3 && not (Backends.is_functional ()) then
604
      begin
605
	Log.report ~level:1 (fun fmt -> Format.fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
606
	let node_schs    = Scheduling.remove_prog_inlined_locals removed_table node_schs in
607
	let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
608
	machines_fusion (machines_reuse_variables machine_code reuse_tables)
609
      end
610
    else
611
      machine_code
612
  in
613
  
614
  (* Salsa optimize machine code *)
615
  (*
616
  let machine_code = 
617
    if !Options.salsa_enabled then
618
      begin
619
	check_main ();
620
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization: optimizing floating-point accuracy with Salsa@,");
621
	(* Selecting float constants for Salsa *)
622
	let constEnv = List.fold_left (
623
	  fun accu c_topdecl ->
624
	    match c_topdecl.top_decl_desc with
625
	    | Const c when Types.is_real_type c.const_type  ->
626
	      (c.const_id, c.const_value) :: accu
627
	    | _ -> accu
628
	) [] (Corelang.get_consts prog) 
629
	in
630
	List.map 
631
	  (Machine_salsa_opt.machine_t2machine_t_optimized_by_salsa constEnv) 
632
	  machine_code 
633
      end
634
    else
635
      machine_code
636
  in
637
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@ "
638
    (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
639
    machine_code);
640
  *)
641

  
642

  
643
    machine_code  
644
    
645
    
570 646
(* Local Variables: *)
571 647
(* compile-command:"make -C .." *)
572 648
(* End: *)
src/options_management.ml
73 73

  
74 74
let set_backend s =
75 75
  output := s;
76
  Backends.setup s
76
  Backends.setup ()
77 77

  
78 78
let common_options =
79 79
  [ "-d", Arg.Set_string dest_dir, "uses the specified \x1b[4mdirectory\x1b[0m as root for generated/imported object and C files <default: .>";

Also available in: Unified diff