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