ai_history.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Abstract Interpretation
 
Author: Martin Brain, martin.brain@cs.ox.ac.uk
 
\*******************************************************************/
 
 
#ifndef CPROVER_ANALYSES_AI_HISTORY_H
#define CPROVER_ANALYSES_AI_HISTORY_H
 
#include <memory>
 
#include <util/json.h>
#include <util/xml.h>
 
#include <goto-programs/goto_program.h>
 
 
class ai_history_baset
{
public:
  typedef goto_programt::const_targett locationt;
 
  typedef std::shared_ptr<const ai_history_baset> trace_ptrt;
 
protected:
  explicit ai_history_baset(locationt)
  {
  }
 
  ai_history_baset(const ai_history_baset &)
  {
  }
 
public:
  virtual ~ai_history_baset()
  {
  }
 
  struct compare_historyt
  {
    bool operator()(const trace_ptrt &l, const trace_ptrt &r) const
    {
      return *l < *r;
    }
  };
  typedef std::set<trace_ptrt, compare_historyt> trace_sett; // Order matters!
 
  enum class step_statust
  {
    NEW,
    MERGED,
    BLOCKED
  };
 
  typedef std::pair<step_statust, trace_ptrt> step_returnt;
  virtual step_returnt step(
    locationt to,
    const trace_sett &others,
    trace_ptrt caller_hist) const = 0;
 
  static const trace_ptrt no_caller_history;
 
  virtual bool operator<(const ai_history_baset &op) const = 0;
 
  virtual bool operator==(const ai_history_baset &op) const = 0;
 
  virtual const locationt &current_location(void) const = 0;
 
  virtual bool should_widen(const ai_history_baset &other) const
  {
    return false;
  }
 
  virtual void output(std::ostream &out) const
  {
  }
  virtual jsont output_json(void) const;
  virtual xmlt output_xml(void) const;
};
 
class ahistoricalt : public ai_history_baset
{
protected:
  // DATA_INVARIANT(current.is_dereferenceable(), "Must not be _::end()")
  locationt current;
 
public:
  explicit ahistoricalt(locationt l) : ai_history_baset(l), current(l)
  {
  }
 
  ahistoricalt(const ahistoricalt &old)
    : ai_history_baset(old), current(old.current)
  {
  }
 
  step_returnt step(
    locationt to,
    const trace_sett &others,
    trace_ptrt caller_hist) const override
  {
    trace_ptrt next(new ahistoricalt(to));
 
    if(others.empty())
    {
      return std::make_pair(step_statust::NEW, next);
    }
    else
    {
      // Aggressively merge histories because they are indistinguishable
      INVARIANT(others.size() == 1, "Only needs one history per location");
 
      const auto it = others.begin();
      INVARIANT(
        *(*(it)) == *next,
        "The next location in history map must contain next history");
 
      return std::make_pair(step_statust::MERGED, *it);
    }
  }
 
  bool operator<(const ai_history_baset &op) const override
  {
    PRECONDITION(dynamic_cast<const ahistoricalt *>(&op) != nullptr);
 
    return this->current_location()->location_number <
           op.current_location()->location_number;
  }
 
  bool operator==(const ai_history_baset &op) const override
  {
    PRECONDITION(dynamic_cast<const ahistoricalt *>(&op) != nullptr);
 
    // It would be nice to:
    //  return this->current == op.current
    // But they may point to different goto_programs,
    // giving undefined behaviour in C++
    // So (safe due to data invariant & uniqueness of location numbers) ...
    return this->current_location()->location_number ==
           op.current_location()->location_number;
  }
 
  const locationt &current_location(void) const override
  {
    return current;
  }
 
  // Use default widening
  // without history there is no reason to say any location is better than
  // another to widen.
  bool should_widen(const ai_history_baset &other) const override
  {
    return ai_history_baset::should_widen(other);
  }
 
  void output(std::ostream &out) const override
  {
    out << "ahistorical : location " << current_location()->location_number;
  }
};
 
 
class ai_history_factory_baset
{
public:
  virtual ai_history_baset::trace_ptrt epoch(ai_history_baset::locationt) = 0;
 
  virtual ~ai_history_factory_baset()
  {
  }
};
 
template <typename traceT>
class ai_history_factory_default_constructort : public ai_history_factory_baset
{
public:
  ai_history_baset::trace_ptrt epoch(ai_history_baset::locationt l) override
  {
    ai_history_baset::trace_ptrt p(new traceT(l));
    return p;
  }
};
 
#endif // CPROVER_ANALYSES_AI_HISTORY_H