Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / compiler_stages.ml @ 9b0432bc

History | View | Annotate | Download (13.6 KB)

1
open Lustrec
2
open Format
3
open Lustrec.Utils
4
open Compiler_common
5
open Lustrec.Lustre_types
6
open Backends
7

    
8
module Mpfr = Lustrec_mpfr
9

    
10
exception StopPhase1 of program_t
11

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

    
17

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

    
62

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

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

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

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

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

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

    
119
  (* Typing *)
120
  Lustrec.Global.type_env := type_decls !Lustrec.Global.type_env prog;
121

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

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

    
128

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

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

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

    
172

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

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

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

    
205

    
206
  (* (\* Registering and checking machine types *\) *)
207
  (* Machine_types.load prog; *)
208

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

    
221

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

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

    
243

    
244
  let prog = SortProg.sort_nodes_locals prog in
245

    
246
  prog, dependencies
247

    
248

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

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

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

    
279
  (* Optimize machine code *)
280
  Optimize_machine.optimize params prog node_schs machine_code
281

    
282

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

    
357
  | _ -> assert false