string_constraint_generator_indexof.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Generates string constraints for the family of indexOf and
        lastIndexOf java functions
 
Author: Romain Brenguier, romain.brenguier@diffblue.com
 
\*******************************************************************/
 
 
#include "string_constraint_generator.h"
 
#include <util/mathematical_expr.h>
 
#include "string_refinement_invariant.h"
 
std::pair<exprt, string_constraintst>
string_constraint_generatort::add_axioms_for_index_of(
  const array_string_exprt &str,
  const exprt &c,
  const exprt &from_index)
{
  string_constraintst constraints;
  const typet &index_type = str.length_type();
  symbol_exprt index = fresh_symbol("index_of", index_type);
  symbol_exprt contains = fresh_symbol("contains_in_index_of");
 
  exprt minus1 = from_integer(-1, index_type);
  and_exprt a1(
    binary_relation_exprt(index, ID_ge, minus1),
    binary_relation_exprt(index, ID_lt, array_pool.get_or_create_length(str)));
  constraints.existential.push_back(a1);
 
  equal_exprt a2(not_exprt(contains), equal_exprt(index, minus1));
  constraints.existential.push_back(a2);
 
  implies_exprt a3(
    contains,
    and_exprt(
      binary_relation_exprt(from_index, ID_le, index),
      equal_exprt(str[index], c)));
  constraints.existential.push_back(a3);
 
  const exprt lower_bound(zero_if_negative(from_index));
 
  symbol_exprt n = fresh_symbol("QA_index_of", index_type);
  string_constraintt a4(
    n,
    lower_bound,
    zero_if_negative(index),
    implies_exprt(contains, notequal_exprt(str[n], c)),
    message_handler);
  constraints.universal.push_back(a4);
 
  symbol_exprt m = fresh_symbol("QA_index_of", index_type);
  string_constraintt a5(
    m,
    lower_bound,
    zero_if_negative(array_pool.get_or_create_length(str)),
    implies_exprt(not_exprt(contains), not_exprt(equal_exprt(str[m], c))),
    message_handler);
  constraints.universal.push_back(a5);
 
  return {index, std::move(constraints)};
}
 
std::pair<exprt, string_constraintst>
string_constraint_generatort::add_axioms_for_index_of_string(
  const array_string_exprt &haystack,
  const array_string_exprt &needle,
  const exprt &from_index)
{
  string_constraintst constraints;
  const typet &index_type = haystack.length_type();
  symbol_exprt offset = fresh_symbol("index_of", index_type);
  symbol_exprt contains = fresh_symbol("contains_substring");
 
  implies_exprt a1(
    contains,
    and_exprt(
      binary_relation_exprt(from_index, ID_le, offset),
      binary_relation_exprt(
        offset,
        ID_le,
        minus_exprt(
          array_pool.get_or_create_length(haystack),
          array_pool.get_or_create_length(needle)))));
  constraints.existential.push_back(a1);
 
  equal_exprt a2(
    not_exprt(contains), equal_exprt(offset, from_integer(-1, index_type)));
  constraints.existential.push_back(a2);
 
  symbol_exprt qvar = fresh_symbol("QA_index_of_string", index_type);
  string_constraintt a3(
    qvar,
    zero_if_negative(array_pool.get_or_create_length(needle)),
    implies_exprt(
      contains, equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar])),
    message_handler);
  constraints.universal.push_back(a3);
 
  // string_not contains_constraintt are formulas of the form:
  // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y]
  const string_not_contains_constraintt a4 = {
    from_index,
    offset,
    contains,
    from_integer(0, index_type),
    array_pool.get_or_create_length(needle),
    haystack,
    needle};
  constraints.not_contains.push_back(a4);
 
  const string_not_contains_constraintt a5 = {
    from_index,
    plus_exprt( // Add 1 for inclusive upper bound.
      minus_exprt(
        array_pool.get_or_create_length(haystack),
        array_pool.get_or_create_length(needle)),
      from_integer(1, index_type)),
    not_exprt(contains),
    from_integer(0, index_type),
    array_pool.get_or_create_length(needle),
    haystack,
    needle};
  constraints.not_contains.push_back(a5);
 
  const implies_exprt a6(
    equal_exprt(
      array_pool.get_or_create_length(needle), from_integer(0, index_type)),
    equal_exprt(offset, from_index));
  constraints.existential.push_back(a6);
 
  return {offset, std::move(constraints)};
}
 
std::pair<exprt, string_constraintst>
string_constraint_generatort::add_axioms_for_last_index_of_string(
  const array_string_exprt &haystack,
  const array_string_exprt &needle,
  const exprt &from_index)
{
  string_constraintst constraints;
  const typet &index_type = haystack.length_type();
  symbol_exprt offset = fresh_symbol("index_of", index_type);
  symbol_exprt contains = fresh_symbol("contains_substring");
 
  implies_exprt a1(
    contains,
    and_exprt(
      binary_relation_exprt(from_integer(-1, index_type), ID_le, offset),
      binary_relation_exprt(
        offset,
        ID_le,
        minus_exprt(
          array_pool.get_or_create_length(haystack),
          array_pool.get_or_create_length(needle))),
      binary_relation_exprt(offset, ID_le, from_index)));
  constraints.existential.push_back(a1);
 
  equal_exprt a2(
    not_exprt(contains), equal_exprt(offset, from_integer(-1, index_type)));
  constraints.existential.push_back(a2);
 
  symbol_exprt qvar = fresh_symbol("QA_index_of_string", index_type);
  equal_exprt constr3(haystack[plus_exprt(qvar, offset)], needle[qvar]);
  const string_constraintt a3(
    qvar,
    zero_if_negative(array_pool.get_or_create_length(needle)),
    implies_exprt(contains, constr3),
    message_handler);
  constraints.universal.push_back(a3);
 
  // end_index is min(from_index, |str| - |substring|)
  minus_exprt length_diff(
    array_pool.get_or_create_length(haystack),
    array_pool.get_or_create_length(needle));
  if_exprt end_index(
    binary_relation_exprt(from_index, ID_le, length_diff),
    from_index,
    length_diff);
 
  const string_not_contains_constraintt a4 = {
    plus_exprt(offset, from_integer(1, index_type)),
    plus_exprt(end_index, from_integer(1, index_type)),
    contains,
    from_integer(0, index_type),
    array_pool.get_or_create_length(needle),
    haystack,
    needle};
  constraints.not_contains.push_back(a4);
 
  string_not_contains_constraintt a5 = {
    from_integer(0, index_type),
    plus_exprt(end_index, from_integer(1, index_type)),
    not_exprt(contains),
    from_integer(0, index_type),
    array_pool.get_or_create_length(needle),
    haystack,
    needle};
  constraints.not_contains.push_back(a5);
 
  const implies_exprt a6(
    equal_exprt(
      array_pool.get_or_create_length(needle), from_integer(0, index_type)),
    equal_exprt(offset, from_index));
  constraints.existential.push_back(a6);
 
  return {offset, std::move(constraints)};
}
 
// NOLINTNEXTLINE
// NOLINTNEXTLINE
std::pair<exprt, string_constraintst>
string_constraint_generatort::add_axioms_for_index_of(
  const function_application_exprt &f)
{
  const function_application_exprt::argumentst &args = f.arguments();
  PRECONDITION(args.size() == 2 || args.size() == 3);
  const array_string_exprt str = get_string_expr(array_pool, args[0]);
  const exprt &c = args[1];
  const typet &index_type = str.length_type();
  const typet &char_type = to_type_with_subtype(str.content().type()).subtype();
  PRECONDITION(f.type() == index_type);
  const exprt from_index =
    args.size() == 2 ? from_integer(0, index_type) : args[2];
 
  if(c.type().id() == ID_unsignedbv || c.type().id() == ID_signedbv)
  {
    return add_axioms_for_index_of(
      str, typecast_exprt(c, char_type), from_index);
  }
  else
  {
    INVARIANT(
      is_refined_string_type(c.type()),
      string_refinement_invariantt(
        "c can only be a (un)signedbv or a refined "
        "string and the (un)signedbv case is already handled"));
    array_string_exprt sub = get_string_expr(array_pool, c);
    return add_axioms_for_index_of_string(str, sub, from_index);
  }
}
 
std::pair<exprt, string_constraintst>
string_constraint_generatort::add_axioms_for_last_index_of(
  const array_string_exprt &str,
  const exprt &c,
  const exprt &from_index)
{
  string_constraintst constraints;
  const typet &index_type = str.length_type();
  const symbol_exprt index = fresh_symbol("last_index_of", index_type);
  const symbol_exprt contains = fresh_symbol("contains_in_last_index_of");
 
  const exprt minus1 = from_integer(-1, index_type);
  const and_exprt a1(
    binary_relation_exprt(index, ID_ge, minus1),
    binary_relation_exprt(index, ID_le, from_index),
    binary_relation_exprt(index, ID_lt, array_pool.get_or_create_length(str)));
  constraints.existential.push_back(a1);
 
  const notequal_exprt a2(contains, equal_exprt(index, minus1));
  constraints.existential.push_back(a2);
 
  const implies_exprt a3(contains, equal_exprt(str[index], c));
  constraints.existential.push_back(a3);
 
  const exprt index1 = from_integer(1, index_type);
  const plus_exprt from_index_plus_one(from_index, index1);
  const if_exprt end_index(
    binary_relation_exprt(
      from_index_plus_one, ID_le, array_pool.get_or_create_length(str)),
    from_index_plus_one,
    array_pool.get_or_create_length(str));
 
  const symbol_exprt n = fresh_symbol("QA_last_index_of1", index_type);
  const string_constraintt a4(
    n,
    zero_if_negative(plus_exprt(index, index1)),
    zero_if_negative(end_index),
    implies_exprt(contains, notequal_exprt(str[n], c)),
    message_handler);
  constraints.universal.push_back(a4);
 
  const symbol_exprt m = fresh_symbol("QA_last_index_of2", index_type);
  const string_constraintt a5(
    m,
    zero_if_negative(end_index),
    implies_exprt(not_exprt(contains), notequal_exprt(str[m], c)),
    message_handler);
  constraints.universal.push_back(a5);
 
  return {index, std::move(constraints)};
}
 
// NOLINTNEXTLINE
// NOLINTNEXTLINE
std::pair<exprt, string_constraintst>
string_constraint_generatort::add_axioms_for_last_index_of(
  const function_application_exprt &f)
{
  const function_application_exprt::argumentst &args = f.arguments();
  PRECONDITION(args.size() == 2 || args.size() == 3);
  const array_string_exprt str = get_string_expr(array_pool, args[0]);
  const exprt c = args[1];
  const typet &index_type = str.length_type();
  const typet &char_type = to_type_with_subtype(str.content().type()).subtype();
  PRECONDITION(f.type() == index_type);
 
  const exprt from_index =
    args.size() == 2 ? array_pool.get_or_create_length(str) : args[2];
 
  if(c.type().id() == ID_unsignedbv || c.type().id() == ID_signedbv)
  {
    return add_axioms_for_last_index_of(
      str, typecast_exprt(c, char_type), from_index);
  }
  else
  {
    const array_string_exprt sub = get_string_expr(array_pool, c);
    return add_axioms_for_last_index_of_string(str, sub, from_index);
  }
}