Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/plugins/mpfr/lustrec_mpfr.ml | ||
---|---|---|
17 | 17 |
open Machine_code_common |
18 | 18 |
|
19 | 19 |
let report = Log.report ~plugin:"MPFR" |
20 |
|
|
21 |
let mpfr_module = mktop (Open(false, "mpfr_lustre")) |
|
20 |
|
|
21 |
let mpfr_module = mktop (Open (false, "mpfr_lustre")) |
|
22 |
|
|
22 | 23 |
let cpt_fresh = ref 0 |
23 |
|
|
24 |
|
|
24 | 25 |
let mpfr_rnd () = "MPFR_RNDN" |
25 | 26 |
|
26 | 27 |
let mpfr_prec () = !Options.mpfr_prec |
... | ... | |
41 | 42 |
not (Types.is_real_type value.value_type && is_const_value value) |
42 | 43 |
|
43 | 44 |
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 |
} |
|
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 } |
|
49 | 47 |
|
50 | 48 |
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 |
|
49 |
Format.fprintf fmt "%s(%a, %a, %s);" inject_real_id pp_var var pp_val value |
|
55 | 50 |
(mpfr_rnd ()) |
56 | 51 |
|
57 | 52 |
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 |
} |
|
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 } |
|
63 | 55 |
|
64 | 56 |
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 |
|
57 |
Format.fprintf fmt "%s(%a, %a, %s);" inject_copy_id pp_var var pp_var value |
|
69 | 58 |
(mpfr_rnd ()) |
70 | 59 |
|
71 |
let pp_inject_assign pp_var fmt (_, value as vv) = |
|
72 |
if is_const_value value |
|
73 |
then |
|
74 |
pp_inject_real pp_var pp_var fmt vv |
|
75 |
else |
|
76 |
pp_inject_copy pp_var fmt vv |
|
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 |
|
77 | 63 |
|
78 | 64 |
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 ()) |
|
65 |
Format.fprintf fmt "%s(%a, %i);" inject_init_id pp_var var (mpfr_prec ()) |
|
83 | 66 |
|
84 | 67 |
let pp_inject_clear pp_var fmt var = |
85 |
Format.fprintf fmt "%s(%a);" |
|
86 |
inject_clear_id |
|
87 |
pp_var var |
|
68 |
Format.fprintf fmt "%s(%a);" inject_clear_id pp_var var |
|
88 | 69 |
|
89 | 70 |
let base_inject_op id = |
90 | 71 |
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" |
|
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" |
|
102 | 94 |
(* 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 |
|
|
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" |
|
112 | 111 |
(* 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 |
|
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 |
|
139 | 164 |
|
140 | 165 |
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 |
|
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 |
|
145 | 169 |
|
146 | 170 |
let homomorphic_funs = |
147 |
List.fold_right (fun id res -> try base_inject_op id :: res with Not_found -> res) Basic_library.internal_funs [] |
|
171 |
List.fold_right |
|
172 |
(fun id res -> try base_inject_op id :: res with Not_found -> res) |
|
173 |
Basic_library.internal_funs [] |
|
148 | 174 |
|
149 |
let is_homomorphic_fun id = |
|
150 |
List.mem id homomorphic_funs |
|
175 |
let is_homomorphic_fun id = List.mem id homomorphic_funs |
|
151 | 176 |
|
152 | 177 |
let inject_call expr = |
153 | 178 |
match expr.expr_desc with |
154 |
| Expr_appl (id, args, None) when not (Basic_library.is_expr_internal_fun expr) -> |
|
179 |
| Expr_appl (id, args, None) |
|
180 |
when not (Basic_library.is_expr_internal_fun expr) -> |
|
155 | 181 |
{ expr with expr_desc = Expr_appl (inject_op id, args, None) } |
156 |
| _ -> expr |
|
182 |
| _ -> |
|
183 |
expr |
|
157 | 184 |
|
158 | 185 |
let expr_of_const_array expr = |
159 | 186 |
match expr.expr_desc with |
160 | 187 |
| Expr_const (Const_array cl) -> |
161 | 188 |
let typ = Types.array_element_type expr.expr_type in |
162 | 189 |
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 (); |
|
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 (); |
|
170 | 198 |
} |
171 |
in { expr with expr_desc = Expr_array (List.map expr_of_const cl) } |
|
172 |
| _ -> assert false |
|
199 |
in |
|
200 |
{ expr with expr_desc = Expr_array (List.map expr_of_const cl) } |
|
201 |
| _ -> |
|
202 |
assert false |
|
173 | 203 |
|
174 |
(* inject_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *) |
|
204 |
(* inject_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * |
|
205 |
normalized <foo> *) |
|
175 | 206 |
let inject_list alias node inject_element defvars elist = |
176 | 207 |
List.fold_right |
177 | 208 |
(fun t (defvars, qlist) -> |
178 | 209 |
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 |
|
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 |
|
238 | 279 |
|
239 | 280 |
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 |
|
|
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, []) |
|
247 | 286 |
|
248 | 287 |
let inject_eq node defvars eq = |
249 |
let (defs', vars'), norm_rhs = inject_expr ~alias:false node defvars eq.eq_rhs in |
|
288 |
let (defs', vars'), norm_rhs = |
|
289 |
inject_expr ~alias:false node defvars eq.eq_rhs |
|
290 |
in |
|
250 | 291 |
let norm_eq = { eq with eq_rhs = norm_rhs } in |
251 |
norm_eq::defs', vars'
|
|
292 |
norm_eq :: defs', vars'
|
|
252 | 293 |
|
253 | 294 |
(* let inject_eexpr ee = |
254 | 295 |
* { ee with eexpr_qfexpr = inject_expr ee.eexpr_qfexpr } |
... | ... | |
264 | 305 |
* } |
265 | 306 |
* ) s.modes |
266 | 307 |
* } *) |
267 |
|
|
268 |
(** normalize_node node returns a normalized node, |
|
269 |
ie. |
|
270 |
- updated locals |
|
271 |
- new equations |
|
272 |
- |
|
273 |
*) |
|
274 |
let inject_node node = |
|
308 |
|
|
309 |
(** normalize_node node returns a normalized node, ie. - updated locals - new |
|
310 |
equations - *) |
|
311 |
let inject_node node = |
|
275 | 312 |
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 |
|
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 |
|
281 | 317 |
let defs, vars = |
282 | 318 |
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 |
|
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 |
|
285 | 323 |
(* Normalize the asserts *) |
286 | 324 |
let vars, assert_defs, _ = |
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 |
|
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 |
|
299 | 338 |
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 *) |
|
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 *) |
|
305 | 343 |
(* See comment below |
306 | 344 |
* let spec = match node.node_spec with |
307 | 345 |
* | None -> None |
308 | 346 |
* | Some spec -> Some (inject_spec spec) |
309 | 347 |
* in *) |
310 | 348 |
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) |
|
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 |
|
326 | 366 |
|
327 | 367 |
let inject_decl decl = |
328 | 368 |
match decl.top_decl_desc with |
329 | 369 |
| 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 |
|
370 |
{ decl with top_decl_desc = Node (inject_node nd) } |
|
371 |
| Include _ | Open _ | ImportedNode _ | Const _ | TypeDef _ -> |
|
372 |
decl |
|
335 | 373 |
|
374 |
let inject_prog decls = List.map inject_decl decls |
|
336 | 375 |
|
337 | 376 |
(* Local Variables: *) |
338 | 377 |
(* compile-command:"make -C .." *) |
Also available in: Unified diff
reformatting