Project

General

Profile

Download (14.8 KB) Statistics
| Branch: | Tag: | Revision:
1
(********************************************************************)
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
open Format
14
open Lustre_types
15
open Corelang
16

    
17
let check_main () =
18
  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

    
23
let create_dest_dir () =
24
  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

    
32
(* Loading Lus/Lusi file and filling type tables with parsed functions/nodes *)
33
let parse filename extension =
34
  (* 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
  (* Parsing *)
39
  let prog =
40
    try
41
      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
    with
57
    (* | (Parse.Error err) as exc ->
58
     *    Parse.report_error err;
59
     *    raise exc *)
60
    | Error.Error (loc, err) as exc ->
61
      eprintf "Parsing error: %a%a@." Error.pp_error_msg err Location.pp_loc loc;
62
      raise exc
63
  in
64
  (* close_in f_in; *)
65
  prog
66

    
67
let expand_automata decls =
68
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. expanding automata@ ");
69
  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
    raise exc
73

    
74
let check_stateless_decls decls =
75
  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
      Location.pp_loc loc;
81
    raise exc
82

    
83
let force_stateful_decls decls =
84
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. forcing stateful status@ ");
85
  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
      Location.pp_loc loc;
89
    raise exc
90

    
91
let type_decls env decls =
92
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ @[<v 2>.. typing@ ");
93
  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
      raise exc
98
  in
99
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]");
100
  if !Options.print_types || !Options.verbose_level > 2 then
101
    Log.report ~level:1 (fun fmt ->
102
        fprintf fmt "@[<v 2>  %a@]@ " Corelang.pp_prog_type decls);
103
  new_env
104

    
105
let clock_decls env decls =
106
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ @[<v 2>.. clock calculus@ ");
107
  let new_env =
108
    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
      raise exc
113
  in
114
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]");
115
  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
  new_env
119

    
120
(* Typing/Clocking with an empty env *)
121
let check_top_decls header =
122
  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
  header, new_tenv, new_cenv
127

    
128
(* 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

    
137
let check_compatibility (_, computed_types_env, computed_clocks_env)
138
    (header, declared_types_env, declared_clocks_env) =
139
  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
    Clock_calculus.check_env_compat header declared_clocks_env
148
      computed_clocks_env;
149

    
150
    (* checking stateless status compatibility *)
151
    Stateless.check_compat header
152
  with
153
  | 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
    raise exc
159
  | Clocks.Error (loc, err) as exc ->
160
    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
    raise exc
165
  | Stateless.Error (loc, err) as exc ->
166
    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
    raise exc
171

    
172
(* Process each node/imported node and introduce the associated contract node *)
173
let resolve_contracts prog =
174
  (* 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
  let process_contract new_contracts c =
177
    (* Format.eprintf "Process contract@."; *)
178
    (* Resolve first the imports *)
179
    let stmts, locals, c =
180
      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

    
187
             Last the contracts elements are replaced with the renamed vars and
188
             merged with c contract. *)
189
          let name = import.import_nodeid in
190
          (* Format.eprintf "Process contract import %s@." name; *)
191
          let loc = import.import_loc in
192
          try
193
            let imp_nd = get_node name new_contracts in
194
            (* Get the contract node in process contracts *)
195
            (* checking that it's actually a (processed) contract *)
196
            let _ =
197
              if not (is_node_contract imp_nd) then assert false
198
                (* should be a contract *)
199
              else
200
                let imp_c = get_node_contract imp_nd in
201
                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
            in
212
            let name_prefix x = "__" ^ name ^ "__" ^ x in
213
            let imp_nd =
214
              rename_node
215
                (fun x -> x (* not changing node names *))
216
                name_prefix imp_nd
217
            in
218
            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
            let locals = imp_in @ imp_out @ imp_locals @ locals in
222
            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
            in
228
            let in_assigns = mk_def imp_in import.inputs in
229
            let out_assigns = mk_def imp_out import.outputs in
230
            let stmts =
231
              in_assigns :: out_assigns :: imp_nd.node_stmts @ stmts
232
            in
233
            let c = merge_contracts c imp_c in
234
            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
    in
241
    let stmts = stmts @ c.stmts in
242
    (* Other contract elements will be normalized later *)
243
    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
    in
253

    
254
    (* Format.eprintf "Processed stmts: %a@." Printers.pp_node_stmts stmts;
255
     * Format.eprintf "Processed locals: %a@." Printers.pp_vars locals; *)
256
    stmts, locals, c
257
  in
258

    
259
  let process_contract_new_node accu_contracts prog top =
260
    let id, spec, inputs, outputs =
261
      match top.top_decl_desc with
262
      | 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
    in
269

    
270
    (* Format.eprintf "Process contract new node for node %s@." id; *)
271
    let stmts, locals, c =
272
      match spec with
273
      | None | Some (NodeSpec _) ->
274
        assert false
275
      | Some (Contract c) ->
276
        (* Format.eprintf "Processing contract of node %s@." id; *)
277
        process_contract accu_contracts c
278
    in
279
    (* Create a fresh name *)
280
    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
    in
290
    let new_nd_id = mk_new_name used (id ^ "_coco") in
291
    let new_nd =
292
      mktop_decl c.spec_loc top.top_decl_owner top.top_decl_itf
293
        (Node
294
           {
295
             node_id = new_nd_id;
296
             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
    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
     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
  let new_contracts, prog =
321
    List.fold_left
322
      (fun (accu_contracts, accu_nodes) top ->
323
        match top.top_decl_desc with
324
        | Node nd when nd.node_iscontract -> (
325
          match nd.node_spec with
326
          | None | Some (NodeSpec _) ->
327
            assert false
328
          | Some (Contract c) ->
329
            (* 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
        | Node nd -> (
341
          match nd.node_spec with
342
          | 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
          match ind.nodei_spec with
361
          | 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
  in
379
  List.rev new_contracts @ List.rev prog
380

    
381
let track_exception () =
382
  if !Options.track_exceptions then (
383
    Printexc.print_backtrace stdout;
384
    flush stdout)
385
  else ()
386

    
387
let update_vdecl_parents_prog prog =
388
  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
(13-13/66)