1 /* Testing linearization algorithm ad its related functions.
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 #include "ppl_test.hh"
25 #include "C_Expr_defs.hh"
26
27 namespace {
28
29 class Test_Oracle : public FP_Oracle<C_Expr,FP_Interval> {
30 public:
Test_Oracle()31 Test_Oracle() : int_store(0) {}
32
Test_Oracle(FP_Interval_Abstract_Store init)33 Test_Oracle(FP_Interval_Abstract_Store init) : int_store(init) {}
34
get_interval(dimension_type dim,FP_Interval & result) const35 bool get_interval(dimension_type dim, FP_Interval& result) const {
36 result = int_store.get_interval(Variable(dim));
37 return true;
38 }
39
get_fp_constant_value(const Floating_Point_Constant<C_Expr> & expr,FP_Interval & result) const40 bool get_fp_constant_value(const Floating_Point_Constant<C_Expr>& expr,
41 FP_Interval& result) const {
42 result = FP_Interval((const char *)expr.value);
43 return true;
44 }
45
get_integer_expr_value(const Concrete_Expression<C_Expr> & expr,FP_Interval & result) const46 bool get_integer_expr_value(const Concrete_Expression<C_Expr>& expr,
47 FP_Interval& result) const {
48 if (expr.kind() == INT_CON) {
49 const Integer_Constant<C_Expr>* ic_expr =
50 reinterpret_cast< const Integer_Constant<C_Expr>* >(&expr);
51 result = FP_Interval(ic_expr->value);
52 }
53 else {
54 const Approximable_Reference<C_Expr>* ar_expr =
55 reinterpret_cast< const Approximable_Reference<C_Expr>* >(&expr);
56 result = FP_Interval(ar_expr->value);
57 }
58
59 return true;
60 }
61
get_associated_dimensions(const Approximable_Reference<C_Expr> & expr,std::set<dimension_type> & result) const62 bool get_associated_dimensions(
63 const Approximable_Reference<C_Expr>& expr,
64 std::set<dimension_type>& result) const {
65 result = expr.dimensions;
66 return true;
67 }
68
69 FP_Interval_Abstract_Store int_store;
70 };
71
72 using namespace Parma_Polyhedra_Library::IO_Operators;
73 Concrete_Expression_Type FP_Type =
74 Concrete_Expression_Type::floating_point(ANALYZED_FP_FORMAT);
75
76 typedef Integer_Interval Int_Interval;
77
78 // Tests division by zero.
79 bool
test01()80 test01() {
81 Floating_Point_Constant<C_Expr> num("3", 2);
82 Floating_Point_Constant<C_Expr> den("0", 2);
83 Binary_Operator<C_Expr> div(FP_Type, Binary_Operator<C_Expr>::DIV, &num, &den);
84 FP_Linear_Form result;
85 if (!linearize(div, Test_Oracle(), FP_Linear_Form_Abstract_Store(),
86 result)) {
87 nout << "*** Linearization failed due to division by zero. ***" << endl;
88 return true;
89 }
90 return false;
91 }
92
93 // Tests multiplication by zero.
94 bool
test02()95 test02() {
96 Test_Oracle oracle(FP_Interval_Abstract_Store(2));
97 oracle.int_store.set_interval(Variable(0), FP_Interval(0));
98 oracle.int_store.set_interval(Variable(1), FP_Interval(10));
99 Floating_Point_Constant<C_Expr> con("5.5", 4);
100 Approximable_Reference<C_Expr> var0(FP_Type, Int_Interval(mpz_class(0)), 0);
101 Approximable_Reference<C_Expr> var1(FP_Type, Int_Interval(mpz_class(0)), 1);
102 Binary_Operator<C_Expr> dif(FP_Type, Binary_Operator<C_Expr>::SUB, &var1, &con);
103 Binary_Operator<C_Expr> mul(FP_Type, Binary_Operator<C_Expr>::MUL, &dif, &var0);
104 FP_Linear_Form result;
105 if (!linearize(mul, oracle, FP_Linear_Form_Abstract_Store(), result))
106 return false;
107
108 FP_Linear_Form known_result(compute_absolute_error<FP_Interval>(ANALYZED_FP_FORMAT));
109
110 nout << "*** result ***" << endl
111 << result << endl;
112 nout << "*** known_result ***" << endl
113 << known_result << endl;
114 bool ok = (result == known_result);
115
116 return ok;
117 }
118
119 // Tests linearization of variables in a given linear form abstract store.
120 bool
test03()121 test03() {
122 FP_Linear_Form_Abstract_Store store;
123 Variable A(0);
124 FP_Linear_Form known_result = FP_Linear_Form(A);
125 store[0] = known_result;
126 Approximable_Reference<C_Expr> var(FP_Type, Int_Interval(mpz_class(0)), 0);
127 FP_Linear_Form result;
128 linearize(var, Test_Oracle(), store, result);
129
130 nout << "*** known_result ***" << endl
131 << known_result << endl;
132 bool ok = (result == known_result);
133
134 return ok;
135 }
136
137 // Tests linearization of A + B.
138 bool
test04()139 test04() {
140 FP_Interval tmp(0);
141 Test_Oracle oracle(FP_Interval_Abstract_Store(2));
142 oracle.int_store.set_interval(Variable(0), tmp);
143 oracle.int_store.set_interval(Variable(1), tmp);
144 Approximable_Reference<C_Expr> var0(FP_Type, Int_Interval(mpz_class(0)), 0);
145 Approximable_Reference<C_Expr> var1(FP_Type, Int_Interval(mpz_class(0)), 1);
146 Binary_Operator<C_Expr> sum(FP_Type, Binary_Operator<C_Expr>::ADD,
147 &var0, &var1);
148 FP_Linear_Form result;
149 linearize(sum, oracle, FP_Linear_Form_Abstract_Store(), result);
150
151 Variable A(0);
152 Variable B(1);
153 FP_Linear_Form known_result = FP_Linear_Form(A);
154 FP_Linear_Form rel_err1;
155 known_result.relative_error(ANALYZED_FP_FORMAT, rel_err1);
156 known_result += rel_err1;
157 FP_Linear_Form lb = FP_Linear_Form(B);
158 known_result += lb;
159 FP_Linear_Form rel_err2;
160 lb.relative_error(ANALYZED_FP_FORMAT, rel_err2);
161 known_result += rel_err2;
162 known_result += compute_absolute_error<FP_Interval>(ANALYZED_FP_FORMAT);
163
164 bool ok = result == known_result;
165
166 return ok;
167 }
168
169 // Tests the linearization of A - B.
170 bool
test05()171 test05() {
172 FP_Interval tmp(0);
173 Test_Oracle oracle(FP_Interval_Abstract_Store(2));
174 oracle.int_store.set_interval(Variable(0), tmp);
175 oracle.int_store.set_interval(Variable(1), tmp);
176 Approximable_Reference<C_Expr> var0(FP_Type, Int_Interval(mpz_class(0)), 0);
177 Approximable_Reference<C_Expr> var1(FP_Type, Int_Interval(mpz_class(0)), 1);
178 Binary_Operator<C_Expr> dif(FP_Type, Binary_Operator<C_Expr>::SUB,
179 &var0, &var1);
180 FP_Linear_Form result;
181 linearize(dif, oracle, FP_Linear_Form_Abstract_Store(), result);
182
183 Variable A(0);
184 Variable B(1);
185 FP_Linear_Form known_result = FP_Linear_Form(A);
186 FP_Linear_Form rel_err1;
187 known_result.relative_error(ANALYZED_FP_FORMAT, rel_err1);
188 known_result += rel_err1;
189 FP_Linear_Form lb = FP_Linear_Form(B);
190 lb.negate();
191 known_result += lb;
192 FP_Linear_Form rel_err2;
193 lb.relative_error(ANALYZED_FP_FORMAT, rel_err2);
194 known_result += rel_err2;
195 known_result += compute_absolute_error<FP_Interval>(ANALYZED_FP_FORMAT);
196
197 bool ok = result == known_result;
198
199 return ok;
200 }
201
202 // Tests linearization of A * B where A in [0, 1] and B in [2, 2].
203 bool
test06()204 test06() {
205 FP_Interval tmp(0);
206 tmp.join_assign(1);
207 Test_Oracle oracle(FP_Interval_Abstract_Store(2));
208 oracle.int_store.set_interval(Variable(0), tmp);
209 oracle.int_store.set_interval(Variable(1), FP_Interval(2));
210 Approximable_Reference<C_Expr> var0(FP_Type, Int_Interval(mpz_class(0)), 0);
211 Approximable_Reference<C_Expr> var1(FP_Type, Int_Interval(mpz_class(0)), 1);
212 Binary_Operator<C_Expr> mul(FP_Type, Binary_Operator<C_Expr>::MUL,
213 &var0, &var1);
214 FP_Linear_Form result;
215 linearize(mul, oracle, FP_Linear_Form_Abstract_Store(), result);
216
217 Variable A(0);
218 FP_Interval coeff = FP_Interval(2);
219 FP_Linear_Form known_result = FP_Linear_Form(A);
220 FP_Linear_Form rel_err;
221 known_result.relative_error(ANALYZED_FP_FORMAT, rel_err);
222 known_result *= coeff;
223 known_result += coeff * rel_err;
224 known_result += compute_absolute_error<FP_Interval>(ANALYZED_FP_FORMAT);
225
226 bool ok = (result == known_result);
227
228 return ok;
229 }
230
231 // Tests the linearization of A / B where A = [0, 1] and B = [2, 2].
232 bool
test07()233 test07() {
234 FP_Interval tmp(0);
235 tmp.join_assign(1);
236 Test_Oracle oracle(FP_Interval_Abstract_Store(2));
237 oracle.int_store.set_interval(Variable(0), tmp);
238 oracle.int_store.set_interval(Variable(1), FP_Interval(2));
239 Approximable_Reference<C_Expr> var0(FP_Type, Int_Interval(mpz_class(0)), 0);
240 Approximable_Reference<C_Expr> var1(FP_Type, Int_Interval(mpz_class(0)), 1);
241 Binary_Operator<C_Expr> div(FP_Type, Binary_Operator<C_Expr>::DIV,
242 &var0, &var1);
243 FP_Linear_Form result;
244 linearize(div, oracle, FP_Linear_Form_Abstract_Store(), result);
245
246 Variable A(0);
247 FP_Interval coeff(FP_Interval::boundary_type(1 / 2.0));
248 FP_Linear_Form known_result(A);
249 FP_Linear_Form rel_err;
250 known_result.relative_error(ANALYZED_FP_FORMAT, rel_err);
251 known_result *= coeff;
252 known_result += rel_err * coeff;
253 known_result += compute_absolute_error<FP_Interval>(ANALYZED_FP_FORMAT);
254
255 bool ok = (result == known_result);
256
257 return ok;
258 }
259
260 // Tests linearization of cast expressions.
261 bool
test08()262 test08() {
263 Int_Interval i(mpz_class(123456789));
264 Integer_Constant<C_Expr> ic_expr(Concrete_Expression_Type::bounded_integer(BITS_32, UNSIGNED, OVERFLOW_WRAPS), i);
265 Cast_Operator<C_Expr> cast(FP_Type, &ic_expr);
266 FP_Linear_Form result;
267 linearize(cast, Test_Oracle(),
268 FP_Linear_Form_Abstract_Store(), result);
269
270 Int_Interval approx(mpz_class(123456700));
271 approx.join_assign(mpz_class(123456850));
272 bool ok1 = approx.contains(result.inhomogeneous_term());
273
274 Approximable_Reference<C_Expr> var(Concrete_Expression_Type::bounded_integer(BITS_32, UNSIGNED, OVERFLOW_WRAPS), i, 0);
275 Cast_Operator<C_Expr> cast2(FP_Type, &var);
276 linearize(cast2, Test_Oracle(), FP_Linear_Form_Abstract_Store(), result);
277
278 bool ok2 = approx.contains(result.inhomogeneous_term());
279
280 return ok1 && ok2;
281 }
282
283 /*
284 Tests linearization of an approximable reference having more than
285 one associated index.
286 */
287 bool
test09()288 test09() {
289 Test_Oracle oracle(FP_Interval_Abstract_Store(4));
290 oracle.int_store.set_interval(Variable(0), FP_Interval(0));
291 oracle.int_store.set_interval(Variable(1), FP_Interval(10));
292 oracle.int_store.set_interval(Variable(2), FP_Interval(20));
293 oracle.int_store.set_interval(Variable(3), FP_Interval(5));
294 Approximable_Reference<C_Expr> ref(FP_Type, Int_Interval(mpz_class(0)), 0);
295 ref.dimensions.insert(1);
296 ref.dimensions.insert(3);
297 FP_Linear_Form result;
298 if (!linearize(ref, oracle, FP_Linear_Form_Abstract_Store(), result))
299 return false;
300
301 FP_Interval known_int(FP_Interval(0));
302 known_int.join_assign(FP_Interval(10));
303 FP_Linear_Form known_result(known_int);
304
305 nout << "*** result ***" << endl
306 << result << endl;
307 nout << "*** known_result ***" << endl
308 << known_result << endl;
309 bool ok = (result == known_result);
310
311 return ok;
312 }
313
314 } // namespace
315
316 BEGIN_MAIN
317 DO_TEST(test01);
318 DO_TEST(test02);
319 DO_TEST(test03);
320 DO_TEST(test04);
321 DO_TEST(test05);
322 DO_TEST(test06);
323 DO_TEST(test07);
324 DO_TEST(test08);
325 DO_TEST(test09);
326 END_MAIN
327