CBMC: /home/runner/work/cbmc/cbmc/src/goto-programs/unwindset.cpp Source File

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
11#include <util/exception_utils.h>
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
23 void 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>
193 unwindsett::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:566
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...
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:621
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition message.h:27
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
Definition unwindset.cpp:193
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)
Definition unwindset.cpp:183
void parse_unwindset_file(const std::string &file_name, abstract_goto_modelt &goto_model, message_handlert &message_handler)
Definition unwindset.cpp:214
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:2416
std::optional< unsigned > string2optional_unsigned(std::string_view 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
void split_string(std::string_view 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.

AltStyle によって変換されたページ (->オリジナル) /