cprover
Loading...
Searching...
No Matches
path_storage.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Path Storage
4
5Author: Kareem Khazem <karkhaz@karkhaz.com>
6
7\*******************************************************************/
8
9#include "path_storage.h"
10
11#include <sstream>
12
13#include <util/cmdline.h>
14#include <util/exit_codes.h>
15#include <util/make_unique.h>
16
18operator()(typet type, source_locationt location)
19{
20 return nondet_symbol_exprt{"symex::nondet" + std::to_string(nondet_count++),
21 std::move(type),
22 std::move(location)};
23}
24
25// _____________________________________________________________________________
26// path_lifot
27
29{
30 last_peeked = paths.end();
32 return paths.back();
33}
34
36{
37 paths.push_back(path);
38}
39
41{
43 paths.erase(last_peeked);
44 last_peeked = paths.end();
45}
46
47std::size_t path_lifot::size() const
48{
49 return paths.size();
50}
51
53{
54 paths.clear();
55}
56
57// _____________________________________________________________________________
58// path_fifot
59
64
66{
67 paths.push_back(path);
68}
69
71{
72 paths.pop_front();
73}
74
75std::size_t path_fifot::size() const
76{
77 return paths.size();
78}
79
81{
82 paths.clear();
83}
84
85// _____________________________________________________________________________
86// path_strategy_choosert
87
88static const std::map<
89 const std::string,
90 std::pair<
91 const std::string,
92 const std::function<std::unique_ptr<path_storaget>()>>>
94 {{"lifo",
95 {" lifo next instruction is pushed before\n"
96 " goto target; paths are popped in\n"
97 " last-in, first-out order. Explores\n"
98 " the program tree depth-first.\n",
99 []() { // NOLINT(whitespace/braces)
101 }}},
102 {"fifo",
103 {" fifo next instruction is pushed before\n"
104 " goto target; paths are popped in\n"
105 " first-in, first-out order. Explores\n"
106 " the program tree breadth-first.\n",
107 []() { // NOLINT(whitespace/braces)
109 }}}});
110
112{
113 std::stringstream ss;
114 for(auto &pair : path_strategies)
115 ss << pair.second.first;
116 return ss.str();
117}
118
120{
121 return "lifo";
122}
123
124bool is_valid_path_strategy(const std::string strategy)
125{
126 return path_strategies.find(strategy) != path_strategies.end();
127}
128
129std::unique_ptr<path_storaget> get_path_strategy(const std::string strategy)
130{
131 auto found = path_strategies.find(strategy);
132 INVARIANT(
133 found != path_strategies.end(), "Unknown strategy '" + strategy + "'.");
134 return found->second.second();
135}
136
138 const cmdlinet &cmdline,
139 optionst &options,
140 message_handlert &message_handler)
141{
142 messaget log(message_handler);
143 if(cmdline.isset("paths"))
144 {
145 options.set_option("paths", true);
146 std::string strategy = cmdline.get_value("paths");
148 {
149 log.error() << "Unknown strategy '" << strategy
150 << "'. Pass the --show-symex-strategies flag to list "
151 "available strategies."
152 << messaget::eom;
154 }
155 options.set_option("exploration-strategy", strategy);
156 }
157 else
158 {
159 options.set_option("exploration-strategy", default_path_strategy());
160 }
161}
virtual void clear()
Reset the abstract state.
Definition ai.h:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
std::string get_value(char option) const
Definition cmdline.cpp:48
virtual bool isset(char option) const
Definition cmdline.cpp:30
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
mstreamt & error() const
Definition message.h:399
static eomt eom
Definition message.h:297
Expression to hold a nondeterministic choice.
Definition std_expr.h:209
void set_option(const std::string &option, const bool value)
Definition options.cpp:28
void clear() override
Clear all saved paths.
void private_pop() override
patht & private_peek() override
std::list< patht > paths
void push(const patht &) override
Add a path to resume to the storage.
std::size_t size() const override
How many paths does this storage contain?
std::list< patht > paths
void private_pop() override
std::list< path_storaget::patht >::iterator last_peeked
void push(const patht &) override
Add a path to resume to the storage.
patht & private_peek() override
std::size_t size() const override
How many paths does this storage contain?
void clear() override
Clear all saved paths.
nondet_symbol_exprt operator()(typet type, source_locationt location)
The type of an expression, extends irept.
Definition type.h:29
Document and give macros for the exit codes of CPROVER binaries.
#define CPROVER_EXIT_USAGE_ERROR
A usage error is returned when the command line is invalid or conflicting.
Definition exit_codes.h:33
std::string default_path_strategy()
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 >();}}}})
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 ...
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.
bool is_valid_path_strategy(const std::string strategy)
is there a factory constructor for the named strategy?
std::string show_path_strategies()
suitable for displaying as a front-end help message
Storage of symbolic execution paths to resume.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
Information saved at a conditional goto to resume execution.