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