CBMC
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
18#include "abstract_goto_model.h"
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 abstract_goto_modelt &goto_model,
32 message_handlert &message_handler)
33{
34 if(val.empty())
35 return;
36
37 std::optional<unsigned> thread_nr;
38 if(isdigit(val[0]))
39 {
40 auto c_pos = val.find(':');
41 if(c_pos != std::string::npos)
42 {
43 std::string nr = val.substr(0, c_pos);
44 thread_nr = unsafe_string2unsigned(nr);
45 val.erase(0, nr.size() + 1);
46 }
47 }
48
49 auto last_c_pos = val.rfind(':');
50 if(last_c_pos != std::string::npos)
51 {
52 std::string id = val.substr(0, last_c_pos);
53
54 // The loop id can take three forms:
55 // 1) Just a function name to limit recursion.
56 // 2) F.N where F is a function name and N is a loop number.
57 // 3) F.L where F is a function name and L is a label.
58 const symbol_table_baset &symbol_table = goto_model.get_symbol_table();
59 const symbolt *maybe_fn = symbol_table.lookup(id);
60 if(maybe_fn && maybe_fn->type.id() == ID_code)
61 {
62 // ok, recursion limit
63 }
64 else
65 {
66 auto last_dot_pos = val.rfind('.');
67 if(last_dot_pos == std::string::npos)
68 {
70 "invalid loop identifier " + id, "unwindset"};
71 }
72
73 std::string function_id = id.substr(0, last_dot_pos);
74 std::string loop_nr_label = id.substr(last_dot_pos + 1);
75
76 if(loop_nr_label.empty())
77 {
79 "invalid loop identifier " + id, "unwindset"};
80 }
81
82 if(!goto_model.can_produce_function(function_id))
83 {
84 messaget log{message_handler};
85 log.warning() << "loop identifier " << id
86 << " for non-existent function provided with unwindset"
88 return;
89 }
90
91 const goto_functiont &goto_function =
92 goto_model.get_goto_function(function_id);
94 {
96 if(!nr.has_value())
97 {
99 "invalid loop identifier " + id, "unwindset"};
100 }
101
102 bool found = std::any_of(
103 goto_function.body.instructions.begin(),
104 goto_function.body.instructions.end(),
105 [&nr](const goto_programt::instructiont &instruction) {
106 return instruction.is_backwards_goto() &&
107 instruction.loop_number == nr;
108 });
109 if(!found)
110 {
111 messaget log{message_handler};
112 log.warning() << "loop identifier " << id
113 << " provided with unwindset does not match any loop"
114 << messaget::eom;
115 return;
116 }
117 }
118 else
119 {
120 std::optional<unsigned> nr;
121 std::optional<source_locationt> location;
122 for(const auto &instruction : goto_function.body.instructions)
123 {
124 if(
125 std::find(
126 instruction.labels.begin(),
127 instruction.labels.end(),
128 loop_nr_label) != instruction.labels.end())
129 {
130 location = instruction.source_location();
131 // the label may be attached to the DECL part of an initializing
132 // declaration, which we may have marked as hidden
133 location->remove(ID_hide);
134 }
135 if(
136 location.has_value() && instruction.is_backwards_goto() &&
137 instruction.source_location() == *location)
138 {
139 if(nr.has_value())
140 {
141 messaget log{message_handler};
142 log.warning()
143 << "loop identifier " << id
144 << " provided with unwindset is ambiguous" << messaget::eom;
145 }
146 nr = instruction.loop_number;
147 }
148 }
149 if(!nr.has_value())
150 {
151 messaget log{message_handler};
152 log.warning() << "loop identifier " << id
153 << " provided with unwindset does not match any loop"
154 << messaget::eom;
155 return;
156 }
157 else
158 id = function_id + "." + std::to_string(*nr);
159 }
160 }
161
162 std::string uw_string = val.substr(last_c_pos + 1);
163
164 // the below initialisation makes g++-5 happy
165 std::optional<unsigned> uw(0);
166
167 if(uw_string.empty())
168 uw = {};
169 else
171
172 if(thread_nr.has_value())
173 {
174 thread_loop_map[std::pair<irep_idt, unsigned>(id, *thread_nr)] = uw;
175 }
176 else
177 {
178 loop_map[id] = uw;
179 }
180 }
181}
182
184 const std::list<std::string> &unwindset,
185 abstract_goto_modelt &goto_model,
186 message_handlert &message_handler)
187{
188 for(auto &element : unwindset)
189 parse_unwindset_one_loop(element, goto_model, message_handler);
190}
191
192std::optional<unsigned>
193unwindsett::get_limit(const irep_idt &loop_id, unsigned thread_nr) const
194{
195 // We use the most specific limit we have
196
197 // thread x loop
198 auto tl_it =
199 thread_loop_map.find(std::pair<irep_idt, unsigned>(loop_id, thread_nr));
200
201 if(tl_it != thread_loop_map.end())
202 return tl_it->second;
203
204 // loop
205 auto l_it = loop_map.find(loop_id);
206
207 if(l_it != loop_map.end())
208 return l_it->second;
209
210 // global, if any
211 return global_limit;
212}
213
215 const std::string &file_name,
216 abstract_goto_modelt &goto_model,
217 message_handlert &message_handler)
218{
219 std::ifstream file(widen_if_needed(file_name));
220
221 if(!file)
222 throw "cannot open file " + file_name;
223
224 std::stringstream buffer;
225 buffer << file.rdbuf();
226
227 std::vector<std::string> unwindset_elements =
228 split_string(buffer.str(), ',', true, true);
229
230 for(auto &element : unwindset_elements)
231 parse_unwindset_one_loop(element, goto_model, message_handler);
232}
Abstract interface to eager or lazy GOTO models.
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:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
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:154
static eomt eom
Definition message.h:289
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:60
std::optional< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
void parse_unwindset_one_loop(std::string loop_limit, abstract_goto_modelt &goto_model, message_handlert &message_handler)
Definition unwindset.cpp:29
void parse_unwind(const std::string &unwind)
Definition unwindset.cpp:23
void parse_unwindset(const std::list< std::string > &unwindset, abstract_goto_modelt &goto_model, message_handlert &message_handler)
void parse_unwindset_file(const std::string &file_name, abstract_goto_modelt &goto_model, message_handlert &message_handler)
std::optional< unsigned > global_limit
Definition unwindset.h:55
thread_loop_mapt thread_loop_map
Definition unwindset.h:65
int isdigit(int c)
Definition ctype.c:24
double log(double x)
Definition math.c:2449
unsigned unsafe_string2unsigned(const std::string &str, int base)
std::optional< 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...
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Author: Diffblue Ltd.
#define widen_if_needed(s)
Definition unicode.h:28
Loop unwinding.