cprover
Loading...
Searching...
No Matches
analyze_symbol.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbol Analyzer
4
5Author: Malte Mues <mail.mues@gmail.com>
6 Daniel Poetzl
7
8\*******************************************************************/
9
12
13#ifndef CPROVER_MEMORY_ANALYZER_ANALYZE_SYMBOL_H
14#define CPROVER_MEMORY_ANALYZER_ANALYZE_SYMBOL_H
15
16#include <map>
17#include <string>
18
19#include "gdb_api.h"
20
21#include <ansi-c/expr2c_class.h>
22
23#include <util/namespace.h>
24#include <util/symbol_table.h>
25
27
28class pointer_typet;
30
32class gdb_value_extractort
33{
34public:
35 gdb_value_extractort(
36 const symbol_table_baset &symbol_table,
37 const std::vector<std::string> &args);
38
43 void analyze_symbols(const std::list<std::string> &symbols);
44
47 std::string get_snapshot_as_c_code();
48
55 symbol_tablet get_snapshot_as_symbol_table();
56
57 using pointer_valuet = gdb_apit::pointer_valuet;
58 using memory_addresst = gdb_apit::memory_addresst;
59
60 void create_gdb_process()
61 {
62 gdb_api.create_gdb_process();
63 }
64 bool run_gdb_to_breakpoint(const std::string &breakpoint)
65 {
66 return gdb_api.run_gdb_to_breakpoint(breakpoint);
67 }
68 void run_gdb_from_core(const std::string &corefile)
69 {
70 gdb_api.run_gdb_from_core(corefile);
71 }
72
73private:
74 gdb_apit gdb_api;
75
78 symbol_tablet symbol_table;
79 const namespacet ns;
80 expr2ct c_converter;
81 allocate_objectst allocate_objects;
82
84 std::map<exprt, exprt> assignments;
85
88 std::map<exprt, memory_addresst> outstanding_assignments;
89
92 std::map<memory_addresst, exprt> values;
93
94 struct memory_scopet
95 {
96 private:
97 size_t begin_int;
98 mp_integer byte_size;
99 irep_idt name;
100
104 size_t address2size_t(const memory_addresst &point) const;
105
109 bool check_containment(const size_t &point_int) const
110 {
111 return point_int >= begin_int && (begin_int + byte_size) > point_int;
112 }
113
114 public:
115 memory_scopet(
116 const memory_addresst &begin,
117 const mp_integer &byte_size,
118 const irep_idt &name);
119
123 bool contains(const memory_addresst &point) const
124 {
125 return check_containment(address2size_t(point));
126 }
127
133 distance(const memory_addresst &point, mp_integer member_size) const;
134
137 irep_idt id() const
138 {
139 return name;
140 }
141
144 mp_integer size() const
145 {
146 return byte_size;
147 }
148 };
149
151 std::vector<memory_scopet> dynamically_allocated;
152
154 std::map<irep_idt, pointer_valuet> memory_map;
155
156 bool has_known_memory_location(const irep_idt &id) const
157 {
158 return memory_map.count(id) != 0;
159 }
160
164 std::vector<memory_scopet>::iterator find_dynamic_allocation(irep_idt name);
165
169 std::vector<memory_scopet>::iterator
170 find_dynamic_allocation(const memory_addresst &point);
171
175 mp_integer get_malloc_size(irep_idt name);
176
189 get_malloc_pointee(const memory_addresst &point, mp_integer member_size);
190
194 mp_integer get_type_size(const typet &type) const;
195
200 void analyze_symbol(const irep_idt &symbol_name);
201
206 void add_assignment(const exprt &lhs, const exprt &value);
207
214 exprt get_array_value(
215 const exprt &expr,
216 const exprt &array,
217 const source_locationt &location);
218
228 exprt get_expr_value(
229 const exprt &expr,
230 const exprt &zero_expr,
231 const source_locationt &location);
232
238 exprt get_struct_value(
239 const exprt &expr,
240 const exprt &zero_expr,
241 const source_locationt &location);
242
248 exprt get_union_value(
249 const exprt &expr,
250 const exprt &zero_expr,
251 const source_locationt &location);
252
260 exprt get_pointer_value(
261 const exprt &expr,
262 const exprt &zero_expr,
263 const source_locationt &location);
264
272 exprt get_pointer_to_member_value(
273 const exprt &expr,
274 const pointer_valuet &pointer_value,
275 const source_locationt &location);
276
284 exprt get_non_char_pointer_value(
285 const exprt &expr,
286 const pointer_valuet &value,
287 const source_locationt &location);
288
296 exprt get_pointer_to_function_value(
297 const exprt &expr,
298 const pointer_valuet &pointer_value,
299 const source_locationt &location);
300
311 exprt get_char_pointer_value(
312 const exprt &expr,
313 const memory_addresst &memory_location,
314 const source_locationt &location);
315
317 void process_outstanding_assignments();
318
322 std::string get_gdb_value(const exprt &expr);
323
329 bool points_to_member(
330 pointer_valuet &pointer_value,
331 const pointer_typet &expected_type);
332};
333
334#endif // CPROVER_MEMORY_ANALYZER_ANALYZE_SYMBOL_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
Interface for running and querying GDB.
Definition gdb_api.h:30
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
The symbol table base class interface.
The symbol table.
The type of an expression, extends irept.
Definition type.h:29
Low-level interface to gdb.
nonstd::optional< T > optionalt
Definition optional.h:35
BigInt mp_integer
Definition smt_terms.h:18
static bool contains(const exprt &index, const symbol_exprt &qvar)
Look for symbol qvar in the expression index and return true if found.
Memory address imbued with the explicit boolean data indicating if the address is null or not.
Definition gdb_api.h:37
Data associated with the value of a pointer, i.e.
Definition gdb_api.h:77
Author: Diffblue Ltd.