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
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...
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 ...
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.
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)
abstract_goto_modelt & goto_model
Definition unwindset.h:52
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)
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...
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
std::wstring widen(const char *s)
Definition unicode.cpp:49
Loop unwinding.