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 
17 operator()(typet type, source_locationt location)
18 {
19  return nondet_symbol_exprt{"symex::nondet" + std::to_string(nondet_count++),
20  std::move(type),
21  std::move(location)};
22 }
23 
24 // _____________________________________________________________________________
25 // path_lifot
26 
28 {
29  last_peeked = paths.end();
30  --last_peeked;
31  return paths.back();
32 }
33 
35 {
36  paths.push_back(path);
37 }
38 
40 {
41  PRECONDITION(last_peeked != paths.end());
42  paths.erase(last_peeked);
43  last_peeked = paths.end();
44 }
45 
46 std::size_t path_lifot::size() const
47 {
48  return paths.size();
49 }
50 
52 {
53  paths.clear();
54 }
55 
56 // _____________________________________________________________________________
57 // path_fifot
58 
60 {
61  return paths.front();
62 }
63 
65 {
66  paths.push_back(path);
67 }
68 
70 {
71  paths.pop_front();
72 }
73 
74 std::size_t path_fifot::size() const
75 {
76  return paths.size();
77 }
78 
80 {
81  paths.clear();
82 }
83 
84 // _____________________________________________________________________________
85 // path_strategy_choosert
86 
87 static const std::map<
88  const std::string,
89  std::pair<
90  const std::string,
91  const std::function<std::unique_ptr<path_storaget>()>>>
93  {{"lifo",
94  {" lifo next instruction is pushed before\n"
95  " goto target; paths are popped in\n"
96  " last-in, first-out order. Explores\n"
97  " the program tree depth-first.\n",
98  []() { // NOLINT(whitespace/braces)
99  return util_make_unique<path_lifot>();
100  }}},
101  {"fifo",
102  {" fifo next instruction is pushed before\n"
103  " goto target; paths are popped in\n"
104  " first-in, first-out order. Explores\n"
105  " the program tree breadth-first.\n",
106  []() { // NOLINT(whitespace/braces)
107  return util_make_unique<path_fifot>();
108  }}}});
109 
110 std::string show_path_strategies()
111 {
112  std::stringstream ss;
113  for(auto &pair : path_strategies)
114  ss << pair.second.first;
115  return ss.str();
116 }
117 
119 {
120  return "lifo";
121 }
122 
123 bool is_valid_path_strategy(const std::string strategy)
124 {
125  return path_strategies.find(strategy) != path_strategies.end();
126 }
127 
128 std::unique_ptr<path_storaget> get_path_strategy(const std::string strategy)
129 {
130  auto found = path_strategies.find(strategy);
131  INVARIANT(
132  found != path_strategies.end(), "Unknown strategy '" + strategy + "'.");
133  return found->second.second();
134 }
135 
137  const cmdlinet &cmdline,
138  optionst &options,
139  message_handlert &message_handler)
140 {
141  messaget log(message_handler);
142  if(cmdline.isset("paths"))
143  {
144  options.set_option("paths", true);
145  std::string strategy = cmdline.get_value("paths");
146  if(!is_valid_path_strategy(strategy))
147  {
148  log.error() << "Unknown strategy '" << strategy
149  << "'. Pass the --show-symex-strategies flag to list "
150  "available strategies."
151  << messaget::eom;
153  }
154  options.set_option("exploration-strategy", strategy);
155  }
156  else
157  {
158  options.set_option("exploration-strategy", default_path_strategy());
159  }
160 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
path_lifot::private_peek
patht & private_peek() override
Definition: path_storage.cpp:27
nondet_symbol_exprt
Expression to hold a nondeterministic choice.
Definition: std_expr.h:197
cmdlinet::isset
virtual bool isset(char option) const
Definition: cmdline.cpp:29
path_fifot::push
void push(const patht &) override
Add a path to resume to the storage.
Definition: path_storage.cpp:64
optionst
Definition: options.h:23
typet
The type of an expression, extends irept.
Definition: type.h:29
path_lifot::paths
std::list< patht > paths
Definition: path_storage.h:175
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
path_fifot::clear
void clear() override
Clear all saved paths.
Definition: path_storage.cpp:79
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:297
path_lifot::clear
void clear() override
Clear all saved paths.
Definition: path_storage.cpp:51
path_storage.h
Storage of symbolic execution paths to resume.
parse_path_strategy_options
void parse_path_strategy_options(const cmdlinet &cmdline, optionst &options, message_handlert &message_handler)
add paths and exploration-strategy option, suitable to be invoked from front-ends.
Definition: path_storage.cpp:136
cmdlinet
Definition: cmdline.h:21
make_unique.h
messaget::error
mstreamt & error() const
Definition: message.h:399
default_path_strategy
std::string default_path_strategy()
Definition: path_storage.cpp:118
path_fifot::private_peek
patht & private_peek() override
Definition: path_storage.cpp:59
path_fifot::size
std::size_t size() const override
How many paths does this storage contain?
Definition: path_storage.cpp:74
symex_nondet_generatort::operator()
nondet_symbol_exprt operator()(typet type, source_locationt location)
Definition: path_storage.cpp:17
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
cmdlinet::get_value
std::string get_value(char option) const
Definition: cmdline.cpp:47
path_fifot::private_pop
void private_pop() override
Definition: path_storage.cpp:69
message_handlert
Definition: message.h:28
path_storaget::patht
Information saved at a conditional goto to resume execution.
Definition: path_storage.h:42
path_lifot::last_peeked
std::list< path_storaget::patht >::iterator last_peeked
Definition: path_storage.h:174
source_locationt
Definition: source_location.h:20
path_lifot::private_pop
void private_pop() override
Definition: path_storage.cpp:39
exit_codes.h
Document and give macros for the exit codes of CPROVER binaries.
path_fifot::paths
std::list< patht > paths
Definition: path_storage.h:191
CPROVER_EXIT_USAGE_ERROR
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition: exit_codes.h:33
path_lifot::push
void push(const patht &) override
Add a path to resume to the storage.
Definition: path_storage.cpp:34
show_path_strategies
std::string show_path_strategies()
suitable for displaying as a front-end help message
Definition: path_storage.cpp:110
path_lifot::size
std::size_t size() const override
How many paths does this storage contain?
Definition: path_storage.cpp:46
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
symex_nondet_generatort::nondet_count
std::size_t nondet_count
Definition: path_storage.h:28
is_valid_path_strategy
bool is_valid_path_strategy(const std::string strategy)
is there a factory constructor for the named strategy?
Definition: path_storage.cpp:123
path_strategies
static const std::map< const std::string, std::pair< const std::string, const std::function< std::unique_ptr< path_storaget >)> > > path_strategies({{"lifo", {" lifo next instruction is pushed before\n" " goto target; paths are popped in\n" " last-in, first-out order. Explores\n" " the program tree depth-first.\n", []() { return util_make_unique< path_lifot >();}}}, {"fifo", {" fifo next instruction is pushed before\n" " goto target; paths are popped in\n" " first-in, first-out order. Explores\n" " the program tree breadth-first.\n", []() { return util_make_unique< path_fifot >();}}}})
get_path_strategy
std::unique_ptr< path_storaget > get_path_strategy(const std::string strategy)
Ensure that is_valid_strategy() returns true for a particular string before calling this function on ...
Definition: path_storage.cpp:128