cprover
analyze_symbol.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbol Analyzer
4 
5 Author: 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/allocate_objects.h>
24 #include <util/message.h>
25 #include <util/namespace.h>
26 #include <util/std_code.h>
27 #include <util/symbol_table.h>
28 
29 class gdb_apit;
30 class exprt;
31 class source_locationt;
32 
35 {
36 public:
39  const std::vector<std::string> &args);
40 
45  void analyze_symbols(const std::vector<irep_idt> &symbols);
46 
49  std::string get_snapshot_as_c_code();
50 
58 
61 
63  {
65  }
66  bool run_gdb_to_breakpoint(const std::string &breakpoint)
67  {
68  return gdb_api.run_gdb_to_breakpoint(breakpoint);
69  }
70  void run_gdb_from_core(const std::string &corefile)
71  {
72  gdb_api.run_gdb_from_core(corefile);
73  }
74 
75 private:
77 
81  const namespacet ns;
84 
86  std::map<exprt, exprt> assignments;
87 
90  std::map<exprt, memory_addresst> outstanding_assignments;
91 
94  std::map<memory_addresst, exprt> values;
95 
97  {
98  private:
99  size_t begin_int;
102 
106  size_t address2size_t(const memory_addresst &point) const;
107 
111  bool check_containment(const size_t &point_int) const
112  {
113  return point_int >= begin_int && (begin_int + byte_size) > point_int;
114  }
115 
116  public:
118  const memory_addresst &begin,
119  const mp_integer &byte_size,
120  const irep_idt &name);
121 
125  bool contains(const memory_addresst &point) const
126  {
127  return check_containment(address2size_t(point));
128  }
129 
134  mp_integer
135  distance(const memory_addresst &point, mp_integer member_size) const;
136 
139  irep_idt id() const
140  {
141  return name;
142  }
143 
146  mp_integer size() const
147  {
148  return byte_size;
149  }
150  };
151 
153  std::vector<memory_scopet> dynamically_allocated;
154 
156  std::map<irep_idt, pointer_valuet> memory_map;
157 
158  bool has_known_memory_location(const irep_idt &id) const
159  {
160  return memory_map.count(id) != 0;
161  }
162 
166  std::vector<memory_scopet>::iterator find_dynamic_allocation(irep_idt name);
167 
171  std::vector<memory_scopet>::iterator
173 
178 
191  get_malloc_pointee(const memory_addresst &point, mp_integer member_size);
192 
196  mp_integer get_type_size(const typet &type) const;
197 
202  void analyze_symbol(const irep_idt &symbol_name);
203 
208  void add_assignment(const exprt &lhs, const exprt &value);
209 
217  const exprt &expr,
218  const exprt &array,
219  const source_locationt &location);
220 
231  const exprt &expr,
232  const exprt &zero_expr,
233  const source_locationt &location);
234 
241  const exprt &expr,
242  const exprt &zero_expr,
243  const source_locationt &location);
244 
251  const exprt &expr,
252  const exprt &zero_expr,
253  const source_locationt &location);
254 
263  const exprt &expr,
264  const exprt &zero_expr,
265  const source_locationt &location);
266 
275  const exprt &expr,
276  const pointer_valuet &pointer_value,
277  const source_locationt &location);
278 
287  const exprt &expr,
288  const pointer_valuet &value,
289  const source_locationt &location);
290 
299  const exprt &expr,
300  const pointer_valuet &pointer_value,
301  const source_locationt &location);
302 
314  const exprt &expr,
315  const memory_addresst &memory_location,
316  const source_locationt &location);
317 
320 
324  std::string get_gdb_value(const exprt &expr);
325 
331  bool
332  points_to_member(pointer_valuet &pointer_value, const typet &expected_type);
333 };
334 
335 #endif // CPROVER_MEMORY_ANALYZER_ANALYZE_SYMBOL_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
gdb_apit::pointer_valuet
Data associated with the value of a pointer, i.e.
Definition: gdb_api.h:78
gdb_value_extractort::gdb_value_extractort
gdb_value_extractort(const symbol_tablet &symbol_table, const std::vector< std::string > &args)
Definition: analyze_symbol.cpp:23
typet
The type of an expression, extends irept.
Definition: type.h:29
gdb_value_extractort::analyze_symbols
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 ...
Definition: analyze_symbol.cpp:108
gdb_value_extractort::get_snapshot_as_symbol_table
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 ...
Definition: analyze_symbol.cpp:185
gdb_value_extractort::memory_scopet::byte_size
mp_integer byte_size
Definition: analyze_symbol.h:100
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
gdb_value_extractort::get_pointer_value
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.
Definition: analyze_symbol.cpp:478
gdb_value_extractort::get_expr_value
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...
Definition: analyze_symbol.cpp:591
gdb_value_extractort::memory_scopet::distance
mp_integer distance(const memory_addresst &point, mp_integer member_size) const
Compute the distance of point from the beginning of this scope.
Definition: analyze_symbol.cpp:50
gdb_value_extractort::get_struct_value
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.
Definition: analyze_symbol.cpp:674
gdb_value_extractort::ns
const namespacet ns
Definition: analyze_symbol.h:81
gdb_value_extractort::get_union_value
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.
Definition: analyze_symbol.cpp:707
gdb_value_extractort::has_known_memory_location
bool has_known_memory_location(const irep_idt &id) const
Definition: analyze_symbol.h:158
exprt
Base class for all expressions.
Definition: expr.h:53
gdb_value_extractort::memory_scopet::begin_int
size_t begin_int
Definition: analyze_symbol.h:99
gdb_apit::memory_addresst
Memory address imbued with the explicit boolean data indicating if the address is null or not.
Definition: gdb_api.h:38
namespace.h
gdb_apit
Interface for running and querying GDB.
Definition: gdb_api.h:31
gdb_api.h
Low-level interface to gdb.
gdb_value_extractort::memory_scopet::check_containment
bool check_containment(const size_t &point_int) const
Helper function that check if a point in memory points inside this scope.
Definition: analyze_symbol.h:111
gdb_value_extractort::create_gdb_process
void create_gdb_process()
Definition: analyze_symbol.h:62
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
gdb_value_extractort::pointer_valuet
gdb_apit::pointer_valuet pointer_valuet
Definition: analyze_symbol.h:59
expr2ct
Definition: expr2c_class.h:28
gdb_value_extractort::values
std::map< memory_addresst, exprt > values
Storing pairs <address, symbol> such that at address is stored the value of symbol.
Definition: analyze_symbol.h:94
gdb_value_extractort::get_gdb_value
std::string get_gdb_value(const exprt &expr)
Extract a stringified value from and c-converted expr.
Definition: analyze_symbol.cpp:738
gdb_value_extractort::get_malloc_size
mp_integer get_malloc_size(irep_idt name)
Search for the size of the allocated memory for name.
Definition: analyze_symbol.cpp:79
gdb_value_extractort
Interface for extracting values from GDB (building on gdb_apit)
Definition: analyze_symbol.h:35
gdb_value_extractort::get_type_size
mp_integer get_type_size(const typet &type) const
Wrapper for call get_offset_pointer_bits.
Definition: analyze_symbol.cpp:101
gdb_value_extractort::get_char_pointer_value
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.
Definition: analyze_symbol.cpp:224
gdb_value_extractort::memory_scopet::size
mp_integer size() const
Getter for the allocation size of this memory scope.
Definition: analyze_symbol.h:146
gdb_value_extractort::get_pointer_to_member_value
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.
Definition: analyze_symbol.cpp:266
gdb_value_extractort::memory_scopet::contains
bool contains(const memory_addresst &point) const
Check if point points somewhere in this memory scope.
Definition: analyze_symbol.h:125
gdb_value_extractort::run_gdb_to_breakpoint
bool run_gdb_to_breakpoint(const std::string &breakpoint)
Definition: analyze_symbol.h:66
gdb_value_extractort::memory_scopet::name
irep_idt name
Definition: analyze_symbol.h:101
gdb_value_extractort::memory_scopet::id
irep_idt id() const
Getter for the name of this memory scope.
Definition: analyze_symbol.h:139
expr2c_class.h
gdb_value_extractort::memory_map
std::map< irep_idt, pointer_valuet > memory_map
Keep track of the memory location for the analyzed symbols.
Definition: analyze_symbol.h:156
gdb_value_extractort::points_to_member
bool points_to_member(pointer_valuet &pointer_value, const typet &expected_type)
Analyzes the pointer_value to decide if it point to a struct or a union (or array)
Definition: analyze_symbol.cpp:452
gdb_value_extractort::get_pointer_to_function_value
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 ...
Definition: analyze_symbol.cpp:327
std_code.h
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
gdb_value_extractort::add_assignment
void add_assignment(const exprt &lhs, const exprt &value)
Create assignment lhs := value (see analyze_symbol)
Definition: analyze_symbol.cpp:218
source_locationt
Definition: source_location.h:20
gdb_value_extractort::c_converter
expr2ct c_converter
Definition: analyze_symbol.h:82
gdb_apit::create_gdb_process
void create_gdb_process()
Create a new gdb process for analysing the binary indicated by the first element in args
Definition: gdb_api.cpp:72
gdb_value_extractort::allocate_objects
allocate_objectst allocate_objects
Definition: analyze_symbol.h:83
gdb_value_extractort::memory_addresst
gdb_apit::memory_addresst memory_addresst
Definition: analyze_symbol.h:60
gdb_value_extractort::memory_scopet::address2size_t
size_t address2size_t(const memory_addresst &point) const
Convert base-16 memory address to a natural number.
Definition: analyze_symbol.cpp:44
gdb_value_extractort::dynamically_allocated
std::vector< memory_scopet > dynamically_allocated
Keep track of the dynamically allocated memory.
Definition: analyze_symbol.h:153
gdb_value_extractort::get_array_value
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...
Definition: analyze_symbol.cpp:567
gdb_apit::run_gdb_to_breakpoint
bool run_gdb_to_breakpoint(const std::string &breakpoint)
Run gdb to the given breakpoint.
Definition: gdb_api.cpp:333
gdb_value_extractort::get_non_char_pointer_value
exprt get_non_char_pointer_value(const exprt &expr, const pointer_valuet &value, const source_locationt &location)
Similar to get_char_pointer_value.
Definition: analyze_symbol.cpp:348
gdb_value_extractort::process_outstanding_assignments
void process_outstanding_assignments()
Call add_assignment for each pair in outstanding_assignments.
Definition: analyze_symbol.cpp:729
gdb_apit::run_gdb_from_core
void run_gdb_from_core(const std::string &corefile)
Run gdb with the given core file.
Definition: gdb_api.cpp:275
gdb_value_extractort::outstanding_assignments
std::map< exprt, memory_addresst > outstanding_assignments
Mapping pointer expression for which get_non_char_pointer_value returned nil expression to memory loc...
Definition: analyze_symbol.h:90
allocate_objectst
Definition: allocate_objects.h:31
gdb_value_extractort::assignments
std::map< exprt, exprt > assignments
Sequence of assignments collected during analyze_symbols.
Definition: analyze_symbol.h:86
symbol_table.h
Author: Diffblue Ltd.
gdb_value_extractort::find_dynamic_allocation
std::vector< memory_scopet >::iterator find_dynamic_allocation(irep_idt name)
Search for a memory scope allocated under name.
Definition: analyze_symbol.cpp:60
message.h
gdb_value_extractort::analyze_symbol
void analyze_symbol(const irep_idt &symbol_name)
Assign the gdb-extracted value for symbol_name to its symbol expression and then process outstanding ...
Definition: analyze_symbol.cpp:144
gdb_value_extractort::memory_scopet::memory_scopet
memory_scopet(const memory_addresst &begin, const mp_integer &byte_size, const irep_idt &name)
Definition: analyze_symbol.cpp:34
allocate_objects.h
gdb_value_extractort::get_snapshot_as_c_code
std::string get_snapshot_as_c_code()
Get memory snapshot as C code.
Definition: analyze_symbol.cpp:170
gdb_value_extractort::memory_scopet
Definition: analyze_symbol.h:97
gdb_value_extractort::get_malloc_pointee
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...
Definition: analyze_symbol.cpp:88
gdb_value_extractort::run_gdb_from_core
void run_gdb_from_core(const std::string &corefile)
Definition: analyze_symbol.h:70
gdb_value_extractort::gdb_api
gdb_apit gdb_api
Definition: analyze_symbol.h:76
gdb_value_extractort::symbol_table
symbol_tablet symbol_table
External symbol table – extracted from read_goto_binary We only expect to analyse symbols located the...
Definition: analyze_symbol.h:80