Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / compiler_common.ml @ f4cba4b8

History | View | Annotate | Download (13.3 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 (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
    | Corelang.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 (Corelang.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 prog c =
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
          assert false; (* TODO: we do not handle imports yet.  The
208
                           algorithm is sketched below *)
209
        (*
210
          try
211
            let imp_nd = xxx in (* Get the contract node in prog *)
212
            (* checking that it's actually a (processed) contract *)
213
            let imp_c =
214
              match imp_nd.node_spec with
215
                Some (Contract imp_c) ->
216
                 if imp_c.imports = [] then
217
                   imp_c
218
                 else
219
                   assert false (* should be processed *)
220
              | _ -> assert false (* should be a contract *)
221
            in  
222
            (* Preparing vars: renaming them *)
223
            let imp_in = rename imp_nd.node_inputs in
224
            let imp_out = rename imp_nd.node_outputs in
225
            let imp_locals = rename imp_nd.node_locals in
226
            let locals = imp_in@imp_out@imp_locals@locals in
227
            (* Assinging in and out *)
228
            let in_assigns =
229
              xxx imp_in = import.inputs
230
            in
231
            let out_assigns =
232
              xxx imp_out = import.outputs
233
            in
234
            let stmts = stmts @ (rename imp_nd.stmts) in
235
            let imp_c = rename imp_c in
236
            let c = merge_contracts c imp_c in
237
            stmts, locals, c 
238
          with Not_found -> raise (Error.Unbound_symbol ("contract " ^ name))
239

    
240
                            *)
241
        ) ([], c.consts@c.locals, c) c.imports
242
    in
243
    (* Other contract elements will be normalized later *)
244
    let c = { c with
245
              locals = [];
246
              consts = [];
247
              stmts = [];
248
              imports = []
249
            }
250
    in
251
    stmts, locals, c
252
    
253
  in
254
  let process_contract_new_node accu_contracts prog top =
255
    let id, spec, inputs, outputs =
256
      match top.top_decl_desc with
257
      | Node nd -> nd.node_id, nd.node_spec, nd.node_inputs, nd.node_outputs
258
      | ImportedNode ind -> ind.nodei_id, ind.nodei_spec, ind.nodei_inputs, ind.nodei_outputs
259
      | _ -> assert false
260
    in
261
    let stmts, locals, c =
262
      match spec with
263
      | None | Some (NodeSpec _) -> assert false
264
      | Some (Contract c) ->
265
         process_contract accu_contracts prog c
266
    in
267
    (* Create a fresh name *)
268
    let used v = List.exists (fun top ->
269
                     match top.top_decl_desc with
270
                     | Node _
271
                       | ImportedNode _ ->
272
                        (node_name top) = v
273
                     | _ -> false
274
                   ) (accu_contracts@prog)
275
    in
276
    let new_nd_id = mk_new_name used (id ^ "_coco") in
277
    let new_nd =
278
      mktop_decl
279
        c.spec_loc
280
        top.top_decl_owner
281
        top.top_decl_itf
282
      (Node {
283
           node_id = new_nd_id;
284
	   node_type = Types.new_var ();
285
	   node_clock = Clocks.new_var true;
286
	   node_inputs = inputs;
287
	   node_outputs = outputs;
288
	   node_locals = locals;
289
	   node_gencalls = [];
290
	   node_checks = [];
291
	   node_asserts = []; 
292
	   node_stmts = stmts;
293
	   node_dec_stateless = false;
294
	   node_stateless = None;
295
	   node_spec = Some (Contract c);
296
	   node_annot = [];
297
	   node_iscontract = true;
298
      }) in
299
    new_nd
300
  in
301
  (* Processing nodes in order. Should have been sorted by now
302

    
303
     Each top level contract is processed: stmts pushed in node
304

    
305
     Each regular imported node or node associated with a contract is
306
     replaced with a simplidfied contract and its contract is bound to
307
     a fresh node.
308

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

    
365
  
366
let track_exception () =
367
  if !Options.track_exceptions
368
  then (Printexc.print_backtrace stdout; flush stdout)
369
  else ()
370

    
371

    
372
let update_vdecl_parents_prog prog =
373
  let update_vdecl_parents parent v =
374
    v.var_parent_nodeid <- Some parent
375
  in
376
  List.iter (
377
    fun top -> match top.top_decl_desc with
378
    | Node nd ->
379
       List.iter
380
	 (update_vdecl_parents nd.node_id)
381
	 (nd.node_inputs @ nd.node_outputs @ nd.node_locals )  
382
    | ImportedNode ind -> 
383
       List.iter
384
	 (update_vdecl_parents ind.nodei_id)
385
	 (ind.nodei_inputs @ ind.nodei_outputs )  
386
    | _ -> ()
387
  ) prog