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{
31 const extractbits_exprt exp_bits(src, spec.f, unsignedbv_typet(spec.e));
32
33 // Exponent is in biased form (numbers from -128 to 127 are encoded with
34 // integer from 0 to 255) we have to remove the bias.
35 return minus_exprt(
36 typecast_exprt(exp_bits, signedbv_typet(32)),
37 from_integer(spec.bias(), signedbv_typet(32)));
38}
39
44exprt get_fraction(const exprt &src, const ieee_float_spect &spec)
45{
46 return extractbits_exprt(src, 0, unsignedbv_typet(spec.f));
47}
48
60 const exprt &src,
61 const ieee_float_spect &spec,
62 const typet &type)
63{
64 PRECONDITION(type.id() == ID_unsignedbv);
65 PRECONDITION(to_unsignedbv_type(type).get_width() > spec.f);
66 typecast_exprt fraction(get_fraction(src, spec), type);
67 exprt exponent = get_exponent(src, spec);
68 equal_exprt all_zeros(exponent, from_integer(0, exponent.type()));
69 exprt hidden_bit = from_integer((1 << spec.f), type);
70 bitor_exprt with_hidden_bit(fraction, hidden_bit);
71 return if_exprt(all_zeros, fraction, with_hidden_bit);
72}
73
78exprt constant_float(const double f, const ieee_float_spect &float_spec)
79{
80 ieee_floatt fl(float_spec);
81 if(float_spec == ieee_float_spect::single_precision())
82 fl.from_float(f);
83 else if(float_spec == ieee_float_spect::double_precision())
84 fl.from_double(f);
85 else
87 return fl.to_expr();
88}
89
99
105exprt floatbv_mult(const exprt &f, const exprt &g)
106{
107 PRECONDITION(f.type() == g.type());
109 exprt mult(ID_floatbv_mult, f.type());
110 mult.copy_to_operands(f);
111 mult.copy_to_operands(g);
113 return mult;
114}
115
123{
124 exprt rounding =
126 return floatbv_typecast_exprt(i, rounding, spec.to_type());
127}
128
142{
143 exprt log_10_of_2 =
144 constant_float(0.30102999566398119521373889472449302, spec);
145 exprt bin_exp = get_exponent(f, spec);
146 exprt float_bin_exp = floatbv_of_int_expr(bin_exp, spec);
147 exprt dec_exp = floatbv_mult(float_bin_exp, log_10_of_2);
148 binary_relation_exprt negative_exp(dec_exp, ID_lt, constant_float(0.0, spec));
149 // Rounding to zero is not correct for negative numbers, so we substract 1.
150 minus_exprt dec_minus_one(dec_exp, constant_float(1.0, spec));
151 if_exprt adjust_for_neg(negative_exp, dec_minus_one, dec_exp);
152 return round_expr_to_zero(adjust_for_neg);
153}
154
160std::pair<exprt, string_constraintst>
168
172std::pair<exprt, string_constraintst>
178
191std::pair<exprt, string_constraintst>
193 const array_string_exprt &res,
194 const exprt &f)
195{
196 const floatbv_typet &type = to_floatbv_type(f.type());
197 const ieee_float_spect float_spec(type);
199 const typet &index_type = res.length_type();
200
201 // We will look at the first 5 digits of the fractional part.
202 // shifted is floor(f * 1e5)
203 const exprt shifting = constant_float(1e5, float_spec);
204 const exprt shifted = round_expr_to_zero(floatbv_mult(f, shifting));
205 // Numbers with greater or equal value to the following, should use
206 // the exponent notation.
207 const exprt max_non_exponent_notation = from_integer(100000, shifted.type());
208 // fractional_part is floor(f * 100000) % 100000
209 const mod_exprt fractional_part(shifted, max_non_exponent_notation);
210 const array_string_exprt fractional_part_str =
211 array_pool.fresh_string(index_type, char_type);
212 auto result1 =
213 add_axioms_for_fractional_part(fractional_part_str, fractional_part, 6);
214
215 // The axiom added to convert to integer should always be satisfiable even
216 // when the preconditions are not satisfied.
217 const mod_exprt integer_part(
218 round_expr_to_zero(f), max_non_exponent_notation);
219 // We should not need more than 8 characters to represent the integer
220 // part of the float.
221 const array_string_exprt integer_part_str =
222 array_pool.fresh_string(index_type, char_type);
223 auto result2 =
224 add_axioms_for_string_of_int(integer_part_str, integer_part, 8);
225
226 auto result3 =
227 add_axioms_for_concat(res, integer_part_str, fractional_part_str);
228 merge(result3.second, std::move(result1.second));
229 merge(result3.second, std::move(result2.second));
230
231 const auto return_code =
232 maximum(result1.first, maximum(result2.first, result3.first));
233 return {return_code, std::move(result3.second)};
234}
235
243std::pair<exprt, string_constraintst>
245 const array_string_exprt &res,
246 const exprt &int_expr,
247 size_t max_size)
248{
249 PRECONDITION(int_expr.type().id() == ID_signedbv);
250 PRECONDITION(max_size >= 2);
251 string_constraintst constraints;
252 const typet &type = int_expr.type();
254 const typet &index_type = res.length_type();
255 const exprt ten = from_integer(10, type);
256 const exprt zero_char = from_integer('0', char_type);
257 const exprt nine_char = from_integer('9', char_type);
258 const exprt max = from_integer(max_size, index_type);
259
260 // We add axioms:
261 // a1 : 2 <= |res| <= max_size
262 // a2 : starts_with_dot && no_trailing_zero && is_number
263 // starts_with_dot: res[0] = '.'
264 // is_number: forall i:[1, max_size[. '0' < res[i] < '9'
265 // no_trailing_zero: forall j:[2, max_size[. !(|res| = j+1 && res[j] = '0')
266 // a3 : int_expr = sum_j 10^j (j < |res| ? res[j] - '0' : 0)
267
268 const and_exprt a1(
271 constraints.existential.push_back(a1);
272
273 equal_exprt starts_with_dot(res[0], from_integer('.', char_type));
274
275 exprt::operandst digit_constraints;
276 digit_constraints.push_back(starts_with_dot);
277 exprt sum = from_integer(0, type);
278
279 for(size_t j = 1; j < max_size; j++)
280 {
281 // after_end is |res| <= j
282 binary_relation_exprt after_end(
284 ID_le,
285 from_integer(j, res.length_type()));
286 mult_exprt ten_sum(sum, ten);
287
288 // sum = 10 * sum + after_end ? 0 : (res[j]-'0')
289 if_exprt to_add(
290 after_end,
291 from_integer(0, type),
292 typecast_exprt(minus_exprt(res[j], zero_char), type));
293 sum = plus_exprt(ten_sum, to_add);
294
296 binary_relation_exprt(res[j], ID_ge, zero_char),
297 binary_relation_exprt(res[j], ID_le, nine_char));
298 digit_constraints.push_back(is_number);
299
300 // There are no trailing zeros except for ".0" (i.e j=2)
301 if(j > 1)
302 {
303 not_exprt no_trailing_zero(and_exprt(
306 from_integer(j + 1, res.length_type())),
307 equal_exprt(res[j], zero_char)));
308 digit_constraints.push_back(no_trailing_zero);
309 }
310 }
311
312 exprt a2 = conjunction(digit_constraints);
313 constraints.existential.push_back(a2);
314
315 equal_exprt a3(int_expr, sum);
316 constraints.existential.push_back(a3);
317
318 return {from_integer(0, signedbv_typet(32)), std::move(constraints)};
319}
320
336std::pair<exprt, string_constraintst>
338 const array_string_exprt &res,
339 const exprt &float_expr)
340{
341 string_constraintst constraints;
343 const typet float_type = float_spec.to_type();
344 const signedbv_typet int_type(32);
345 const typet &index_type = res.length_type();
347
348 // This is used for rounding float to integers.
349 exprt round_to_zero_expr = from_integer(ieee_floatt::ROUND_TO_ZERO, int_type);
350
351 // `bin_exponent` is $e$ in the formulas
352 exprt bin_exponent = get_exponent(float_expr, float_spec);
353
354 // $m$ from the formula is a value between 0.0 and 2.0 represented
355 // with values in the range 0x000000 0xFFFFFF so 1 corresponds to 0x800000.
356 // `bin_significand_int` represents $m * 0x800000$
357 exprt bin_significand_int =
358 get_significand(float_expr, float_spec, unsignedbv_typet(32));
359 // `bin_significand` represents $m$ and is obtained
360 // by multiplying `binary_significand_as_int` by
361 // 1/0x800000 = 2^-23 = 1.1920928955078125 * 10^-7
362 exprt bin_significand = floatbv_mult(
363 floatbv_typecast_exprt(bin_significand_int, round_to_zero_expr, float_type),
364 constant_float(1.1920928955078125e-7, float_spec));
365
366 // This is a first approximation of the exponent that will adjust
367 // if the fraction we get is greater than 10
368 exprt dec_exponent_estimate =
369 estimate_decimal_exponent(float_expr, float_spec);
370
371 // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[0,128]
372 std::vector<double> two_power_e_over_ten_power_d_table(
373 {1, 2, 4, 8, 1.6, 3.2, 6.4, 1.28,
374 2.56, 5.12, 1.024, 2.048, 4.096, 8.192, 1.6384, 3.2768,
375 6.5536, 1.31072, 2.62144, 5.24288, 1.04858, 2.09715, 4.19430, 8.38861,
376 1.67772, 3.35544, 6.71089, 1.34218, 2.68435, 5.36871, 1.07374, 2.14748,
377 4.29497, 8.58993, 1.71799, 3.43597, 6.87195, 1.37439, 2.74878, 5.49756,
378 1.09951, 2.19902, 4.39805, 8.79609, 1.75922, 3.51844, 7.03687, 1.40737,
379 2.81475, 5.62950, 1.12590, 2.25180, 4.50360, 9.00720, 1.80144, 3.60288,
380 7.20576, 1.44115, 2.88230, 5.76461, 1.15292, 2.30584, 4.61169, 9.22337,
381 1.84467, 3.68935, 7.37870, 1.47574, 2.95148, 5.90296, 1.18059, 2.36118,
382 4.72237, 9.44473, 1.88895, 3.77789, 7.55579, 1.51116, 3.02231, 6.04463,
383 1.20893, 2.41785, 4.83570, 9.67141, 1.93428, 3.86856, 7.73713, 1.54743,
384 3.09485, 6.18970, 1.23794, 2.47588, 4.95176, 9.90352, 1.98070, 3.96141,
385 7.92282, 1.58456, 3.16913, 6.33825, 1.26765, 2.53530, 5.07060, 1.01412,
386 2.02824, 4.05648, 8.11296, 1.62259, 3.24519, 6.49037, 1.29807, 2.59615,
387 5.1923, 1.03846, 2.07692, 4.15384, 8.30767, 1.66153, 3.32307, 6.64614,
388 1.32923, 2.65846, 5.31691, 1.06338, 2.12676, 4.25353, 8.50706, 1.70141});
389
390 // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[-128,-1]
391 std::vector<double> two_power_e_over_ten_power_d_table_negatives(
392 {2.93874, 5.87747, 1.17549, 2.35099, 4.70198, 9.40395, 1.88079, 3.76158,
393 7.52316, 1.50463, 3.00927, 6.01853, 1.20371, 2.40741, 4.81482, 9.62965,
394 1.92593, 3.85186, 7.70372, 1.54074, 3.08149, 6.16298, 1.23260, 2.46519,
395 4.93038, 9.86076, 1.97215, 3.94430, 7.88861, 1.57772, 3.15544, 6.31089,
396 1.26218, 2.52435, 5.04871, 1.00974, 2.01948, 4.03897, 8.07794, 1.61559,
397 3.23117, 6.46235, 1.29247, 2.58494, 5.16988, 1.03398, 2.06795, 4.13590,
398 8.27181, 1.65436, 3.30872, 6.61744, 1.32349, 2.64698, 5.29396, 1.05879,
399 2.11758, 4.23516, 8.47033, 1.69407, 3.38813, 6.77626, 1.35525, 2.71051,
400 5.42101, 1.08420, 2.16840, 4.33681, 8.67362, 1.73472, 3.46945, 6.93889,
401 1.38778, 2.77556, 5.55112, 1.11022, 2.22045, 4.44089, 8.88178, 1.77636,
402 3.55271, 7.10543, 1.42109, 2.84217, 5.68434, 1.13687, 2.27374, 4.54747,
403 9.09495, 1.81899, 3.63798, 7.27596, 1.45519, 2.91038, 5.82077, 1.16415,
404 2.32831, 4.65661, 9.31323, 1.86265, 3.72529, 7.45058, 1.49012, 2.98023,
405 5.96046, 1.19209, 2.38419, 4.76837, 9.53674, 1.90735, 3.81470, 7.62939,
406 1.52588, 3.05176, 6.10352, 1.22070, 2.44141, 4.88281, 9.76563, 1.95313,
407 3.90625, 7.81250, 1.56250, 3.12500, 6.25000, 1.25000, 2.50000, 5});
408
409 // bias_table used to find the bias factor
410 exprt conversion_factor_table_size = from_integer(
411 two_power_e_over_ten_power_d_table_negatives.size() +
412 two_power_e_over_ten_power_d_table.size(),
413 int_type);
414 array_exprt conversion_factor_table(
415 {}, array_typet(float_type, conversion_factor_table_size));
416 for(const auto &negative : two_power_e_over_ten_power_d_table_negatives)
417 conversion_factor_table.copy_to_operands(
418 constant_float(negative, float_spec));
419 for(const auto &positive : two_power_e_over_ten_power_d_table)
420 conversion_factor_table.copy_to_operands(
421 constant_float(positive, float_spec));
422
423 // The index in the table, corresponding to exponent e is e+128
424 plus_exprt shifted_index(bin_exponent, from_integer(128, int_type));
425
426 // bias_factor is $2^e / 10^(floor(log_10(2)*e))$ that is $2^e/10^d$
427 index_exprt conversion_factor(
428 conversion_factor_table, shifted_index, float_type);
429
430 // `dec_significand` is $n = m * bias_factor$
431 exprt dec_significand = floatbv_mult(conversion_factor, bin_significand);
432 exprt dec_significand_int = round_expr_to_zero(dec_significand);
433
434 // `dec_exponent` is $d$ in the formulas
435 // it is obtained from the approximation, checking whether it is not too small
436 binary_relation_exprt estimate_too_small(
437 dec_significand_int, ID_ge, from_integer(10, int_type));
438 if_exprt decimal_exponent(
439 estimate_too_small,
440 plus_exprt(dec_exponent_estimate, from_integer(1, int_type)),
441 dec_exponent_estimate);
442
443 // `dec_significand` is divided by 10 if it exceeds 10
444 dec_significand = if_exprt(
445 estimate_too_small,
446 floatbv_mult(dec_significand, constant_float(0.1, float_spec)),
447 dec_significand);
448 dec_significand_int = round_expr_to_zero(dec_significand);
449 array_string_exprt string_expr_integer_part =
450 array_pool.fresh_string(index_type, char_type);
451 auto result1 = add_axioms_for_string_of_int(
452 string_expr_integer_part, dec_significand_int, 3);
453 minus_exprt fractional_part(
454 dec_significand, floatbv_of_int_expr(dec_significand_int, float_spec));
455
456 // shifted_float is floor(float_expr * 1e5)
457 exprt shifting = constant_float(1e5, float_spec);
458 exprt shifted_float =
459 round_expr_to_zero(floatbv_mult(fractional_part, shifting));
460
461 // Numbers with greater or equal value to the following, should use
462 // the exponent notation.
463 exprt max_non_exponent_notation = from_integer(100000, shifted_float.type());
464
465 // fractional_part_shifted is floor(float_expr * 100000) % 100000
466 const mod_exprt fractional_part_shifted(
467 shifted_float, max_non_exponent_notation);
468
469 array_string_exprt string_fractional_part =
470 array_pool.fresh_string(index_type, char_type);
471 auto result2 = add_axioms_for_fractional_part(
472 string_fractional_part, fractional_part_shifted, 6);
473
474 // string_expr_with_fractional_part =
475 // concat(string_with_do, string_fractional_part)
476 const array_string_exprt string_expr_with_fractional_part =
477 array_pool.fresh_string(index_type, char_type);
478 auto result3 = add_axioms_for_concat(
479 string_expr_with_fractional_part,
480 string_expr_integer_part,
481 string_fractional_part);
482
483 // string_expr_with_E = concat(string_fraction, string_lit_E)
484 const array_string_exprt stringE =
485 array_pool.fresh_string(index_type, char_type);
486 auto result4 = add_axioms_for_constant(stringE, "E");
487 const array_string_exprt string_expr_with_E =
488 array_pool.fresh_string(index_type, char_type);
489 auto result5 = add_axioms_for_concat(
490 string_expr_with_E, string_expr_with_fractional_part, stringE);
491
492 // exponent_string = string_of_int(decimal_exponent)
493 const array_string_exprt exponent_string =
494 array_pool.fresh_string(index_type, char_type);
495 auto result6 =
496 add_axioms_for_string_of_int(exponent_string, decimal_exponent, 3);
497
498 // string_expr = concat(string_expr_with_E, exponent_string)
499 auto result7 =
500 add_axioms_for_concat(res, string_expr_with_E, exponent_string);
501
502 const exprt return_code = maximum(
503 result1.first,
504 maximum(
505 result2.first,
506 maximum(
507 result3.first,
508 maximum(
509 result4.first,
510 maximum(result5.first, maximum(result6.first, result7.first))))));
511 merge(result7.second, std::move(result1.second));
512 merge(result7.second, std::move(result2.second));
513 merge(result7.second, std::move(result3.second));
514 merge(result7.second, std::move(result4.second));
515 merge(result7.second, std::move(result5.second));
516 merge(result7.second, std::move(result6.second));
517 return {return_code, std::move(result7.second)};
518}
519
526std::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:177
bitvector_typet char_type()
Definition c_types.cpp:106
Boolean AND.
Definition std_expr.h:2125
Array constructor from list of elements.
Definition std_expr.h:1621
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.
const typet & length_type() const
Definition string_expr.h:70
Arrays with given size.
Definition std_types.h:807
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
Bit-wise OR.
Equality.
Definition std_expr.h:1366
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:163
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
constant_exprt to_expr() const
void from_float(const float f)
void from_double(const double d)
The trinary if-then-else operator.
Definition std_expr.h:2375
Array index operator.
Definition std_expr.h:1470
const irep_idt & id() const
Definition irep.h:388
Binary minus.
Definition std_expr.h:1061
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1228
Binary multiplication Associativity is not specified.
Definition std_expr.h:1107
Boolean negation.
Definition std_expr.h:2332
The plus expression Associativity is not specified.
Definition std_expr.h:1002
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.
const typet & subtype() const
Definition type.h:187
Semantic type conversion.
Definition std_expr.h:2073
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:83
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:208