1 /* Linearization function implementation.
2 Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
3 Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com)
4
5 This file is part of the Parma Polyhedra Library (PPL).
6
7 The PPL is free software; you can redistribute it and/or modify it
8 under the terms of the GNU General Public License as published by the
9 Free Software Foundation; either version 3 of the License, or (at your
10 option) any later version.
11
12 The PPL is distributed in the hope that it will be useful, but WITHOUT
13 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
14 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
15 for more details.
16
17 You should have received a copy of the GNU General Public License
18 along with this program; if not, write to the Free Software Foundation,
19 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.
20
21 For the most up-to-date information see the Parma Polyhedra Library
22 site: http://bugseng.com/products/ppl/ . */
23
24 #ifndef PPL_linearize_hh
25 #define PPL_linearize_hh 1
26
27 #include "Concrete_Expression_defs.hh"
28 #include "Float_defs.hh"
29 #include "Linear_Form_defs.hh"
30 #include "Box_defs.hh"
31 #include <map>
32
33 namespace Parma_Polyhedra_Library {
34
35 /*! \brief \relates Parma_Polyhedra_Library::Concrete_Expression
36 Helper function used by <CODE>linearize</CODE> to linearize a
37 sum of floating point expressions.
38
39 Makes \p result become the linearization of \p *this in the given
40 composite abstract store.
41
42 \tparam Target
43 A type template parameter specifying the instantiation of
44 Concrete_Expression to be used.
45
46 \tparam FP_Interval_Type
47 A type template parameter for the intervals used in the abstract domain.
48 The interval bounds should have a floating point type.
49
50 \return
51 <CODE>true</CODE> if the linearization succeeded,
52 <CODE>false</CODE> otherwise.
53
54 \param bop_expr
55 The binary operator concrete expression to linearize.
56 Its binary operator type must be <CODE>ADD</CODE>.
57
58 \param oracle
59 The FP_Oracle to be queried.
60
61 \param lf_store
62 The linear form abstract store.
63
64 \param result
65 The modified linear form.
66
67 \par Linearization of sum floating-point expressions
68
69 Let \f$i + \sum_{v \in \cV}i_{v}v \f$ and
70 \f$i' + \sum_{v \in \cV}i'_{v}v \f$
71 be two linear forms and \f$\aslf\f$ a sound abstract operator on linear
72 forms such that:
73
74 \f[
75 \left(i + \sum_{v \in \cV}i_{v}v \right)
76 \aslf
77 \left(i' + \sum_{v \in \cV}i'_{v}v \right)
78 =
79 \left(i \asifp i'\right)
80 + \sum_{v \in \cV}\left(i_{v} \asifp i'_{v} \right)v.
81 \f]
82
83 Given an expression \f$e_{1} \oplus e_{2}\f$ and a composite
84 abstract store \f$\left \llbracket \rho^{\#}, \rho^{\#}_l \right
85 \rrbracket\f$, we construct the interval linear form
86 \f$\linexprenv{e_{1} \oplus e_{2}}{\rho^{\#}}{\rho^{\#}_l}\f$
87 as follows:
88 \f[
89 \linexprenv{e_{1} \oplus e_{2}}{\rho^{\#}}{\rho^{\#}_l}
90 =
91 \linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l}
92 \aslf
93 \linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l}
94 \aslf
95 \varepsilon_{\mathbf{f}}\left(\linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l}
96 \right)
97 \aslf
98 \varepsilon_{\mathbf{f}}\left(\linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l}
99 \right)
100 \aslf
101 mf_{\mathbf{f}}[-1, 1]
102 \f]
103 where \f$\varepsilon_{\mathbf{f}}(l)\f$ is the relative error
104 associated to \f$l\f$ (see method <CODE>relative_error</CODE> of
105 class Linear_Form) and \f$mf_{\mathbf{f}}\f$ is a rounding
106 error computed by function <CODE>compute_absolute_error</CODE>.
107 */
108 template <typename Target, typename FP_Interval_Type>
109 static bool
add_linearize(const Binary_Operator<Target> & bop_expr,const FP_Oracle<Target,FP_Interval_Type> & oracle,const std::map<dimension_type,Linear_Form<FP_Interval_Type>> & lf_store,Linear_Form<FP_Interval_Type> & result)110 add_linearize(const Binary_Operator<Target>& bop_expr,
111 const FP_Oracle<Target,FP_Interval_Type>& oracle,
112 const std::map<dimension_type, Linear_Form<FP_Interval_Type> >&
113 lf_store,
114 Linear_Form<FP_Interval_Type>& result) {
115 PPL_ASSERT(bop_expr.binary_operator() == Binary_Operator<Target>::ADD);
116
117 typedef Linear_Form<FP_Interval_Type> FP_Linear_Form;
118
119 if (!linearize(*(bop_expr.left_hand_side()), oracle, lf_store, result)) {
120 return false;
121 }
122
123 Floating_Point_Format analyzed_format =
124 bop_expr.type().floating_point_format();
125 FP_Linear_Form rel_error;
126 result.relative_error(analyzed_format, rel_error);
127 result += rel_error;
128 FP_Linear_Form linearized_second_operand;
129 if (!linearize(*(bop_expr.right_hand_side()), oracle, lf_store,
130 linearized_second_operand)) {
131 return false;
132 }
133
134 result += linearized_second_operand;
135 linearized_second_operand.relative_error(analyzed_format, rel_error);
136 result += rel_error;
137 FP_Interval_Type absolute_error =
138 compute_absolute_error<FP_Interval_Type>(analyzed_format);
139 result += absolute_error;
140 return !result.overflows();
141 }
142
143 /*! \brief \relates Parma_Polyhedra_Library::Concrete_Expression
144 Helper function used by <CODE>linearize</CODE> to linearize a
145 difference of floating point expressions.
146
147 Makes \p result become the linearization of \p *this in the given
148 composite abstract store.
149
150 \tparam Target
151 A type template parameter specifying the instantiation of
152 Concrete_Expression to be used.
153
154 \tparam FP_Interval_Type
155 A type template parameter for the intervals used in the abstract domain.
156 The interval bounds should have a floating point type.
157
158 \return
159 <CODE>true</CODE> if the linearization succeeded,
160 <CODE>false</CODE> otherwise.
161
162 \param bop_expr
163 The binary operator concrete expression to linearize.
164 Its binary operator type must be <CODE>SUB</CODE>.
165
166 \param oracle
167 The FP_Oracle to be queried.
168
169 \param lf_store
170 The linear form abstract store.
171
172 \param result
173 The modified linear form.
174
175 \par Linearization of difference floating-point expressions
176
177 Let \f$i + \sum_{v \in \cV}i_{v}v \f$ and
178 \f$i' + \sum_{v \in \cV}i'_{v}v \f$
179 be two linear forms, \f$\aslf\f$ and \f$\adlf\f$ two sound abstract
180 operators on linear form such that:
181 \f[
182 \left(i + \sum_{v \in \cV}i_{v}v\right)
183 \aslf
184 \left(i' + \sum_{v \in \cV}i'_{v}v\right)
185 =
186 \left(i \asifp i'\right)
187 + \sum_{v \in \cV}\left(i_{v} \asifp i'_{v}\right)v,
188 \f]
189 \f[
190 \left(i + \sum_{v \in \cV}i_{v}v\right)
191 \adlf
192 \left(i' + \sum_{v \in \cV}i'_{v}v\right)
193 =
194 \left(i \adifp i'\right)
195 + \sum_{v \in \cV}\left(i_{v} \adifp i'_{v}\right)v.
196 \f]
197 Given an expression \f$e_{1} \ominus e_{2}\f$ and a composite
198 abstract store \f$\left \llbracket \rho^{\#}, \rho^{\#}_l \right
199 \rrbracket\f$, we construct the interval linear form
200 \f$\linexprenv{e_{1} \ominus e_{2}}{\rho^{\#}}{\rho^{\#}_l}\f$
201 on \f$\cV\f$ as follows:
202 \f[
203 \linexprenv{e_{1} \ominus e_{2}}{\rho^{\#}}{\rho^{\#}_l}
204 =
205 \linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l}
206 \adlf
207 \linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l}
208 \aslf
209 \varepsilon_{\mathbf{f}}\left(\linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l}
210 \right)
211 \aslf
212 \varepsilon_{\mathbf{f}}\left(\linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l}
213 \right)
214 \aslf
215 mf_{\mathbf{f}}[-1, 1]
216 \f]
217 where \f$\varepsilon_{\mathbf{f}}(l)\f$ is the relative error
218 associated to \f$l\f$ (see method <CODE>relative_error</CODE> of
219 class Linear_Form) and \f$mf_{\mathbf{f}}\f$ is a rounding
220 error computed by function <CODE>compute_absolute_error</CODE>.
221 */
222 template <typename Target, typename FP_Interval_Type>
223 static bool
sub_linearize(const Binary_Operator<Target> & bop_expr,const FP_Oracle<Target,FP_Interval_Type> & oracle,const std::map<dimension_type,Linear_Form<FP_Interval_Type>> & lf_store,Linear_Form<FP_Interval_Type> & result)224 sub_linearize(const Binary_Operator<Target>& bop_expr,
225 const FP_Oracle<Target,FP_Interval_Type>& oracle,
226 const std::map<dimension_type, Linear_Form<FP_Interval_Type> >& lf_store,
227 Linear_Form<FP_Interval_Type>& result) {
228 PPL_ASSERT(bop_expr.binary_operator() == Binary_Operator<Target>::SUB);
229
230 typedef Linear_Form<FP_Interval_Type> FP_Linear_Form;
231
232 if (!linearize(*(bop_expr.left_hand_side()), oracle, lf_store, result)) {
233 return false;
234 }
235
236 Floating_Point_Format analyzed_format =
237 bop_expr.type().floating_point_format();
238 FP_Linear_Form rel_error;
239 result.relative_error(analyzed_format, rel_error);
240 result += rel_error;
241 FP_Linear_Form linearized_second_operand;
242 if (!linearize(*(bop_expr.right_hand_side()), oracle, lf_store,
243 linearized_second_operand)) {
244 return false;
245 }
246
247 result -= linearized_second_operand;
248 linearized_second_operand.relative_error(analyzed_format, rel_error);
249 result += rel_error;
250 FP_Interval_Type absolute_error =
251 compute_absolute_error<FP_Interval_Type>(analyzed_format);
252 result += absolute_error;
253 return !result.overflows();
254 }
255
256 /*! \brief \relates Parma_Polyhedra_Library::Concrete_Expression
257 Helper function used by <CODE>linearize</CODE> to linearize a
258 product of floating point expressions.
259
260 Makes \p result become the linearization of \p *this in the given
261 composite abstract store.
262
263 \tparam Target
264 A type template parameter specifying the instantiation of
265 Concrete_Expression to be used.
266
267 \tparam FP_Interval_Type
268 A type template parameter for the intervals used in the abstract domain.
269 The interval bounds should have a floating point type.
270
271 \return
272 <CODE>true</CODE> if the linearization succeeded,
273 <CODE>false</CODE> otherwise.
274
275 \param bop_expr
276 The binary operator concrete expression to linearize.
277 Its binary operator type must be <CODE>MUL</CODE>.
278
279 \param oracle
280 The FP_Oracle to be queried.
281
282 \param lf_store
283 The linear form abstract store.
284
285 \param result
286 The modified linear form.
287
288 \par Linearization of multiplication floating-point expressions
289
290 Let \f$i + \sum_{v \in \cV}i_{v}v \f$ and
291 \f$i' + \sum_{v \in \cV}i'_{v}v \f$
292 be two linear forms, \f$\aslf\f$ and \f$\amlf\f$ two sound abstract
293 operators on linear forms such that:
294 \f[
295 \left(i + \sum_{v \in \cV}i_{v}v\right)
296 \aslf
297 \left(i' + \sum_{v \in \cV}i'_{v}v\right)
298 =
299 \left(i \asifp i'\right)
300 + \sum_{v \in \cV}\left(i_{v} \asifp i'_{v}\right)v,
301 \f]
302 \f[
303 i
304 \amlf
305 \left(i' + \sum_{v \in \cV}i'_{v}v\right)
306 =
307 \left(i \amifp i'\right)
308 + \sum_{v \in \cV}\left(i \amifp i'_{v}\right)v.
309 \f]
310 Given an expression \f$[a, b] \otimes e_{2}\f$ and a composite
311 abstract store \f$\left \llbracket \rho^{\#}, \rho^{\#}_l \right
312 \rrbracket\f$, we construct the interval linear form
313 \f$\linexprenv{[a, b] \otimes e_{2}}{\rho^{\#}}{\rho^{\#}_l}\f$
314 as follows:
315 \f[
316 \linexprenv{[a, b] \otimes e_{2}}{\rho^{\#}}{\rho^{\#}_l}
317 =
318 \left([a, b]
319 \amlf
320 \linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l}\right)
321 \aslf
322 \left([a, b]
323 \amlf
324 \varepsilon_{\mathbf{f}}\left(\linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l}
325 \right)\right)
326 \aslf
327 mf_{\mathbf{f}}[-1, 1].
328 \f].
329
330 Given an expression \f$e_{1} \otimes [a, b]\f$ and a composite
331 abstract store \f$\left \llbracket \rho^{\#}, \rho^{\#}_l \right
332 \rrbracket\f$, we construct the interval linear form
333 \f$\linexprenv{e_{1} \otimes [a, b]}{\rho^{\#}}{\rho^{\#}_l}\f$
334 as follows:
335 \f[
336 \linexprenv{e_{1} \otimes [a, b]}{\rho^{\#}}{\rho^{\#}_l}
337 =
338 \linexprenv{[a, b] \otimes e_{1}}{\rho^{\#}}{\rho^{\#}_l}.
339 \f]
340
341 Given an expression \f$e_{1} \otimes e_{2}\f$ and a composite
342 abstract store \f$\left \llbracket \rho^{\#}, \rho^{\#}_l \right
343 \rrbracket\f$, we construct the interval linear form
344 \f$\linexprenv{e_{1} \otimes e_{2}}{\rho^{\#}}{\rho^{\#}_l}\f$
345 as follows:
346 \f[
347 \linexprenv{e_{1} \otimes e_{2}}{\rho^{\#}}{\rho^{\#}_l}
348 =
349 \linexprenv{\iota\left(\linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l}
350 \right)\rho^{\#}
351 \otimes e_{2}}{\rho^{\#}}{\rho^{\#}_l},
352 \f]
353 where \f$\varepsilon_{\mathbf{f}}(l)\f$ is the relative error
354 associated to \f$l\f$ (see method <CODE>relative_error</CODE> of
355 class Linear_Form), \f$\iota(l)\rho^{\#}\f$ is the intervalization
356 of \f$l\f$ (see method <CODE>intervalize</CODE> of class Linear_Form),
357 and \f$mf_{\mathbf{f}}\f$ is a rounding error computed by function
358 <CODE>compute_absolute_error</CODE>.
359
360 Even though we intervalize the first operand in the above example, the
361 actual implementation utilizes an heuristics for choosing which of the two
362 operands must be intervalized in order to obtain the most precise result.
363 */
364 template <typename Target, typename FP_Interval_Type>
365 static bool
mul_linearize(const Binary_Operator<Target> & bop_expr,const FP_Oracle<Target,FP_Interval_Type> & oracle,const std::map<dimension_type,Linear_Form<FP_Interval_Type>> & lf_store,Linear_Form<FP_Interval_Type> & result)366 mul_linearize(const Binary_Operator<Target>& bop_expr,
367 const FP_Oracle<Target,FP_Interval_Type>& oracle,
368 const std::map<dimension_type, Linear_Form<FP_Interval_Type> >& lf_store,
369 Linear_Form<FP_Interval_Type>& result) {
370 PPL_ASSERT(bop_expr.binary_operator() == Binary_Operator<Target>::MUL);
371
372 typedef typename FP_Interval_Type::boundary_type analyzer_format;
373 typedef Linear_Form<FP_Interval_Type> FP_Linear_Form;
374
375 /*
376 FIXME: We currently adopt the "Interval-Size Local" strategy in order to
377 decide which of the two linear forms must be intervalized, as described
378 in Section 6.2.4 ("Multiplication Strategies") of Antoine Mine's Ph.D.
379 thesis "Weakly Relational Numerical Abstract Domains".
380 In this Section are also described other multiplication strategies, such
381 as All-Cases, Relative-Size Local, Simplification-Driven Global and
382 Homogeneity Global.
383 */
384
385 // Here we choose which of the two linear forms must be intervalized.
386
387 // true if we intervalize the first form, false if we intervalize the second.
388 bool intervalize_first;
389 FP_Linear_Form linearized_first_operand;
390 if (!linearize(*(bop_expr.left_hand_side()), oracle, lf_store,
391 linearized_first_operand)) {
392 return false;
393 }
394 FP_Interval_Type intervalized_first_operand;
395 if (!linearized_first_operand.intervalize(oracle,
396 intervalized_first_operand)) {
397 return false;
398 }
399 FP_Linear_Form linearized_second_operand;
400 if (!linearize(*(bop_expr.right_hand_side()), oracle, lf_store,
401 linearized_second_operand)) {
402 return false;
403 }
404 FP_Interval_Type intervalized_second_operand;
405 if (!linearized_second_operand.intervalize(oracle,
406 intervalized_second_operand)) {
407 return false;
408 }
409
410 // FIXME: we are not sure that what we do here is policy-proof.
411 if (intervalized_first_operand.is_bounded()) {
412 if (intervalized_second_operand.is_bounded()) {
413 analyzer_format first_interval_size
414 = intervalized_first_operand.upper()
415 - intervalized_first_operand.lower();
416 analyzer_format second_interval_size
417 = intervalized_second_operand.upper()
418 - intervalized_second_operand.lower();
419 if (first_interval_size <= second_interval_size) {
420 intervalize_first = true;
421 }
422 else {
423 intervalize_first = false;
424 }
425 }
426 else {
427 intervalize_first = true;
428 }
429 }
430 else {
431 if (intervalized_second_operand.is_bounded()) {
432 intervalize_first = false;
433 }
434 else {
435 return false;
436 }
437 }
438
439 // Here we do the actual computation.
440 // For optimizing, we store the relative error directly into result.
441 Floating_Point_Format analyzed_format =
442 bop_expr.type().floating_point_format();
443 if (intervalize_first) {
444 linearized_second_operand.relative_error(analyzed_format, result);
445 linearized_second_operand *= intervalized_first_operand;
446 result *= intervalized_first_operand;
447 result += linearized_second_operand;
448 }
449 else {
450 linearized_first_operand.relative_error(analyzed_format, result);
451 linearized_first_operand *= intervalized_second_operand;
452 result *= intervalized_second_operand;
453 result += linearized_first_operand;
454 }
455
456 FP_Interval_Type absolute_error =
457 compute_absolute_error<FP_Interval_Type>(analyzed_format);
458 result += absolute_error;
459 return !result.overflows();
460 }
461
462 /*! \brief \relates Parma_Polyhedra_Library::Concrete_Expression
463 Helper function used by <CODE>linearize</CODE> to linearize a
464 division of floating point expressions.
465
466 Makes \p result become the linearization of \p *this in the given
467 composite abstract store.
468
469 \tparam Target
470 A type template parameter specifying the instantiation of
471 Concrete_Expression to be used.
472
473 \tparam FP_Interval_Type
474 A type template parameter for the intervals used in the abstract domain.
475 The interval bounds should have a floating point type.
476
477 \return
478 <CODE>true</CODE> if the linearization succeeded,
479 <CODE>false</CODE> otherwise.
480
481 \param bop_expr
482 The binary operator concrete expression to linearize.
483 Its binary operator type must be <CODE>DIV</CODE>.
484
485 \param oracle
486 The FP_Oracle to be queried.
487
488 \param lf_store
489 The linear form abstract store.
490
491 \param result
492 The modified linear form.
493
494 \par Linearization of division floating-point expressions
495
496 Let \f$i + \sum_{v \in \cV}i_{v}v \f$ and
497 \f$i' + \sum_{v \in \cV}i'_{v}v \f$
498 be two linear forms, \f$\aslf\f$ and \f$\adivlf\f$ two sound abstract
499 operator on linear forms such that:
500 \f[
501 \left(i + \sum_{v \in \cV}i_{v}v\right)
502 \aslf
503 \left(i' + \sum_{v \in \cV}i'_{v}v\right)
504 =
505 \left(i \asifp i'\right)
506 + \sum_{v \in \cV}\left(i_{v} \asifp i'_{v}\right)v,
507 \f]
508 \f[
509 \left(i + \sum_{v \in \cV}i_{v}v\right)
510 \adivlf
511 i'
512 =
513 \left(i \adivifp i'\right)
514 + \sum_{v \in \cV}\left(i_{v} \adivifp i'\right)v.
515 \f]
516 Given an expression \f$e_{1} \oslash [a, b]\f$ and a composite
517 abstract store \f$\left \llbracket \rho^{\#}, \rho^{\#}_l \right
518 \rrbracket\f$,
519 we construct the interval linear form
520 \f$
521 \linexprenv{e_{1} \oslash [a, b]}{\rho^{\#}}{\rho^{\#}_l}
522 \f$
523 as follows:
524 \f[
525 \linexprenv{e_{1} \oslash [a, b]}{\rho^{\#}}{\rho^{\#}_l}
526 =
527 \left(\linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l}
528 \adivlf
529 [a, b]\right)
530 \aslf
531 \left(\varepsilon_{\mathbf{f}}\left(
532 \linexprenv{e_{1}}{\rho^{\#}}{\rho^{\#}_l}
533 \right)
534 \adivlf
535 [a, b]\right)
536 \aslf
537 mf_{\mathbf{f}}[-1, 1],
538 \f]
539 given an expression \f$e_{1} \oslash e_{2}\f$ and a composite
540 abstract store \f$\left \llbracket \rho^{\#}, \rho^{\#}_l \right
541 \rrbracket\f$, we construct the interval linear form
542 \f$\linexprenv{e_{1} \oslash e_{2}}{\rho^{\#}}{\rho^{\#}_l}\f$
543 as follows:
544 \f[
545 \linexprenv{e_{1} \oslash e_{2}}{\rho^{\#}}{\rho^{\#}_l}
546 =
547 \linexprenv{e_{1} \oslash \iota\left(
548 \linexprenv{e_{2}}{\rho^{\#}}{\rho^{\#}_l}
549 \right)\rho^{\#}}{\rho^{\#}}{\rho^{\#}_l},
550 \f]
551 where \f$\varepsilon_{\mathbf{f}}(l)\f$ is the relative error
552 associated to \f$l\f$ (see method <CODE>relative_error</CODE> of
553 class Linear_Form), \f$\iota(l)\rho^{\#}\f$ is the intervalization
554 of \f$l\f$ (see method <CODE>intervalize</CODE> of class Linear_Form),
555 and \f$mf_{\mathbf{f}}\f$ is a rounding error computed by function
556 <CODE>compute_absolute_error</CODE>.
557 */
558 template <typename Target, typename FP_Interval_Type>
559 static bool
div_linearize(const Binary_Operator<Target> & bop_expr,const FP_Oracle<Target,FP_Interval_Type> & oracle,const std::map<dimension_type,Linear_Form<FP_Interval_Type>> & lf_store,Linear_Form<FP_Interval_Type> & result)560 div_linearize(const Binary_Operator<Target>& bop_expr,
561 const FP_Oracle<Target,FP_Interval_Type>& oracle,
562 const std::map<dimension_type, Linear_Form<FP_Interval_Type> >& lf_store,
563 Linear_Form<FP_Interval_Type>& result) {
564 PPL_ASSERT(bop_expr.binary_operator() == Binary_Operator<Target>::DIV);
565
566 typedef Linear_Form<FP_Interval_Type> FP_Linear_Form;
567
568 FP_Linear_Form linearized_second_operand;
569 if (!linearize(*(bop_expr.right_hand_side()), oracle, lf_store,
570 linearized_second_operand)) {
571 return false;
572 }
573 FP_Interval_Type intervalized_second_operand;
574 if (!linearized_second_operand.intervalize(oracle,
575 intervalized_second_operand)) {
576 return false;
577 }
578 // Check if we may divide by zero.
579 if ((intervalized_second_operand.lower_is_boundary_infinity()
580 || intervalized_second_operand.lower() <= 0) &&
581 (intervalized_second_operand.upper_is_boundary_infinity()
582 || intervalized_second_operand.upper() >= 0)) {
583 return false;
584 }
585 if (!linearize(*(bop_expr.left_hand_side()), oracle, lf_store, result)) {
586 return false;
587 }
588
589 Floating_Point_Format analyzed_format =
590 bop_expr.type().floating_point_format();
591 FP_Linear_Form rel_error;
592 result.relative_error(analyzed_format, rel_error);
593 result /= intervalized_second_operand;
594 rel_error /= intervalized_second_operand;
595 result += rel_error;
596 FP_Interval_Type absolute_error =
597 compute_absolute_error<FP_Interval_Type>(analyzed_format);
598 result += absolute_error;
599 return !result.overflows();
600 }
601
602 /*! \brief \relates Parma_Polyhedra_Library::Concrete_Expression
603 Helper function used by <CODE>linearize</CODE> to linearize a cast
604 floating point expression.
605
606 Makes \p result become the linearization of \p *this in the given
607 composite abstract store.
608
609 \tparam Target
610 A type template parameter specifying the instantiation of
611 Concrete_Expression to be used.
612
613 \tparam FP_Interval_Type
614 A type template parameter for the intervals used in the abstract domain.
615 The interval bounds should have a floating point type.
616
617 \return
618 <CODE>true</CODE> if the linearization succeeded,
619 <CODE>false</CODE> otherwise.
620
621 \param cast_expr
622 The cast operator concrete expression to linearize.
623
624 \param oracle
625 The FP_Oracle to be queried.
626
627 \param lf_store
628 The linear form abstract store.
629
630 \param result
631 The modified linear form.
632 */
633 template <typename Target, typename FP_Interval_Type>
634 static bool
cast_linearize(const Cast_Operator<Target> & cast_expr,const FP_Oracle<Target,FP_Interval_Type> & oracle,const std::map<dimension_type,Linear_Form<FP_Interval_Type>> & lf_store,Linear_Form<FP_Interval_Type> & result)635 cast_linearize(const Cast_Operator<Target>& cast_expr,
636 const FP_Oracle<Target,FP_Interval_Type>& oracle,
637 const std::map<dimension_type, Linear_Form<FP_Interval_Type> >& lf_store,
638 Linear_Form<FP_Interval_Type>& result) {
639 typedef typename FP_Interval_Type::boundary_type analyzer_format;
640 typedef Linear_Form<FP_Interval_Type> FP_Linear_Form;
641
642 Floating_Point_Format analyzed_format =
643 cast_expr.type().floating_point_format();
644 const Concrete_Expression<Target>* cast_arg = cast_expr.argument();
645 if (cast_arg->type().is_floating_point()) {
646 if (!linearize(*cast_arg, oracle, lf_store, result)) {
647 return false;
648 }
649 if (!is_less_precise_than(analyzed_format,
650 cast_arg->type().floating_point_format())
651 || result == FP_Linear_Form(FP_Interval_Type(0))
652 || result == FP_Linear_Form(FP_Interval_Type(1))) {
653 /*
654 FIXME: find a general way to check if the casted constant
655 is exactly representable in the less precise format.
656 */
657 /*
658 We are casting to a more precise format or casting
659 a definitely safe value: do not add errors.
660 */
661 return true;
662 }
663 }
664 else {
665 FP_Interval_Type expr_value;
666 if (!oracle.get_integer_expr_value(*cast_arg, expr_value))
667 return false;
668 result = FP_Linear_Form(expr_value);
669 if (is_less_precise_than(Float<analyzer_format>::Binary::floating_point_format, analyzed_format)
670 || result == FP_Linear_Form(FP_Interval_Type(0))
671 || result == FP_Linear_Form(FP_Interval_Type(1))) {
672 /*
673 FIXME: find a general way to check if the casted constant
674 is exactly representable in the less precise format.
675 */
676 /*
677 We are casting to a more precise format or casting
678 a definitely safe value: do not add errors.
679 */
680 return true;
681 }
682 }
683
684 FP_Linear_Form rel_error;
685 result.relative_error(analyzed_format, rel_error);
686 result += rel_error;
687 FP_Interval_Type absolute_error =
688 compute_absolute_error<FP_Interval_Type>(analyzed_format);
689 result += absolute_error;
690 return !result.overflows();
691 }
692
693 //! Linearizes a floating point expression.
694 /*! \relates Parma_Polyhedra_Library::Concrete_Expression
695 Makes \p result become a linear form that correctly approximates the
696 value of \p expr in the given composite abstract store.
697
698 \tparam Target
699 A type template parameter specifying the instantiation of
700 Concrete_Expression to be used.
701
702 \tparam FP_Interval_Type
703 A type template parameter for the intervals used in the abstract domain.
704 The interval bounds should have a floating point type.
705
706 \return
707 <CODE>true</CODE> if the linearization succeeded,
708 <CODE>false</CODE> otherwise.
709
710 \param expr
711 The concrete expression to linearize.
712
713 \param oracle
714 The FP_Oracle to be queried.
715
716 \param lf_store
717 The linear form abstract store.
718
719 \param result
720 Becomes the linearized expression.
721
722 Formally, if \p expr represents the expression \f$e\f$ and
723 \p lf_store represents the linear form abstract store \f$\rho^{\#}_l\f$,
724 then \p result will become \f$\linexprenv{e}{\rho^{\#}}{\rho^{\#}_l}\f$
725 if the linearization succeeds.
726 */
727 template <typename Target, typename FP_Interval_Type>
728 bool
linearize(const Concrete_Expression<Target> & expr,const FP_Oracle<Target,FP_Interval_Type> & oracle,const std::map<dimension_type,Linear_Form<FP_Interval_Type>> & lf_store,Linear_Form<FP_Interval_Type> & result)729 linearize(const Concrete_Expression<Target>& expr,
730 const FP_Oracle<Target,FP_Interval_Type>& oracle,
731 const std::map<dimension_type, Linear_Form<FP_Interval_Type> >& lf_store,
732 Linear_Form<FP_Interval_Type>& result) {
733 typedef typename FP_Interval_Type::boundary_type analyzer_format;
734 typedef Linear_Form<FP_Interval_Type> FP_Linear_Form;
735 typedef std::map<dimension_type, FP_Linear_Form>
736 FP_Linear_Form_Abstract_Store;
737
738 PPL_ASSERT(expr.type().is_floating_point());
739 // Check that analyzer_format is a floating point type.
740 PPL_COMPILE_TIME_CHECK(!std::numeric_limits<analyzer_format>::is_exact,
741 "linearize<Target, FP_Interval_Type>:"
742 " FP_Interval_Type is not the type of an interval with floating point boundaries.");
743
744 switch(expr.kind()) {
745 case Integer_Constant<Target>::KIND:
746 PPL_UNREACHABLE;
747 break;
748 case Floating_Point_Constant<Target>::KIND:
749 {
750 const Floating_Point_Constant<Target>* fpc_expr =
751 expr.template as<Floating_Point_Constant>();
752 FP_Interval_Type constant_value;
753 if (!oracle.get_fp_constant_value(*fpc_expr, constant_value)) {
754 return false;
755 }
756 result = FP_Linear_Form(constant_value);
757 return true;
758 }
759 case Unary_Operator<Target>::KIND:
760 {
761 const Unary_Operator<Target>* uop_expr =
762 expr.template as<Unary_Operator>();
763 switch (uop_expr->unary_operator()) {
764 case Unary_Operator<Target>::UPLUS:
765 return linearize(*(uop_expr->argument()), oracle, lf_store, result);
766 case Unary_Operator<Target>::UMINUS:
767 if (!linearize(*(uop_expr->argument()), oracle, lf_store, result)) {
768 return false;
769 }
770
771 result.negate();
772 return true;
773 case Unary_Operator<Target>::BNOT:
774 throw std::runtime_error("PPL internal error: unimplemented");
775 break;
776 default:
777 PPL_UNREACHABLE;
778 break;
779 }
780 break;
781 }
782 case Binary_Operator<Target>::KIND:
783 {
784 const Binary_Operator<Target>* bop_expr =
785 expr.template as<Binary_Operator>();
786 switch (bop_expr->binary_operator()) {
787 case Binary_Operator<Target>::ADD:
788 return add_linearize(*bop_expr, oracle, lf_store, result);
789 case Binary_Operator<Target>::SUB:
790 return sub_linearize(*bop_expr, oracle, lf_store, result);
791 case Binary_Operator<Target>::MUL:
792 return mul_linearize(*bop_expr, oracle, lf_store, result);
793 case Binary_Operator<Target>::DIV:
794 return div_linearize(*bop_expr, oracle, lf_store, result);
795 case Binary_Operator<Target>::REM:
796 case Binary_Operator<Target>::BAND:
797 case Binary_Operator<Target>::BOR:
798 case Binary_Operator<Target>::BXOR:
799 case Binary_Operator<Target>::LSHIFT:
800 case Binary_Operator<Target>::RSHIFT:
801 // FIXME: can we do better?
802 return false;
803 default:
804 PPL_UNREACHABLE;
805 return false;
806 }
807 break;
808 }
809 case Approximable_Reference<Target>::KIND:
810 {
811 const Approximable_Reference<Target>* ref_expr =
812 expr.template as<Approximable_Reference>();
813 std::set<dimension_type> associated_dimensions;
814 if (!oracle.get_associated_dimensions(*ref_expr, associated_dimensions)
815 || associated_dimensions.empty()) {
816 /*
817 We were unable to find any associated space dimension:
818 linearization fails.
819 */
820 return false;
821 }
822
823 if (associated_dimensions.size() == 1) {
824 /* If a linear form associated to the only referenced
825 space dimension exists in lf_store, return that form.
826 Otherwise, return the simplest linear form. */
827 dimension_type variable_index = *associated_dimensions.begin();
828 PPL_ASSERT(variable_index != not_a_dimension());
829
830 typename FP_Linear_Form_Abstract_Store::const_iterator
831 variable_value = lf_store.find(variable_index);
832 if (variable_value == lf_store.end()) {
833 result = FP_Linear_Form(Variable(variable_index));
834 return true;
835 }
836
837 result = FP_Linear_Form(variable_value->second);
838 /* FIXME: do we really need to contemplate the possibility
839 that an unbounded linear form was saved into lf_store? */
840 return !result.overflows();
841 }
842
843 /*
844 Here associated_dimensions.size() > 1. Try to return the LUB
845 of all intervals associated to each space dimension.
846 */
847 PPL_ASSERT(associated_dimensions.size() > 1);
848 std::set<dimension_type>::const_iterator i
849 = associated_dimensions.begin();
850 std::set<dimension_type>::const_iterator i_end
851 = associated_dimensions.end();
852 FP_Interval_Type lub(EMPTY);
853 for (; i != i_end; ++i) {
854 FP_Interval_Type curr_int;
855 PPL_ASSERT(*i != not_a_dimension());
856 if (!oracle.get_interval(*i, curr_int)) {
857 return false;
858 }
859
860 lub.join_assign(curr_int);
861 }
862
863 result = FP_Linear_Form(lub);
864 return !result.overflows();
865 }
866 case Cast_Operator<Target>::KIND:
867 {
868 const Cast_Operator<Target>* cast_expr =
869 expr.template as<Cast_Operator>();
870 return cast_linearize(*cast_expr, oracle, lf_store, result);
871 }
872 default:
873 PPL_UNREACHABLE;
874 break;
875 }
876
877 PPL_UNREACHABLE;
878 return false;
879 }
880
881 } // namespace Parma_Polyhedra_Library
882
883 #endif // !defined(PPL_linearize_hh)
884