dirty.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Variables whose address is taken
 
Author: Daniel Kroening
 
Date: March 2013
 
\*******************************************************************/
 
 
#ifndef CPROVER_ANALYSES_DIRTY_H
#define CPROVER_ANALYSES_DIRTY_H
 
#include <util/invariant.h>
#include <util/std_expr.h>
 
#include <goto-programs/goto_functions.h>
 
#include <unordered_set>
 
class dirtyt
{
private:
  void die_if_uninitialized() const
  {
    INVARIANT(
      initialized,
      "Uninitialized dirtyt. This dirtyt was constructed using the default "
      "constructor and not subsequently initialized using "
      "dirtyt::build().");
  }
 
public:
  bool initialized;
  typedef goto_functionst::goto_functiont goto_functiont;
 
  dirtyt() : initialized(false)
  {
  }
 
  explicit dirtyt(const goto_functiont &goto_function) : initialized(false)
  {
    build(goto_function);
    initialized = true;
  }
 
  explicit dirtyt(const goto_functionst &goto_functions) : initialized(false)
  {
    build(goto_functions);
    // build(g_funs) responsible for setting initialized to true, since
    // it is public and can be called independently
  }
 
  void output(std::ostream &out) const;
 
  bool operator()(const irep_idt &id) const
  {
    die_if_uninitialized();
    return dirty.find(id) != dirty.end();
  }
 
  bool operator()(const symbol_exprt &expr) const
  {
    die_if_uninitialized();
    return operator()(expr.get_identifier());
  }
 
  const std::unordered_set<irep_idt> &get_dirty_ids() const
  {
    die_if_uninitialized();
    return dirty;
  }
 
  void add_function(const goto_functiont &goto_function)
  {
    build(goto_function);
    initialized = true;
  }
 
  void build(const goto_functionst &goto_functions)
  {
    // dirtyts should not be initialized twice
    PRECONDITION(!initialized);
    for(const auto &gf_entry : goto_functions.function_map)
      build(gf_entry.second);
    initialized = true;
  }
 
protected:
  void build(const goto_functiont &goto_function);
 
  // variables whose address is taken
  std::unordered_set<irep_idt> dirty;
  void search_other(const goto_programt::instructiont &instruction);
  void find_dirty(const exprt &expr);
  void find_dirty_address_of(const exprt &expr);
};
 
inline std::ostream &operator<<(std::ostream &out, const dirtyt &dirty)
{
  dirty.output(out);
  return out;
}
 
class incremental_dirtyt
{
public:
  void populate_dirty_for_function(
    const irep_idt &id,
    const goto_functionst::goto_functiont &function);
 
  bool operator()(const irep_idt &id) const
  {
    return dirty(id);
  }
 
  bool operator()(const symbol_exprt &expr) const
  {
    return dirty(expr);
  }
 
private:
  dirtyt dirty;
  std::unordered_set<irep_idt> dirty_processed_functions;
};
 
#endif // CPROVER_ANALYSES_DIRTY_H