cprover
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 
16 #ifdef _MSC_VER
17 # include <util/unicode.h>
18 #endif
19 
20 #include <fstream>
21 
22 void 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"
85  << messaget::eom;
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
154  optionalt<unsigned> uw(0);
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 
183 unwindsett::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 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:37
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:598
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.
Definition: symbol_table.h:14
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)
Definition: unwindset.cpp:204
abstract_goto_modelt & goto_model
Definition: unwindset.h:52
optionalt< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
Definition: unwindset.cpp:183
void parse_unwindset(const std::list< std::string > &unwindset, message_handlert &message_handler)
Definition: unwindset.cpp:168
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...
Definition: string2int.cpp:64
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)
Definition: kdev_t.h:19
std::wstring widen(const char *s)
Definition: unicode.cpp:48
Loop unwinding.