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 
61  virtual void
62  push(const patht &next_instruction, const patht &jump_target) = 0;
63 
65  void pop()
66  {
67  PRECONDITION(!empty());
68  private_pop();
69  }
70 
72  virtual std::size_t size() const = 0;
73 
75  bool empty() const
76  {
77  return size() == 0;
78  };
79 
80 private:
81  // Derived classes should override these methods, allowing the base class to
82  // enforce preconditions.
83  virtual patht &private_peek() = 0;
84  virtual void private_pop() = 0;
85 };
86 
88 class path_lifot : public path_storaget
89 {
90 public:
91  void push(const patht &, const patht &) override;
92  std::size_t size() const override;
93 
94 protected:
95  std::list<path_storaget::patht>::iterator last_peeked;
96  std::list<patht> paths;
97 
98 private:
99  patht &private_peek() override;
100  void private_pop() override;
101 };
102 
104 class path_fifot : public path_storaget
105 {
106 public:
107  void push(const patht &, const patht &) override;
108  std::size_t size() const override;
109 
110 protected:
111  std::list<patht> paths;
112 
113 private:
114  patht &private_peek() override;
115  void private_pop() override;
116 };
117 
120 {
121 public:
123 
125  std::string show_strategies() const;
126 
128  bool is_valid_strategy(const std::string strategy) const
129  {
130  return strategies.find(strategy) != strategies.end();
131  }
132 
137  std::unique_ptr<path_storaget> get(const std::string strategy) const
138  {
139  auto found = strategies.find(strategy);
140  INVARIANT(
141  found != strategies.end(), "Unknown strategy '" + strategy + "'.");
142  return found->second.second();
143  }
144 
147  void
149 
150 protected:
151  std::string default_strategy() const
152  {
153  return "lifo";
154  }
155 
159  std::map<const std::string,
160  std::pair<const std::string,
161  const std::function<std::unique_ptr<path_storaget>()>>>
163 };
164 
165 #endif /* CPROVER_GOTO_SYMEX_PATH_STORAGE_H */
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 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.
symex_target_equationt equation
Definition: path_storage.h:30
virtual void private_pop()=0
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
Factory and information for path_storaget.
Definition: path_storage.h:119
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:104
bool is_valid_strategy(const std::string strategy) const
is there a factory constructor for the named strategy?
Definition: path_storage.h:128
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:230
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:88
void pop()
Remove the next path to resume from the storage.
Definition: path_storage.h:65
patht & peek()
Reference to the next path to resume.
Definition: path_storage.h:47
std::list< patht > paths
Definition: path_storage.h:111
virtual std::size_t size() const =0
How many paths does this storage contain?
std::string default_strategy() const
Definition: path_storage.h:151
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:75
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:96
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:162
std::list< path_storaget::patht >::iterator last_peeked
Definition: path_storage.h:95