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 
41 symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr);
42 
47 {
49  void insert(const renamedt<ssa_exprt, L0> &ssa, std::size_t index);
50 
55  insert_or_replace(const renamedt<ssa_exprt, L0> &ssa, std::size_t index);
56 
58  bool has(const renamedt<ssa_exprt, L0> &ssa) const;
59 
64 
66  void restore_from(const symex_level1t &other);
67 
68 private:
70 };
71 
76 {
78 
82 
84  unsigned latest_index(const irep_idt &identifier) const;
85 
88  std::size_t increase_generation(
89  const irep_idt &l1_identifier,
90  const ssa_exprt &lhs,
91  std::function<std::size_t(const irep_idt &)> fresh_l2_name_provider);
92 };
93 
96 
99 
102 bool check_renaming(const exprt &expr);
103 
106 bool check_renaming_l1(const exprt &expr);
107 
110 bool check_renaming(const typet &type);
111 
112 #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:37
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:21
symex_level1t::restore_from
void restore_from(const symex_level1t &other)
Insert the content of other into this renaming.
Definition: renaming_level.cpp:108
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:100
sharing_mapt< irep_idt, std::pair< ssa_exprt, std::size_t > >
typet
The type of an expression, extends irept.
Definition: type.h:28
exprt
Base class for all expressions.
Definition: expr.h:54
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:135
renamed.h
Class for expressions or types renamed up to a given level.
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:76
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:237
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:212
get_original_name
exprt get_original_name(exprt expr)
Undo all levels of renaming.
Definition: renaming_level.cpp:156
symex_level1t::current_names
symex_renaming_levelt current_names
Definition: renaming_level.h:69
symex_level1t::insert
void insert(const renamedt< ssa_exprt, L0 > &ssa, std::size_t index)
Assume ssa is not already known.
Definition: renaming_level.cpp:46
range.h
Ranges: pair of begin and end iterators, which can be initialized from containers,...
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
simplify_expr.h
ssa_expr.h
expr_iterator.h
Forward depth-first search iterators These iterators' copy operations are expensive,...
symex_level2t::current_names
symex_renaming_levelt current_names
Definition: renaming_level.h:77
symex_level1t
Functor to set the level 1 renaming of SSA expressions.
Definition: renaming_level.h:47
symex_level1t::has
bool has(const renamedt< ssa_exprt, L0 > &ssa) const
Definition: renaming_level.cpp:70
symex_level1t::operator()
renamedt< ssa_exprt, L1 > operator()(renamedt< ssa_exprt, L0 > l0_expr) const
Definition: renaming_level.cpp:76
symex_level2t::latest_index
unsigned latest_index(const irep_idt &identifier) const
Counter corresponding to an identifier.
Definition: renaming_level.cpp:129
sharing_map.h
Sharing map.
renamedt
Wrapper for expressions or types which have been renamed up to a given level.
Definition: renamed.h:27
symex_level1t::insert_or_replace
optionalt< std::pair< ssa_exprt, std::size_t > > insert_or_replace(const renamedt< ssa_exprt, L0 > &ssa, std::size_t index)
Set the index for ssa to index.
Definition: renaming_level.cpp:54
irep.h