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)"                                                             \
                                                                               \
    // clang-format off
#define HELP_VSD                                                               \
  " --vsd-values                 value tracking - "                            \
  "constants|intervals|set-of-constants\n" /* NOLINT(whitespace/line_length) */\
  " --vsd-structs                struct field sensitive analysis - "           \
  "top-bottom|every-field\n" /* NOLINT(whitespace/line_length) */              \
  " --vsd-arrays                 array entry sensitive analysis - "            \
  "top-bottom|smash|up-to-n-elements|every-element\n" /* NOLINT(whitespace/line_length) */ \
  " --vsd-array-max-elements     the n in --vsd-arrays up-to-n-elements - "    \
  "defaults to 10 if not given\n" /* NOLINT(whitespace/line_length) */         \
  " --vsd-pointers               pointer sensitive analysis - "                \
  "top-bottom|constants|value-set\n" /* NOLINT(whitespace/line_length) */      \
  " --vsd-unions                 union sensitive analysis - top-bottom\n"      \
  " --vsd-data-dependencies      track data dependencies\n"                    \
  " --vsd-liveness               track variable liveness\n"                    \
  " --vsd-flow-insensitive       disables flow sensitivity\n"                  \
 
// cland-format on
 
#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 make_entry() 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_call,
    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;
 
  std::vector<irep_idt>
  get_modified_symbols(const variable_sensitivity_domaint &other) const;
 
  void apply_domain(
    std::vector<symbol_exprt> modified_symbols,
    const variable_sensitivity_domaint &target,
    const namespacet &ns);
 
  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 = util_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