abstract_environment.h

Go to the documentation of this file.

/*******************************************************************\
 
 Module: analyses variable-sensitivity
 
 Author: Thomas Kiley, thomas.kiley@diffblue.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_ENVIROMENT_H
#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_ENVIROMENT_H
 
#include <memory>
 
#include <analyses/variable-sensitivity/abstract_object.h>
 
exprt simplify_vsd_expr(exprt src, const namespacet &ns);
bool is_ptr_diff(const exprt &expr);
bool is_ptr_comparison(const exprt &expr);
 
class variable_sensitivity_object_factoryt;
using variable_sensitivity_object_factory_ptrt =
  std::shared_ptr<variable_sensitivity_object_factoryt>;
 
enum class widen_modet
{
  no,
  could_widen
};
 
struct vsd_configt;
 
class abstract_environmentt
{
public:
  using map_keyt = irep_idt;
 
  abstract_environmentt() = delete;
 
  explicit abstract_environmentt(
    variable_sensitivity_object_factory_ptrt _object_factory)
    : bottom(true), object_factory(std::move(_object_factory))
  {
  }
 
 
  virtual abstract_object_pointert
  eval(const exprt &expr, const namespacet &ns) const;
 
  virtual bool assign(
    const exprt &expr,
    const abstract_object_pointert &value,
    const namespacet &ns);
 
  virtual bool assume(const exprt &expr, const namespacet &ns);
  exprt do_assume(const exprt &e, const namespacet &ns);
 
  virtual abstract_object_pointert write(
    const abstract_object_pointert &lhs,
    const abstract_object_pointert &rhs,
    std::stack<exprt> remaining_stack,
    const namespacet &ns,
    bool merge_write);
 
  void erase(const symbol_exprt &expr);
 
  virtual abstract_object_pointert abstract_object_factory(
    const typet &type,
    const namespacet &ns,
    bool top,
    bool bottom) const;
 
  virtual abstract_object_pointert abstract_object_factory(
    const typet &type,
    const exprt &e,
    const namespacet &ns) const;
 
  const vsd_configt &configuration() const;
 
  virtual bool merge(
    const abstract_environmentt &env,
    const goto_programt::const_targett &merge_location,
    widen_modet widen_mode);
 
  virtual void havoc(const std::string &havoc_string);
 
  void make_top();
 
  void make_bottom();
 
  bool is_bottom() const;
 
  bool is_top() const;
 
  void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
    const;
 
  exprt to_predicate() const;
 
  bool verify() const;
 
  static std::vector<abstract_environmentt::map_keyt> modified_symbols(
    const abstract_environmentt &first,
    const abstract_environmentt &second);
 
  abstract_object_statisticst gather_statistics(const namespacet &ns) const;
 
protected:
  bool bottom;
 
  // We may need to break out more of these cases into these
  virtual abstract_object_pointert
  eval_expression(const exprt &e, const namespacet &ns) const;
 
  abstract_object_pointert
  resolve_symbol(const exprt &e, const namespacet &ns) const;
 
  sharing_mapt<map_keyt, abstract_object_pointert> map;
 
private:
  abstract_object_pointert abstract_object_factory(
    const typet &type,
    bool top,
    bool bottom,
    const exprt &e,
    const abstract_environmentt &environment,
    const namespacet &ns) const;
 
  variable_sensitivity_object_factory_ptrt object_factory;
};
 
#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_ENVIROMENT_H