string_builtin_function.h

Go to the documentation of this file.

 
#ifndef CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
#define CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
 
#include "string_constraint_generator.h"
 
#include <util/mathematical_expr.h>
#include <util/string_expr.h>
 
#include <vector>
 
#define CHARACTER_FOR_UNKNOWN '?'
 
class string_builtin_functiont
{
public:
  string_builtin_functiont() = delete;
  string_builtin_functiont(const string_builtin_functiont &) = delete;
  virtual ~string_builtin_functiont() = default;
 
  virtual std::optional<array_string_exprt> string_result() const
  {
    return {};
  }
 
  virtual std::vector<array_string_exprt> string_arguments() const
  {
    return {};
  }
 
  virtual std::optional<exprt>
  eval(const std::function<exprt(const exprt &)> &get_value) const = 0;
 
  virtual std::string name() const = 0;
 
  virtual string_constraintst
  constraints(string_constraint_generatort &, message_handlert &) const = 0;
 
  virtual exprt length_constraint() const = 0;
 
  exprt return_code;
 
  virtual bool maybe_testing_function() const
  {
    return true;
  }
 
protected:
  array_poolt &array_pool;
 
  string_builtin_functiont(exprt return_code, array_poolt &array_pool)
    : return_code(std::move(return_code)), array_pool(array_pool)
  {
  }
};
 
class string_transformation_builtin_functiont : public string_builtin_functiont
{
public:
  array_string_exprt result;
  array_string_exprt input;
 
  string_transformation_builtin_functiont(
    exprt return_code,
    array_string_exprt result,
    array_string_exprt input,
    array_poolt &array_pool)
    : string_builtin_functiont(std::move(return_code), array_pool),
      result(std::move(result)),
      input(std::move(input))
  {
  }
 
  string_transformation_builtin_functiont(
    const exprt &return_code,
    const std::vector<exprt> &fun_args,
    array_poolt &array_pool);
 
  std::optional<array_string_exprt> string_result() const override
  {
    return result;
  }
  std::vector<array_string_exprt> string_arguments() const override
  {
    return {input};
  }
  bool maybe_testing_function() const override
  {
    return false;
  }
};
 
class string_concat_char_builtin_functiont
  : public string_transformation_builtin_functiont
{
public:
  exprt character;
 
  string_concat_char_builtin_functiont(
    const exprt &return_code,
    const std::vector<exprt> &fun_args,
    array_poolt &array_pool)
    : string_transformation_builtin_functiont(return_code, fun_args, array_pool)
  {
    PRECONDITION(fun_args.size() == 4);
    character = fun_args[3];
  }
 
  std::optional<exprt>
  eval(const std::function<exprt(const exprt &)> &get_value) const override;
 
  std::string name() const override
  {
    return "concat_char";
  }
 
  string_constraintst constraints(
    string_constraint_generatort &generator,
    message_handlert &message_handlert) const override;
 
  exprt length_constraint() const override;
};
 
class string_set_char_builtin_functiont
  : public string_transformation_builtin_functiont
{
public:
  exprt position;
  exprt character;
 
  string_set_char_builtin_functiont(
    const exprt &return_code,
    const std::vector<exprt> &fun_args,
    array_poolt &array_pool)
    : string_transformation_builtin_functiont(return_code, fun_args, array_pool)
  {
    PRECONDITION(fun_args.size() == 5);
    position = fun_args[3];
    character = fun_args[4];
  }
 
  std::optional<exprt>
  eval(const std::function<exprt(const exprt &)> &get_value) const override;
 
  std::string name() const override
  {
    return "set_char";
  }
 
  string_constraintst constraints(
    string_constraint_generatort &generator,
    message_handlert &message_handler) const override;
 
  // \todo: length_constraint is not the best possible name because we also
  // \todo: add constraint about the return code
  exprt length_constraint() const override;
};
 
class string_to_lower_case_builtin_functiont
  : public string_transformation_builtin_functiont
{
public:
  string_to_lower_case_builtin_functiont(
    const exprt &return_code,
    const std::vector<exprt> &fun_args,
    array_poolt &array_pool)
    : string_transformation_builtin_functiont(return_code, fun_args, array_pool)
  {
  }
 
  std::optional<exprt>
  eval(const std::function<exprt(const exprt &)> &get_value) const override;
 
  std::string name() const override
  {
    return "to_lower_case";
  }
 
  string_constraintst constraints(
    string_constraint_generatort &generator,
    message_handlert &message_handler) const override;
 
  exprt length_constraint() const override
  {
    return and_exprt(
      equal_exprt(
        array_pool.get_or_create_length(result),
        array_pool.get_or_create_length(input)),
      equal_exprt(return_code, from_integer(0, return_code.type())));
  };
};
 
class string_to_upper_case_builtin_functiont
  : public string_transformation_builtin_functiont
{
public:
  string_to_upper_case_builtin_functiont(
    const exprt &return_code,
    const std::vector<exprt> &fun_args,
    array_poolt &array_pool)
    : string_transformation_builtin_functiont(return_code, fun_args, array_pool)
  {
  }
 
  string_to_upper_case_builtin_functiont(
    exprt return_code,
    array_string_exprt result,
    array_string_exprt input,
    array_poolt &array_pool)
    : string_transformation_builtin_functiont(
        std::move(return_code),
        std::move(result),
        std::move(input),
        array_pool)
  {
  }
 
  std::optional<exprt>
  eval(const std::function<exprt(const exprt &)> &get_value) const override;
 
  std::string name() const override
  {
    return "to_upper_case";
  }
 
  string_constraintst constraints(
    class symbol_generatort &fresh_symbol,
    message_handlert &message_handler) const;
 
  string_constraintst constraints(
    string_constraint_generatort &generator,
    message_handlert &message_handler) const override
  {
    return constraints(generator.fresh_symbol, message_handler);
  };
 
  exprt length_constraint() const override
  {
    return and_exprt(
      equal_exprt(
        array_pool.get_or_create_length(result),
        array_pool.get_or_create_length(input)),
      equal_exprt(return_code, from_integer(0, return_code.type())));
  };
};
 
class string_creation_builtin_functiont : public string_builtin_functiont
{
public:
  array_string_exprt result;
  exprt arg;
 
  string_creation_builtin_functiont(
    const exprt &return_code,
    const std::vector<exprt> &fun_args,
    array_poolt &array_pool);
 
  std::optional<array_string_exprt> string_result() const override
  {
    return result;
  }
 
  bool maybe_testing_function() const override
  {
    return false;
  }
};
 
class string_of_int_builtin_functiont : public string_creation_builtin_functiont
{
public:
  string_of_int_builtin_functiont(
    const exprt &return_code,
    const std::vector<exprt> &fun_args,
    array_poolt &array_pool)
    : string_creation_builtin_functiont(return_code, fun_args, array_pool)
  {
    PRECONDITION(fun_args.size() <= 4);
    if(fun_args.size() == 4)
      radix = fun_args[3];
    else
      radix = from_integer(10, arg.type());
  };
 
  std::optional<exprt>
  eval(const std::function<exprt(const exprt &)> &get_value) const override;
 
  std::string name() const override
  {
    return "string_of_int";
  }
 
  string_constraintst constraints(
    string_constraint_generatort &generator,
    message_handlert &message_handler) const override;
 
  exprt length_constraint() const override;
 
private:
  exprt radix;
};
 
class string_test_builtin_functiont : public string_builtin_functiont
{
public:
  exprt result;
  std::vector<array_string_exprt> under_test;
  std::vector<exprt> args;
  std::vector<array_string_exprt> string_arguments() const override
  {
    return under_test;
  }
};
 
class string_builtin_function_with_no_evalt : public string_builtin_functiont
{
public:
  function_application_exprt function_application;
  std::optional<array_string_exprt> string_res;
  std::vector<array_string_exprt> string_args;
  std::vector<exprt> args;
 
  string_builtin_function_with_no_evalt(
    const exprt &return_code,
    const function_application_exprt &f,
    array_poolt &array_pool);
 
  std::string name() const override
  {
    PRECONDITION(function_application.function().id() == ID_symbol);
    return id2string(
      to_symbol_expr(function_application.function()).get_identifier());
  }
  std::vector<array_string_exprt> string_arguments() const override
  {
    return std::vector<array_string_exprt>(string_args);
  }
  std::optional<array_string_exprt> string_result() const override
  {
    return string_res;
  }
 
  std::optional<exprt>
  eval(const std::function<exprt(const exprt &)> &) const override
  {
    return {};
  }
 
  string_constraintst constraints(
    string_constraint_generatort &generator,
    message_handlert &message_handler) const override;
 
  exprt length_constraint() const override
  {
    // For now, there is no need for implementing that as `constraints`
    // should always be called on these functions
    UNIMPLEMENTED;
  }
};
 
std::optional<std::vector<mp_integer>> eval_string(
  const array_string_exprt &a,
  const std::function<exprt(const exprt &)> &get_value);
 
array_string_exprt make_string(
  const std::vector<mp_integer> &array,
  const array_typet &array_type);
 
#endif // CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H