Project

General

Profile

Download (15.6 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
let build_env locals non_locals =
46
  let all = VSet.union locals non_locals in
47
  {
48
    is_local = (fun id -> VSet.exists (fun v -> v.var_id = id) locals);
49 7ee5f69e Lélio Brun
    get_var = (fun id -> try VSet.get id all with Not_found ->
50
        (* Format.eprintf "Impossible to find variable %s in set %a@.@?"
51
         *   id
52
         *   VSet.pp all; *)
53
        raise Not_found)
54 5de4dde4 ploc
  }
55
56 7ee5f69e Lélio Brun
57 5de4dde4 ploc
58
(****************************************************************)
59
(* Basic functions to translate to machine values, instructions *) 
60
(****************************************************************)
61
62
let translate_ident env id =
63 380a8d33 ploc
  (* Format.eprintf "trnaslating ident: %s@." id; *)
64 75c459f4 Lélio Brun
  (* id is a var that shall be visible here , ie. in vars *)
65
  try
66 5de4dde4 ploc
    let var_id = env.get_var id in
67 c35de73b ploc
    mk_val (Var var_id) var_id.var_type
68 ef34b4ae xthirioux
  with Not_found ->
69 75c459f4 Lélio Brun
70
 (* id is a constant *)
71
  try
72 7ee5f69e Lélio Brun
    let vdecl = (Corelang.var_decl_of_const
73
                   (const_of_top (Hashtbl.find Corelang.consts_table id)))
74
    in
75
    mk_val (Var vdecl) vdecl.var_type
76
  with Not_found ->
77 75c459f4 Lélio Brun
78
   (* id is a tag, getting its type in the list of declared enums *)
79 7ee5f69e Lélio Brun
  try
80
    let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
81
    mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
82
  with Not_found ->
83
    Format.eprintf "internal error: Machine_code.translate_ident %s@.@?" id;
84
    assert false
85 22fe1c93 ploc
86
87 5de4dde4 ploc
(* specialize predefined (polymorphic) operators wrt their instances,
88
   so that the C semantics is preserved *)
89 25b4311f xthirioux
let specialize_to_c expr =
90 7ee5f69e Lélio Brun
  match expr.expr_desc with
91
  | Expr_appl (id, e, r) ->
92
    if List.exists (fun e -> Types.is_bool_type e.expr_type) (expr_list_of_expr e)
93
    then let id =
94
           match id with
95
           | "="  -> "equi"
96
           | "!=" -> "xor"
97
           | _    -> id in
98
      { expr with expr_desc = Expr_appl (id, e, r) }
99
    else expr
100
  | _ -> expr
101 25b4311f xthirioux
102
let specialize_op expr =
103
  match !Options.output with
104
  | "C" -> specialize_to_c expr
105
  | _   -> expr
106
107 5de4dde4 ploc
let rec translate_expr env expr =
108 f2b1c245 ploc
  let expr = specialize_op expr in
109 5de4dde4 ploc
  let translate_expr = translate_expr env in
110 04a63d25 xthirioux
  let value_desc = 
111
    match expr.expr_desc with
112 7ee5f69e Lélio Brun
    | Expr_const v ->
113
      Cst v
114
    | Expr_ident x ->
115
      (translate_ident env x).value_desc
116
    | Expr_array el ->
117
      Array (List.map translate_expr el)
118
    | Expr_access (t, i) ->
119
      Access (translate_expr t, translate_expr (expr_of_dimension i))
120
    | Expr_power  (e, n) ->
121
      Power (translate_expr e, translate_expr (expr_of_dimension n))
122
    | Expr_when (e1, _, _) ->
123
      (translate_expr e1).value_desc
124 04a63d25 xthirioux
    | Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr ->
125 7ee5f69e Lélio Brun
      let nd = node_from_name id in
126
      Fun (node_name nd, List.map translate_expr (expr_list_of_expr e))
127
    | Expr_ite (g,t,e) when Backends.is_functional () ->
128 5de4dde4 ploc
      (* special treatment depending on the active backend. For
129
         functional ones, like horn backend, ite are preserved in
130
         expression. While they are removed for C or Java backends. *)
131 7ee5f69e Lélio Brun
      Fun ("ite", [translate_expr g; translate_expr t; translate_expr e])
132
    | _ ->
133
      Format.eprintf "Normalization error for backend %s: %a@."
134
        !Options.output
135
        Printers.pp_expr expr;
136
      raise NormalizationError
137 04a63d25 xthirioux
  in
138
  mk_val value_desc expr.expr_type
139 22fe1c93 ploc
140 5de4dde4 ploc
let translate_guard env expr =
141 0777a7be ploc
  match expr.expr_desc with
142 7ee5f69e Lélio Brun
  | Expr_ident x -> translate_ident env x
143
  | _ ->
144
    Format.eprintf "internal error: translate_guard %a@." Printers.pp_expr expr;
145
    assert false
146 22fe1c93 ploc
147 5de4dde4 ploc
let rec translate_act env (y, expr) =
148
  let translate_act = translate_act env in
149
  let translate_guard = translate_guard env in
150
  let translate_ident = translate_ident env in
151
  let translate_expr = translate_expr env in
152 7ee5f69e Lélio Brun
  let lustre_eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in
153 0777a7be ploc
  match expr.expr_desc with
154 7ee5f69e Lélio Brun
  | Expr_ite (c, t, e) ->
155
    mk_conditional ~lustre_eq
156
      (translate_guard c)
157
      [translate_act (y, t)]
158
      [translate_act (y, e)]
159
  | Expr_merge (x, hl) ->
160 75c459f4 Lélio Brun
    mk_branch ~lustre_eq
161
      (translate_ident x)
162
      (List.map (fun (t, h) -> t, [translate_act (y, h)]) hl)
163
  | _ ->
164
    mk_assign ~lustre_eq y (translate_expr expr)
165 5de4dde4 ploc
166
(* Datastructure updated while visiting equations *)
167
type machine_ctx = {
168 75c459f4 Lélio Brun
  (* Memories *)
169
  m: VSet.t;
170
  (* Reset instructions *)
171 7ee5f69e Lélio Brun
  si: instr_t list;
172 75c459f4 Lélio Brun
  (* Instances *)
173
  j: (Lustre_types.top_decl * Dimension.dim_expr list) IMap.t;
174
  (* Step instructions *)
175 7ee5f69e Lélio Brun
  s: instr_t list;
176 75c459f4 Lélio Brun
  (* Memory pack spec *)
177
  mp: mc_formula_t list;
178
  (* Clocked spec *)
179
  c: mc_formula_t IMap.t;
180
  (* Transition spec *)
181
  t: mc_formula_t list;
182 7ee5f69e Lélio Brun
}
183 5de4dde4 ploc
184 75c459f4 Lélio Brun
let ctx_init = {
185
  m = VSet.empty;
186
  si = [];
187
  j = IMap.empty;
188
  s = [];
189
  mp = [];
190
  c = IMap.empty;
191
  t = []
192
}
193 7ee5f69e Lélio Brun
194 5de4dde4 ploc
(****************************************************************)
195
(* Main function to translate equations into this machine context we
196
   are building *) 
197
(****************************************************************)
198
199 75c459f4 Lélio Brun
let mk_control id vs v l inst =
200
  mkinstr
201
    (Imply (mk_clocked_on id vs, inst.instr_spec))
202
    (MBranch (v, [l, [inst]]))
203
204
let control_on_clock env ctx ck inst =
205
  let rec aux (ck_ids, vs, ctx, inst as acc) ck =
206
    match (Clocks.repr ck).cdesc with
207
    | Con (ck, cr, l) ->
208
      let id = Clocks.const_of_carrier cr in
209
      let v = translate_ident env id in
210
      let ck_ids' = String.concat "_" ck_ids in
211
      let id' = id ^ "_" ^ ck_ids' in
212
      let ck_spec = mk_condition v l in
213
      aux (id :: ck_ids,
214
           v :: vs,
215
           { ctx
216
             with c = IMap.add id ck_spec
217
                      (IMap.add id'
218
                         (And [ck_spec; mk_clocked_on ck_ids' vs]) ctx.c)
219
           },
220
           mk_control id' (v :: vs) v l inst) ck
221
    | _ -> acc
222
  in
223
  let _, _, ctx, inst = aux ([], [], ctx, inst) ck in
224
  ctx, inst
225
226
let reset_instance env i r c =
227
  match r with
228
  | Some r ->
229
    [snd (control_on_clock env ctx_init c
230
            (mk_conditional
231
               (translate_guard env r)
232
               [mkinstr True (MReset i)]
233
               [mkinstr True (MNoReset i)]))]
234
  | None -> []
235 7ee5f69e Lélio Brun
236 5de4dde4 ploc
237
let translate_eq env ctx eq =
238
  let translate_expr = translate_expr env in
239
  let translate_act = translate_act env in
240 75c459f4 Lélio Brun
  let control_on_clock ck inst =
241
    let ctx, ins = control_on_clock env ctx ck inst in
242
    { ctx with s = ins :: ctx.s }
243
  in
244 5de4dde4 ploc
  let reset_instance = reset_instance env in
245 75c459f4 Lélio Brun
  let mkinstr' = mkinstr ~lustre_eq:eq True in
246 7ee5f69e Lélio Brun
  let ctl ?(ck=eq.eq_rhs.expr_clock) instr =
247
    control_on_clock ck (mkinstr' instr) in
248 22fe1c93 ploc
249 59020713 ploc
  (* Format.eprintf "translate_eq %a with clock %a@." 
250
     Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;  *)
251 22fe1c93 ploc
  match eq.eq_lhs, eq.eq_rhs.expr_desc with
252
  | [x], Expr_arrow (e1, e2)                     ->
253 7ee5f69e Lélio Brun
    let var_x = env.get_var x in
254
    let o = new_instance (Arrow.arrow_top_decl ()) eq.eq_rhs.expr_tag in
255
    let c1 = translate_expr e1 in
256
    let c2 = translate_expr e2 in
257 75c459f4 Lélio Brun
    let ctx = ctl (MStep ([var_x], o, [c1;c2])) in
258 7ee5f69e Lélio Brun
    { ctx with
259 75c459f4 Lélio Brun
      si = mkinstr True (MReset o) :: ctx.si;
260
      j = IMap.add o (Arrow.arrow_top_decl (), []) ctx.j;
261 7ee5f69e Lélio Brun
    }
262 5de4dde4 ploc
  | [x], Expr_pre e1 when env.is_local x    ->
263 7ee5f69e Lélio Brun
    let var_x = env.get_var x in
264 75c459f4 Lélio Brun
    let ctx = ctl (MStateAssign (var_x, translate_expr e1)) in
265 7ee5f69e Lélio Brun
    { ctx with
266
      m = VSet.add var_x ctx.m;
267
    }
268 5de4dde4 ploc
  | [x], Expr_fby (e1, e2) when env.is_local x ->
269 7ee5f69e Lélio Brun
    let var_x = env.get_var x in
270 75c459f4 Lélio Brun
    let ctx = ctl (MStateAssign (var_x, translate_expr e2)) in
271 7ee5f69e Lélio Brun
    { ctx with
272
      m = VSet.add var_x ctx.m;
273
      si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si;
274
    }
275
  | p, Expr_appl (f, arg, r)
276
    when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
277
    let var_p = List.map (fun v -> env.get_var v) p in
278
    let el = expr_list_of_expr arg in
279
    let vl = List.map translate_expr el in
280
    let node_f = node_from_name f in
281
    let call_f = node_f, NodeDep.filter_static_inputs (node_inputs node_f) el in
282
    let o = new_instance node_f eq.eq_rhs.expr_tag in
283
    let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks)
284
        el [eq.eq_rhs.expr_clock] in
285
    let call_ck = Clock_calculus.compute_root_clock
286
        (Clock_predef.ck_tuple env_cks) in
287 75c459f4 Lélio Brun
    let ctx = ctl ~ck:call_ck (MStep (var_p, o, vl)) in
288 7ee5f69e Lélio Brun
    (*Clocks.new_var true in
289
      Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
290
      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;*)
291
    { ctx with
292
      si = if Stateless.check_node node_f
293 75c459f4 Lélio Brun
        then ctx.si else mkinstr True (MReset o) :: ctx.si;
294
      j = IMap.add o call_f ctx.j;
295 5de4dde4 ploc
      s = (if Stateless.check_node node_f
296 75c459f4 Lélio Brun
           then []
297
           else reset_instance o r call_ck)
298
          @ ctx.s
299 7ee5f69e Lélio Brun
    }
300
  | [x], _ ->
301 5de4dde4 ploc
    let var_x = env.get_var x in
302 75c459f4 Lélio Brun
    control_on_clock eq.eq_rhs.expr_clock (translate_act (var_x, eq.eq_rhs))
303 7ee5f69e Lélio Brun
  | _ ->
304
    Format.eprintf "internal error: Machine_code.translate_eq %a@?"
305
      Printers.pp_node_eq eq;
306
    assert false
307 a38c681e xthirioux
308 5de4dde4 ploc
let constant_equations locals =
309 7ee5f69e Lélio Brun
  VSet.fold (fun vdecl eqs ->
310
      if vdecl.var_dec_const
311
      then
312
        { eq_lhs = [vdecl.var_id];
313 75c459f4 Lélio Brun
          eq_rhs = desome vdecl.var_dec_value;
314 7ee5f69e Lélio Brun
          eq_loc = vdecl.var_loc
315
        } :: eqs
316
      else eqs)
317
    locals []
318 ec433d69 xthirioux
319 5de4dde4 ploc
let translate_eqs env ctx eqs =
320 7ee5f69e Lélio Brun
  List.fold_right (fun eq ctx -> translate_eq env ctx eq) eqs ctx
321 5de4dde4 ploc
322
323
(****************************************************************)
324
(* Processing nodes *) 
325
(****************************************************************)
326 22fe1c93 ploc
327 59020713 ploc
let process_asserts nd =
328 7ee5f69e Lélio Brun
329
  let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
330
  if Backends.is_functional () then
331
    [], [], exprl
332
  else (* Each assert(e) is associated to a fresh variable v and declared as
333
          v=e; assert (v); *)
334
    let _, vars, eql, assertl =
335
      List.fold_left (fun (i, vars, eqlist, assertlist) expr ->
336
          let loc = expr.expr_loc in
337
          let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in
338
          let assert_var =
339
            mkvar_decl
340
              loc
341
              ~orig:false (* fresh var *)
342
              (var_id,
343
               mktyp loc Tydec_bool,
344
               mkclock loc Ckdec_any,
345
               false, (* not a constant *)
346
               None, (* no default value *)
347
               Some nd.node_id
348
              )
349
          in
350
          assert_var.var_type <- Type_predef.type_bool (* Types.new_ty (Types.Tbool) *);
351
          let eq = mkeq loc ([var_id], expr) in
352 5de4dde4 ploc
          (i+1,
353
           assert_var::vars,
354
           eq::eqlist,
355
           {expr with expr_desc = Expr_ident var_id}::assertlist)
356 7ee5f69e Lélio Brun
        ) (1, [], [], []) exprl
357
    in
358
    vars, eql, assertl
359 5de4dde4 ploc
360
let translate_core sorted_eqs locals other_vars =
361
  let constant_eqs = constant_equations locals in
362 7ee5f69e Lélio Brun
363 5de4dde4 ploc
  let env = build_env locals other_vars  in
364 7ee5f69e Lélio Brun
365 5de4dde4 ploc
  (* Compute constants' instructions  *)
366
  let ctx0 = translate_eqs env ctx_init constant_eqs in
367
  assert (VSet.is_empty ctx0.m);
368
  assert (ctx0.si = []);
369 75c459f4 Lélio Brun
  assert (IMap.is_empty ctx0.j);
370 7ee5f69e Lélio Brun
371 5de4dde4 ploc
  (* Compute ctx for all eqs *)
372
  let ctx = translate_eqs env ctx_init sorted_eqs in
373 7ee5f69e Lélio Brun
374 5de4dde4 ploc
  ctx, ctx0.s
375 0d065e73 ploc
376 7ee5f69e Lélio Brun
377 5de4dde4 ploc
let translate_decl nd sch =
378 1fd3d002 ploc
  (* Format.eprintf "Translating node %s@." nd.node_id; *)
379 5de4dde4 ploc
  (* Extracting eqs, variables ..  *)
380
  let eqs, auts = get_node_eqs nd in
381
  assert (auts = []); (* Automata should be expanded by now *)
382 7ee5f69e Lélio Brun
383 59020713 ploc
  (* In case of non functional backend (eg. C), additional local variables have
384
     to be declared for each assert *)
385
  let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in
386 5de4dde4 ploc
387
  (* Build the env: variables visible in the current scope *)
388 59020713 ploc
  let locals_list = nd.node_locals @ new_locals in
389 5de4dde4 ploc
  let locals = VSet.of_list locals_list in
390
  let inout_vars = (VSet.of_list (nd.node_inputs @ nd.node_outputs)) in
391
  let env = build_env locals inout_vars  in 
392 1fd3d002 ploc
393
  (* Format.eprintf "Node content is %a@." Printers.pp_node nd; *)
394 7ee5f69e Lélio Brun
395 5de4dde4 ploc
  (* Computing main content *)
396 1fd3d002 ploc
  (* Format.eprintf "ok1@.@?"; *)
397 5de4dde4 ploc
  let schedule = sch.Scheduling_type.schedule in
398 1fd3d002 ploc
  (* Format.eprintf "ok2@.@?"; *)
399 25320f03 ploc
  let sorted_eqs, unused = Scheduling.sort_equations_from_schedule eqs schedule in
400 1fd3d002 ploc
  (* Format.eprintf "ok3@.locals=%a@.inout:%a@?"
401
   *   VSet.pp locals
402
   *   VSet.pp inout_vars
403
   * ; *)
404 7ee5f69e Lélio Brun
405 5de4dde4 ploc
  let ctx, ctx0_s = translate_core (assert_instrs@sorted_eqs) locals inout_vars in
406 7ee5f69e Lélio Brun
407 1fd3d002 ploc
  (* Format.eprintf "ok4@.@?"; *)
408 25320f03 ploc
409
  (* Removing computed memories from locals. We also removed unused variables. *)
410
  let updated_locals =
411
    let l = VSet.elements (VSet.diff locals ctx.m) in
412
    List.fold_left (fun res v -> if List.mem v.var_id unused then res else v::res) [] l
413
  in
414 75c459f4 Lélio Brun
  let mmap = IMap.bindings ctx.j in
415 22fe1c93 ploc
  {
416
    mname = nd;
417 5de4dde4 ploc
    mmemory = VSet.elements ctx.m;
418 22fe1c93 ploc
    mcalls = mmap;
419 e135421f xthirioux
    minstances = List.filter (fun (_, (n,_)) -> not (Stateless.check_node n)) mmap;
420 5de4dde4 ploc
    minit = ctx.si;
421
    mconst = ctx0_s;
422 22fe1c93 ploc
    mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs;
423
    mstep = {
424 7ee5f69e Lélio Brun
      step_inputs = nd.node_inputs;
425
      step_outputs = nd.node_outputs;
426
      step_locals = updated_locals;
427
      step_checks = List.map (fun d -> d.Dimension.dim_loc,
428
                                       translate_expr env
429
                                         (expr_of_dimension d))
430
          nd.node_checks;
431
      step_instrs = (
432
        (* special treatment depending on the active backend. For horn backend,
433
           common branches are not merged while they are in C or Java
434
           backends. *)
435
        if !Backends.join_guards then
436
          join_guards_list ctx.s
437
        else
438
          ctx.s
439
      );
440
      step_asserts = List.map (translate_expr env) nd_node_asserts;
441
    };
442 f4cba4b8 ploc
443
    (* Processing spec: there is no processing performed here. Contract
444 7ee5f69e Lélio Brun
       have been processed already. Either one of the other machine is a
445
       cocospec node, or the current one is a cocospec node. Contract do
446
       not contain any statement or import. *)
447
448
    mspec = { mnode_spec = nd.node_spec; mtransitions = [] };
449 22fe1c93 ploc
    mannot = nd.node_annot;
450 95fb046e ploc
    msch = Some sch;
451 22fe1c93 ploc
  }
452
453 ec433d69 xthirioux
(** takes the global declarations and the scheduling associated to each node *)
454 88486aaf ploc
let translate_prog decls node_schs =
455 e9b71779 tkahsai
  let nodes = get_nodes decls in
456 f4cba4b8 ploc
  let machines =
457
    List.map
458 7ee5f69e Lélio Brun
      (fun decl ->
459
         let node = node_of_top decl in
460 75c459f4 Lélio Brun
         let sch = IMap.find node.node_id node_schs in
461 7ee5f69e Lélio Brun
         translate_decl node sch
462
      ) nodes
463 f4cba4b8 ploc
  in
464
  machines
465 22fe1c93 ploc
466 7ee5f69e Lélio Brun
(* Local Variables: *)
467
(* compile-command:"make -C .." *)
468
(* End: *)