Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / compiler_stages.ml @ 04a188ec

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

    
58

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

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

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

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

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

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

    
115
  (* Typing *)
116
  Global.type_env := type_decls !Global.type_env prog;
117

    
118
  (* Clock calculus *)
119
  Global.clock_env := clock_decls !Global.clock_env prog;
120

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

    
124

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

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

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

    
168

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

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

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

    
201

    
202
  (* (\* Registering and checking machine types *\) *)
203
  (* Machine_types.load prog; *)
204

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

    
216

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

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

    
238

    
239
  let prog = SortProg.sort_nodes_locals prog in
240

    
241
  prog, dependencies
242

    
243

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

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

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

    
274
  (* Optimize machine code *)
275
  Optimize_machine.optimize params prog node_schs machine_code
276

    
277

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

    
348
  | _ -> assert false