Project

General

Profile

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

    
56

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

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

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

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

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

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

    
113
  (* Typing *)
114
  Global.type_env := type_decls !Global.type_env prog;
115

    
116
  (* Clock calculus *)
117
  Global.clock_env := clock_decls !Global.clock_env prog;
118

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

    
122

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

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

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

    
166

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

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

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

    
199

    
200
  (* (\* Registering and checking machine types *\) *)
201
  (* Machine_types.load prog; *)
202

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

    
215

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

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

    
237

    
238
  let prog = SortProg.sort_nodes_locals prog in
239

    
240
  prog, dependencies
241

    
242

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

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

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

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

    
276

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

    
347
  | _ -> assert false
(14-14/63)