lustrec / src / plugins / mpfr / lustrec_mpfr.ml @ f0195e96
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 
(* compilecommand:"make C .." *) 
339 
(* End: *) 