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