Project

General

Profile

Download (14.8 KB) Statistics
| Branch: | Tag: | Revision:
1 ef34b4ae xthirioux
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11
12
open Utils
13 ca7ff3f7 Lélio Brun
open Format
14 8446bf03 ploc
open Lustre_types
15 ef34b4ae xthirioux
open Corelang
16
17 04a63d25 xthirioux
let check_main () =
18 ca7ff3f7 Lélio Brun
  if !Options.main_node = "" then (
19
    eprintf "Code generation error: %a@." Error.pp_error_msg
20
      Error.No_main_specified;
21
    raise (Error.Error (Location.dummy_loc, Error.No_main_specified)))
22 04a63d25 xthirioux
23 ef34b4ae xthirioux
let create_dest_dir () =
24 ca7ff3f7 Lélio Brun
  if not (Sys.file_exists !Options.dest_dir) then (
25
    Log.report ~level:1 (fun fmt ->
26
        fprintf fmt ".. creating destination directory@ ");
27
    Unix.mkdir !Options.dest_dir (Unix.stat ".").Unix.st_perm);
28
  if (Unix.stat !Options.dest_dir).Unix.st_kind <> Unix.S_DIR then (
29
    eprintf "Failure: destination %s is not a directory.@.@." !Options.dest_dir;
30
    exit 1)
31 ef34b4ae xthirioux
32 ca7ff3f7 Lélio Brun
(* Loading Lus/Lusi file and filling type tables with parsed functions/nodes *)
33 217837e2 ploc
let parse filename extension =
34 90e83deb Lélio Brun
  (* Location.set_input filename; *)
35
  (* let f_in = open_in filename in *)
36
  (* let lexbuf = Lexing.from_channel f_in in *)
37
  (* Location.init lexbuf filename; *)
38 ef34b4ae xthirioux
  (* Parsing *)
39 ca7ff3f7 Lélio Brun
  let prog =
40 ef34b4ae xthirioux
    try
41 ca7ff3f7 Lélio Brun
      Parse.(
42
        parse_filename
43
          (module Lexer_lustre)
44
          filename
45
          (match extension with
46
          | ".lusi" ->
47
            Log.report ~level:1 (fun fmt ->
48
                fprintf fmt ".. parsing header file %s@ " filename);
49
            Header
50
          | ".lus" ->
51
            Log.report ~level:1 (fun fmt ->
52
                fprintf fmt ".. parsing source file %s@ " filename);
53
            Program
54
          | _ ->
55
            assert false))
56 ef34b4ae xthirioux
    with
57 90e83deb Lélio Brun
    (* | (Parse.Error err) as exc ->
58
     *    Parse.report_error err;
59
     *    raise exc *)
60 ca7ff3f7 Lélio Brun
    | Error.Error (loc, err) as exc ->
61
      eprintf "Parsing error: %a%a@." Error.pp_error_msg err Location.pp_loc loc;
62 ef34b4ae xthirioux
      raise exc
63 217837e2 ploc
  in
64 90e83deb Lélio Brun
  (* close_in f_in; *)
65 217837e2 ploc
  prog
66 ef34b4ae xthirioux
67 04a63d25 xthirioux
let expand_automata decls =
68 7ee5f69e Lélio Brun
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. expanding automata@ ");
69 ca7ff3f7 Lélio Brun
  try Automata.expand_decls decls
70
  with Error.Error (loc, err) as exc ->
71
    eprintf "Automata error: %a%a@." Error.pp_error_msg err Location.pp_loc loc;
72 04a63d25 xthirioux
    raise exc
73
74 ef34b4ae xthirioux
let check_stateless_decls decls =
75 ca7ff3f7 Lélio Brun
  Log.report ~level:1 (fun fmt ->
76
      fprintf fmt "@ .. checking stateless/stateful status@ ");
77
  try Stateless.check_prog decls
78
  with Stateless.Error (loc, err) as exc ->
79
    eprintf "Stateless status error: %a%a@." Stateless.pp_error err
80 ef34b4ae xthirioux
      Location.pp_loc loc;
81
    raise exc
82
83 04a63d25 xthirioux
let force_stateful_decls decls =
84 7ee5f69e Lélio Brun
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. forcing stateful status@ ");
85 ca7ff3f7 Lélio Brun
  try Stateless.force_prog decls
86
  with Stateless.Error (loc, err) as exc ->
87
    eprintf "Stateless status error: %a%a@." Stateless.pp_error err
88 04a63d25 xthirioux
      Location.pp_loc loc;
89
    raise exc
90
91 ca7ff3f7 Lélio Brun
let type_decls env decls =
92 7ee5f69e Lélio Brun
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ @[<v 2>.. typing@ ");
93 ca7ff3f7 Lélio Brun
  let new_env =
94
    try Typing.type_prog env decls
95
    with Types.Error (loc, err) as exc ->
96
      eprintf "Typing error: %a%a@." Types.pp_error err Location.pp_loc loc;
97 7ee5f69e Lélio Brun
      raise exc
98 ef34b4ae xthirioux
  in
99 7ee5f69e Lélio Brun
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]");
100 e7cc5186 ploc
  if !Options.print_types || !Options.verbose_level > 2 then
101 ca7ff3f7 Lélio Brun
    Log.report ~level:1 (fun fmt ->
102
        fprintf fmt "@[<v 2>  %a@]@ " Corelang.pp_prog_type decls);
103 ef34b4ae xthirioux
  new_env
104 ca7ff3f7 Lélio Brun
105
let clock_decls env decls =
106 7ee5f69e Lélio Brun
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ @[<v 2>.. clock calculus@ ");
107 ef34b4ae xthirioux
  let new_env =
108 ca7ff3f7 Lélio Brun
    try Clock_calculus.clock_prog env decls
109
    with Clocks.Error (loc, err) as exc ->
110
      eprintf "Clock calculus error: %a%a@." Clocks.pp_error err Location.pp_loc
111
        loc;
112 7ee5f69e Lélio Brun
      raise exc
113 ef34b4ae xthirioux
  in
114 7ee5f69e Lélio Brun
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]");
115 ca7ff3f7 Lélio Brun
  if !Options.print_clocks || !Options.verbose_level > 2 then
116
    Log.report ~level:1 (fun fmt ->
117
        fprintf fmt "@[<v 2>  %a@]@ " Corelang.pp_prog_clock decls);
118 ef34b4ae xthirioux
  new_env
119
120 2d27eedd ploc
(* Typing/Clocking with an empty env *)
121 ef34b4ae xthirioux
let check_top_decls header =
122 ca7ff3f7 Lélio Brun
  let new_tenv = type_decls Basic_library.type_env header in
123
  (* Typing *)
124
  let new_cenv = clock_decls Basic_library.clock_env header in
125
  (* Clock calculus *)
126 ef34b4ae xthirioux
  header, new_tenv, new_cenv
127
128 ca7ff3f7 Lélio Brun
(* List.fold_right (fun top_decl (ty_env, ck_env) -> match
129
   top_decl.top_decl_desc with | Node nd -> (Env.add_value ty_env nd.node_id
130
   nd.node_type, Env.add_value ck_env nd.node_id nd.node_clock) | ImportedNode
131
   ind -> (Env.add_value ty_env ind.nodei_id ind.nodei_type, Env.add_value
132
   ck_env ind.nodei_id ind.nodei_clock) | Const c -> get_envs_from_const c
133
   (ty_env, ck_env) | TypeDef _ -> List.fold_left (fun envs top ->
134
   consts_of_enum_type top_decl | Open _ -> (ty_env, ck_env)) header
135
   (Env.initial, Env.initial) *)
136 ef34b4ae xthirioux
137 ca7ff3f7 Lélio Brun
let check_compatibility (_, computed_types_env, computed_clocks_env)
138
    (header, declared_types_env, declared_clocks_env) =
139 ef34b4ae xthirioux
  try
140
    (* checking defined types are compatible with declared types*)
141
    Typing.check_typedef_compat header;
142
143
    (* checking type compatibility with computed types*)
144
    Typing.check_env_compat header declared_types_env computed_types_env;
145
146
    (* checking clocks compatibility with computed clocks*)
147 ca7ff3f7 Lélio Brun
    Clock_calculus.check_env_compat header declared_clocks_env
148
      computed_clocks_env;
149 ef34b4ae xthirioux
150
    (* checking stateless status compatibility *)
151
    Stateless.check_compat header
152
  with
153 ca7ff3f7 Lélio Brun
  | Types.Error (loc, err) as exc ->
154
    eprintf
155
      "Type mismatch between computed type and declared type in lustre \
156
       interface file: %a%a@."
157
      Types.pp_error err Location.pp_loc loc;
158 ef34b4ae xthirioux
    raise exc
159
  | Clocks.Error (loc, err) as exc ->
160 ca7ff3f7 Lélio Brun
    eprintf
161
      "Clock mismatch between computed clock and declared clock in lustre \
162
       interface file: %a%a@."
163
      Clocks.pp_error err Location.pp_loc loc;
164 ef34b4ae xthirioux
    raise exc
165
  | Stateless.Error (loc, err) as exc ->
166 ca7ff3f7 Lélio Brun
    eprintf
167
      "Stateless status mismatch between defined status and declared status in \
168
       lustre interface file: %a%a@."
169
      Stateless.pp_error err Location.pp_loc loc;
170 ef34b4ae xthirioux
    raise exc
171
172 f4cba4b8 ploc
(* Process each node/imported node and introduce the associated contract node *)
173
let resolve_contracts prog =
174 ca7ff3f7 Lélio Brun
  (* Bind a fresh node with a new name according to existing nodes and freshly
175
     binded contract node. Clean the contract to remove the stmts *)
176 1fd3d002 ploc
  let process_contract new_contracts c =
177 8a11dc80 ploc
    (* Format.eprintf "Process contract@."; *)
178 f4cba4b8 ploc
    (* Resolve first the imports *)
179
    let stmts, locals, c =
180 ca7ff3f7 Lélio Brun
      List.fold_left
181
        (fun (stmts, locals, c) import ->
182
          (* Search for contract in prog. The node have to be processed already.
183
             Otherwise raise an error. Each stmts in injected with a fresh name
184
             Inputs are renamed and associated to the expression in1 Same thing
185
             for outputs.
186 ef34b4ae xthirioux
187 ca7ff3f7 Lélio Brun
             Last the contracts elements are replaced with the renamed vars and
188
             merged with c contract. *)
189 f4cba4b8 ploc
          let name = import.import_nodeid in
190 8a11dc80 ploc
          (* Format.eprintf "Process contract import %s@." name; *)
191 1fd3d002 ploc
          let loc = import.import_loc in
192 f4cba4b8 ploc
          try
193 ca7ff3f7 Lélio Brun
            let imp_nd = get_node name new_contracts in
194
            (* Get the contract node in process contracts *)
195 f4cba4b8 ploc
            (* checking that it's actually a (processed) contract *)
196 1fd3d002 ploc
            let _ =
197 ca7ff3f7 Lélio Brun
              if not (is_node_contract imp_nd) then assert false
198
                (* should be a contract *)
199 1fd3d002 ploc
              else
200
                let imp_c = get_node_contract imp_nd in
201 ca7ff3f7 Lélio Brun
                if
202
                  not
203
                    (imp_c.imports = [] && imp_c.locals = []
204
                   && imp_c.consts = [] && imp_c.stmts = [])
205
                then (
206
                  Format.eprintf "Invalid processed contract: %i %i %i %i@.@?"
207
                    (List.length imp_c.imports)
208
                    (List.length imp_c.locals) (List.length imp_c.consts)
209
                    (List.length imp_c.stmts);
210
                  assert false (* should be processed *))
211 f4cba4b8 ploc
            in
212 1fd3d002 ploc
            let name_prefix x = "__" ^ name ^ "__" ^ x in
213 ca7ff3f7 Lélio Brun
            let imp_nd =
214
              rename_node
215
                (fun x -> x (* not changing node names *))
216
                name_prefix imp_nd
217
            in
218 1fd3d002 ploc
            let imp_in = imp_nd.node_inputs in
219
            let imp_out = imp_nd.node_outputs in
220
            let imp_locals = imp_nd.node_locals in
221 ca7ff3f7 Lélio Brun
            let locals = imp_in @ imp_out @ imp_locals @ locals in
222 1fd3d002 ploc
            let imp_c = get_node_contract imp_nd in
223
            (* Assigning in and out *)
224
            let mk_def vars_l e =
225
              let lhs = List.map (fun v -> v.var_id) vars_l in
226
              Eq (mkeq loc (lhs, e))
227 f4cba4b8 ploc
            in
228 1fd3d002 ploc
            let in_assigns = mk_def imp_in import.inputs in
229
            let out_assigns = mk_def imp_out import.outputs in
230 ca7ff3f7 Lélio Brun
            let stmts =
231
              in_assigns :: out_assigns :: imp_nd.node_stmts @ stmts
232
            in
233 f4cba4b8 ploc
            let c = merge_contracts c imp_c in
234 ca7ff3f7 Lélio Brun
            stmts, locals, c
235
          with Not_found ->
236
            Format.eprintf "Where is contract %s@.@?" name;
237
            raise (Error.Error (loc, Error.Unbound_symbol ("contract " ^ name))))
238
        ([], c.consts @ c.locals, c)
239
        c.imports
240 f4cba4b8 ploc
    in
241 ca7ff3f7 Lélio Brun
    let stmts = stmts @ c.stmts in
242 f4cba4b8 ploc
    (* Other contract elements will be normalized later *)
243 ca7ff3f7 Lélio Brun
    let c =
244
      {
245
        c with
246
        (* we erase locals and stmts sinced they are now in the parent node *)
247
        locals = [];
248
        consts = [];
249
        stmts = [];
250
        imports = [];
251
      }
252 f4cba4b8 ploc
    in
253 ca7ff3f7 Lélio Brun
254 1fd3d002 ploc
    (* Format.eprintf "Processed stmts: %a@." Printers.pp_node_stmts stmts;
255
     * Format.eprintf "Processed locals: %a@." Printers.pp_vars locals; *)
256 f4cba4b8 ploc
    stmts, locals, c
257
  in
258 ca7ff3f7 Lélio Brun
259 f4cba4b8 ploc
  let process_contract_new_node accu_contracts prog top =
260
    let id, spec, inputs, outputs =
261
      match top.top_decl_desc with
262 ca7ff3f7 Lélio Brun
      | Node nd ->
263
        nd.node_id, nd.node_spec, nd.node_inputs, nd.node_outputs
264
      | ImportedNode ind ->
265
        ind.nodei_id, ind.nodei_spec, ind.nodei_inputs, ind.nodei_outputs
266
      | _ ->
267
        assert false
268 f4cba4b8 ploc
    in
269 1fd3d002 ploc
270 ca7ff3f7 Lélio Brun
    (* Format.eprintf "Process contract new node for node %s@." id; *)
271 f4cba4b8 ploc
    let stmts, locals, c =
272
      match spec with
273 ca7ff3f7 Lélio Brun
      | None | Some (NodeSpec _) ->
274
        assert false
275 f4cba4b8 ploc
      | Some (Contract c) ->
276 ca7ff3f7 Lélio Brun
        (* Format.eprintf "Processing contract of node %s@." id; *)
277
        process_contract accu_contracts c
278 f4cba4b8 ploc
    in
279
    (* Create a fresh name *)
280 ca7ff3f7 Lélio Brun
    let used v =
281
      List.exists
282
        (fun top ->
283
          match top.top_decl_desc with
284
          | Node _ | ImportedNode _ ->
285
            node_name top = v
286
          | _ ->
287
            false)
288
        (accu_contracts @ prog)
289 f4cba4b8 ploc
    in
290
    let new_nd_id = mk_new_name used (id ^ "_coco") in
291
    let new_nd =
292 ca7ff3f7 Lélio Brun
      mktop_decl c.spec_loc top.top_decl_owner top.top_decl_itf
293
        (Node
294
           {
295 1fd3d002 ploc
             node_id = new_nd_id;
296 ca7ff3f7 Lélio Brun
             node_type = Types.new_var ();
297
             node_clock = Clocks.new_var true;
298
             node_inputs = inputs;
299
             node_outputs = outputs;
300
             node_locals = locals;
301
             node_gencalls = [];
302
             node_checks = [];
303
             node_asserts = [];
304
             node_stmts = stmts;
305
             node_dec_stateless = false;
306
             node_stateless = None;
307
             node_spec = Some (Contract c);
308
             node_annot = [];
309
             node_iscontract = true;
310
           })
311
    in
312 f4cba4b8 ploc
    new_nd
313
  in
314
  (* Processing nodes in order. Should have been sorted by now
315
316
     Each top level contract is processed: stmts pushed in node
317
318 ca7ff3f7 Lélio Brun
     Each regular imported node or node associated with a contract is replaced
319
     with a simplidfied contract and its contract is bound to a fresh node. *)
320 f4cba4b8 ploc
  let new_contracts, prog =
321
    List.fold_left
322 ca7ff3f7 Lélio Brun
      (fun (accu_contracts, accu_nodes) top ->
323 f4cba4b8 ploc
        match top.top_decl_desc with
324
        | Node nd when nd.node_iscontract -> (
325
          match nd.node_spec with
326 ca7ff3f7 Lélio Brun
          | None | Some (NodeSpec _) ->
327
            assert false
328 f4cba4b8 ploc
          | Some (Contract c) ->
329 ca7ff3f7 Lélio Brun
            (* Format.eprintf "Processing top contract %s@." nd.node_id; *)
330
            let stmts, locals, c = process_contract accu_contracts c in
331
            let nd =
332
              {
333
                nd with
334
                node_locals = nd.node_locals @ locals;
335
                node_stmts = nd.node_stmts @ stmts;
336
                node_spec = Some (Contract c);
337
              }
338
            in
339
            { top with top_decl_desc = Node nd } :: accu_contracts, accu_nodes)
340 f4cba4b8 ploc
        | Node nd -> (
341
          match nd.node_spec with
342 ca7ff3f7 Lélio Brun
          | None ->
343
            accu_contracts, top :: accu_nodes (* A boring node: no contract *)
344
          | Some (NodeSpec _) ->
345
            (* shall not happen, its too early *)
346
            assert false
347
          | Some (Contract _) ->
348
            (* A contract: processing it *)
349
            (* we bind a fresh node *)
350
            let new_nd = process_contract_new_node accu_contracts prog top in
351
            (* Format.eprintf "Creating new contract node %s@." (node_name
352
               new_nd); *)
353
            let nd =
354
              { nd with node_spec = Some (NodeSpec (node_name new_nd)) }
355
            in
356
            ( new_nd :: accu_contracts,
357
              { top with top_decl_desc = Node nd } :: accu_nodes ))
358
        | ImportedNode ind -> (
359
          (* Similar treatment for imported nodes *)
360 f4cba4b8 ploc
          match ind.nodei_spec with
361 ca7ff3f7 Lélio Brun
          | None ->
362
            accu_contracts, top :: accu_nodes (* A boring node: no contract *)
363
          | Some (NodeSpec _) ->
364
            (* shall not happen, its too early *)
365
            assert false
366
          | Some (Contract _) ->
367
            (* A contract: processing it *)
368
            (* we bind a fresh node *)
369
            let new_nd = process_contract_new_node accu_contracts prog top in
370
            let ind =
371
              { ind with nodei_spec = Some (NodeSpec (node_name new_nd)) }
372
            in
373
            ( new_nd :: accu_contracts,
374
              { top with top_decl_desc = ImportedNode ind } :: accu_nodes ))
375
        | _ ->
376
          accu_contracts, top :: accu_nodes)
377
      ([], []) prog
378 f4cba4b8 ploc
  in
379 ca7ff3f7 Lélio Brun
  List.rev new_contracts @ List.rev prog
380 f4cba4b8 ploc
381 990210f3 ploc
let track_exception () =
382 ca7ff3f7 Lélio Brun
  if !Options.track_exceptions then (
383
    Printexc.print_backtrace stdout;
384
    flush stdout)
385 990210f3 ploc
  else ()
386
387 66359a5e ploc
let update_vdecl_parents_prog prog =
388 ca7ff3f7 Lélio Brun
  let update_vdecl_parents parent v = v.var_parent_nodeid <- Some parent in
389
  List.iter
390
    (fun top ->
391
      match top.top_decl_desc with
392
      | Node nd ->
393
        List.iter
394
          (update_vdecl_parents nd.node_id)
395
          (nd.node_inputs @ nd.node_outputs @ nd.node_locals)
396
      | ImportedNode ind ->
397
        List.iter
398
          (update_vdecl_parents ind.nodei_id)
399
          (ind.nodei_inputs @ ind.nodei_outputs)
400
      | _ ->
401
        ())
402
    prog