cprover
Loading...
Searching...
No Matches
string_constraint_generator_float.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Generates string constraints for functions generating strings
4 from other types, in particular int, long, float, double, char, bool
5
6Author: Romain Brenguier, romain.brenguier@diffblue.com
7
8\*******************************************************************/
9
13
15
16#include <util/bitvector_expr.h>
17#include <util/floatbv_expr.h>
18#include <util/ieee_float.h>
20
29exprt get_exponent(const exprt &src, const ieee_float_spect &spec)
30{
32 src, spec.f + spec.e - 1, spec.f, unsignedbv_typet(spec.e));
33
34 // Exponent is in biased form (numbers from -128 to 127 are encoded with
35 // integer from 0 to 255) we have to remove the bias.
36 return minus_exprt(
38 from_integer(spec.bias(), signedbv_typet(32)));
39}
40
45exprt get_fraction(const exprt &src, const ieee_float_spect &spec)
46{
47 return extractbits_exprt(src, spec.f - 1, 0, unsignedbv_typet(spec.f));
48}
49
61 const exprt &src,
62 const ieee_float_spect &spec,
63 const typet &type)
64{
65 PRECONDITION(type.id() == ID_unsignedbv);
66 PRECONDITION(to_unsignedbv_type(type).get_width() > spec.f);
67 typecast_exprt fraction(get_fraction(src, spec), type);
68 exprt exponent = get_exponent(src, spec);
69 equal_exprt all_zeros(exponent, from_integer(0, exponent.type()));
70 exprt hidden_bit = from_integer((1 << spec.f), type);
72 return if_exprt(all_zeros, fraction, with_hidden_bit);
73}
74
80{
83 fl.from_float(f);
85 fl.from_double(f);
86 else
88 return fl.to_expr();
89}
90
100
106exprt floatbv_mult(const exprt &f, const exprt &g)
107{
108 PRECONDITION(f.type() == g.type());
110 exprt mult(ID_floatbv_mult, f.type());
111 mult.copy_to_operands(f);
112 mult.copy_to_operands(g);
114 return mult;
115}
116
129
143{
145 constant_float(0.30102999566398119521373889472449302, spec);
146 exprt bin_exp = get_exponent(f, spec);
150 // Rounding to zero is not correct for negative numbers, so we substract 1.
154}
155
161std::pair<exprt, string_constraintst>
169
173std::pair<exprt, string_constraintst>
179
192std::pair<exprt, string_constraintst>
194 const array_string_exprt &res,
195 const exprt &f)
196{
197 const floatbv_typet &type = to_floatbv_type(f.type());
198 const ieee_float_spect float_spec(type);
199 const typet &char_type = to_type_with_subtype(res.content().type()).subtype();
200 const typet &index_type = res.length_type();
201
202 // We will look at the first 5 digits of the fractional part.
203 // shifted is floor(f * 1e5)
206 // Numbers with greater or equal value to the following, should use
207 // the exponent notation.
208 const exprt max_non_exponent_notation = from_integer(100000, shifted.type());
209 // fractional_part is floor(f * 100000) % 100000
213 auto result1 =
215
216 // The axiom added to convert to integer should always be satisfiable even
217 // when the preconditions are not satisfied.
220 // We should not need more than 8 characters to represent the integer
221 // part of the float.
224 auto result2 =
226
227 auto result3 =
229 merge(result3.second, std::move(result1.second));
230 merge(result3.second, std::move(result2.second));
231
232 const auto return_code =
233 maximum(result1.first, maximum(result2.first, result3.first));
234 return {return_code, std::move(result3.second)};
235}
236
244std::pair<exprt, string_constraintst>
246 const array_string_exprt &res,
247 const exprt &int_expr,
248 size_t max_size)
249{
250 PRECONDITION(int_expr.type().id() == ID_signedbv);
252 string_constraintst constraints;
253 const typet &type = int_expr.type();
254 const typet &char_type = to_type_with_subtype(res.content().type()).subtype();
255 const typet &index_type = res.length_type();
256 const exprt ten = from_integer(10, type);
260
261 // We add axioms:
262 // a1 : 2 <= |res| <= max_size
263 // a2 : starts_with_dot && no_trailing_zero && is_number
264 // starts_with_dot: res[0] = '.'
265 // is_number: forall i:[1, max_size[. '0' < res[i] < '9'
266 // no_trailing_zero: forall j:[2, max_size[. !(|res| = j+1 && res[j] = '0')
267 // a3 : int_expr = sum_j 10^j (j < |res| ? res[j] - '0' : 0)
268
269 const and_exprt a1(
272 constraints.existential.push_back(a1);
273
275
278 exprt sum = from_integer(0, type);
279
280 for(size_t j = 1; j < max_size; j++)
281 {
282 // after_end is |res| <= j
285 ID_le,
286 from_integer(j, res.length_type()));
288
289 // sum = 10 * sum + after_end ? 0 : (res[j]-'0')
291 after_end,
292 from_integer(0, type),
295
299 digit_constraints.push_back(is_number);
300
301 // There are no trailing zeros except for ".0" (i.e j=2)
302 if(j > 1)
303 {
307 from_integer(j + 1, res.length_type())),
310 }
311 }
312
314 constraints.existential.push_back(a2);
315
317 constraints.existential.push_back(a3);
318
319 return {from_integer(0, signedbv_typet(32)), std::move(constraints)};
320}
321
337std::pair<exprt, string_constraintst>
339 const array_string_exprt &res,
340 const exprt &float_expr)
341{
342 string_constraintst constraints;
344 const typet float_type = float_spec.to_type();
345 const signedbv_typet int_type(32);
346 const typet &index_type = res.length_type();
347 const typet &char_type = to_type_with_subtype(res.content().type()).subtype();
348
349 // This is used for rounding float to integers.
351
352 // `bin_exponent` is $e$ in the formulas
354
355 // $m$ from the formula is a value between 0.0 and 2.0 represented
356 // with values in the range 0x000000 0xFFFFFF so 1 corresponds to 0x800000.
357 // `bin_significand_int` represents $m * 0x800000$
360 // `bin_significand` represents $m$ and is obtained
361 // by multiplying `binary_significand_as_int` by
362 // 1/0x800000 = 2^-23 = 1.1920928955078125 * 10^-7
365 constant_float(1.1920928955078125e-7, float_spec));
366
367 // This is a first approximation of the exponent that will adjust
368 // if the fraction we get is greater than 10
371
372 // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[0,128]
373 std::vector<double> two_power_e_over_ten_power_d_table(
374 {1, 2, 4, 8, 1.6, 3.2, 6.4, 1.28,
375 2.56, 5.12, 1.024, 2.048, 4.096, 8.192, 1.6384, 3.2768,
376 6.5536, 1.31072, 2.62144, 5.24288, 1.04858, 2.09715, 4.19430, 8.38861,
377 1.67772, 3.35544, 6.71089, 1.34218, 2.68435, 5.36871, 1.07374, 2.14748,
378 4.29497, 8.58993, 1.71799, 3.43597, 6.87195, 1.37439, 2.74878, 5.49756,
379 1.09951, 2.19902, 4.39805, 8.79609, 1.75922, 3.51844, 7.03687, 1.40737,
380 2.81475, 5.62950, 1.12590, 2.25180, 4.50360, 9.00720, 1.80144, 3.60288,
381 7.20576, 1.44115, 2.88230, 5.76461, 1.15292, 2.30584, 4.61169, 9.22337,
382 1.84467, 3.68935, 7.37870, 1.47574, 2.95148, 5.90296, 1.18059, 2.36118,
383 4.72237, 9.44473, 1.88895, 3.77789, 7.55579, 1.51116, 3.02231, 6.04463,
384 1.20893, 2.41785, 4.83570, 9.67141, 1.93428, 3.86856, 7.73713, 1.54743,
385 3.09485, 6.18970, 1.23794, 2.47588, 4.95176, 9.90352, 1.98070, 3.96141,
386 7.92282, 1.58456, 3.16913, 6.33825, 1.26765, 2.53530, 5.07060, 1.01412,
387 2.02824, 4.05648, 8.11296, 1.62259, 3.24519, 6.49037, 1.29807, 2.59615,
388 5.1923, 1.03846, 2.07692, 4.15384, 8.30767, 1.66153, 3.32307, 6.64614,
389 1.32923, 2.65846, 5.31691, 1.06338, 2.12676, 4.25353, 8.50706, 1.70141});
390
391 // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[-128,-1]
393 {2.93874, 5.87747, 1.17549, 2.35099, 4.70198, 9.40395, 1.88079, 3.76158,
394 7.52316, 1.50463, 3.00927, 6.01853, 1.20371, 2.40741, 4.81482, 9.62965,
395 1.92593, 3.85186, 7.70372, 1.54074, 3.08149, 6.16298, 1.23260, 2.46519,
396 4.93038, 9.86076, 1.97215, 3.94430, 7.88861, 1.57772, 3.15544, 6.31089,
397 1.26218, 2.52435, 5.04871, 1.00974, 2.01948, 4.03897, 8.07794, 1.61559,
398 3.23117, 6.46235, 1.29247, 2.58494, 5.16988, 1.03398, 2.06795, 4.13590,
399 8.27181, 1.65436, 3.30872, 6.61744, 1.32349, 2.64698, 5.29396, 1.05879,
400 2.11758, 4.23516, 8.47033, 1.69407, 3.38813, 6.77626, 1.35525, 2.71051,
401 5.42101, 1.08420, 2.16840, 4.33681, 8.67362, 1.73472, 3.46945, 6.93889,
402 1.38778, 2.77556, 5.55112, 1.11022, 2.22045, 4.44089, 8.88178, 1.77636,
403 3.55271, 7.10543, 1.42109, 2.84217, 5.68434, 1.13687, 2.27374, 4.54747,
404 9.09495, 1.81899, 3.63798, 7.27596, 1.45519, 2.91038, 5.82077, 1.16415,
405 2.32831, 4.65661, 9.31323, 1.86265, 3.72529, 7.45058, 1.49012, 2.98023,
406 5.96046, 1.19209, 2.38419, 4.76837, 9.53674, 1.90735, 3.81470, 7.62939,
407 1.52588, 3.05176, 6.10352, 1.22070, 2.44141, 4.88281, 9.76563, 1.95313,
408 3.90625, 7.81250, 1.56250, 3.12500, 6.25000, 1.25000, 2.50000, 5});
409
410 // bias_table used to find the bias factor
414 int_type);
418 conversion_factor_table.copy_to_operands(
421 conversion_factor_table.copy_to_operands(
423
424 // The index in the table, corresponding to exponent e is e+128
426
427 // bias_factor is $2^e / 10^(floor(log_10(2)*e))$ that is $2^e/10^d$
430
431 // `dec_significand` is $n = m * bias_factor$
434
435 // `dec_exponent` is $d$ in the formulas
436 // it is obtained from the approximation, checking whether it is not too small
443
444 // `dec_significand` is divided by 10 if it exceeds 10
456
457 // shifted_float is floor(float_expr * 1e5)
461
462 // Numbers with greater or equal value to the following, should use
463 // the exponent notation.
465
466 // fractional_part_shifted is floor(float_expr * 100000) % 100000
469
474
475 // string_expr_with_fractional_part =
476 // concat(string_with_do, string_fractional_part)
483
484 // string_expr_with_E = concat(string_fraction, string_lit_E)
492
493 // exponent_string = string_of_int(decimal_exponent)
496 auto result6 =
498
499 // string_expr = concat(string_expr_with_E, exponent_string)
500 auto result7 =
502
503 const exprt return_code = maximum(
504 result1.first,
505 maximum(
506 result2.first,
507 maximum(
508 result3.first,
509 maximum(
510 result4.first,
511 maximum(result5.first, maximum(result6.first, result7.first))))));
512 merge(result7.second, std::move(result1.second));
513 merge(result7.second, std::move(result2.second));
514 merge(result7.second, std::move(result3.second));
515 merge(result7.second, std::move(result4.second));
516 merge(result7.second, std::move(result5.second));
517 merge(result7.second, std::move(result6.second));
518 return {return_code, std::move(result7.second)};
519}
520
527std::pair<exprt, string_constraintst>
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
API to expression classes for bitvectors.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
floatbv_typet float_type()
Definition c_types.cpp:182
bitvector_typet index_type()
Definition c_types.cpp:22
bitvector_typet char_type()
Definition c_types.cpp:111
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Boolean AND.
Definition std_expr.h:2071
Array constructor from list of elements.
Definition std_expr.h:1563
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
Construct a string expression whose length and content are new variables.
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
Arrays with given size.
Definition std_types.h:763
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:707
Bit-wise OR.
Equality.
Definition std_expr.h:1306
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition expr.h:155
typet & type()
Return the type of the expression.
Definition expr.h:84
Extracts a sub-range of a bit-vector operand.
Semantic type conversion from/to floating-point formats.
Fixed-width bit-vector with IEEE floating-point interpretation.
Application of (mathematical) function.
static ieee_float_spect single_precision()
Definition ieee_float.h:70
class floatbv_typet to_type() const
mp_integer bias() const
static ieee_float_spect double_precision()
Definition ieee_float.h:76
std::size_t f
Definition ieee_float.h:26
std::size_t e
Definition ieee_float.h:26
The trinary if-then-else operator.
Definition std_expr.h:2323
Array index operator.
Definition std_expr.h:1410
const irep_idt & id() const
Definition irep.h:396
Binary minus.
Definition std_expr.h:1006
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1168
Binary multiplication Associativity is not specified.
Definition std_expr.h:1052
Boolean negation.
Definition std_expr.h:2278
The plus expression Associativity is not specified.
Definition std_expr.h:947
Fixed-width bit-vector with two's complement interpretation.
std::pair< exprt, string_constraintst > add_axioms_from_double(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(D) java function.
std::pair< exprt, string_constraintst > add_axioms_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that res is equal to the concatenation of s1 and s2.
std::pair< exprt, string_constraintst > add_axioms_for_fractional_part(const array_string_exprt &res, const exprt &int_expr, size_t max_size)
Add axioms for representing the fractional part of a floating point starting with a dot.
std::pair< exprt, string_constraintst > add_axioms_for_string_of_int(const array_string_exprt &res, const exprt &input_int, size_t max_size)
Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String....
std::pair< exprt, string_constraintst > add_axioms_from_float_scientific_notation(const array_string_exprt &res, const exprt &f)
Add axioms to write the float in scientific notation.
std::pair< exprt, string_constraintst > add_axioms_for_string_of_float(const function_application_exprt &f)
String representation of a float value.
std::pair< exprt, string_constraintst > add_axioms_for_constant(const array_string_exprt &res, irep_idt sval, const exprt &guard=true_exprt())
Add axioms ensuring that the provided string expression and constant are equal.
Semantic type conversion.
Definition std_expr.h:2017
The type of an expression, extends irept.
Definition type.h:29
Fixed-width bit-vector with unsigned binary interpretation.
API to expression classes for floating-point arithmetic.
API to expression classes for 'mathematical' expressions.
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:63
Generates string constraints to link results from string functions with their arguments.
exprt maximum(const exprt &a, const exprt &b)
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
exprt floatbv_of_int_expr(const exprt &i, const ieee_float_spect &spec)
Convert integers to floating point to be used in operations with other values that are in floating po...
exprt floatbv_mult(const exprt &f, const exprt &g)
Multiplication of expressions representing floating points.
exprt get_significand(const exprt &src, const ieee_float_spect &spec, const typet &type)
Gets the significand as a java integer, looking for the hidden bit.
exprt estimate_decimal_exponent(const exprt &f, const ieee_float_spect &spec)
Estimate the decimal exponent that should be used to represent a given floating point value in decima...
exprt get_exponent(const exprt &src, const ieee_float_spect &spec)
Gets the unbiased exponent in a floating-point bit-vector.
exprt constant_float(const double f, const ieee_float_spect &float_spec)
Create an expression to represent a float or double value.
exprt round_expr_to_zero(const exprt &f)
Round a float expression to an integer closer to 0.
exprt get_fraction(const exprt &src, const ieee_float_spect &spec)
Gets the fraction without hidden bit.
binary_relation_exprt less_than_or_equal_to(exprt lhs, exprt rhs)
Definition string_expr.h:37
binary_relation_exprt greater_than(exprt lhs, exprt rhs)
Definition string_expr.h:26
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< exprt > existential
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:175