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
static void increase_counter(const current_namest::iterator &it)
Increase the counter corresponding to an identifier.
symex_level0t()=default
void get_variables(std::unordered_set< ssa_exprt, irep_hash > &vars) const
Add the ssa_exprt of current_names to vars.
void operator()(ssa_exprt &ssa_expr)
unsigned current_count(const irep_idt &identifier) const
Counter corresponding to an identifier.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
Functor to set the level 2 renaming of SSA expressions.
current_namest current_names
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
~symex_level1t() override=default
void operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
~symex_level0t() override=default
virtual ~symex_renaming_levelt()=default
void restore_from(const current_namest &other)
Insert the content of other into this renaming.
std::map< irep_idt, std::pair< ssa_exprt, unsigned > > current_namest
Map identifier to ssa_exprt and counter.
symex_level2t()=default
Functor to set the level 0 renaming of SSA expressions.
Wrapper for a current_names map, which maps each identifier to an SSA expression and a counter.
~symex_level2t() override=default
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
symex_level1t()=default
Functor to set the level 1 renaming of SSA expressions.