Project

General

Profile

Download (15 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.No_main_specified;
20
    raise (Error.Error (Location.dummy, Error.No_main_specified)))
21

    
22
let create_dest_dir () =
23
  if not (Sys.file_exists !Options.dest_dir) then (
24
    Log.report ~level:1 (fun fmt ->
25
        fprintf fmt ".. creating destination directory@ ");
26
    Unix.mkdir !Options.dest_dir (Unix.stat ".").Unix.st_perm);
27
  if (Unix.stat !Options.dest_dir).Unix.st_kind <> Unix.S_DIR then (
28
    eprintf "Failure: destination %s is not a directory.@.@." !Options.dest_dir;
29
    exit 1)
30

    
31
(* Loading Lus/Lusi file and filling type tables with parsed functions/nodes *)
32
let parse filename extension =
33
  (* Location.set_input filename; *)
34
  (* let f_in = open_in filename in *)
35
  (* let lexbuf = Lexing.from_channel f_in in *)
36
  (* Location.init lexbuf filename; *)
37
  (* Parsing *)
38
  let prog =
39
    try
40
      Parse.(
41
        parse_filename
42
          (module Lexer_lustre)
43
          filename
44
          (match extension with
45
          | ".lusi" ->
46
            Log.report ~level:1 (fun fmt ->
47
                fprintf fmt ".. parsing header file %s@ " filename);
48
            Header
49
          | ".lus" ->
50
            Log.report ~level:1 (fun fmt ->
51
                fprintf fmt ".. parsing source file %s@ " filename);
52
            Program
53
          | _ ->
54
            assert false))
55
    with
56
    (* | (Parse.Error err) as exc ->
57
     *    Parse.report_error err;
58
     *    raise exc *)
59
    | Error.Error (loc, err) as exc ->
60
      eprintf "Parsing error: %a%a@." Error.pp err Location.pp loc;
61
      raise exc
62
  in
63
  (* close_in f_in; *)
64
  prog
65

    
66
let expand_automata decls =
67
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. expanding automata@ ");
68
  try Automata.expand_decls decls
69
  with Error.Error (loc, err) as exc ->
70
    eprintf "Automata error: %a%a@." Error.pp err Location.pp loc;
71
    raise exc
72

    
73
let check_stateless_decls decls =
74
  Log.report ~level:1 (fun fmt ->
75
      fprintf fmt "@ .. checking stateless/stateful status@ ");
76
  try Stateless.check_prog decls
77
  with Stateless.Error (loc, err) as exc ->
78
    eprintf
79
      "Stateless status error: %a%a@."
80
      Stateless.pp_error
81
      err
82
      Location.pp
83
      loc;
84
    raise exc
85

    
86
let force_stateful_decls decls =
87
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. forcing stateful status@ ");
88
  try Stateless.force_prog decls
89
  with Stateless.Error (loc, err) as exc ->
90
    eprintf
91
      "Stateless status error: %a%a@."
92
      Stateless.pp_error
93
      err
94
      Location.pp
95
      loc;
96
    raise exc
97

    
98
let type_decls env decls =
99
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ @[<v 2>.. typing@ ");
100
  let new_env =
101
    try Typing.type_prog env decls
102
    with Types.Error (loc, err) as exc ->
103
      eprintf "Typing error: %a%a@." Types.pp_error err Location.pp loc;
104
      raise exc
105
  in
106
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]");
107
  if !Options.print_types || !Options.verbose_level > 2 then
108
    Log.report ~level:1 (fun fmt ->
109
        fprintf fmt "@[<v 2>  %a@]@ " Corelang.pp_prog_type decls);
110
  new_env
111

    
112
let clock_decls env decls =
113
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ @[<v 2>.. clock calculus@ ");
114
  let new_env =
115
    try Clock_calculus.clock_prog env decls
116
    with Clocks.Error (loc, err) as exc ->
117
      eprintf "Clock calculus error: %a%a@." Clocks.pp_error err Location.pp loc;
118
      raise exc
119
  in
120
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]");
121
  if !Options.print_clocks || !Options.verbose_level > 2 then
122
    Log.report ~level:1 (fun fmt ->
123
        fprintf fmt "@[<v 2>  %a@]@ " Corelang.pp_prog_clock decls);
124
  new_env
125

    
126
(* XXX: UNUSED *)
127
(* Typing/Clocking with an empty env *)
128
(* let check_top_decls header =
129
 *   let new_tenv = type_decls Basic_library.type_env header in
130
 *   (\* Typing *\)
131
 *   let new_cenv = clock_decls Basic_library.clock_env header in
132
 *   (\* Clock calculus *\)
133
 *   header, new_tenv, new_cenv *)
134

    
135
(* List.fold_right (fun top_decl (ty_env, ck_env) -> match
136
   top_decl.top_decl_desc with | Node nd -> (Env.add_value ty_env nd.node_id
137
   nd.node_type, Env.add_value ck_env nd.node_id nd.node_clock) | ImportedNode
138
   ind -> (Env.add_value ty_env ind.nodei_id ind.nodei_type, Env.add_value
139
   ck_env ind.nodei_id ind.nodei_clock) | Const c -> get_envs_from_const c
140
   (ty_env, ck_env) | TypeDef _ -> List.fold_left (fun envs top ->
141
   consts_of_enum_type top_decl | Open _ -> (ty_env, ck_env)) header
142
   (Env.initial, Env.initial) *)
143

    
144
let check_compatibility (_, computed_types_env, computed_clocks_env)
145
    (header, declared_types_env, declared_clocks_env) =
146
  try
147
    (* checking defined types are compatible with declared types*)
148
    Typing.check_typedef_compat header;
149

    
150
    (* checking type compatibility with computed types*)
151
    Typing.check_env_compat header declared_types_env computed_types_env;
152

    
153
    (* checking clocks compatibility with computed clocks*)
154
    Clock_calculus.check_env_compat
155
      header
156
      declared_clocks_env
157
      computed_clocks_env;
158

    
159
    (* checking stateless status compatibility *)
160
    Stateless.check_compat header
161
  with
162
  | Types.Error (loc, err) as exc ->
163
    eprintf
164
      "Type mismatch between computed type and declared type in lustre \
165
       interface file: %a%a@."
166
      Types.pp_error
167
      err
168
      Location.pp
169
      loc;
170
    raise exc
171
  | Clocks.Error (loc, err) as exc ->
172
    eprintf
173
      "Clock mismatch between computed clock and declared clock in lustre \
174
       interface file: %a%a@."
175
      Clocks.pp_error
176
      err
177
      Location.pp
178
      loc;
179
    raise exc
180
  | Stateless.Error (loc, err) as exc ->
181
    eprintf
182
      "Stateless status mismatch between defined status and declared status in \
183
       lustre interface file: %a%a@."
184
      Stateless.pp_error
185
      err
186
      Location.pp
187
      loc;
188
    raise exc
189

    
190
(* Process each node/imported node and introduce the associated contract node *)
191
let resolve_contracts prog =
192
  (* Bind a fresh node with a new name according to existing nodes and freshly
193
     binded contract node. Clean the contract to remove the stmts *)
194
  let process_contract new_contracts c =
195
    (* Format.eprintf "Process contract@."; *)
196
    (* Resolve first the imports *)
197
    let stmts, locals, c =
198
      List.fold_left
199
        (fun (stmts, locals, c) import ->
200
          (* Search for contract in prog. The node have to be processed already.
201
             Otherwise raise an error. Each stmts in injected with a fresh name
202
             Inputs are renamed and associated to the expression in1 Same thing
203
             for outputs.
204

    
205
             Last the contracts elements are replaced with the renamed vars and
206
             merged with c contract. *)
207
          let name = import.import_nodeid in
208
          (* Format.eprintf "Process contract import %s@." name; *)
209
          let loc = import.import_loc in
210
          try
211
            let imp_nd = get_node name new_contracts in
212
            (* Get the contract node in process contracts *)
213
            (* checking that it's actually a (processed) contract *)
214
            let _ =
215
              if not (is_node_contract imp_nd) then assert false
216
                (* should be a contract *)
217
              else
218
                let imp_c = get_node_contract imp_nd in
219
                if
220
                  not
221
                    (imp_c.imports = [] && imp_c.locals = []
222
                   && imp_c.consts = [] && imp_c.stmts = [])
223
                then (
224
                  Format.eprintf
225
                    "Invalid processed contract: %i %i %i %i@.@?"
226
                    (List.length imp_c.imports)
227
                    (List.length imp_c.locals)
228
                    (List.length imp_c.consts)
229
                    (List.length imp_c.stmts);
230
                  assert false (* should be processed *))
231
            in
232
            let name_prefix x = "__" ^ name ^ "__" ^ x in
233
            let imp_nd =
234
              rename_node
235
                (fun x -> x (* not changing node names *))
236
                name_prefix
237
                imp_nd
238
            in
239
            let imp_in = imp_nd.node_inputs in
240
            let imp_out = imp_nd.node_outputs in
241
            let imp_locals = imp_nd.node_locals in
242
            let locals = imp_in @ imp_out @ imp_locals @ locals in
243
            let imp_c = get_node_contract imp_nd in
244
            (* Assigning in and out *)
245
            let mk_def vars_l e =
246
              let lhs = List.map (fun v -> v.var_id) vars_l in
247
              Eq (mkeq loc (lhs, e))
248
            in
249
            let in_assigns = mk_def imp_in import.inputs in
250
            let out_assigns = mk_def imp_out import.outputs in
251
            let stmts =
252
              in_assigns :: out_assigns :: imp_nd.node_stmts @ stmts
253
            in
254
            let c = merge_contracts c imp_c in
255
            stmts, locals, c
256
          with Not_found ->
257
            Format.eprintf "Where is contract %s@.@?" name;
258
            raise (Error.Error (loc, Error.Unbound_symbol ("contract " ^ name))))
259
        ([], c.consts @ c.locals, c)
260
        c.imports
261
    in
262
    let stmts = stmts @ c.stmts in
263
    (* Other contract elements will be normalized later *)
264
    let c =
265
      {
266
        c with
267
        (* we erase locals and stmts sinced they are now in the parent node *)
268
        locals = [];
269
        consts = [];
270
        stmts = [];
271
        imports = [];
272
      }
273
    in
274

    
275
    (* Format.eprintf "Processed stmts: %a@." Printers.pp_node_stmts stmts;
276
     * Format.eprintf "Processed locals: %a@." Printers.pp_vars locals; *)
277
    stmts, locals, c
278
  in
279

    
280
  let process_contract_new_node accu_contracts prog top =
281
    let id, spec, inputs, outputs =
282
      match top.top_decl_desc with
283
      | Node nd ->
284
        nd.node_id, nd.node_spec, nd.node_inputs, nd.node_outputs
285
      | ImportedNode ind ->
286
        ind.nodei_id, ind.nodei_spec, ind.nodei_inputs, ind.nodei_outputs
287
      | _ ->
288
        assert false
289
    in
290

    
291
    (* Format.eprintf "Process contract new node for node %s@." id; *)
292
    let node_stmts, node_locals, c =
293
      match spec with
294
      | None | Some (NodeSpec _) ->
295
        assert false
296
      | Some (Contract c) ->
297
        (* Format.eprintf "Processing contract of node %s@." id; *)
298
        process_contract accu_contracts c
299
    in
300
    (* Create a fresh name *)
301
    let used v =
302
      List.exists
303
        (fun top ->
304
          match top.top_decl_desc with
305
          | Node _ | ImportedNode _ ->
306
            node_name top = v
307
          | _ ->
308
            false)
309
        (accu_contracts @ prog)
310
    in
311
    let nd = {
312
      node_id = mk_new_name used (id ^ "_contract");
313
      node_type = Types.new_var ();
314
      node_clock = Clocks.new_var true;
315
      node_inputs = inputs @ outputs;
316
      node_outputs = [];
317
      node_locals;
318
      node_gencalls = [];
319
      node_checks = [];
320
      node_asserts = [];
321
      node_stmts;
322
      node_dec_stateless = false;
323
      node_stateless = None;
324
      node_spec = Some (Contract c);
325
      node_annot = [];
326
      node_iscontract = true;
327
    } in
328
    (* let stateless = Stateless.compute_node nd in *)
329
    mktop_decl
330
      c.spec_loc
331
      top.top_decl_owner
332
      top.top_decl_itf
333
      (Node nd)
334
         (* { nd with
335
          *   node_dec_stateless = stateless;
336
          *   node_stateless = Some stateless;
337
          * }) *)
338
  in
339
  (* Processing nodes in order. Should have been sorted by now
340

    
341
     Each top level contract is processed: stmts pushed in node
342

    
343
     Each regular imported node or node associated with a contract is replaced
344
     with a simplidfied contract and its contract is bound to a fresh node. *)
345
  let new_contracts, prog =
346
    List.fold_left
347
      (fun (accu_contracts, accu_nodes) top ->
348
        match top.top_decl_desc with
349
        | Node nd when nd.node_iscontract -> (
350
          match nd.node_spec with
351
          | None | Some (NodeSpec _) ->
352
            assert false
353
          | Some (Contract c) ->
354
            (* Format.eprintf "Processing top contract %s@." nd.node_id; *)
355
            let stmts, locals, c = process_contract accu_contracts c in
356
            let nd =
357
              {
358
                nd with
359
                node_locals = nd.node_locals @ locals;
360
                node_stmts = nd.node_stmts @ stmts;
361
                node_spec = Some (Contract c);
362
              }
363
            in
364
            { top with top_decl_desc = Node nd } :: accu_contracts, accu_nodes)
365
        | Node nd -> (
366
          match nd.node_spec with
367
          | None ->
368
            accu_contracts, top :: accu_nodes (* A boring node: no contract *)
369
          | Some (NodeSpec _) ->
370
            (* shall not happen, its too early *)
371
            assert false
372
          | Some (Contract _) ->
373
            (* A contract: processing it *)
374
            (* we bind a fresh node *)
375
            let new_nd = process_contract_new_node accu_contracts prog top in
376
            (* Format.eprintf "Creating new contract node %s@." (node_name
377
               new_nd); *)
378
            let nd =
379
              { nd with node_spec = Some (NodeSpec (node_name new_nd)) }
380
            in
381
            ( new_nd :: accu_contracts,
382
              { top with top_decl_desc = Node nd } :: accu_nodes ))
383
        | ImportedNode ind -> (
384
          (* Similar treatment for imported nodes *)
385
          match ind.nodei_spec with
386
          | None ->
387
            accu_contracts, top :: accu_nodes (* A boring node: no contract *)
388
          | Some (NodeSpec _) ->
389
            (* shall not happen, its too early *)
390
            assert false
391
          | Some (Contract _) ->
392
            (* A contract: processing it *)
393
            (* we bind a fresh node *)
394
            let new_nd = process_contract_new_node accu_contracts prog top in
395
            let ind =
396
              { ind with nodei_spec = Some (NodeSpec (node_name new_nd)) }
397
            in
398
            ( new_nd :: accu_contracts,
399
              { top with top_decl_desc = ImportedNode ind } :: accu_nodes ))
400
        | _ ->
401
          accu_contracts, top :: accu_nodes)
402
      ([], [])
403
      prog
404
  in
405
  List.rev new_contracts @ List.rev prog
406

    
407
let track_exception () =
408
  if !Options.track_exceptions then (
409
    Printexc.print_backtrace stdout;
410
    flush stdout)
411
  else ()
412

    
413
let update_vdecl_parents_prog prog =
414
  let update_vdecl_parents parent v = v.var_parent_nodeid <- Some parent in
415
  List.iter
416
    (fun top ->
417
      match top.top_decl_desc with
418
      | Node nd ->
419
        List.iter
420
          (update_vdecl_parents nd.node_id)
421
          (nd.node_inputs @ nd.node_outputs @ nd.node_locals)
422
      | ImportedNode ind ->
423
        List.iter
424
          (update_vdecl_parents ind.nodei_id)
425
          (ind.nodei_inputs @ ind.nodei_outputs)
426
      | _ ->
427
        ())
428
    prog
(20-20/99)