cprover
renamed.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 \*******************************************************************/
10 
11 #ifndef CPROVER_GOTO_SYMEX_RENAMED_H
12 #define CPROVER_GOTO_SYMEX_RENAMED_H
13 
15 enum levelt
16 {
17  L0 = 0,
18  L1 = 1,
20  L2 = 3
21 };
22 
25 template <typename underlyingt, levelt level>
26 class renamedt : private underlyingt
27 {
28 public:
29  static_assert(
30  std::is_base_of<exprt, underlyingt>::value ||
31  std::is_base_of<typet, underlyingt>::value,
32  "underlyingt should inherit from exprt or typet");
33 
34  const underlyingt &get() const
35  {
36  return static_cast<const underlyingt &>(*this);
37  }
38 
39  void simplify(const namespacet &ns)
40  {
41  (void)::simplify(value(), ns);
42  }
43 
45  std::function<optionalt<renamedt>(const renamedt &)>;
46 
47 private:
48  underlyingt &value()
49  {
50  return static_cast<underlyingt &>(*this);
51  };
52 
54  symex_level0(ssa_exprt, const namespacet &, std::size_t);
55  friend struct symex_level1t;
56  friend struct symex_level2t;
57  friend class goto_symex_statet;
58 
59  template <levelt make_renamed_level>
61  make_renamed(constant_exprt constant);
62 
63  template <levelt selectively_mutate_level>
64  friend void selectively_mutate(
67  get_mutated_expr);
68 
70  explicit renamedt(underlyingt value) : underlyingt(std::move(value))
71  {
72  }
73 };
74 
75 template <levelt level>
77 {
78  return renamedt<exprt, level>(std::move(constant));
79 }
80 
88 template <levelt level>
90  renamedt<exprt, level> &renamed,
91  typename renamedt<exprt, level>::mutator_functiont get_mutated_expr)
92 {
93  for(auto it = renamed.depth_begin(), itend = renamed.depth_end(); it != itend;
94  ++it)
95  {
97  get_mutated_expr(static_cast<const renamedt<exprt, level> &>(*it));
98 
99  if(replacement)
100  it.mutate() = std::move(replacement->value());
101  }
102 }
103 
104 #endif // CPROVER_GOTO_SYMEX_RENAMED_H
L2
@ L2
Definition: renamed.h:20
renamedt::renamedt
renamedt(underlyingt value)
Only the friend classes can create renamedt objects.
Definition: renamed.h:70
L1
@ L1
Definition: renamed.h:18
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:46
renamedt::simplify
void simplify(const namespacet &ns)
Definition: renamed.h:39
renamedt::get
const underlyingt & get() const
Definition: renamed.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:92
symex_level2t
Functor to set the level 2 renaming of SSA expressions.
Definition: renaming_level.h:82
L0
@ L0
Definition: renamed.h:17
renamedt::symex_level0
friend renamedt< ssa_exprt, L0 > symex_level0(ssa_exprt, const namespacet &, std::size_t)
Set the level 0 renaming of SSA expressions.
Definition: renaming_level.cpp:34
renamedt::selectively_mutate
friend void selectively_mutate(renamedt< exprt, selectively_mutate_level > &renamed, typename renamedt< exprt, selectively_mutate_level >::mutator_functiont get_mutated_expr)
selectively_mutate
void selectively_mutate(renamedt< exprt, level > &renamed, typename renamedt< exprt, level >::mutator_functiont get_mutated_expr)
This permits replacing subexpressions of the renamed value, so long as each replacement is consistent...
Definition: renamed.h:89
L1_WITH_CONSTANT_PROPAGATION
@ L1_WITH_CONSTANT_PROPAGATION
Definition: renamed.h:19
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
renamedt::make_renamed
friend renamedt< exprt, make_renamed_level > make_renamed(constant_exprt constant)
Definition: renamed.h:76
levelt
levelt
Symex renaming level names.
Definition: renamed.h:16
symex_level1t
Functor to set the level 1 renaming of SSA expressions.
Definition: renaming_level.h:53
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
renamedt::value
underlyingt & value()
Definition: renamed.h:48
renamedt
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:27
renamedt::mutator_functiont
std::function< optionalt< renamedt >(const renamedt &)> mutator_functiont
Definition: renamed.h:45
make_renamed
renamedt< exprt, level > make_renamed(constant_exprt constant)
Definition: renamed.h:76