Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / machine_code.ml @ e8f55c25

History | View | Annotate | Download (16.6 KB)

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
47
                  VSet.get id all
48
                with Not_found -> (
49
                  (* Format.eprintf "Impossible to find variable %s in set %a@.@?"
50
                   *   id
51
                   *   VSet.pp all; *)
52
                  raise Not_found
53
                )
54
              )  
55
  }
56

    
57
  
58

    
59
(****************************************************************)
60
(* Basic functions to translate to machine values, instructions *) 
61
(****************************************************************)
62

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

    
84
let rec control_on_clock env ck inst =
85
 match (Clocks.repr ck).cdesc with
86
 | Con    (ck1, cr, l) ->
87
   let id  = Clocks.const_of_carrier cr in
88
   control_on_clock env ck1
89
     (mkinstr
90
	(MBranch (translate_ident env id,
91
		  [l, [inst]] )))
92
 | _                   -> inst
93

    
94

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

    
110
let specialize_op expr =
111
  match !Options.output with
112
  | "C" -> specialize_to_c expr
113
  | _   -> expr
114

    
115
let rec translate_expr env expr =
116
  let expr = specialize_op expr in
117
  let translate_expr = translate_expr env in
118
  let value_desc = 
119
    match expr.expr_desc with
120
    | Expr_const v                     -> Cst v
121
    | Expr_ident x                     -> (translate_ident env x).value_desc
122
    | Expr_array el                    -> Array (List.map translate_expr el)
123
    | Expr_access (t, i)               -> Access (translate_expr t,
124
                                                  translate_expr 
125
                                                    (expr_of_dimension i))
126
    | Expr_power  (e, n)               -> Power  (translate_expr e,
127
                                                  translate_expr
128
                                                    (expr_of_dimension n))
129
    | Expr_tuple _
130
      | Expr_arrow _ 
131
      | Expr_fby _
132
      | Expr_pre _                       -> (Printers.pp_expr
133
                                               Format.err_formatter expr;
134
                                             Format.pp_print_flush
135
                                               Format.err_formatter ();
136
                                             raise NormalizationError)
137
                                          
138
    | Expr_when    (e1, _, _)          -> (translate_expr e1).value_desc
139
    | Expr_merge   (x, _)              -> raise NormalizationError
140
    | Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr ->
141
       let nd = node_from_name id in
142
       Fun (node_name nd, List.map translate_expr (expr_list_of_expr e))
143
    | Expr_ite (g,t,e) -> (
144
      (* special treatment depending on the active backend. For
145
         functional ones, like horn backend, ite are preserved in
146
         expression. While they are removed for C or Java backends. *)
147
      if Backends.is_functional () then
148
	Fun ("ite", [translate_expr g; translate_expr t; translate_expr e])
149
      else 
150
	(Format.eprintf "Normalization error for backend %s: %a@."
151
	   !Options.output
152
	   Printers.pp_expr expr;
153
	 raise NormalizationError)
154
    )
155
    | _                   -> raise NormalizationError
156
  in
157
  mk_val value_desc expr.expr_type
158

    
159
let translate_guard env expr =
160
  match expr.expr_desc with
161
  | Expr_ident x  -> translate_ident env x
162
  | _ -> (Format.eprintf "internal error: translate_guard %a@."
163
            Printers.pp_expr expr;
164
          assert false)
165

    
166
let rec translate_act env (y, expr) =
167
  let translate_act = translate_act env in
168
  let translate_guard = translate_guard env in
169
  let translate_ident = translate_ident env in
170
  let translate_expr = translate_expr env in
171
  let eq = Corelang.mkeq Location.dummy_loc ([y.var_id], expr) in
172
  match expr.expr_desc with
173
  | Expr_ite   (c, t, e) -> let g = translate_guard c in
174
			    mk_conditional ?lustre_eq:(Some eq) g
175
                              [translate_act (y, t)]
176
                              [translate_act (y, e)]
177
  | Expr_merge (x, hl)   -> mkinstr ?lustre_eq:(Some eq)
178
                              (MBranch (translate_ident x,
179
                                        List.map (fun (t,  h) ->
180
                                            t, [translate_act (y, h)])
181
                                          hl))
182
  | _                    -> mkinstr ?lustre_eq:(Some eq)
183
                              (MLocalAssign (y, translate_expr expr))
184

    
185
let reset_instance env i r c =
186
  match r with
187
  | None        -> []
188
  | Some r      -> let g = translate_guard env r in
189
                   [control_on_clock
190
                      env
191
                      c
192
                      (mk_conditional
193
                         g
194
                         [mkinstr (MReset i)]
195
                         [mkinstr (MNoReset i)])
196
                   ]
197

    
198

    
199
(* Datastructure updated while visiting equations *)
200
type machine_ctx = {
201
    m: VSet.t; (* Memories *)
202
    si: instr_t list;
203
    j: (Lustre_types.top_decl * Dimension.dim_expr list) Utils.IMap.t;
204
    s: instr_t list;
205
  }
206

    
207
let ctx_init = { m = VSet.empty; (* memories *)
208
                 si = []; (* init instr *)
209
                 j = Utils.IMap.empty;
210
                 s = [] }
211
             
212
(****************************************************************)
213
(* Main function to translate equations into this machine context we
214
   are building *) 
215
(****************************************************************)
216

    
217
                   
218

    
219
let translate_eq env ctx eq =
220
  let translate_expr = translate_expr env in
221
  let translate_act = translate_act env in
222
  let control_on_clock = control_on_clock env in
223
  let reset_instance = reset_instance env in
224

    
225
  (* Format.eprintf "translate_eq %a with clock %a@." 
226
     Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;  *)
227
  match eq.eq_lhs, eq.eq_rhs.expr_desc with
228
  | [x], Expr_arrow (e1, e2)                     ->
229
     let var_x = env.get_var x in
230
     let o = new_instance Arrow.arrow_top_decl eq.eq_rhs.expr_tag in
231
     let c1 = translate_expr e1 in
232
     let c2 = translate_expr e2 in
233
     { ctx with
234
       si = mkinstr (MReset o) :: ctx.si;
235
       j = Utils.IMap.add o (Arrow.arrow_top_decl, []) ctx.j;
236
       s = (control_on_clock
237
              eq.eq_rhs.expr_clock
238
              (mkinstr ?lustre_eq:(Some eq) (MStep ([var_x], o, [c1;c2])))
239
           ) :: ctx.s
240
     }
241
  | [x], Expr_pre e1 when env.is_local x    ->
242
     let var_x = env.get_var x in
243
     
244
      { ctx with
245
        m = VSet.add var_x ctx.m;
246
        s = control_on_clock
247
              eq.eq_rhs.expr_clock
248
              (mkinstr ?lustre_eq:(Some eq)
249
                 (MStateAssign (var_x, translate_expr e1)))
250
            :: ctx.s
251
      }
252
  | [x], Expr_fby (e1, e2) when env.is_local x ->
253
     let var_x = env.get_var x in
254
     { ctx with
255
       m = VSet.add var_x ctx.m;
256
       si = mkinstr ?lustre_eq:(Some eq)
257
              (MStateAssign (var_x, translate_expr e1))
258
            :: ctx.si;
259
       s = control_on_clock
260
             eq.eq_rhs.expr_clock
261
             (mkinstr ?lustre_eq:(Some eq)
262
                (MStateAssign (var_x, translate_expr e2)))
263
           :: ctx.s
264
     }
265

    
266
  | p  , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
267
     let var_p = List.map (fun v -> env.get_var v) p in
268
     let el = expr_list_of_expr arg in
269
     let vl = List.map translate_expr el in
270
     let node_f = node_from_name f in
271
     let call_f =
272
       node_f,
273
       NodeDep.filter_static_inputs (node_inputs node_f) el in
274
     let o = new_instance node_f eq.eq_rhs.expr_tag in
275
     let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in
276
     let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in
277
     (*Clocks.new_var true in
278
       Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
279
       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;*)
280
     { ctx with
281
       si = 
282
         (if Stateless.check_node node_f then ctx.si else mkinstr (MReset o) :: ctx.si);
283
      j = Utils.IMap.add o call_f ctx.j;
284
      s = (if Stateless.check_node node_f
285
           then []
286
           else reset_instance o r call_ck) @
287
	    (control_on_clock call_ck
288
               (mkinstr ?lustre_eq:(Some eq) (MStep (var_p, o, vl))))
289
            :: ctx.s
290
     }
291

    
292
  | [x], _                                       -> (
293
    let var_x = env.get_var x in
294
    { ctx with
295
      s = 
296
     control_on_clock 
297
       eq.eq_rhs.expr_clock
298
       (translate_act (var_x, eq.eq_rhs)) :: ctx.s
299
    }
300
  )
301
  | _                                            ->
302
     begin
303
       Format.eprintf "internal error: Machine_code.translate_eq %a@?"
304
         Printers.pp_node_eq eq;
305
       assert false
306
     end
307

    
308

    
309

    
310
let constant_equations locals =
311
 VSet.fold (fun vdecl eqs ->
312
   if vdecl.var_dec_const
313
   then
314
     { eq_lhs = [vdecl.var_id];
315
       eq_rhs = Utils.desome vdecl.var_dec_value;
316
       eq_loc = vdecl.var_loc
317
     } :: eqs
318
   else eqs)
319
   locals []
320

    
321
let translate_eqs env ctx eqs =
322
  List.fold_right (fun eq ctx -> translate_eq env ctx eq) eqs ctx;;
323

    
324

    
325
(****************************************************************)
326
(* Processing nodes *) 
327
(****************************************************************)
328

    
329
let process_asserts nd =
330
  
331
    let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
332
    if Backends.is_functional () then
333
      [], [], exprl  
334
    else (* Each assert(e) is associated to a fresh variable v and declared as
335
	    v=e; assert (v); *)
336
      let _, vars, eql, assertl =
337
	List.fold_left (fun (i, vars, eqlist, assertlist) expr ->
338
	  let loc = expr.expr_loc in
339
	  let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in
340
	  let assert_var =
341
	    mkvar_decl
342
	      loc
343
	      ~orig:false (* fresh var *)
344
	      (var_id,
345
	       mktyp loc Tydec_bool,
346
	       mkclock loc Ckdec_any,
347
	       false, (* not a constant *)
348
	       None, (* no default value *)
349
	       Some nd.node_id
350
	      )
351
	  in
352
	  assert_var.var_type <- Type_predef.type_bool (* Types.new_ty (Types.Tbool) *); 
353
	  let eq = mkeq loc ([var_id], expr) in
354
          (i+1,
355
           assert_var::vars,
356
           eq::eqlist,
357
           {expr with expr_desc = Expr_ident var_id}::assertlist)
358
	) (1, [], [], []) exprl
359
      in
360
      vars, eql, assertl
361

    
362
let translate_core sorted_eqs locals other_vars =
363
  let constant_eqs = constant_equations locals in
364
  
365
  let env = build_env locals other_vars  in
366
  
367
  (* Compute constants' instructions  *)
368
  let ctx0 = translate_eqs env ctx_init constant_eqs in
369
  assert (VSet.is_empty ctx0.m);
370
  assert (ctx0.si = []);
371
  assert (Utils.IMap.is_empty ctx0.j);
372
  
373
  (* Compute ctx for all eqs *)
374
  let ctx = translate_eqs env ctx_init sorted_eqs in
375
  
376
  ctx, ctx0.s
377

    
378
 
379
let translate_decl nd sch =
380
  (* Format.eprintf "Translating node %s@." nd.node_id; *)
381
  (* Extracting eqs, variables ..  *)
382
  let eqs, auts = get_node_eqs nd in
383
  assert (auts = []); (* Automata should be expanded by now *)
384
  
385
  (* In case of non functional backend (eg. C), additional local variables have
386
     to be declared for each assert *)
387
  let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in
388

    
389
  (* Build the env: variables visible in the current scope *)
390
  let locals_list = nd.node_locals @ new_locals in
391
  let locals = VSet.of_list locals_list in
392
  let inout_vars = (VSet.of_list (nd.node_inputs @ nd.node_outputs)) in
393
  let env = build_env locals inout_vars  in 
394

    
395
  (* Format.eprintf "Node content is %a@." Printers.pp_node nd; *)
396
  
397
  (* Computing main content *)
398
  (* Format.eprintf "ok1@.@?"; *)
399
  let schedule = sch.Scheduling_type.schedule in
400
  (* Format.eprintf "ok2@.@?"; *)
401
  let sorted_eqs, unused = Scheduling.sort_equations_from_schedule eqs schedule in
402
  (* Format.eprintf "ok3@.locals=%a@.inout:%a@?"
403
   *   VSet.pp locals
404
   *   VSet.pp inout_vars
405
   * ; *)
406
  
407
  let ctx, ctx0_s = translate_core (assert_instrs@sorted_eqs) locals inout_vars in
408
  
409
  (* Format.eprintf "ok4@.@?"; *)
410

    
411
  (* Removing computed memories from locals. We also removed unused variables. *)
412
  let updated_locals =
413
    let l = VSet.elements (VSet.diff locals ctx.m) in
414
    List.fold_left (fun res v -> if List.mem v.var_id unused then res else v::res) [] l
415
  in
416
  let mmap = Utils.IMap.elements ctx.j in
417
  {
418
    mname = nd;
419
    mmemory = VSet.elements ctx.m;
420
    mcalls = mmap;
421
    minstances = List.filter (fun (_, (n,_)) -> not (Stateless.check_node n)) mmap;
422
    minit = ctx.si;
423
    mconst = ctx0_s;
424
    mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs;
425
    mstep = {
426
        step_inputs = nd.node_inputs;
427
        step_outputs = nd.node_outputs;
428
        step_locals = updated_locals;
429
        step_checks = List.map (fun d -> d.Dimension.dim_loc,
430
                                         translate_expr env 
431
                                           (expr_of_dimension d))
432
                        nd.node_checks;
433
        step_instrs = (
434
	  (* special treatment depending on the active backend. For horn backend,
435
	   common branches are not merged while they are in C or Java
436
	   backends. *)
437
	  if !Backends.join_guards then
438
	    join_guards_list ctx.s
439
	  else
440
	    ctx.s
441
        );
442
        step_asserts = List.map (translate_expr env) nd_node_asserts;
443
      };
444

    
445
    (* Processing spec: there is no processing performed here. Contract
446
     have been processed already. Either one of the other machine is a
447
     cocospec node, or the current one is a cocospec node. Contract do
448
     not contain any statement or import. *)
449
 
450
    mspec = nd.node_spec;
451
    mannot = nd.node_annot;
452
    msch = Some sch;
453
  }
454

    
455
(** takes the global declarations and the scheduling associated to each node *)
456
let translate_prog decls node_schs =
457
  let nodes = get_nodes decls in
458
  let machines =
459
    List.map
460
    (fun decl ->
461
     let node = node_of_top decl in
462
      let sch = Utils.IMap.find node.node_id node_schs in
463
      translate_decl node sch
464
    ) nodes
465
  in
466
  machines
467

    
468
    (* Local Variables: *)
469
    (* compile-command:"make -C .." *)
470
    (* End: *)