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 
46 // _____________________________________________________________________________
47 // path_fifot
48 
50 {
51  return paths.front();
52 }
53 
55  const path_storaget::patht &next_instruction,
56  const path_storaget::patht &jump_target)
57 {
58  paths.push_back(next_instruction);
59  paths.push_back(jump_target);
60 }
61 
63 {
64  paths.pop_front();
65 }
66 
67 std::size_t path_fifot::size() const
68 {
69  return paths.size();
70 }
71 
72 // _____________________________________________________________________________
73 // path_strategy_choosert
74 
76 {
77  std::stringstream ss;
78  for(auto &pair : strategies)
79  ss << pair.second.first;
80  return ss.str();
81 }
82 
84  const cmdlinet &cmdline,
85  optionst &options,
86  messaget &message) const
87 {
88  if(cmdline.isset("paths"))
89  {
90  options.set_option("paths", true);
91  std::string strategy = cmdline.get_value("paths");
92  if(!is_valid_strategy(strategy))
93  {
94  message.error() << "Unknown strategy '" << strategy
95  << "'. Pass the --show-symex-strategies flag to list "
96  "available strategies."
97  << message.eom;
99  }
100  options.set_option("exploration-strategy", strategy);
101  }
102  else
103  options.set_option("exploration-strategy", default_strategy());
104 }
105 
107  : strategies(
108  {{"lifo",
109  {" lifo next instruction is pushed before\n"
110  " goto target; paths are popped in\n"
111  " last-in, first-out order. Explores\n"
112  " the program tree depth-first.\n",
113  []() { // NOLINT(whitespace/braces)
114  return util_make_unique<path_lifot>();
115  }}},
116  {"fifo",
117  {" fifo next instruction is pushed before\n"
118  " goto target; paths are popped in\n"
119  " first-in, first-out order. Explores\n"
120  " the program tree breadth-first.\n",
121  []() { // NOLINT(whitespace/braces)
122  return util_make_unique<path_fifot>();
123  }}}})
124 {
125 }
void private_pop() override
patht & private_peek() override
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?
std::string get_value(char option) const
Definition: cmdline.cpp:45
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
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:128
std::size_t size() const override
How many paths does this storage contain?
mstreamt & error() const
Definition: message.h:302
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
void private_pop() override
patht & private_peek() override
void push(const patht &, const patht &) override
Document and give macros for the exit codes of CPROVER binaries.
std::list< patht > paths
Definition: path_storage.h:111
std::string default_strategy() const
Definition: path_storage.h:151
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:24
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition: exit_codes.h:28
Storage of symbolic execution paths to resume.
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