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 */
virtual void clear()=0
Clear all saved paths.
Generate Equation using Symbolic Execution.
void private_pop() override
patht & private_peek() override
patht(const symex_target_equationt &e, const goto_symex_statet &s)
Definition: path_storage.h:33
void clear() override
Clear all saved paths.
void push(const patht &, const patht &) override
Add paths to resume to the storage.
std::size_t size() const override
How many paths does this storage contain?
Symbolic Execution.
void clear() override
Clear all saved paths.
symex_target_equationt equation
Definition: path_storage.h:30
virtual void private_pop()=0
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
Factory and information for path_storaget.
Definition: path_storage.h:129
std::string show_strategies() const
suitable for displaying as a front-end help message
void set_path_strategy_options(const cmdlinet &, optionst &, messaget &) const
add paths and exploration-strategy option, suitable to be invoked from front-ends.
FIFO save queue: paths are resumed in the order that they were saved.
Definition: path_storage.h:113
bool is_valid_strategy(const std::string strategy) const
is there a factory constructor for the named strategy?
Definition: path_storage.h:138
patht(const patht &other)
Definition: path_storage.h:38
std::list< path_nodet > patht
Definition: path.h:45
std::size_t size() const override
How many paths does this storage contain?
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
void private_pop() override
patht & private_peek() override
Storage for symbolic execution paths to be resumed later.
Definition: path_storage.h:24
void push(const patht &, const patht &) override
LIFO save queue: depth-first search, try to finish paths.
Definition: path_storage.h:96
void pop()
Remove the next path to resume from the storage.
Definition: path_storage.h:73
patht & peek()
Reference to the next path to resume.
Definition: path_storage.h:47
std::list< patht > paths
Definition: path_storage.h:121
virtual std::size_t size() const =0
How many paths does this storage contain?
std::string default_strategy() const
Definition: path_storage.h:161
Information saved at a conditional goto to resume execution.
Definition: path_storage.h:28
bool empty() const
Is this storage empty?
Definition: path_storage.h:83
virtual ~path_storaget()=default
Options.
virtual patht & private_peek()=0
virtual void push(const patht &next_instruction, const patht &jump_target)=0
Add paths to resume to the storage.
goto_symex_statet state
Definition: path_storage.h:31
std::list< patht > paths
Definition: path_storage.h:105
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
std::list< path_storaget::patht >::iterator last_peeked
Definition: path_storage.h:104