cprover
unwindset.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Loop unwinding setup
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "unwindset.h"
10
12#include <util/message.h>
13#include <util/string2int.h>
14#include <util/string_utils.h>
15
16#ifdef _MSC_VER
17# include <util/unicode.h>
18#endif
19
20#include <fstream>
21
22void unwindsett::parse_unwind(const std::string &unwind)
23{
24 if(!unwind.empty())
26}
27
29 std::string val,
30 message_handlert &message_handler)
31{
32 if(val.empty())
33 return;
34
35 optionalt<unsigned> thread_nr;
36 if(isdigit(val[0]))
37 {
38 auto c_pos = val.find(':');
39 if(c_pos != std::string::npos)
40 {
41 std::string nr = val.substr(0, c_pos);
42 thread_nr = unsafe_string2unsigned(nr);
43 val.erase(0, nr.size() + 1);
44 }
45 }
46
47 auto last_c_pos = val.rfind(':');
48 if(last_c_pos != std::string::npos)
49 {
50 std::string id = val.substr(0, last_c_pos);
51
52 // The loop id can take three forms:
53 // 1) Just a function name to limit recursion.
54 // 2) F.N where F is a function name and N is a loop number.
55 // 3) F.L where F is a function name and L is a label.
56 const symbol_tablet &symbol_table = goto_model.get_symbol_table();
57 const symbolt *maybe_fn = symbol_table.lookup(id);
58 if(maybe_fn && maybe_fn->type.id() == ID_code)
59 {
60 // ok, recursion limit
61 }
62 else
63 {
64 auto last_dot_pos = val.rfind('.');
65 if(last_dot_pos == std::string::npos)
66 {
68 "invalid loop identifier " + id, "unwindset"};
69 }
70
71 std::string function_id = id.substr(0, last_dot_pos);
72 std::string loop_nr_label = id.substr(last_dot_pos + 1);
73
74 if(loop_nr_label.empty())
75 {
77 "invalid loop identifier " + id, "unwindset"};
78 }
79
80 if(!goto_model.can_produce_function(function_id))
81 {
82 messaget log{message_handler};
83 log.warning() << "loop identifier " << id
84 << " for non-existent function provided with unwindset"
86 return;
87 }
88
89 const goto_functiont &goto_function =
90 goto_model.get_goto_function(function_id);
91 if(isdigit(loop_nr_label[0]))
92 {
93 auto nr = string2optional_unsigned(loop_nr_label);
94 if(!nr.has_value())
95 {
97 "invalid loop identifier " + id, "unwindset"};
98 }
99
100 bool found = std::any_of(
101 goto_function.body.instructions.begin(),
102 goto_function.body.instructions.end(),
103 [&nr](const goto_programt::instructiont &instruction) {
104 return instruction.is_backwards_goto() &&
105 instruction.loop_number == nr;
106 });
107 if(!found)
108 {
109 messaget log{message_handler};
110 log.warning() << "loop identifier " << id
111 << " provided with unwindset does not match any loop"
112 << messaget::eom;
113 return;
114 }
115 }
116 else
117 {
120 for(const auto &instruction : goto_function.body.instructions)
121 {
122 if(
123 std::find(
124 instruction.labels.begin(),
125 instruction.labels.end(),
126 loop_nr_label) != instruction.labels.end())
127 {
128 location = instruction.source_location();
129 }
130 if(
131 location.has_value() && instruction.is_backwards_goto() &&
132 instruction.source_location() == *location)
133 {
134 nr = instruction.loop_number;
135 break;
136 }
137 }
138 if(!nr.has_value())
139 {
140 messaget log{message_handler};
141 log.warning() << "loop identifier " << id
142 << " provided with unwindset does not match any loop"
143 << messaget::eom;
144 return;
145 }
146 else
147 id = function_id + "." + std::to_string(*nr);
148 }
149 }
150
151 std::string uw_string = val.substr(last_c_pos + 1);
152
153 // the below initialisation makes g++-5 happy
155
156 if(uw_string.empty())
157 uw = {};
158 else
159 uw = unsafe_string2unsigned(uw_string);
160
161 if(thread_nr.has_value())
162 thread_loop_map[std::pair<irep_idt, unsigned>(id, *thread_nr)] = uw;
163 else
164 loop_map[id] = uw;
165 }
166}
167
169 const std::list<std::string> &unwindset,
170 message_handlert &message_handler)
171{
172 for(auto &element : unwindset)
173 {
174 std::vector<std::string> unwindset_elements =
175 split_string(element, ',', true, true);
176
177 for(auto &element : unwindset_elements)
178 parse_unwindset_one_loop(element, message_handler);
179 }
180}
181
183unwindsett::get_limit(const irep_idt &loop_id, unsigned thread_nr) const
184{
185 // We use the most specific limit we have
186
187 // thread x loop
188 auto tl_it =
189 thread_loop_map.find(std::pair<irep_idt, unsigned>(loop_id, thread_nr));
190
191 if(tl_it != thread_loop_map.end())
192 return tl_it->second;
193
194 // loop
195 auto l_it = loop_map.find(loop_id);
196
197 if(l_it != loop_map.end())
198 return l_it->second;
199
200 // global, if any
201 return global_limit;
202}
203
205 const std::string &file_name,
206 message_handlert &message_handler)
207{
208 #ifdef _MSC_VER
209 std::ifstream file(widen(file_name));
210 #else
211 std::ifstream file(file_name);
212 #endif
213
214 if(!file)
215 throw "cannot open file "+file_name;
216
217 std::stringstream buffer;
218 buffer << file.rdbuf();
219
220 std::vector<std::string> unwindset_elements =
221 split_string(buffer.str(), ',', true, true);
222
223 for(auto &element : unwindset_elements)
224 parse_unwindset_one_loop(element, message_handler);
225}
virtual bool can_produce_function(const irep_idt &id) const =0
Determines if this model can produce a body for the given function.
virtual const goto_functionst::goto_functiont & get_goto_function(const irep_idt &id)=0
Get a GOTO function by name, or throw if no such function exists.
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
goto_programt body
Definition: goto_function.h:26
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:598
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
const irep_idt & id() const
Definition: irep.h:396
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
static eomt eom
Definition: message.h:297
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
typet type
Type of symbol.
Definition: symbol.h:31
loop_mapt loop_map
Definition: unwindset.h:59
void parse_unwindset_one_loop(std::string loop_limit, message_handlert &message_handler)
Definition: unwindset.cpp:28
void parse_unwind(const std::string &unwind)
Definition: unwindset.cpp:22
optionalt< unsigned > global_limit
Definition: unwindset.h:54
thread_loop_mapt thread_loop_map
Definition: unwindset.h:64
void parse_unwindset_file(const std::string &file_name, message_handlert &message_handler)
Definition: unwindset.cpp:204
abstract_goto_modelt & goto_model
Definition: unwindset.h:52
optionalt< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
Definition: unwindset.cpp:183
void parse_unwindset(const std::list< std::string > &unwindset, message_handlert &message_handler)
Definition: unwindset.cpp:168
nonstd::optional< T > optionalt
Definition: optional.h:35
optionalt< unsigned > string2optional_unsigned(const std::string &str, int base)
Convert string to unsigned similar to the stoul or stoull functions, return nullopt when the conversi...
Definition: string2int.cpp:64
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:35
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Definition: kdev_t.h:19
std::wstring widen(const char *s)
Definition: unicode.cpp:48
Loop unwinding.