CBMC
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 
14 #include <util/expr_iterator.h>
15 #include <util/simplify_expr.h>
16 #include <util/std_expr.h>
17 
18 class ssa_exprt;
19 
21 enum levelt
22 {
23  L0 = 0,
24  L1 = 1,
26  L2 = 3
27 };
28 
31 template <typename underlyingt, levelt level>
32 class renamedt : private underlyingt
33 {
34 public:
35  static_assert(
36  std::is_base_of<exprt, underlyingt>::value ||
37  std::is_base_of<typet, underlyingt>::value,
38  "underlyingt should inherit from exprt or typet");
39 
40  const underlyingt &get() const
41  {
42  return static_cast<const underlyingt &>(*this);
43  }
44 
45  void simplify(const namespacet &ns)
46  {
47  (void)::simplify(value(), ns);
48  }
49 
51  std::function<std::optional<renamedt>(const renamedt &)>;
52 
53 private:
54  underlyingt &value()
55  {
56  return static_cast<underlyingt &>(*this);
57  };
58 
60  symex_level0(ssa_exprt, const namespacet &, std::size_t);
61  friend struct symex_level1t;
62  friend struct symex_level2t;
63  friend class goto_symex_statet;
64 
65  template <levelt make_renamed_level>
67  make_renamed(constant_exprt constant);
68 
69  template <levelt selectively_mutate_level>
70  friend void selectively_mutate(
73  get_mutated_expr);
74 
76  explicit renamedt(underlyingt value) : underlyingt(std::move(value))
77  {
78  }
79 };
80 
81 template <levelt level>
83 {
84  return renamedt<exprt, level>(std::move(constant));
85 }
86 
94 template <levelt level>
96  renamedt<exprt, level> &renamed,
97  typename renamedt<exprt, level>::mutator_functiont get_mutated_expr)
98 {
99  for(auto it = renamed.depth_begin(), itend = renamed.depth_end(); it != itend;
100  ++it)
101  {
102  std::optional<renamedt<exprt, level>> replacement =
103  get_mutated_expr(static_cast<const renamedt<exprt, level> &>(*it));
104 
105  if(replacement)
106  it.mutate() = std::move(replacement->value());
107  }
108 }
109 
110 #endif // CPROVER_GOTO_SYMEX_RENAMED_H
A constant literal expression.
Definition: std_expr.h:2995
Central data structure: state.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:33
const underlyingt & get() const
Definition: renamed.h:40
renamedt(underlyingt value)
Only the friend classes can create renamedt objects.
Definition: renamed.h:76
friend renamedt< exprt, make_renamed_level > make_renamed(constant_exprt constant)
Definition: renamed.h:82
void simplify(const namespacet &ns)
Definition: renamed.h:45
underlyingt & value()
Definition: renamed.h:54
std::function< std::optional< renamedt >(const renamedt &)> mutator_functiont
Definition: renamed.h:51
friend renamedt< ssa_exprt, L0 > symex_level0(ssa_exprt, const namespacet &, std::size_t)
Set the level 0 renaming of SSA expressions.
friend void selectively_mutate(renamedt< exprt, selectively_mutate_level > &renamed, typename renamedt< exprt, selectively_mutate_level >::mutator_functiont get_mutated_expr)
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
Forward depth-first search iterators These iterators' copy operations are expensive,...
renamedt< exprt, level > make_renamed(constant_exprt constant)
Definition: renamed.h:82
levelt
Symex renaming level names.
Definition: renamed.h:22
@ L2
Definition: renamed.h:26
@ L0
Definition: renamed.h:23
@ L1_WITH_CONSTANT_PROPAGATION
Definition: renamed.h:25
@ L1
Definition: renamed.h:24
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:95
API to expression classes.
Functor to set the level 1 renaming of SSA expressions.
Functor to set the level 2 renaming of SSA expressions.