Project

General

Profile

Download (21.2 KB) Statistics
| Branch: | Tag: | Revision:
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 Lustre_types
13
open Machine_code_types
14
open Machine_code_common
15
open Spec_types
16
open Spec_common
17
open Corelang
18
open Clocks
19
open Causality
20
open Utils
21

    
22
exception NormalizationError
23

    
24
(* Questions:
25

    
26
   - 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

    
29
(* translate_<foo> : vars -> context -> <foo> -> machine code/expression *)
30
(* 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

    
36
(* 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

    
40
let build_env inputs locals outputs =
41
  let all = List.sort_uniq VDeclModule.compare (locals @ inputs @ outputs) in
42
  {
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
  }
52

    
53
(****************************************************************)
54
(* Basic functions to translate to machine values, instructions *)
55
(****************************************************************)
56

    
57
let translate_ident env id =
58
  (* Format.eprintf "trnaslating ident: %s@." id; *)
59
  (* id is a var that shall be visible here , ie. in vars *)
60
  try
61
    let var_id = env.get_var id in
62
    vdecl_to_val var_id
63
  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
let specialize_to_c expr =
81
  match expr.expr_desc with
82
  | Expr_appl (id, e, r) ->
83
    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
      { expr with expr_desc = Expr_appl (id, e, r) }
90
    else expr
91
  | _ ->
92
    expr
93

    
94
let specialize_op expr =
95
  match !Options.output with Options.OutC -> specialize_to_c expr | _ -> expr
96

    
97
let rec translate_expr env expr =
98
  let expr = specialize_op expr in
99
  let translate_expr = translate_expr env in
100
  let value_desc =
101
    match expr.expr_desc with
102
    | 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
    | Expr_power (e, n) ->
111
      Power (translate_expr e, translate_expr (expr_of_dimension n))
112
    | Expr_when (e1, _, _) ->
113
      (translate_expr e1).value_desc
114
    | Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr ->
115
      let nd = node_from_name id in
116
      Fun (node_name nd, List.map translate_expr (expr_list_of_expr e))
117
    | 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
    | _ ->
123
      Format.eprintf
124
        "Normalization error for backend %t: %a@."
125
        Options.pp_output
126
        Printers.pp_expr
127
        expr;
128
      raise NormalizationError
129
  in
130
  mk_val value_desc expr.expr_type
131

    
132
let translate_guard env expr =
133
  match expr.expr_desc with
134
  | Expr_ident x ->
135
    translate_ident env x
136
  | _ ->
137
    Format.eprintf "internal error: translate_guard %a@." Printers.pp_expr expr;
138
    assert false
139

    
140
let rec translate_act env (y, expr) =
141
  let translate_act = translate_act env in
142
  let translate_guard = translate_guard env in
143
  let translate_expr = translate_expr env in
144
  let lustre_eq = Corelang.mkeq Location.dummy ([ y.var_id ], expr) in
145
  match expr.expr_desc with
146
  | Expr_ite (c, t, e) ->
147
    let c = translate_guard c in
148
    let t, spec_t = translate_act (y, t) in
149
    let e, spec_e = translate_act (y, e) in
150
    mk_conditional ~lustre_eq c [ t ] [ e ], mk_conditional_tr c spec_t spec_e
151
  | Expr_merge (x, hl) ->
152
    let var_x = env.get_var x in
153
    let hl, spec_hl =
154
      List.(
155
        split
156
          (map
157
             (fun (t, h) ->
158
               let h, spec_h = translate_act (y, h) in
159
               (t, [ h ]), (t, spec_h))
160
             hl))
161
    in
162
    mk_branch' ~lustre_eq var_x hl, mk_branch_tr var_x spec_hl
163
  | _ ->
164
    let e = translate_expr expr in
165
    mk_assign ~lustre_eq y e, mk_assign_tr y e
166

    
167
let get_memory env mems eq =
168
  match eq.eq_lhs, eq.eq_rhs.expr_desc with
169
  | ([ x ], Expr_pre _ | [ x ], Expr_fby _) when env.is_local x ->
170
    let var_x = env.get_var x in
171
    VSet.add var_x mems
172
  | _ ->
173
    mems
174

    
175
let get_memories env = List.fold_left (get_memory env) VSet.empty
176

    
177
(* Datastructure updated while visiting equations *)
178
type machine_ctx = {
179
  (* memories *)
180
  m : ISet.t;
181
  (* Reset instructions *)
182
  si : instr_t list;
183
  (* Instances *)
184
  j : (Lustre_types.top_decl * Dimension.t list) IMap.t;
185
  (* Step instructions *)
186
  s : instr_t list;
187
  (* Memory pack spec *)
188
  mp : mc_formula_t list;
189
  (* Transition spec *)
190
  t :
191
    (var_decl list
192
    (* vars *)
193
    * ISet.t (* memory footprint *)
194
    * ident IMap.t
195
    (* memory instances footprint *)
196
    * mc_formula_t)
197
    (* formula *)
198
    list;
199
}
200

    
201
let ctx_init =
202
  { m = ISet.empty; si = []; j = IMap.empty; s = []; mp = []; t = [] }
203

    
204
(****************************************************************)
205
(* Main function to translate equations into this machine context we are
206
   building *)
207
(****************************************************************)
208

    
209
let mk_control v l inst = mkinstr (MBranch (vdecl_to_val v, [ l, [ inst ] ]))
210

    
211
let control_on_clock env ck inst =
212
  let rec aux ((fspec, inst) as acc) ck =
213
    match (Clocks.repr ck).cdesc with
214
    | Con (ck, cr, l) ->
215
      let id = Clocks.const_of_carrier cr in
216
      let v = env.get_var id in
217
      aux
218
        ( (fun spec -> Imply (Equal (Var v, Tag l), fspec spec)),
219
          mk_control v l inst )
220
        ck
221
    | _ ->
222
      acc
223
  in
224
  let fspec, inst = aux ((fun spec -> spec), inst) ck in
225
  fspec, inst
226

    
227
let reset_instance env i r c =
228
  match r with
229
  | Some r ->
230
    let r = translate_guard env r in
231
    let _, inst =
232
      control_on_clock
233
        env
234
        c
235
        (mk_conditional r [ mkinstr (MSetReset i) ] [ mkinstr (MNoReset i) ])
236
    in
237
    Some r, [ inst ]
238
  | None ->
239
    None, []
240

    
241
let translate_eq env ctx nd inputs locals outputs i eq =
242
  let id = nd.node_id in
243
  let translate_expr = translate_expr env in
244
  let translate_act = translate_act env in
245
  let locals_pi = Lustre_live.inter_live_i_with id (i - 1) locals in
246
  let outputs_pi = Lustre_live.inter_live_i_with id (i - 1) outputs in
247
  let locals_i = Lustre_live.inter_live_i_with id i locals in
248
  let outputs_i = Lustre_live.inter_live_i_with id i outputs in
249
  let pred_mp ctx a = And [ mk_memory_pack ~i:(i - 1) id; a ] :: ctx.mp in
250
  let pred_t ctx a =
251
    ( inputs @ locals_i @ outputs_i,
252
      ctx.m,
253
      IMap.map (fun (td, _) -> node_name td) ctx.j,
254
      Exists
255
        ( Lustre_live.existential_vars id i eq (locals @ outputs),
256
          And
257
            [
258
              mk_transition
259
                ~i:(i - 1)
260
                id
261
                (vdecls_to_vals (inputs @ locals_pi @ outputs_pi));
262
              a;
263
            ] ) )
264
    :: ctx.t
265
  in
266
  let control_on_clock ck inst spec_mp spec_t ctx =
267
    let fspec, inst = control_on_clock env ck inst in
268
    {
269
      ctx with
270
      s =
271
        {
272
          inst with
273
          instr_spec =
274
            (if fst (get_stateless_status_node nd) then []
275
            else [ mk_memory_pack ~i id ])
276
            @ [
277
                mk_transition
278
                  ~i
279
                  id
280
                  (vdecls_to_vals (inputs @ locals_i @ outputs_i));
281
              ];
282
        }
283
        :: ctx.s;
284
      mp = pred_mp ctx spec_mp;
285
      t = pred_t ctx (fspec spec_t);
286
    }
287
  in
288
  let reset_instance = reset_instance env in
289
  let mkinstr' = mkinstr ~lustre_eq:eq in
290
  let ctl ?(ck = eq.eq_rhs.expr_clock) instr =
291
    control_on_clock ck (mkinstr' instr)
292
  in
293

    
294
  (* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq
295
     Clocks.print_ck eq.eq_rhs.expr_clock; *)
296
  match eq.eq_lhs, eq.eq_rhs.expr_desc with
297
  | [ x ], Expr_arrow (e1, e2) ->
298
    let var_x = env.get_var x in
299
    let td = Arrow.arrow_top_decl () in
300
    let inst = new_instance td eq.eq_rhs.expr_tag in
301
    let c1 = translate_expr e1 in
302
    let c2 = translate_expr e2 in
303
    assert (c1.value_desc = Cst (Const_tag "true"));
304
    assert (c2.value_desc = Cst (Const_tag "false"));
305
    let ctx =
306
      ctl
307
        (MStep ([ var_x ], inst, [ c1; c2 ]))
308
        (mk_memory_pack ~inst (node_name td))
309
        (mk_transition ~inst (node_name td) [ vdecl_to_val var_x ])
310
        { ctx with j = IMap.add inst (td, []) ctx.j }
311
    in
312
    { ctx with si = mkinstr (MSetReset inst) :: ctx.si }
313
  | [ x ], Expr_pre e when env.is_local x ->
314
    let var_x = env.get_var x in
315
    let e = translate_expr e in
316
    ctl
317
      (MStateAssign (var_x, e))
318
      (mk_state_variable_pack var_x)
319
      (mk_state_assign_tr var_x e)
320
      { ctx with m = ISet.add x ctx.m }
321
  | [ x ], Expr_fby (e1, e2) when env.is_local x ->
322
    let var_x = env.get_var x in
323
    let e2 = translate_expr e2 in
324
    let ctx =
325
      ctl
326
        (MStateAssign (var_x, e2))
327
        (mk_state_variable_pack var_x)
328
        (mk_state_assign_tr var_x e2)
329
        { ctx with m = ISet.add x ctx.m }
330
    in
331
    {
332
      ctx with
333
      si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si;
334
    }
335
  | p, Expr_appl (f, arg, r)
336
    when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
337
    let var_p = List.map env.get_var p in
338
    let el = expr_list_of_expr arg in
339
    let vl = List.map translate_expr el in
340
    let node_f = node_from_name f in
341
    let call_f = node_f, NodeDep.filter_static_inputs (node_inputs node_f) el in
342
    let inst = new_instance node_f eq.eq_rhs.expr_tag in
343
    let env_cks =
344
      List.fold_right
345
        (fun arg cks -> arg.expr_clock :: cks)
346
        el
347
        [ eq.eq_rhs.expr_clock ]
348
    in
349
    let call_ck =
350
      Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks)
351
    in
352
    let r, reset_inst = reset_instance inst r call_ck in
353
    let ctx =
354
      ctl
355
        ~ck:call_ck
356
        (MStep (var_p, inst, vl))
357
        (mk_memory_pack ~inst (node_name node_f))
358
        (mk_transition ?r ~inst (node_name node_f) (vl @ vdecls_to_vals var_p))
359
        {
360
          ctx with
361
          j = IMap.add inst call_f ctx.j;
362
          s = (if Stateless.check_node node_f then [] else reset_inst) @ ctx.s;
363
        }
364
    in
365
    (*Clocks.new_var true in Clock_calculus.unify_imported_clock (Some call_ck)
366
      eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc; Format.eprintf "call %a: %a:
367
      %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple
368
      env_cks) Clocks.print_ck call_ck;*)
369
    {
370
      ctx with
371
      si =
372
        (if Stateless.check_node node_f then ctx.si
373
        else mkinstr (MSetReset inst) :: ctx.si);
374
    }
375
  | [ x ], _ ->
376
    begin try
377
    let var_x = env.get_var x in
378
    let instr, spec = translate_act (var_x, eq.eq_rhs) in
379
    control_on_clock eq.eq_rhs.expr_clock instr True spec ctx
380
      with Not_found ->
381
        Format.eprintf "ERROR: node %s, eq %a@." id Printers.pp_node_eq eq  ;
382
        raise Not_found
383
        end
384
  | _ ->
385
    Format.eprintf
386
      "internal error: Machine_code.translate_eq %a@?"
387
      Printers.pp_node_eq
388
      eq;
389
    assert false
390

    
391
let constant_equations locals =
392
  List.fold_left
393
    (fun eqs vdecl ->
394
      if vdecl.var_dec_const then
395
        {
396
          eq_lhs = [ vdecl.var_id ];
397
          eq_rhs = desome vdecl.var_dec_value;
398
          eq_loc = vdecl.var_loc;
399
        }
400
        :: eqs
401
      else eqs)
402
    []
403
    locals
404

    
405
let translate_eqs env ctx nd inputs locals outputs eqs =
406
  List.fold_left
407
    (fun (ctx, i) eq ->
408
      let ctx = translate_eq env ctx nd inputs locals outputs i eq in
409
      ctx, i + 1)
410
    (ctx, 1)
411
    eqs
412
  |> fst
413

    
414
(****************************************************************)
415
(* Processing nodes *)
416
(****************************************************************)
417

    
418
let process_asserts nd =
419
  let exprl = List.map (fun assert_ -> assert_.assert_expr) nd.node_asserts in
420
  if Backends.is_functional () then [], [], exprl
421
  else
422
    (* Each assert(e) is associated to a fresh variable v and declared as v=e;
423
       assert (v); *)
424
    let _, vars, eql, assertl =
425
      List.fold_left
426
        (fun (i, vars, eqlist, assertlist) expr ->
427
          let loc = expr.expr_loc in
428
          let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in
429
          let assert_var =
430
            mkvar_decl
431
              loc
432
              ~orig:false
433
              (* fresh var *)
434
              ( var_id,
435
                mktyp loc Tydec_bool,
436
                mkclock loc Ckdec_any,
437
                false,
438
                (* not a constant *)
439
                None,
440
                (* no default value *)
441
                Some nd.node_id )
442
          in
443
          assert_var.var_type <- Type_predef.type_bool
444
          (* Types.new_ty (Types.Tbool) *);
445
          let eq = mkeq loc ([ var_id ], expr) in
446
          ( i + 1,
447
            assert_var :: vars,
448
            eq :: eqlist,
449
            { expr with expr_desc = Expr_ident var_id } :: assertlist ))
450
        (1, [], [], [])
451
        exprl
452
    in
453
    vars, eql, assertl
454

    
455
let translate_core env nd sorted_eqs inputs locals outputs =
456
  let constant_eqs = constant_equations locals in
457

    
458
  (* Compute constants' instructions *)
459
  let ctx0 = translate_eqs env ctx_init nd inputs locals outputs constant_eqs in
460
  assert (ctx0.si = []);
461
  assert (IMap.is_empty ctx0.j);
462

    
463
  (* Compute ctx for all eqs *)
464
  let ctx = translate_eqs env ctx_init nd inputs locals outputs sorted_eqs in
465

    
466
  ctx, ctx0.s
467

    
468
let zero = mk_val (Cst (Const_int 0)) Type_predef.type_int
469

    
470
let memory_pack_0 nd =
471
  {
472
    mpname = nd;
473
    mpindex = Some 0;
474
    mpformula =
475
      And [ StateVarPack ResetFlag; Equal (Memory ResetFlag, Val zero) ];
476
  }
477

    
478
let memory_pack_toplevel nd i =
479
  {
480
    mpname = nd;
481
    mpindex = None;
482
    mpformula =
483
      Ternary
484
        (Memory ResetFlag, StateVarPack ResetFlag, mk_memory_pack ~i nd.node_id);
485
  }
486

    
487
let transition_0 nd =
488
  {
489
    tname = nd;
490
    tindex = Some 0;
491
    tvars = nd.node_inputs;
492
    tformula = if fst (get_stateless_status_node nd) then True else StateVarPack ResetFlag;
493
    tmem_footprint = ISet.empty;
494
    tinst_footprint = IMap.empty;
495
  }
496

    
497
let transition_toplevel nd i =
498
  let tr =
499
    mk_transition
500
      nd.node_id
501
      ~i
502
      (vdecls_to_vals (nd.node_inputs @ nd.node_outputs))
503
  in
504
  {
505
    tname = nd;
506
    tindex = None;
507
    tvars = nd.node_inputs @ nd.node_outputs;
508
    tformula =
509
      (if fst (get_stateless_status_node nd) then tr
510
      else ExistsMem (nd.node_id, Predicate (ResetCleared nd.node_id), tr));
511
    tmem_footprint = ISet.empty;
512
    tinst_footprint = IMap.empty;
513
  }
514

    
515
let translate_eexpr env e =
516
  try
517
  List.fold_right (fun (qt, xs) f -> match qt with
518
      | Lustre_types.Exists -> Exists (xs, f)
519
      | Lustre_types.Forall -> Forall (xs, f))
520
    e.eexpr_quantifiers
521
    (Value (translate_expr env e.eexpr_qfexpr))
522
  with
523
  NormalizationError ->
524
  Format.eprintf
525
    "Normalization error: %a@."
526
    Printers.pp_eexpr
527
    e;
528
  raise NormalizationError
529

    
530

    
531
let translate_contract env c = {
532
  mc_pre = And (List.map (translate_eexpr env) c.Lustre_types.assume);
533
  mc_post = And (List.map (translate_eexpr env) c.Lustre_types.guarantees);
534
  mc_proof = c.proof
535
}
536

    
537
let translate_spec env = function
538
  | Contract c ->
539
    Contract (translate_contract env c)
540
  | NodeSpec s ->
541
    NodeSpec s
542

    
543
let translate_decl nd sch =
544
  (* Format.eprintf "Translating node %s@." nd.node_id; *)
545
  (* Extracting eqs, variables ..  *)
546
  let eqs, auts = get_node_eqs nd in
547
  assert (auts = []);
548

    
549
  (* Automata should be expanded by now *)
550

    
551
  (* In case of non functional backend (eg. C), additional local variables have
552
     to be declared for each assert *)
553
  let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in
554

    
555
  (* Build the env: variables visible in the current scope *)
556
  let locals = nd.node_locals @ new_locals in
557
  (* let locals = VSet.of_list locals_list in *)
558
  (* let inout_vars = nd.node_inputs @ nd.node_outputs in *)
559
  let env = build_env nd.node_inputs locals nd.node_outputs in
560

    
561
  (* Format.eprintf "Node content is %a@." Printers.pp_node nd; *)
562

    
563
  (* Computing main content *)
564
  (* Format.eprintf "ok1@.@?"; *)
565
  let schedule = sch.Scheduling_type.schedule in
566
  (* Format.eprintf "ok2@.@?"; *)
567
  let sorted_eqs, unused =
568
    Scheduling.sort_equations_from_schedule eqs schedule
569
  in
570

    
571
  (* Format.eprintf "ok3@.locals=%a@.inout:%a@?"
572
   *   VSet.pp locals
573
   *   VSet.pp inout_vars
574
   * ; *)
575
  let equations = assert_instrs @ sorted_eqs in
576
  let mems = get_memories env equations in
577
  (* Removing computed memories from locals. We also removed unused variables. *)
578
  let locals =
579
    List.filter
580
      (fun v -> (not (VSet.mem v mems)) && not (List.mem v.var_id unused))
581
      locals
582
  in
583
  (* Compute live sets for spec *)
584
  Lustre_live.set_live_of nd.node_id nd.node_outputs locals equations;
585

    
586
  (* Translate equations *)
587
  let ctx, ctx0_s =
588
    translate_core env nd equations nd.node_inputs locals nd.node_outputs
589
  in
590

    
591
  (* Format.eprintf "ok4@.@?"; *)
592

    
593
  (* Build the machine *)
594
  let mmap = IMap.bindings ctx.j in
595
  let mmemory_packs =
596
    memory_pack_0 nd
597
    ::
598
    List.mapi
599
      (fun i f -> { mpname = nd; mpindex = Some (i + 1); mpformula = red f })
600
      (List.rev ctx.mp)
601
    @ [ memory_pack_toplevel nd (List.length ctx.mp) ]
602
  in
603
  let mtransitions =
604
    transition_0 nd
605
    ::
606
    List.mapi
607
      (fun i (tvars, tmem_footprint, tinst_footprint, f) ->
608
        {
609
          tname = nd;
610
          tindex = Some (i + 1);
611
          tvars;
612
          tformula = red f;
613
          tmem_footprint;
614
          tinst_footprint;
615
        })
616
      (List.rev ctx.t)
617
    @ [ transition_toplevel nd (List.length ctx.t) ]
618
  in
619
  let clear_reset =
620
    mkinstr
621
      ~instr_spec:
622
        ((if fst (get_stateless_status_node nd) then []
623
         else [ mk_memory_pack ~i:0 nd.node_id ])
624
        @ [ mk_transition ~i:0 nd.node_id (vdecls_to_vals nd.node_inputs) ])
625
      MClearReset
626
  in
627
  let mnode_spec = Utils.option_map (translate_spec env) nd.node_spec in
628
  {
629
    mname = nd;
630
    mmemory = VSet.elements mems;
631
    mcalls = mmap;
632
    minstances =
633
      List.filter (fun (_, (n, _)) -> not (Stateless.check_node n)) mmap;
634
    minit = List.rev ctx.si;
635
    mconst = List.rev ctx0_s;
636
    mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs;
637
    mstep =
638
      {
639
        step_inputs = nd.node_inputs;
640
        step_outputs = nd.node_outputs;
641
        step_locals = locals;
642
        step_checks =
643
          List.map
644
            (fun d ->
645
              d.Dimension.dim_loc, translate_expr env (expr_of_dimension d))
646
            nd.node_checks;
647
        step_instrs =
648
          clear_reset
649
          ::
650
          (* special treatment depending on the active backend. For horn
651
             backend, common branches are not merged while they are in C or Java
652
             backends. *)
653
          (if !Backends.join_guards then join_guards_list (List.rev ctx.s)
654
          else List.rev ctx.s);
655
        step_asserts = List.map (translate_expr env) nd_node_asserts;
656
      };
657
    (* Processing spec: there is no processing performed here. Contract have
658
       been processed already. Either one of the other machine is a cocospec
659
       node, or the current one is a cocospec node. Contract do not contain any
660
       statement or import. *)
661
    mspec = { mnode_spec; mtransitions; mmemory_packs };
662
    mannot = nd.node_annot;
663
    msch = Some sch;
664
    mis_contract = nd.node_iscontract
665
  }
666

    
667
(** takes the global declarations and the scheduling associated to each node *)
668
let translate_prog decls node_schs =
669
  let nodes = get_nodes decls in
670
  let machines =
671
    List.map
672
      (fun decl ->
673
        let node = node_of_top decl in
674
        let sch = IMap.find node.node_id node_schs in
675
        translate_decl node sch)
676
      nodes
677
  in
678
  machines
679

    
680
(* Local Variables: *)
681
(* compile-command:"make -C .." *)
682
(* End: *)
(46-46/99)