Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / normalization.ml @ 22fe1c93

History | View | Annotate | Download (13.6 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

    
200
and normalize_branches node offsets defvars hl =
201
 List.fold_right
202
   (fun (t, h) (defvars, norm_q) ->
203
     let (defvars, norm_h) = normalize_cond_expr node offsets defvars h in
204
     defvars, (t, norm_h) :: norm_q
205
   )
206
   hl (defvars, [])
207

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

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

    
240
and normalize_guard node defvars expr =
241
  match expr.expr_desc with
242
  | Expr_ident _ -> defvars, expr
243
  | _ ->
244
    let defvars, norm_expr = normalize_expr node [] defvars expr in
245
    mk_expr_alias_opt true node defvars norm_expr
246

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

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

    
295
let normalize_node node = 
296
  cpt_fresh := 0;
297
  let inputs_outputs = node.node_inputs@node.node_outputs in
298
  let is_local v =
299
    List.for_all ((!=) v) inputs_outputs in
300
  let defs, vars = 
301
    List.fold_left (normalize_eq node) ([], inputs_outputs@node.node_locals) node.node_eqs in
302
  let new_locals = List.filter is_local vars in
303
  let node =
304
  { node with node_locals = new_locals; node_eqs = defs }
305
  in ((*Printers.pp_node Format.err_formatter node;*) node)
306

    
307
let normalize_decl decl =
308
  match decl.top_decl_desc with
309
  | Node nd ->
310
    {decl with top_decl_desc = Node (normalize_node nd)}
311
  | Include _ | ImportedNode _ | ImportedFun _ | Consts _ -> decl
312
  
313
let normalize_prog decls = 
314
  List.map normalize_decl decls
315

    
316
(* Local Variables: *)
317
(* compile-command:"make -C .." *)
318
(* End: *)