ai_domain.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Abstract Interpretation
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_ANALYSES_AI_DOMAIN_H
#define CPROVER_ANALYSES_AI_DOMAIN_H
 
#include <util/json.h>
#include <util/xml.h>
 
#include "ai_history.h"
 
// forward reference the abstract interpreter interface
class ai_baset;
 
class ai_domain_baset
{
protected:
  ai_domain_baset()
  {
  }
 
  ai_domain_baset(const ai_domain_baset &old)
  {
  }
 
public:
  virtual ~ai_domain_baset()
  {
  }
 
  typedef goto_programt::const_targett locationt;
  typedef ai_history_baset::trace_ptrt trace_ptrt;
 
  virtual void transform(
    const irep_idt &function_from,
    trace_ptrt from,
    const irep_idt &function_to,
    trace_ptrt to,
    ai_baset &ai,
    const namespacet &ns) = 0;
 
  virtual void
  output(std::ostream &, const ai_baset &, const namespacet &) const
  {
  }
 
  virtual jsont output_json(const ai_baset &ai, const namespacet &ns) const;
 
  virtual xmlt output_xml(const ai_baset &ai, const namespacet &ns) const;
 
  virtual void make_bottom() = 0;
 
  virtual void make_top() = 0;
 
  virtual void make_entry()
  {
    make_top();
  }
 
  virtual bool is_bottom() const = 0;
 
  virtual bool is_top() const = 0;
 
 
 
  virtual bool ai_simplify(exprt &condition, const namespacet &) const
  {
    (void)condition; // unused parameter
    return true;
  }
 
  virtual bool ai_simplify_lhs(exprt &condition, const namespacet &ns) const;
 
  virtual exprt to_predicate(void) const
  {
    if(is_bottom())
      return false_exprt();
    else
      return true_exprt();
  }
};
 
// No virtual interface is complete without a factory!
class ai_domain_factory_baset
{
public:
  typedef ai_domain_baset statet;
  typedef ai_domain_baset::locationt locationt;
  typedef ai_domain_baset::trace_ptrt trace_ptrt;
 
  virtual ~ai_domain_factory_baset()
  {
  }
 
  virtual std::unique_ptr<statet> make(locationt l) const = 0;
  virtual std::unique_ptr<statet> copy(const statet &s) const = 0;
 
  // Not domain construction but requires knowing the precise type of statet
  virtual bool
  merge(statet &dest, const statet &src, trace_ptrt from, trace_ptrt to)
    const = 0;
};
// Converting make to take a trace_ptr instead of a location would
// require removing the backwards-compatible
//  location_sensitive_storaget::get_state(locationt l)
// function which is used by some of the older domains
 
// It would be great to have a single (templated) default implementation.
// However, a default constructor is not part of the ai_domain_baset interface
// and there are some domains which don't have one.  So we need to separate the
// methods.
template <typename domainT>
class ai_domain_factoryt : public ai_domain_factory_baset
{
public:
  typedef ai_domain_factory_baset::statet statet;
  typedef ai_domain_factory_baset::locationt locationt;
  typedef ai_domain_factory_baset::trace_ptrt trace_ptrt;
 
  std::unique_ptr<statet> copy(const statet &s) const override
  {
    return std::make_unique<domainT>(static_cast<const domainT &>(s));
  }
 
  bool merge(statet &dest, const statet &src, trace_ptrt from, trace_ptrt to)
    const override
  {
    // For backwards compatability, use the location version
    return static_cast<domainT &>(dest).merge(
      static_cast<const domainT &>(src), from, to);
  }
};
 
template <typename domainT>
class ai_domain_factory_default_constructort
  : public ai_domain_factoryt<domainT>
{
public:
  typedef ai_domain_factory_baset::statet statet;
  typedef ai_domain_factory_baset::locationt locationt;
  typedef ai_domain_factory_baset::trace_ptrt trace_ptrt;
 
  std::unique_ptr<statet> make(locationt l) const override
  {
    auto d = std::make_unique<domainT>();
    CHECK_RETURN(d->is_bottom());
    return std::unique_ptr<statet>(d.release());
  }
};
 
template <typename domainT>
class ai_domain_factory_location_constructort
  : public ai_domain_factoryt<domainT>
{
public:
  typedef ai_domain_factory_baset::statet statet;
  typedef ai_domain_factory_baset::locationt locationt;
  typedef ai_domain_factory_baset::trace_ptrt trace_ptrt;
 
  std::unique_ptr<statet> make(locationt l) const override
  {
    auto d = std::make_unique<domainT>(l);
    CHECK_RETURN(d->is_bottom());
    return std::unique_ptr<statet>(d.release());
  }
};
 
#endif