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/message.h>
24#include <util/namespace.h>
25#include <util/pointer_expr.h>
26#include <util/std_code.h>
27#include <util/symbol_table.h>
28
30
31class gdb_apit;
32class exprt;
34
37{
38public:
41 const std::vector<std::string> &args);
42
47 void analyze_symbols(const std::vector<irep_idt> &symbols);
48
51 std::string get_snapshot_as_c_code();
52
60
63
65 {
67 }
68 bool run_gdb_to_breakpoint(const std::string &breakpoint)
69 {
70 return gdb_api.run_gdb_to_breakpoint(breakpoint);
71 }
72 void run_gdb_from_core(const std::string &corefile)
73 {
74 gdb_api.run_gdb_from_core(corefile);
75 }
76
77private:
79
86
88 std::map<exprt, exprt> assignments;
89
92 std::map<exprt, memory_addresst> outstanding_assignments;
93
96 std::map<memory_addresst, exprt> values;
97
99 {
100 private:
101 size_t begin_int;
104
108 size_t address2size_t(const memory_addresst &point) const;
109
113 bool check_containment(const size_t &point_int) const
114 {
115 return point_int >= begin_int && (begin_int + byte_size) > point_int;
116 }
117
118 public:
120 const memory_addresst &begin,
121 const mp_integer &byte_size,
122 const irep_idt &name);
123
127 bool contains(const memory_addresst &point) const
128 {
129 return check_containment(address2size_t(point));
130 }
131
137 distance(const memory_addresst &point, mp_integer member_size) const;
138
141 irep_idt id() const
142 {
143 return name;
144 }
145
149 {
150 return byte_size;
151 }
152 };
153
155 std::vector<memory_scopet> dynamically_allocated;
156
158 std::map<irep_idt, pointer_valuet> memory_map;
159
161 {
162 return memory_map.count(id) != 0;
163 }
164
168 std::vector<memory_scopet>::iterator find_dynamic_allocation(irep_idt name);
169
173 std::vector<memory_scopet>::iterator
175
180
193 get_malloc_pointee(const memory_addresst &point, mp_integer member_size);
194
198 mp_integer get_type_size(const typet &type) const;
199
204 void analyze_symbol(const irep_idt &symbol_name);
205
210 void add_assignment(const exprt &lhs, const exprt &value);
211
219 const exprt &expr,
220 const exprt &array,
221 const source_locationt &location);
222
233 const exprt &expr,
234 const exprt &zero_expr,
235 const source_locationt &location);
236
243 const exprt &expr,
244 const exprt &zero_expr,
245 const source_locationt &location);
246
253 const exprt &expr,
254 const exprt &zero_expr,
255 const source_locationt &location);
256
265 const exprt &expr,
266 const exprt &zero_expr,
267 const source_locationt &location);
268
277 const exprt &expr,
278 const pointer_valuet &pointer_value,
279 const source_locationt &location);
280
289 const exprt &expr,
290 const pointer_valuet &value,
291 const source_locationt &location);
292
301 const exprt &expr,
302 const pointer_valuet &pointer_value,
303 const source_locationt &location);
304
316 const exprt &expr,
317 const memory_addresst &memory_location,
318 const source_locationt &location);
319
322
326 std::string get_gdb_value(const exprt &expr);
327
333 bool points_to_member(
334 pointer_valuet &pointer_value,
335 const pointer_typet &expected_type);
336};
337
338#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:37
Base class for all expressions.
Definition expr.h:54
Interface for running and querying GDB.
Definition gdb_api.h:31
bool run_gdb_to_breakpoint(const std::string &breakpoint)
Run gdb to the given breakpoint.
Definition gdb_api.cpp:335
void create_gdb_process()
Create a new gdb process for analysing the binary indicated by the first element in args
Definition gdb_api.cpp:69
void run_gdb_from_core(const std::string &corefile)
Run gdb with the given core file.
Definition gdb_api.cpp:277
Interface for extracting values from GDB (building on gdb_apit)
std::string get_gdb_value(const exprt &expr)
Extract a stringified value from and c-converted expr.
exprt get_pointer_to_member_value(const exprt &expr, const pointer_valuet &pointer_value, const source_locationt &location)
Call get_subexpression_at_offset to get the correct member expression.
allocate_objectst allocate_objects
bool run_gdb_to_breakpoint(const std::string &breakpoint)
std::map< irep_idt, pointer_valuet > memory_map
Keep track of the memory location for the analyzed symbols.
std::map< exprt, memory_addresst > outstanding_assignments
Mapping pointer expression for which get_non_char_pointer_value returned nil expression to memory loc...
optionalt< std::string > get_malloc_pointee(const memory_addresst &point, mp_integer member_size)
Build the pointee string for address point assuming it points to a dynamic allocation of ā€˜n’ elements...
gdb_apit::pointer_valuet pointer_valuet
void analyze_symbol(const irep_idt &symbol_name)
Assign the gdb-extracted value for symbol_name to its symbol expression and then process outstanding ...
bool has_known_memory_location(const irep_idt &id) const
exprt get_char_pointer_value(const exprt &expr, const memory_addresst &memory_location, const source_locationt &location)
If memory_location is found among values then return the symbol expression associated with it.
exprt get_pointer_to_function_value(const exprt &expr, const pointer_valuet &pointer_value, const source_locationt &location)
Extract the function name from pointer_value, check it has a symbol and return the associated symbol ...
void process_outstanding_assignments()
Call add_assignment for each pair in outstanding_assignments.
exprt get_array_value(const exprt &expr, const exprt &array, const source_locationt &location)
Iterate over array and fill its operands with the results of calling get_expr_value on index expressi...
void add_assignment(const exprt &lhs, const exprt &value)
Create assignment lhs := value (see analyze_symbol)
std::vector< memory_scopet > dynamically_allocated
Keep track of the dynamically allocated memory.
void run_gdb_from_core(const std::string &corefile)
std::map< exprt, exprt > assignments
Sequence of assignments collected during analyze_symbols.
std::string get_snapshot_as_c_code()
Get memory snapshot as C code.
std::map< memory_addresst, exprt > values
Storing pairs <address, symbol> such that at address is stored the value of symbol.
exprt get_expr_value(const exprt &expr, const exprt &zero_expr, const source_locationt &location)
Case analysis on the typet of expr 1) For integers, booleans, and enums: call gdb_apit::get_value dir...
mp_integer get_type_size(const typet &type) const
Wrapper for call get_offset_pointer_bits.
void analyze_symbols(const std::vector< irep_idt > &symbols)
For each input symbol in symbols: map its value address to its symbol_exprt (via the values map) and ...
bool points_to_member(pointer_valuet &pointer_value, const pointer_typet &expected_type)
Analyzes the pointer_value to decide if it point to a struct or a union (or array)
mp_integer get_malloc_size(irep_idt name)
Search for the size of the allocated memory for name.
exprt get_pointer_value(const exprt &expr, const exprt &zero_expr, const source_locationt &location)
Call gdb_apit::get_memory on expr then split based on the points-to type being char type or not.
symbol_tablet symbol_table
External symbol table – extracted from read_goto_binary We only expect to analyse symbols located the...
exprt get_struct_value(const exprt &expr, const exprt &zero_expr, const source_locationt &location)
For each of the members of the struct: call get_expr_value.
std::vector< memory_scopet >::iterator find_dynamic_allocation(irep_idt name)
Search for a memory scope allocated under name.
exprt get_union_value(const exprt &expr, const exprt &zero_expr, const source_locationt &location)
For each of the members of the struct: call get_expr_value.
symbol_tablet get_snapshot_as_symbol_table()
Get memory snapshot as symbol table Build a new symbol_tablet and for each lhs symbol from collected ...
exprt get_non_char_pointer_value(const exprt &expr, const pointer_valuet &value, const source_locationt &location)
Similar to get_char_pointer_value.
gdb_apit::memory_addresst memory_addresst
const namespacet ns
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.
The type of an expression, extends irept.
Definition type.h:29
Low-level interface to gdb.
nonstd::optional< T > optionalt
Definition optional.h:35
API to expression classes for Pointers.
BigInt mp_integer
Definition smt_terms.h:12
Memory address imbued with the explicit boolean data indicating if the address is null or not.
Definition gdb_api.h:38
Data associated with the value of a pointer, i.e.
Definition gdb_api.h:78
mp_integer distance(const memory_addresst &point, mp_integer member_size) const
Compute the distance of point from the beginning of this scope.
bool check_containment(const size_t &point_int) const
Helper function that check if a point in memory points inside this scope.
mp_integer size() const
Getter for the allocation size of this memory scope.
bool contains(const memory_addresst &point) const
Check if point points somewhere in this memory scope.
size_t address2size_t(const memory_addresst &point) const
Convert base-16 memory address to a natural number.
irep_idt id() const
Getter for the name of this memory scope.
Author: Diffblue Ltd.