CBMC
dirty.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Variables whose address is taken
4 
5 Author: Daniel Kroening
6 
7 Date: March 2013
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_ANALYSES_DIRTY_H
15 #define CPROVER_ANALYSES_DIRTY_H
16 
17 #include <util/invariant.h>
18 #include <util/std_expr.h>
19 
21 
22 #include <unordered_set>
23 
27 class dirtyt
28 {
29 private:
30  void die_if_uninitialized() const
31  {
32  INVARIANT(
34  "Uninitialized dirtyt. This dirtyt was constructed using the default "
35  "constructor and not subsequently initialized using "
36  "dirtyt::build().");
37  }
38 
39 public:
42 
47  dirtyt() : initialized(false)
48  {
49  }
50 
51  explicit dirtyt(const goto_functiont &goto_function) : initialized(false)
52  {
53  build(goto_function);
54  initialized = true;
55  }
56 
57  explicit dirtyt(const goto_functionst &goto_functions) : initialized(false)
58  {
59  build(goto_functions);
60  // build(g_funs) responsible for setting initialized to true, since
61  // it is public and can be called independently
62  }
63 
64  void output(std::ostream &out) const;
65 
66  bool operator()(const irep_idt &id) const
67  {
69  return dirty.find(id) != dirty.end();
70  }
71 
72  bool operator()(const symbol_exprt &expr) const
73  {
75  return operator()(expr.get_identifier());
76  }
77 
78  const std::unordered_set<irep_idt> &get_dirty_ids() const
79  {
81  return dirty;
82  }
83 
84  void add_function(const goto_functiont &goto_function)
85  {
86  build(goto_function);
87  initialized = true;
88  }
89 
90  void build(const goto_functionst &goto_functions)
91  {
92  // dirtyts should not be initialized twice
94  for(const auto &gf_entry : goto_functions.function_map)
95  build(gf_entry.second);
96  initialized = true;
97  }
98 
99 protected:
100  void build(const goto_functiont &goto_function);
101 
102  // variables whose address is taken
103  std::unordered_set<irep_idt> dirty;
104  void search_other(const goto_programt::instructiont &instruction);
105  void find_dirty(const exprt &expr);
106  void find_dirty_address_of(const exprt &expr);
107 };
108 
109 inline std::ostream &operator<<(std::ostream &out, const dirtyt &dirty)
110 {
111  dirty.output(out);
112  return out;
113 }
114 
118 {
119 public:
121  const irep_idt &id,
122  const goto_functionst::goto_functiont &function);
123 
124  bool operator()(const irep_idt &id) const
125  {
126  return dirty(id);
127  }
128 
129  bool operator()(const symbol_exprt &expr) const
130  {
131  return dirty(expr);
132  }
133 
134 private:
136  std::unordered_set<irep_idt> dirty_processed_functions;
137 };
138 
139 #endif // CPROVER_ANALYSES_DIRTY_H
Dirty variables are ones which have their address taken so we can't reliably work out where they may ...
Definition: dirty.h:28
bool operator()(const symbol_exprt &expr) const
Definition: dirty.h:72
void add_function(const goto_functiont &goto_function)
Definition: dirty.h:84
void build(const goto_functionst &goto_functions)
Definition: dirty.h:90
void find_dirty(const exprt &expr)
Definition: dirty.cpp:60
bool operator()(const irep_idt &id) const
Definition: dirty.h:66
bool initialized
Definition: dirty.h:40
const std::unordered_set< irep_idt > & get_dirty_ids() const
Definition: dirty.h:78
void find_dirty_address_of(const exprt &expr)
Definition: dirty.cpp:73
void output(std::ostream &out) const
Definition: dirty.cpp:102
dirtyt(const goto_functionst &goto_functions)
Definition: dirty.h:57
std::unordered_set< irep_idt > dirty
Definition: dirty.h:103
dirtyt(const goto_functiont &goto_function)
Definition: dirty.h:51
dirtyt()
Definition: dirty.h:47
void search_other(const goto_programt::instructiont &instruction)
Definition: dirty.cpp:34
void die_if_uninitialized() const
Definition: dirty.h:30
goto_functionst::goto_functiont goto_functiont
Definition: dirty.h:41
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly on...
Definition: dirty.h:118
bool operator()(const symbol_exprt &expr) const
Definition: dirty.h:129
std::unordered_set< irep_idt > dirty_processed_functions
Definition: dirty.h:136
void populate_dirty_for_function(const irep_idt &id, const goto_functionst::goto_functiont &function)
Analyse the given function with dirtyt if it hasn't been seen before.
Definition: dirty.cpp:112
bool operator()(const irep_idt &id) const
Definition: dirty.h:124
dirtyt dirty
Definition: dirty.h:135
Expression to hold a symbol (variable)
Definition: std_expr.h:131
const irep_idt & get_identifier() const
Definition: std_expr.h:160
std::ostream & operator<<(std::ostream &out, const dirtyt &dirty)
Definition: dirty.h:109
Goto Programs with Functions.
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.