cprover
path_storage.h
Go to the documentation of this file.
1 
5 #ifndef CPROVER_GOTO_SYMEX_PATH_STORAGE_H
6 #define CPROVER_GOTO_SYMEX_PATH_STORAGE_H
7 
8 #include "goto_symex_state.h"
10 
11 #include <util/options.h>
12 #include <util/cmdline.h>
13 #include <util/ui_message.h>
14 #include <util/invariant.h>
15 
16 #include <memory>
17 
25 {
26 public:
28  struct patht
29  {
32 
33  explicit patht(const symex_target_equationt &e, const goto_symex_statet &s)
34  : equation(e), state(s, &equation)
35  {
36  }
37 
38  explicit patht(const patht &other)
39  : equation(other.equation), state(other.state, &equation)
40  {
41  }
42  };
43 
44  virtual ~path_storaget() = default;
45 
48  {
49  PRECONDITION(!empty());
50  return private_peek();
51  }
52 
59  virtual void clear() = 0;
60 
69  virtual void
70  push(const patht &next_instruction, const patht &jump_target) = 0;
71 
73  void pop()
74  {
75  PRECONDITION(!empty());
76  private_pop();
77  }
78 
80  virtual std::size_t size() const = 0;
81 
83  bool empty() const
84  {
85  return size() == 0;
86  };
87 
88 private:
89  // Derived classes should override these methods, allowing the base class to
90  // enforce preconditions.
91  virtual patht &private_peek() = 0;
92  virtual void private_pop() = 0;
93 };
94 
96 class path_lifot : public path_storaget
97 {
98 public:
99  void push(const patht &, const patht &) override;
100  std::size_t size() const override;
101  void clear() override;
102 
103 protected:
104  std::list<path_storaget::patht>::iterator last_peeked;
105  std::list<patht> paths;
106 
107 private:
108  patht &private_peek() override;
109  void private_pop() override;
110 };
111 
113 class path_fifot : public path_storaget
114 {
115 public:
116  void push(const patht &, const patht &) override;
117  std::size_t size() const override;
118  void clear() override;
119 
120 protected:
121  std::list<patht> paths;
122 
123 private:
124  patht &private_peek() override;
125  void private_pop() override;
126 };
127 
130 {
131 public:
133 
135  std::string show_strategies() const;
136 
138  bool is_valid_strategy(const std::string strategy) const
139  {
140  return strategies.find(strategy) != strategies.end();
141  }
142 
147  std::unique_ptr<path_storaget> get(const std::string strategy) const
148  {
149  auto found = strategies.find(strategy);
150  INVARIANT(
151  found != strategies.end(), "Unknown strategy '" + strategy + "'.");
152  return found->second.second();
153  }
154 
157  void
159 
160 protected:
161  std::string default_strategy() const
162  {
163  return "lifo";
164  }
165 
169  std::map<const std::string,
170  std::pair<const std::string,
171  const std::function<std::unique_ptr<path_storaget>()>>>
173 };
174 
175 #endif /* CPROVER_GOTO_SYMEX_PATH_STORAGE_H */
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
symex_target_equation.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
path_strategy_choosert::get
std::unique_ptr< path_storaget > get(const std::string strategy) const
Factory for a path_storaget.
Definition: path_storage.h:147
path_storaget::empty
bool empty() const
Is this storage empty?
Definition: path_storage.h:83
path_lifot::private_peek
patht & private_peek() override
Definition: path_storage.cpp:19
path_storaget::peek
patht & peek()
Reference to the next path to resume.
Definition: path_storage.h:47
path_storaget::patht::patht
patht(const symex_target_equationt &e, const goto_symex_statet &s)
Definition: path_storage.h:33
path_fifot
FIFO save queue: paths are resumed in the order that they were saved.
Definition: path_storage.h:113
optionst
Definition: options.h:22
path_fifot::push
void push(const patht &, const patht &) override
Add paths to resume to the storage.
Definition: path_storage.cpp:59
path_lifot::paths
std::list< patht > paths
Definition: path_storage.h:105
path_storaget
Storage for symbolic execution paths to be resumed later.
Definition: path_storage.h:24
goto_symex_statet
Definition: goto_symex_state.h:34
path_strategy_choosert::strategies
std::map< const std::string, std::pair< const std::string, const std::function< std::unique_ptr< path_storaget >)> > > strategies
Map from the name of a strategy (to be supplied on the command line), to the help text for that strat...
Definition: path_storage.h:172
options.h
invariant.h
path_storaget::~path_storaget
virtual ~path_storaget()=default
path_strategy_choosert::path_strategy_choosert
path_strategy_choosert()
Definition: path_storage.cpp:116
path_fifot::clear
void clear() override
Clear all saved paths.
Definition: path_storage.cpp:77
path_storaget::pop
void pop()
Remove the next path to resume from the storage.
Definition: path_storage.h:73
path_lifot::clear
void clear() override
Clear all saved paths.
Definition: path_storage.cpp:46
path_strategy_choosert::set_path_strategy_options
void set_path_strategy_options(const cmdlinet &, optionst &, messaget &) const
add paths and exploration-strategy option, suitable to be invoked from front-ends.
Definition: path_storage.cpp:93
path_storaget::patht::equation
symex_target_equationt equation
Definition: path_storage.h:30
cmdlinet
Definition: cmdline.h:19
path_fifot::private_peek
patht & private_peek() override
Definition: path_storage.cpp:54
path_fifot::size
std::size_t size() const override
How many paths does this storage contain?
Definition: path_storage.cpp:72
path_strategy_choosert::show_strategies
std::string show_strategies() const
suitable for displaying as a front-end help message
Definition: path_storage.cpp:85
path_storaget::private_pop
virtual void private_pop()=0
path_fifot::private_pop
void private_pop() override
Definition: path_storage.cpp:67
path_storaget::patht::patht
patht(const patht &other)
Definition: path_storage.h:38
path_storaget::clear
virtual void clear()=0
Clear all saved paths.
path_lifot::push
void push(const patht &, const patht &) override
Add paths to resume to the storage.
Definition: path_storage.cpp:26
path_storaget::patht
Information saved at a conditional goto to resume execution.
Definition: path_storage.h:28
path_lifot::last_peeked
std::list< path_storaget::patht >::iterator last_peeked
Definition: path_storage.h:104
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:35
path_strategy_choosert::default_strategy
std::string default_strategy() const
Definition: path_storage.h:161
goto_symex_state.h
path_lifot::private_pop
void private_pop() override
Definition: path_storage.cpp:34
patht
std::list< path_nodet > patht
Definition: path.h:45
path_storaget::patht::state
goto_symex_statet state
Definition: path_storage.h:31
cmdline.h
path_fifot::paths
std::list< patht > paths
Definition: path_storage.h:121
path_strategy_choosert::is_valid_strategy
bool is_valid_strategy(const std::string strategy) const
is there a factory constructor for the named strategy?
Definition: path_storage.h:138
path_strategy_choosert
Factory and information for path_storaget.
Definition: path_storage.h:129
path_lifot::size
std::size_t size() const override
How many paths does this storage contain?
Definition: path_storage.cpp:41
path_storaget::push
virtual void push(const patht &next_instruction, const patht &jump_target)=0
Add paths to resume to the storage.
path_lifot
LIFO save queue: depth-first search, try to finish paths.
Definition: path_storage.h:96
path_storaget::size
virtual std::size_t size() const =0
How many paths does this storage contain?
path_storaget::private_peek
virtual patht & private_peek()=0
validation_modet::INVARIANT
ui_message.h