Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / normalization.ml @ 52cfee34

History | View | Annotate | Download (13.8 KB)

1
(* ----------------------------------------------------------------------------
2
 * SchedMCore - A MultiCore Scheduling Framework
3
 * Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
4
 * Copyright (C) 2012-2013, INPT, Toulouse, FRANCE
5
 *
6
 * This file is part of Prelude
7
 *
8
 * Prelude is free software; you can redistribute it and/or
9
 * modify it under the terms of the GNU Lesser General Public License
10
 * as published by the Free Software Foundation ; either version 2 of
11
 * the License, or (at your option) any later version.
12
 *
13
 * Prelude is distributed in the hope that it will be useful, but
14
 * WITHOUT ANY WARRANTY ; without even the implied warranty of
15
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
16
 * Lesser General Public License for more details.
17
 *
18
 * You should have received a copy of the GNU Lesser General Public
19
 * License along with this program ; if not, write to the Free Software
20
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
21
 * USA
22
 *---------------------------------------------------------------------------- *)
23

    
24
(* This module is used for the lustre to C compiler *)
25

    
26

    
27
open Utils
28
open LustreSpec
29
open Corelang
30
(* open Clocks *)
31
open Format
32

    
33
let cpt_fresh = ref 0
34

    
35
(* Generate a new local [node] variable *)
36
let mk_fresh_var node loc ty ck =
37
  let vars = node_vars node in
38
  let rec aux () =
39
  incr cpt_fresh;
40
  let s = Printf.sprintf "__%s_%d" node.node_id !cpt_fresh in
41
  if List.exists (fun v -> v.var_id = s) vars then aux () else
42
  {
43
    var_id = s;
44
    var_dec_type = dummy_type_dec;
45
    var_dec_clock = dummy_clock_dec;
46
    var_dec_const = false;
47
    var_type = ty;
48
    var_clock = ck;
49
    var_loc = loc
50
  }
51
  in aux ()
52

    
53
(* Generate a new ident expression from a declared variable *)
54
let mk_ident_expr v =
55
  { expr_tag = new_tag ();
56
    expr_desc = Expr_ident v.var_id;
57
    expr_type = v.var_type;
58
    expr_clock = v.var_clock;
59
    expr_delay = Delay.new_var ();
60
    expr_annot = None;
61
    expr_loc = v.var_loc }
62

    
63
(* Get the equation in [defs] with [expr] as rhs, if any *)
64
let get_expr_alias defs expr =
65
 try Some (List.find (fun eq -> is_eq_expr eq.eq_rhs expr) defs)
66
 with
67
   Not_found -> None
68

    
69
(* Replace [expr] with (tuple of) [locals] *)
70
let replace_expr locals expr =
71
 match locals with
72
 | []  -> assert false
73
 | [v] -> { expr with
74
   expr_tag = Utils.new_tag ();
75
   expr_desc = Expr_ident v.var_id }
76
 | _   -> { expr with
77
   expr_tag = Utils.new_tag ();
78
   expr_desc = Expr_tuple (List.map mk_ident_expr locals) }
79

    
80
let unfold_offsets e offsets =
81
  let add_offset e d =
82
(*Format.eprintf "add_offset %a %a@." Dimension.pp_dimension (Types.array_type_dimension e.expr_type) Dimension.pp_dimension d;*)
83
    { e with
84
      expr_tag = Utils.new_tag ();
85
      expr_loc = d.Dimension.dim_loc;
86
      expr_type = Types.array_element_type e.expr_type;
87
      expr_desc = Expr_access (e, d) } in
88
 List.fold_left add_offset e offsets
89

    
90
(* Create an alias for [expr], if none exists yet *)
91
let mk_expr_alias node (defs, vars) expr =
92
  match get_expr_alias defs expr with
93
  | Some eq ->
94
    let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
95
    (defs, vars), replace_expr aliases expr
96
  | None    ->
97
    let new_aliases =
98
      List.map2
99
	(mk_fresh_var node expr.expr_loc)
100
	(Types.type_list_of_type expr.expr_type)
101
	(Clocks.clock_list_of_clock expr.expr_clock) in
102
    let new_def =
103
      mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
104
    in (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
105

    
106
(* Create an alias for [expr], if [opt] *)
107
let mk_expr_alias_opt opt node defvars expr =
108
 if opt
109
 then
110
   mk_expr_alias node defvars expr
111
 else
112
   defvars, expr
113

    
114
(* Create a (normalized) expression from [ref_e], 
115
   replacing description with [norm_d],
116
   taking propagated [offsets] into account 
117
   in order to change expression type *)
118
let mk_norm_expr offsets ref_e norm_d =
119
  let drop_array_type ty =
120
    Types.map_tuple_type Types.array_element_type ty in
121
  { ref_e with
122
    expr_desc = norm_d;
123
    expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type }
124

    
125
(* normalize_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
126
let rec normalize_list alias node offsets norm_element defvars elist =
127
  List.fold_right
128
    (fun t (defvars, qlist) ->
129
      let defvars, norm_t = norm_element alias node offsets defvars t in
130
      (defvars, norm_t :: qlist)
131
    ) elist (defvars, [])
132

    
133
let rec normalize_expr ?(alias=true) node offsets defvars expr =
134
(*  Format.eprintf "normalize %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
135
  match expr.expr_desc with
136
  | Expr_const _ 
137
  | Expr_ident _ -> defvars, unfold_offsets expr offsets
138
  | Expr_array elist ->
139
    let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
140
    let norm_expr = mk_norm_expr offsets expr (Expr_array norm_elist) in
141
    mk_expr_alias_opt alias node defvars norm_expr
142
  | Expr_power (e1, d) when offsets = [] ->
143
    let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
144
    let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in
145
    mk_expr_alias_opt alias node defvars norm_expr
146
  | Expr_power (e1, d) ->
147
    normalize_expr ~alias:alias node (List.tl offsets) defvars e1
148
  | Expr_access (e1, d) ->
149
    normalize_expr ~alias:alias node (d::offsets) defvars e1
150
  | Expr_tuple elist -> 
151
    let defvars, norm_elist =
152
      normalize_list alias node offsets (fun alias -> normalize_expr ~alias:alias) defvars elist in
153
    defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)
154
  | Expr_appl (id, args, None) when Basic_library.is_internal_fun id && Types.is_array_type expr.expr_type ->
155
    let defvars, norm_args = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in
156
    defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
157
  | Expr_appl (id, args, None) when Basic_library.is_internal_fun id ->
158
    let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in
159
    defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None))
160
  | Expr_appl (id, args, r) ->
161
    let defvars, norm_args = normalize_expr node [] defvars args in
162
    let norm_expr = mk_norm_expr [] expr (Expr_appl (id, norm_args, r)) in
163
    if offsets <> []
164
    then
165
      let defvars, norm_expr = normalize_expr node [] defvars norm_expr in
166
      normalize_expr ~alias:alias node offsets defvars norm_expr
167
    else
168
      mk_expr_alias_opt (alias && not (Basic_library.is_internal_fun id)) node defvars norm_expr
169
  | Expr_arrow (e1,e2) -> (* Here we differ from Colaco paper: arrows are pushed to the top *)
170
    let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
171
    let defvars, norm_e2 = normalize_expr node offsets defvars e2 in
172
    let norm_expr = mk_norm_expr offsets expr (Expr_arrow (norm_e1, norm_e2)) in
173
    mk_expr_alias_opt alias node defvars norm_expr
174
  | Expr_pre e ->
175
    let defvars, norm_e = normalize_expr node offsets defvars e in
176
    let norm_expr = mk_norm_expr offsets expr (Expr_pre norm_e) in
177
    mk_expr_alias_opt alias node defvars norm_expr
178
  | Expr_fby (e1, e2) ->
179
    let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
180
    let defvars, norm_e2 = normalize_expr node offsets defvars e2 in
181
    let norm_expr = mk_norm_expr offsets expr (Expr_fby (norm_e1, norm_e2)) in
182
    mk_expr_alias_opt alias node defvars norm_expr
183
  | Expr_when (e, c, l) ->
184
    let defvars, norm_e = normalize_expr node offsets defvars e in
185
    defvars, mk_norm_expr offsets expr (Expr_when (norm_e, c, l))
186
  | Expr_ite (c, t, e) ->
187
    let defvars, norm_c = normalize_guard node defvars c in
188
    let defvars, norm_t = normalize_cond_expr  node offsets defvars t in
189
    let defvars, norm_e = normalize_cond_expr  node offsets defvars e in
190
    let norm_expr = mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e)) in
191
    mk_expr_alias_opt alias node defvars norm_expr
192
  | Expr_merge (c, hl) ->
193
    let defvars, norm_hl = normalize_branches node offsets defvars hl in
194
    let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in
195
    mk_expr_alias_opt alias node defvars norm_expr
196
  | Expr_uclock _
197
  | Expr_dclock _ 
198
  | Expr_phclock _ -> assert false (* Not handled yet *)
199
(* Creates a conditional with a merge construct, which is more lazy *)
200
(*
201
let norm_conditional_as_merge alias node norm_expr offsets defvars expr =
202
 match expr.expr_desc with
203
 | Expr_ite (c, t, e) ->
204
   let defvars, norm_t = norm_expr (alias node offsets defvars t in
205
 | _ -> assert false
206
*)
207
and normalize_branches node offsets defvars hl =
208
 List.fold_right
209
   (fun (t, h) (defvars, norm_q) ->
210
     let (defvars, norm_h) = normalize_cond_expr node offsets defvars h in
211
     defvars, (t, norm_h) :: norm_q
212
   )
213
   hl (defvars, [])
214

    
215
and normalize_array_expr ?(alias=true) node offsets defvars expr =
216
(*  Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
217
  match expr.expr_desc with
218
  | Expr_power (e1, d) when offsets = [] ->
219
    let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
220
    defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))
221
  | Expr_power (e1, d) ->
222
    normalize_array_expr ~alias:alias node (List.tl offsets) defvars e1
223
  | Expr_access (e1, d) -> normalize_array_expr ~alias:alias node (d::offsets) defvars e1
224
  | Expr_array elist when offsets = [] ->
225
    let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
226
    defvars, mk_norm_expr offsets expr (Expr_array norm_elist)
227
  | Expr_appl (id, args, None) when Basic_library.is_internal_fun id ->
228
    let defvars, norm_args = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in
229
    defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
230
  |  _ -> normalize_expr ~alias:alias node offsets defvars expr
231

    
232
and normalize_cond_expr ?(alias=true) node offsets defvars expr =
233
  (*Format.eprintf "normalize_cond %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
234
  match expr.expr_desc with
235
  | Expr_access (e1, d) ->
236
    normalize_cond_expr ~alias:alias node (d::offsets) defvars e1
237
  | Expr_ite (c, t, e) ->
238
    let defvars, norm_c = normalize_guard node defvars c in
239
    let defvars, norm_t = normalize_cond_expr node offsets defvars t in
240
    let defvars, norm_e = normalize_cond_expr node offsets defvars e in
241
    defvars, mk_norm_expr offsets expr (Expr_ite (norm_c, norm_t, norm_e))
242
  | Expr_merge (c, hl) ->
243
    let defvars, norm_hl = normalize_branches node offsets defvars hl in
244
    defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl))
245
  | _ -> normalize_expr ~alias:alias node offsets defvars expr
246

    
247
and normalize_guard node defvars expr =
248
  match expr.expr_desc with
249
  | Expr_ident _ -> defvars, expr
250
  | _ ->
251
    let defvars, norm_expr = normalize_expr node [] defvars expr in
252
    mk_expr_alias_opt true node defvars norm_expr
253

    
254
(* outputs cannot be memories as well. If so, introduce new local variable.
255
*)
256
let decouple_outputs node defvars eq =
257
  let rec fold_lhs defvars lhs tys cks =
258
   match lhs, tys, cks with
259
   | [], [], []          -> defvars, []
260
   | v::qv, t::qt, c::qc -> let (defs_q, vars_q), lhs_q = fold_lhs defvars qv qt qc in
261
			    if List.exists (fun o -> o.var_id = v) node.node_outputs
262
			    then
263
			      let newvar = mk_fresh_var node eq.eq_loc t c in
264
			      let neweq  = mkeq eq.eq_loc ([v], mk_ident_expr newvar) in
265
			      (neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q
266
			    else
267
			      (defs_q, vars_q), v::lhs_q
268
   | _                   -> assert false in
269
  let defvars', lhs' =
270
    fold_lhs
271
      defvars
272
      eq.eq_lhs
273
      (Types.type_list_of_type eq.eq_rhs.expr_type)
274
      (Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in
275
  defvars', {eq with eq_lhs = lhs' }
276

    
277
let rec normalize_eq node defvars eq = 
278
  match eq.eq_rhs.expr_desc with
279
  | Expr_pre _
280
  | Expr_fby _  ->
281
    let (defvars', eq') = decouple_outputs node defvars eq in
282
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars' eq'.eq_rhs in
283
    let norm_eq = { eq' with eq_rhs = norm_rhs } in
284
    (norm_eq::defs', vars')
285
  | Expr_array _ ->
286
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
287
    let norm_eq = { eq with eq_rhs = norm_rhs } in
288
    (norm_eq::defs', vars')
289
  | Expr_appl (id, _, None) when Basic_library.is_internal_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
290
    let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
291
    let norm_eq = { eq with eq_rhs = norm_rhs } in
292
    (norm_eq::defs', vars')
293
  | Expr_appl _ ->
294
    let (defs', vars'), norm_rhs = normalize_expr ~alias:false node [] defvars eq.eq_rhs in
295
    let norm_eq = { eq with eq_rhs = norm_rhs } in
296
    (norm_eq::defs', vars')
297
  | _ ->
298
    let (defs', vars'), norm_rhs = normalize_cond_expr ~alias:false node [] defvars eq.eq_rhs in
299
    let norm_eq = { eq with eq_rhs = norm_rhs } in
300
    norm_eq::defs', vars'
301

    
302
let normalize_node node = 
303
  cpt_fresh := 0;
304
  let inputs_outputs = node.node_inputs@node.node_outputs in
305
  let is_local v =
306
    List.for_all ((!=) v) inputs_outputs in
307
  let defs, vars = 
308
    List.fold_left (normalize_eq node) ([], inputs_outputs@node.node_locals) node.node_eqs in
309
  let new_locals = List.filter is_local vars in
310
  let node =
311
  { node with node_locals = new_locals; node_eqs = defs }
312
  in ((*Printers.pp_node Format.err_formatter node;*) node)
313

    
314
let normalize_decl decl =
315
  match decl.top_decl_desc with
316
  | Node nd ->
317
    {decl with top_decl_desc = Node (normalize_node nd)}
318
  | Open _ | ImportedNode _ | Consts _ -> decl
319
  
320
let normalize_prog decls = 
321
  List.map normalize_decl decls
322

    
323
(* Local Variables: *)
324
(* compile-command:"make -C .." *)
325
(* End: *)