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/expr_iterator.h>
19 #include <util/irep.h>
20 #include <util/range.h>
21 #include <util/sharing_map.h>
22 #include <util/simplify_expr.h>
23 #include <util/ssa_expr.h>
24 
25 #include "renamed.h"
26 
33 
35 DEPRECATED(SINCE(2019, 6, 5, "Unused"))
36 void get_variables(
37  const symex_renaming_levelt &current_names,
38  std::unordered_set<ssa_exprt, irep_hash> &vars);
39 
47 symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr);
48 
53 {
55  void insert(const renamedt<ssa_exprt, L0> &ssa, std::size_t index);
56 
61  insert_or_replace(const renamedt<ssa_exprt, L0> &ssa, std::size_t index);
62 
64  bool has(const renamedt<ssa_exprt, L0> &ssa) const;
65 
69  renamedt<ssa_exprt, L1> operator()(renamedt<ssa_exprt, L0> l0_expr) const;
70 
72  void restore_from(const symex_level1t &other);
73 
74 private:
76 };
77 
82 {
84 
88 
90  unsigned latest_index(const irep_idt &identifier) const;
91 
94  std::size_t increase_generation(
95  const irep_idt &l1_identifier,
96  const ssa_exprt &lhs,
97  std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider);
98 };
99 
102 
105 
108 bool check_renaming(const exprt &expr);
109 
112 bool check_renaming_l1(const exprt &expr);
113 
116 bool check_renaming(const typet &type);
117 
118 #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:36
symex_level0
renamedt< ssa_exprt, L0 > symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr)
Set the level 0 renaming of SSA expressions.
Definition: renaming_level.cpp:34
symex_level2t::operator()
renamedt< ssa_exprt, L2 > operator()(renamedt< ssa_exprt, L1 > l1_expr) const
Set L2 tag to correspond to the current count of the identifier of l1_expr's.
Definition: renaming_level.cpp:113
sharing_mapt
A map implemented as a tree where subtrees can be shared between different maps.
Definition: sharing_map.h:179
typet
The type of an expression, extends irept.
Definition: type.h:28
get_variables
void get_variables(const symex_renaming_levelt &current_names, std::unordered_set< ssa_exprt, irep_hash > &vars)
Add the ssa_exprt of current_names to vars.
exprt
Base class for all expressions.
Definition: expr.h:52
symex_level2t::increase_generation
std::size_t increase_generation(const irep_idt &l1_identifier, const ssa_exprt &lhs, std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider)
Allocates a fresh L2 name for the given L1 identifier, and makes it the latest generation on this pat...
Definition: renaming_level.cpp:148
renamed.h
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:16
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
symex_level2t
Functor to set the level 2 renaming of SSA expressions.
Definition: renaming_level.h:81
check_renaming
bool check_renaming(const exprt &expr)
Check that expr is correctly renamed to level 2 and return true in case an error is detected.
Definition: renaming_level.cpp:250
L0
Definition: renamed.h:17
check_renaming_l1
bool check_renaming_l1(const exprt &expr)
Check that expr is correctly renamed to level 1 and return true in case an error is detected.
Definition: renaming_level.cpp:225
get_original_name
exprt get_original_name(exprt expr)
Undo all levels of renaming.
Definition: renaming_level.cpp:169
symex_level1t::current_names
symex_renaming_levelt current_names
Definition: renaming_level.h:75
range.h
irep_hash
Definition: irep.h:497
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
simplify_expr.h
ssa_expr.h
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
expr_iterator.h
symex_level2t::current_names
symex_renaming_levelt current_names
Definition: renaming_level.h:83
symex_level1t
Functor to set the level 1 renaming of SSA expressions.
Definition: renaming_level.h:52
symex_level2t::latest_index
unsigned latest_index(const irep_idt &identifier) const
Counter corresponding to an identifier.
Definition: renaming_level.cpp:142
sharing_map.h
renamedt
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:26
irep.h