CBMC: /home/runner/work/cbmc/cbmc/src/solvers/strings/string_constraint_generator_float.cpp Source File

CBMC
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
14#include "string_constraint_generator.h"
15
16#include <util/bitvector_expr.h>
17#include <util/floatbv_expr.h>
18#include <util/ieee_float.h>
19#include <util/mathematical_expr.h>
20
29 exprt 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(
37 from_integer(spec.bias(), signedbv_typet(32)));
38}
39
44 exprt 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);
71 return if_exprt(all_zeros, fraction, with_hidden_bit);
72}
73
79{
82 fl.from_float(f);
84 fl.from_double(f);
85 else
87 return fl.to_expr();
88}
89
99
105 exprt 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
128
142{
144 constant_float(0.30102999566398119521373889472449302, spec);
145 exprt bin_exp = get_exponent(f, spec);
149 // Rounding to zero is not correct for negative numbers, so we substract 1.
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);
198 const typet &char_type = to_type_with_subtype(res.content().type()).subtype();
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)
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
211 array_pool.fresh_string(index_type, char_type);
212 auto result1 =
214
215 // The axiom added to convert to integer should always be satisfiable even
216 // when the preconditions are not satisfied.
219 // We should not need more than 8 characters to represent the integer
220 // part of the float.
222 array_pool.fresh_string(index_type, char_type);
223 auto result2 =
225
226 auto result3 =
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);
251 string_constraintst constraints;
252 const typet &type = int_expr.type();
253 const typet &char_type = to_type_with_subtype(res.content().type()).subtype();
254 const typet &index_type = res.length_type();
255 const exprt ten = from_integer(10, 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
274
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
284 ID_le,
285 from_integer(j, res.length_type()));
287
288 // sum = 10 * sum + after_end ? 0 : (res[j]-'0')
290 after_end,
291 from_integer(0, type),
294
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 {
306 from_integer(j + 1, res.length_type())),
309 }
310 }
311
313 constraints.existential.push_back(a2);
314
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();
346 const typet &char_type = to_type_with_subtype(res.content().type()).subtype();
347
348 // This is used for rounding float to integers.
350
351 // `bin_exponent` is $e$ in the formulas
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$
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
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
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]
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
413 int_type);
417 conversion_factor_table.copy_to_operands(
420 conversion_factor_table.copy_to_operands(
422
423 // The index in the table, corresponding to exponent e is e+128
425
426 // bias_factor is 2ドル^e / 10^(floor(log_10(2)*e))$ that is 2ドル^e/10^d$
429
430 // `dec_significand` is $n = m * bias_factor$
433
434 // `dec_exponent` is $d$ in the formulas
435 // it is obtained from the approximation, checking whether it is not too small
442
443 // `dec_significand` is divided by 10 if it exceeds 10
450 array_pool.fresh_string(index_type, char_type);
455
456 // shifted_float is floor(float_expr * 1e5)
460
461 // Numbers with greater or equal value to the following, should use
462 // the exponent notation.
464
465 // fractional_part_shifted is floor(float_expr * 100000) % 100000
468
470 array_pool.fresh_string(index_type, char_type);
473
474 // string_expr_with_fractional_part =
475 // concat(string_with_do, string_fractional_part)
477 array_pool.fresh_string(index_type, char_type);
482
483 // string_expr_with_E = concat(string_fraction, string_lit_E)
485 array_pool.fresh_string(index_type, char_type);
488 array_pool.fresh_string(index_type, char_type);
491
492 // exponent_string = string_of_int(decimal_exponent)
494 array_pool.fresh_string(index_type, char_type);
495 auto result6 =
497
498 // string_expr = concat(string_expr_with_E, exponent_string)
499 auto result7 =
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
Boolean AND All operands must be boolean, and the result is always boolean.
Definition std_expr.h:2043
Array constructor from list of elements.
Definition std_expr.h:1570
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
Definition array_pool.cpp:26
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
Construct a string expression whose length and content are new variables.
Definition array_pool.cpp:57
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
Definition array_pool.cpp:184
Definition string_expr.h:68
Arrays with given size.
Definition std_types.h:806
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:784
Bit-wise OR Any number of operands that is greater or equal one.
Equality.
Definition std_expr.h:1339
Base class for all expressions.
Definition expr.h:57
std::vector< exprt > operandst
Definition expr.h:59
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition expr.h:164
typet & type()
Return the type of the expression.
Definition expr.h:85
Extracts a sub-range of a bit-vector operand.
Semantic type conversion from/to floating-point formats.
Definition floatbv_expr.h:19
Fixed-width bit-vector with IEEE floating-point interpretation.
Application of (mathematical) function.
argumentst & arguments()
Definition ieee_float.h:22
static ieee_float_spect single_precision()
Definition ieee_float.h:70
class floatbv_typet to_type() const
Definition ieee_float.cpp:25
mp_integer bias() const
Definition ieee_float.cpp:20
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
An IEEE 754 floating-point value, including specificiation.
Definition ieee_float.h:117
rounding_modet
Definition ieee_float.h:378
@ ROUND_TO_ZERO
Definition ieee_float.h:382
@ ROUND_TO_EVEN
Definition ieee_float.h:379
The trinary if-then-else operator.
Definition std_expr.h:2426
Array index operator.
Definition std_expr.h:1431
const irep_idt & id() const
Definition irep.h:388
Binary minus.
Definition std_expr.h:1065
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1216
Binary multiplication Associativity is not specified.
Definition std_expr.h:1104
Boolean negation.
Definition std_expr.h:2388
The plus expression Associativity is not specified.
Definition std_expr.h:1006
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....
array_poolt array_pool
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:1995
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(exprt a, exprt b)
Conjunction of two expressions.
Definition std_expr.cpp:252
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

AltStyle によって変換されたページ (->オリジナル) /