lustrec / src / mpfr.ml @ 7db425aa
History | View | Annotate | Download (8.43 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 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 pp_val fmt var value = |
47 |
Format.fprintf fmt "%s(%a, %a, %s);" |
48 |
inject_real_id |
49 |
pp_var var |
50 |
pp_val 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 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: *) |