Project

General

Profile

« Previous | Next » 

Revision 66359a5e

Added by Pierre-Loïc Garoche about 7 years ago

[general] large modification: added machine types, a second typing phase dealing with machine types (eg uint8)
typing was transformed as a functor and parametrized by basic types (int/real/bool)
it can also be applied multiple times on the same program

View differences:

src/main_lustre_compiler.ml
55 55

  
56 56

  
57 57

  
58
(* from source to machine code, with optimization *)
59
let stage2 prog =    
60
  (* Computation of node equation scheduling. It also breaks dependency cycles
61
     and warns about unused input or memory variables *)
62
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. @[<v 2>scheduling@ ");
63
  let prog, node_schs =
64
    try 
65
      Scheduling.schedule_prog prog
66
    with Causality.Error _ -> (* Error is not kept. It is recomputed in a more
67
				 systemtic way in AlgebraicLoop module *)
68
      AlgebraicLoop.analyze prog
69
  in
70
  Log.report ~level:1 (fun fmt -> fprintf fmt "%a"              Scheduling.pp_warning_unused node_schs);
71
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs);
72
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);
73
  Log.report ~level:5 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_dep_graph node_schs);
74
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
75
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
76

  
77
  (* TODO Salsa optimize prog: 
78
     - emits warning for programs with pre inside expressions
79
     - make sure each node arguments and memory is bounded by a local annotation
80
     - introduce fresh local variables for each real pure subexpression
81
  *)
82
  (* DFS with modular code generation *)
83
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,");
84
  let machine_code = Machine_code.translate_prog prog node_schs in
85

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

  
88
  (* Optimize machine code *)
89
  Optimize_machine.optimize prog node_schs machine_code
90

  
91

  
92
(* printing code *)
93
let stage3 prog machine_code dependencies basename =
94
  let basename    =  Filename.basename basename in
95
  match !Options.output with
96
    "C" -> 
97
      begin
98
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
99
	C_backend.translate_to_c
100
	  (* alloc_header_file source_lib_file source_main_file makefile_file *)
101
	  basename prog machine_code dependencies
102
      end
103
  | "java" ->
104
     begin
105
       (Format.eprintf "internal error: sorry, but not yet supported !"; assert false)
106
     (*let source_file = basename ^ ".java" in
107
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
108
       let source_out = open_out source_file in
109
       let source_fmt = formatter_of_out_channel source_out in
110
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
111
       Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
112
     end
113
  | "horn" ->
114
     begin
115
       let destname = !Options.dest_dir ^ "/" ^ basename in
116
       let source_file = destname ^ ".smt2" in (* Could be changed *)
117
       let source_out = open_out source_file in
118
       let fmt = formatter_of_out_channel source_out in
119
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
120
       Horn_backend.translate fmt basename prog (Machine_code.arrow_machine::machine_code);
121
       (* Tracability file if option is activated *)
122
       if !Options.traces then (
123
	 let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
124
	 let traces_out = open_out traces_file in
125
	 let fmt = formatter_of_out_channel traces_out in
126
         Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
127
	 Horn_backend_traces.traces_file fmt basename prog machine_code;
128
       )
129
     end
130
  | "lustre" ->
131
     begin
132
       let destname = !Options.dest_dir ^ "/" ^ basename in
133
       let source_file = destname ^ ".lustrec.lus" in (* Could be changed *)
134
       let source_out = open_out source_file in
135
       let fmt = formatter_of_out_channel source_out in
136
       Printers.pp_prog fmt prog;
137
       Format.fprintf fmt "@.@?";
138
       (*	Lustre_backend.translate fmt basename normalized_prog machine_code *)
139
       ()
140
     end
141
  | "emf" ->
142
     begin
143
       let destname = !Options.dest_dir ^ "/" ^ basename in
144
       let source_file = destname ^ ".emf" in (* Could be changed *)
145
       let source_out = open_out source_file in
146
       let fmt = formatter_of_out_channel source_out in
147
       EMF_backend.translate fmt basename prog machine_code;
148
       ()
149
     end
150

  
151
  | _ -> assert false
152 58

  
153 59
(* compile a .lus source file *)
154 60
let rec compile_source dirname basename extension =
......
188 94
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 2 : Machines generation@,");
189 95

  
190 96
  let machine_code = 
191
    stage2 prog 
97
    Compiler_stages.stage2 prog 
192 98
  in
193 99

  
194 100
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
......
207 113

  
208 114
  let machine_code = Plugins.refine_machine_code prog machine_code in
209 115
  
210
  stage3 prog machine_code dependencies basename;
116
  Compiler_stages.stage3 prog machine_code dependencies basename;
211 117
  begin
212 118
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
213 119
    (* We stop the process here *)

Also available in: Unified diff