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 Lustre_types
|
14
|
open Machine_code_types
|
15
|
open Corelang
|
16
|
open Normalization
|
17
|
open Machine_code_common
|
18
|
|
19
|
let report = Log.report ~plugin:"MPFR"
|
20
|
|
21
|
let mpfr_module = mktop (Open (false, "mpfr_lustre"))
|
22
|
|
23
|
let cpt_fresh = ref 0
|
24
|
|
25
|
let mpfr_rnd () = "MPFR_RNDN"
|
26
|
|
27
|
let mpfr_prec () = !Options.mpfr_prec
|
28
|
|
29
|
let inject_id = "MPFRId"
|
30
|
|
31
|
let inject_copy_id = "mpfr_set"
|
32
|
|
33
|
let inject_real_id = "mpfr_set_flt"
|
34
|
|
35
|
let inject_init_id = "mpfr_init2"
|
36
|
|
37
|
let inject_clear_id = "mpfr_clear"
|
38
|
|
39
|
let mpfr_t = "mpfr_t"
|
40
|
|
41
|
let unfoldable_value value =
|
42
|
not (Types.is_real_type value.value_type && is_const_value value)
|
43
|
|
44
|
let inject_id_id expr =
|
45
|
let e = mkpredef_call expr.expr_loc inject_id [ expr ] in
|
46
|
{ e with expr_type = Type_predef.type_real; expr_clock = expr.expr_clock }
|
47
|
|
48
|
let pp_inject_real pp_var pp_val fmt (var, value) =
|
49
|
Format.fprintf fmt "%s(%a, %a, %s);" inject_real_id pp_var var pp_val value
|
50
|
(mpfr_rnd ())
|
51
|
|
52
|
let inject_assign expr =
|
53
|
let e = mkpredef_call expr.expr_loc inject_copy_id [ expr ] in
|
54
|
{ e with expr_type = Type_predef.type_real; expr_clock = expr.expr_clock }
|
55
|
|
56
|
let pp_inject_copy pp_var fmt (var, value) =
|
57
|
Format.fprintf fmt "%s(%a, %a, %s);" inject_copy_id pp_var var pp_var value
|
58
|
(mpfr_rnd ())
|
59
|
|
60
|
let pp_inject_assign pp_var fmt ((_, value) as vv) =
|
61
|
if is_const_value value then pp_inject_real pp_var pp_var fmt vv
|
62
|
else pp_inject_copy pp_var fmt vv
|
63
|
|
64
|
let pp_inject_init pp_var fmt var =
|
65
|
Format.fprintf fmt "%s(%a, %i);" inject_init_id pp_var var (mpfr_prec ())
|
66
|
|
67
|
let pp_inject_clear pp_var fmt var =
|
68
|
Format.fprintf fmt "%s(%a);" inject_clear_id pp_var var
|
69
|
|
70
|
let base_inject_op id =
|
71
|
match id with
|
72
|
| "+" ->
|
73
|
"MPFRPlus"
|
74
|
| "-" ->
|
75
|
"MPFRMinus"
|
76
|
| "*" ->
|
77
|
"MPFRTimes"
|
78
|
| "/" ->
|
79
|
"MPFRDiv"
|
80
|
| "uminus" ->
|
81
|
"MPFRUminus"
|
82
|
| "<=" ->
|
83
|
"MPFRLe"
|
84
|
| "<" ->
|
85
|
"MPFRLt"
|
86
|
| ">=" ->
|
87
|
"MPFRGe"
|
88
|
| ">" ->
|
89
|
"MPFRGt"
|
90
|
| "=" ->
|
91
|
"MPFREq"
|
92
|
| "!=" ->
|
93
|
"MPFRNeq"
|
94
|
(* Conv functions *)
|
95
|
| "int_to_real" ->
|
96
|
"MPFRint_to_real"
|
97
|
| "real_to_int" ->
|
98
|
"MPFRreal_to_int"
|
99
|
| "_floor" ->
|
100
|
"MPFRfloor"
|
101
|
| "_ceil" ->
|
102
|
"MPFRceil"
|
103
|
| "_round" ->
|
104
|
"MPFRround"
|
105
|
| "_Floor" ->
|
106
|
"MPFRFloor"
|
107
|
| "_Ceiling" ->
|
108
|
"MPFRCeiling"
|
109
|
| "_Round" ->
|
110
|
"MPFRRound"
|
111
|
(* Math library functions *)
|
112
|
| "acos" ->
|
113
|
"MPFRacos"
|
114
|
| "acosh" ->
|
115
|
"MPFRacosh"
|
116
|
| "asin" ->
|
117
|
"MPFRasin"
|
118
|
| "asinh" ->
|
119
|
"MPFRasinh"
|
120
|
| "atan" ->
|
121
|
"MPFRatan"
|
122
|
| "atan2" ->
|
123
|
"MPFRatan2"
|
124
|
| "atanh" ->
|
125
|
"MPFRatanh"
|
126
|
| "cbrt" ->
|
127
|
"MPFRcbrt"
|
128
|
| "cos" ->
|
129
|
"MPFRcos"
|
130
|
| "cosh" ->
|
131
|
"MPFRcosh"
|
132
|
| "ceil" ->
|
133
|
"MPFRceil"
|
134
|
| "erf" ->
|
135
|
"MPFRerf"
|
136
|
| "exp" ->
|
137
|
"MPFRexp"
|
138
|
| "fabs" ->
|
139
|
"MPFRfabs"
|
140
|
| "floor" ->
|
141
|
"MPFRfloor"
|
142
|
| "fmod" ->
|
143
|
"MPFRfmod"
|
144
|
| "log" ->
|
145
|
"MPFRlog"
|
146
|
| "log10" ->
|
147
|
"MPFRlog10"
|
148
|
| "pow" ->
|
149
|
"MPFRpow"
|
150
|
| "round" ->
|
151
|
"MPFRround"
|
152
|
| "sin" ->
|
153
|
"MPFRsin"
|
154
|
| "sinh" ->
|
155
|
"MPFRsinh"
|
156
|
| "sqrt" ->
|
157
|
"MPFRsqrt"
|
158
|
| "trunc" ->
|
159
|
"MPFRtrunc"
|
160
|
| "tan" ->
|
161
|
"MPFRtan"
|
162
|
| _ ->
|
163
|
raise Not_found
|
164
|
|
165
|
let inject_op id =
|
166
|
report ~level:3 (fun fmt ->
|
167
|
Format.fprintf fmt "trying to inject mpfr into function %s@." id);
|
168
|
try base_inject_op id with Not_found -> id
|
169
|
|
170
|
let homomorphic_funs =
|
171
|
List.fold_right
|
172
|
(fun id res -> try base_inject_op id :: res with Not_found -> res)
|
173
|
Basic_library.internal_funs []
|
174
|
|
175
|
let is_homomorphic_fun id = List.mem id homomorphic_funs
|
176
|
|
177
|
let inject_call expr =
|
178
|
match expr.expr_desc with
|
179
|
| Expr_appl (id, args, None)
|
180
|
when not (Basic_library.is_expr_internal_fun expr) ->
|
181
|
{ expr with expr_desc = Expr_appl (inject_op id, args, None) }
|
182
|
| _ ->
|
183
|
expr
|
184
|
|
185
|
let expr_of_const_array expr =
|
186
|
match expr.expr_desc with
|
187
|
| Expr_const (Const_array cl) ->
|
188
|
let typ = Types.array_element_type expr.expr_type in
|
189
|
let expr_of_const c =
|
190
|
{
|
191
|
expr_desc = Expr_const c;
|
192
|
expr_type = typ;
|
193
|
expr_clock = expr.expr_clock;
|
194
|
expr_loc = expr.expr_loc;
|
195
|
expr_delay = Delay.new_var ();
|
196
|
expr_annot = None;
|
197
|
expr_tag = new_tag ();
|
198
|
}
|
199
|
in
|
200
|
{ expr with expr_desc = Expr_array (List.map expr_of_const cl) }
|
201
|
| _ ->
|
202
|
assert false
|
203
|
|
204
|
(* inject_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) *
|
205
|
normalized <foo> *)
|
206
|
let inject_list alias node inject_element defvars elist =
|
207
|
List.fold_right
|
208
|
(fun t (defvars, qlist) ->
|
209
|
let defvars, norm_t = inject_element alias node defvars t in
|
210
|
defvars, norm_t :: qlist)
|
211
|
elist (defvars, [])
|
212
|
|
213
|
let rec inject_expr ?(alias = true) node defvars expr =
|
214
|
let res =
|
215
|
match expr.expr_desc with
|
216
|
| Expr_const (Const_real _) ->
|
217
|
mk_expr_alias_opt alias node defvars expr
|
218
|
| Expr_const (Const_array _) ->
|
219
|
inject_expr ~alias node defvars (expr_of_const_array expr)
|
220
|
| Expr_const (Const_struct _) ->
|
221
|
assert false
|
222
|
| Expr_ident _ | Expr_const _ ->
|
223
|
defvars, expr
|
224
|
| Expr_array elist ->
|
225
|
let defvars, norm_elist =
|
226
|
inject_list alias node (fun _ -> inject_expr ~alias:true) defvars elist
|
227
|
in
|
228
|
let norm_expr = { expr with expr_desc = Expr_array norm_elist } in
|
229
|
defvars, norm_expr
|
230
|
| Expr_power (e1, d) ->
|
231
|
let defvars, norm_e1 = inject_expr node defvars e1 in
|
232
|
let norm_expr = { expr with expr_desc = Expr_power (norm_e1, d) } in
|
233
|
defvars, norm_expr
|
234
|
| Expr_access (e1, d) ->
|
235
|
let defvars, norm_e1 = inject_expr node defvars e1 in
|
236
|
let norm_expr = { expr with expr_desc = Expr_access (norm_e1, d) } in
|
237
|
defvars, norm_expr
|
238
|
| Expr_tuple elist ->
|
239
|
let defvars, norm_elist =
|
240
|
inject_list alias node (fun alias -> inject_expr ~alias) defvars elist
|
241
|
in
|
242
|
let norm_expr = { expr with expr_desc = Expr_tuple norm_elist } in
|
243
|
defvars, norm_expr
|
244
|
| Expr_appl (id, args, r) ->
|
245
|
let defvars, norm_args = inject_expr node defvars args in
|
246
|
let norm_expr = { expr with expr_desc = Expr_appl (id, norm_args, r) } in
|
247
|
mk_expr_alias_opt alias node defvars (inject_call norm_expr)
|
248
|
| Expr_arrow _ ->
|
249
|
defvars, expr
|
250
|
| Expr_pre e ->
|
251
|
let defvars, norm_e = inject_expr node defvars e in
|
252
|
let norm_expr = { expr with expr_desc = Expr_pre norm_e } in
|
253
|
defvars, norm_expr
|
254
|
| Expr_fby (e1, e2) ->
|
255
|
let defvars, norm_e1 = inject_expr node defvars e1 in
|
256
|
let defvars, norm_e2 = inject_expr node defvars e2 in
|
257
|
let norm_expr = { expr with expr_desc = Expr_fby (norm_e1, norm_e2) } in
|
258
|
defvars, norm_expr
|
259
|
| Expr_when (e, c, l) ->
|
260
|
let defvars, norm_e = inject_expr node defvars e in
|
261
|
let norm_expr = { expr with expr_desc = Expr_when (norm_e, c, l) } in
|
262
|
defvars, norm_expr
|
263
|
| Expr_ite (c, t, e) ->
|
264
|
let defvars, norm_c = inject_expr node defvars c in
|
265
|
let defvars, norm_t = inject_expr node defvars t in
|
266
|
let defvars, norm_e = inject_expr node defvars e in
|
267
|
let norm_expr =
|
268
|
{ expr with expr_desc = Expr_ite (norm_c, norm_t, norm_e) }
|
269
|
in
|
270
|
defvars, norm_expr
|
271
|
| Expr_merge (c, hl) ->
|
272
|
let defvars, norm_hl = inject_branches node defvars hl in
|
273
|
let norm_expr = { expr with expr_desc = Expr_merge (c, norm_hl) } in
|
274
|
defvars, norm_expr
|
275
|
in
|
276
|
(*Format.eprintf "inject_expr %B %a = %a@." alias Printers.pp_expr expr
|
277
|
Printers.pp_expr (snd res);*)
|
278
|
res
|
279
|
|
280
|
and inject_branches node defvars hl =
|
281
|
List.fold_right
|
282
|
(fun (t, h) (defvars, norm_q) ->
|
283
|
let defvars, norm_h = inject_expr node defvars h in
|
284
|
defvars, (t, norm_h) :: norm_q)
|
285
|
hl (defvars, [])
|
286
|
|
287
|
let inject_eq node defvars eq =
|
288
|
let (defs', vars'), norm_rhs =
|
289
|
inject_expr ~alias:false node defvars eq.eq_rhs
|
290
|
in
|
291
|
let norm_eq = { eq with eq_rhs = norm_rhs } in
|
292
|
norm_eq :: defs', vars'
|
293
|
|
294
|
(* let inject_eexpr ee =
|
295
|
* { ee with eexpr_qfexpr = inject_expr ee.eexpr_qfexpr }
|
296
|
*
|
297
|
* let inject_spec s =
|
298
|
* { s with
|
299
|
* assume = List.map inject_eexpr s.assume;
|
300
|
* guarantees = List.map inject_eexpr s.guarantees;
|
301
|
* modes = List.map (fun m ->
|
302
|
* { m with
|
303
|
* require = List.map inject_eexpr m.require;
|
304
|
* ensure = List.map inject_eexpr m.ensure
|
305
|
* }
|
306
|
* ) s.modes
|
307
|
* } *)
|
308
|
|
309
|
(** normalize_node node returns a normalized node, ie. - updated locals - new
|
310
|
equations - *)
|
311
|
let inject_node node =
|
312
|
cpt_fresh := 0;
|
313
|
let inputs_outputs = node.node_inputs @ node.node_outputs in
|
314
|
let norm_ctx = node.node_id, get_node_vars node in
|
315
|
let is_local v = List.for_all (( != ) v) inputs_outputs in
|
316
|
let orig_vars = inputs_outputs @ node.node_locals in
|
317
|
let defs, vars =
|
318
|
let eqs, auts = get_node_eqs node in
|
319
|
if auts != [] then assert false;
|
320
|
(* Automata should be expanded by now. *)
|
321
|
List.fold_left (inject_eq norm_ctx) ([], orig_vars) eqs
|
322
|
in
|
323
|
(* Normalize the asserts *)
|
324
|
let vars, assert_defs, _ =
|
325
|
List.fold_left
|
326
|
(fun (vars, def_accu, assert_accu) assert_ ->
|
327
|
let assert_expr = assert_.assert_expr in
|
328
|
let (defs, vars'), expr =
|
329
|
inject_expr ~alias:false norm_ctx ([], vars)
|
330
|
(* defvar only contains vars *)
|
331
|
assert_expr
|
332
|
in
|
333
|
( vars',
|
334
|
defs @ def_accu,
|
335
|
{ assert_ with assert_expr = expr } :: assert_accu ))
|
336
|
(vars, [], []) node.node_asserts
|
337
|
in
|
338
|
let new_locals = List.filter is_local vars in
|
339
|
(* Compute traceability info: - gather newly bound variables - compute the
|
340
|
associated expression without aliases *)
|
341
|
(* let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals))
|
342
|
new_locals in *)
|
343
|
(* See comment below
|
344
|
* let spec = match node.node_spec with
|
345
|
* | None -> None
|
346
|
* | Some spec -> Some (inject_spec spec)
|
347
|
* in *)
|
348
|
let node =
|
349
|
{
|
350
|
node with
|
351
|
node_locals = new_locals;
|
352
|
node_stmts =
|
353
|
List.map (fun eq -> Eq eq) (defs @ assert_defs)
|
354
|
(* Incomplete work: TODO. Do we have to inject MPFR code here? Does it
|
355
|
make sense for annotations? For me, only if we produce C code for
|
356
|
annotations. Otherwise the various verification backend should have
|
357
|
their own understanding, but would not necessarily require this
|
358
|
additional normalization. *)
|
359
|
(* node_spec = spec; node_annot = List.map (fun ann -> {ann with annots
|
360
|
= List.map (fun (ids, ee) -> ids, inject_eexpr ee) ann.annots} )
|
361
|
node.node_annot *);
|
362
|
}
|
363
|
in
|
364
|
(*Printers.pp_node Format.err_formatter node;*)
|
365
|
node
|
366
|
|
367
|
let inject_decl decl =
|
368
|
match decl.top_decl_desc with
|
369
|
| Node nd ->
|
370
|
{ decl with top_decl_desc = Node (inject_node nd) }
|
371
|
| Include _ | Open _ | ImportedNode _ | Const _ | TypeDef _ ->
|
372
|
decl
|
373
|
|
374
|
let inject_prog decls = List.map inject_decl decls
|
375
|
|
376
|
(* Local Variables: *)
|
377
|
(* compile-command:"make -C .." *)
|
378
|
(* End: *)
|