Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / compiler_common.ml @ e6b644f4

History | View | Annotate | Download (14.4 KB)

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