Project

General

Profile

Download (14.8 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 Corelang
16
open Clocks
17
open Causality
18

    
19
exception NormalizationError
20

    
21
(* Questions:
22

    
23
   - where are used the mconst. They contain initialization of
24
     constant in nodes. But they do not seem to be used by c_backend *)
25

    
26

    
27
(* translate_<foo> : vars -> context -> <foo> -> machine code/expression *)
28
(* the context contains  m : state aka memory variables  *)
29
(*                      si : initialization instructions *)
30
(*                       j : node aka machine instances  *)
31
(*                       d : local variables             *)
32
(*                       s : step instructions           *)
33

    
34
(* Machine processing requires knowledge about variables and local
35
   variables. Local could be memories while other could not.  *)
36
type machine_env = {
37
  is_local: string -> bool;
38
  get_var: string -> var_decl
39
}
40

    
41

    
42
let build_env locals non_locals =
43
  let all = VSet.union locals non_locals in
44
  {
45
    is_local = (fun id -> VSet.exists (fun v -> v.var_id = id) locals);
46
    get_var = (fun id -> try VSet.get id all with Not_found ->
47
        (* Format.eprintf "Impossible to find variable %s in set %a@.@?"
48
         *   id
49
         *   VSet.pp all; *)
50
        raise Not_found)
51
  }
52

    
53

    
54

    
55
(****************************************************************)
56
(* Basic functions to translate to machine values, instructions *) 
57
(****************************************************************)
58

    
59
let translate_ident env id =
60
  (* Format.eprintf "trnaslating ident: %s@." id; *)
61
  try (* id is a var that shall be visible here , ie. in vars *)
62
    let var_id = env.get_var id in
63
    mk_val (Var var_id) var_id.var_type
64
  with Not_found ->
65
  try (* id is a constant *)
66
    let vdecl = (Corelang.var_decl_of_const
67
                   (const_of_top (Hashtbl.find Corelang.consts_table id)))
68
    in
69
    mk_val (Var vdecl) vdecl.var_type
70
  with Not_found ->
71
  (* id is a tag, getting its type in the list of declared enums *)
72
  try
73
    let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
74
    mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
75
  with Not_found ->
76
    Format.eprintf "internal error: Machine_code.translate_ident %s@.@?" id;
77
    assert false
78

    
79
let rec control_on_clock env ck inst =
80
  match (Clocks.repr ck).cdesc with
81
  | Con (ck1, cr, l) ->
82
    let id = Clocks.const_of_carrier cr in
83
    control_on_clock env ck1
84
      (mkinstr (MBranch (translate_ident env id, [l, [inst]])))
85
  | _ -> inst
86

    
87

    
88
(* specialize predefined (polymorphic) operators wrt their instances,
89
   so that the C semantics is preserved *)
90
let specialize_to_c expr =
91
  match expr.expr_desc with
92
  | Expr_appl (id, e, r) ->
93
    if List.exists (fun e -> Types.is_bool_type e.expr_type) (expr_list_of_expr e)
94
    then let id =
95
           match id with
96
           | "="  -> "equi"
97
           | "!=" -> "xor"
98
           | _    -> id in
99
      { expr with expr_desc = Expr_appl (id, e, r) }
100
    else expr
101
  | _ -> expr
102

    
103
let specialize_op expr =
104
  match !Options.output with
105
  | "C" -> specialize_to_c expr
106
  | _   -> expr
107

    
108
let rec translate_expr env expr =
109
  let expr = specialize_op expr in
110
  let translate_expr = translate_expr env in
111
  let value_desc = 
112
    match expr.expr_desc with
113
    | Expr_const v ->
114
      Cst v
115
    | Expr_ident x ->
116
      (translate_ident env x).value_desc
117
    | Expr_array el ->
118
      Array (List.map translate_expr el)
119
    | Expr_access (t, i) ->
120
      Access (translate_expr t, translate_expr (expr_of_dimension i))
121
    | Expr_power  (e, n) ->
122
      Power (translate_expr e, translate_expr (expr_of_dimension n))
123
    | Expr_when (e1, _, _) ->
124
      (translate_expr e1).value_desc
125
    | Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr ->
126
      let nd = node_from_name id in
127
      Fun (node_name nd, List.map translate_expr (expr_list_of_expr e))
128
    | Expr_ite (g,t,e) when Backends.is_functional () ->
129
      (* special treatment depending on the active backend. For
130
         functional ones, like horn backend, ite are preserved in
131
         expression. While they are removed for C or Java backends. *)
132
      Fun ("ite", [translate_expr g; translate_expr t; translate_expr e])
133
    | _ ->
134
      Format.eprintf "Normalization error for backend %s: %a@."
135
        !Options.output
136
        Printers.pp_expr expr;
137
      raise NormalizationError
138
  in
139
  mk_val value_desc expr.expr_type
140

    
141
let translate_guard env expr =
142
  match expr.expr_desc with
143
  | Expr_ident x -> translate_ident env x
144
  | _ ->
145
    Format.eprintf "internal error: translate_guard %a@." Printers.pp_expr expr;
146
    assert false
147

    
148
let rec translate_act env (y, expr) =
149
  let translate_act = translate_act env in
150
  let translate_guard = translate_guard env in
151
  let translate_ident = translate_ident env in
152
  let translate_expr = translate_expr env in
153
  let lustre_eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in
154
  match expr.expr_desc with
155
  | Expr_ite (c, t, e) ->
156
    mk_conditional ~lustre_eq
157
      (translate_guard c)
158
      [translate_act (y, t)]
159
      [translate_act (y, e)]
160
  | Expr_merge (x, hl) ->
161
    mkinstr ~lustre_eq
162
      (MBranch (translate_ident x,
163
                List.map (fun (t,  h) -> t, [translate_act (y, h)]) hl))
164
  | _ -> mkinstr ~lustre_eq (MLocalAssign (y, translate_expr expr))
165

    
166
let reset_instance env i r c =
167
  match r with
168
  | Some r ->
169
    [control_on_clock env c
170
       (mk_conditional
171
          (translate_guard env r)
172
          [mkinstr (MReset i)]
173
          [mkinstr (MNoReset i)])]
174
  | None -> []
175

    
176

    
177
(* Datastructure updated while visiting equations *)
178
type machine_ctx = {
179
  m: VSet.t; (* Memories *)
180
  si: instr_t list;
181
  j: (Lustre_types.top_decl * Dimension.dim_expr list) Utils.IMap.t;
182
  s: instr_t list;
183
}
184

    
185
let ctx_init = { m = VSet.empty; (* memories *)
186
                 si = []; (* init instr *)
187
                 j = Utils.IMap.empty;
188
                 s = [] }
189

    
190
(****************************************************************)
191
(* Main function to translate equations into this machine context we
192
   are building *) 
193
(****************************************************************)
194

    
195

    
196

    
197
let translate_eq env ctx eq =
198
  let translate_expr = translate_expr env in
199
  let translate_act = translate_act env in
200
  let control_on_clock = control_on_clock env in
201
  let reset_instance = reset_instance env in
202
  let mkinstr' = mkinstr ~lustre_eq:eq in
203
  let ctl ?(ck=eq.eq_rhs.expr_clock) instr =
204
    control_on_clock ck (mkinstr' instr) in
205

    
206
  (* Format.eprintf "translate_eq %a with clock %a@." 
207
     Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;  *)
208
  match eq.eq_lhs, eq.eq_rhs.expr_desc with
209
  | [x], Expr_arrow (e1, e2)                     ->
210
    let var_x = env.get_var x in
211
    let o = new_instance (Arrow.arrow_top_decl ()) eq.eq_rhs.expr_tag in
212
    let c1 = translate_expr e1 in
213
    let c2 = translate_expr e2 in
214
    { ctx with
215
      si = mkinstr (MReset o) :: ctx.si;
216
      j = Utils.IMap.add o (Arrow.arrow_top_decl (), []) ctx.j;
217
      s = ctl (MStep ([var_x], o, [c1;c2])) :: ctx.s
218
    }
219
  | [x], Expr_pre e1 when env.is_local x    ->
220
    let var_x = env.get_var x in
221
    { ctx with
222
      m = VSet.add var_x ctx.m;
223
      s = ctl (MStateAssign (var_x, translate_expr e1)) :: ctx.s
224
    }
225
  | [x], Expr_fby (e1, e2) when env.is_local x ->
226
    let var_x = env.get_var x in
227
    { ctx with
228
      m = VSet.add var_x ctx.m;
229
      si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si;
230
      s = ctl (MStateAssign (var_x, translate_expr e2)) :: ctx.s
231
    }
232
  | p, Expr_appl (f, arg, r)
233
    when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
234
    let var_p = List.map (fun v -> env.get_var v) p in
235
    let el = expr_list_of_expr arg in
236
    let vl = List.map translate_expr el in
237
    let node_f = node_from_name f in
238
    let call_f = node_f, NodeDep.filter_static_inputs (node_inputs node_f) el in
239
    let o = new_instance node_f eq.eq_rhs.expr_tag in
240
    let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks)
241
        el [eq.eq_rhs.expr_clock] in
242
    let call_ck = Clock_calculus.compute_root_clock
243
        (Clock_predef.ck_tuple env_cks) in
244
    (*Clocks.new_var true in
245
      Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
246
      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;*)
247
    { ctx with
248
      si = if Stateless.check_node node_f
249
        then ctx.si else mkinstr (MReset o) :: ctx.si;
250
      j = Utils.IMap.add o call_f ctx.j;
251
      s = (if Stateless.check_node node_f
252
           then [] else reset_instance o r call_ck)
253
          @ ctl ~ck:call_ck (MStep (var_p, o, vl))
254
          :: ctx.s
255
    }
256
  | [x], _ ->
257
    let var_x = env.get_var x in
258
    { ctx with
259
      s = control_on_clock eq.eq_rhs.expr_clock
260
          (translate_act (var_x, eq.eq_rhs))
261
          :: ctx.s
262
      }
263
  | _ ->
264
    Format.eprintf "internal error: Machine_code.translate_eq %a@?"
265
      Printers.pp_node_eq eq;
266
    assert false
267

    
268
let constant_equations locals =
269
  VSet.fold (fun vdecl eqs ->
270
      if vdecl.var_dec_const
271
      then
272
        { eq_lhs = [vdecl.var_id];
273
          eq_rhs = Utils.desome vdecl.var_dec_value;
274
          eq_loc = vdecl.var_loc
275
        } :: eqs
276
      else eqs)
277
    locals []
278

    
279
let translate_eqs env ctx eqs =
280
  List.fold_right (fun eq ctx -> translate_eq env ctx eq) eqs ctx
281

    
282

    
283
(****************************************************************)
284
(* Processing nodes *) 
285
(****************************************************************)
286

    
287
let process_asserts nd =
288

    
289
  let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
290
  if Backends.is_functional () then
291
    [], [], exprl
292
  else (* Each assert(e) is associated to a fresh variable v and declared as
293
          v=e; assert (v); *)
294
    let _, vars, eql, assertl =
295
      List.fold_left (fun (i, vars, eqlist, assertlist) expr ->
296
          let loc = expr.expr_loc in
297
          let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in
298
          let assert_var =
299
            mkvar_decl
300
              loc
301
              ~orig:false (* fresh var *)
302
              (var_id,
303
               mktyp loc Tydec_bool,
304
               mkclock loc Ckdec_any,
305
               false, (* not a constant *)
306
               None, (* no default value *)
307
               Some nd.node_id
308
              )
309
          in
310
          assert_var.var_type <- Type_predef.type_bool (* Types.new_ty (Types.Tbool) *);
311
          let eq = mkeq loc ([var_id], expr) in
312
          (i+1,
313
           assert_var::vars,
314
           eq::eqlist,
315
           {expr with expr_desc = Expr_ident var_id}::assertlist)
316
        ) (1, [], [], []) exprl
317
    in
318
    vars, eql, assertl
319

    
320
let translate_core sorted_eqs locals other_vars =
321
  let constant_eqs = constant_equations locals in
322

    
323
  let env = build_env locals other_vars  in
324

    
325
  (* Compute constants' instructions  *)
326
  let ctx0 = translate_eqs env ctx_init constant_eqs in
327
  assert (VSet.is_empty ctx0.m);
328
  assert (ctx0.si = []);
329
  assert (Utils.IMap.is_empty ctx0.j);
330

    
331
  (* Compute ctx for all eqs *)
332
  let ctx = translate_eqs env ctx_init sorted_eqs in
333

    
334
  ctx, ctx0.s
335

    
336

    
337
let translate_decl nd sch =
338
  (* Format.eprintf "Translating node %s@." nd.node_id; *)
339
  (* Extracting eqs, variables ..  *)
340
  let eqs, auts = get_node_eqs nd in
341
  assert (auts = []); (* Automata should be expanded by now *)
342

    
343
  (* In case of non functional backend (eg. C), additional local variables have
344
     to be declared for each assert *)
345
  let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in
346

    
347
  (* Build the env: variables visible in the current scope *)
348
  let locals_list = nd.node_locals @ new_locals in
349
  let locals = VSet.of_list locals_list in
350
  let inout_vars = (VSet.of_list (nd.node_inputs @ nd.node_outputs)) in
351
  let env = build_env locals inout_vars  in 
352

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

    
355
  (* Computing main content *)
356
  (* Format.eprintf "ok1@.@?"; *)
357
  let schedule = sch.Scheduling_type.schedule in
358
  (* Format.eprintf "ok2@.@?"; *)
359
  let sorted_eqs, unused = Scheduling.sort_equations_from_schedule eqs schedule in
360
  (* Format.eprintf "ok3@.locals=%a@.inout:%a@?"
361
   *   VSet.pp locals
362
   *   VSet.pp inout_vars
363
   * ; *)
364

    
365
  let ctx, ctx0_s = translate_core (assert_instrs@sorted_eqs) locals inout_vars in
366

    
367
  (* Format.eprintf "ok4@.@?"; *)
368

    
369
  (* Removing computed memories from locals. We also removed unused variables. *)
370
  let updated_locals =
371
    let l = VSet.elements (VSet.diff locals ctx.m) in
372
    List.fold_left (fun res v -> if List.mem v.var_id unused then res else v::res) [] l
373
  in
374
  let mmap = Utils.IMap.bindings ctx.j in
375
  {
376
    mname = nd;
377
    mmemory = VSet.elements ctx.m;
378
    mcalls = mmap;
379
    minstances = List.filter (fun (_, (n,_)) -> not (Stateless.check_node n)) mmap;
380
    minit = ctx.si;
381
    mconst = ctx0_s;
382
    mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs;
383
    mstep = {
384
      step_inputs = nd.node_inputs;
385
      step_outputs = nd.node_outputs;
386
      step_locals = updated_locals;
387
      step_checks = List.map (fun d -> d.Dimension.dim_loc,
388
                                       translate_expr env
389
                                         (expr_of_dimension d))
390
          nd.node_checks;
391
      step_instrs = (
392
        (* special treatment depending on the active backend. For horn backend,
393
           common branches are not merged while they are in C or Java
394
           backends. *)
395
        if !Backends.join_guards then
396
          join_guards_list ctx.s
397
        else
398
          ctx.s
399
      );
400
      step_asserts = List.map (translate_expr env) nd_node_asserts;
401
    };
402

    
403
    (* Processing spec: there is no processing performed here. Contract
404
       have been processed already. Either one of the other machine is a
405
       cocospec node, or the current one is a cocospec node. Contract do
406
       not contain any statement or import. *)
407

    
408
    mspec = { mnode_spec = nd.node_spec; mtransitions = [] };
409
    mannot = nd.node_annot;
410
    msch = Some sch;
411
  }
412

    
413
(** takes the global declarations and the scheduling associated to each node *)
414
let translate_prog decls node_schs =
415
  let nodes = get_nodes decls in
416
  let machines =
417
    List.map
418
      (fun decl ->
419
         let node = node_of_top decl in
420
         let sch = Utils.IMap.find node.node_id node_schs in
421
         translate_decl node sch
422
      ) nodes
423
  in
424
  machines
425

    
426
(* Local Variables: *)
427
(* compile-command:"make -C .." *)
428
(* End: *)
(30-30/63)