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 <ansi-c/expr2c_class.h>
17
18#include <util/namespace.h>
19#include <util/symbol_table.h>
20
22
23#include "gdb_api.h"
24
25#include <map>
26#include <string>
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
188 std::optional<std::string>
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
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Low-level interface to gdb.
BigInt mp_integer
Definition smt_terms.h:17
static bool contains(const exprt &index, const symbol_exprt &qvar)
Look for symbol qvar in the expression index and return true if found.
Author: Diffblue Ltd.
dstringt irep_idt