recursive_initialization.h

Go to the documentation of this file.

/******************************************************************\
 
Module: recursive_initialization
 
Author: Diffblue Ltd.
 
\******************************************************************/
 
#ifndef CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H
#define CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H
 
#include <map>
#include <set>
#include <unordered_set>
 
#include <util/cprover_prefix.h>
#include <util/optional.h>
#include <util/prefix.h>
#include <util/std_expr.h>
#include <util/symbol.h>
 
class code_blockt;
class goto_modelt;
 
#define GOTO_HARNESS_PREFIX "__GOTO_HARNESS"
struct recursive_initialization_configt
{
  std::size_t min_null_tree_depth = 1;
  std::size_t max_nondet_tree_depth = 2;
  irep_idt mode;
  std::unordered_set<irep_idt> potential_null_function_pointers;
 
  // array stuff
  std::size_t max_dynamic_array_size = 2;
  std::size_t min_dynamic_array_size = 1;
 
  std::set<irep_idt> pointers_to_treat_as_arrays;
  std::set<irep_idt> variables_that_hold_array_sizes;
  std::map<irep_idt, irep_idt> array_name_to_associated_array_size_variable;
 
  std::set<irep_idt> pointers_to_treat_as_cstrings;
  std::vector<std::set<irep_idt>> pointers_to_treat_equal;
 
  bool arguments_may_be_equal = false;
 
  std::vector<std::vector<irep_idt>> selection_specs;
 
  std::string to_string() const; // for debugging purposes
 
  bool handle_option(
    const std::string &option,
    const std::list<std::string> &values);
};
 
class recursive_initializationt
{
public:
  using recursion_sett = std::set<irep_idt>;
  using equal_cluster_idt = std::size_t;
  struct constructor_keyt
  {
    typet constructor_type;
    bool is_nullable;
    bool has_size_parameter;
    bool operator<(const constructor_keyt &other) const
    {
      return std::tie(constructor_type, is_nullable, has_size_parameter) <
             std::tie(
               other.constructor_type,
               other.is_nullable,
               other.has_size_parameter);
    };
    bool operator==(const constructor_keyt &other) const
    {
      return std::tie(constructor_type, is_nullable, has_size_parameter) ==
             std::tie(
               other.constructor_type,
               other.is_nullable,
               other.has_size_parameter);
    };
  };
  using type_constructor_namest = std::map<constructor_keyt, irep_idt>;
 
  recursive_initializationt(
    recursive_initialization_configt initialization_config,
    goto_modelt &goto_model);
 
  void initialize(const exprt &lhs, const exprt &depth, code_blockt &body);
 
  symbol_exprt get_free_function();
 
  static bool is_initialization_allowed(const symbolt &symbol)
  {
    auto const symbol_name = id2string(symbol.name);
    return (
      symbol.is_static_lifetime && symbol.is_lvalue &&
      !symbol.type.get_bool(ID_C_constant) && symbol.type.id() != ID_code &&
      !has_prefix(symbol_name, CPROVER_PREFIX) &&
      !has_prefix(symbol_name, GOTO_HARNESS_PREFIX));
  }
 
  bool needs_freeing(const exprt &expr) const;
  void free_if_possible(const exprt &expr, code_blockt &body);
  void free_cluster_origins(code_blockt &body);
 
private:
  const recursive_initialization_configt initialization_config;
  goto_modelt &goto_model;
  irep_idt max_depth_var_name;
  irep_idt min_depth_var_name;
  type_constructor_namest type_constructor_names;
  std::vector<optionalt<exprt>> common_arguments_origins;
 
  symbol_exprt get_malloc_function();
 
  bool should_be_treated_as_array(const irep_idt &pointer_name) const;
  optionalt<equal_cluster_idt> find_equal_cluster(const irep_idt &name) const;
  bool is_array_size_parameter(const irep_idt &cmdline_arg) const;
  optionalt<irep_idt>
  get_associated_size_variable(const irep_idt &array_name) const;
  bool should_be_treated_as_cstring(const irep_idt &pointer_name) const;
 
  irep_idt get_fresh_global_name(
    const std::string &symbol_name,
    const exprt &initial_value) const;
 
  symbol_exprt get_fresh_global_symexpr(const std::string &symbol_name) const;
 
  symbol_exprt get_fresh_local_symexpr(const std::string &symbol_name) const;
 
  symbol_exprt get_fresh_local_typed_symexpr(
    const std::string &symbol_name,
    const typet &type) const;
 
  const symbolt &
  get_fresh_fun_symbol(const std::string &fun_name, const typet &fun_type);
 
  symbolt &get_fresh_param_symbol(
    const std::string &param_name,
    const typet &param_type);
 
  symbol_exprt get_symbol_expr(const irep_idt &symbol_name) const;
 
  std::string type2id(const typet &type) const;
 
  code_blockt build_constructor_body(
    const exprt &depth_symbol,
    const symbol_exprt &result_symbol,
    const optionalt<exprt> &size_symbol,
    const optionalt<irep_idt> &lhs_name,
    const bool is_nullable);
 
  irep_idt build_constructor(const exprt &expr);
 
  code_blockt build_function_pointer_constructor(
    const symbol_exprt &result,
    bool is_nullable);
 
  code_blockt
  build_pointer_constructor(const exprt &depth, const symbol_exprt &result);
 
  code_blockt
  build_struct_constructor(const exprt &depth, const symbol_exprt &result);
 
  code_blockt build_nondet_constructor(const symbol_exprt &result) const;
 
  code_blockt
  build_array_constructor(const exprt &depth, const symbol_exprt &result);
 
  code_blockt build_dynamic_array_constructor(
    const exprt &depth,
    const symbol_exprt &result,
    const exprt &size,
    const optionalt<irep_idt> &lhs_name);
 
  void initialize_selected_member(
    const exprt &lhs,
    const exprt &depth,
    code_blockt &body,
    const std::vector<irep_idt> &selection_spec);
};
 
#endif // CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H