cprover
string_constraint_generator_float.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Generates string constraints for functions generating strings
4  from other types, in particular int, long, float, double, char, bool
5 
6 Author: Romain Brenguier, romain.brenguier@diffblue.com
7 
8 \*******************************************************************/
9 
13 
15 
17 
18 
28  const exprt &src, const ieee_float_spect &spec)
29 {
30  const extractbits_exprt exp_bits(
31  src, spec.f + spec.e - 1, 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 
44 exprt get_fraction(const exprt &src, const ieee_float_spect &spec)
45 {
46  return extractbits_exprt(src, spec.f-1, 0, unsignedbv_typet(spec.f));
47 }
48 
60  const exprt &src, const ieee_float_spect &spec, const typet &type)
61 {
62  PRECONDITION(type.id()==ID_unsignedbv);
63  PRECONDITION(to_unsignedbv_type(type).get_width()>spec.f);
64  typecast_exprt fraction(get_fraction(src, spec), type);
65  exprt exponent=get_exponent(src, spec);
66  equal_exprt all_zeros(exponent, from_integer(0, exponent.type()));
67  exprt hidden_bit=from_integer((1 << spec.f), type);
68  bitor_exprt with_hidden_bit(fraction, hidden_bit);
69  return if_exprt(all_zeros, fraction, with_hidden_bit);
70 }
71 
76 exprt constant_float(const double f, const ieee_float_spect &float_spec)
77 {
78  ieee_floatt fl(float_spec);
79  if(float_spec==ieee_float_spect::single_precision())
80  fl.from_float(f);
81  else if(float_spec==ieee_float_spect::double_precision())
82  fl.from_double(f);
83  else
85  return fl.to_expr();
86 }
87 
92 {
94  return floatbv_typecast_exprt(f, rounding, signedbv_typet(32));
95 }
96 
102 exprt floatbv_mult(const exprt &f, const exprt &g)
103 {
104  PRECONDITION(f.type()==g.type());
106  exprt mult(ID_floatbv_mult, f.type());
107  mult.copy_to_operands(f);
108  mult.copy_to_operands(g);
109  mult.copy_to_operands(from_integer(rounding, unsignedbv_typet(32)));
110  return mult;
111 }
112 
120 {
122  return floatbv_typecast_exprt(i, rounding, spec.to_type());
123 }
124 
138 {
139  exprt log_10_of_2=constant_float(0.30102999566398119521373889472449302, spec);
140  exprt bin_exp=get_exponent(f, spec);
141  exprt float_bin_exp=floatbv_of_int_expr(bin_exp, spec);
142  exprt dec_exp=floatbv_mult(float_bin_exp, log_10_of_2);
143  binary_relation_exprt negative_exp(dec_exp, ID_lt, constant_float(0.0, spec));
144  // Rounding to zero is not correct for negative numbers, so we substract 1.
145  minus_exprt dec_minus_one(dec_exp, constant_float(1.0, spec));
146  if_exprt adjust_for_neg(negative_exp, dec_minus_one, dec_exp);
147  return round_expr_to_zero(adjust_for_neg);
148 }
149 
157 {
158  PRECONDITION(f.arguments().size() == 3);
159  array_string_exprt res =
160  char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
161  return add_axioms_for_string_of_float(res, f.arguments()[2]);
162 }
163 
169 {
171 }
172 
186  const array_string_exprt &res,
187  const exprt &f)
188 {
189  const floatbv_typet &type=to_floatbv_type(f.type());
190  const ieee_float_spect float_spec(type);
191  const typet &char_type = res.content().type().subtype();
192  const typet &index_type = res.length().type();
193 
194  // We will look at the first 5 digits of the fractional part.
195  // shifted is floor(f * 1e5)
196  const exprt shifting = constant_float(1e5, float_spec);
197  const exprt shifted = round_expr_to_zero(floatbv_mult(f, shifting));
198  // Numbers with greater or equal value to the following, should use
199  // the exponent notation.
200  const exprt max_non_exponent_notation = from_integer(100000, shifted.type());
201  // fractional_part is floor(f * 100000) % 100000
202  const mod_exprt fractional_part(shifted, max_non_exponent_notation);
203  const array_string_exprt fractional_part_str =
205  const exprt return_code1 =
206  add_axioms_for_fractional_part(fractional_part_str, fractional_part, 6);
207 
208  // The axiom added to convert to integer should always be satisfiable even
209  // when the preconditions are not satisfied.
210  const mod_exprt integer_part(
211  round_expr_to_zero(f), max_non_exponent_notation);
212  // We should not need more than 8 characters to represent the integer
213  // part of the float.
214  const array_string_exprt integer_part_str =
216  const exprt return_code2 =
217  add_axioms_from_int(integer_part_str, integer_part, 8);
218 
219  return add_axioms_for_concat(res, integer_part_str, fractional_part_str);
220 }
221 
230  const array_string_exprt &res,
231  const exprt &int_expr,
232  size_t max_size)
233 {
234  PRECONDITION(int_expr.type().id()==ID_signedbv);
235  PRECONDITION(max_size>=2);
236  const typet &type=int_expr.type();
237  const typet &char_type = res.content().type().subtype();
238  const typet &index_type = res.length().type();
239  const exprt ten = from_integer(10, type);
240  const exprt zero_char = constant_char('0', char_type);
241  const exprt nine_char = constant_char('9', char_type);
242  const exprt max = from_integer(max_size, index_type);
243 
244  // We add axioms:
245  // a1 : 2 <= |res| <= max_size
246  // a2 : starts_with_dot && no_trailing_zero && is_number
247  // starts_with_dot: res[0] = '.'
248  // is_number: forall i:[1, max_size[. '0' < res[i] < '9'
249  // no_trailing_zero: forall j:[2, max_size[. !(|res| = j+1 && res[j] = '0')
250  // a3 : int_expr = sum_j 10^j (j < |res| ? res[j] - '0' : 0)
251 
252  and_exprt a1(res.axiom_for_length_gt(1),
253  res.axiom_for_length_le(max));
254  lemmas.push_back(a1);
255 
256  equal_exprt starts_with_dot(res[0], from_integer('.', char_type));
257 
258  exprt::operandst digit_constraints;
259  digit_constraints.push_back(starts_with_dot);
260  exprt sum=from_integer(0, type);
261 
262  for(size_t j=1; j<max_size; j++)
263  {
264  // after_end is |res| <= j
265  binary_relation_exprt after_end(
266  res.length(), ID_le, from_integer(j, res.length().type()));
267  mult_exprt ten_sum(sum, ten);
268 
269  // sum = 10 * sum + after_end ? 0 : (res[j]-'0')
270  if_exprt to_add(
271  after_end,
272  from_integer(0, type),
273  typecast_exprt(minus_exprt(res[j], zero_char), type));
274  sum=plus_exprt(ten_sum, to_add);
275 
277  binary_relation_exprt(res[j], ID_ge, zero_char),
278  binary_relation_exprt(res[j], ID_le, nine_char));
279  digit_constraints.push_back(is_number);
280 
281  // There are no trailing zeros except for ".0" (i.e j=2)
282  if(j>1)
283  {
284  not_exprt no_trailing_zero(and_exprt(
285  equal_exprt(res.length(), from_integer(j+1, res.length().type())),
286  equal_exprt(res[j], zero_char)));
287  digit_constraints.push_back(no_trailing_zero);
288  }
289  }
290 
291  exprt a2=conjunction(digit_constraints);
292  lemmas.push_back(a2);
293 
294  equal_exprt a3(int_expr, sum);
295  lemmas.push_back(a3);
296 
297  return from_integer(0, signedbv_typet(32));
298 }
299 
316  const array_string_exprt &res,
317  const exprt &f)
318 {
320  const typet float_type = float_spec.to_type();
321  const signedbv_typet int_type(32);
322  const typet &index_type = res.length().type();
323  const typet &char_type = res.content().type().subtype();
324 
325  // This is used for rounding float to integers.
326  exprt round_to_zero_expr=from_integer(ieee_floatt::ROUND_TO_ZERO, int_type);
327 
328  // `bin_exponent` is $e$ in the formulas
329  exprt bin_exponent=get_exponent(f, float_spec);
330 
331  // $m$ from the formula is a value between 0.0 and 2.0 represented
332  // with values in the range 0x000000 0xFFFFFF so 1 corresponds to 0x800000.
333  // `bin_significand_int` represents $m * 0x800000$
334  exprt bin_significand_int=
335  get_significand(f, float_spec, unsignedbv_typet(32));
336  // `bin_significand` represents $m$ and is obtained
337  // by multiplying `binary_significand_as_int` by
338  // 1/0x800000 = 2^-23 = 1.1920928955078125 * 10^-7
339  exprt bin_significand=floatbv_mult(
340  floatbv_typecast_exprt(bin_significand_int, round_to_zero_expr, float_type),
341  constant_float(1.1920928955078125e-7, float_spec));
342 
343  // This is a first approximation of the exponent that will adjust
344  // if the fraction we get is greater than 10
345  exprt dec_exponent_estimate=estimate_decimal_exponent(f, float_spec);
346 
347  // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[0,128]
348  std::vector<double> two_power_e_over_ten_power_d_table(
349  { 1, 2, 4, 8, 1.6, 3.2, 6.4, 1.28, 2.56,
350  5.12, 1.024, 2.048, 4.096, 8.192, 1.6384, 3.2768, 6.5536,
351  1.31072, 2.62144, 5.24288, 1.04858, 2.09715, 4.19430, 8.38861, 1.67772,
352  3.35544, 6.71089, 1.34218, 2.68435, 5.36871, 1.07374, 2.14748, 4.29497,
353  8.58993, 1.71799, 3.43597, 6.87195, 1.37439, 2.74878, 5.49756, 1.09951,
354  2.19902, 4.39805, 8.79609, 1.75922, 3.51844, 7.03687, 1.40737, 2.81475,
355  5.62950, 1.12590, 2.25180, 4.50360, 9.00720, 1.80144, 3.60288, 7.20576,
356  1.44115, 2.88230, 5.76461, 1.15292, 2.30584, 4.61169, 9.22337, 1.84467,
357  3.68935, 7.37870, 1.47574, 2.95148, 5.90296, 1.18059, 2.36118, 4.72237,
358  9.44473, 1.88895, 3.77789, 7.55579, 1.51116, 3.02231, 6.04463, 1.20893,
359  2.41785, 4.83570, 9.67141, 1.93428, 3.86856, 7.73713, 1.54743, 3.09485,
360  6.18970, 1.23794, 2.47588, 4.95176, 9.90352, 1.98070, 3.96141, 7.92282,
361  1.58456, 3.16913, 6.33825, 1.26765, 2.53530, 5.07060, 1.01412, 2.02824,
362  4.05648, 8.11296, 1.62259, 3.24519, 6.49037, 1.29807, 2.59615, 5.1923,
363  1.03846, 2.07692, 4.15384, 8.30767, 1.66153, 3.32307, 6.64614, 1.32923,
364  2.65846, 5.31691, 1.06338, 2.12676, 4.25353, 8.50706, 1.70141});
365 
366  // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[-128,-1]
367  std::vector<double> two_power_e_over_ten_power_d_table_negatives(
368  { 2.93874, 5.87747, 1.17549, 2.35099, 4.70198, 9.40395, 1.88079, 3.76158,
369  7.52316, 1.50463, 3.00927, 6.01853, 1.20371, 2.40741, 4.81482, 9.62965,
370  1.92593, 3.85186, 7.70372, 1.54074, 3.08149, 6.16298, 1.23260, 2.46519,
371  4.93038, 9.86076, 1.97215, 3.94430, 7.88861, 1.57772, 3.15544, 6.31089,
372  1.26218, 2.52435, 5.04871, 1.00974, 2.01948, 4.03897, 8.07794, 1.61559,
373  3.23117, 6.46235, 1.29247, 2.58494, 5.16988, 1.03398, 2.06795, 4.13590,
374  8.27181, 1.65436, 3.30872, 6.61744, 1.32349, 2.64698, 5.29396, 1.05879,
375  2.11758, 4.23516, 8.47033, 1.69407, 3.38813, 6.77626, 1.35525, 2.71051,
376  5.42101, 1.08420, 2.16840, 4.33681, 8.67362, 1.73472, 3.46945, 6.93889,
377  1.38778, 2.77556, 5.55112, 1.11022, 2.22045, 4.44089, 8.88178, 1.77636,
378  3.55271, 7.10543, 1.42109, 2.84217, 5.68434, 1.13687, 2.27374, 4.54747,
379  9.09495, 1.81899, 3.63798, 7.27596, 1.45519, 2.91038, 5.82077, 1.16415,
380  2.32831, 4.65661, 9.31323, 1.86265, 3.72529, 7.45058, 1.49012, 2.98023,
381  5.96046, 1.19209, 2.38419, 4.76837, 9.53674, 1.90735, 3.81470, 7.62939,
382  1.52588, 3.05176, 6.10352, 1.22070, 2.44141, 4.88281, 9.76563, 1.95313,
383  3.90625, 7.81250, 1.56250, 3.12500, 6.25000, 1.25000, 2.50000, 5});
384 
385  // bias_table used to find the bias factor
386  exprt conversion_factor_table_size=from_integer(
387  two_power_e_over_ten_power_d_table_negatives.size()+
388  two_power_e_over_ten_power_d_table.size(),
389  int_type);
390  array_exprt conversion_factor_table(
391  array_typet(float_type, conversion_factor_table_size));
392  for(const auto &f : two_power_e_over_ten_power_d_table_negatives)
393  conversion_factor_table.copy_to_operands(constant_float(f, float_spec));
394  for(const auto &f : two_power_e_over_ten_power_d_table)
395  conversion_factor_table.copy_to_operands(constant_float(f, float_spec));
396 
397  // The index in the table, corresponding to exponent e is e+128
398  plus_exprt shifted_index(bin_exponent, from_integer(128, int_type));
399 
400  // bias_factor is $2^e / 10^(floor(log_10(2)*e))$ that is $2^e/10^d$
401  index_exprt conversion_factor(
402  conversion_factor_table, shifted_index, float_type);
403 
404  // `dec_significand` is $n = m * bias_factor$
405  exprt dec_significand=floatbv_mult(conversion_factor, bin_significand);
406  exprt dec_significand_int=round_expr_to_zero(dec_significand);
407 
408  // `dec_exponent` is $d$ in the formulas
409  // it is obtained from the approximation, checking whether it is not too small
410  binary_relation_exprt estimate_too_small(
411  dec_significand_int, ID_ge, from_integer(10, int_type));
412  if_exprt decimal_exponent(
413  estimate_too_small,
414  plus_exprt(dec_exponent_estimate, from_integer(1, int_type)),
415  dec_exponent_estimate);
416 
417  // `dec_significand` is divided by 10 if it exceeds 10
418  dec_significand=if_exprt(
419  estimate_too_small,
420  floatbv_mult(dec_significand, constant_float(0.1, float_spec)),
421  dec_significand);
422  dec_significand_int=round_expr_to_zero(dec_significand);
423 
424  array_string_exprt string_expr_integer_part =
426  exprt return_code1 =
427  add_axioms_from_int(string_expr_integer_part, dec_significand_int, 3);
428  minus_exprt fractional_part(
429  dec_significand, floatbv_of_int_expr(dec_significand_int, float_spec));
430 
431  // shifted_float is floor(f * 1e5)
432  exprt shifting=constant_float(1e5, float_spec);
433  exprt shifted_float=
434  round_expr_to_zero(floatbv_mult(fractional_part, shifting));
435 
436  // Numbers with greater or equal value to the following, should use
437  // the exponent notation.
438  exprt max_non_exponent_notation=from_integer(100000, shifted_float.type());
439 
440  // fractional_part_shifted is floor(f * 100000) % 100000
441  const mod_exprt fractional_part_shifted(
442  shifted_float, max_non_exponent_notation);
443 
444  array_string_exprt string_fractional_part =
446  const exprt return_code2 = add_axioms_for_fractional_part(
447  string_fractional_part, fractional_part_shifted, 6);
448 
449  // string_expr_with_fractional_part =
450  // concat(string_with_do, string_fractional_part)
451  const array_string_exprt string_expr_with_fractional_part =
453  const exprt return_code3 = add_axioms_for_concat(
454  string_expr_with_fractional_part,
455  string_expr_integer_part,
456  string_fractional_part);
457 
458  // string_expr_with_E = concat(string_fraction, string_lit_E)
460  const exprt return_code4 = add_axioms_for_constant(stringE, "E");
461  const array_string_exprt string_expr_with_E =
463  const exprt return_code5 = add_axioms_for_concat(
464  string_expr_with_E, string_expr_with_fractional_part, stringE);
465 
466  // exponent_string = string_of_int(decimal_exponent)
467  const array_string_exprt exponent_string =
469  const exprt return_code6 =
470  add_axioms_from_int(exponent_string, decimal_exponent, 3);
471 
472  // string_expr = concat(string_expr_with_E, exponent_string)
473  return add_axioms_for_concat(res, string_expr_with_E, exponent_string);
474 }
475 
484 {
485  PRECONDITION(f.arguments().size() == 3);
486  const array_string_exprt res =
487  char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
488  const exprt &arg = f.arguments()[2];
490 }
The type of an expression.
Definition: type.h:22
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1220
Boolean negation.
Definition: std_expr.h:3230
semantic type conversion
Definition: std_expr.h:2111
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...
Generates string constraints to link results from string functions with their arguments.
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
application of (mathematical) function
Definition: std_expr.h:4531
constant_exprt to_expr() const
Definition: ieee_float.cpp:686
exprt add_axioms_from_int(const function_application_exprt &f)
Convert an integer to a string.
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1342
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
exprt constant_float(const double f, const ieee_float_spect &float_spec)
Create an expression to represent a float or double value.
argumentst & arguments()
Definition: std_expr.h:4564
The trinary if-then-else operator.
Definition: std_expr.h:3361
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...
typet & type()
Definition: expr.h:56
static ieee_float_spect double_precision()
Definition: ieee_float.h:80
class floatbv_typet to_type() const
Definition: ieee_float.cpp:26
equality
Definition: std_expr.h:1354
exprt conjunction(const exprt::operandst &op)
Definition: std_expr.cpp:48
exprt add_axioms_from_double(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(D) java function.
const irep_idt & id() const
Definition: irep.h:189
exprt add_axioms_from_float_scientific_notation(const array_string_exprt &res, const exprt &f)
Add axioms to write the float in scientific notation.
Bit-wise OR.
Definition: std_expr.h:2583
exprt 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.
bitvector_typet float_type()
Definition: c_types.cpp:185
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1262
boolean AND
Definition: std_expr.h:2255
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:3072
binary_relation_exprt axiom_for_length_le(const string_exprt &rhs) const
Definition: string_expr.h:88
static ieee_float_spect single_precision()
Definition: ieee_float.h:74
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
void from_float(const float f)
The plus expression.
Definition: std_expr.h:893
bitvector_typet index_type()
Definition: c_types.cpp:16
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.
mp_integer bias() const
Definition: ieee_float.cpp:21
std::vector< exprt > operandst
Definition: expr.h:45
binary multiplication
Definition: std_expr.h:1017
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1245
static constant_exprt constant_char(int i, const typet &char_type)
generate constant character expression with character type.
exprt round_expr_to_zero(const exprt &f)
Round a float expression to an integer closer to 0.
bool is_number(const typet &type)
Definition: type.cpp:25
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1373
semantic type conversion from/to floating-point formats
Definition: std_expr.h:2176
Base class for all expressions.
Definition: expr.h:42
void from_double(const double d)
binary_relation_exprt axiom_for_length_gt(const exprt &rhs) const
Definition: string_expr.h:70
exprt add_axioms_for_string_of_float(const function_application_exprt &f)
String representation of a float value.
#define UNREACHABLE
Definition: invariant.h:250
exprt get_fraction(const exprt &src, const ieee_float_spect &spec)
Gets the fraction without hidden bit.
arrays with given size
Definition: std_types.h:1004
binary minus
Definition: std_expr.h:959
exprt add_axioms_for_fractional_part(const array_string_exprt &res, const exprt &i, size_t max_size)
Add axioms for representing the fractional part of a floating point starting with a dot...
std::size_t f
Definition: ieee_float.h:30
const array_string_exprt & char_array_of_pointer(const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
const typet & subtype() const
Definition: type.h:33
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
construct a string expression whose length and content are new variables
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::size_t e
Definition: ieee_float.h:30
bitvector_typet char_type()
Definition: c_types.cpp:114
exprt 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.
array constructor from list of elements
Definition: std_expr.h:1617
binary modulo
Definition: std_expr.h:1133
exprt get_exponent(const exprt &src, const ieee_float_spect &spec)
Gets the unbiased exponent in a floating-point bit-vector.
array index operator
Definition: std_expr.h:1462