Project

General

Profile

Download (19.4 KB) Statistics
| Branch: | Tag: | Revision:
1 a2d97a3e ploc
(********************************************************************)
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 22fe1c93 ploc
12 8446bf03 ploc
open Lustre_types
13
open Machine_code_types
14 2863281f ploc
open Machine_code_common
15 75c459f4 Lélio Brun
open Spec_types
16
open Spec_common
17 22fe1c93 ploc
open Corelang
18
open Clocks
19
open Causality
20 75c459f4 Lélio Brun
open Utils
21 7ee5f69e Lélio Brun
22 22fe1c93 ploc
exception NormalizationError
23
24 5de4dde4 ploc
(* Questions:
25
26
   - where are used the mconst. They contain initialization of
27 7ee5f69e Lélio Brun
     constant in nodes. But they do not seem to be used by c_backend *)
28
29 22fe1c93 ploc
30 59020713 ploc
(* translate_<foo> : vars -> context -> <foo> -> machine code/expression *)
31 22fe1c93 ploc
(* the context contains  m : state aka memory variables  *)
32
(*                      si : initialization instructions *)
33
(*                       j : node aka machine instances  *)
34
(*                       d : local variables             *)
35
(*                       s : step instructions           *)
36 5de4dde4 ploc
37
(* Machine processing requires knowledge about variables and local
38
   variables. Local could be memories while other could not.  *)
39
type machine_env = {
40 7ee5f69e Lélio Brun
  is_local: string -> bool;
41
  get_var: string -> var_decl
42
}
43
44 5de4dde4 ploc
45 6d1693b9 Lélio Brun
let build_env inputs locals outputs =
46
  let all = List.sort_uniq VDeclModule.compare (locals @ inputs @ outputs) in
47
  { is_local = (fun id -> List.exists (fun v -> v.var_id = id) locals);
48
    get_var = (fun id -> try List.find (fun v -> v.var_id = id) all with Not_found ->
49 7ee5f69e Lélio Brun
        (* Format.eprintf "Impossible to find variable %s in set %a@.@?"
50
         *   id
51
         *   VSet.pp all; *)
52
        raise Not_found)
53 5de4dde4 ploc
  }
54
55 7ee5f69e Lélio Brun
56 5de4dde4 ploc
57
(****************************************************************)
58
(* Basic functions to translate to machine values, instructions *) 
59
(****************************************************************)
60
61
let translate_ident env id =
62 380a8d33 ploc
  (* Format.eprintf "trnaslating ident: %s@." id; *)
63 75c459f4 Lélio Brun
  (* id is a var that shall be visible here , ie. in vars *)
64
  try
65 5de4dde4 ploc
    let var_id = env.get_var id in
66 6d1693b9 Lélio Brun
    vdecl_to_val var_id
67 ef34b4ae xthirioux
  with Not_found ->
68 75c459f4 Lélio Brun
69
 (* id is a constant *)
70
  try
71 7ee5f69e Lélio Brun
    let vdecl = (Corelang.var_decl_of_const
72
                   (const_of_top (Hashtbl.find Corelang.consts_table id)))
73
    in
74 6d1693b9 Lélio Brun
    vdecl_to_val vdecl
75 7ee5f69e Lélio Brun
  with Not_found ->
76 75c459f4 Lélio Brun
77
   (* id is a tag, getting its type in the list of declared enums *)
78 7ee5f69e Lélio Brun
  try
79 6d1693b9 Lélio Brun
    id_to_tag id
80 7ee5f69e Lélio Brun
  with Not_found ->
81
    Format.eprintf "internal error: Machine_code.translate_ident %s@.@?" id;
82
    assert false
83 22fe1c93 ploc
84
85 5de4dde4 ploc
(* specialize predefined (polymorphic) operators wrt their instances,
86
   so that the C semantics is preserved *)
87 25b4311f xthirioux
let specialize_to_c expr =
88 7ee5f69e Lélio Brun
  match expr.expr_desc with
89
  | Expr_appl (id, e, r) ->
90
    if List.exists (fun e -> Types.is_bool_type e.expr_type) (expr_list_of_expr e)
91
    then let id =
92
           match id with
93
           | "="  -> "equi"
94
           | "!=" -> "xor"
95
           | _    -> id in
96
      { expr with expr_desc = Expr_appl (id, e, r) }
97
    else expr
98
  | _ -> expr
99 25b4311f xthirioux
100
let specialize_op expr =
101
  match !Options.output with
102
  | "C" -> specialize_to_c expr
103
  | _   -> expr
104
105 5de4dde4 ploc
let rec translate_expr env expr =
106 f2b1c245 ploc
  let expr = specialize_op expr in
107 5de4dde4 ploc
  let translate_expr = translate_expr env in
108 04a63d25 xthirioux
  let value_desc = 
109
    match expr.expr_desc with
110 7ee5f69e Lélio Brun
    | Expr_const v ->
111
      Cst v
112
    | Expr_ident x ->
113
      (translate_ident env x).value_desc
114
    | Expr_array el ->
115
      Array (List.map translate_expr el)
116
    | Expr_access (t, i) ->
117
      Access (translate_expr t, translate_expr (expr_of_dimension i))
118
    | Expr_power  (e, n) ->
119
      Power (translate_expr e, translate_expr (expr_of_dimension n))
120
    | Expr_when (e1, _, _) ->
121
      (translate_expr e1).value_desc
122 04a63d25 xthirioux
    | Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr ->
123 7ee5f69e Lélio Brun
      let nd = node_from_name id in
124
      Fun (node_name nd, List.map translate_expr (expr_list_of_expr e))
125
    | Expr_ite (g,t,e) when Backends.is_functional () ->
126 5de4dde4 ploc
      (* special treatment depending on the active backend. For
127
         functional ones, like horn backend, ite are preserved in
128
         expression. While they are removed for C or Java backends. *)
129 7ee5f69e Lélio Brun
      Fun ("ite", [translate_expr g; translate_expr t; translate_expr e])
130
    | _ ->
131
      Format.eprintf "Normalization error for backend %s: %a@."
132
        !Options.output
133
        Printers.pp_expr expr;
134
      raise NormalizationError
135 04a63d25 xthirioux
  in
136
  mk_val value_desc expr.expr_type
137 22fe1c93 ploc
138 5de4dde4 ploc
let translate_guard env expr =
139 0777a7be ploc
  match expr.expr_desc with
140 7ee5f69e Lélio Brun
  | Expr_ident x -> translate_ident env x
141
  | _ ->
142
    Format.eprintf "internal error: translate_guard %a@." Printers.pp_expr expr;
143
    assert false
144 22fe1c93 ploc
145 5de4dde4 ploc
let rec translate_act env (y, expr) =
146
  let translate_act = translate_act env in
147
  let translate_guard = translate_guard env in
148 6d1693b9 Lélio Brun
  (* let translate_ident = translate_ident env in *)
149 5de4dde4 ploc
  let translate_expr = translate_expr env in
150 7ee5f69e Lélio Brun
  let lustre_eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in
151 0777a7be ploc
  match expr.expr_desc with
152 7ee5f69e Lélio Brun
  | Expr_ite (c, t, e) ->
153 6d1693b9 Lélio Brun
    let c = translate_guard c in
154
    let t, spec_t = translate_act (y, t) in
155
    let e, spec_e = translate_act (y, e) in
156
    mk_conditional ~lustre_eq c [t] [e],
157
    mk_conditional_tr c spec_t spec_e
158 7ee5f69e Lélio Brun
  | Expr_merge (x, hl) ->
159 6d1693b9 Lélio Brun
    let var_x = env.get_var x in
160
    let hl, spec_hl = List.(split (map (fun (t, h) ->
161
        let h, spec_h = translate_act (y, h) in
162
        (t, [h]), (t, spec_h))
163
        hl)) in
164
    mk_branch ~lustre_eq var_x hl,
165
    mk_branch_tr var_x spec_hl
166 75c459f4 Lélio Brun
  | _ ->
167 6d1693b9 Lélio Brun
    let e = translate_expr expr in
168
    mk_assign ~lustre_eq y e,
169
    mk_assign_tr y e
170
171
let get_memory env mems eq = match eq.eq_lhs, eq.eq_rhs.expr_desc with
172
  | ([x], Expr_pre _ | [x], Expr_fby _) when env.is_local x ->
173
    let var_x = env.get_var x in
174
    VSet.add var_x mems
175
  | _ -> mems
176
177
let get_memories env =
178
  List.fold_left (get_memory env) VSet.empty
179 5de4dde4 ploc
180
(* Datastructure updated while visiting equations *)
181
type machine_ctx = {
182 75c459f4 Lélio Brun
  (* Reset instructions *)
183 7ee5f69e Lélio Brun
  si: instr_t list;
184 75c459f4 Lélio Brun
  (* Instances *)
185
  j: (Lustre_types.top_decl * Dimension.dim_expr list) IMap.t;
186
  (* Step instructions *)
187 7ee5f69e Lélio Brun
  s: instr_t list;
188 75c459f4 Lélio Brun
  (* Memory pack spec *)
189
  mp: mc_formula_t list;
190
  (* Transition spec *)
191 6d1693b9 Lélio Brun
  t: (var_decl list * var_decl list * var_decl list * mc_formula_t) list;
192 7ee5f69e Lélio Brun
}
193 5de4dde4 ploc
194 6d1693b9 Lélio Brun
let ctx_init = {
195 75c459f4 Lélio Brun
  si = [];
196
  j = IMap.empty;
197
  s = [];
198
  mp = [];
199
  t = []
200
}
201 7ee5f69e Lélio Brun
202 5de4dde4 ploc
(****************************************************************)
203
(* Main function to translate equations into this machine context we
204
   are building *) 
205
(****************************************************************)
206
207 6cbbe1c1 Lélio Brun
let mk_control v l inst =
208 75c459f4 Lélio Brun
  mkinstr
209 6d1693b9 Lélio Brun
    (MBranch (vdecl_to_val v, [l, [inst]]))
210 75c459f4 Lélio Brun
211 6d1693b9 Lélio Brun
let control_on_clock env ck inst =
212
  let rec aux (fspec, inst as acc) ck =
213 75c459f4 Lélio Brun
    match (Clocks.repr ck).cdesc with
214
    | Con (ck, cr, l) ->
215
      let id = Clocks.const_of_carrier cr in
216 6d1693b9 Lélio Brun
      let v = env.get_var id in
217
      aux ((fun spec -> Imply (Equal (Var v, Tag l), fspec spec)),
218
           mk_control v l inst)
219
        ck
220 75c459f4 Lélio Brun
    | _ -> acc
221
  in
222 6d1693b9 Lélio Brun
  let fspec, inst = aux ((fun spec -> spec), inst) ck in
223
  fspec, inst
224 75c459f4 Lélio Brun
225
let reset_instance env i r c =
226
  match r with
227
  | Some r ->
228 6d1693b9 Lélio Brun
    let _, inst = control_on_clock env c
229 6cbbe1c1 Lélio Brun
        (mk_conditional
230
           (translate_guard env r)
231 6d1693b9 Lélio Brun
           [mkinstr (MSetReset i)]
232
           [mkinstr (MNoReset i)]) in
233 6cbbe1c1 Lélio Brun
    [ inst ]
234 75c459f4 Lélio Brun
  | None -> []
235 7ee5f69e Lélio Brun
236 6d1693b9 Lélio Brun
let translate_eq env ctx id inputs locals outputs i eq =
237 5de4dde4 ploc
  let translate_expr = translate_expr env in
238
  let translate_act = translate_act env in
239 6d1693b9 Lélio Brun
  let locals_pi = Lustre_live.inter_live_i_with id (i-1) locals in
240
  let outputs_pi = Lustre_live.inter_live_i_with id (i-1) outputs in
241
  let locals_i = Lustre_live.inter_live_i_with id i locals in
242
  let outputs_i = Lustre_live.inter_live_i_with id i outputs in
243
  let pred_mp ctx a =
244
    And [mk_memory_pack ~i:(i-1) id; a] :: ctx.mp in
245
  let pred_t ctx a =
246
    (inputs, locals_i, outputs_i,
247
     Exists
248
       (Lustre_live.existential_vars id i eq (locals @ outputs),
249
        And [
250
          mk_transition ~i:(i-1) id
251
            (vdecls_to_vals inputs)
252
            (vdecls_to_vals locals_pi)
253
            (vdecls_to_vals outputs_pi);
254
          a
255
        ]))
256
    :: ctx.t in
257
  let control_on_clock ck inst spec_mp spec_t =
258
    let fspec, inst = control_on_clock env ck inst in
259 6cbbe1c1 Lélio Brun
    { ctx with
260
      s = { inst with
261 6d1693b9 Lélio Brun
            instr_spec = [
262
              mk_memory_pack ~i id;
263
              mk_transition ~i id
264
                (vdecls_to_vals inputs)
265
                (vdecls_to_vals locals_i)
266
                (vdecls_to_vals outputs_i)
267
            ] }
268
          :: ctx.s;
269
      mp = pred_mp ctx spec_mp;
270
      t = pred_t ctx (fspec spec_t);
271
    }
272 75c459f4 Lélio Brun
  in
273 5de4dde4 ploc
  let reset_instance = reset_instance env in
274 6d1693b9 Lélio Brun
  let mkinstr' = mkinstr ~lustre_eq:eq in
275
  let ctl ?(ck=eq.eq_rhs.expr_clock) instr spec_mp spec_t =
276
    control_on_clock ck (mkinstr' instr) spec_mp spec_t in
277 22fe1c93 ploc
278 59020713 ploc
  (* Format.eprintf "translate_eq %a with clock %a@." 
279
     Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;  *)
280 22fe1c93 ploc
  match eq.eq_lhs, eq.eq_rhs.expr_desc with
281
  | [x], Expr_arrow (e1, e2)                     ->
282 7ee5f69e Lélio Brun
    let var_x = env.get_var x in
283 6cbbe1c1 Lélio Brun
    let td = Arrow.arrow_top_decl () in
284 6d1693b9 Lélio Brun
    let inst = new_instance td eq.eq_rhs.expr_tag in
285 7ee5f69e Lélio Brun
    let c1 = translate_expr e1 in
286
    let c2 = translate_expr e2 in
287 6d1693b9 Lélio Brun
    assert (c1.value_desc = Cst (Const_tag "true"));
288
    assert (c2.value_desc = Cst (Const_tag "false"));
289 6cbbe1c1 Lélio Brun
    let ctx = ctl
290 6d1693b9 Lélio Brun
        (MStep ([var_x], inst, [c1; c2]))
291
        (mk_memory_pack ~inst (node_name td))
292
        (mk_transition ~inst (node_name td) [] [] [vdecl_to_val var_x])
293
    in
294 7ee5f69e Lélio Brun
    { ctx with
295 6d1693b9 Lélio Brun
      si = mkinstr (MSetReset inst) :: ctx.si;
296
      j = IMap.add inst (td, []) ctx.j;
297 7ee5f69e Lélio Brun
    }
298 6cbbe1c1 Lélio Brun
299 6d1693b9 Lélio Brun
  | [x], Expr_pre e when env.is_local x    ->
300 7ee5f69e Lélio Brun
    let var_x = env.get_var x in
301 6d1693b9 Lélio Brun
    let e = translate_expr e in
302
    ctl
303
      (MStateAssign (var_x, e))
304
      (mk_state_variable_pack var_x)
305
      (mk_state_assign_tr var_x e)
306 6cbbe1c1 Lélio Brun
307 5de4dde4 ploc
  | [x], Expr_fby (e1, e2) when env.is_local x ->
308 7ee5f69e Lélio Brun
    let var_x = env.get_var x in
309 6d1693b9 Lélio Brun
    let e2 = translate_expr e2 in
310 6cbbe1c1 Lélio Brun
    let ctx = ctl
311 6d1693b9 Lélio Brun
        (MStateAssign (var_x, e2))
312
        (mk_state_variable_pack var_x)
313
        (mk_state_assign_tr var_x e2)
314
    in
315 7ee5f69e Lélio Brun
    { ctx with
316
      si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si;
317
    }
318 6cbbe1c1 Lélio Brun
319 7ee5f69e Lélio Brun
  | p, Expr_appl (f, arg, r)
320
    when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
321
    let var_p = List.map (fun v -> env.get_var v) p in
322
    let el = expr_list_of_expr arg in
323
    let vl = List.map translate_expr el in
324
    let node_f = node_from_name f in
325
    let call_f = node_f, NodeDep.filter_static_inputs (node_inputs node_f) el in
326 6d1693b9 Lélio Brun
    let inst = new_instance node_f eq.eq_rhs.expr_tag in
327 7ee5f69e Lélio Brun
    let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks)
328
        el [eq.eq_rhs.expr_clock] in
329
    let call_ck = Clock_calculus.compute_root_clock
330
        (Clock_predef.ck_tuple env_cks) in
331 6cbbe1c1 Lélio Brun
    let ctx = ctl
332
        ~ck:call_ck
333 6d1693b9 Lélio Brun
        (MStep (var_p, inst, vl))
334
        (mk_memory_pack ~inst (node_name node_f))
335
        (mk_transition ~inst (node_name node_f) vl [] (vdecls_to_vals var_p))
336
    in
337 7ee5f69e Lélio Brun
    (*Clocks.new_var true in
338
      Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
339
      Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*)
340
    { ctx with
341
      si = if Stateless.check_node node_f
342 6d1693b9 Lélio Brun
        then ctx.si else mkinstr (MSetReset inst) :: ctx.si;
343
      j = IMap.add inst call_f ctx.j;
344 5de4dde4 ploc
      s = (if Stateless.check_node node_f
345 75c459f4 Lélio Brun
           then []
346 6d1693b9 Lélio Brun
           else reset_instance inst r call_ck)
347
          @ ctx.s;
348 7ee5f69e Lélio Brun
    }
349 6cbbe1c1 Lélio Brun
350 7ee5f69e Lélio Brun
  | [x], _ ->
351 5de4dde4 ploc
    let var_x = env.get_var x in
352 6d1693b9 Lélio Brun
    let instr, spec = translate_act (var_x, eq.eq_rhs) in
353
    control_on_clock eq.eq_rhs.expr_clock instr True spec
354 6cbbe1c1 Lélio Brun
355 7ee5f69e Lélio Brun
  | _ ->
356
    Format.eprintf "internal error: Machine_code.translate_eq %a@?"
357
      Printers.pp_node_eq eq;
358
    assert false
359 a38c681e xthirioux
360 5de4dde4 ploc
let constant_equations locals =
361 6d1693b9 Lélio Brun
  List.fold_left (fun eqs vdecl ->
362 7ee5f69e Lélio Brun
      if vdecl.var_dec_const
363
      then
364
        { eq_lhs = [vdecl.var_id];
365 75c459f4 Lélio Brun
          eq_rhs = desome vdecl.var_dec_value;
366 7ee5f69e Lélio Brun
          eq_loc = vdecl.var_loc
367
        } :: eqs
368
      else eqs)
369 6d1693b9 Lélio Brun
    [] locals
370 ec433d69 xthirioux
371 6d1693b9 Lélio Brun
let translate_eqs env ctx id inputs locals outputs eqs =
372 6cbbe1c1 Lélio Brun
  List.fold_right (fun eq (ctx, i) ->
373 6d1693b9 Lélio Brun
      let ctx = translate_eq env ctx id inputs locals outputs i eq in
374 6cbbe1c1 Lélio Brun
      ctx, i - 1)
375
    eqs (ctx, List.length eqs)
376
  |> fst
377 5de4dde4 ploc
378
379
(****************************************************************)
380
(* Processing nodes *) 
381
(****************************************************************)
382 22fe1c93 ploc
383 59020713 ploc
let process_asserts nd =
384 7ee5f69e Lélio Brun
385
  let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
386
  if Backends.is_functional () then
387
    [], [], exprl
388
  else (* Each assert(e) is associated to a fresh variable v and declared as
389
          v=e; assert (v); *)
390
    let _, vars, eql, assertl =
391
      List.fold_left (fun (i, vars, eqlist, assertlist) expr ->
392
          let loc = expr.expr_loc in
393
          let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in
394
          let assert_var =
395
            mkvar_decl
396
              loc
397
              ~orig:false (* fresh var *)
398
              (var_id,
399
               mktyp loc Tydec_bool,
400
               mkclock loc Ckdec_any,
401
               false, (* not a constant *)
402
               None, (* no default value *)
403
               Some nd.node_id
404
              )
405
          in
406
          assert_var.var_type <- Type_predef.type_bool (* Types.new_ty (Types.Tbool) *);
407
          let eq = mkeq loc ([var_id], expr) in
408 5de4dde4 ploc
          (i+1,
409
           assert_var::vars,
410
           eq::eqlist,
411
           {expr with expr_desc = Expr_ident var_id}::assertlist)
412 7ee5f69e Lélio Brun
        ) (1, [], [], []) exprl
413
    in
414
    vars, eql, assertl
415 5de4dde4 ploc
416 6d1693b9 Lélio Brun
let translate_core env nid sorted_eqs inputs locals outputs =
417 5de4dde4 ploc
  let constant_eqs = constant_equations locals in
418 7ee5f69e Lélio Brun
419 5de4dde4 ploc
  (* Compute constants' instructions  *)
420 6d1693b9 Lélio Brun
  let ctx0 = translate_eqs env ctx_init nid inputs locals outputs constant_eqs in
421 5de4dde4 ploc
  assert (ctx0.si = []);
422 75c459f4 Lélio Brun
  assert (IMap.is_empty ctx0.j);
423 7ee5f69e Lélio Brun
424 5de4dde4 ploc
  (* Compute ctx for all eqs *)
425 6d1693b9 Lélio Brun
  let ctx = translate_eqs env ctx_init nid inputs locals outputs sorted_eqs in
426 7ee5f69e Lélio Brun
427 5de4dde4 ploc
  ctx, ctx0.s
428 0d065e73 ploc
429 6d1693b9 Lélio Brun
let zero = mk_val (Cst (Const_int 0)) Type_predef.type_int
430
431
let memory_pack_0 nd =
432
  {
433
    mpname = nd;
434
    mpindex = Some 0;
435
    mpformula = And [StateVarPack ResetFlag; Equal (Memory ResetFlag, Val zero)]
436
  }
437
438
let memory_pack_toplevel nd i =
439
  {
440
    mpname = nd;
441
    mpindex = None;
442
    mpformula = Ternary (Memory ResetFlag,
443
                         StateVarPack ResetFlag,
444
                         mk_memory_pack ~i nd.node_id)
445
  }
446
447
let transition_0 nd =
448
  {
449
    tname = nd;
450
    tindex = Some 0;
451
    tinputs = nd.node_inputs;
452
    tlocals = [];
453
    toutputs = [];
454
    tformula = True;
455
  }
456
457
let transition_toplevel nd i =
458
  {
459
    tname = nd;
460
    tindex = None;
461
    tinputs = nd.node_inputs;
462
    tlocals = [];
463
    toutputs = nd.node_outputs;
464
    tformula = ExistsMem (Predicate (ResetCleared nd.node_id),
465
                          mk_transition nd.node_id ~i
466
                            (vdecls_to_vals (nd.node_inputs))
467
                            []
468
                            (vdecls_to_vals nd.node_outputs));
469
  }
470 7ee5f69e Lélio Brun
471 5de4dde4 ploc
let translate_decl nd sch =
472 1fd3d002 ploc
  (* Format.eprintf "Translating node %s@." nd.node_id; *)
473 5de4dde4 ploc
  (* Extracting eqs, variables ..  *)
474
  let eqs, auts = get_node_eqs nd in
475
  assert (auts = []); (* Automata should be expanded by now *)
476 7ee5f69e Lélio Brun
477 59020713 ploc
  (* In case of non functional backend (eg. C), additional local variables have
478
     to be declared for each assert *)
479
  let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in
480 5de4dde4 ploc
481
  (* Build the env: variables visible in the current scope *)
482 6d1693b9 Lélio Brun
  let locals = nd.node_locals @ new_locals in
483
  (* let locals = VSet.of_list locals_list in *)
484
  (* let inout_vars = nd.node_inputs @ nd.node_outputs in *)
485
  let env = build_env nd.node_inputs locals nd.node_outputs in
486 1fd3d002 ploc
487
  (* Format.eprintf "Node content is %a@." Printers.pp_node nd; *)
488 7ee5f69e Lélio Brun
489 5de4dde4 ploc
  (* Computing main content *)
490 1fd3d002 ploc
  (* Format.eprintf "ok1@.@?"; *)
491 5de4dde4 ploc
  let schedule = sch.Scheduling_type.schedule in
492 1fd3d002 ploc
  (* Format.eprintf "ok2@.@?"; *)
493 25320f03 ploc
  let sorted_eqs, unused = Scheduling.sort_equations_from_schedule eqs schedule in
494 1fd3d002 ploc
  (* Format.eprintf "ok3@.locals=%a@.inout:%a@?"
495
   *   VSet.pp locals
496
   *   VSet.pp inout_vars
497
   * ; *)
498 7ee5f69e Lélio Brun
499 6d1693b9 Lélio Brun
  let equations = assert_instrs @ sorted_eqs in
500
  let mems = get_memories env equations in
501
  (* Removing computed memories from locals. We also removed unused variables. *)
502
  let locals = List.filter
503
      (fun v -> not (VSet.mem v mems) && not (List.mem v.var_id unused)) locals in
504
  (* Compute live sets for spec *)
505
  Lustre_live.set_live_of nd.node_id nd.node_outputs locals equations;
506
507
  (* Translate equations *)
508
  let ctx, ctx0_s = translate_core env nd.node_id equations
509
     nd.node_inputs locals nd.node_outputs in
510 7ee5f69e Lélio Brun
511 1fd3d002 ploc
  (* Format.eprintf "ok4@.@?"; *)
512 25320f03 ploc
513 6d1693b9 Lélio Brun
  (* Build the machine *)
514 75c459f4 Lélio Brun
  let mmap = IMap.bindings ctx.j in
515 6d1693b9 Lélio Brun
  let mmemory_packs =
516
    memory_pack_0 nd
517
    :: List.mapi (fun i f ->
518
      {
519
        mpname = nd;
520
        mpindex = Some (i + 1);
521
        mpformula = red f
522
      }) ctx.mp
523
    @ [memory_pack_toplevel nd (List.length ctx.mp)]
524
  in
525
  let mtransitions =
526
    transition_0 nd
527
    :: List.mapi (fun i (tinputs, tlocals, toutputs, f) ->
528
        {
529
          tname = nd;
530
          tindex = Some (i + 1);
531
          tinputs;
532
          tlocals;
533
          toutputs;
534
          tformula = red f;
535
        }) ctx.t
536
    @ [transition_toplevel nd (List.length ctx.t)]
537
  in
538
  let clear_reset = mkinstr ~instr_spec:[
539
      mk_memory_pack ~i:0 nd.node_id;
540
      mk_transition ~i:0 nd.node_id
541
        (vdecls_to_vals nd.node_inputs)
542
        []
543
        []] MClearReset in
544 22fe1c93 ploc
  {
545
    mname = nd;
546 6d1693b9 Lélio Brun
    mmemory = VSet.elements mems;
547 22fe1c93 ploc
    mcalls = mmap;
548 e135421f xthirioux
    minstances = List.filter (fun (_, (n,_)) -> not (Stateless.check_node n)) mmap;
549 5de4dde4 ploc
    minit = ctx.si;
550
    mconst = ctx0_s;
551 22fe1c93 ploc
    mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs;
552
    mstep = {
553 7ee5f69e Lélio Brun
      step_inputs = nd.node_inputs;
554
      step_outputs = nd.node_outputs;
555 6d1693b9 Lélio Brun
      step_locals = locals;
556 7ee5f69e Lélio Brun
      step_checks = List.map (fun d -> d.Dimension.dim_loc,
557
                                       translate_expr env
558
                                         (expr_of_dimension d))
559
          nd.node_checks;
560 6d1693b9 Lélio Brun
      step_instrs = clear_reset ::
561
                    (* special treatment depending on the active backend. For horn backend,
562
                       common branches are not merged while they are in C or Java
563
                       backends. *)
564
                    (if !Backends.join_guards then
565
                       join_guards_list ctx.s
566
                     else
567
                       ctx.s);
568 7ee5f69e Lélio Brun
      step_asserts = List.map (translate_expr env) nd_node_asserts;
569
    };
570 f4cba4b8 ploc
571
    (* Processing spec: there is no processing performed here. Contract
572 7ee5f69e Lélio Brun
       have been processed already. Either one of the other machine is a
573
       cocospec node, or the current one is a cocospec node. Contract do
574
       not contain any statement or import. *)
575
576 6d1693b9 Lélio Brun
    mspec = { mnode_spec = nd.node_spec; mtransitions; mmemory_packs };
577 22fe1c93 ploc
    mannot = nd.node_annot;
578 95fb046e ploc
    msch = Some sch;
579 22fe1c93 ploc
  }
580
581 ec433d69 xthirioux
(** takes the global declarations and the scheduling associated to each node *)
582 88486aaf ploc
let translate_prog decls node_schs =
583 e9b71779 tkahsai
  let nodes = get_nodes decls in
584 f4cba4b8 ploc
  let machines =
585
    List.map
586 7ee5f69e Lélio Brun
      (fun decl ->
587
         let node = node_of_top decl in
588 75c459f4 Lélio Brun
         let sch = IMap.find node.node_id node_schs in
589 7ee5f69e Lélio Brun
         translate_decl node sch
590
      ) nodes
591 f4cba4b8 ploc
  in
592
  machines
593 22fe1c93 ploc
594 7ee5f69e Lélio Brun
(* Local Variables: *)
595
(* compile-command:"make -C .." *)
596
(* End: *)