cprover
Loading...
Searching...
No Matches
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#include <util/symbol_table.h>
16#include <util/unicode.h>
17
19
20#include <algorithm>
21#include <fstream>
22
23void unwindsett::parse_unwind(const std::string &unwind)
24{
25 if(!unwind.empty())
27}
28
30 std::string val,
31 message_handlert &message_handler)
32{
33 if(val.empty())
34 return;
35
36// Work around spurious GCC 12 warning about thread_nr being uninitialised.
37#pragma GCC diagnostic push
38#ifndef __clang__
39# pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
40#endif
41 optionalt<unsigned> thread_nr;
42#pragma GCC diagnostic pop
43 if(isdigit(val[0]))
44 {
45 auto c_pos = val.find(':');
46 if(c_pos != std::string::npos)
47 {
48 std::string nr = val.substr(0, c_pos);
49 thread_nr = unsafe_string2unsigned(nr);
50 val.erase(0, nr.size() + 1);
51 }
52 }
53
54 auto last_c_pos = val.rfind(':');
55 if(last_c_pos != std::string::npos)
56 {
57 std::string id = val.substr(0, last_c_pos);
58
59 // The loop id can take three forms:
60 // 1) Just a function name to limit recursion.
61 // 2) F.N where F is a function name and N is a loop number.
62 // 3) F.L where F is a function name and L is a label.
63 const symbol_table_baset &symbol_table = goto_model.get_symbol_table();
64 const symbolt *maybe_fn = symbol_table.lookup(id);
65 if(maybe_fn && maybe_fn->type.id() == ID_code)
66 {
67 // ok, recursion limit
68 }
69 else
70 {
71 auto last_dot_pos = val.rfind('.');
72 if(last_dot_pos == std::string::npos)
73 {
75 "invalid loop identifier " + id, "unwindset"};
76 }
77
78 std::string function_id = id.substr(0, last_dot_pos);
79 std::string loop_nr_label = id.substr(last_dot_pos + 1);
80
81 if(loop_nr_label.empty())
82 {
84 "invalid loop identifier " + id, "unwindset"};
85 }
86
87 if(!goto_model.can_produce_function(function_id))
88 {
89 messaget log{message_handler};
90 log.warning() << "loop identifier " << id
91 << " for non-existent function provided with unwindset"
93 return;
94 }
95
96 const goto_functiont &goto_function =
97 goto_model.get_goto_function(function_id);
99 {
101 if(!nr.has_value())
102 {
104 "invalid loop identifier " + id, "unwindset"};
105 }
106
107 bool found = std::any_of(
108 goto_function.body.instructions.begin(),
109 goto_function.body.instructions.end(),
110 [&nr](const goto_programt::instructiont &instruction) {
111 return instruction.is_backwards_goto() &&
112 instruction.loop_number == nr;
113 });
114 if(!found)
115 {
116 messaget log{message_handler};
117 log.warning() << "loop identifier " << id
118 << " provided with unwindset does not match any loop"
119 << messaget::eom;
120 return;
121 }
122 }
123 else
124 {
127 for(const auto &instruction : goto_function.body.instructions)
128 {
129 if(
130 std::find(
131 instruction.labels.begin(),
132 instruction.labels.end(),
133 loop_nr_label) != instruction.labels.end())
134 {
135 location = instruction.source_location();
136 // the label may be attached to the DECL part of an initializing
137 // declaration, which we may have marked as hidden
138 location->remove(ID_hide);
139 }
140 if(
141 location.has_value() && instruction.is_backwards_goto() &&
142 instruction.source_location() == *location)
143 {
144 if(nr.has_value())
145 {
146 messaget log{message_handler};
147 log.warning()
148 << "loop identifier " << id
149 << " provided with unwindset is ambiguous" << messaget::eom;
150 }
151 nr = instruction.loop_number;
152 }
153 }
154 if(!nr.has_value())
155 {
156 messaget log{message_handler};
157 log.warning() << "loop identifier " << id
158 << " provided with unwindset does not match any loop"
159 << messaget::eom;
160 return;
161 }
162 else
163// Work around spurious GCC 12 warning about thread_nr being uninitialised.
164#pragma GCC diagnostic push
165#ifndef __clang__
166# pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
167#endif
168 id = function_id + "." + std::to_string(*nr);
169#pragma GCC diagnostic pop
170 }
171 }
172
173 std::string uw_string = val.substr(last_c_pos + 1);
174
175 // the below initialisation makes g++-5 happy
177
178 if(uw_string.empty())
179 uw = {};
180 else
182
183 if(thread_nr.has_value())
184 {
185// Work around spurious GCC 12 warning about thread_nr being uninitialised.
186#pragma GCC diagnostic push
187#ifndef __clang__
188# pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
189#endif
190 thread_loop_map[std::pair<irep_idt, unsigned>(id, *thread_nr)] = uw;
191#pragma GCC diagnostic pop
192 }
193 else
194 {
195 loop_map[id] = uw;
196 }
197 }
198}
199
201 const std::list<std::string> &unwindset,
202 message_handlert &message_handler)
203{
204 for(auto &element : unwindset)
205 parse_unwindset_one_loop(element, message_handler);
206}
207
209unwindsett::get_limit(const irep_idt &loop_id, unsigned thread_nr) const
210{
211 // We use the most specific limit we have
212
213 // thread x loop
214 auto tl_it =
215 thread_loop_map.find(std::pair<irep_idt, unsigned>(loop_id, thread_nr));
216
217 if(tl_it != thread_loop_map.end())
218 return tl_it->second;
219
220 // loop
221 auto l_it = loop_map.find(loop_id);
222
223 if(l_it != loop_map.end())
224 return l_it->second;
225
226 // global, if any
227 return global_limit;
228}
229
231 const std::string &file_name,
232 message_handlert &message_handler)
233{
234 std::ifstream file(widen_if_needed(file_name));
235
236 if(!file)
237 throw "cannot open file "+file_name;
238
239 std::stringstream buffer;
240 buffer << file.rdbuf();
241
242 std::vector<std::string> unwindset_elements =
243 split_string(buffer.str(), ',', true, true);
244
245 for(auto &element : unwindset_elements)
246 parse_unwindset_one_loop(element, message_handler);
247}
Abstract interface to eager or lazy GOTO models.
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_programt body
This class represents an instruction in the GOTO intermediate representation.
instructionst instructions
The list of instructions in the goto program.
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
static eomt eom
Definition message.h:297
The symbol table base class interface.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.
Definition symbol.h:28
loop_mapt loop_map
Definition unwindset.h:61
void parse_unwindset_one_loop(std::string loop_limit, message_handlert &message_handler)
Definition unwindset.cpp:29
void parse_unwind(const std::string &unwind)
Definition unwindset.cpp:23
optionalt< unsigned > global_limit
Definition unwindset.h:56
thread_loop_mapt thread_loop_map
Definition unwindset.h:66
void parse_unwindset_file(const std::string &file_name, message_handlert &message_handler)
abstract_goto_modelt & goto_model
Definition unwindset.h:54
optionalt< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
void parse_unwindset(const std::list< std::string > &unwindset, message_handlert &message_handler)
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...
unsigned unsafe_string2unsigned(const std::string &str, int base)
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Definition kdev_t.h:19
Author: Diffblue Ltd.
#define widen_if_needed(s)
Definition unicode.h:28
Loop unwinding.