Project

General

Profile

Download (12.5 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
  let open Options in
10
  match !output, !spec with OutC, SpecC -> true | _ -> false
11

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

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

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

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

    
75
  (* (\* Extracting dependencies (and updating Global.(type_env/clock_env) *\)
76
   * let dependencies = import_dependencies prog in *)
77

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

    
87
  (* Consolidating main node *)
88
  let _ =
89
    match !Options.main_node with
90
    | "" ->
91
      ()
92
    | main_node -> (
93
      Global.main_node := main_node;
94
      try ignore (Corelang.node_from_name main_node)
95
      with Not_found ->
96
        Format.eprintf "Code generation error: %a@." Error.pp
97
          Error.Main_not_found;
98
        raise (Error.Error (Location.dummy, Error.Main_not_found)))
99
  in
100

    
101
  (* Perform inlining before any analysis *)
102
  let _, prog =
103
    if !Options.global_inline && !Global.main_node <> "" then
104
      (if !Options.witnesses then prog else []), Inliner.global_inline prog
105
    else (* if !Option.has_local_inline *)
106
      [], Inliner.local_inline prog
107
    (* type_env clock_env *)
108
  in
109

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

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

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

    
120
  (* Registering and checking machine types *)
121
  if Machine_types.is_active then Machine_types.load prog;
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: - Unfold consts - eliminate trivial expressions *)
130
  let prog =
131
    if !Options.const_unfold || !Options.optimization >= 5 then (
132
      Log.report ~level:1 (fun fmt ->
133
          fprintf fmt ".. eliminating constants and aliases@,");
134
      Optimize_prog.prog_unfold_consts prog)
135
    else prog
136
  in
137

    
138
  (* Delay calculus *)
139
  (* TO BE DONE LATER (Xavier) if(!Options.delay_calculus) then begin Log.report
140
     ~level:1 (fun fmt -> fprintf fmt ".. initialisation analysis@?"); try
141
     Delay_calculus.delay_prog Basic_library.delay_env prog with (Delay.Error
142
     (loc,err)) as exc -> Location.print loc; eprintf "%a" Delay.pp_error err;
143
     Utils.track_exception (); raise exc end; *)
144

    
145
  (* Creating destination directory if needed *)
146
  create_dest_dir ();
147

    
148
  Typing.uneval_prog_generics prog;
149
  Clock_calculus.uneval_prog_generics prog;
150

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

    
160
  (* Computes and stores generic calls for each node, only useful for ANSI C90
161
     compliant generic node compilation *)
162
  if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
163

    
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
169
     become runtime checks *)
170
  let prog = if dynamic_checks () then Spec.enforce_spec_prog prog else prog in
171

    
172
  (* (\* Registering and checking machine types *\) *)
173
  (* Machine_types.load prog; *)
174

    
175
  (* Normalization phase *)
176
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. normalization@ ");
177
  let prog = Normalization.normalize_prog params prog in
178
  Log.report ~level:2 (fun fmt ->
179
      fprintf fmt "@[<v 2>@ %a@]@ " Printers.pp_prog_short prog);
180
  Log.report ~level:3 (fun fmt ->
181
      fprintf fmt "@[<v 2>@ %a@]@ " Printers.pp_prog prog);
182

    
183
  (* Compatibility with Lusi *)
184
  (* If compiling a lusi, generate the lusic. If this is a lus file, Check the
185
     existence of a lusi (Lustre Interface file) *)
186
  if !Options.compile_header then
187
    compile_source_to_header prog !Global.type_env !Global.clock_env dirname
188
      basename extension;
189

    
190
  let prog =
191
    if !Options.mpfr then (
192
      Log.report ~level:1 (fun fmt ->
193
          fprintf fmt "@ .. targetting MPFR library@,");
194
      Mpfr.inject_prog prog)
195
    else (
196
      Log.report ~level:1 (fun fmt ->
197
          fprintf fmt "@ .. keeping floating-point numbers@,");
198
      prog)
199
  in
200
  Log.report ~level:3 (fun fmt ->
201
      fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
202

    
203
  (* Checking array accesses *)
204
  if !Options.check then (
205
    Log.report ~level:1 (fun fmt ->
206
        fprintf fmt "@ .. checking array accesses@,");
207
    Access.check_prog prog);
208

    
209
  let prog = SortProg.sort_nodes_locals prog in
210

    
211
  prog, dependencies
212

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

    
233
  (* TODO Salsa optimize prog: - emits warning for programs with pre inside
234
     expressions - make sure each node arguments and memory is bounded by a
235
     local annotation - introduce fresh local variables for each real pure
236
     subexpression *)
237
  (* DFS with modular code generation *)
238
  Log.report ~level:1 (fun fmt ->
239
      fprintf fmt "@ @[<v 2>.. machines generation@ ");
240
  let machine_code = Machine_code.translate_prog prog node_schs in
241
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]");
242

    
243
  Log.report ~level:3 (fun fmt ->
244
      fprintf fmt "@ @[<v 2>.. generated machines (unoptimized):@ %a@]@ "
245
        Machine_code_common.pp_machines machine_code);
246

    
247
  (* Optimize machine code *)
248
  Optimize_machine.optimize params prog node_schs machine_code
249

    
250
(* printing code *)
251
let stage3 prog machine_code dependencies basename extension =
252
  let open Options in
253
  let basename = Filename.basename basename in
254
  match !output, extension with
255
  | OutC, ".lus" ->
256
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
257
    C_backend.translate_to_c !generate_c_header
258
      (* alloc_header_file source_lib_file source_main_file makefile_file *)
259
      basename prog machine_code dependencies
260
  (* | "acsl", ".lus" -> begin Log.report ~level:1 (fun fmt -> fprintf fmt "..
261
     ACSL annotations generation@,"); ACSL_backend.translate_to_acsl (*
262
     alloc_header_file source_lib_file source_main_file makefile_file *)
263
     basename prog machine_code dependencies end *)
264
  | OutC, _ ->
265
    C_backend.print_c_header basename;
266
    Log.report ~level:1 (fun fmt ->
267
        fprintf fmt ".. no C code generation for lusi@,")
268
  | OutJava, _ ->
269
    Format.eprintf "internal error: sorry, but not yet supported !";
270
    assert false
271
  (*let source_file = basename ^ ".java" in Log.report ~level:1 (fun fmt ->
272
    fprintf fmt ".. opening file %s@,@?" source_file); let source_out = open_out
273
    source_file in let source_fmt = formatter_of_out_channel source_out in
274
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
275
    Java_backend.translate_to_java source_fmt basename normalized_prog
276
    machine_code;*)
277
  | OutAda, _ ->
278
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. Ada code generation@.");
279
    Ada_backend.translate_to_ada basename
280
      (Machine_code_common.arrow_machine :: machine_code)
281
  | OutHorn, _ ->
282
    let destname = !Options.dest_dir ^ "/" ^ basename in
283
    let source_file = destname ^ ".smt2" in
284
    (* Could be changed *)
285
    let source_out = open_out source_file in
286
    let fmt = formatter_of_out_channel source_out in
287
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
288
    Horn_backend.translate fmt prog
289
      (Machine_code_common.arrow_machine :: machine_code);
290
    (* Tracability file if option is activated *)
291
    if !Options.traces then (
292
      let traces_file = destname ^ ".traces.xml" in
293
      (* Could be changed *)
294
      let traces_out = open_out traces_file in
295
      let fmt = formatter_of_out_channel traces_out in
296
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
297
      Horn_backend_traces.traces_file fmt machine_code)
298
  | OutLustre, _ ->
299
    let destname = !Options.dest_dir ^ "/" ^ basename in
300
    let source_file = destname ^ ".lustrec" ^ extension in
301
    (* Could be changed *)
302
    Log.report ~level:1 (fun fmt ->
303
        fprintf fmt ".. exporting processed file as %s@," source_file);
304
    let source_out = open_out source_file in
305
    let fmt = formatter_of_out_channel source_out in
306
    Printers.pp_prog fmt prog;
307
    Format.fprintf fmt "@.@?";
308
    (* Lustre_backend.translate fmt basename normalized_prog machine_code *)
309
    ()
310
  | OutEMF, _ ->
311
    let destname = !Options.dest_dir ^ "/" ^ basename in
312
    let source_file = destname ^ ".json" in
313
    (* Could be changed *)
314
    let source_out = open_out source_file in
315
    let fmt = formatter_of_out_channel source_out in
316
    EMF_backend.translate fmt basename prog machine_code;
317
    ()
(22-22/111)