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 
(* compilecommand:"make C .." *) 
265 
(* End: *) 