Project

General

Profile

Download (14.6 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
open Format 
14 8446bf03 ploc
open Lustre_types
15 ef34b4ae xthirioux
open Corelang
16
17 04a63d25 xthirioux
let check_main () =
18
  if !Options.main_node = "" then
19
    begin
20 e7cc5186 ploc
      eprintf "Code generation error: %a@." Error.pp_error_msg Error.No_main_specified;
21 04a188ec ploc
      raise (Error.Error (Location.dummy_loc, Error.No_main_specified))
22 04a63d25 xthirioux
    end
23
24 ef34b4ae xthirioux
let create_dest_dir () =
25
  begin
26
    if not (Sys.file_exists !Options.dest_dir) then
27
      begin
28 521e2a6b ploc
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. creating destination directory@ ");
29 ef34b4ae xthirioux
	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 217837e2 ploc
(* Loading Lus/Lusi file and filling type tables with parsed
39 ef34b4ae xthirioux
   functions/nodes *)
40 217837e2 ploc
let parse filename extension =
41 90e83deb Lélio Brun
  (* 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 ef34b4ae xthirioux
  (* Parsing *)
46 217837e2 ploc
  let prog = 
47 ef34b4ae xthirioux
    try
48 a2327c71 Lélio Brun
      Parse.(parse_filename (module Lexer_lustre) filename
49 90e83deb Lélio Brun
               (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 ef34b4ae xthirioux
    with
60 90e83deb Lélio Brun
    (* | (Parse.Error err) as exc ->
61
     *    Parse.report_error err;
62
     *    raise exc *)
63 04a188ec ploc
    | Error.Error (loc, err) as exc -> (
64 ef34b4ae xthirioux
      eprintf "Parsing error: %a%a@."
65 217837e2 ploc
        Error.pp_error_msg err
66
        Location.pp_loc loc;
67 ef34b4ae xthirioux
      raise exc
68
    )
69 217837e2 ploc
  in
70 90e83deb Lélio Brun
  (* close_in f_in; *)
71 217837e2 ploc
  prog
72
    
73 ef34b4ae xthirioux
74 04a63d25 xthirioux
let expand_automata decls =
75 7ee5f69e Lélio Brun
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. expanding automata@ ");
76 04a63d25 xthirioux
  try
77
    Automata.expand_decls decls
78 04a188ec ploc
  with (Error.Error (loc, err)) as exc ->
79 04a63d25 xthirioux
    eprintf "Automata error: %a%a@."
80 e7cc5186 ploc
      Error.pp_error_msg err
81 04a63d25 xthirioux
      Location.pp_loc loc;
82
    raise exc
83
84 ef34b4ae xthirioux
let check_stateless_decls decls =
85 7ee5f69e Lélio Brun
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. checking stateless/stateful status@ ");
86 ef34b4ae xthirioux
  try
87
    Stateless.check_prog decls
88
  with (Stateless.Error (loc, err)) as exc ->
89 ec433d69 xthirioux
    eprintf "Stateless status error: %a%a@."
90 ef34b4ae xthirioux
      Stateless.pp_error err
91
      Location.pp_loc loc;
92
    raise exc
93
94 04a63d25 xthirioux
let force_stateful_decls decls =
95 7ee5f69e Lélio Brun
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ .. forcing stateful status@ ");
96 04a63d25 xthirioux
  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 ef34b4ae xthirioux
let type_decls env decls =  
105 7ee5f69e Lélio Brun
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ @[<v 2>.. typing@ ");
106 ef34b4ae xthirioux
  let new_env = 
107 7ee5f69e Lélio Brun
    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 ef34b4ae xthirioux
  in
115 7ee5f69e Lélio Brun
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]");
116 e7cc5186 ploc
  if !Options.print_types || !Options.verbose_level > 2 then
117 ef34b4ae xthirioux
    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 7ee5f69e Lélio Brun
  Log.report ~level:1 (fun fmt -> fprintf fmt "@ @[<v 2>.. clock calculus@ ");
122 ef34b4ae xthirioux
  let new_env =
123 7ee5f69e Lélio Brun
    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 ef34b4ae xthirioux
  in
129 7ee5f69e Lélio Brun
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]");
130 e7cc5186 ploc
  if !Options.print_clocks  || !Options.verbose_level > 2 then
131 ef34b4ae xthirioux
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>  %a@]@ " Corelang.pp_prog_clock decls);
132
  new_env
133
134 2d27eedd ploc
(* Typing/Clocking with an empty env *)
135 ef34b4ae xthirioux
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 e70326c9 ploc
	 
157
158
    
159 ca7e8027 Lélio Brun
let check_compatibility (_, computed_types_env, computed_clocks_env) (header, declared_types_env, declared_clocks_env) =
160 ef34b4ae xthirioux
  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 6efbcb73 xthirioux
    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 ef34b4ae xthirioux
    raise exc
178
  | Clocks.Error (loc, err) as exc ->
179 6efbcb73 xthirioux
    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 ef34b4ae xthirioux
    raise exc
183
  | Stateless.Error (loc, err) as exc ->
184 6efbcb73 xthirioux
    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 ef34b4ae xthirioux
    raise exc
188
189 f4cba4b8 ploc
(* 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 1fd3d002 ploc
  let process_contract new_contracts c =
193 8a11dc80 ploc
    (* Format.eprintf "Process contract@."; *)
194 f4cba4b8 ploc
    (* 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 ef34b4ae xthirioux
204 f4cba4b8 ploc
             Last the contracts elements are replaced with the renamed vars and merged with c contract.
205
           *)
206
          let name = import.import_nodeid in
207 8a11dc80 ploc
          (* Format.eprintf "Process contract import %s@." name; *)
208 1fd3d002 ploc
          let loc = import.import_loc in
209 f4cba4b8 ploc
          try
210 1fd3d002 ploc
            let imp_nd = get_node name new_contracts in (* Get the contract node in process contracts *)
211 f4cba4b8 ploc
            (* checking that it's actually a (processed) contract *)
212 1fd3d002 ploc
            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 f4cba4b8 ploc
            in
222 1fd3d002 ploc
            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 f4cba4b8 ploc
            in
234 1fd3d002 ploc
            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 f4cba4b8 ploc
            let c = merge_contracts c imp_c in
238
            stmts, locals, c 
239 04a188ec ploc
          with Not_found -> Format.eprintf "Where is contract %s@.@?" name; raise (Error.Error (loc, (Error.Unbound_symbol ("contract " ^ name))))
240 f4cba4b8 ploc
241 1fd3d002 ploc
         
242 f4cba4b8 ploc
        ) ([], c.consts@c.locals, c) c.imports
243
    in
244 1fd3d002 ploc
    let stmts = stmts @ c.stmts in 
245 f4cba4b8 ploc
    (* Other contract elements will be normalized later *)
246 1fd3d002 ploc
    let c = { c with (* we erase locals and stmts sinced they are now in the parent node *)
247 f4cba4b8 ploc
              locals = [];
248
              consts = [];
249
              stmts = [];
250
              imports = []
251
            }
252
    in
253 1fd3d002 ploc
    
254
    (* 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
    
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 8a11dc80 ploc
    (* Format.eprintf "Process contract new node for node %s@." id; *)
267 1fd3d002 ploc
268 f4cba4b8 ploc
    let stmts, locals, c =
269
      match spec with
270
      | None | Some (NodeSpec _) -> assert false
271
      | Some (Contract c) ->
272 1fd3d002 ploc
         (* Format.eprintf "Processing contract of node %s@." id; *)
273
         process_contract accu_contracts c
274 f4cba4b8 ploc
    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 1fd3d002 ploc
        (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 f4cba4b8 ploc
    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 1fd3d002 ploc
             (* Format.eprintf "Processing top contract %s@." nd.node_id; *)
329
             let stmts, locals, c = process_contract accu_contracts c in
330 f4cba4b8 ploc
             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 ca7e8027 Lélio Brun
          | Some (NodeSpec _) -> (* shall not happen, its too early *)
345 f4cba4b8 ploc
             assert false
346 ca7e8027 Lélio Brun
          | Some (Contract _) -> (* A contract: processing it *)
347 f4cba4b8 ploc
             (* we bind a fresh node *)
348
             let new_nd = process_contract_new_node accu_contracts prog top in
349 1fd3d002 ploc
             (* Format.eprintf "Creating new contract node %s@." (node_name new_nd); *)
350 f4cba4b8 ploc
             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 ca7e8027 Lélio Brun
          | Some (NodeSpec _) -> (* shall not happen, its too early *)
360 f4cba4b8 ploc
             assert false
361 ca7e8027 Lélio Brun
          | Some (Contract _) -> (* A contract: processing it *)
362 f4cba4b8 ploc
             (* 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 990210f3 ploc
let track_exception () =
376
  if !Options.track_exceptions
377
  then (Printexc.print_backtrace stdout; flush stdout)
378
  else ()
379
380
381 66359a5e ploc
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