CBMC
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 <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 
28 class pointer_typet;
29 class source_locationt;
30 
33 {
34 public:
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 
56 
59 
61  {
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 
73 private:
75 
79  const namespacet ns;
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 
95  {
96  private:
97  size_t begin_int;
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:
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 
132  mp_integer
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
171 
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 
215  const exprt &expr,
216  const exprt &array,
217  const source_locationt &location);
218 
229  const exprt &expr,
230  const exprt &zero_expr,
231  const source_locationt &location);
232 
239  const exprt &expr,
240  const exprt &zero_expr,
241  const source_locationt &location);
242 
249  const exprt &expr,
250  const exprt &zero_expr,
251  const source_locationt &location);
252 
261  const exprt &expr,
262  const exprt &zero_expr,
263  const source_locationt &location);
264 
273  const exprt &expr,
274  const pointer_valuet &pointer_value,
275  const source_locationt &location);
276 
285  const exprt &expr,
286  const pointer_valuet &value,
287  const source_locationt &location);
288 
297  const exprt &expr,
298  const pointer_valuet &pointer_value,
299  const source_locationt &location);
300 
312  const exprt &expr,
313  const memory_addresst &memory_location,
314  const source_locationt &location);
315 
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:38
Base class for all expressions.
Definition: expr.h:56
Interface for running and querying GDB.
Definition: gdb_api.h:30
bool run_gdb_to_breakpoint(const std::string &breakpoint)
Run gdb to the given breakpoint.
Definition: gdb_api.cpp:345
void create_gdb_process()
Create a new gdb process for analysing the binary indicated by the first element in args
Definition: gdb_api.cpp:67
void run_gdb_from_core(const std::string &corefile)
Run gdb with the given core file.
Definition: gdb_api.cpp:275
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...
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.
gdb_value_extractort(const symbol_table_baset &symbol_table, const std::vector< std::string > &args)
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::list< std::string > &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.
std::optional< 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...
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:94
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
The symbol table base class interface.
The symbol table.
Definition: symbol_table.h:14
The type of an expression, extends irept.
Definition: type.h:29
Low-level interface to gdb.
BigInt mp_integer
Definition: smt_terms.h:17
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
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.
memory_scopet(const memory_addresst &begin, const mp_integer &byte_size, const irep_idt &name)
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.