From 9c94cb30bfdf207ccbc686dd96e7793a01481a07 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 2 May 2017 16:50:38 +0100 Subject: [PATCH 01/15] Correcting initialization of floatbv_typecast_exprt This was calling initializer of binary_exprt that resize the operators to size 2 without filling them up, which resulted in 4 operands instead of 2 for floatbv_typecast_exprt, with two of them being empty. --- src/util/std_expr.h | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 69a03bdfa9c..0d64ede33c6 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -1790,9 +1790,8 @@ class floatbv_typecast_exprt:public binary_exprt floatbv_typecast_exprt( const exprt &op, const exprt &rounding, - const typet &_type):binary_exprt(ID_floatbv_typecast, _type) + const typet &_type):binary_exprt(op, ID_floatbv_typecast, rounding, _type) { - copy_to_operands(op, rounding); } exprt &op() From d8af6b64887e3ae50ab408187456807d06f25925 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 10 May 2017 14:04:45 +0100 Subject: [PATCH 02/15] Adding id for scientific notation of floats --- src/util/irep_ids.def | 1 + 1 file changed, 1 insertion(+) diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 38b8783ee8e..8a22f226fc0 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -797,6 +797,7 @@ IREP_ID_ONE(cprover_string_of_int_hex_func) IREP_ID_ONE(cprover_string_of_long_func) IREP_ID_ONE(cprover_string_of_bool_func) IREP_ID_ONE(cprover_string_of_float_func) +IREP_ID_ONE(cprover_string_of_float_scientific_notation_func) IREP_ID_ONE(cprover_string_of_double_func) IREP_ID_ONE(cprover_string_of_char_func) IREP_ID_ONE(cprover_string_of_char_array_func) From 5f28dc66d1d099cfbd2bbffe5c99c3bd59073fe8 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 10 May 2017 14:24:13 +0100 Subject: [PATCH 03/15] New file for conversion between floats and strings This add a new file for functions of the solver responsible for adding axioms for the conversion between floating point values and strings. --- .../string_constraint_generator_float.cpp | 445 ++++++++++++++++++ 1 file changed, 445 insertions(+) create mode 100644 src/solvers/refinement/string_constraint_generator_float.cpp diff --git a/src/solvers/refinement/string_constraint_generator_float.cpp b/src/solvers/refinement/string_constraint_generator_float.cpp new file mode 100644 index 00000000000..569b44cb4c0 --- /dev/null +++ b/src/solvers/refinement/string_constraint_generator_float.cpp @@ -0,0 +1,445 @@ +/*******************************************************************\ + +Module: Generates string constraints for functions generating strings + from other types, in particular int, long, float, double, char, bool + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +/// \file +/// Generates string constraints for functions generating strings from other +/// types, in particular int, long, float, double, char, bool + +#include + +#include "string_constraint_generator.h" + + +/// Gets the unbiased exponent in a floating-point bit-vector +/// +/// TODO: factorize with float_bv.cpp float_utils.h +/// \param src: a floating point expression +/// \param spec: specification for floating points +/// \return A 32 bit integer representing the exponent. Note that 32 bits are +/// sufficient for the exponent even in octuple precision. +exprt get_exponent( + const exprt &src, const ieee_float_spect &spec) +{ + exprt exp_bits=extractbits_exprt( + src, spec.f+spec.e-1, spec.f, unsignedbv_typet(spec.e)); + + // Exponent is in biased from (numbers form -128 to 127 are encoded with + // integer from 0 to 255) we have to remove the bias. + return minus_exprt( + typecast_exprt(exp_bits, signedbv_typet(32)), + from_integer(spec.bias(), signedbv_typet(32))); +} + +/// Gets the magnitude without hidden bit +/// \param src: a floating point expression +/// \param spec: specification for floating points +/// \return An unsigned value representing the magnitude. +exprt get_magnitude(const exprt &src, const ieee_float_spect &spec) +{ + return extractbits_exprt(src, spec.f-1, 0, unsignedbv_typet(spec.f)); +} + +/// Gets the significand as a java integer, looking for the hidden bit +/// \param src: a floating point expression +/// \param spec: specification for floating points +/// \param type: type of the output, should be unsigned with width greater than +/// the width of the significand in the given spec +/// \return An integer expression of the given type representing the +/// significand. +exprt get_significand( + const exprt &src, const ieee_float_spect &spec, const typet &type) +{ + assert(type.id()==ID_unsignedbv); + assert(to_unsignedbv_type(type).get_width()>spec.f); + typecast_exprt magnitude(get_magnitude(src, spec), type); + exprt exponent=get_exponent(src, spec); + equal_exprt all_zeros(exponent, from_integer(0, exponent.type())); + exprt hidden_bit=from_integer((1 << spec.f), type); + plus_exprt with_hidden_bit(magnitude, hidden_bit); + return if_exprt(all_zeros, magnitude, with_hidden_bit); +} + +/// \param f: a floating point value in double precision +/// \return an expression representing this floating point +exprt constant_float(const double f, const ieee_float_spect &float_spec) +{ + ieee_floatt fl(float_spec); + if(float_spec==ieee_float_spect::single_precision()) + { + fl.from_float(f); + } + else + { + assert(float_spec==ieee_float_spect::double_precision()); + fl.from_double(f); + } + return fl.to_expr(); +} + +/// Round a float expression to an integer closer to 0 +/// \param f: expression representing a float +/// \return expression representing a 32 bit integer +exprt round_expr_to_zero(const exprt &f) +{ + exprt rounding=from_integer(ieee_floatt::ROUND_TO_ZERO, unsignedbv_typet(32)); + return floatbv_typecast_exprt(f, rounding, signedbv_typet(32)); +} + +/// Multiplication of expressions representing floating points. +/// Note that the rounding mode is set to ROUND_TO_EVEN. +/// \param f: a floating point expression +/// \param g: a floating point expression +/// \param rounding: rounding mode +/// \return An expression representing floating point multiplication. +exprt floatbv_mult(const exprt &f, const exprt &g) +{ + ieee_floatt::rounding_modet rounding=ieee_floatt::ROUND_TO_EVEN; + assert(f.type()==g.type()); + exprt mult(ID_floatbv_mult, f.type()); + mult.copy_to_operands(f); + mult.copy_to_operands(g); + mult.copy_to_operands(from_integer(rounding, unsignedbv_typet(32))); + return mult; +} + +/// Convert integers to floating point to be used in operations with +/// other values that are in floating point representation. +/// \param i: an expression representing an integer +/// \param spec: specification for floating point numbers +/// \return An expression representing representing the value of the input +/// integer as a float. +exprt floatbv_of_int_expr(const exprt &i, const ieee_float_spect &spec) +{ + exprt rounding=from_integer(ieee_floatt::ROUND_TO_ZERO, unsignedbv_typet(32)); + return floatbv_typecast_exprt(i, rounding, spec.to_type()); +} + +/// Estimate the decimal exponent that should be used to represent a given +/// floating point value in decimal. +/// We are looking for d such that n * 10^d = m * 10^e, so: +/// d = log_10(m) + log_10(2) * e - log_10(n) +/// m -- the magnitude -- should be between 1 and 2 so log_10(m) +/// in [0,log_10(2)]. +/// n -- the magnitude in base 10 -- should be between 1 and 10 so +/// log_10(n) in [0, 1]. +/// So the estimate is given by: +/// d ~=~ floor( log_10(2) * e) +/// \param f: a floating point expression +/// \param spec: specification for floating point +exprt estimate_decimal_exponent(const exprt &f, const ieee_float_spect &spec) +{ + exprt log_10_of_2=constant_float(0.30102999566398119521373889472449302, spec); + exprt bin_exp=get_exponent(f, spec); + exprt float_bin_exp=floatbv_of_int_expr(bin_exp, spec); + exprt dec_exp=floatbv_mult(float_bin_exp, log_10_of_2); + binary_relation_exprt negative_exp(dec_exp, ID_lt, constant_float(0.0, spec)); + // Rounding to zero is not correct for negative number, so we remove 1. + minus_exprt dec_minus_one(dec_exp, constant_float(1.0, spec)); + if_exprt adjust_for_neg(negative_exp, dec_minus_one, dec_exp); + return round_expr_to_zero(adjust_for_neg); +} + +/// add axioms corresponding to the String.valueOf(F) java function +/// \param f: function application with one float argument +/// \return a new string expression +string_exprt string_constraint_generatort::add_axioms_from_float( + const function_application_exprt &f) +{ + const refined_string_typet &ref_type=to_refined_string_type(f.type()); + return add_axioms_from_float(args(f, 1)[0], ref_type); +} + +/// add axioms corresponding to the String.valueOf(D) java function +/// \param f: function application with one double argument +/// \return a new string expression +string_exprt string_constraint_generatort::add_axioms_from_double( + const function_application_exprt &f) +{ + const refined_string_typet &ref_type=to_refined_string_type(f.type()); + return add_axioms_from_float(args(f, 1)[0], ref_type); +} + +/// add axioms corresponding to the integer part of m, in decimal form with no +/// leading zeroes, followed by '.' ('\u002E'), followed by one or more decimal +/// digits representing the fractional part of m. +/// +/// TODO: this specification is not correct for negative numbers and +/// double precision and floating point value that exceed 100000 +/// \param f: expression representing a float +/// \param ref_type: refined type for strings +/// \return a new string expression +string_exprt string_constraint_generatort::add_axioms_from_float( + const exprt &f, const refined_string_typet &ref_type) +{ + const floatbv_typet &type=to_floatbv_type(f.type()); + ieee_float_spect float_spec(type); + + // We will look at the first 5 digits of the fractional part. + // shifted is floor(f * 1e5) + exprt shifting=constant_float(1e5, float_spec); + exprt shifted=round_expr_to_zero(floatbv_mult(f, shifting)); + // fractional_part is floor(f * 100000) % 100000 + mod_exprt fractional_part(shifted, from_integer(100000, shifted.type())); + string_exprt fractional_part_str= + add_axioms_for_fractional_part(fractional_part, 6, ref_type); + + // The axiom added to convert to integer should always been satisfiable even + // when the precondition are not satisfied. + mod_exprt integer_part( + round_expr_to_zero(f), from_integer(1000000, shifted.type())); + // We should not need more than 8 characters to represent the integer + // part of the float. + string_exprt integer_part_str=add_axioms_from_int(integer_part, 8, ref_type); + + return add_axioms_for_concat(integer_part_str, fractional_part_str); +} + +/// add axioms for representing the fractional part of a floating point starting +/// with a dot +/// \param i: an integer expression +/// \param max_size: a maximal size for the string +/// \param ref_type: a type for refined strings +/// \return a string expression +string_exprt string_constraint_generatort::add_axioms_for_fractional_part( + const exprt &i, size_t max_size, const refined_string_typet &ref_type) +{ + string_exprt res=fresh_string(ref_type); + const typet &type=i.type(); + assert(type.id()==ID_signedbv); + exprt ten=from_integer(10, type); + const typet &char_type=ref_type.get_char_type(); + const typet &index_type=ref_type.get_index_type(); + exprt zero_char=constant_char('0', char_type); + exprt nine_char=constant_char('9', char_type); + exprt max=from_integer(max_size, index_type); + + // We add axioms: + // a1 : 2 <= |res| <= max_size + // a2 : forall 1 <= i < size '0' < res[i] < '9' + // res[0] = '.' + // a3 : i = sum_j 10^j res[j] - '0' + // for all j : !(|res| = j+1 && res[j]='0') + // for all j : |res| <= j => res[j]='0' + + and_exprt a1(res.axiom_for_is_strictly_longer_than(1), + res.axiom_for_is_shorter_than(max)); + axioms.push_back(a1); + + equal_exprt starts_with_dot(res[0], from_integer('.', char_type)); + + exprt::operandst digit_constraints; + digit_constraints.push_back(starts_with_dot); + exprt sum=from_integer(0, type); + + for(size_t j=1; j1) + { + not_exprt no_trailing_zero(and_exprt( + equal_exprt(res.length(), from_integer(j+1, res.length().type())), + equal_exprt(res[j], zero_char))); + axioms.push_back(no_trailing_zero); + } + } + + exprt a2=conjunction(digit_constraints); + axioms.push_back(a2); + + equal_exprt a3(i, sum); + axioms.push_back(a3); + + return res; +} + +/// Add axioms to write the float in scientific notation. +/// +/// A float is represented as $f = m * 2^e$ where $0 <= m < 2$ is the +/// significand and $-126 <= e <= 127$ is the exponent. +/// We want an alternate representation by finding $n$ and +/// $d$ such that $f=n*10^d$. We can estimate $d$ the following way: +/// $d ~= log_10(f/n) ~= log_10(m) + log_10(2) * e - log_10(n)$ +/// $d = floor(log_10(2) * e)$ +/// Then $n$ can be expressed by the equation: +/// $log_10(n) = log_10(m) + log_10(2) * e - d$ +/// $n = f /10^d = m * 2^e / 10^d = m * 2^e / 10^(floor(log_10(2) * e))$ +/// +/// TODO: For now we only consider single precision. +/// \param f: a float expression, which is positive +/// \param max_size: a maximal size for the string +/// \param ref_type: a type for refined strings +/// \return a string expression +string_exprt string_constraint_generatort:: + add_axioms_from_float_scientific_notation( + const exprt &f, const refined_string_typet &ref_type) +{ + ieee_float_spect float_spec=ieee_float_spect::single_precision(); + typet float_type=float_spec.to_type(); + signedbv_typet int_type(32); + + // This is used for rounding float to integers. + exprt round_to_zero_expr=from_integer(ieee_floatt::ROUND_TO_ZERO, int_type); + + // `bin_exponent` is $e$ in the formulas + exprt bin_exponent=get_exponent(f, float_spec); + + // $m$ from the formula is a value between 0.0 and 2.0 represented + // with values in the range 0x000000 0x0FFFFFF so 1 corresponds to 0x0800000. + // `bin_significand_int` represents $m * 0x800000$ + exprt bin_significand_int= + get_significand(f, float_spec, unsignedbv_typet(32)); + // `bin_significand` represents $m$ it is obtained + // by multiplying `binary_significand_as_int` by 1/0x800000=1.192092896e-7. + exprt bin_significand=floatbv_mult( + floatbv_typecast_exprt(bin_significand_int, round_to_zero_expr, float_type), + constant_float(1.192092896e-7, float_spec)); + + // This is a first approximation of the exponent that will adjust + // if the magnitude we get is greater than 10 + exprt dec_exponent_estimate=estimate_decimal_exponent(f, float_spec); + + // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[0,128] + std::vector two_power_e_over_ten_power_d_table( + {1, 2, 4, 8, 1.6, 3.2, 6.4, 1.28, 2.56, + 5.12, 1.024, 2.048, 4.096, 8.192, 1.6384, 3.2768, 6.5536, + 1.31072, 2.62144, 5.24288, 1.04858, 2.09715, 4.19430, 8.38861, 1.67772, + 3.35544, 6.71089, 1.34218, 2.68435, 5.36871, 1.07374, 2.14748, 4.29497, + 8.58993, 1.71799, 3.43597, 6.87195, 1.37439, 2.74878, 5.49756, 1.09951, + 2.19902, 4.39805, 8.79609, 1.75922, 3.51844, 7.03687, 1.40737, 2.81475, + 5.62950, 1.12590, 2.25180, 4.50360, 9.00720, 1.80144, 3.60288, 7.20576, + 1.44115, 2.88230, 5.76461, 1.15292, 2.30584, 4.61169, 9.22337, 1.84467, + 3.68935, 7.37870, 1.47574, 2.95148, 5.90296, 1.18059, 2.36118, 4.72237, + 9.44473, 1.88895, 3.77789, 7.55579, 1.51116, 3.02231, 6.04463, 1.20893, + 2.41785, 4.83570, 9.67141, 1.93428, 3.86856, 7.73713, 1.54743, 3.09485, + 6.18970, 1.23794, 2.47588, 4.95176, 9.90352, 1.98070, 3.96141, 7.92282, + 1.58456, 3.16913, 6.33825, 1.26765, 2.53530, 5.07060, 1.01412, 2.02824, + 4.05648, 8.11296, 1.62259, 3.24519, 6.49037, 1.29807, 2.59615, 5.1923, + 1.03846, 2.07692, 4.15384, 8.30767, 1.66153, 3.32307, 6.64614, 1.32923, + 2.65846, 5.31691, 1.06338, 2.12676, 4.25353, 8.50706, 1.70141}); + + // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[-128,-1] + std::vector two_power_e_over_ten_power_d_table_negatives( + { 2.93874, 5.87747, 1.17549, 2.35099, 4.70198, 9.40395, 1.88079, 3.76158, + 7.52316, 1.50463, 3.00927, 6.01853, 1.20371, 2.40741, 4.81482, 9.62965, + 1.92593, 3.85186, 7.70372, 1.54074, 3.08149, 6.16298, 1.23260, 2.46519, + 4.93038, 9.86076, 1.97215, 3.94430, 7.88861, 1.57772, 3.15544, 6.31089, + 1.26218, 2.52435, 5.04871, 1.00974, 2.01948, 4.03897, 8.07794, 1.61559, + 3.23117, 6.46235, 1.29247, 2.58494, 5.16988, 1.03398, 2.06795, 4.13590, + 8.27181, 1.65436, 3.30872, 6.61744, 1.32349, 2.64698, 5.29396, 1.05879, + 2.11758, 4.23516, 8.47033, 1.69407, 3.38813, 6.77626, 1.35525, 2.71051, + 5.42101, 1.08420, 2.16840, 4.33681, 8.67362, 1.73472, 3.46945, 6.93889, + 1.38778, 2.77556, 5.55112, 1.11022, 2.22045, 4.44089, 8.88178, 1.77636, + 3.55271, 7.10543, 1.42109, 2.84217, 5.68434, 1.13687, 2.27374, 4.54747, + 9.09495, 1.81899, 3.63798, 7.27596, 1.45519, 2.91038, 5.82077, 1.16415, + 2.32831, 4.65661, 9.31323, 1.86265, 3.72529, 7.45058, 1.49012, 2.98023, + 5.96046, 1.19209, 2.38419, 4.76837, 9.53674, 1.90735, 3.81470, 7.62939, + 1.52588, 3.05176, 6.10352, 1.22070, 2.44141, 4.88281, 9.76563, 1.95313, + 3.90625, 7.81250, 1.56250, 3.12500, 6.25000, 1.25000, 2.50000, 5}); + + // bias_table used to find the bias factor + exprt conversion_factor_table_size=from_integer( + two_power_e_over_ten_power_d_table_negatives.size()+ + two_power_e_over_ten_power_d_table.size(), + int_type); + array_exprt conversion_factor_table( + array_typet(float_type, conversion_factor_table_size)); + for(const auto &f : two_power_e_over_ten_power_d_table_negatives) + conversion_factor_table.copy_to_operands(constant_float(f, float_spec)); + for(const auto &f : two_power_e_over_ten_power_d_table) + conversion_factor_table.copy_to_operands(constant_float(f, float_spec)); + + // The index in the table, corresponding to exponent e is e+128 + plus_exprt shifted_index(bin_exponent, from_integer(128, int_type)); + + // bias_factor is $2^e / 10^(floor(log_10(2)*e))$ that is $2^e/10^d$ + index_exprt conversion_factor( + conversion_factor_table, shifted_index, float_type); + + // `dec_significand` is $n = m * bias_factor$ + exprt dec_significand=floatbv_mult(conversion_factor, bin_significand); + exprt dec_significand_int=round_expr_to_zero(dec_significand); + + // `dec_exponent` is $d$ in the formulas + // it is obtained from the approximation, checking whether it is not too small + binary_relation_exprt estimate_too_small( + dec_significand_int, ID_ge, from_integer(10, int_type)); + if_exprt decimal_exponent( + estimate_too_small, + plus_exprt(dec_exponent_estimate, from_integer(1, int_type)), + dec_exponent_estimate); + + // `dec_significand` is divided by 10 if it exeeds 10 + dec_significand=if_exprt( + estimate_too_small, + floatbv_mult(dec_significand, constant_float(0.1, float_spec)), + dec_significand); + dec_significand_int=round_expr_to_zero(dec_significand); + + string_exprt string_expr_integer_part= + add_axioms_from_int(dec_significand_int, 3, ref_type); + minus_exprt fractional_part( + dec_significand, floatbv_of_int_expr(dec_significand_int, float_spec)); + + // shifted_float is floor(f * 1e5) + exprt shifting=constant_float(1e5, float_spec); + exprt shifted_float= + round_expr_to_zero(floatbv_mult(fractional_part, shifting)); + + // fractional_part_shifted is floor(f * 100000) % 100000 + mod_exprt fractional_part_shifted( + shifted_float, from_integer(100000, shifted_float.type())); + + string_exprt string_fractional_part=add_axioms_for_fractional_part( + fractional_part_shifted, 6, ref_type); + + // string_expr_with_fractional_part = + // concat(string_with_do, string_fractional_part) + string_exprt string_expr_with_fractional_part=add_axioms_for_concat( + string_expr_integer_part, string_fractional_part); + + // string_expr_with_E = concat(string_magnitude, string_lit_E) + string_exprt string_expr_with_E=add_axioms_for_concat_char( + string_expr_with_fractional_part, + from_integer('E', ref_type.get_char_type())); + + // exponent_string = string_of_int(decimal_exponent) + string_exprt exponent_string=add_axioms_from_int( + decimal_exponent, 3, ref_type); + + // string_expr = concat(string_expr_with_E, exponent_string) + return add_axioms_for_concat(string_expr_with_E, exponent_string); +} + +/// add axioms corresponding to the scientific representation of floating point +/// values +/// \param f: a function application expression +/// \return a new string expression +string_exprt string_constraint_generatort:: + add_axioms_from_float_scientific_notation( + const function_application_exprt &f) +{ + const refined_string_typet &ref_type=to_refined_string_type(f.type()); + return add_axioms_from_float_scientific_notation(args(f, 1)[0], ref_type); +} From 518efa49785a82d93c0c1a8cd40b9c8d13f4ca6b Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 10 May 2017 14:23:06 +0100 Subject: [PATCH 04/15] Conversion between string and float moved into a new file We remove the add_axioms_from_float that was defined in string_constraint_generator_valueof.cpp and use the new one from string_constraint_generator_float.cpp instead. We add string_constraint_generator_float.cpp to Makefile We also define an helper method for concatenation of char which can be used in float conversion. Improved documentation in string_constraint_generator_valueof and in string_constraint_generator_concat. --- src/solvers/Makefile | 1 + .../refinement/string_constraint_generator.h | 13 +- .../string_constraint_generator_concat.cpp | 19 +- .../string_constraint_generator_insert.cpp | 4 +- .../string_constraint_generator_main.cpp | 2 + .../string_constraint_generator_valueof.cpp | 176 +++--------------- 6 files changed, 61 insertions(+), 154 deletions(-) diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 3f3465277a3..5c994aefc14 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -165,6 +165,7 @@ SRC = $(BOOLEFORCE_SRC) \ refinement/string_constraint_generator_constants.cpp \ refinement/string_constraint_generator_indexof.cpp \ refinement/string_constraint_generator_insert.cpp \ + refinement/string_constraint_generator_float.cpp \ refinement/string_constraint_generator_main.cpp \ refinement/string_constraint_generator_testing.cpp \ refinement/string_constraint_generator_transformation.cpp \ diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 447bfd5f6f0..6812a28cf0d 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -155,6 +155,8 @@ class string_constraint_generatort string_exprt add_axioms_for_concat_long(const function_application_exprt &f); string_exprt add_axioms_for_concat_bool(const function_application_exprt &f); string_exprt add_axioms_for_concat_char(const function_application_exprt &f); + string_exprt add_axioms_for_concat_char( + const string_exprt &string_expr, const exprt &char_expr); string_exprt add_axioms_for_concat_double( const function_application_exprt &f); string_exprt add_axioms_for_concat_float(const function_application_exprt &f); @@ -236,9 +238,14 @@ class string_constraint_generatort // the start for negative number string_exprt add_axioms_from_float(const function_application_exprt &f); string_exprt add_axioms_from_float( - const exprt &f, - const refined_string_typet &ref_type, - bool double_precision); + const exprt &f, const refined_string_typet &ref_type); + + string_exprt add_axioms_for_fractional_part( + const exprt &i, size_t max_size, const refined_string_typet &ref_type); + string_exprt add_axioms_from_float_scientific_notation( + const exprt &f, const refined_string_typet &ref_type); + string_exprt add_axioms_from_float_scientific_notation( + const function_application_exprt &f); // Add axioms corresponding to the String.valueOf(D) java function // TODO: the specifications is only partial diff --git a/src/solvers/refinement/string_constraint_generator_concat.cpp b/src/solvers/refinement/string_constraint_generator_concat.cpp index b2c9a418055..a1b73940af2 100644 --- a/src/solvers/refinement/string_constraint_generator_concat.cpp +++ b/src/solvers/refinement/string_constraint_generator_concat.cpp @@ -148,9 +148,22 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_char( const function_application_exprt &f) { string_exprt s1=get_string_expr(args(f, 2)[0]); - const refined_string_typet &ref_type=to_refined_string_type(s1.type()); - string_exprt s2=add_axioms_from_char(args(f, 2)[1], ref_type); - return add_axioms_for_concat(s1, s2); + return add_axioms_for_concat_char(s1, args(f, 2)[1]); +} + +/// Add axioms corresponding adding the character char at the end of +/// string_expr. +/// \param string_expr: a string expression +/// \param char' a character expression +/// \return a new string expression + +string_exprt string_constraint_generatort::add_axioms_for_concat_char( + const string_exprt &string_expr, const exprt &char_expr) +{ + const refined_string_typet &ref_type= + to_refined_string_type(string_expr.type()); + string_exprt s2=add_axioms_from_char(char_expr, ref_type); + return add_axioms_for_concat(string_expr, s2); } /// Add axioms corresponding to the StringBuilder.append(D) java function diff --git a/src/solvers/refinement/string_constraint_generator_insert.cpp b/src/solvers/refinement/string_constraint_generator_insert.cpp index 0fb39e8a658..b0424fd6f87 100644 --- a/src/solvers/refinement/string_constraint_generator_insert.cpp +++ b/src/solvers/refinement/string_constraint_generator_insert.cpp @@ -119,7 +119,7 @@ string_exprt string_constraint_generatort::add_axioms_for_insert_double( { string_exprt s1=get_string_expr(args(f, 3)[0]); const refined_string_typet &ref_type=to_refined_string_type(s1.type()); - string_exprt s2=add_axioms_from_float(args(f, 3)[2], ref_type, true); + string_exprt s2=add_axioms_from_float(args(f, 3)[2], ref_type); return add_axioms_for_insert(s1, s2, args(f, 3)[1]); } @@ -133,7 +133,7 @@ string_exprt string_constraint_generatort::add_axioms_for_insert_float( { string_exprt s1=get_string_expr(args(f, 3)[0]); const refined_string_typet &ref_type=to_refined_string_type(s1.type()); - string_exprt s2=add_axioms_from_float(args(f, 3)[2], ref_type, false); + string_exprt s2=add_axioms_from_float(args(f, 3)[2], ref_type); return add_axioms_for_insert(s1, s2, args(f, 3)[1]); } diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index df7589529be..11b1a0aa893 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -454,6 +454,8 @@ exprt string_constraint_generatort::add_axioms_for_function_application( res=add_axioms_from_int_hex(expr); else if(id==ID_cprover_string_of_float_func) res=add_axioms_from_float(expr); + else if(id==ID_cprover_string_of_float_scientific_notation_func) + res=add_axioms_from_float_scientific_notation(expr); else if(id==ID_cprover_string_of_double_func) res=add_axioms_from_double(expr); else if(id==ID_cprover_string_of_long_func) diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index 7416bc1a341..914df80ee03 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp @@ -12,10 +12,9 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// types, in particular int, long, float, double, char, bool #include -#include -/// add axioms corresponding to the String.valueOf(I) java function -/// \par parameters: function application with one integer argument +/// Add axioms corresponding to the String.valueOf(I) java function. +/// \param expr: function application with one integer argument /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_from_int( const function_application_exprt &expr) @@ -24,8 +23,8 @@ string_exprt string_constraint_generatort::add_axioms_from_int( return add_axioms_from_int(args(expr, 1)[0], MAX_INTEGER_LENGTH, ref_type); } -/// add axioms corresponding to the String.valueOf(J) java function -/// \par parameters: function application with one long argument +/// Add axioms corresponding to the String.valueOf(J) java function. +/// \param expr: function application with one long argument /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_from_long( const function_application_exprt &expr) @@ -34,125 +33,8 @@ string_exprt string_constraint_generatort::add_axioms_from_long( return add_axioms_from_int(args(expr, 1)[0], MAX_LONG_LENGTH, ref_type); } -/// add axioms corresponding to the String.valueOf(F) java function -/// \par parameters: function application with one float argument -/// \return a new string expression -string_exprt string_constraint_generatort::add_axioms_from_float( - const function_application_exprt &f) -{ - const refined_string_typet &ref_type=to_refined_string_type(f.type()); - return add_axioms_from_float(args(f, 1)[0], ref_type, false); -} - -/// add axioms corresponding to the String.valueOf(D) java function -/// \par parameters: function application with one double argument -/// \return a new string expression -string_exprt string_constraint_generatort::add_axioms_from_double( - const function_application_exprt &f) -{ - const refined_string_typet &ref_type=to_refined_string_type(f.type()); - return add_axioms_from_float(args(f, 1)[0], ref_type, true); -} - -/// add axioms corresponding to the String.valueOf(F) java function Warning: we -/// currently only have partial specification -/// \par parameters: float expression and Boolean signaling that the argument -/// has -/// double precision -/// \return a new string expression -string_exprt string_constraint_generatort::add_axioms_from_float( - const exprt &f, const refined_string_typet &ref_type, bool double_precision) -{ - string_exprt res=fresh_string(ref_type); - const typet &index_type=ref_type.get_index_type(); - const typet &char_type=ref_type.get_char_type(); - const exprt &index24=from_integer(24, index_type); - axioms.push_back(res.axiom_for_is_shorter_than(index24)); - - string_exprt magnitude=fresh_string(ref_type); - string_exprt sign_string=fresh_string(ref_type); - string_exprt nan_string=add_axioms_for_constant("NaN", ref_type); - - // We add the axioms: - // a1 : If the argument is NaN, the result length is that of "NaN". - // a2 : If the argument is NaN, the result content is the string "NaN". - // a3 : f<0 => |sign_string|=1 - // a4 : f>=0 => |sign_string|=0 - // a5 : f<0 => sign_string[0]='-' - // a6 : f infinite => |magnitude|=|"Infinity"| - // a7 : forall i<|"Infinity"|, f infinite => magnitude[i]="Infinity"[i] - // a8 : f=0 => |magnitude|=|"0.0"| - // a9 : forall i<|"0.0"|, f=0 => f[i]="0.0"[i] - - ieee_float_spect fspec= - double_precision?ieee_float_spect::double_precision() - :ieee_float_spect::single_precision(); - - exprt isnan=float_bvt().isnan(f, fspec); - implies_exprt a1(isnan, magnitude.axiom_for_has_same_length_as(nan_string)); - axioms.push_back(a1); - - symbol_exprt qvar=fresh_univ_index("QA_equal_nan", index_type); - string_constraintt a2( - qvar, - nan_string.length(), - isnan, - equal_exprt(magnitude[qvar], nan_string[qvar])); - axioms.push_back(a2); - - // If the argument is not NaN, the result is a string that represents - // the sign and magnitude (absolute value) of the argument. - // If the sign is negative, the first character of the result is '-'; - // if the sign is positive, no sign character appears in the result. - - bitvector_typet bv_type=to_bitvector_type(f.type()); - unsigned width=bv_type.get_width(); - exprt isneg=extractbit_exprt(f, width-1); - - implies_exprt a3(isneg, sign_string.axiom_for_has_length(1)); - axioms.push_back(a3); - - implies_exprt a4(not_exprt(isneg), sign_string.axiom_for_has_length(0)); - axioms.push_back(a4); - - implies_exprt a5( - isneg, equal_exprt(sign_string[0], constant_char('-', char_type))); - axioms.push_back(a5); - - // If m is infinity, it is represented by the characters "Infinity"; - // thus, positive infinity produces the result "Infinity" and negative - // infinity produces the result "-Infinity". - - string_exprt infinity_string=add_axioms_for_constant("Infinity", ref_type); - exprt isinf=float_bvt().isinf(f, fspec); - implies_exprt a6( - isinf, magnitude.axiom_for_has_same_length_as(infinity_string)); - axioms.push_back(a6); - - symbol_exprt qvar_inf=fresh_univ_index("QA_equal_infinity", index_type); - equal_exprt meq(magnitude[qvar_inf], infinity_string[qvar_inf]); - string_constraintt a7(qvar_inf, infinity_string.length(), isinf, meq); - axioms.push_back(a7); - - // If m is zero, it is represented by the characters "0.0"; thus, negative - // zero produces the result "-0.0" and positive zero produces "0.0". - - string_exprt zero_string=add_axioms_for_constant("0.0", ref_type); - exprt iszero=float_bvt().is_zero(f, fspec); - implies_exprt a8(iszero, magnitude.axiom_for_has_same_length_as(zero_string)); - axioms.push_back(a8); - - symbol_exprt qvar_zero=fresh_univ_index("QA_equal_zero", index_type); - equal_exprt eq_zero(magnitude[qvar_zero], zero_string[qvar_zero]); - string_constraintt a9(qvar_zero, zero_string.length(), iszero, eq_zero); - axioms.push_back(a9); - - return add_axioms_for_concat(sign_string, magnitude); -} - - -/// add axioms corresponding to the String.valueOf(Z) java function -/// \par parameters: function application with on Boolean argument +/// Add axioms corresponding to the String.valueOf(Z) java function. +/// \param f: function application with a Boolean argument /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_from_bool( const function_application_exprt &f) @@ -161,10 +43,10 @@ string_exprt string_constraint_generatort::add_axioms_from_bool( return add_axioms_from_bool(args(f, 1)[0], ref_type); } - -/// add axioms stating that the returned string equals "true" when the Boolean -/// expression is true and "false" when it is false -/// \par parameters: Boolean expression +/// Add axioms stating that the returned string equals "true" when the Boolean +/// expression is true and "false" when it is false. +/// \param b: Boolean expression +/// \param ref_type: type of refined string expressions /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_from_bool( const exprt &b, const refined_string_typet &ref_type) @@ -329,8 +211,8 @@ string_exprt string_constraint_generatort::add_axioms_from_int( return res; } -/// returns the value represented by the character -/// \par parameters: a character expression in the following set: +/// Returns the integer value represented by the character. +/// \param chr: a character expression in the following set: /// 0123456789abcdef /// \return an integer expression exprt string_constraint_generatort::int_of_hex_char(const exprt &chr) const @@ -344,9 +226,10 @@ exprt string_constraint_generatort::int_of_hex_char(const exprt &chr) const minus_exprt(chr, zero_char)); } -/// add axioms stating that the returned string corresponds to the integer -/// argument written in hexadecimal -/// \par parameters: one integer argument +/// Add axioms stating that the returned string corresponds to the integer +/// argument written in hexadecimal. +/// \param i: an integer argument +/// \param ref_type: type of refined string expressions /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_from_int_hex( const exprt &i, const refined_string_typet &ref_type) @@ -402,7 +285,7 @@ string_exprt string_constraint_generatort::add_axioms_from_int_hex( } /// add axioms corresponding to the Integer.toHexString(I) java function -/// \par parameters: function application with integer argument +/// \param f: function application with an integer argument /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_from_int_hex( const function_application_exprt &f) @@ -411,8 +294,8 @@ string_exprt string_constraint_generatort::add_axioms_from_int_hex( return add_axioms_from_int_hex(args(f, 1)[0], ref_type); } -/// add axioms corresponding to the String.valueOf(C) java function -/// \par parameters: function application one char argument +/// Add axioms corresponding to the String.valueOf(C) java function. +/// \param f: function application one char argument /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_from_char( const function_application_exprt &f) @@ -421,9 +304,10 @@ string_exprt string_constraint_generatort::add_axioms_from_char( return add_axioms_from_char(args(f, 1)[0], ref_type); } -/// add axioms stating that the returned string has length 1 and the character -/// it contains correspond to the input expression -/// \par parameters: one expression of type char +/// Add axioms stating that the returned string has length 1 and the character +/// it contains correspond to the input expression. +/// \param c: one expression of type char +/// \param ref_type: type of refined string expressions /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_from_char( const exprt &c, const refined_string_typet &ref_type) @@ -434,9 +318,9 @@ string_exprt string_constraint_generatort::add_axioms_from_char( return res; } -/// add axioms corresponding to the String.valueOf([C) and String.valueOf([CII) -/// functions -/// \par parameters: function application with one or three arguments +/// Add axioms corresponding to the String.valueOf([C) and String.valueOf([CII) +/// functions. +/// \param f: function application with one or three arguments /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_for_value_of( const function_application_exprt &f) @@ -471,9 +355,9 @@ string_exprt string_constraint_generatort::add_axioms_for_value_of( } } -/// add axioms making the return value true if the given string is a correct -/// number -/// \par parameters: function application with one string expression +/// Add axioms making the return value true if the given string is a correct +/// number. +/// \param f: function application with one string expression /// \return an boolean expression exprt string_constraint_generatort::add_axioms_for_correct_number_format( const string_exprt &str, std::size_t max_size) @@ -527,7 +411,7 @@ exprt string_constraint_generatort::add_axioms_for_correct_number_format( } /// add axioms corresponding to the Integer.parseInt java function -/// \par parameters: function application with one string expression +/// \param f: function application with one string expression /// \return an integer expression exprt string_constraint_generatort::add_axioms_for_parse_int( const function_application_exprt &f) From 685a105e25c6957064ce30d1699b4d600cfe7b59 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 15 Jun 2017 09:37:20 +0100 Subject: [PATCH 05/15] Improving the float to string conversion in the preprocessing Also improves the string preprocessing documentation --- .../java_string_library_preprocess.cpp | 251 ++++++++++++------ .../java_string_library_preprocess.h | 3 +- 2 files changed, 173 insertions(+), 81 deletions(-) diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index d19b649908a..7839f6724d4 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -29,6 +29,8 @@ Date: April 2017 /// \param type: a type /// \param tag: a string +/// \return Boolean telling whether the type is a struct with the given tag or a +/// symbolic type with the tag prefixed by "java::" bool java_string_library_preprocesst::java_type_matches_tag( const typet &type, const std::string &tag) { @@ -45,7 +47,8 @@ bool java_string_library_preprocesst::java_type_matches_tag( return false; } -/// \par parameters: a type +/// \param type: a type +/// \return Boolean telling whether the type is that of java string pointer bool java_string_library_preprocesst::is_java_string_pointer_type( const typet &type) { @@ -58,21 +61,25 @@ bool java_string_library_preprocesst::is_java_string_pointer_type( return false; } -/// \par parameters: a type +/// \param type: a type +/// \return Boolean telling whether the type is that of java string bool java_string_library_preprocesst::is_java_string_type( const typet &type) { return java_type_matches_tag(type, "java.lang.String"); } -/// \par parameters: a type +/// \param type: a type +/// \return Boolean telling whether the type is that of java StringBuilder bool java_string_library_preprocesst::is_java_string_builder_type( const typet &type) { return java_type_matches_tag(type, "java.lang.StringBuilder"); } -/// \par parameters: a type +/// \param type: a type +/// \return Boolean telling whether the type is that of java StringBuilder +/// pointers bool java_string_library_preprocesst::is_java_string_builder_pointer_type( const typet &type) { @@ -85,14 +92,17 @@ bool java_string_library_preprocesst::is_java_string_builder_pointer_type( return false; } -/// \par parameters: a type +/// \param type: a type +/// \return Boolean telling whether the type is that of java StringBuffer bool java_string_library_preprocesst::is_java_string_buffer_type( const typet &type) { return java_type_matches_tag(type, "java.lang.StringBuffer"); } -/// \par parameters: a type +/// \param type: a type +/// \return Boolean telling whether the type is that of java StringBuffer +/// pointers bool java_string_library_preprocesst::is_java_string_buffer_pointer_type( const typet &type) { @@ -105,14 +115,17 @@ bool java_string_library_preprocesst::is_java_string_buffer_pointer_type( return false; } -/// \par parameters: a type +/// \param type: a type +/// \return Boolean telling whether the type is that of java char sequence bool java_string_library_preprocesst::is_java_char_sequence_type( const typet &type) { return java_type_matches_tag(type, "java.lang.CharSequence"); } -/// \par parameters: a type +/// \param type: a type +/// \return Boolean telling whether the type is that of a pointer to a java char +/// sequence bool java_string_library_preprocesst::is_java_char_sequence_pointer_type( const typet &type) { @@ -125,7 +138,8 @@ bool java_string_library_preprocesst::is_java_char_sequence_pointer_type( return false; } -/// \par parameters: a type +/// \param type: a type +/// \return Boolean telling whether the type is that of java char array bool java_string_library_preprocesst::is_java_char_array_type( const typet &type) { @@ -148,6 +162,7 @@ bool java_string_library_preprocesst::is_java_char_array_pointer_type( } /// \param symbol_table: a symbol_table containing an entry for java Strings +/// \return the type of data fields in java Strings. typet string_data_type(symbol_tablet symbol_table) { symbolt sym=symbol_table.lookup("java::java.lang.String"); @@ -242,6 +257,7 @@ void java_string_library_preprocesst::declare_function( /// \param symbol_table: symbol table /// \param init_code: code block, in which declaration of some arguments may be /// added +/// \return a list of expressions exprt::operandst java_string_library_preprocesst::process_parameters( const code_typet::parameterst ¶ms, const source_locationt &loc, @@ -295,6 +311,7 @@ void java_string_library_preprocesst::process_single_operand( /// \param symbol_table: symbol table /// \param init_code: code block, in which declaration of some arguments may be /// added +/// \return a list of expressions exprt::operandst java_string_library_preprocesst::process_operands( const exprt::operandst &operands, const source_locationt &loc, @@ -329,6 +346,7 @@ exprt::operandst java_string_library_preprocesst::process_operands( /// \param symbol_table: symbol table /// \param init_code: code block, in which declaration of some arguments may be /// added +/// \return a list of expressions exprt::operandst java_string_library_preprocesst::process_equals_function_operands( const exprt::operandst &operands, @@ -357,6 +375,7 @@ exprt::operandst /// Finds the type of the data component /// \param type: a type containing a "data" component /// \param symbol_table: symbol table +/// \return type of the "data" component typet java_string_library_preprocesst::get_data_type( const typet &type, const symbol_tablet &symbol_table) { @@ -380,6 +399,7 @@ typet java_string_library_preprocesst::get_data_type( /// Finds the type of the length component /// \param type: a type containing a "length" component /// \param symbol_table: symbol table +/// \return type of the "length" component typet java_string_library_preprocesst::get_length_type( const typet &type, const symbol_tablet &symbol_table) { @@ -403,6 +423,7 @@ typet java_string_library_preprocesst::get_length_type( /// access length member /// \param expr: an expression of structured type with length component /// \param symbol_table: symbol table +/// \return expression representing the "length" member exprt java_string_library_preprocesst::get_length( const exprt &expr, const symbol_tablet &symbol_table) { @@ -413,6 +434,7 @@ exprt java_string_library_preprocesst::get_length( /// access data member /// \param expr: an expression of structured type with length component /// \param symbol_table: symbol table +/// \return expression representing the "data" member exprt java_string_library_preprocesst::get_data( const exprt &expr, const symbol_tablet &symbol_table) { @@ -425,6 +447,7 @@ exprt java_string_library_preprocesst::get_data( /// \param loc: location in the source /// \param symbol_table: symbol table /// \param code: code block, in which some assignments will be added +/// \return a string expression string_exprt java_string_library_preprocesst::replace_char_array( const exprt &array_pointer, const source_locationt &loc, @@ -464,6 +487,7 @@ string_exprt java_string_library_preprocesst::replace_char_array( /// \param type: a type for refined strings /// \param loc: a location in the program /// \param symbol_table: symbol table +/// \return a new symbol symbol_exprt java_string_library_preprocesst::fresh_string( const typet &type, const source_locationt &loc, symbol_tablet &symbol_table) { @@ -478,6 +502,7 @@ symbol_exprt java_string_library_preprocesst::fresh_string( /// \param loc: a location in the program /// \param symbol_table: symbol table /// \param code: code block to which allocation instruction will be added +/// \return a new string_expr string_exprt java_string_library_preprocesst::fresh_string_expr( const source_locationt &loc, symbol_tablet &symbol_table, code_blockt &code) { @@ -503,6 +528,7 @@ string_exprt java_string_library_preprocesst::fresh_string_expr( /// \param loc: a location in the program /// \param symbol_table: symbol table /// \param code: code block to which allocation instruction will be added +/// \return a new expression of refined string type exprt java_string_library_preprocesst::fresh_string_expr_symbol( const source_locationt &loc, symbol_tablet &symbol_table, code_blockt &code) { @@ -522,6 +548,7 @@ exprt java_string_library_preprocesst::fresh_string_expr_symbol( /// \param loc: a location in the program /// \param symbol_table: symbol table /// \param code: code block to which allocation instruction will be added +/// \return a new string exprt java_string_library_preprocesst::allocate_fresh_string( const typet &type, const source_locationt &loc, @@ -540,6 +567,7 @@ exprt java_string_library_preprocesst::allocate_fresh_string( /// \param loc: a location in the program /// \param symbol_table: symbol table /// \param code: code block to which allocation instruction will be added +/// \return a new array exprt java_string_library_preprocesst::allocate_fresh_array( const typet &type, const source_locationt &loc, @@ -557,6 +585,7 @@ exprt java_string_library_preprocesst::allocate_fresh_array( /// \param arguments: a list of arguments /// \param type: return type of the function /// \param symbol_table: a symbol table +/// \return a function application representing: function_name(arguments) exprt java_string_library_preprocesst::make_function_application( const irep_idt &function_name, const exprt::operandst &arguments, @@ -580,6 +609,7 @@ exprt java_string_library_preprocesst::make_function_application( /// \param function_name: the name of the function /// \param arguments: a list of arguments /// \param symbol_table: a symbol table +/// \return the following code: > lhs=function_name_length(arguments) codet java_string_library_preprocesst::code_assign_function_application( const exprt &lhs, const irep_idt &function_name, @@ -596,6 +626,7 @@ codet java_string_library_preprocesst::code_assign_function_application( /// \param arguments: a list of arguments /// \param type: the return type /// \param symbol_table: a symbol table +/// \return the following code: > return function_name_length(arguments) codet java_string_library_preprocesst::code_return_function_application( const irep_idt &function_name, const exprt::operandst &arguments, @@ -611,6 +642,9 @@ codet java_string_library_preprocesst::code_return_function_application( /// \param function_name: the name of the function /// \param arguments: arguments of the function /// \param symbol_table: symbol table +/// \return return the following code: > str.length <- +/// function_name_length(arguments) > str.data <- +/// function_name_data(arguments) codet java_string_library_preprocesst::code_assign_function_to_string_expr( const string_exprt &string_expr, const irep_idt &function_name, @@ -635,6 +669,9 @@ codet java_string_library_preprocesst::code_assign_function_to_string_expr( /// \param loc: a location in the program /// \param symbol_table: symbol table /// \param code: code block in which we add instructions +/// \return return a string expr str and add the following code: > array +/// str.data > str.length <- function_name_length(arguments) > str.data <- +/// function_name_data(arguments) string_exprt java_string_library_preprocesst:: string_expr_of_function_application( const irep_idt &function_name, @@ -654,6 +691,8 @@ string_exprt java_string_library_preprocesst:: /// \param rhs_array: pointer to the array to assign /// \param rhs_length: length of the array to assign /// \param symbol_table: symbol table +/// \return return the following code: > lhs = { {Object}, length=rhs_length, +/// data=rhs_array } codet java_string_library_preprocesst::code_assign_components_to_java_string( const exprt &lhs, const exprt &rhs_array, @@ -687,6 +726,8 @@ codet java_string_library_preprocesst::code_assign_components_to_java_string( /// \param lhs: an expression representing a java string /// \param rhs: a string expression /// \param symbol_table: symbol table +/// \return return the following code: > lhs = { {Object}, length=rhs.length, +/// data=rhs.data } codet java_string_library_preprocesst::code_assign_string_expr_to_java_string( const exprt &lhs, const string_exprt &rhs, @@ -701,6 +742,8 @@ codet java_string_library_preprocesst::code_assign_string_expr_to_java_string( /// \param rhs: a string expression /// \param loc: a location in the program /// \param symbol_table: symbol table +/// \return return the following code: > data = new array[]; > *data = rhs.data; +/// > lhs = { {Object} , length=rhs.length, data=data} codet java_string_library_preprocesst:: code_assign_string_expr_to_new_java_string( const exprt &lhs, @@ -726,6 +769,8 @@ codet java_string_library_preprocesst:: /// \param lhs: a string expression /// \param rhs: an expression representing a java string /// \param symbol_table: symbol table +/// \return return the following code: > lhs.length=rhs->length > +/// lhs.data=*(rhs->data) codet java_string_library_preprocesst::code_assign_java_string_to_string_expr( const string_exprt &lhs, const exprt &rhs, symbol_tablet &symbol_table) { @@ -753,21 +798,19 @@ codet java_string_library_preprocesst::code_assign_java_string_to_string_expr( } /// \param lhs: an expression representing a java string -/// \param tmp_string: a temporary string to hold the literal /// \param s: the literal to be assigned /// \param symbol_table: symbol table +/// \return return the following code: > tmp_string = "s" > lhs = (string_expr) +/// tmp_string codet java_string_library_preprocesst:: code_assign_string_literal_to_string_expr( const string_exprt &lhs, - const exprt &tmp_string, const std::string &s, symbol_tablet &symbol_table) { - code_blockt code; - code.add(code_assignt(tmp_string, string_literal(s))); - code.add(code_assign_java_string_to_string_expr( - lhs, tmp_string, symbol_table)); - return code; + constant_exprt expr(s, string_typet()); + return code_assign_function_to_string_expr( + lhs, ID_cprover_string_literal_func, {expr}, symbol_table); } /// Used to provide code for the Java String.equals(Object) function. @@ -797,15 +840,16 @@ codet java_string_library_preprocesst::make_equals_function_code( return code; } -/// construct a Java string literal from a constant string value +/// construct a string_exprt from a constant string value /// \param s: a string -/// \return an expression representing a Java string literal with the given -/// content. -exprt java_string_library_preprocesst::string_literal(const std::string &s) +/// \param symbol_table: a symbol table +/// \return an expression representing a string expr with the given content +exprt java_string_library_preprocesst::string_literal( + const std::string &s, symbol_tablet &symbol_table) { - exprt string_literal(ID_java_string_literal); - string_literal.set(ID_value, s); - return string_literal; + constant_exprt expr(s, string_typet()); + return make_function_application( + ID_cprover_string_literal_func, {expr}, refined_string_type, symbol_table); } /// Provide code for the Float.toString(F) function. @@ -837,83 +881,122 @@ codet java_string_library_preprocesst::make_float_to_string_code( // Declaring and allocating String * str exprt str=allocate_fresh_string(type.return_type(), loc, symbol_table, code); - exprt tmp_string=fresh_string(type.return_type(), loc, symbol_table); - // Declaring CPROVER_string string_expr - string_exprt string_expr=fresh_string_expr(loc, symbol_table, code); - exprt string_expr_sym=fresh_string_expr_symbol(loc, symbol_table, code); - - // List of the different cases - std::vector case_list; - - // First case in the list is the default - code_ifthenelset case_sci_notation; + // Expression representing 0.0 ieee_float_spect float_spec=ieee_float_spect::single_precision(); - // Subcase of 0.0 - // TODO: case of -0.0 ieee_floatt zero_float(float_spec); zero_float.from_float(0.0); constant_exprt zero=zero_float.to_expr(); - case_sci_notation.cond()=ieee_float_equal_exprt(arg, zero); - case_sci_notation.then_case()=code_assign_string_literal_to_string_expr( - string_expr, tmp_string, "0.0", symbol_table); - // Subcase of computerized scientific notation - case_sci_notation.else_case()=code_assign_function_to_string_expr( - string_expr, ID_cprover_string_of_float_func, {arg}, symbol_table); - case_list.push_back(case_sci_notation); + // For each possible case with have a condition and a string_exprt + std::vector condition_list; + std::vector string_expr_list; + + // Case of computerized scientific notation + condition_list.push_back(binary_relation_exprt(arg, ID_ge, zero)); + string_exprt sci_notation=fresh_string_expr(loc, symbol_table, code); + exprt sci_notation_sym=fresh_string_expr_symbol(loc, symbol_table, code); + code.add(code_assign_function_to_string_expr( + sci_notation, + ID_cprover_string_of_float_scientific_notation_func, + {arg}, + symbol_table)); + // Assign string_expr_sym = { string_expr_length, string_expr_content } + code.add(code_assignt(sci_notation_sym, sci_notation)); + string_expr_list.push_back(sci_notation); + + // Subcase of negative scientific notation + condition_list.push_back(binary_relation_exprt(arg, ID_lt, zero)); + string_exprt neg_sci_notation=fresh_string_expr(loc, symbol_table, code); + exprt neg_sci_notation_sym=fresh_string_expr_symbol(loc, symbol_table, code); + string_exprt minus_sign=fresh_string_expr(loc, symbol_table, code); + code.add(code_assign_string_literal_to_string_expr( + minus_sign, "-", symbol_table)); + code.add(code_assign_function_to_string_expr( + neg_sci_notation, + ID_cprover_string_concat_func, + {minus_sign, sci_notation}, + symbol_table)); + code.add(code_assignt(neg_sci_notation_sym, neg_sci_notation)); + string_expr_list.push_back(neg_sci_notation); // Case of NaN - code_ifthenelset case_nan; - case_nan.cond()=isnan_exprt(arg); - case_nan.then_case()=code_assign_string_literal_to_string_expr( - string_expr, tmp_string, "NaN", symbol_table); - case_list.push_back(case_nan); + condition_list.push_back(isnan_exprt(arg)); + string_exprt nan=fresh_string_expr(loc, symbol_table, code); + code.add(code_assign_string_literal_to_string_expr( + nan, "NaN", symbol_table)); + string_expr_list.push_back(nan); // Case of Infinity - code_ifthenelset case_infinity; - code_ifthenelset case_minus_infinity; + extractbit_exprt is_neg(arg, float_spec.width()-1); + condition_list.push_back(and_exprt(isinf_exprt(arg), not_exprt(is_neg))); + string_exprt infinity=fresh_string_expr(loc, symbol_table, code); + code.add(code_assign_string_literal_to_string_expr( + infinity, "Infinity", symbol_table)); + string_expr_list.push_back(infinity); - case_infinity.cond()=isinf_exprt(arg); // Case -Infinity - exprt isneg=extractbit_exprt(arg, float_spec.width()-1); - case_minus_infinity.cond()=isneg; - case_minus_infinity.then_case()=code_assign_string_literal_to_string_expr( - string_expr, tmp_string, "-Infinity", symbol_table); - case_minus_infinity.else_case()=code_assign_string_literal_to_string_expr( - string_expr, tmp_string, "Infinity", symbol_table); - case_infinity.then_case()=case_minus_infinity; - case_list.push_back(case_infinity); + string_exprt minus_infinity=fresh_string_expr(loc, symbol_table, code); + condition_list.push_back(and_exprt(isinf_exprt(arg), is_neg)); + code.add(code_assign_string_literal_to_string_expr( + minus_infinity, "-Infinity", symbol_table)); + string_expr_list.push_back(minus_infinity); // Case of simple notation - code_ifthenelset case_simple_notation; - ieee_floatt bound_inf_float(float_spec); ieee_floatt bound_sup_float(float_spec); bound_inf_float.from_float(1e-3); bound_sup_float.from_float(1e7); + bound_inf_float.change_spec(float_spec); + bound_sup_float.change_spec(float_spec); constant_exprt bound_inf=bound_inf_float.to_expr(); constant_exprt bound_sup=bound_sup_float.to_expr(); and_exprt is_simple_float( binary_relation_exprt(arg, ID_ge, bound_inf), binary_relation_exprt(arg, ID_lt, bound_sup)); - case_simple_notation.cond()=is_simple_float; - case_simple_notation.then_case()=code_assign_function_to_string_expr( - string_expr, ID_cprover_string_of_float_func, {arg}, symbol_table); - case_list.push_back(case_simple_notation); + condition_list.push_back(is_simple_float); - // Combining all cases - for(std::size_t i=1; i Date: Thu, 15 Jun 2017 09:52:58 +0100 Subject: [PATCH 06/15] Improve the documentation of the string preprocessing Improves the formatting of the code in comments which add been changed when switching to doxygen. --- .../java_string_library_preprocess.cpp | 149 ++++++++++++------ 1 file changed, 98 insertions(+), 51 deletions(-) diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index 7839f6724d4..5de3f45d364 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -585,7 +585,7 @@ exprt java_string_library_preprocesst::allocate_fresh_array( /// \param arguments: a list of arguments /// \param type: return type of the function /// \param symbol_table: a symbol table -/// \return a function application representing: function_name(arguments) +/// \return a function application representing: `function_name(arguments)` exprt java_string_library_preprocesst::make_function_application( const irep_idt &function_name, const exprt::operandst &arguments, @@ -609,7 +609,10 @@ exprt java_string_library_preprocesst::make_function_application( /// \param function_name: the name of the function /// \param arguments: a list of arguments /// \param symbol_table: a symbol table -/// \return the following code: > lhs=function_name_length(arguments) +/// \return the following code: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// lhs = (arguments) +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::code_assign_function_application( const exprt &lhs, const irep_idt &function_name, @@ -626,7 +629,10 @@ codet java_string_library_preprocesst::code_assign_function_application( /// \param arguments: a list of arguments /// \param type: the return type /// \param symbol_table: a symbol table -/// \return the following code: > return function_name_length(arguments) +/// \return the following code: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// return (arguments) +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::code_return_function_application( const irep_idt &function_name, const exprt::operandst &arguments, @@ -642,9 +648,11 @@ codet java_string_library_preprocesst::code_return_function_application( /// \param function_name: the name of the function /// \param arguments: arguments of the function /// \param symbol_table: symbol table -/// \return return the following code: > str.length <- -/// function_name_length(arguments) > str.data <- -/// function_name_data(arguments) +/// \return return the following code: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// str.length = _length(arguments) +/// str.data = _data(arguments) +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::code_assign_function_to_string_expr( const string_exprt &string_expr, const irep_idt &function_name, @@ -669,9 +677,12 @@ codet java_string_library_preprocesst::code_assign_function_to_string_expr( /// \param loc: a location in the program /// \param symbol_table: symbol table /// \param code: code block in which we add instructions -/// \return return a string expr str and add the following code: > array -/// str.data > str.length <- function_name_length(arguments) > str.data <- -/// function_name_data(arguments) +/// \return return a string expr str and add the following code: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// array = str.data +/// str.length = _length(arguments) +/// str.data = _data(arguments) +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ string_exprt java_string_library_preprocesst:: string_expr_of_function_application( const irep_idt &function_name, @@ -691,8 +702,10 @@ string_exprt java_string_library_preprocesst:: /// \param rhs_array: pointer to the array to assign /// \param rhs_length: length of the array to assign /// \param symbol_table: symbol table -/// \return return the following code: > lhs = { {Object}, length=rhs_length, -/// data=rhs_array } +/// \return return the following code: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// lhs = { {Object}, length=rhs_length, data=rhs_array } +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::code_assign_components_to_java_string( const exprt &lhs, const exprt &rhs_array, @@ -726,8 +739,10 @@ codet java_string_library_preprocesst::code_assign_components_to_java_string( /// \param lhs: an expression representing a java string /// \param rhs: a string expression /// \param symbol_table: symbol table -/// \return return the following code: > lhs = { {Object}, length=rhs.length, -/// data=rhs.data } +/// \return return the following code: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// lhs = { {Object}, length=rhs.length, data=rhs.data } +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::code_assign_string_expr_to_java_string( const exprt &lhs, const string_exprt &rhs, @@ -742,8 +757,12 @@ codet java_string_library_preprocesst::code_assign_string_expr_to_java_string( /// \param rhs: a string expression /// \param loc: a location in the program /// \param symbol_table: symbol table -/// \return return the following code: > data = new array[]; > *data = rhs.data; -/// > lhs = { {Object} , length=rhs.length, data=data} +/// \return return the following code: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// data = new array[]; +/// *data = rhs.data; +/// lhs = { {Object} , length=rhs.length, data=data} +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst:: code_assign_string_expr_to_new_java_string( const exprt &lhs, @@ -769,8 +788,11 @@ codet java_string_library_preprocesst:: /// \param lhs: a string expression /// \param rhs: an expression representing a java string /// \param symbol_table: symbol table -/// \return return the following code: > lhs.length=rhs->length > -/// lhs.data=*(rhs->data) +/// \return return the following code: +/// ~~~~~~~~~~~~~~~~~~~~~~ +/// lhs.length=rhs->length +/// lhs.data=*(rhs->data) +/// ~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::code_assign_java_string_to_string_expr( const string_exprt &lhs, const exprt &rhs, symbol_tablet &symbol_table) { @@ -800,8 +822,11 @@ codet java_string_library_preprocesst::code_assign_java_string_to_string_expr( /// \param lhs: an expression representing a java string /// \param s: the literal to be assigned /// \param symbol_table: symbol table -/// \return return the following code: > tmp_string = "s" > lhs = (string_expr) -/// tmp_string +/// \return return the following code: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// tmp_string = "" +/// lhs = (string_expr) tmp_string +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst:: code_assign_string_literal_to_string_expr( const string_exprt &lhs, @@ -817,9 +842,12 @@ codet java_string_library_preprocesst:: /// \param type: type of the function call /// \param loc: location in the program_invocation_name /// \param symbol_table: symbol table -/// \return Code corresponding to: > string_expr1 = {this->length; *this->data} -/// > string_expr2 = {arg->length; *arg->data} > return -/// cprover_string_equal(string_expr1, string_expr2) +/// \return Code corresponding to: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// string_expr1 = {this->length; *this->data} +/// string_expr2 = {arg->length; *arg->data} +/// return cprover_string_equal(string_expr1, string_expr2) +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_equals_function_code( const code_typet &type, const source_locationt &loc, @@ -852,20 +880,11 @@ exprt java_string_library_preprocesst::string_literal( ID_cprover_string_literal_func, {expr}, refined_string_type, symbol_table); } -/// Provide code for the Float.toString(F) function. +/// Provide code for the String.valueOf(F) function. /// \param type: type of the function call /// \param loc: location in the program_invocation_name /// \param symbol_table: symbol table -/// \return Code corresponding to: > String * str; > str = MALLOC(String); > -/// String * tmp_string; > int string_expr_length; > char[] -/// string_expr_content; > CPROVER_string string_expr_sym; > if -/// arguments[1]==NaN > then {tmp_string="NaN"; -/// string_expr=(string_expr)tmp_string} > if arguments[1]==Infinity > then -/// {tmp_string="Infinity"; string_expr=(string_expr)tmp_string} > if -/// 1e-3 then -/// string_expr=cprover_float_to_string(arguments[1]) > else -/// string_expr=cprover_float_to_scientific_notation_string(arg[1]) > -/// string_expr_sym=string_expr; > str=(String*) string_expr; > return str; +/// \return Code corresponding to the Java conversion of floats to strings. codet java_string_library_preprocesst::make_float_to_string_code( const code_typet &type, const source_locationt &loc, @@ -1011,10 +1030,14 @@ codet java_string_library_preprocesst::make_float_to_string_code( /// \param ignore_first_arg: boolean flag telling that the first argument should /// not be part of the arguments of the call (but only used to be assigned the /// result) -/// \return code for the String.(args) function: > cprover_string_length = -/// fun(arg).length; > cprover_string_array = fun(arg).data; > this->length = -/// cprover_string_length; > this->data = cprover_string_array; > -/// cprover_string = {.=cprover_string_length, .=cprover_string_array}; +/// \return code for the String.(args) function: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// cprover_string_length = fun(arg).length; +/// cprover_string_array = fun(arg).data; +/// this->length = cprover_string_length; +/// this->data = cprover_string_array; +/// cprover_string = {.=cprover_string_length, .=cprover_string_array}; +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_init_function_from_call( const irep_idt &function_name, const code_typet &type, @@ -1163,9 +1186,13 @@ codet java_string_library_preprocesst::make_string_to_char_array_code( /// \param type: type of the function called /// \param loc: location in the source /// \param symbol_table: the symbol table -/// \return Code corresponding to > Class class1; > string_expr1 = -/// substr(this->@class_identifier, 6) > class1=Class.forName(string_expr1) > -/// return class1 +/// \return Code corresponding to +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// Class class1; +/// string_expr1 = substr(this->@class_identifier, 6) +/// class1=Class.forName(string_expr1) +/// return class1 +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_object_get_class_code( const code_typet &type, const source_locationt &loc, @@ -1243,7 +1270,10 @@ codet java_string_library_preprocesst::make_object_get_class_code( /// \param type: type of the function /// \param loc: location in the source /// \param symbol_table: symbol table -/// \return Code corresponding to: > return function_name(args); +/// \return Code corresponding to: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// return function_name(args) +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_function_from_call( const irep_idt &function_name, const code_typet &type, @@ -1264,8 +1294,13 @@ codet java_string_library_preprocesst::make_function_from_call( /// \param type: type of the function /// \param loc: location in the source /// \param symbol_table: symbol table -/// \return Code corresponding to: > string_expr = function_name(args) > string -/// = new String > string = string_expr_to_string(string) > return string +/// \return Code corresponding to: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// string_expr = function_name(args) +/// string = new String +/// string = string_expr_to_string(string) +/// return string +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst:: make_string_returning_function_from_call( const irep_idt &function_name, @@ -1303,9 +1338,14 @@ codet java_string_library_preprocesst:: /// \param type: type of the function /// \param loc: location in the source /// \param symbol_table: symbol table -/// \return Code corresponding to: > string_expr = string_to_string_expr(arg0) > -/// string_expr_sym = { string_expr.length; string_expr.content } > str = new -/// String > str = string_expr_to_string(string_expr) > return str +/// \return Code corresponding to: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// string_expr = string_to_string_expr(arg0) +/// string_expr_sym = { string_expr.length; string_expr.content } +/// str = new String +/// str = string_expr_to_string(string_expr) +/// return str +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_copy_string_code( const code_typet &type, const source_locationt &loc, @@ -1342,9 +1382,12 @@ codet java_string_library_preprocesst::make_copy_string_code( /// \param type: type of the function /// \param loc: location in the source /// \param symbol_table: symbol table -/// \return Code corresponding to: > string_expr = -/// java_string_to_string_expr(arg1) > string_expr_sym = { string_expr.length; -/// string_expr.content } > this = string_expr_to_java_string(string_expr) +/// \return Code corresponding to: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// string_expr = java_string_to_string_expr(arg1) +/// string_expr_sym = { string_expr.length; string_expr.content } +/// this = string_expr_to_java_string(string_expr) +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_copy_constructor_code( const code_typet &type, const source_locationt &loc, @@ -1378,8 +1421,12 @@ codet java_string_library_preprocesst::make_copy_constructor_code( /// \param type: type of the function /// \param loc: location in the source /// \param symbol_table: symbol table -/// \return Code corresponding to: > str_expr = java_string_to_string_expr(this) -/// > str_expr_sym = str_expr > return this->length +/// \return Code corresponding to: +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// str_expr = java_string_to_string_expr(this) +/// str_expr_sym = str_expr +/// return this->length +/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ codet java_string_library_preprocesst::make_string_length_code( const code_typet &type, const source_locationt &loc, From 8367ff52291320194498bfcaa0d8a0a6a65e25ae Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 19 Jun 2017 16:08:09 +0100 Subject: [PATCH 07/15] Allocate array in String result of String.valueOf(F) This could otherwise lead to problems in the generation of the verification condition. --- src/java_bytecode/java_string_library_preprocess.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp index 5de3f45d364..5a1fedf65a9 100644 --- a/src/java_bytecode/java_string_library_preprocess.cpp +++ b/src/java_bytecode/java_string_library_preprocess.cpp @@ -1010,8 +1010,8 @@ codet java_string_library_preprocesst::make_float_to_string_code( { code_ifthenelset ife; ife.cond()=condition_list[i]; - ife.then_case()=code_assign_string_expr_to_java_string( - str, string_expr_list[i], symbol_table); + ife.then_case()=code_assign_string_expr_to_new_java_string( + str, string_expr_list[i], loc, symbol_table); ife.else_case()=tmp_code; tmp_code=ife; } From 6518369962c522651a6de2a86780ca721ca4ef48 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 19 Jun 2017 16:11:40 +0100 Subject: [PATCH 08/15] Adding test for the String.valueOf(F) function Add and enable a test for a float to string conversion. --- .../java_value_of_float/test.class | Bin 0 -> 688 bytes .../java_value_of_float/test.desc | 8 ++++++++ .../java_value_of_float/test.java | 11 +++++++++++ 3 files changed, 19 insertions(+) create mode 100644 regression/strings-smoke-tests/java_value_of_float/test.class create mode 100644 regression/strings-smoke-tests/java_value_of_float/test.desc create mode 100644 regression/strings-smoke-tests/java_value_of_float/test.java diff --git a/regression/strings-smoke-tests/java_value_of_float/test.class b/regression/strings-smoke-tests/java_value_of_float/test.class new file mode 100644 index 0000000000000000000000000000000000000000..ddb0cfbdc0be0b1dfccc7d96614a2f70fe4426fe GIT binary patch literal 688 zcmY*XT~8B16g_vl+vzTgEd^?+qEb;?Y9MMQQHW6y5|auKH74@5-Hy1hZe>46{3-Uy zH=or6h$Q&#Kk*OvWQ=#VmTEScxpU{-bI(0H-+zBS1<=Gz3uBnkAOHOE&O!wjOqjTs z!>l@761Z$ZU`F7Ig*j9Ot`a8aohXuF?Dc}^i5EE?Uv>$!O~|f#ffqj@WNP&n1bwa7 zm4tlD3*=_9t{<*hhZ<|&WcB% zZesxrLScm5>g-B4{x8*zLoe82`UA&LZMGVkVENAX)~1sOcc#SSbYfnBlOG{=p)vl RYQ Date: Wed, 21 Jun 2017 15:36:03 +0100 Subject: [PATCH 09/15] Comment corrections in string_constraint_generator_concat --- .../refinement/string_constraint_generator_concat.cpp | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_concat.cpp b/src/solvers/refinement/string_constraint_generator_concat.cpp index a1b73940af2..72dd10b2ae5 100644 --- a/src/solvers/refinement/string_constraint_generator_concat.cpp +++ b/src/solvers/refinement/string_constraint_generator_concat.cpp @@ -13,7 +13,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include -/// Add axioms to say that the returned string expression is equal to the +/// Add axioms enforcing that the returned string expression is equal to the /// concatenation of s1 with the substring of s2 starting at index start_index /// and ending at index end_index. /// @@ -77,7 +77,7 @@ string_exprt string_constraint_generatort::add_axioms_for_concat( return add_axioms_for_concat_substr(s1, s2, index_zero, s2.length()); } -/// Add axioms to say that the returned string expression is equal to the +/// Add axioms enforcing that the returned string expression is equal to the /// concatenation of the two string arguments of the function application. /// /// In case 4 arguments instead of 2 are given the last two arguments are @@ -85,7 +85,7 @@ string_exprt string_constraint_generatort::add_axioms_for_concat( /// of the second argument: this is similar to the Java /// StringBuilder.append(CharSequence s, int start, int end) method. /// -/// \param f: function application with two arguments which are strings +/// \param f: function application with two string arguments /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_for_concat( const function_application_exprt &f) @@ -151,12 +151,11 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_char( return add_axioms_for_concat_char(s1, args(f, 2)[1]); } -/// Add axioms corresponding adding the character char at the end of +/// Add axioms corresponding to adding the character char at the end of /// string_expr. /// \param string_expr: a string expression /// \param char' a character expression /// \return a new string expression - string_exprt string_constraint_generatort::add_axioms_for_concat_char( const string_exprt &string_expr, const exprt &char_expr) { From a8b1e8ec63801919b68625a688bec0f36f0c8a7a Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 21 Jun 2017 15:41:14 +0100 Subject: [PATCH 10/15] Changing assert for PRECONDITION and UNREACHABLE in float to string conversion --- .../string_constraint_generator_float.cpp | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_float.cpp b/src/solvers/refinement/string_constraint_generator_float.cpp index 569b44cb4c0..7d3b9a404b0 100644 --- a/src/solvers/refinement/string_constraint_generator_float.cpp +++ b/src/solvers/refinement/string_constraint_generator_float.cpp @@ -55,8 +55,8 @@ exprt get_magnitude(const exprt &src, const ieee_float_spect &spec) exprt get_significand( const exprt &src, const ieee_float_spect &spec, const typet &type) { - assert(type.id()==ID_unsignedbv); - assert(to_unsignedbv_type(type).get_width()>spec.f); + PRECONDITION(type.id()==ID_unsignedbv); + PRECONDITION(to_unsignedbv_type(type).get_width()>spec.f); typecast_exprt magnitude(get_magnitude(src, spec), type); exprt exponent=get_exponent(src, spec); equal_exprt all_zeros(exponent, from_integer(0, exponent.type())); @@ -71,14 +71,11 @@ exprt constant_float(const double f, const ieee_float_spect &float_spec) { ieee_floatt fl(float_spec); if(float_spec==ieee_float_spect::single_precision()) - { fl.from_float(f); - } - else - { - assert(float_spec==ieee_float_spect::double_precision()); + else if(float_spec==ieee_float_spect::double_precision()) fl.from_double(f); - } + else + UNREACHABLE; return fl.to_expr(); } @@ -99,8 +96,8 @@ exprt round_expr_to_zero(const exprt &f) /// \return An expression representing floating point multiplication. exprt floatbv_mult(const exprt &f, const exprt &g) { + PRECONDITION(f.type()==g.type()); ieee_floatt::rounding_modet rounding=ieee_floatt::ROUND_TO_EVEN; - assert(f.type()==g.type()); exprt mult(ID_floatbv_mult, f.type()); mult.copy_to_operands(f); mult.copy_to_operands(g); @@ -209,9 +206,9 @@ string_exprt string_constraint_generatort::add_axioms_from_float( string_exprt string_constraint_generatort::add_axioms_for_fractional_part( const exprt &i, size_t max_size, const refined_string_typet &ref_type) { - string_exprt res=fresh_string(ref_type); + PRECONDITION(i.type().id()==ID_signedbv); const typet &type=i.type(); - assert(type.id()==ID_signedbv); + string_exprt res=fresh_string(ref_type); exprt ten=from_integer(10, type); const typet &char_type=ref_type.get_char_type(); const typet &index_type=ref_type.get_index_type(); From 105925ac45fc005070d0d5acfe1031a048d483ca Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 21 Jun 2017 15:37:23 +0100 Subject: [PATCH 11/15] Comment corrections in string_constraint_generator_float --- .../string_constraint_generator_float.cpp | 27 +++++++++++-------- 1 file changed, 16 insertions(+), 11 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_float.cpp b/src/solvers/refinement/string_constraint_generator_float.cpp index 7d3b9a404b0..7b79d1072ad 100644 --- a/src/solvers/refinement/string_constraint_generator_float.cpp +++ b/src/solvers/refinement/string_constraint_generator_float.cpp @@ -21,15 +21,16 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// TODO: factorize with float_bv.cpp float_utils.h /// \param src: a floating point expression /// \param spec: specification for floating points -/// \return A 32 bit integer representing the exponent. Note that 32 bits are -/// sufficient for the exponent even in octuple precision. +/// \return A new 32 bit integer expression representing the exponent. +/// Note that 32 bits are sufficient for the exponent even +/// in octuple precision. exprt get_exponent( const exprt &src, const ieee_float_spect &spec) { exprt exp_bits=extractbits_exprt( src, spec.f+spec.e-1, spec.f, unsignedbv_typet(spec.e)); - // Exponent is in biased from (numbers form -128 to 127 are encoded with + // Exponent is in biased from (numbers from -128 to 127 are encoded with // integer from 0 to 255) we have to remove the bias. return minus_exprt( typecast_exprt(exp_bits, signedbv_typet(32)), @@ -45,7 +46,10 @@ exprt get_magnitude(const exprt &src, const ieee_float_spect &spec) return extractbits_exprt(src, spec.f-1, 0, unsignedbv_typet(spec.f)); } -/// Gets the significand as a java integer, looking for the hidden bit +/// Gets the significand as a java integer, looking for the hidden bit. +/// Since the most significant bit is 1 for normalized number, it is not part +/// of the encoding of the significand and is 0 only if all the bits of the +/// exponent are 0, that is why it is called the hidden bit. /// \param src: a floating point expression /// \param spec: specification for floating points /// \param type: type of the output, should be unsigned with width greater than @@ -65,6 +69,7 @@ exprt get_significand( return if_exprt(all_zeros, magnitude, with_hidden_bit); } +/// Create an expression to represent a float or double value. /// \param f: a floating point value in double precision /// \return an expression representing this floating point exprt constant_float(const double f, const ieee_float_spect &float_spec) @@ -109,7 +114,7 @@ exprt floatbv_mult(const exprt &f, const exprt &g) /// other values that are in floating point representation. /// \param i: an expression representing an integer /// \param spec: specification for floating point numbers -/// \return An expression representing representing the value of the input +/// \return An expression representing the value of the input /// integer as a float. exprt floatbv_of_int_expr(const exprt &i, const ieee_float_spect &spec) { @@ -119,14 +124,14 @@ exprt floatbv_of_int_expr(const exprt &i, const ieee_float_spect &spec) /// Estimate the decimal exponent that should be used to represent a given /// floating point value in decimal. -/// We are looking for d such that n * 10^d = m * 10^e, so: +/// We are looking for d such that n * 10^d = m * 2^e, so: /// d = log_10(m) + log_10(2) * e - log_10(n) /// m -- the magnitude -- should be between 1 and 2 so log_10(m) /// in [0,log_10(2)]. /// n -- the magnitude in base 10 -- should be between 1 and 10 so /// log_10(n) in [0, 1]. /// So the estimate is given by: -/// d ~=~ floor( log_10(2) * e) +/// d ~=~ floor(log_10(2) * e) /// \param f: a floating point expression /// \param spec: specification for floating point exprt estimate_decimal_exponent(const exprt &f, const ieee_float_spect &spec) @@ -136,13 +141,13 @@ exprt estimate_decimal_exponent(const exprt &f, const ieee_float_spect &spec) exprt float_bin_exp=floatbv_of_int_expr(bin_exp, spec); exprt dec_exp=floatbv_mult(float_bin_exp, log_10_of_2); binary_relation_exprt negative_exp(dec_exp, ID_lt, constant_float(0.0, spec)); - // Rounding to zero is not correct for negative number, so we remove 1. + // Rounding to zero is not correct for negative numbers, so we substract 1. minus_exprt dec_minus_one(dec_exp, constant_float(1.0, spec)); if_exprt adjust_for_neg(negative_exp, dec_minus_one, dec_exp); return round_expr_to_zero(adjust_for_neg); } -/// add axioms corresponding to the String.valueOf(F) java function +/// Add axioms corresponding to the String.valueOf(F) java function /// \param f: function application with one float argument /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_from_float( @@ -152,7 +157,7 @@ string_exprt string_constraint_generatort::add_axioms_from_float( return add_axioms_from_float(args(f, 1)[0], ref_type); } -/// add axioms corresponding to the String.valueOf(D) java function +/// Add axioms corresponding to the String.valueOf(D) java function /// \param f: function application with one double argument /// \return a new string expression string_exprt string_constraint_generatort::add_axioms_from_double( @@ -162,7 +167,7 @@ string_exprt string_constraint_generatort::add_axioms_from_double( return add_axioms_from_float(args(f, 1)[0], ref_type); } -/// add axioms corresponding to the integer part of m, in decimal form with no +/// Add axioms corresponding to the integer part of m, in decimal form with no /// leading zeroes, followed by '.' ('\u002E'), followed by one or more decimal /// digits representing the fractional part of m. /// From 4eacbd359f37dfed5958fcac85f71cf5fca8ba9f Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 21 Jun 2017 15:51:01 +0100 Subject: [PATCH 12/15] Renaming add_axioms_from_float to add_axioms_for_string_of_float This function name is more explicit about what the function does --- src/solvers/refinement/string_constraint_generator.h | 5 +++-- .../string_constraint_generator_concat.cpp | 4 ++-- .../refinement/string_constraint_generator_float.cpp | 12 ++++++------ .../string_constraint_generator_insert.cpp | 4 ++-- .../refinement/string_constraint_generator_main.cpp | 2 +- 5 files changed, 14 insertions(+), 13 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 6812a28cf0d..ca8bf17b5f0 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -236,8 +236,9 @@ class string_constraint_generatort // and minus infinity the string are "Infinity" and "-Infinity respectively // otherwise the string contains only characters in [0123456789.] and '-' at // the start for negative number - string_exprt add_axioms_from_float(const function_application_exprt &f); - string_exprt add_axioms_from_float( + string_exprt add_axioms_for_string_of_float( + const function_application_exprt &f); + string_exprt add_axioms_for_string_of_float( const exprt &f, const refined_string_typet &ref_type); string_exprt add_axioms_for_fractional_part( diff --git a/src/solvers/refinement/string_constraint_generator_concat.cpp b/src/solvers/refinement/string_constraint_generator_concat.cpp index 72dd10b2ae5..1a157bbd859 100644 --- a/src/solvers/refinement/string_constraint_generator_concat.cpp +++ b/src/solvers/refinement/string_constraint_generator_concat.cpp @@ -174,7 +174,7 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_double( string_exprt s1=get_string_expr(args(f, 2)[0]); PRECONDITION(refined_string_typet::is_refined_string_type(f.type())); refined_string_typet ref_type=to_refined_string_type(f.type()); - string_exprt s2=add_axioms_from_float(args(f, 2)[1], ref_type, true); + string_exprt s2=add_axioms_for_string_of_float(args(f, 2)[1], ref_type); return add_axioms_for_concat(s1, s2); } @@ -187,7 +187,7 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_float( string_exprt s1=get_string_expr(args(f, 2)[0]); PRECONDITION(refined_string_typet::is_refined_string_type(f.type())); refined_string_typet ref_type=to_refined_string_type(f.type()); - string_exprt s2=add_axioms_from_float(args(f, 2)[1], ref_type, false); + string_exprt s2=add_axioms_for_string_of_float(args(f, 2)[1], ref_type); return add_axioms_for_concat(s1, s2); } diff --git a/src/solvers/refinement/string_constraint_generator_float.cpp b/src/solvers/refinement/string_constraint_generator_float.cpp index 7b79d1072ad..b85abd49ae7 100644 --- a/src/solvers/refinement/string_constraint_generator_float.cpp +++ b/src/solvers/refinement/string_constraint_generator_float.cpp @@ -150,11 +150,11 @@ exprt estimate_decimal_exponent(const exprt &f, const ieee_float_spect &spec) /// Add axioms corresponding to the String.valueOf(F) java function /// \param f: function application with one float argument /// \return a new string expression -string_exprt string_constraint_generatort::add_axioms_from_float( +string_exprt string_constraint_generatort::add_axioms_for_string_of_float( const function_application_exprt &f) { - const refined_string_typet &ref_type=to_refined_string_type(f.type()); - return add_axioms_from_float(args(f, 1)[0], ref_type); + return add_axioms_for_string_of_float( + args(f, 1)[0], to_refined_string_type(f.type())); } /// Add axioms corresponding to the String.valueOf(D) java function @@ -163,8 +163,8 @@ string_exprt string_constraint_generatort::add_axioms_from_float( string_exprt string_constraint_generatort::add_axioms_from_double( const function_application_exprt &f) { - const refined_string_typet &ref_type=to_refined_string_type(f.type()); - return add_axioms_from_float(args(f, 1)[0], ref_type); + return add_axioms_for_string_of_float( + args(f, 1)[0], to_refined_string_type(f.type())); } /// Add axioms corresponding to the integer part of m, in decimal form with no @@ -176,7 +176,7 @@ string_exprt string_constraint_generatort::add_axioms_from_double( /// \param f: expression representing a float /// \param ref_type: refined type for strings /// \return a new string expression -string_exprt string_constraint_generatort::add_axioms_from_float( +string_exprt string_constraint_generatort::add_axioms_for_string_of_float( const exprt &f, const refined_string_typet &ref_type) { const floatbv_typet &type=to_floatbv_type(f.type()); diff --git a/src/solvers/refinement/string_constraint_generator_insert.cpp b/src/solvers/refinement/string_constraint_generator_insert.cpp index b0424fd6f87..b7a0a381bad 100644 --- a/src/solvers/refinement/string_constraint_generator_insert.cpp +++ b/src/solvers/refinement/string_constraint_generator_insert.cpp @@ -119,7 +119,7 @@ string_exprt string_constraint_generatort::add_axioms_for_insert_double( { string_exprt s1=get_string_expr(args(f, 3)[0]); const refined_string_typet &ref_type=to_refined_string_type(s1.type()); - string_exprt s2=add_axioms_from_float(args(f, 3)[2], ref_type); + string_exprt s2=add_axioms_for_string_of_float(args(f, 3)[2], ref_type); return add_axioms_for_insert(s1, s2, args(f, 3)[1]); } @@ -133,7 +133,7 @@ string_exprt string_constraint_generatort::add_axioms_for_insert_float( { string_exprt s1=get_string_expr(args(f, 3)[0]); const refined_string_typet &ref_type=to_refined_string_type(s1.type()); - string_exprt s2=add_axioms_from_float(args(f, 3)[2], ref_type); + string_exprt s2=add_axioms_for_string_of_float(args(f, 3)[2], ref_type); return add_axioms_for_insert(s1, s2, args(f, 3)[1]); } diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 11b1a0aa893..8ac4f30f26c 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -453,7 +453,7 @@ exprt string_constraint_generatort::add_axioms_for_function_application( else if(id==ID_cprover_string_of_int_hex_func) res=add_axioms_from_int_hex(expr); else if(id==ID_cprover_string_of_float_func) - res=add_axioms_from_float(expr); + res=add_axioms_for_string_of_float(expr); else if(id==ID_cprover_string_of_float_scientific_notation_func) res=add_axioms_from_float_scientific_notation(expr); else if(id==ID_cprover_string_of_double_func) From cae6d279b5522ca9e36c5b09163e0f41b7668f2b Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 21 Jun 2017 15:57:19 +0100 Subject: [PATCH 13/15] Style improvements in string_constraint_generator_float.cpp Defining a constant for the maximal value not using scientific notation Adding precondition on the max_size given to fractional part Renaming i argument to int_expr Making comments correspond to added axioms in float to string conversion Replacing magnitude by fraction and improving comments Replacing hexadecimal float number by decimal Hexadecimals are not supported by all compilers Editing TODO in string of float which should be part of specifications Typo in comment (from -> form) --- .../string_constraint_generator_float.cpp | 164 ++++++++++-------- 1 file changed, 87 insertions(+), 77 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_float.cpp b/src/solvers/refinement/string_constraint_generator_float.cpp index b85abd49ae7..0bbb9ae6efa 100644 --- a/src/solvers/refinement/string_constraint_generator_float.cpp +++ b/src/solvers/refinement/string_constraint_generator_float.cpp @@ -30,18 +30,18 @@ exprt get_exponent( exprt exp_bits=extractbits_exprt( src, spec.f+spec.e-1, spec.f, unsignedbv_typet(spec.e)); - // Exponent is in biased from (numbers from -128 to 127 are encoded with + // Exponent is in biased form (numbers from -128 to 127 are encoded with // integer from 0 to 255) we have to remove the bias. return minus_exprt( typecast_exprt(exp_bits, signedbv_typet(32)), from_integer(spec.bias(), signedbv_typet(32))); } -/// Gets the magnitude without hidden bit +/// Gets the fraction without hidden bit /// \param src: a floating point expression /// \param spec: specification for floating points -/// \return An unsigned value representing the magnitude. -exprt get_magnitude(const exprt &src, const ieee_float_spect &spec) +/// \return An unsigned value representing the fractional part. +exprt get_fraction(const exprt &src, const ieee_float_spect &spec) { return extractbits_exprt(src, spec.f-1, 0, unsignedbv_typet(spec.f)); } @@ -61,12 +61,12 @@ exprt get_significand( { PRECONDITION(type.id()==ID_unsignedbv); PRECONDITION(to_unsignedbv_type(type).get_width()>spec.f); - typecast_exprt magnitude(get_magnitude(src, spec), type); + typecast_exprt fraction(get_fraction(src, spec), type); exprt exponent=get_exponent(src, spec); equal_exprt all_zeros(exponent, from_integer(0, exponent.type())); exprt hidden_bit=from_integer((1 << spec.f), type); - plus_exprt with_hidden_bit(magnitude, hidden_bit); - return if_exprt(all_zeros, magnitude, with_hidden_bit); + bitor_exprt with_hidden_bit(fraction, hidden_bit); + return if_exprt(all_zeros, fraction, with_hidden_bit); } /// Create an expression to represent a float or double value. @@ -126,9 +126,9 @@ exprt floatbv_of_int_expr(const exprt &i, const ieee_float_spect &spec) /// floating point value in decimal. /// We are looking for d such that n * 10^d = m * 2^e, so: /// d = log_10(m) + log_10(2) * e - log_10(n) -/// m -- the magnitude -- should be between 1 and 2 so log_10(m) +/// m -- the fraction -- should be between 1 and 2 so log_10(m) /// in [0,log_10(2)]. -/// n -- the magnitude in base 10 -- should be between 1 and 10 so +/// n -- the fraction in base 10 -- should be between 1 and 10 so /// log_10(n) in [0, 1]. /// So the estimate is given by: /// d ~=~ floor(log_10(2) * e) @@ -169,10 +169,12 @@ string_exprt string_constraint_generatort::add_axioms_from_double( /// Add axioms corresponding to the integer part of m, in decimal form with no /// leading zeroes, followed by '.' ('\u002E'), followed by one or more decimal -/// digits representing the fractional part of m. +/// digits representing the fractional part of m. This specification is correct +/// for inputs that do not exceed 100000 and the function is unspecified for +/// other values. /// /// TODO: this specification is not correct for negative numbers and -/// double precision and floating point value that exceed 100000 +/// double precision /// \param f: expression representing a float /// \param ref_type: refined type for strings /// \return a new string expression @@ -186,15 +188,17 @@ string_exprt string_constraint_generatort::add_axioms_for_string_of_float( // shifted is floor(f * 1e5) exprt shifting=constant_float(1e5, float_spec); exprt shifted=round_expr_to_zero(floatbv_mult(f, shifting)); + // Numbers with greater or equal value to the following, should use + // the exponent notation. + exprt max_non_exponent_notation=from_integer(100000, shifted.type()); // fractional_part is floor(f * 100000) % 100000 - mod_exprt fractional_part(shifted, from_integer(100000, shifted.type())); + mod_exprt fractional_part(shifted, max_non_exponent_notation); string_exprt fractional_part_str= add_axioms_for_fractional_part(fractional_part, 6, ref_type); - // The axiom added to convert to integer should always been satisfiable even - // when the precondition are not satisfied. - mod_exprt integer_part( - round_expr_to_zero(f), from_integer(1000000, shifted.type())); + // The axiom added to convert to integer should always be satisfiable even + // when the preconditions are not satisfied. + mod_exprt integer_part(round_expr_to_zero(f), max_non_exponent_notation); // We should not need more than 8 characters to represent the integer // part of the float. string_exprt integer_part_str=add_axioms_from_int(integer_part, 8, ref_type); @@ -202,17 +206,19 @@ string_exprt string_constraint_generatort::add_axioms_for_string_of_float( return add_axioms_for_concat(integer_part_str, fractional_part_str); } -/// add axioms for representing the fractional part of a floating point starting +/// Add axioms for representing the fractional part of a floating point starting /// with a dot -/// \param i: an integer expression -/// \param max_size: a maximal size for the string +/// \param int_expr: an integer expression +/// \param max_size: a maximal size for the string, this includes the +/// potential minus sign and therefore should be greater than 2 /// \param ref_type: a type for refined strings /// \return a string expression string_exprt string_constraint_generatort::add_axioms_for_fractional_part( - const exprt &i, size_t max_size, const refined_string_typet &ref_type) + const exprt &int_expr, size_t max_size, const refined_string_typet &ref_type) { - PRECONDITION(i.type().id()==ID_signedbv); - const typet &type=i.type(); + PRECONDITION(int_expr.type().id()==ID_signedbv); + PRECONDITION(max_size>=2); + const typet &type=int_expr.type(); string_exprt res=fresh_string(ref_type); exprt ten=from_integer(10, type); const typet &char_type=ref_type.get_char_type(); @@ -223,11 +229,11 @@ string_exprt string_constraint_generatort::add_axioms_for_fractional_part( // We add axioms: // a1 : 2 <= |res| <= max_size - // a2 : forall 1 <= i < size '0' < res[i] < '9' - // res[0] = '.' - // a3 : i = sum_j 10^j res[j] - '0' - // for all j : !(|res| = j+1 && res[j]='0') - // for all j : |res| <= j => res[j]='0' + // a2 : starts_with_dot && no_trailing_zero && is_number + // starts_with_dot: res[0] = '.' + // is_number: forall i:[1, max_size[. '0' < res[i] < '9' + // no_trailing_zero: forall j:[2, max_size[. !(|res| = j+1 && res[j] = '0') + // a3 : int_expr = sum_j 10^j (j < |res| ? res[j] - '0' : 0) and_exprt a1(res.axiom_for_is_strictly_longer_than(1), res.axiom_for_is_shorter_than(max)); @@ -241,11 +247,12 @@ string_exprt string_constraint_generatort::add_axioms_for_fractional_part( for(size_t j=1; j two_power_e_over_ten_power_d_table( - {1, 2, 4, 8, 1.6, 3.2, 6.4, 1.28, 2.56, - 5.12, 1.024, 2.048, 4.096, 8.192, 1.6384, 3.2768, 6.5536, - 1.31072, 2.62144, 5.24288, 1.04858, 2.09715, 4.19430, 8.38861, 1.67772, - 3.35544, 6.71089, 1.34218, 2.68435, 5.36871, 1.07374, 2.14748, 4.29497, - 8.58993, 1.71799, 3.43597, 6.87195, 1.37439, 2.74878, 5.49756, 1.09951, - 2.19902, 4.39805, 8.79609, 1.75922, 3.51844, 7.03687, 1.40737, 2.81475, - 5.62950, 1.12590, 2.25180, 4.50360, 9.00720, 1.80144, 3.60288, 7.20576, - 1.44115, 2.88230, 5.76461, 1.15292, 2.30584, 4.61169, 9.22337, 1.84467, - 3.68935, 7.37870, 1.47574, 2.95148, 5.90296, 1.18059, 2.36118, 4.72237, - 9.44473, 1.88895, 3.77789, 7.55579, 1.51116, 3.02231, 6.04463, 1.20893, - 2.41785, 4.83570, 9.67141, 1.93428, 3.86856, 7.73713, 1.54743, 3.09485, - 6.18970, 1.23794, 2.47588, 4.95176, 9.90352, 1.98070, 3.96141, 7.92282, - 1.58456, 3.16913, 6.33825, 1.26765, 2.53530, 5.07060, 1.01412, 2.02824, - 4.05648, 8.11296, 1.62259, 3.24519, 6.49037, 1.29807, 2.59615, 5.1923, - 1.03846, 2.07692, 4.15384, 8.30767, 1.66153, 3.32307, 6.64614, 1.32923, - 2.65846, 5.31691, 1.06338, 2.12676, 4.25353, 8.50706, 1.70141}); + { 1, 2, 4, 8, 1.6, 3.2, 6.4, 1.28, 2.56, + 5.12, 1.024, 2.048, 4.096, 8.192, 1.6384, 3.2768, 6.5536, + 1.31072, 2.62144, 5.24288, 1.04858, 2.09715, 4.19430, 8.38861, 1.67772, + 3.35544, 6.71089, 1.34218, 2.68435, 5.36871, 1.07374, 2.14748, 4.29497, + 8.58993, 1.71799, 3.43597, 6.87195, 1.37439, 2.74878, 5.49756, 1.09951, + 2.19902, 4.39805, 8.79609, 1.75922, 3.51844, 7.03687, 1.40737, 2.81475, + 5.62950, 1.12590, 2.25180, 4.50360, 9.00720, 1.80144, 3.60288, 7.20576, + 1.44115, 2.88230, 5.76461, 1.15292, 2.30584, 4.61169, 9.22337, 1.84467, + 3.68935, 7.37870, 1.47574, 2.95148, 5.90296, 1.18059, 2.36118, 4.72237, + 9.44473, 1.88895, 3.77789, 7.55579, 1.51116, 3.02231, 6.04463, 1.20893, + 2.41785, 4.83570, 9.67141, 1.93428, 3.86856, 7.73713, 1.54743, 3.09485, + 6.18970, 1.23794, 2.47588, 4.95176, 9.90352, 1.98070, 3.96141, 7.92282, + 1.58456, 3.16913, 6.33825, 1.26765, 2.53530, 5.07060, 1.01412, 2.02824, + 4.05648, 8.11296, 1.62259, 3.24519, 6.49037, 1.29807, 2.59615, 5.1923, + 1.03846, 2.07692, 4.15384, 8.30767, 1.66153, 3.32307, 6.64614, 1.32923, + 2.65846, 5.31691, 1.06338, 2.12676, 4.25353, 8.50706, 1.70141}); // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[-128,-1] std::vector two_power_e_over_ten_power_d_table_negatives( - { 2.93874, 5.87747, 1.17549, 2.35099, 4.70198, 9.40395, 1.88079, 3.76158, - 7.52316, 1.50463, 3.00927, 6.01853, 1.20371, 2.40741, 4.81482, 9.62965, - 1.92593, 3.85186, 7.70372, 1.54074, 3.08149, 6.16298, 1.23260, 2.46519, - 4.93038, 9.86076, 1.97215, 3.94430, 7.88861, 1.57772, 3.15544, 6.31089, - 1.26218, 2.52435, 5.04871, 1.00974, 2.01948, 4.03897, 8.07794, 1.61559, - 3.23117, 6.46235, 1.29247, 2.58494, 5.16988, 1.03398, 2.06795, 4.13590, - 8.27181, 1.65436, 3.30872, 6.61744, 1.32349, 2.64698, 5.29396, 1.05879, - 2.11758, 4.23516, 8.47033, 1.69407, 3.38813, 6.77626, 1.35525, 2.71051, - 5.42101, 1.08420, 2.16840, 4.33681, 8.67362, 1.73472, 3.46945, 6.93889, - 1.38778, 2.77556, 5.55112, 1.11022, 2.22045, 4.44089, 8.88178, 1.77636, - 3.55271, 7.10543, 1.42109, 2.84217, 5.68434, 1.13687, 2.27374, 4.54747, - 9.09495, 1.81899, 3.63798, 7.27596, 1.45519, 2.91038, 5.82077, 1.16415, - 2.32831, 4.65661, 9.31323, 1.86265, 3.72529, 7.45058, 1.49012, 2.98023, - 5.96046, 1.19209, 2.38419, 4.76837, 9.53674, 1.90735, 3.81470, 7.62939, - 1.52588, 3.05176, 6.10352, 1.22070, 2.44141, 4.88281, 9.76563, 1.95313, - 3.90625, 7.81250, 1.56250, 3.12500, 6.25000, 1.25000, 2.50000, 5}); + { 2.93874, 5.87747, 1.17549, 2.35099, 4.70198, 9.40395, 1.88079, 3.76158, + 7.52316, 1.50463, 3.00927, 6.01853, 1.20371, 2.40741, 4.81482, 9.62965, + 1.92593, 3.85186, 7.70372, 1.54074, 3.08149, 6.16298, 1.23260, 2.46519, + 4.93038, 9.86076, 1.97215, 3.94430, 7.88861, 1.57772, 3.15544, 6.31089, + 1.26218, 2.52435, 5.04871, 1.00974, 2.01948, 4.03897, 8.07794, 1.61559, + 3.23117, 6.46235, 1.29247, 2.58494, 5.16988, 1.03398, 2.06795, 4.13590, + 8.27181, 1.65436, 3.30872, 6.61744, 1.32349, 2.64698, 5.29396, 1.05879, + 2.11758, 4.23516, 8.47033, 1.69407, 3.38813, 6.77626, 1.35525, 2.71051, + 5.42101, 1.08420, 2.16840, 4.33681, 8.67362, 1.73472, 3.46945, 6.93889, + 1.38778, 2.77556, 5.55112, 1.11022, 2.22045, 4.44089, 8.88178, 1.77636, + 3.55271, 7.10543, 1.42109, 2.84217, 5.68434, 1.13687, 2.27374, 4.54747, + 9.09495, 1.81899, 3.63798, 7.27596, 1.45519, 2.91038, 5.82077, 1.16415, + 2.32831, 4.65661, 9.31323, 1.86265, 3.72529, 7.45058, 1.49012, 2.98023, + 5.96046, 1.19209, 2.38419, 4.76837, 9.53674, 1.90735, 3.81470, 7.62939, + 1.52588, 3.05176, 6.10352, 1.22070, 2.44141, 4.88281, 9.76563, 1.95313, + 3.90625, 7.81250, 1.56250, 3.12500, 6.25000, 1.25000, 2.50000, 5}); // bias_table used to find the bias factor exprt conversion_factor_table_size=from_integer( @@ -392,7 +399,7 @@ string_exprt string_constraint_generatort:: plus_exprt(dec_exponent_estimate, from_integer(1, int_type)), dec_exponent_estimate); - // `dec_significand` is divided by 10 if it exeeds 10 + // `dec_significand` is divided by 10 if it exceeds 10 dec_significand=if_exprt( estimate_too_small, floatbv_mult(dec_significand, constant_float(0.1, float_spec)), @@ -409,9 +416,12 @@ string_exprt string_constraint_generatort:: exprt shifted_float= round_expr_to_zero(floatbv_mult(fractional_part, shifting)); + // Numbers with greater or equal value to the following, should use + // the exponent notation. + exprt max_non_exponent_notation=from_integer(100000, shifted_float.type()); + // fractional_part_shifted is floor(f * 100000) % 100000 - mod_exprt fractional_part_shifted( - shifted_float, from_integer(100000, shifted_float.type())); + mod_exprt fractional_part_shifted(shifted_float, max_non_exponent_notation); string_exprt string_fractional_part=add_axioms_for_fractional_part( fractional_part_shifted, 6, ref_type); @@ -421,7 +431,7 @@ string_exprt string_constraint_generatort:: string_exprt string_expr_with_fractional_part=add_axioms_for_concat( string_expr_integer_part, string_fractional_part); - // string_expr_with_E = concat(string_magnitude, string_lit_E) + // string_expr_with_E = concat(string_fraction, string_lit_E) string_exprt string_expr_with_E=add_axioms_for_concat_char( string_expr_with_fractional_part, from_integer('E', ref_type.get_char_type())); @@ -434,7 +444,7 @@ string_exprt string_constraint_generatort:: return add_axioms_for_concat(string_expr_with_E, exponent_string); } -/// add axioms corresponding to the scientific representation of floating point +/// Add axioms corresponding to the scientific representation of floating point /// values /// \param f: a function application expression /// \return a new string expression From 64558ca161dc9d6e9e188f761c41533cdfa45130 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 21 Jun 2017 16:37:23 +0100 Subject: [PATCH 14/15] Update comments in string_constraint_generator_valueof.cpp --- .../refinement/string_constraint_generator_valueof.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index 914df80ee03..c009dd6e412 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp @@ -89,8 +89,9 @@ string_exprt string_constraint_generatort::add_axioms_from_bool( return res; } -/// add axioms to say the string corresponds to the result of String.valueOf(I) -/// or String.valueOf(J) java functions applied on the integer expression +/// Add axioms enforcing that the string corresponds to the result +/// of String.valueOf(I) or String.valueOf(J) Java functions applied +/// on the integer expression. /// \param i: a signed integer expression /// \param max_size: a maximal size for the string representation /// \param ref_type: type for refined strings @@ -305,7 +306,7 @@ string_exprt string_constraint_generatort::add_axioms_from_char( } /// Add axioms stating that the returned string has length 1 and the character -/// it contains correspond to the input expression. +/// it contains corresponds to the input expression. /// \param c: one expression of type char /// \param ref_type: type of refined string expressions /// \return a new string expression From e1f2d77faf9a78415d326f36cf3047145395d1d9 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 29 Jun 2017 15:40:18 +0100 Subject: [PATCH 15/15] Adding tests for String.valueOf float Add several tests, some take long and are marked as THOROUGH, fail probably due to some problem in CBMC and are marked as KNOWNBUG. --- .../java_value_of_float_2/test.class | Bin 0 -> 672 bytes .../java_value_of_float_2/test.desc | 8 ++++++++ .../java_value_of_float_2/test.java | 9 +++++++++ .../java_value_of_float_3/test.class | Bin 0 -> 721 bytes .../java_value_of_float_3/test.desc | 9 +++++++++ .../java_value_of_float_3/test.java | 10 ++++++++++ .../java_value_of_float_4/test.class | Bin 0 -> 828 bytes .../java_value_of_float_4/test.desc | 10 ++++++++++ .../java_value_of_float_4/test.java | 13 +++++++++++++ .../java_value_of_float_5/test.class | Bin 0 -> 673 bytes .../java_value_of_float_5/test.desc | 8 ++++++++ .../java_value_of_float_5/test.java | 9 +++++++++ 12 files changed, 76 insertions(+) create mode 100644 regression/strings-smoke-tests/java_value_of_float_2/test.class create mode 100644 regression/strings-smoke-tests/java_value_of_float_2/test.desc create mode 100644 regression/strings-smoke-tests/java_value_of_float_2/test.java create mode 100644 regression/strings-smoke-tests/java_value_of_float_3/test.class create mode 100644 regression/strings-smoke-tests/java_value_of_float_3/test.desc create mode 100644 regression/strings-smoke-tests/java_value_of_float_3/test.java create mode 100644 regression/strings-smoke-tests/java_value_of_float_4/test.class create mode 100644 regression/strings-smoke-tests/java_value_of_float_4/test.desc create mode 100644 regression/strings-smoke-tests/java_value_of_float_4/test.java create mode 100644 regression/strings-smoke-tests/java_value_of_float_5/test.class create mode 100644 regression/strings-smoke-tests/java_value_of_float_5/test.desc create mode 100644 regression/strings-smoke-tests/java_value_of_float_5/test.java diff --git a/regression/strings-smoke-tests/java_value_of_float_2/test.class b/regression/strings-smoke-tests/java_value_of_float_2/test.class new file mode 100644 index 0000000000000000000000000000000000000000..7e8016e0b84e19a2ee91146383acbd9fe81932f1 GIT binary patch literal 672 zcmY*XT~8B16g_vl?R2+`Eeoyn1Cb;lD7(JBxJjWoGV~bI-Z=&Yb@F{u975?%1fHX>R}eShsNnS1nk$R>pN5 zObOhuAN9%X*Ihe-+p{aRGfed$-o}QPw9z}zQYtlLbEeCCM2(_HK z)!SEI@*mVqB0t<^`9m3`YU>T5-r8ty<~e7C74BTUPh}8m!iDQI$(1&brkW?M1w21O zqpxB=QvFedJd7me3m)DMrui8v{6JJ|>K6G_0O`(ot#LHPJMmuZ9D_bfgc5PcgvS;uim;(ibcX(^O82{ZwzAR#IQDh&q;Jp_U1&9S$wTh~GMrWbxm z^9MKsQi?zVi6b|T{1=3nb=z1Kmz~)+Z|A+8-JgHId;_q8+a`*b(eM2D_1nZ{T*;$= znt@rhnKN)z#d(fvCi0l!xNc$rH#imb1X3!t8Q@G#O(G5kt;gB zI+B+nmaRSK(6LZPg}4^#Xjr&_66xJ--LufdO-k37?_0Q~(yF4j11H>RKR$E39!33# ztf_V!%NAN_Gn7;2W^Yfp@*LEakst0b@IxmUh|O(=sd}fek)AmrJYX_@^I8>SJ-0TpPZTbQRuD$?_@a#dZNG7V%E6zXb+5Bs)cj3GEMNIi~p>p%=$SRuUUP#V(9s4Z-#I Y(6vv{)0SucRhuj_)+2SxYNB}QAHD61q5uE@ literal 0 HcmV?d00001 diff --git a/regression/strings-smoke-tests/java_value_of_float_3/test.desc b/regression/strings-smoke-tests/java_value_of_float_3/test.desc new file mode 100644 index 00000000000..771fdebe7cc --- /dev/null +++ b/regression/strings-smoke-tests/java_value_of_float_3/test.desc @@ -0,0 +1,9 @@ +KNOWNBUG +test.class +--refine-strings --function test.check +^EXIT=10$ +^SIGNAL=0$ +assertion.* file test.java line 7 .* SUCCESS$ +assertion.* file test.java line 8 .* FAILURE$ + +-- diff --git a/regression/strings-smoke-tests/java_value_of_float_3/test.java b/regression/strings-smoke-tests/java_value_of_float_3/test.java new file mode 100644 index 00000000000..47bfa2b43cf --- /dev/null +++ b/regression/strings-smoke-tests/java_value_of_float_3/test.java @@ -0,0 +1,10 @@ +public class test +{ + public static void check() + { + String s5=String.valueOf(5.67e-9f); + // The result may not be exactly 5.67E-9 as 5.66999...E-9 is also valid + assert(s5.startsWith("5.6") && s5.endsWith("E-9")); + assert(!s5.startsWith("5.6") || !s5.endsWith("E-9")); + } + } diff --git a/regression/strings-smoke-tests/java_value_of_float_4/test.class b/regression/strings-smoke-tests/java_value_of_float_4/test.class new file mode 100644 index 0000000000000000000000000000000000000000..b9330858ee9274276f68939beff183e05dd57a8a GIT binary patch literal 828 zcmZuvT~8B16g|^!JKOC7Whu3OR0R>+@=-r{gBT3j#8ApZjYi(4+W{BWt?q6~d;)() z`v-hh6EK>n&&J<`-s##F6OzrHyJyZlbMBq_b@uf;fE7G2kU@dtx^{F77`TC(+8@fa zqn|(uP8HCIG;!v2FLY7ojUU7xDSE;&f5mL2@MJ$<^ghe_}yG%P=s^ak>qNL=69~A4VQ+@kZZ}n@nvi1nI;x?XoDuagBiN93|%bC z0Q1+8pnj@i7^T7Og+uZ(U;2=iFjq$*-F1#qFLi7nCO9PAE3oQgO5%c S3`D6V5Hr`+*sk`CT>A@*mZVYu literal 0 HcmV?d00001 diff --git a/regression/strings-smoke-tests/java_value_of_float_4/test.desc b/regression/strings-smoke-tests/java_value_of_float_4/test.desc new file mode 100644 index 00000000000..7f1e0f8819a --- /dev/null +++ b/regression/strings-smoke-tests/java_value_of_float_4/test.desc @@ -0,0 +1,10 @@ +THOROUGH +test.class +--refine-strings --function test.check +^EXIT=10$ +^SIGNAL=0$ +assertion.* test.java line 8 .* SUCCESS$ +assertion.* test.java line 9 .* SUCCESS$ +assertion.* test.java line 10 .* SUCCESS$ +assertion.* test.java line 11 .* FAILURE$ +-- diff --git a/regression/strings-smoke-tests/java_value_of_float_4/test.java b/regression/strings-smoke-tests/java_value_of_float_4/test.java new file mode 100644 index 00000000000..13c1151eb7b --- /dev/null +++ b/regression/strings-smoke-tests/java_value_of_float_4/test.java @@ -0,0 +1,13 @@ +public class test +{ + public static void check() + { + String s7=String.valueOf(java.lang.Float.POSITIVE_INFINITY); + String s8=String.valueOf(java.lang.Float.NEGATIVE_INFINITY); + String s9=String.valueOf(java.lang.Float.NaN); + assert(s7.equals("Infinity")); + assert(s8.equals("-Infinity")); + assert(s9.equals("NaN")); + assert(!s7.equals("Infinity") || !s8.equals("-Infinity") || !s9.equals("NaN")); + } +} diff --git a/regression/strings-smoke-tests/java_value_of_float_5/test.class b/regression/strings-smoke-tests/java_value_of_float_5/test.class new file mode 100644 index 0000000000000000000000000000000000000000..576229eef2628e90fc4db16494a34de85f61ce5b GIT binary patch literal 673 zcmY*XT~8B16g_vl?R2+`Eeq88fr6s8HA2+l3&d#ncoF2G#6;ev+YuJlt?mbjKgIq5 zpVb76CYt!@Kk*OvWQ=zf>Eg@G+%xB%bMKw`@#phb03F=6Q9;A}{_E!(8y9fVf`vn74W*p#m_T;MvPyzB-4MC|S$jXbsP>l7sSILGICFg>xzys>RP&^j zfCosZ_f_misz0ibr;((5!PDEpEWbmAUx;cA-6Nk0Al*8zHIAlvC*F(gW6*m|#5k{| z4CHyi9Z~mSWay%6d_v*L2be=lw%y_pN<&n>Ks-N2`P*6eZ4PT`Ba?PvYCpCpvAf{E zQ^o`%7L4Eet4!7zm>RiuGEZRKwT@s9A