path_storage.h

Go to the documentation of this file.

 
#ifndef CPROVER_GOTO_SYMEX_PATH_STORAGE_H
#define CPROVER_GOTO_SYMEX_PATH_STORAGE_H
 
#include <util/invariant.h>
 
#include <analyses/dirty.h>
#include <analyses/local_safe_pointers.h> // IWYU pragma: keep
 
#include "goto_symex_state.h"
#include "symex_target_equation.h"
 
#include <memory>
 
class cmdlinet;
class optionst;
 
class symex_nondet_generatort
{
public:
  nondet_symbol_exprt operator()(typet type, source_locationt location);
 
private:
  std::size_t nondet_count = 0;
};
 
class path_storaget
{
public:
  struct patht
  {
    symex_target_equationt equation;
    goto_symex_statet state;
 
    patht(const symex_target_equationt &e, const goto_symex_statet &s)
      : equation(e), state(s, &equation)
    {
    }
 
    explicit patht(const patht &other)
      : equation(other.equation), state(other.state, &equation)
    {
    }
  };
 
  virtual ~path_storaget() = default;
 
  patht &peek()
  {
    PRECONDITION(!empty());
    return private_peek();
  }
 
  virtual void clear() = 0;
 
  virtual void push(const patht &) = 0;
 
  void pop()
  {
    PRECONDITION(!empty());
    private_pop();
  }
 
  virtual std::size_t size() const = 0;
 
  bool empty() const
  {
    return size() == 0;
  };
 
  symex_nondet_generatort build_symex_nondet;
 
  std::unordered_map<irep_idt, local_safe_pointerst> safe_pointers;
 
  std::size_t get_unique_l1_index(const irep_idt &id, std::size_t minimum_index)
  {
    return get_unique_index(l1_indices, id, minimum_index);
  }
 
  std::size_t get_unique_l2_index(const irep_idt &id)
  {
    return get_unique_index(l2_indices, id, 1);
  }
 
  incremental_dirtyt dirty;
 
  void add_function_loops(const irep_idt &identifier, const goto_programt &body)
  {
    auto loop_iter = loop_analysis_map.find(identifier);
    if(loop_iter == loop_analysis_map.end())
    {
      loop_analysis_map[identifier] =
        std::make_shared<lexical_loopst>(lexical_loopst(body));
    }
  }
 
  inline std::shared_ptr<lexical_loopst>
  get_loop_analysis(const irep_idt &function_id)
  {
    return loop_analysis_map.at(function_id);
  }
 
private:
  std::unordered_map<irep_idt, std::shared_ptr<lexical_loopst>>
    loop_analysis_map;
 
  // Derived classes should override these methods, allowing the base class to
  // enforce preconditions.
  virtual patht &private_peek() = 0;
  virtual void private_pop() = 0;
 
  typedef std::unordered_map<irep_idt, std::size_t> name_index_mapt;
 
  std::size_t get_unique_index(
    name_index_mapt &unique_index_map,
    const irep_idt &id,
    std::size_t minimum_index)
  {
    auto entry = unique_index_map.emplace(id, minimum_index);
 
    if(!entry.second)
      entry.first->second = std::max(entry.first->second + 1, minimum_index);
 
    return entry.first->second;
  }
 
  name_index_mapt l1_indices;
  name_index_mapt l2_indices;
};
 
class path_lifot : public path_storaget
{
public:
  void push(const patht &) override;
  std::size_t size() const override;
  void clear() override;
 
protected:
  std::list<path_storaget::patht>::iterator last_peeked;
  std::list<patht> paths;
 
private:
  patht &private_peek() override;
  void private_pop() override;
};
 
class path_fifot : public path_storaget
{
public:
  void push(const patht &) override;
  std::size_t size() const override;
  void clear() override;
 
protected:
  std::list<patht> paths;
 
private:
  patht &private_peek() override;
  void private_pop() override;
};
 
std::string show_path_strategies();
 
bool is_valid_path_strategy(const std::string strategy);
 
std::unique_ptr<path_storaget> get_path_strategy(const std::string strategy);
 
void parse_path_strategy_options(
  const cmdlinet &,
  optionst &,
  message_handlert &);
 
#endif /* CPROVER_GOTO_SYMEX_PATH_STORAGE_H */