Project

General

Profile

Download (14.6 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
    begin
20
      eprintf "Code generation error: %a@." Error.pp_error_msg Error.No_main_specified;
21
      raise (Error.Error (Location.dummy_loc, Error.No_main_specified))
22
    end
23

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

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

    
74
let expand_automata decls =
75
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. expanding automata@ ");
76
  try
77
    Automata.expand_decls decls
78
  with (Error.Error (loc, err)) as exc ->
79
    eprintf "Automata error: %a%a@."
80
      Error.pp_error_msg err
81
      Location.pp_loc loc;
82
    raise exc
83

    
84
let check_stateless_decls decls =
85
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. checking stateless/stateful status@ ");
86
  try
87
    Stateless.check_prog decls
88
  with (Stateless.Error (loc, err)) as exc ->
89
    eprintf "Stateless status error: %a%a@."
90
      Stateless.pp_error err
91
      Location.pp_loc loc;
92
    raise exc
93

    
94
let force_stateful_decls decls =
95
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. forcing stateful status@ ");
96
  try
97
    Stateless.force_prog decls
98
  with (Stateless.Error (loc, err)) as exc ->
99
    eprintf "Stateless status error: %a%a@."
100
      Stateless.pp_error err
101
      Location.pp_loc loc;
102
    raise exc
103

    
104
let type_decls env decls =  
105
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ @[<v 2>.. typing@ ");
106
  let new_env = 
107
    try
108
      Typing.type_prog env decls
109
    with Types.Error (loc,err) as exc ->
110
      eprintf "Typing error: %a%a@."
111
        Types.pp_error err
112
        Location.pp_loc loc;
113
      raise exc
114
  in
115
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]");
116
  if !Options.print_types || !Options.verbose_level > 2 then
117
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>  %a@]@ " Corelang.pp_prog_type decls);
118
  new_env
119
      
120
let clock_decls env decls = 
121
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ @[<v 2>.. clock calculus@ ");
122
  let new_env =
123
    try
124
      Clock_calculus.clock_prog env decls
125
    with (Clocks.Error (loc,err)) as exc ->
126
      eprintf "Clock calculus error: %a%a@." Clocks.pp_error err Location.pp_loc loc;
127
      raise exc
128
  in
129
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]");
130
  if !Options.print_clocks  || !Options.verbose_level > 2 then
131
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>  %a@]@ " Corelang.pp_prog_clock decls);
132
  new_env
133

    
134
(* Typing/Clocking with an empty env *)
135
let check_top_decls header =
136
  let new_tenv = type_decls Basic_library.type_env header in   (* Typing *)
137
  let new_cenv = clock_decls Basic_library.clock_env header in   (* Clock calculus *)
138
  header, new_tenv, new_cenv
139

    
140

    
141
(*
142
 List.fold_right
143
   (fun top_decl (ty_env, ck_env) ->
144
     match top_decl.top_decl_desc with
145
     | Node nd          -> (Env.add_value ty_env nd.node_id nd.node_type,
146
			    Env.add_value ck_env nd.node_id nd.node_clock)
147
     | ImportedNode ind -> (Env.add_value ty_env ind.nodei_id ind.nodei_type,
148
			    Env.add_value ck_env ind.nodei_id ind.nodei_clock)
149
     | Const c          -> get_envs_from_const c (ty_env, ck_env)
150
     | TypeDef _        -> List.fold_left (fun envs top -> consts_of_enum_type top_decl
151
     | Open _           -> (ty_env, ck_env))
152
   header
153
   (Env.initial, Env.initial)
154
 *)
155

    
156
	 
157

    
158
    
159
let check_compatibility (_, computed_types_env, computed_clocks_env) (header, declared_types_env, declared_clocks_env) =
160
  try
161
    (* checking defined types are compatible with declared types*)
162
    Typing.check_typedef_compat header;
163

    
164
    (* checking type compatibility with computed types*)
165
    Typing.check_env_compat header declared_types_env computed_types_env;
166

    
167
    (* checking clocks compatibility with computed clocks*)
168
    Clock_calculus.check_env_compat header declared_clocks_env computed_clocks_env;
169

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

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

    
204
             Last the contracts elements are replaced with the renamed vars and merged with c contract.
205
           *)
206
          let name = import.import_nodeid in
207
          (* Format.eprintf "Process contract import %s@." name; *)
208
          let loc = import.import_loc in
209
          try
210
            let imp_nd = get_node name new_contracts in (* Get the contract node in process contracts *)
211
            (* checking that it's actually a (processed) contract *)
212
            let _ =
213
              if not (is_node_contract imp_nd) then
214
                assert false (* should be a contract *)
215
              else
216
                let imp_c = get_node_contract imp_nd in
217
                if not (imp_c.imports = [] && imp_c.locals = [] && imp_c.consts = [] && imp_c.stmts = []) then
218
                (  Format.eprintf "Invalid processed contract: %i %i %i %i@.@?" (List.length imp_c.imports) (List.length imp_c.locals) (List.length imp_c.consts) (List.length imp_c.stmts);
219
                assert false (* should be processed *)
220
                )
221
            in
222
            let name_prefix x = "__" ^ name ^ "__" ^ x in
223
            let imp_nd = rename_node (fun x -> x (* not changing node names *)) name_prefix imp_nd in
224
            let imp_in = imp_nd.node_inputs in
225
            let imp_out = imp_nd.node_outputs in
226
            let imp_locals = imp_nd.node_locals in
227
            let locals = imp_in@imp_out@imp_locals@locals in
228
            let imp_c = get_node_contract imp_nd in
229
            (* Assigning in and out *)
230
            let mk_def vars_l e =
231
              let lhs = List.map (fun v -> v.var_id) vars_l in
232
              Eq (mkeq loc (lhs, e))
233
            in
234
            let in_assigns = mk_def imp_in import.inputs in
235
            let out_assigns = mk_def imp_out import.outputs in
236
            let stmts = in_assigns :: out_assigns :: imp_nd.node_stmts @ stmts in
237
            let c = merge_contracts c imp_c in
238
            stmts, locals, c 
239
          with Not_found -> Format.eprintf "Where is contract %s@.@?" name; raise (Error.Error (loc, (Error.Unbound_symbol ("contract " ^ name))))
240

    
241
         
242
        ) ([], c.consts@c.locals, c) c.imports
243
    in
244
    let stmts = stmts @ c.stmts in 
245
    (* Other contract elements will be normalized later *)
246
    let c = { c with (* 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
    
258
  in
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 -> nd.node_id, nd.node_spec, nd.node_inputs, nd.node_outputs
263
      | ImportedNode ind -> ind.nodei_id, ind.nodei_spec, ind.nodei_inputs, ind.nodei_outputs
264
      | _ -> assert false
265
    in
266
    (* Format.eprintf "Process contract new node for node %s@." id; *)
267

    
268
    let stmts, locals, c =
269
      match spec with
270
      | None | Some (NodeSpec _) -> assert false
271
      | Some (Contract c) ->
272
         (* Format.eprintf "Processing contract of node %s@." id; *)
273
         process_contract accu_contracts c
274
    in
275
    (* Create a fresh name *)
276
    let used v = List.exists (fun top ->
277
                     match top.top_decl_desc with
278
                     | Node _
279
                       | ImportedNode _ ->
280
                        (node_name top) = v
281
                     | _ -> false
282
                   ) (accu_contracts@prog)
283
    in
284
    let new_nd_id = mk_new_name used (id ^ "_coco") in
285
    let new_nd =
286
      mktop_decl
287
        c.spec_loc
288
        top.top_decl_owner
289
        top.top_decl_itf
290
        (Node {
291
             node_id = new_nd_id;
292
	     node_type = Types.new_var ();
293
	     node_clock = Clocks.new_var true;
294
	     node_inputs = inputs;
295
	     node_outputs = outputs;
296
	     node_locals = locals;
297
	     node_gencalls = [];
298
	     node_checks = [];
299
	     node_asserts = []; 
300
	     node_stmts = stmts;
301
	     node_dec_stateless = false;
302
	     node_stateless = None;
303
	     node_spec = Some (Contract c);
304
	     node_annot = [];
305
	     node_iscontract = true;
306
        }) in
307
    new_nd
308
  in
309
  (* Processing nodes in order. Should have been sorted by now
310

    
311
     Each top level contract is processed: stmts pushed in node
312

    
313
     Each regular imported node or node associated with a contract is
314
     replaced with a simplidfied contract and its contract is bound to
315
     a fresh node.
316

    
317
   *)
318
  let new_contracts, prog =
319
    List.fold_left
320
      (
321
        fun (accu_contracts, accu_nodes) top ->
322
        match top.top_decl_desc with
323
          
324
        | Node nd when nd.node_iscontract -> (
325
          match nd.node_spec with
326
          | None | Some (NodeSpec _) -> assert false
327
          | Some (Contract c) ->
328
             (* Format.eprintf "Processing top contract %s@." nd.node_id; *)
329
             let stmts, locals, c = process_contract accu_contracts c in
330
             let nd =
331
               { nd with
332
                 node_locals = nd.node_locals @ locals;
333
                 node_stmts = nd.node_stmts @ stmts;
334
                 node_spec = Some (Contract c);
335
               }
336
             in
337
             { top with top_decl_desc = Node nd }::accu_contracts,
338
             accu_nodes
339
             
340
        )
341
        | Node nd -> (
342
          match nd.node_spec with
343
          | None -> accu_contracts, top::accu_nodes (* A boring node: no contract *)
344
          | Some (NodeSpec _) -> (* shall not happen, its too early *)
345
             assert false
346
          | Some (Contract _) -> (* A contract: processing it *)
347
             (* we bind a fresh node *)
348
             let new_nd = process_contract_new_node accu_contracts prog top in
349
             (* Format.eprintf "Creating new contract node %s@." (node_name new_nd); *)
350
             let nd = { nd with node_spec = (Some (NodeSpec (node_name new_nd))) } in
351
             new_nd::accu_contracts,
352
             { top with top_decl_desc = Node nd }::accu_nodes
353
             
354
        )
355
                   
356
        | ImportedNode ind -> ( (* Similar treatment for imported nodes *)
357
          match ind.nodei_spec with
358
            None -> accu_contracts, top::accu_nodes (* A boring node: no contract *)
359
          | Some (NodeSpec _) -> (* shall not happen, its too early *)
360
             assert false
361
          | Some (Contract _) -> (* A contract: processing it *)
362
             (* we bind a fresh node *)
363
             let new_nd = process_contract_new_node accu_contracts prog top in
364
             let ind = { ind with nodei_spec = (Some (NodeSpec (node_name new_nd))) } in
365
             new_nd::accu_contracts,
366
             { top with top_decl_desc = ImportedNode ind }::accu_nodes
367
        )
368
        | _ -> accu_contracts, top::accu_nodes
369
      ) ([],[]) prog
370
  in
371
  (List.rev new_contracts) @ (List.rev prog)
372
         
373

    
374
  
375
let track_exception () =
376
  if !Options.track_exceptions
377
  then (Printexc.print_backtrace stdout; flush stdout)
378
  else ()
379

    
380

    
381
let update_vdecl_parents_prog prog =
382
  let update_vdecl_parents parent v =
383
    v.var_parent_nodeid <- Some parent
384
  in
385
  List.iter (
386
    fun top -> match top.top_decl_desc with
387
    | Node nd ->
388
       List.iter
389
	 (update_vdecl_parents nd.node_id)
390
	 (nd.node_inputs @ nd.node_outputs @ nd.node_locals )  
391
    | ImportedNode ind -> 
392
       List.iter
393
	 (update_vdecl_parents ind.nodei_id)
394
	 (ind.nodei_inputs @ ind.nodei_outputs )  
395
    | _ -> ()
396
  ) prog
(13-13/64)