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 Utils
|
13
|
open LustreSpec
|
14
|
open Corelang
|
15
|
open Normalization
|
16
|
open Machine_code
|
17
|
|
18
|
let mpfr_module = mktop (Open(false, "mpfr_lustre"))
|
19
|
|
20
|
let mpfr_rnd () = "MPFR_RNDN"
|
21
|
|
22
|
let mpfr_prec () = !Options.mpfr_prec
|
23
|
|
24
|
let inject_id = "MPFRId"
|
25
|
|
26
|
let inject_copy_id = "mpfr_set"
|
27
|
|
28
|
let inject_real_id = "mpfr_set_flt"
|
29
|
|
30
|
let inject_init_id = "mpfr_init2"
|
31
|
|
32
|
let inject_clear_id = "mpfr_clear"
|
33
|
|
34
|
let mpfr_t = "mpfr_t"
|
35
|
|
36
|
let unfoldable_value value =
|
37
|
not (Types.is_real_type value.value_type && is_const_value value)
|
38
|
|
39
|
let inject_id_id expr =
|
40
|
let e = mkpredef_call expr.expr_loc inject_id [expr] in
|
41
|
{ e with
|
42
|
expr_type = Type_predef.type_real;
|
43
|
expr_clock = expr.expr_clock;
|
44
|
}
|
45
|
|
46
|
let pp_inject_real pp_var fmt var value =
|
47
|
Format.fprintf fmt "%s(%a, %a, %s);"
|
48
|
inject_real_id
|
49
|
pp_var var
|
50
|
pp_var value
|
51
|
(mpfr_rnd ())
|
52
|
|
53
|
let inject_assign expr =
|
54
|
let e = mkpredef_call expr.expr_loc inject_copy_id [expr] in
|
55
|
{ e with
|
56
|
expr_type = Type_predef.type_real;
|
57
|
expr_clock = expr.expr_clock;
|
58
|
}
|
59
|
|
60
|
let pp_inject_copy pp_var fmt var value =
|
61
|
Format.fprintf fmt "%s(%a, %a, %s);"
|
62
|
inject_copy_id
|
63
|
pp_var var
|
64
|
pp_var value
|
65
|
(mpfr_rnd ())
|
66
|
|
67
|
let rec pp_inject_assign pp_var fmt var value =
|
68
|
if is_const_value value
|
69
|
then
|
70
|
pp_inject_real pp_var fmt var value
|
71
|
else
|
72
|
pp_inject_copy pp_var fmt var value
|
73
|
|
74
|
let pp_inject_init pp_var fmt var =
|
75
|
Format.fprintf fmt "%s(%a, %i);"
|
76
|
inject_init_id
|
77
|
pp_var var
|
78
|
(mpfr_prec ())
|
79
|
|
80
|
let pp_inject_clear pp_var fmt var =
|
81
|
Format.fprintf fmt "%s(%a);"
|
82
|
inject_clear_id
|
83
|
pp_var var
|
84
|
|
85
|
let base_inject_op id =
|
86
|
match id with
|
87
|
| "+" -> "MPFRPlus"
|
88
|
| "-" -> "MPFRMinus"
|
89
|
| "*" -> "MPFRTimes"
|
90
|
| "/" -> "MPFRDiv"
|
91
|
| "uminus" -> "MPFRUminus"
|
92
|
| "<=" -> "MPFRLe"
|
93
|
| "<" -> "MPFRLt"
|
94
|
| ">=" -> "MPFRGe"
|
95
|
| ">" -> "MPFRGt"
|
96
|
| "=" -> "MPFREq"
|
97
|
| "!=" -> "MPFRNeq"
|
98
|
| _ -> raise Not_found
|
99
|
|
100
|
let inject_op id =
|
101
|
try
|
102
|
base_inject_op id
|
103
|
with Not_found -> id
|
104
|
|
105
|
let homomorphic_funs =
|
106
|
List.fold_right (fun id res -> try base_inject_op id :: res with Not_found -> res) Basic_library.internal_funs []
|
107
|
|
108
|
let is_homomorphic_fun id =
|
109
|
List.mem id homomorphic_funs
|
110
|
|
111
|
let inject_call expr =
|
112
|
match expr.expr_desc with
|
113
|
| Expr_appl (id, args, None) when not (Basic_library.is_expr_internal_fun expr) ->
|
114
|
{ expr with expr_desc = Expr_appl (inject_op id, args, None) }
|
115
|
| _ -> expr
|
116
|
|
117
|
let expr_of_const_array expr =
|
118
|
match expr.expr_desc with
|
119
|
| Expr_const (Const_array cl) ->
|
120
|
let typ = Types.array_element_type expr.expr_type in
|
121
|
let expr_of_const c =
|
122
|
{ expr_desc = Expr_const c;
|
123
|
expr_type = typ;
|
124
|
expr_clock = expr.expr_clock;
|
125
|
expr_loc = expr.expr_loc;
|
126
|
expr_delay = Delay.new_var ();
|
127
|
expr_annot = None;
|
128
|
expr_tag = new_tag ();
|
129
|
}
|
130
|
in { expr with expr_desc = Expr_array (List.map expr_of_const cl) }
|
131
|
| _ -> assert false
|
132
|
|
133
|
(* inject_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
|
134
|
let rec inject_list alias node inject_element defvars elist =
|
135
|
List.fold_right
|
136
|
(fun t (defvars, qlist) ->
|
137
|
let defvars, norm_t = inject_element alias node defvars t in
|
138
|
(defvars, norm_t :: qlist)
|
139
|
) elist (defvars, [])
|
140
|
|
141
|
let rec inject_expr ?(alias=true) node defvars expr =
|
142
|
let res=
|
143
|
match expr.expr_desc with
|
144
|
| Expr_const (Const_real _) -> mk_expr_alias_opt alias node defvars expr
|
145
|
| Expr_const (Const_array _) -> inject_expr ~alias:alias node defvars (expr_of_const_array expr)
|
146
|
| Expr_const (Const_struct _) -> assert false
|
147
|
| Expr_ident _
|
148
|
| Expr_const _ -> defvars, expr
|
149
|
| Expr_array elist ->
|
150
|
let defvars, norm_elist = inject_list alias node (fun _ -> inject_expr ~alias:true) defvars elist in
|
151
|
let norm_expr = { expr with expr_desc = Expr_array norm_elist } in
|
152
|
defvars, norm_expr
|
153
|
| Expr_power (e1, d) ->
|
154
|
let defvars, norm_e1 = inject_expr node defvars e1 in
|
155
|
let norm_expr = { expr with expr_desc = Expr_power (norm_e1, d) } in
|
156
|
defvars, norm_expr
|
157
|
| Expr_access (e1, d) ->
|
158
|
let defvars, norm_e1 = inject_expr node defvars e1 in
|
159
|
let norm_expr = { expr with expr_desc = Expr_access (norm_e1, d) } in
|
160
|
defvars, norm_expr
|
161
|
| Expr_tuple elist ->
|
162
|
let defvars, norm_elist =
|
163
|
inject_list alias node (fun alias -> inject_expr ~alias:alias) defvars elist in
|
164
|
let norm_expr = { expr with expr_desc = Expr_tuple norm_elist } in
|
165
|
defvars, norm_expr
|
166
|
| Expr_appl (id, args, r) ->
|
167
|
let defvars, norm_args = inject_expr node defvars args in
|
168
|
let norm_expr = { expr with expr_desc = Expr_appl (id, norm_args, r) } in
|
169
|
mk_expr_alias_opt alias node defvars (inject_call norm_expr)
|
170
|
| Expr_arrow _ -> defvars, expr
|
171
|
| Expr_pre e ->
|
172
|
let defvars, norm_e = inject_expr node defvars e in
|
173
|
let norm_expr = { expr with expr_desc = Expr_pre norm_e } in
|
174
|
defvars, norm_expr
|
175
|
| Expr_fby (e1, e2) ->
|
176
|
let defvars, norm_e1 = inject_expr node defvars e1 in
|
177
|
let defvars, norm_e2 = inject_expr node defvars e2 in
|
178
|
let norm_expr = { expr with expr_desc = Expr_fby (norm_e1, norm_e2) } in
|
179
|
defvars, norm_expr
|
180
|
| Expr_when (e, c, l) ->
|
181
|
let defvars, norm_e = inject_expr node defvars e in
|
182
|
let norm_expr = { expr with expr_desc = Expr_when (norm_e, c, l) } in
|
183
|
defvars, norm_expr
|
184
|
| Expr_ite (c, t, e) ->
|
185
|
let defvars, norm_c = inject_expr node defvars c in
|
186
|
let defvars, norm_t = inject_expr node defvars t in
|
187
|
let defvars, norm_e = inject_expr node defvars e in
|
188
|
let norm_expr = { expr with expr_desc = Expr_ite (norm_c, norm_t, norm_e) } in
|
189
|
defvars, norm_expr
|
190
|
| Expr_merge (c, hl) ->
|
191
|
let defvars, norm_hl = inject_branches node defvars hl in
|
192
|
let norm_expr = { expr with expr_desc = Expr_merge (c, norm_hl) } in
|
193
|
defvars, norm_expr
|
194
|
in
|
195
|
(*Format.eprintf "inject_expr %B %a = %a@." alias Printers.pp_expr expr Printers.pp_expr (snd res);*)
|
196
|
res
|
197
|
|
198
|
and inject_branches node defvars hl =
|
199
|
List.fold_right
|
200
|
(fun (t, h) (defvars, norm_q) ->
|
201
|
let (defvars, norm_h) = inject_expr node defvars h in
|
202
|
defvars, (t, norm_h) :: norm_q
|
203
|
)
|
204
|
hl (defvars, [])
|
205
|
|
206
|
|
207
|
let rec inject_eq node defvars eq =
|
208
|
let (defs', vars'), norm_rhs = inject_expr ~alias:false node defvars eq.eq_rhs in
|
209
|
let norm_eq = { eq with eq_rhs = norm_rhs } in
|
210
|
norm_eq::defs', vars'
|
211
|
|
212
|
(** normalize_node node returns a normalized node,
|
213
|
ie.
|
214
|
- updated locals
|
215
|
- new equations
|
216
|
-
|
217
|
*)
|
218
|
let inject_node node =
|
219
|
cpt_fresh := 0;
|
220
|
let inputs_outputs = node.node_inputs@node.node_outputs in
|
221
|
let is_local v =
|
222
|
List.for_all ((!=) v) inputs_outputs in
|
223
|
let orig_vars = inputs_outputs@node.node_locals in
|
224
|
let defs, vars =
|
225
|
List.fold_left (inject_eq node) ([], orig_vars) (get_node_eqs node) in
|
226
|
(* Normalize the asserts *)
|
227
|
let vars, assert_defs, asserts =
|
228
|
List.fold_left (
|
229
|
fun (vars, def_accu, assert_accu) assert_ ->
|
230
|
let assert_expr = assert_.assert_expr in
|
231
|
let (defs, vars'), expr =
|
232
|
inject_expr
|
233
|
~alias:false
|
234
|
node
|
235
|
([], vars) (* defvar only contains vars *)
|
236
|
assert_expr
|
237
|
in
|
238
|
vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
|
239
|
) (vars, [], []) node.node_asserts in
|
240
|
let new_locals = List.filter is_local vars in
|
241
|
(* Compute traceability info:
|
242
|
- gather newly bound variables
|
243
|
- compute the associated expression without aliases
|
244
|
*)
|
245
|
(* let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals)) new_locals in *)
|
246
|
let node =
|
247
|
{ node with
|
248
|
node_locals = new_locals;
|
249
|
node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
|
250
|
}
|
251
|
in ((*Printers.pp_node Format.err_formatter node;*) node)
|
252
|
|
253
|
let inject_decl decl =
|
254
|
match decl.top_decl_desc with
|
255
|
| Node nd ->
|
256
|
{decl with top_decl_desc = Node (inject_node nd)}
|
257
|
| Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
|
258
|
|
259
|
let inject_prog decls =
|
260
|
List.map inject_decl decls
|
261
|
|
262
|
|
263
|
(* Local Variables: *)
|
264
|
(* compile-command:"make -C .." *)
|
265
|
(* End: *)
|