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