string_constraint_generator_valueof.cpp

Go to the documentation of this file.

/*******************************************************************\
 
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
 
\*******************************************************************/

 
#include "string_constraint_generator.h"
 
#include <util/deprecate.h>
#include <util/mathematical_expr.h>
#include <util/simplify_expr.h>
 
#include <cmath>

static unsigned long to_integer_or_default(
  const exprt &expr,
  unsigned long def,
  const namespacet &ns)
{
  if(const auto i = numeric_cast<unsigned long>(simplify_expr(expr, ns)))
    return *i;
  return def;
}

DEPRECATED(SINCE(2017, 10, 5, "use add_axioms_for_string_of_int instead"))
std::pair<exprt, string_constraintst>
string_constraint_generatort::add_axioms_from_long(
  const function_application_exprt &f)
{
  PRECONDITION(f.arguments().size() == 3 || f.arguments().size() == 4);
  const array_string_exprt res =
    array_pool.find(f.arguments()[1], f.arguments()[0]);
  if(f.arguments().size() == 4)
    return add_axioms_for_string_of_int_with_radix(
      res, f.arguments()[2], f.arguments()[3], 0);
  else
    return add_axioms_for_string_of_int(res, f.arguments()[2], 0);
}

DEPRECATED(SINCE(2017, 10, 5, "Java specific, should be implemented in Java"))
std::pair<exprt, string_constraintst>
string_constraint_generatort::add_axioms_from_bool(
  const array_string_exprt &res,
  const exprt &b)
{
  const typet &char_type = to_type_with_subtype(res.content().type()).subtype();
  PRECONDITION(b.type() == bool_typet() || b.type().id() == ID_c_bool);
  string_constraintst constraints;
  typecast_exprt eq(b, bool_typet());
 
  // We add axioms:
  // a1 : eq => res = |"true"|
  // a2 : forall i < |"true"|. eq => res[i]="true"[i]
  // a3 : !eq => res = |"false"|
  // a4 : forall i < |"false"|. !eq => res[i]="false"[i]
 
  std::string str_true = "true";
  const implies_exprt a1(
    eq, equal_to(array_pool.get_or_create_length(res), str_true.length()));
  constraints.existential.push_back(a1);
 
  for(std::size_t i = 0; i < str_true.length(); i++)
  {
    exprt chr = from_integer(str_true[i], char_type);
    implies_exprt a2(eq, equal_exprt(res[i], chr));
    constraints.existential.push_back(a2);
  }
 
  std::string str_false = "false";
  const implies_exprt a3(
    not_exprt(eq),
    equal_to(array_pool.get_or_create_length(res), str_false.length()));
  constraints.existential.push_back(a3);
 
  for(std::size_t i = 0; i < str_false.length(); i++)
  {
    exprt chr = from_integer(str_false[i], char_type);
    implies_exprt a4(not_exprt(eq), equal_exprt(res[i], chr));
    constraints.existential.push_back(a4);
  }
 
  return {from_integer(0, get_return_code_type()), std::move(constraints)};
}

std::pair<exprt, string_constraintst>
string_constraint_generatort::add_axioms_for_string_of_int(
  const array_string_exprt &res,
  const exprt &input_int,
  size_t max_size)
{
  const constant_exprt radix = from_integer(10, input_int.type());
  return add_axioms_for_string_of_int_with_radix(
    res, input_int, radix, max_size);
}

std::pair<exprt, string_constraintst>
string_constraint_generatort::add_axioms_for_string_of_int_with_radix(
  const array_string_exprt &res,
  const exprt &input_int,
  const exprt &radix,
  size_t max_size)
{
  PRECONDITION(max_size < std::numeric_limits<size_t>::max());
  const typet &type = input_int.type();
  PRECONDITION(type.id() == ID_signedbv);

  const unsigned long radix_ul = to_integer_or_default(radix, 0, ns);
  CHECK_RETURN((radix_ul >= 2 && radix_ul <= 36) || radix_ul == 0);
 
  if(max_size == 0)
  {
    max_size = max_printed_string_length(type, radix_ul);
    CHECK_RETURN(max_size < std::numeric_limits<size_t>::max());
  }
 
  const typet &char_type = to_type_with_subtype(res.content().type()).subtype();
  const typecast_exprt radix_as_char(radix, char_type);
  const typecast_exprt radix_input_type(radix, type);
  const bool strict_formatting = true;
 
  auto result1 = get_conjuncts_for_correct_number_format(
    res, radix_as_char, radix_ul, max_size, strict_formatting);
  auto result2 = add_axioms_for_characters_in_integer_string(
    input_int,
    type,
    strict_formatting,
    res,
    max_size,
    radix_input_type,
    radix_ul);
  result2.existential.push_back(conjunction(std::move(result1)));
  return {from_integer(0, get_return_code_type()), std::move(result2)};
}

static exprt int_of_hex_char(const exprt &chr)
{
  const exprt zero_char = from_integer('0', chr.type());
  const exprt nine_char = from_integer('9', chr.type());
  const exprt a_char = from_integer('a', chr.type());
  return if_exprt(
    binary_relation_exprt(chr, ID_gt, nine_char),
    plus_exprt(from_integer(10, chr.type()), minus_exprt(chr, a_char)),
    minus_exprt(chr, zero_char));
}

DEPRECATED(SINCE(2017, 10, 5, "use add_axioms_for_string_of_int_with_radix"))
std::pair<exprt, string_constraintst>
string_constraint_generatort::add_axioms_from_int_hex(
  const array_string_exprt &res,
  const exprt &i)
{
  const typet &type = i.type();
  PRECONDITION(type.id() == ID_signedbv);
  string_constraintst constraints;
  const typet &index_type = res.length_type();
  const typet &char_type = to_type_with_subtype(res.content().type()).subtype();
  exprt sixteen = from_integer(16, index_type);
  exprt minus_char = from_integer('-', char_type);
  exprt zero_char = from_integer('0', char_type);
  exprt nine_char = from_integer('9', char_type);
  exprt a_char = from_integer('a', char_type);
  exprt f_char = from_integer('f', char_type);
 
  size_t max_size = 8;
  constraints.existential.push_back(and_exprt(
    greater_than(array_pool.get_or_create_length(res), 0),
    less_than_or_equal_to(array_pool.get_or_create_length(res), max_size)));
 
  for(size_t size = 1; size <= max_size; size++)
  {
    exprt sum = from_integer(0, type);
    exprt all_numbers = true_exprt();
    exprt chr = res[0];
 
    for(size_t j = 0; j < size; j++)
    {
      chr = res[j];
      exprt chr_int = int_of_hex_char(chr);
      sum = plus_exprt(mult_exprt(sum, sixteen), typecast_exprt(chr_int, type));
      or_exprt is_number(
        and_exprt(
          binary_relation_exprt(chr, ID_ge, zero_char),
          binary_relation_exprt(chr, ID_le, nine_char)),
        and_exprt(
          binary_relation_exprt(chr, ID_ge, a_char),
          binary_relation_exprt(chr, ID_le, f_char)));
      all_numbers = and_exprt(all_numbers, is_number);
    }
 
    const equal_exprt premise =
      equal_to(array_pool.get_or_create_length(res), size);
    constraints.existential.push_back(
      implies_exprt(premise, and_exprt(equal_exprt(i, sum), all_numbers)));
 
    // disallow 0s at the beginning
    if(size > 1)
      constraints.existential.push_back(
        implies_exprt(premise, not_exprt(equal_exprt(res[0], zero_char))));
  }
  return {from_integer(0, get_return_code_type()), std::move(constraints)};
}

std::pair<exprt, string_constraintst>
string_constraint_generatort::add_axioms_from_int_hex(
  const function_application_exprt &f)
{
  PRECONDITION(f.arguments().size() == 3);
  const array_string_exprt res =
    array_pool.find(f.arguments()[1], f.arguments()[0]);
  return add_axioms_from_int_hex(res, f.arguments()[2]);
}

std::vector<exprt>
string_constraint_generatort::get_conjuncts_for_correct_number_format(
  const array_string_exprt &str,
  const exprt &radix_as_char,
  const unsigned long radix_ul,
  const std::size_t max_size,
  const bool strict_formatting)
{
  std::vector<exprt> conjuncts;
  const typet &char_type = to_type_with_subtype(str.content().type()).subtype();
  const typet &index_type = str.length_type();
 
  const exprt &chr = str[0];
  const equal_exprt starts_with_minus(chr, from_integer('-', char_type));
  const equal_exprt starts_with_plus(chr, from_integer('+', char_type));
  const exprt starts_with_digit =
    is_digit_with_radix(chr, strict_formatting, radix_as_char, radix_ul);
 
  // |str| > 0
  const exprt non_empty = greater_or_equal_to(
    array_pool.get_or_create_length(str), from_integer(1, index_type));
  conjuncts.push_back(non_empty);
 
  if(strict_formatting)
  {
    // str[0] = '-' || is_digit_with_radix(str[0], radix)
    const or_exprt correct_first(starts_with_minus, starts_with_digit);
    conjuncts.push_back(correct_first);
  }
  else
  {
    // str[0] = '-' || str[0] = '+' || is_digit_with_radix(str[0], radix)
    const or_exprt correct_first(
      starts_with_minus, starts_with_digit, starts_with_plus);
    conjuncts.push_back(correct_first);
  }
 
  // str[0]='+' or '-' ==> |str| > 1
  const implies_exprt contains_digit(
    or_exprt(starts_with_minus, starts_with_plus),
    greater_or_equal_to(
      array_pool.get_or_create_length(str), from_integer(2, index_type)));
  conjuncts.push_back(contains_digit);
 
  // |str| <= max_size
  conjuncts.push_back(
    less_than_or_equal_to(array_pool.get_or_create_length(str), max_size));
 
  // forall 1 <= i < |str| . is_digit_with_radix(str[i], radix)
  // We unfold the above because we know that it will be used for all i up to
  // |str|, and |str| <= max_size.
  for(std::size_t index = 1; index < max_size; ++index)
  {
    const implies_exprt character_at_index_is_digit(
      greater_or_equal_to(
        array_pool.get_or_create_length(str),
        from_integer(index + 1, index_type)),
      is_digit_with_radix(
        str[index], strict_formatting, radix_as_char, radix_ul));
    conjuncts.push_back(character_at_index_is_digit);
  }
 
  if(strict_formatting)
  {
    const exprt zero_char = from_integer('0', char_type);
 
    // no_leading_zero : str[0] = '0' => |str| = 1
    const implies_exprt no_leading_zero(
      equal_exprt(chr, zero_char),
      equal_to(
        array_pool.get_or_create_length(str), from_integer(1, index_type)));
    conjuncts.push_back(no_leading_zero);
 
    // no_leading_zero_after_minus : str[0]='-' => str[1]!='0'
    implies_exprt no_leading_zero_after_minus(
      starts_with_minus, not_exprt(equal_exprt(str[1], zero_char)));
    conjuncts.push_back(no_leading_zero_after_minus);
  }
  return conjuncts;
}

string_constraintst
string_constraint_generatort::add_axioms_for_characters_in_integer_string(
  const exprt &input_int,
  const typet &type,
  const bool strict_formatting,
  const array_string_exprt &str,
  const std::size_t max_string_length,
  const exprt &radix,
  const unsigned long radix_ul)
{
  string_constraintst constraints;
  const typet &char_type = to_type_with_subtype(str.content().type()).subtype();
 
  const equal_exprt starts_with_minus(str[0], from_integer('-', char_type));
  const constant_exprt zero_expr = from_integer(0, type);
 
  exprt sum = get_numeric_value_from_character(
    str[0], char_type, type, strict_formatting, radix_ul);

  constraints.existential.push_back(implies_exprt(
    equal_to(array_pool.get_or_create_length(str), 1),
    equal_exprt(input_int, sum)));
 
  for(size_t size = 2; size <= max_string_length; size++)
  {
    // sum_0 := numeric value of res[0] (which is 0 if res[0] is '-')
    // For each 1<=j<max_string_length, we have:
    // sum_j := radix * sum_{j-1} + numeric value of res[j]
    // no_overflow_j := sum_{j-1} == (radix * sum_{j-1} / radix)
    //                  && sum_j >= sum_{j - 1}
    //   (the first part avoid overflows in the multiplication and the second
    //     one in the addition of the definition of sum_j)
    // For all 1<=size<=max_string_length we add axioms:
    // a5 : |res| >= size => no_overflow_j (only added when overflow possible)
    // a6 : |res| == size && res[0] is a digit for radix =>
    //        input_int == sum_{size-1}
    // a7 : |res| == size && res[0] == '-' => input_int == -sum_{size-1}
 
    const mult_exprt radix_sum(sum, radix);
    // new_sum = radix * sum + (numeric value of res[j])
    const exprt new_sum = plus_exprt(
      radix_sum,
      get_numeric_value_from_character(
        str[size - 1], char_type, type, strict_formatting, radix_ul));
 
    // An overflow can happen when reaching the last index which can contain
    // a digit, which is `max_string_length - 2` because of the space left for
    // a minus sign. That assumes that we were able to identify the radix. If we
    // weren't then we check for overflow on every index.
    std::optional<exprt> no_overflow;
    if(size - 1 >= max_string_length - 2 || radix_ul == 0)
    {
      no_overflow = and_exprt{equal_exprt(sum, div_exprt(radix_sum, radix)),
                              binary_relation_exprt(new_sum, ID_ge, radix_sum)};
    }
    sum = new_sum;
 
    exprt length_expr = array_pool.get_or_create_length(str);
 
    if(no_overflow.has_value())
    {
      const binary_predicate_exprt string_length_ge_size{
        length_expr, ID_ge, from_integer(size, length_expr.type())};
      const implies_exprt a5(string_length_ge_size, *no_overflow);
      constraints.existential.push_back(a5);
    }
 
    const equal_exprt string_length_equals_size = equal_to(length_expr, size);
 
    const implies_exprt a6(
      and_exprt(string_length_equals_size, not_exprt(starts_with_minus)),
      equal_exprt(input_int, sum));
    constraints.existential.push_back(a6);
 
    const implies_exprt a7(
      and_exprt(string_length_equals_size, starts_with_minus),
      equal_exprt(input_int, unary_minus_exprt(sum)));
    constraints.existential.push_back(a7);
  }
  return constraints;
}
 
string_constraint_generatort::parseint_argumentst
string_constraint_generatort::unpack_parseint_arguments(
  const function_application_exprt &f,
  const typet &target_int_type)
{
  PRECONDITION(f.arguments().size() == 1 || f.arguments().size() == 2);
  PRECONDITION(target_int_type.id() == ID_signedbv);
  const array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]);
 
  const exprt radix =
    f.arguments().size() == 1
      ? static_cast<exprt>(from_integer(10, target_int_type))
      : static_cast<exprt>(typecast_exprt(f.arguments()[1], target_int_type));
  // Most of the time we can evaluate radix as an integer. The value 0 is used
  // to indicate when we can't tell what the radix is.
  const unsigned long radix_ul = to_integer_or_default(radix, 0, ns);
  PRECONDITION((radix_ul >= 2 && radix_ul <= 36) || radix_ul == 0);
 
  const std::size_t max_string_length =
    max_printed_string_length(target_int_type, radix_ul);
 
  return {str, radix, radix_ul, max_string_length};
}

std::pair<exprt, string_constraintst>
string_constraint_generatort::add_axioms_for_is_valid_int(
  const function_application_exprt &f)
{
  irep_idt called_function = to_symbol_expr(f.function()).get_identifier();
  PRECONDITION(
    called_function == ID_cprover_string_is_valid_int_func ||
    called_function == ID_cprover_string_is_valid_long_func);
  const signedbv_typet target_int_type{static_cast<size_t>(
    called_function == ID_cprover_string_is_valid_int_func ? 32 : 64)};
  auto args = unpack_parseint_arguments(f, target_int_type);
 
  const typet &char_type =
    to_type_with_subtype(args.str.content().type()).subtype();
  const typecast_exprt radix_as_char(args.radix, char_type);
  const bool strict_formatting = false;

  auto conjuncts = get_conjuncts_for_correct_number_format(
    args.str,
    radix_as_char,
    args.radix_ul,
    args.max_string_length,
    strict_formatting);
 
  return {typecast_exprt{conjunction(conjuncts), f.type()}, {}};
}

std::pair<exprt, string_constraintst>
string_constraint_generatort::add_axioms_for_parse_int(
  const function_application_exprt &f)
{
  auto args = unpack_parseint_arguments(f, f.type());
 
  const typet &type = f.type();
 
  const symbol_exprt input_int = fresh_symbol("parsed_int", type);
  const bool strict_formatting = false;
 
  auto constraints2 = add_axioms_for_characters_in_integer_string(
    input_int,
    type,
    strict_formatting,
    args.str,
    args.max_string_length,
    args.radix,
    args.radix_ul);
 
  return {input_int, std::move(constraints2)};
}

exprt is_digit_with_radix(
  const exprt &chr,
  const bool strict_formatting,
  const exprt &radix_as_char,
  const unsigned long radix_ul)
{
  PRECONDITION((radix_ul >= 2 && radix_ul <= 36) || radix_ul == 0);
  const typet &char_type = chr.type();
  const exprt zero_char = from_integer('0', char_type);
 
  const and_exprt is_digit_when_radix_le_10(
    binary_relation_exprt(chr, ID_ge, zero_char),
    binary_relation_exprt(chr, ID_lt, plus_exprt(zero_char, radix_as_char)));
 
  if(radix_ul <= 10 && radix_ul != 0)
  {
    return is_digit_when_radix_le_10;
  }
  else
  {
    const exprt nine_char = from_integer('9', char_type);
    const exprt a_char = from_integer('a', char_type);
    const constant_exprt ten_char_type = from_integer(10, char_type);
 
    const minus_exprt radix_minus_ten(radix_as_char, ten_char_type);
 
    or_exprt is_digit_when_radix_gt_10(
      and_exprt(
        binary_relation_exprt(chr, ID_ge, zero_char),
        binary_relation_exprt(chr, ID_le, nine_char)),
      and_exprt(
        binary_relation_exprt(chr, ID_ge, a_char),
        binary_relation_exprt(
          chr, ID_lt, plus_exprt(a_char, radix_minus_ten))));
 
    if(!strict_formatting)
    {
      exprt A_char = from_integer('A', char_type);
      is_digit_when_radix_gt_10.copy_to_operands(and_exprt(
        binary_relation_exprt(chr, ID_ge, A_char),
        binary_relation_exprt(
          chr, ID_lt, plus_exprt(A_char, radix_minus_ten))));
    }
 
    if(radix_ul == 0)
    {
      return if_exprt(
        binary_relation_exprt(radix_as_char, ID_le, ten_char_type),
        is_digit_when_radix_le_10,
        is_digit_when_radix_gt_10);
    }
    else
    {
      return std::move(is_digit_when_radix_gt_10);
    }
  }
}

exprt get_numeric_value_from_character(
  const exprt &chr,
  const typet &char_type,
  const typet &type,
  const bool strict_formatting,
  const unsigned long radix_ul)
{
  const constant_exprt zero_char = from_integer('0', char_type);

  const binary_relation_exprt upper_case_lower_case_or_digit(
    chr, ID_ge, zero_char);
 
  if(radix_ul <= 10 && radix_ul != 0)
  {
    return typecast_exprt(
      if_exprt(
        upper_case_lower_case_or_digit,
        minus_exprt(chr, zero_char),
        from_integer(0, char_type)),
      type);
  }
  else
  {
    const constant_exprt a_char = from_integer('a', char_type);
    const binary_relation_exprt lower_case(chr, ID_ge, a_char);
    const constant_exprt A_char = from_integer('A', char_type);
    const binary_relation_exprt upper_case_or_lower_case(chr, ID_ge, A_char);
    const constant_exprt ten_int = from_integer(10, char_type);
 
    if(strict_formatting)
    {
      return typecast_exprt(
        if_exprt(
          lower_case,
          plus_exprt(minus_exprt(chr, a_char), ten_int),
          if_exprt(
            upper_case_lower_case_or_digit,
            minus_exprt(chr, zero_char),
            from_integer(0, char_type))),
        type);
    }
    else
    {
      return typecast_exprt(
        if_exprt(
          lower_case,
          plus_exprt(minus_exprt(chr, a_char), ten_int),
          if_exprt(
            upper_case_or_lower_case,
            plus_exprt(minus_exprt(chr, A_char), ten_int),
            if_exprt(
              upper_case_lower_case_or_digit,
              minus_exprt(chr, zero_char),
              from_integer(0, char_type)))),
        type);
    }
  }
}

size_t max_printed_string_length(const typet &type, unsigned long radix_ul)
{
  if(radix_ul == 0)
  {
    radix_ul = 2;
  }
  double n_bits = static_cast<double>(to_bitvector_type(type).get_width());
  double radix = static_cast<double>(radix_ul);
  bool signed_type = type.id() == ID_signedbv;
  double max = signed_type
                 ? floor(static_cast<double>(n_bits - 1) / log2(radix)) + 2.0
                 : ceil(static_cast<double>(n_bits) / log2(radix));
  return static_cast<size_t>(max);
}