cprover
replace_symbol.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_REPLACE_SYMBOL_H
11 #define CPROVER_UTIL_REPLACE_SYMBOL_H
12 
13 //
14 // true: did nothing
15 // false: replaced something
16 //
17 
18 #include "expr.h"
19 
20 #include <unordered_map>
21 
25 {
26 public:
27  typedef std::unordered_map<irep_idt, exprt> expr_mapt;
28 
32  void insert(const class symbol_exprt &old_expr,
33  const exprt &new_expr);
34 
36  void set(const class symbol_exprt &old_expr, const exprt &new_expr);
37 
38  virtual bool replace(exprt &dest) const;
39  virtual bool replace(typet &dest) const;
40 
41  void operator()(exprt &dest) const
42  {
43  replace(dest);
44  }
45 
46  void operator()(typet &dest) const
47  {
48  replace(dest);
49  }
50 
51  void clear()
52  {
53  expr_map.clear();
54  }
55 
56  bool empty() const
57  {
58  return expr_map.empty();
59  }
60 
61  std::size_t erase(const irep_idt &id)
62  {
63  return expr_map.erase(id);
64  }
65 
66  expr_mapt::iterator erase(expr_mapt::iterator it)
67  {
68  return expr_map.erase(it);
69  }
70 
71  bool replaces_symbol(const irep_idt &id) const
72  {
73  return expr_map.find(id) != expr_map.end();
74  }
75 
77  virtual ~replace_symbolt();
78 
79  const expr_mapt &get_expr_map() const
80  {
81  return expr_map;
82  }
83 
85  {
86  return expr_map;
87  }
88 
89 protected:
91 
92  virtual bool replace_symbol_expr(symbol_exprt &dest) const;
93 
94  bool have_to_replace(const exprt &dest) const;
95  bool have_to_replace(const typet &type) const;
96 };
97 
99 {
100 public:
102  {
103  }
104 
105  void insert(const symbol_exprt &old_expr, const exprt &new_expr);
106 
107 protected:
108  bool replace_symbol_expr(symbol_exprt &dest) const override;
109 };
110 
120 {
121 public:
122  bool replace(exprt &dest) const override;
123 
124 private:
125  mutable bool require_lvalue = false;
126 
128  {
129  public:
132  {
133  require_lvalue = value;
134  }
135 
137  {
139  }
140 
141  private:
144  };
145 
146  bool replace_symbol_expr(symbol_exprt &dest) const override;
147 };
148 
149 #endif // CPROVER_UTIL_REPLACE_SYMBOL_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
address_of_aware_replace_symbolt
Replace symbols with constants while maintaining syntactically valid expressions.
Definition: replace_symbol.h:120
replace_symbolt::~replace_symbolt
virtual ~replace_symbolt()
Definition: replace_symbol.cpp:20
replace_symbolt::have_to_replace
bool have_to_replace(const exprt &dest) const
Definition: replace_symbol.cpp:124
replace_symbolt::replaces_symbol
bool replaces_symbol(const irep_idt &id) const
Definition: replace_symbol.h:71
address_of_aware_replace_symbolt::set_require_lvalue_and_backupt::require_lvalue
bool & require_lvalue
Definition: replace_symbol.h:142
address_of_aware_replace_symbolt::set_require_lvalue_and_backupt::~set_require_lvalue_and_backupt
~set_require_lvalue_and_backupt()
Definition: replace_symbol.h:136
typet
The type of an expression, extends irept.
Definition: type.h:29
replace_symbolt::replace_symbolt
replace_symbolt()
Definition: replace_symbol.cpp:16
replace_symbolt::erase
expr_mapt::iterator erase(expr_mapt::iterator it)
Definition: replace_symbol.h:66
replace_symbolt::expr_mapt
std::unordered_map< irep_idt, exprt > expr_mapt
Definition: replace_symbol.h:27
replace_symbolt::get_expr_map
const expr_mapt & get_expr_map() const
Definition: replace_symbol.h:79
exprt
Base class for all expressions.
Definition: expr.h:53
replace_symbolt::expr_map
expr_mapt expr_map
Definition: replace_symbol.h:90
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
replace_symbolt::get_expr_map
expr_mapt & get_expr_map()
Definition: replace_symbol.h:84
address_of_aware_replace_symbolt::set_require_lvalue_and_backupt::set_require_lvalue_and_backupt
set_require_lvalue_and_backupt(bool &require_lvalue, const bool value)
Definition: replace_symbol.h:130
expr.h
replace_symbolt::replace_symbol_expr
virtual bool replace_symbol_expr(symbol_exprt &dest) const
Definition: replace_symbol.cpp:43
replace_symbolt::operator()
void operator()(typet &dest) const
Definition: replace_symbol.h:46
replace_symbolt::clear
void clear()
Definition: replace_symbol.h:51
address_of_aware_replace_symbolt::replace
bool replace(exprt &dest) const override
Definition: replace_symbol.cpp:263
replace_symbolt::operator()
void operator()(exprt &dest) const
Definition: replace_symbol.h:41
unchecked_replace_symbolt::unchecked_replace_symbolt
unchecked_replace_symbolt()
Definition: replace_symbol.h:101
replace_symbolt::replace
virtual bool replace(exprt &dest) const
Definition: replace_symbol.cpp:59
replace_symbolt::empty
bool empty() const
Definition: replace_symbol.h:56
replace_symbolt::insert
void insert(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr if we don't already have a replacement; otherwise does nothi...
Definition: replace_symbol.cpp:24
address_of_aware_replace_symbolt::require_lvalue
bool require_lvalue
Definition: replace_symbol.h:125
unchecked_replace_symbolt::insert
void insert(const symbol_exprt &old_expr, const exprt &new_expr)
Definition: replace_symbol.cpp:244
replace_symbolt::erase
std::size_t erase(const irep_idt &id)
Definition: replace_symbol.h:61
unchecked_replace_symbolt
Definition: replace_symbol.h:99
address_of_aware_replace_symbolt::replace_symbol_expr
bool replace_symbol_expr(symbol_exprt &dest) const override
Definition: replace_symbol.cpp:327
address_of_aware_replace_symbolt::set_require_lvalue_and_backupt::prev_value
bool prev_value
Definition: replace_symbol.h:143
address_of_aware_replace_symbolt::set_require_lvalue_and_backupt
Definition: replace_symbol.h:128
unchecked_replace_symbolt::replace_symbol_expr
bool replace_symbol_expr(symbol_exprt &dest) const override
Definition: replace_symbol.cpp:251
replace_symbolt::set
void set(const class symbol_exprt &old_expr, const exprt &new_expr)
Sets old_expr to be replaced by new_expr.
Definition: replace_symbol.cpp:36
replace_symbolt
Replace expression or type symbols by an expression or type, respectively.
Definition: replace_symbol.h:25