Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / compiler_stages.ml @ ef776f2f

History | View | Annotate | Download (11.4 KB)

1
open Format
2
open Utils
3
open Compiler_common
4
open Lustre_types
5

    
6
exception StopPhase1 of program_t
7

    
8
let dynamic_checks () =
9
  match !Options.output, !Options.spec with
10
  | "C", "C" -> true
11
  | _ -> false
12
     
13

    
14
(* check whether a source file has a compiled header, if not, generate the
15
   compiled header *)
16
let compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension =
17
  let destname = !Options.dest_dir ^ "/" ^ basename in
18
  let lusic_ext = extension ^ "c" in
19
  let header_name = destname ^ lusic_ext in
20
  begin
21
    if not (Sys.file_exists header_name) then
22
      begin
23
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
24
	Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
25
	if !Options.output = "C" then
26
	  Lusic.print_lusic_to_h destname lusic_ext
27
      end
28
    else
29
      let lusic = Lusic.read_lusic destname lusic_ext in
30
      if not lusic.Lusic.from_lusi then
31
	begin
32
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
33
       	  Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
34
	  (*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*)
35
	  if !Options.output = "C" then
36
	    Lusic.print_lusic_to_h destname lusic_ext
37
	end
38
      else
39
	begin
40
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
41
	  Modules.check_dependency lusic destname;
42
	  let header = lusic.Lusic.contents in
43
	  let (declared_types_env, declared_clocks_env) = get_envs_from_top_decls header in
44
	  check_compatibility
45
	    (prog, computed_types_env, computed_clocks_env)
46
	    (header, declared_types_env, declared_clocks_env)
47
	end
48
  end
49

    
50

    
51
(* From prog to prog *)
52
let stage1 params prog dirname basename =
53
  (* Updating parent node information for variables *)
54
  Compiler_common.update_vdecl_parents_prog prog;
55

    
56
  (* Removing automata *)
57
  let prog = expand_automata prog in
58
  Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@,  @[<v 2>@,%a@]@ " Printers.pp_prog prog);
59

    
60
  (* Importing source *)
61
  let _ = Modules.load_program ISet.empty prog in
62

    
63
  (* Extracting dependencies (and updating Global.(type_env/clock_env) *)
64
  let dependencies = import_dependencies prog in
65

    
66
  (* Sorting nodes *)
67
  let prog = SortProg.sort prog in
68

    
69
  (* Perform inlining before any analysis *)
70
  let orig, prog =
71
    if !Options.global_inline && !Options.main_node <> "" then
72
      (if !Options.witnesses then prog else []),
73
      Inliner.global_inline basename prog 
74
    else (* if !Option.has_local_inline *)
75
      [],
76
      Inliner.local_inline prog (* type_env clock_env *)
77
  in
78

    
79
  (* Checking stateless/stateful status *)
80
  if Plugins.check_force_stateful () then
81
    force_stateful_decls prog
82
  else
83
    check_stateless_decls prog;
84

    
85
  (* Typing *)
86
  Global.type_env := type_decls !Global.type_env prog;
87

    
88
  (* Clock calculus *)
89
  Global.clock_env := clock_decls !Global.clock_env prog;
90

    
91
  (* Registering and checking machine types *)
92
  if Machine_types.is_active then Machine_types.load prog;
93
  
94

    
95
  (* Generating a .lusi header file only *)
96
  if !Options.lusi then
97
    (* We stop here the processing and produce the current prog. It will be
98
       exported as a lusi *)
99
    raise (StopPhase1 prog);
100

    
101
  (* Optimization of prog: 
102
     - Unfold consts 
103
     - eliminate trivial expressions
104
  *)
105
  (*
106
    let prog = 
107
    if !Options.const_unfold || !Options.optimization >= 5 then
108
    begin
109
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. eliminating constants and aliases@,");
110
    Optimize_prog.prog_unfold_consts prog
111
    end
112
    else
113
    prog
114
    in
115
  *)
116
  (* Delay calculus *)
117
  (* TO BE DONE LATER (Xavier)
118
     if(!Options.delay_calculus)
119
     then
120
     begin
121
     Log.report ~level:1 (fun fmt -> fprintf fmt ".. initialisation analysis@?");
122
     try
123
     Delay_calculus.delay_prog Basic_library.delay_env prog
124
     with (Delay.Error (loc,err)) as exc ->
125
     Location.print loc;
126
     eprintf "%a" Delay.pp_error err;
127
     Utils.track_exception ();
128
     raise exc
129
     end;
130
  *)
131

    
132
  (* Creating destination directory if needed *)
133
  create_dest_dir ();
134

    
135
  (* Compatibility with Lusi *)
136
  (* Checking the existence of a lusi (Lustre Interface file) *)
137
  let extension = ".lusi" in
138
  compile_source_to_header prog !Global.type_env !Global.clock_env dirname basename extension;
139

    
140
  Typing.uneval_prog_generics prog;
141
  Clock_calculus.uneval_prog_generics prog;
142

    
143

    
144
(* Disabling witness option. Could but reactivated later 
145
  if !Options.global_inline && !Options.main_node <> "" && !Options.witnesses then
146
    begin
147
      let orig = Corelang.copy_prog orig in
148
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating witness file@,");
149
      check_stateless_decls orig;
150
      let _ = Typing.type_prog type_env orig in
151
      let _ = Clock_calculus.clock_prog clock_env orig in
152
      Typing.uneval_prog_generics orig;
153
      Clock_calculus.uneval_prog_generics orig;
154
      Inliner.witness
155
	basename
156
	!Options.main_node
157
	orig prog type_env clock_env
158
    end;
159
*)  
160

    
161
  (* Computes and stores generic calls for each node,
162
     only useful for ANSI C90 compliant generic node compilation *)
163
  if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
164
  (*Hashtbl.iter (fun id td -> match td.Corelang.top_decl_desc with
165
    Corelang.Node nd -> Format.eprintf "%s calls %a" id
166
    Causality.NodeDep.pp_generic_calls nd | _ -> ()) Corelang.node_table;*)
167

    
168
  (* If some backend involving dynamic checks are active, then node annotations become runtime checks *)
169
  let prog =
170
    if dynamic_checks () then
171
      Spec.enforce_spec_prog prog
172
    else
173
      prog
174
  in
175

    
176

    
177
  (* (\* Registering and checking machine types *\) *)
178
  (* Machine_types.load prog; *)
179

    
180
  (* Normalization phase *)
181
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
182
  let prog = Normalization.normalize_prog params prog in
183
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
184

    
185
  (* (\* Removed. Is it used ? TODO *\)
186
   * (\* Postprocessing for VHDL backend *\)
187
   * let prog =
188
   *   match !Options.output with
189
   *   | "vhdl" ->
190
   *      Vhdl_normalization.post_process prog       
191
   *   | _ -> prog
192
   * in *)
193
  
194
  let prog =
195
    if !Options.mpfr
196
    then
197
      begin
198
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. targetting MPFR library@,");
199
	Mpfr.inject_prog prog
200
      end
201
    else
202
      begin
203
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping floating-point numbers@,");
204
	prog
205
      end in
206
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
207

    
208
  (* Checking array accesses *)
209
  if !Options.check then
210
    begin
211
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking array accesses@,");
212
      Access.check_prog prog;
213
    end;
214

    
215
  
216
  let prog = SortProg.sort_nodes_locals prog in
217
  
218
  prog, dependencies
219

    
220

    
221
    (* from source to machine code, with optimization *)
222
let stage2 prog =    
223
  (* Computation of node equation scheduling. It also breaks dependency cycles
224
     and warns about unused input or memory variables *)
225
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. @[<v 2>scheduling@ ");
226
  let prog, node_schs =
227
    try 
228
      Scheduling.schedule_prog prog
229
    with Causality.Error _ -> (* Error is not kept. It is recomputed in a more
230
				 systemtic way in AlgebraicLoop module *)
231
      AlgebraicLoop.analyze prog
232
  in
233
  Log.report ~level:1 (fun fmt -> fprintf fmt "%a"              Scheduling.pp_warning_unused node_schs);
234
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs);
235
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);
236
  Log.report ~level:5 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_dep_graph node_schs);
237
  Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
238
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
239

    
240
  (* TODO Salsa optimize prog: 
241
     - emits warning for programs with pre inside expressions
242
     - make sure each node arguments and memory is bounded by a local annotation
243
     - introduce fresh local variables for each real pure subexpression
244
  *)
245
  (* DFS with modular code generation *)
246
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,");
247
  let machine_code = Machine_code.translate_prog prog node_schs in
248

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

    
251
  (* Optimize machine code *)
252
  Optimize_machine.optimize prog node_schs machine_code   
253

    
254

    
255
(* printing code *)
256
let stage3 prog machine_code dependencies basename =
257
  let basename    =  Filename.basename basename in
258
  match !Options.output with
259
    "C" -> 
260
      begin
261
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
262
	C_backend.translate_to_c
263
	  (* alloc_header_file source_lib_file source_main_file makefile_file *)
264
	  basename prog machine_code dependencies
265
      end
266
  | "java" ->
267
     begin
268
       (Format.eprintf "internal error: sorry, but not yet supported !"; assert false)
269
     (*let source_file = basename ^ ".java" in
270
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
271
       let source_out = open_out source_file in
272
       let source_fmt = formatter_of_out_channel source_out in
273
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
274
       Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
275
     end
276
  | "horn" ->
277
     begin
278
       let destname = !Options.dest_dir ^ "/" ^ basename in
279
       let source_file = destname ^ ".smt2" in (* Could be changed *)
280
       let source_out = open_out source_file in
281
       let fmt = formatter_of_out_channel source_out in
282
       Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
283
       Horn_backend.translate fmt basename prog (Machine_code_common.arrow_machine::machine_code);
284
       (* Tracability file if option is activated *)
285
       if !Options.traces then (
286
	 let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
287
	 let traces_out = open_out traces_file in
288
	 let fmt = formatter_of_out_channel traces_out in
289
         Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
290
	 Horn_backend_traces.traces_file fmt basename prog machine_code;
291
       )
292
     end
293
  | "lustre" ->
294
     begin
295
       let destname = !Options.dest_dir ^ "/" ^ basename in
296
       let source_file = destname ^ ".lustrec.lus" in (* Could be changed *)
297
       let source_out = open_out source_file in
298
       let fmt = formatter_of_out_channel source_out in
299
       Printers.pp_prog fmt prog;
300
       Format.fprintf fmt "@.@?";
301
       (*	Lustre_backend.translate fmt basename normalized_prog machine_code *)
302
       ()
303
     end
304
  | "emf" ->
305
     begin
306
       let destname = !Options.dest_dir ^ "/" ^ basename in
307
       let source_file = destname ^ ".emf" in (* Could be changed *)
308
       let source_out = open_out source_file in
309
       let fmt = formatter_of_out_channel source_out in
310
       EMF_backend.translate fmt basename prog machine_code;
311
       ()
312
     end
313
  (* TODO Faut-il remettre *)
314
  (* | "vhdl" ->
315
   *    begin
316
   *      let destname = !Options.dest_dir ^ "/" ^ basename in
317
   *      let source_file = destname ^ ".vhd" in (\* Could be changed *\)
318
   *      let source_out = open_out source_file in
319
   *      let fmt = formatter_of_out_channel source_out in
320
   *      Vhdl_backend.translate fmt basename prog machine_code;
321
   *      ()
322
   *    end *)
323
       
324
     
325
  | _ -> assert false