variable_sensitivity_domain.h

Go to the documentation of this file.

/*******************************************************************\
 
 Module: analyses variable-sensitivity
 
 Author: Thomas Kiley, thomas.kiley@diffblue.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DOMAIN_H
#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DOMAIN_H
 
#include <iosfwd>
#include <memory>
 
#include <analyses/ai_domain.h>
#include <analyses/variable-sensitivity/abstract_environment.h>
#include <analyses/variable-sensitivity/variable_sensitivity_configuration.h>
 
#define OPT_VSD                                                                \
  "(vsd-values):"                                                              \
  "(vsd-structs):"                                                             \
  "(vsd-arrays):"                                                              \
  "(vsd-array-max-elements):"                                                  \
  "(vsd-pointers):"                                                            \
  "(vsd-unions):"                                                              \
  "(vsd-flow-insensitive)"                                                     \
  "(vsd-data-dependencies)"                                                    \
  "(vsd-liveness)"
 
#define HELP_VSD                                                               \
  " {y--vsd-values} [{yconstants}|{yintervals}|{yset-of-constants}] \t "       \
  "value tracking\n"                                                           \
  " {y--vsd-structs} [{ytop-bottom}|{yevery-field}] \t "                       \
  "struct field sensitive analysis\n"                                          \
  " {y--vsd-arrays} [{ytop-bottom}|{ysmash}|{yup-to-n-elements}|"              \
  "{yevery-element}] \t "                                                      \
  "array entry sensitive analysis\n"                                           \
  " {y--vsd-array-max-elements} {uN} \t "                                      \
  "set the {un} in {y--vsd-arrays} {yup-to-n-elements} (defaults to 10 if "    \
  "not given)\n"                                                               \
  " {y--vsd-pointers} [{ytop-bottom}|{yconstants}|{yvalue-set}] \t "           \
  "pointer sensitive analysis\n"                                               \
  " {y--vsd-unions} [{ytop-bottom}] \t union sensitive analysis\n"             \
  " {y--vsd-data-dependencies} \t track data dependencies\n"                   \
  " {y--vsd-liveness} \t track variable liveness\n"                            \
  " {y--vsd-flow-insensitive} \t disables flow sensitivity\n"
 
#define PARSE_OPTIONS_VSD(cmdline, options)                                    \
  options.set_option("values", cmdline.get_value("vsd-values"));               \
  options.set_option("pointers", cmdline.get_value("vsd-pointers"));           \
  options.set_option("arrays", cmdline.get_value("vsd-arrays"));               \
  options.set_option("array-max-elements", cmdline.get_value("vsd-array-max-elements")); /* NOLINT(whitespace/line_length) */ \
  options.set_option("structs", cmdline.get_value("vsd-structs"));             \
  options.set_option("unions", cmdline.get_value("vsd-unions"));               \
  options.set_option("flow-insensitive", cmdline.isset("vsd-flow-insensitive")); /* NOLINT(whitespace/line_length) */ \
  options.set_option("data-dependencies", cmdline.isset("vsd-data-dependencies")); /* NOLINT(whitespace/line_length) */ \
  options.set_option("liveness", cmdline.isset("vsd-liveness")); /* NOLINT(whitespace/line_length) */ \
  (void)0
 
class variable_sensitivity_domaint : public ai_domain_baset
{
public:
  explicit variable_sensitivity_domaint(
    variable_sensitivity_object_factory_ptrt _object_factory,
    const vsd_configt &_configuration)
    : abstract_state(_object_factory),
      flow_sensitivity(_configuration.flow_sensitivity)
  {
  }
 
  void transform(
    const irep_idt &function_from,
    trace_ptrt trace_from,
    const irep_idt &function_to,
    trace_ptrt trace_to,
    ai_baset &ai,
    const namespacet &ns) override;
 
  void make_bottom() override;
 
  void make_top() override;
 
  void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
    const override;
 
  exprt to_predicate() const override;
 
  exprt to_predicate(const exprt &expr, const namespacet &ns) const;
  exprt to_predicate(const exprt::operandst &exprs, const namespacet &ns) const;
 
  virtual bool
  merge(const variable_sensitivity_domaint &b, trace_ptrt from, trace_ptrt to);
 
  virtual void merge_three_way_function_return(
    const ai_domain_baset &function_start,
    const ai_domain_baset &function_end,
    const namespacet &ns);
 
  bool ai_simplify(exprt &condition, const namespacet &ns) const override;
 
  bool is_bottom() const override;
 
  bool is_top() const override;
 
  virtual abstract_object_pointert
  eval(const exprt &expr, const namespacet &ns) const
  {
    return abstract_state.eval(expr, ns);
  }
 
private:
  void transform_function_call(
    locationt from,
    locationt to,
    ai_baset &ai,
    const namespacet &ns);
 
  bool ignore_function_call_transform(const irep_idt &function_id) const;
 
  void assume(exprt expr, namespacet ns);
 
  abstract_environmentt abstract_state;
  flow_sensitivityt flow_sensitivity;
 
#ifdef ENABLE_STATS
public:
  abstract_object_statisticst gather_statistics(const namespacet &ns) const;
#endif
};
 
class variable_sensitivity_domain_factoryt
  : public ai_domain_factoryt<variable_sensitivity_domaint>
{
public:
  explicit variable_sensitivity_domain_factoryt(
    variable_sensitivity_object_factory_ptrt _object_factory,
    const vsd_configt &_configuration)
    : object_factory(_object_factory), configuration(_configuration)
  {
  }
 
  std::unique_ptr<statet> make(locationt l) const override
  {
    auto d = std::make_unique<variable_sensitivity_domaint>(
      object_factory, configuration);
    CHECK_RETURN(d->is_bottom());
    return std::unique_ptr<statet>(d.release());
  }
 
private:
  variable_sensitivity_object_factory_ptrt object_factory;
  const vsd_configt configuration;
};
 
#ifdef ENABLE_STATS
template <>
struct get_domain_statisticst<variable_sensitivity_domaint>
{
  abstract_object_statisticst total_statistics = {};
  void
  add_entry(const variable_sensitivity_domaint &domain, const namespacet &ns)
  {
    auto statistics = domain.gather_statistics(ns);
    total_statistics.number_of_interval_abstract_objects +=
      statistics.number_of_interval_abstract_objects;
    total_statistics.number_of_globals += statistics.number_of_globals;
    total_statistics.number_of_single_value_intervals +=
      statistics.number_of_single_value_intervals;
    total_statistics.number_of_constants += statistics.number_of_constants;
    total_statistics.number_of_pointers += statistics.number_of_constants;
    total_statistics.number_of_arrays += statistics.number_of_arrays;
    total_statistics.number_of_structs += statistics.number_of_arrays;
    total_statistics.objects_memory_usage += statistics.objects_memory_usage;
  }
 
  void print(std::ostream &out) const
  {
    out << "<< Begin Variable Sensitivity Domain Statistics >>\n"
        << "  Memory Usage: "
        << total_statistics.objects_memory_usage.to_string() << '\n'
        << "  Number of structs: " << total_statistics.number_of_structs << '\n'
        << "  Number of arrays: " << total_statistics.number_of_arrays << '\n'
        << "  Number of pointers: " << total_statistics.number_of_pointers
        << '\n'
        << "  Number of constants: " << total_statistics.number_of_constants
        << '\n'
        << "  Number of intervals: "
        << total_statistics.number_of_interval_abstract_objects << '\n'
        << "  Number of single value intervals: "
        << total_statistics.number_of_single_value_intervals << '\n'
        << "  Number of globals: " << total_statistics.number_of_globals << '\n'
        << "<< End Variable Sensitivity Domain Statistics >>\n";
  }
};
#endif
 
#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_DOMAIN_H