reaching_definitions.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Range-based reaching definitions analysis (following Field-
        Sensitive Program Dependence Analysis, Litvak et al., FSE 2010)
 
Author: Michael Tautschnig
 
Date: February 2013
 
\*******************************************************************/
 
 
#ifndef CPROVER_ANALYSES_REACHING_DEFINITIONS_H
#define CPROVER_ANALYSES_REACHING_DEFINITIONS_H
 
#include <util/threeval.h>
 
#include "ai.h"
#include "goto_rw.h"
 
class value_setst;
class is_threadedt;
class dirtyt;
class reaching_definitions_analysist;
 
template<typename V>
class sparse_bitvector_analysist
{
public:
  const V &get(const std::size_t value_index) const
  {
    PRECONDITION(value_index < values.size());
    return values[value_index]->first;
  }
 
  std::size_t add(const V &value)
  {
    inner_mapt &m=value_map[value.identifier];
 
    std::pair<typename inner_mapt::iterator, bool> entry=
      m.insert(std::make_pair(value, values.size()));
 
    if(entry.second)
      values.push_back(entry.first);
 
    return entry.first->second;
  }
 
  void clear()
  {
    value_map.clear();
    values.clear();
  }
 
protected:
  typedef typename std::map<V, std::size_t> inner_mapt;
  std::vector<typename inner_mapt::const_iterator> values;
  std::unordered_map<irep_idt, inner_mapt> value_map;
};
 
struct reaching_definitiont
{
  irep_idt identifier;
  ai_domain_baset::locationt definition_at;
  range_spect bit_begin;
  range_spect bit_end;
 
  reaching_definitiont(
    const irep_idt &identifier,
    const ai_domain_baset::locationt &definition_at,
    const range_spect &bit_begin,
    const range_spect &bit_end)
    : identifier(identifier),
      definition_at(definition_at),
      bit_begin(bit_begin),
      bit_end(bit_end)
  {
  }
};
 
inline bool operator<(
  const reaching_definitiont &a,
  const reaching_definitiont &b)
{
  if(goto_programt::target_less_than()(a.definition_at, b.definition_at))
    return true;
  if(goto_programt::target_less_than()(b.definition_at, a.definition_at))
    return false;
 
  if(a.bit_begin.is_unknown() != b.bit_begin.is_unknown())
    return a.bit_begin.is_unknown();
 
  if(!a.bit_begin.is_unknown())
  {
    if(a.bit_begin < b.bit_begin)
      return true;
    if(b.bit_begin < a.bit_begin)
      return false;
  }
 
  if(a.bit_end.is_unknown() != b.bit_end.is_unknown())
    return a.bit_end.is_unknown();
 
  if(!a.bit_end.is_unknown())
  {
    if(a.bit_end < b.bit_end)
      return true;
    if(b.bit_end < a.bit_end)
      return false;
  }
 
  // we do not expect comparison of unrelated definitions
  // as this operator< is only used in sparse_bitvector_analysist
  INVARIANT(
    a.identifier == b.identifier, "comparison of unrelated definitions");
 
  return false;
}
 
class rd_range_domaint:public ai_domain_baset
{
public:
  rd_range_domaint(
    sparse_bitvector_analysist<reaching_definitiont> *_bv_container,
    message_handlert &message_handler)
    : ai_domain_baset(),
      has_values(false),
      bv_container(_bv_container),
      message_handler(message_handler)
  {
    PRECONDITION(bv_container != nullptr);
  }
 
  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) final override;
 
  void output(
    std::ostream &out,
    const ai_baset &,
    const namespacet &) const final override
  {
    output(out);
  }
 
  void make_top() final override
  {
    values.clear();
    if(bv_container)
      bv_container->clear();
    has_values=tvt(true);
  }
 
  void make_bottom() final override
  {
    values.clear();
    if(bv_container)
      bv_container->clear();
    has_values=tvt(false);
  }
 
  bool is_top() const override final
  {
    DATA_INVARIANT(!has_values.is_true() || values.empty(),
                   "If domain is top, the value map must be empty");
    return has_values.is_true();
  }
 
  bool is_bottom() const override final
  {
    DATA_INVARIANT(!has_values.is_false() || values.empty(),
                   "If domain is bottom, the value map must be empty");
    return has_values.is_false();
  }
 
  bool merge(const rd_range_domaint &other, trace_ptrt from, trace_ptrt to);
 
  bool merge_shared(
    const rd_range_domaint &other,
    locationt from,
    locationt to,
    const namespacet &ns);
 
  // each element x represents a range of bits [x.first, x.second)
  typedef std::multimap<range_spect, range_spect> rangest;
  typedef std::map<locationt, rangest, goto_programt::target_less_than>
    ranges_at_loct;
 
  const ranges_at_loct &get(const irep_idt &identifier) const;
  void clear_cache(const irep_idt &identifier) const
  {
    export_cache[identifier].clear();
  }
 
private:
  tvt has_values;
 
  sparse_bitvector_analysist<reaching_definitiont> *const bv_container;
 
  typedef std::set<std::size_t> values_innert;
  typedef std::map<irep_idt, values_innert> valuest;
  valuest values;
 
  typedef std::map<irep_idt, ranges_at_loct> export_cachet;
  mutable export_cachet export_cache;
 
  void populate_cache(const irep_idt &identifier) const;
 
  void transform_dead(
    const namespacet &ns,
    locationt from);
  void transform_start_thread(
    const namespacet &ns,
    reaching_definitions_analysist &rd);
  void transform_function_call(
    const namespacet &ns,
    const irep_idt &function_from,
    locationt from,
    const irep_idt &function_to,
    reaching_definitions_analysist &rd);
  void transform_end_function(
    const namespacet &ns,
    const irep_idt &function_from,
    locationt from,
    const irep_idt &function_to,
    locationt to,
    reaching_definitions_analysist &rd);
  void transform_assign(
    const namespacet &ns,
    locationt from,
    const irep_idt &function_to,
    locationt to,
    reaching_definitions_analysist &rd);
 
  void kill(
    const irep_idt &identifier,
    const range_spect &range_start,
    const range_spect &range_end);
  void kill_inf(
    const irep_idt &identifier,
    const range_spect &range_start);
  bool gen(
    locationt from,
    const irep_idt &identifier,
    const range_spect &range_start,
    const range_spect &range_end);
 
  void output(std::ostream &out) const;
 
  bool merge_inner(
    values_innert &dest,
    const values_innert &other);
 
  message_handlert &message_handler;
};
 
class reaching_definitions_analysist:
  public concurrency_aware_ait<rd_range_domaint>,
  public sparse_bitvector_analysist<reaching_definitiont>
{
public:
  // constructor
  reaching_definitions_analysist(const namespacet &_ns, message_handlert &);
 
  virtual ~reaching_definitions_analysist();
 
  void initialize(const goto_functionst &goto_functions) override;
 
  value_setst &get_value_sets() const
  {
    PRECONDITION(value_sets);
    return *value_sets;
  }
 
  const is_threadedt &get_is_threaded() const
  {
    PRECONDITION(is_threaded);
    return *is_threaded;
  }
 
  const dirtyt &get_is_dirty() const
  {
    PRECONDITION(is_dirty);
    return *is_dirty;
  }
 
protected:
  const namespacet &ns;
  std::unique_ptr<value_setst> value_sets;
  std::unique_ptr<is_threadedt> is_threaded;
  std::unique_ptr<dirtyt> is_dirty;
};
 
#endif // CPROVER_ANALYSES_REACHING_DEFINITIONS_H