Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / compiler_stages.ml @ 3769b712

History | View | Annotate | Download (13.4 KB)

1
open Lustrec
2
open Format
3
open Lustrec.Utils
4
open Compiler_common
5
open Lustrec.Lustre_types
6
module Mpfr = Lustrec_mpfr
7

    
8
exception StopPhase1 of program_t
9

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

    
15

    
16
(* check whether a source file has a compiled header, if not, generate the
17
   compiled header *)
18
let compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension =
19
  let destname = !Lustrec.Options.dest_dir ^ "/" ^ basename in
20
  let lusic_ext = ".lusic" in
21
  let header_name = destname ^ lusic_ext in
22
  begin
23
    if (* Generating the lusic file *)
24
      extension = ".lusi" (* because input is a lusi *)
25
      || (extension = ".lus" &&
26
            not (Sys.file_exists header_name))
27
           (* or because it is a lus but not lusic exists *)
28
      || (let lusic = Lusic.read_lusic destname lusic_ext in
29
          not lusic.Lusic.from_lusi)
30
         (* or the lusic exists but is not generated from a lusi, hence it
31
            has te be regenerated *)
32
    then
33
      begin
34
	Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
35
	Lusic.write_lusic
36
          (extension = ".lusi") (* is it a lusi file ? *)
37
          (if extension = ".lusi" then prog else Lusic.extract_header dirname basename prog)
38
          destname
39
          lusic_ext;
40
        let _ =
41
          match !Lustrec.Options.output with
42
          | "C" -> C_backend_lusic.print_lusic_to_h destname lusic_ext
43
          | _ -> ()
44
        in
45
        ()
46
      end
47
    else (* Lusic exists and is usable. Checking compatibility *)
48
      begin
49
	Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
50
        let lusic = Lusic.read_lusic destname lusic_ext in
51
        Lusic.check_obsolete lusic destname;
52
	let header = lusic.Lusic.contents in
53
	let (declared_types_env, declared_clocks_env) = Modules.get_envs_from_top_decls header in
54
	check_compatibility
55
	  (prog, computed_types_env, computed_clocks_env)
56
	  (header, declared_types_env, declared_clocks_env)
57
      end
58
  end
59

    
60

    
61
(* From prog to prog *)
62
let stage1 params prog dirname basename extension =
63
  (* Updating parent node information for variables *)
64
  Compiler_common.update_vdecl_parents_prog prog;
65

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

    
70
  (* Importing source *)
71
  let prog, dependencies, (typ_env, clk_env) = Modules.load ~is_header:(extension = ".lusi") prog in
72
  (* Registering types and clocks for future checks *)
73
  Lustrec.Global.type_env := Lustrec.Env.overwrite !Lustrec.Global.type_env typ_env;
74
  Lustrec.Global.clock_env := Lustrec.Env.overwrite !Lustrec.Global.clock_env clk_env;
75
  
76
  (* (\* Extracting dependencies (and updating Lustrec.Global.(type_env/clock_env) *\)
77
   * let dependencies = import_dependencies prog in *)
78

    
79
  (* Sorting nodes *)
80
  let prog = SortProg.sort prog in
81
  (* Consolidating contracts *)
82
  let prog = resolve_contracts prog in
83
  let prog = SortProg.sort prog in
84
  Lustrec.Log.report ~level:3 (fun fmt ->
85
      Format.fprintf fmt "@[<v 0>Contracts resolved:@ %a@ @]@ " Lustrec.Printers.pp_prog prog);
86

    
87
  (* Consolidating main node *)
88
  let _ =
89
    match !Lustrec.Options.main_node with
90
    | "" -> ()
91
    | main_node -> (
92
      Lustrec.Global.main_node := main_node;
93
      try
94
        ignore (Lustrec.Corelang.node_from_name main_node)
95
      with Not_found -> (
96
        Format.eprintf "Code generation error: %a@." Lustrec.Error.pp_error_msg Lustrec.Error.Main_not_found;
97
        raise (Error.Error (Lustrec.Location.dummy_loc,Lustrec.Error.Main_not_found))
98
    ))
99
  in
100
  
101
  (* Perform inlining before any analysis *)
102
  let orig, prog =
103
    if !Lustrec.Options.global_inline && !Lustrec.Global.main_node <> "" then
104
      (if !Lustrec.Options.witnesses then prog else []),
105
      Inliner.global_inline basename prog
106
    else (* if !Option.has_local_inline *)
107
      [],
108
      Inliner.local_inline prog (* type_env clock_env *)
109
  in
110

    
111
  (* Checking stateless/stateful status *)
112
  if Plugins.check_force_stateful () then
113
    force_stateful_decls prog
114
  else
115
    check_stateless_decls prog;
116

    
117
  (* Typing *)
118
  Lustrec.Global.type_env := type_decls !Lustrec.Global.type_env prog;
119

    
120
  (* Clock calculus *)
121
  Lustrec.Global.clock_env := clock_decls !Lustrec.Global.clock_env prog;
122

    
123
  (* Registering and checking machine types *)
124
  if Machine_types.is_active then Machine_types.load prog;
125

    
126

    
127
  (* Generating a .lusi header file only *)
128
  if !Lustrec.Options.lusi || !Lustrec.Options.print_nodes then
129
    (* We stop here the processing and produce the current prog. It will be
130
       exported as a lusi *)
131
    raise (StopPhase1 prog);
132

    
133
  (* Optimization of prog:
134
     - Unfold consts
135
     - eliminate trivial expressions
136
   *)
137
  
138
  let prog =
139
    if !Lustrec.Options.const_unfold || !Lustrec.Options.optimization >= 5 then
140
      begin
141
        Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. eliminating constants and aliases@,");
142
        Optimize_prog.prog_unfold_consts prog
143
      end
144
    else
145
      prog
146
  in
147
  
148
  (* Delay calculus *)
149
  (* TO BE DONE LATER (Xavier)
150
     if(!Lustrec.Options.delay_calculus)
151
     then
152
     begin
153
     Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. initialisation analysis@?");
154
     try
155
     Delay_calculus.delay_prog Lustrec.Basic_library.delay_env prog
156
     with (Lustrec.Delay.Error (loc,err)) as exc ->
157
     Lustrec.Location.print loc;
158
     eprintf "%a" Lustrec.Delay.pp_error err;
159
     Lustrec.Utils.track_exception ();
160
     raise exc
161
     end;
162
   *)
163

    
164
  (* Creating destination directory if needed *)
165
  create_dest_dir ();
166
  
167
  Typing.uneval_prog_generics prog;
168
  Clock_calculus.uneval_prog_generics prog;
169

    
170

    
171
  (* Disabling witness option. Could but reactivated later
172
  if !Lustrec.Options.global_inline && !Lustrec.Options.main_node <> "" && !Lustrec.Options.witnesses then
173
    begin
174
      let orig = Lustrec.Corelang.copy_prog orig in
175
      Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating witness file@,");
176
      check_stateless_decls orig;
177
      let _ = Typing.type_prog type_env orig in
178
      let _ = Clock_calculus.clock_prog clock_env orig in
179
      Typing.uneval_prog_generics orig;
180
      Clock_calculus.uneval_prog_generics orig;
181
      Inliner.witness
182
	basename
183
	!Lustrec.Options.main_node
184
	orig prog type_env clock_env
185
    end;
186
   *)
187

    
188
  (* Computes and stores generic calls for each node,
189
     only useful for ANSI C90 compliant generic node compilation *)
190
  if !Lustrec.Options.ansi then Lustrec.Causality.NodeDep.compute_generic_calls prog;
191
  (*Hashtbl.iter (fun id td -> match td.Lustrec.Corelang.top_decl_desc with
192
    Lustrec.Corelang.Node nd -> Format.eprintf "%s calls %a" id
193
    Lustrec.Causality.NodeDep.pp_generic_calls nd | _ -> ()) Lustrec.Corelang.node_table;*)
194

    
195
  (* If some backend involving dynamic checks are active, then node annotations become runtime checks *)
196
  let prog =
197
    if dynamic_checks () then
198
      Spec.enforce_spec_prog prog
199
    else
200
      prog
201
  in
202

    
203

    
204
  (* (\* Registering and checking machine types *\) *)
205
  (* Machine_types.load prog; *)
206

    
207
  (* Lustrec.Normalization phase *)
208
  Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
209
  let prog = Lustrec.Normalization.normalize_prog params prog in
210
  Lustrec.Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Lustrec.Printers.pp_prog_short prog);
211
  Lustrec.Log.report ~level:3  (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Lustrec.Printers.pp_prog prog);
212
  
213
  (* Compatibility with Lusi *)
214
  (* If compiling a lusi, generate the lusic. If this is a lus file, Check the existence of a lusi (Lustre Interface file) *)
215
  if !Lustrec.Options.compile_header then
216
    compile_source_to_header
217
      prog !Lustrec.Global.type_env !Lustrec.Global.clock_env dirname basename extension;
218

    
219

    
220
  let prog =
221
    if !Lustrec.Options.mpfr
222
    then
223
      begin
224
	Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. targetting MPFR library@,");
225
	Mpfr.inject_prog prog
226
      end
227
    else
228
      begin
229
	Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping floating-point numbers@,");
230
	prog
231
      end in
232
  Lustrec.Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Lustrec.Printers.pp_prog prog);
233

    
234
  (* Checking array accesses *)
235
  if !Lustrec.Options.check then
236
    begin
237
      Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking array accesses@,");
238
      Access.check_prog prog;
239
    end;
240

    
241

    
242
  let prog = SortProg.sort_nodes_locals prog in
243

    
244
  prog, dependencies
245

    
246

    
247
    (* from source to machine code, with optimization *)
248
let stage2 params prog =
249
  (* Computation of node equation scheduling. It also breaks dependency cycles
250
     and warns about unused input or memory variables *)
251
  Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. @[<v 2>scheduling@ ");
252
  let prog, node_schs =
253
    try
254
      Scheduling.schedule_prog prog
255
    with Lustrec.Causality.Error _ -> (*Lustrec.Error is not kept. It is recomputed in a more
256
				 systemtic way in AlgebraicLoop module *)
257
      AlgebraicLoop.analyze prog
258
  in
259
  Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt "%a"              Scheduling.pp_warning_unused node_schs);
260
  Lustrec.Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs);
261
  Lustrec.Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);
262
  Lustrec.Log.report ~level:5 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_dep_graph node_schs);
263
  Lustrec.Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Lustrec.Printers.pp_prog prog);
264
  Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
265

    
266
  (* TODO Salsa optimize prog:
267
     - emits warning for programs with pre inside expressions
268
     - make sure each node arguments and memory is bounded by a local annotation
269
     - introduce fresh local variables for each real pure subexpression
270
  *)
271
  (* DFS with modular code generation *)
272
  Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,");
273
  let machine_code = Machine_code.translate_prog prog node_schs in
274

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

    
277
  (* Optimize machine code *)
278
  Optimize_machine.optimize params prog node_schs machine_code
279

    
280

    
281
(* printing code *)
282
let stage3 prog machine_code dependencies basename extension =
283
  let basename    =  Filename.basename basename in
284
  match !Lustrec.Options.output, extension with
285
    "C", ".lus" -> 
286
     begin
287
       Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
288
       C_backend.translate_to_c
289
	 (* alloc_header_file source_lib_file source_main_file makefile_file *)
290
	 basename prog machine_code dependencies
291
     end
292
  |  "C", _ -> 
293
      begin
294
      	Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. no C code generation for lusi@,");
295
      end
296
  | "java", _ ->
297
     begin
298
       (Format.eprintf "internal error: sorry, but not yet supported !"; assert false)
299
     (*let source_file = basename ^ ".java" in
300
       Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
301
       let source_out = open_out source_file in
302
       let source_fmt = formatter_of_out_channel source_out in
303
       Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
304
       Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
305
     end
306
  | "Ada", _ ->
307
    begin
308
      Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. Ada code generation@.");
309
      Ada_backend.translate_to_ada
310
      basename prog (Lustrec.Machine_code_common.arrow_machine::machine_code) dependencies
311
    end
312
  | "horn", _ ->
313
     begin
314
       let destname = !Lustrec.Options.dest_dir ^ "/" ^ basename in
315
       let source_file = destname ^ ".smt2" in (* Could be changed *)
316
       let source_out = open_out source_file in
317
       let fmt = formatter_of_out_channel source_out in
318
       Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
319
       Horn_backend.translate fmt basename prog (Lustrec.Machine_code_common.arrow_machine::machine_code);
320
       (* Tracability file if option is activated *)
321
       if !Lustrec.Options.traces then (
322
	 let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
323
	 let traces_out = open_out traces_file in
324
	 let fmt = formatter_of_out_channel traces_out in
325
         Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
326
	 Horn_backend_traces.traces_file fmt basename prog machine_code;
327
       )
328
     end
329
  | "lustre", _ ->
330
     begin
331
       let destname = !Lustrec.Options.dest_dir ^ "/" ^ basename in
332
       let source_file = destname ^ ".lustrec" ^ extension  in (* Could be changed *)
333
       Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. exporting processed file as %s@," source_file);
334
       let source_out = open_out source_file in
335
       let fmt = formatter_of_out_channel source_out in
336
       Lustrec.Printers.pp_prog fmt prog;
337
       Format.fprintf fmt "@.@?";
338
       (*	Lustre_backend.translate fmt basename normalized_prog machine_code *)
339
       ()
340
     end
341
  | "emf", _ ->
342
     begin
343
       let destname = !Lustrec.Options.dest_dir ^ "/" ^ basename in
344
       let source_file = destname ^ ".json" in (* Could be changed *)
345
       let source_out = open_out source_file in
346
       let fmt = formatter_of_out_channel source_out in
347
       EMF_backend.translate fmt basename prog machine_code;
348
       ()
349
     end
350

    
351
  | _ -> assert false