Project

General

Profile

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