cprover
path_storage.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Path Storage
4 
5 Author: Kareem Khazem <karkhaz@karkhaz.com>
6 
7 \*******************************************************************/
8 
9 #include "path_storage.h"
10 
11 #include <sstream>
12 
13 #include <util/exit_codes.h>
14 #include <util/make_unique.h>
15 
16 // _____________________________________________________________________________
17 // path_lifot
18 
20 {
21  last_peeked = paths.end();
22  --last_peeked;
23  return paths.back();
24 }
25 
27  const path_storaget::patht &next_instruction,
28  const path_storaget::patht &jump_target)
29 {
30  paths.push_back(next_instruction);
31  paths.push_back(jump_target);
32 }
33 
35 {
36  PRECONDITION(last_peeked != paths.end());
37  paths.erase(last_peeked);
38  last_peeked = paths.end();
39 }
40 
41 std::size_t path_lifot::size() const
42 {
43  return paths.size();
44 }
45 
47 {
48  paths.clear();
49 }
50 
51 // _____________________________________________________________________________
52 // path_fifot
53 
55 {
56  return paths.front();
57 }
58 
60  const path_storaget::patht &next_instruction,
61  const path_storaget::patht &jump_target)
62 {
63  paths.push_back(next_instruction);
64  paths.push_back(jump_target);
65 }
66 
68 {
69  paths.pop_front();
70 }
71 
72 std::size_t path_fifot::size() const
73 {
74  return paths.size();
75 }
76 
78 {
79  paths.clear();
80 }
81 
82 // _____________________________________________________________________________
83 // path_strategy_choosert
84 
86 {
87  std::stringstream ss;
88  for(auto &pair : strategies)
89  ss << pair.second.first;
90  return ss.str();
91 }
92 
94  const cmdlinet &cmdline,
95  optionst &options,
96  messaget &message) const
97 {
98  if(cmdline.isset("paths"))
99  {
100  options.set_option("paths", true);
101  std::string strategy = cmdline.get_value("paths");
102  if(!is_valid_strategy(strategy))
103  {
104  message.error() << "Unknown strategy '" << strategy
105  << "'. Pass the --show-symex-strategies flag to list "
106  "available strategies."
107  << message.eom;
109  }
110  options.set_option("exploration-strategy", strategy);
111  }
112  else
113  options.set_option("exploration-strategy", default_strategy());
114 }
115 
117  : strategies(
118  {{"lifo",
119  {" lifo next instruction is pushed before\n"
120  " goto target; paths are popped in\n"
121  " last-in, first-out order. Explores\n"
122  " the program tree depth-first.\n",
123  []() { // NOLINT(whitespace/braces)
124  return util_make_unique<path_lifot>();
125  }}},
126  {"fifo",
127  {" fifo next instruction is pushed before\n"
128  " goto target; paths are popped in\n"
129  " first-in, first-out order. Explores\n"
130  " the program tree breadth-first.\n",
131  []() { // NOLINT(whitespace/braces)
132  return util_make_unique<path_fifot>();
133  }}}})
134 {
135 }
void private_pop() override
patht & private_peek() override
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?
void clear() override
Clear all saved paths.
std::string get_value(char option) const
Definition: cmdline.cpp:45
std::string show_strategies() const
suitable for displaying as a front-end help message
virtual bool isset(char option) const
Definition: cmdline.cpp:27
void set_path_strategy_options(const cmdlinet &, optionst &, messaget &) const
add paths and exploration-strategy option, suitable to be invoked from front-ends.
bool is_valid_strategy(const std::string strategy) const
is there a factory constructor for the named strategy?
Definition: path_storage.h:138
std::size_t size() const override
How many paths does this storage contain?
mstreamt & error() const
Definition: message.h:386
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
void private_pop() override
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
patht & private_peek() override
void push(const patht &, const patht &) override
Add paths to resume to the storage.
static eomt eom
Definition: message.h:284
Document and give macros for the exit codes of CPROVER binaries.
std::list< patht > paths
Definition: path_storage.h:121
std::string default_strategy() const
Definition: path_storage.h:161
Information saved at a conditional goto to resume execution.
Definition: path_storage.h:28
void set_option(const std::string &option, const bool value)
Definition: options.cpp:26
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition: exit_codes.h:33
Storage of symbolic execution paths to resume.
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