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/string2int.h>
12 #include <util/string_utils.h>
13 #include <util/unicode.h>
14 
15 #include <fstream>
16 #include <sstream>
17 
18 void unwindsett::parse_unwind(const std::string &unwind)
19 {
20  if(!unwind.empty())
22 }
23 
24 void unwindsett::parse_unwindset(const std::string &unwindset)
25 {
26  std::vector<std::string> unwindset_loops;
27  split_string(unwindset, ',', unwindset_loops, true, true);
28 
29  for(auto &val : unwindset_loops)
30  {
31  unsigned thread_nr = 0;
32  bool thread_nr_set = false;
33 
34  if(!val.empty() && isdigit(val[0]) && val.find(":") != std::string::npos)
35  {
36  std::string nr = val.substr(0, val.find(":"));
37  thread_nr = unsafe_string2unsigned(nr);
38  thread_nr_set = true;
39  val.erase(0, nr.size() + 1);
40  }
41 
42  if(val.rfind(":") != std::string::npos)
43  {
44  std::string id = val.substr(0, val.rfind(":"));
45  std::string uw_string = val.substr(val.rfind(":") + 1);
46 
47  // the below initialisation makes g++-5 happy
48  optionalt<unsigned> uw(0);
49 
50  if(uw_string.empty())
51  uw = { };
52  else
53  uw = unsafe_string2unsigned(uw_string);
54 
55  if(thread_nr_set)
56  thread_loop_map[std::pair<irep_idt, unsigned>(id, thread_nr)] = uw;
57  else
58  loop_map[id] = uw;
59  }
60  }
61 }
62 
64 unwindsett::get_limit(const irep_idt &loop_id, unsigned thread_nr) const
65 {
66  // We use the most specific limit we have
67 
68  // thread x loop
69  auto tl_it =
70  thread_loop_map.find(std::pair<irep_idt, unsigned>(loop_id, thread_nr));
71 
72  if(tl_it != thread_loop_map.end())
73  return tl_it->second;
74 
75  // loop
76  auto l_it = loop_map.find(loop_id);
77 
78  if(l_it != loop_map.end())
79  return l_it->second;
80 
81  // global, if any
82  return global_limit;
83 }
84 
85 void unwindsett::parse_unwindset_file(const std::string &file_name)
86 {
87  #ifdef _MSC_VER
88  std::ifstream file(widen(file_name));
89  #else
90  std::ifstream file(file_name);
91  #endif
92 
93  if(!file)
94  throw "cannot open file "+file_name;
95 
96  std::stringstream buffer;
97  buffer << file.rdbuf();
98  parse_unwindset(buffer.str());
99 }
std::wstring widen(const char *s)
Definition: unicode.cpp:46
loop_mapt loop_map
Definition: unwindset.h:48
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:69
nonstd::optional< T > optionalt
Definition: optional.h:35
optionalt< unsigned > global_limit
Definition: unwindset.h:43
void parse_unwindset_file(const std::string &file_name)
Definition: unwindset.cpp:85
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Loop unwinding.
void parse_unwindset(const std::string &unwindset)
Definition: unwindset.cpp:24
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Given a string s, split into a sequence of substrings when separated by specified delimiter...
thread_loop_mapt thread_loop_map
Definition: unwindset.h:53
void parse_unwind(const std::string &unwind)
Definition: unwindset.cpp:18
optionalt< unsigned > get_limit(const irep_idt &loop, unsigned thread_id) const
Definition: unwindset.cpp:64
Definition: kdev_t.h:19