Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / compiler_common.ml @ 04a188ec

History | View | Annotate | Download (14.4 KB)

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
      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
    with
59
    | (Parse.Error err) as exc -> 
60
       Parse.report_error err;
61
       raise exc
62
    | Error.Error (loc, err) as exc -> (
63
      eprintf "Parsing error: %a%a@."
64
        Error.pp_error_msg err
65
        Location.pp_loc loc;
66
      raise exc
67
    )
68
  in
69
  close_in f_in;
70
  prog
71
    
72

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

    
83
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
    eprintf "Stateless status error: %a%a@."
89
      Stateless.pp_error err
90
      Location.pp_loc loc;
91
    raise exc
92

    
93
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
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
	eprintf "Typing error: %a%a@."
111
	  Types.pp_error err
112
	  Location.pp_loc loc;
113
	raise exc
114
    end 
115
  in
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 ".. 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
	eprintf "Clock calculus error: %a%a@." Clocks.pp_error err Location.pp_loc loc;
128
	raise exc
129
    end
130
  in
131
  if !Options.print_clocks  || !Options.verbose_level > 2 then
132
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>  %a@]@ " Corelang.pp_prog_clock decls);
133
  new_env
134

    
135
(* Typing/Clocking with an empty env *)
136
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
	 
158

    
159
    
160
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
    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
    raise exc
179
  | Clocks.Error (loc, err) as exc ->
180
    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
    raise exc
184
  | Stateless.Error (loc, err) as exc ->
185
    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
    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 binded contract node. Clean the contract to remove the stmts  *)
193
  let process_contract new_contracts c =
194
    (* Format.eprintf "Process contract@."; *)
195
    (* 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

    
205
             Last the contracts elements are replaced with the renamed vars and merged with c contract.
206
           *)
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 (* Get the contract node in process contracts *)
212
            (* checking that it's actually a (processed) contract *)
213
            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
            in
223
            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
            in
235
            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
            let c = merge_contracts c imp_c in
239
            stmts, locals, c 
240
          with Not_found -> Format.eprintf "Where is contract %s@.@?" name; raise (Error.Error (loc, (Error.Unbound_symbol ("contract " ^ name))))
241

    
242
         
243
        ) ([], c.consts@c.locals, c) c.imports
244
    in
245
    let stmts = stmts @ c.stmts in 
246
    (* Other contract elements will be normalized later *)
247
    let c = { c with (* we erase locals and stmts sinced they are now in the parent node *)
248
              locals = [];
249
              consts = [];
250
              stmts = [];
251
              imports = []
252
            }
253
    in
254
    
255
    (* Format.eprintf "Processed stmts: %a@." Printers.pp_node_stmts stmts;
256
     * Format.eprintf "Processed locals: %a@." Printers.pp_vars locals; *)
257
    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
    (* Format.eprintf "Process contract new node for node %s@." id; *)
268

    
269
    let stmts, locals, c =
270
      match spec with
271
      | None | Some (NodeSpec _) -> assert false
272
      | Some (Contract c) ->
273
         (* Format.eprintf "Processing contract of node %s@." id; *)
274
         process_contract accu_contracts c
275
    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
        (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
    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
             (* Format.eprintf "Processing top contract %s@." nd.node_id; *)
330
             let stmts, locals, c = process_contract accu_contracts c in
331
             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
             (* Format.eprintf "Creating new contract node %s@." (node_name new_nd); *)
351
             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
let track_exception () =
377
  if !Options.track_exceptions
378
  then (Printexc.print_backtrace stdout; flush stdout)
379
  else ()
380

    
381

    
382
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