cprover
renaming_level.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Romain Brenguier, romain.brenguier@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_SYMEX_RENAMING_LEVEL_H
13 #define CPROVER_GOTO_SYMEX_RENAMING_LEVEL_H
14 
15 #include <map>
16 #include <unordered_set>
17 
18 #include <util/irep.h>
19 #include <util/ssa_expr.h>
20 
26 {
27  virtual ~symex_renaming_levelt() = default;
28 
30  typedef std::map<irep_idt, std::pair<ssa_exprt, unsigned>> current_namest;
32 
34  unsigned current_count(const irep_idt &identifier) const
35  {
36  const auto it = current_names.find(identifier);
37  return it == current_names.end() ? 0 : it->second.second;
38  }
39 
41  static void increase_counter(const current_namest::iterator &it)
42  {
43  ++it->second.second;
44  }
45 
47  void get_variables(std::unordered_set<ssa_exprt, irep_hash> &vars) const
48  {
49  for(const auto &pair : current_names)
50  vars.insert(pair.second.first);
51  }
52 };
53 
58 {
59  void
60  operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr);
61 
62  symex_level0t() = default;
63  ~symex_level0t() override = default;
64 };
65 
70 {
71  void operator()(ssa_exprt &ssa_expr);
72 
74  void restore_from(const current_namest &other);
75 
76  symex_level1t() = default;
77  ~symex_level1t() override = default;
78 };
79 
84 {
85  symex_level2t() = default;
86  ~symex_level2t() override = default;
87 };
88 
89 #endif // CPROVER_GOTO_SYMEX_RENAMING_LEVEL_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
symex_level1t::~symex_level1t
~symex_level1t() override=default
symex_level1t::operator()
void operator()(ssa_exprt &ssa_expr)
Definition: renaming_level.cpp:43
symex_renaming_levelt::get_variables
void get_variables(std::unordered_set< ssa_exprt, irep_hash > &vars) const
Add the ssa_exprt of current_names to vars.
Definition: renaming_level.h:47
symex_renaming_levelt::current_namest
std::map< irep_idt, std::pair< ssa_exprt, unsigned > > current_namest
Map identifier to ssa_exprt and counter.
Definition: renaming_level.h:30
symex_level0t::symex_level0t
symex_level0t()=default
symex_level0t::~symex_level0t
~symex_level0t() override=default
symex_renaming_levelt::increase_counter
static void increase_counter(const current_namest::iterator &it)
Increase the counter corresponding to an identifier.
Definition: renaming_level.h:41
symex_level1t::symex_level1t
symex_level1t()=default
symex_level2t::symex_level2t
symex_level2t()=default
symex_renaming_levelt::current_count
unsigned current_count(const irep_idt &identifier) const
Counter corresponding to an identifier.
Definition: renaming_level.h:34
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
symex_level2t
Functor to set the level 2 renaming of SSA expressions.
Definition: renaming_level.h:83
symex_level2t::~symex_level2t
~symex_level2t() override=default
symex_renaming_levelt::~symex_renaming_levelt
virtual ~symex_renaming_levelt()=default
symex_level0t::operator()
void operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
Definition: renaming_level.cpp:19
ssa_expr.h
symex_renaming_levelt
Wrapper for a current_names map, which maps each identifier to an SSA expression and a counter.
Definition: renaming_level.h:25
symex_level0t
Functor to set the level 0 renaming of SSA expressions.
Definition: renaming_level.h:57
symex_level1t::restore_from
void restore_from(const current_namest &other)
Insert the content of other into this renaming.
Definition: renaming_level.cpp:59
symex_level1t
Functor to set the level 1 renaming of SSA expressions.
Definition: renaming_level.h:69
symex_renaming_levelt::current_names
current_namest current_names
Definition: renaming_level.h:31
irep.h