cprover
analyze_symbol.cpp
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 
10 #include <cstdlib>
11 
12 #include "analyze_symbol.h"
13 
14 #include <util/c_types.h>
15 #include <util/c_types_util.h>
16 #include <util/config.h>
17 #include <util/expr_initializer.h>
19 #include <util/string2int.h>
20 #include <util/string_constant.h>
21 #include <util/string_utils.h>
22 
24  const symbol_tablet &symbol_table,
25  const std::vector<std::string> &args)
26  : gdb_api(args),
27  symbol_table(symbol_table),
28  ns(symbol_table),
29  c_converter(ns, expr2c_configurationt::clean_configuration),
30  allocate_objects(ID_C, source_locationt(), irep_idt{}, this->symbol_table)
31 {
32 }
33 
35  const memory_addresst &begin,
36  const mp_integer &byte_size,
37  const irep_idt &name)
38  : begin_int(safe_string2size_t(begin.address_string, 0)),
39  byte_size(byte_size),
40  name(name)
41 {
42 }
43 
45  const memory_addresst &point) const
46 {
47  return safe_string2size_t(point.address_string, 0);
48 }
49 
51  const memory_addresst &point,
52  mp_integer member_size) const
53 {
54  auto point_int = address2size_t(point);
55  CHECK_RETURN(check_containment(point_int));
56  return (point_int - begin_int) / member_size;
57 }
58 
59 std::vector<gdb_value_extractort::memory_scopet>::iterator
61 {
62  return std::find_if(
63  dynamically_allocated.begin(),
65  [&name](const memory_scopet &scope) { return scope.id() == name; });
66 }
67 
68 std::vector<gdb_value_extractort::memory_scopet>::iterator
70 {
71  return std::find_if(
72  dynamically_allocated.begin(),
74  [&point](const memory_scopet &memory_scope) {
75  return memory_scope.contains(point);
76  });
77 }
78 
80 {
81  const auto scope_it = find_dynamic_allocation(name);
82  if(scope_it == dynamically_allocated.end())
83  return 1;
84  else
85  return scope_it->size();
86 }
87 
89  const memory_addresst &point,
90  mp_integer member_size)
91 {
92  const auto scope_it = find_dynamic_allocation(point);
93  if(scope_it == dynamically_allocated.end())
94  return {};
95 
96  const auto pointer_distance = scope_it->distance(point, member_size);
97  return id2string(scope_it->id()) +
98  (pointer_distance > 0 ? "+" + integer2string(pointer_distance) : "");
99 }
100 
102 {
103  const auto maybe_size = pointer_offset_bits(type, ns);
104  CHECK_RETURN(maybe_size.has_value());
105  return *maybe_size / 8;
106 }
107 
108 void gdb_value_extractort::analyze_symbols(const std::vector<irep_idt> &symbols)
109 {
110  // record addresses of given symbols
111  for(const auto &id : symbols)
112  {
113  const symbolt &symbol = ns.lookup(id);
114  if(symbol.type.id() != ID_pointer || is_c_char_type(symbol.type.subtype()))
115  {
116  const symbol_exprt &symbol_expr = ns.lookup(id).symbol_expr();
117  const address_of_exprt aoe(symbol_expr);
118 
119  const std::string c_expr = c_converter.convert(aoe);
120  const pointer_valuet &value = gdb_api.get_memory(c_expr);
121  CHECK_RETURN(value.pointee.empty() || (id == value.pointee));
122 
123  memory_map[id] = value;
124  }
125  else
126  {
127  const std::string c_symbol = c_converter.convert(symbol.symbol_expr());
128  const pointer_valuet &symbol_value = gdb_api.get_memory(c_symbol);
129  size_t symbol_size = gdb_api.query_malloc_size(c_symbol);
130 
131  if(symbol_size > 1)
132  dynamically_allocated.emplace_back(
133  symbol_value.address, symbol_size, id);
134  memory_map[id] = symbol_value;
135  }
136  }
137 
138  for(const auto &id : symbols)
139  {
140  analyze_symbol(id);
141  }
142 }
143 
145 {
146  const symbolt &symbol = ns.lookup(symbol_name);
147  const symbol_exprt symbol_expr = symbol.symbol_expr();
148 
149  try
150  {
151  const typet target_type = symbol.type;
152 
153  const auto zero_expr = zero_initializer(target_type, symbol.location, ns);
154  CHECK_RETURN(zero_expr);
155 
156  const exprt target_expr =
157  get_expr_value(symbol_expr, *zero_expr, symbol.location);
158 
159  add_assignment(symbol_expr, target_expr);
160  }
161  catch(const gdb_interaction_exceptiont &e)
162  {
163  throw analysis_exceptiont(e.what());
164  }
165 
167 }
168 
171 {
172  code_blockt generated_code;
173 
175 
176  for(auto const &pair : assignments)
177  {
178  generated_code.add(code_assignt(pair.first, pair.second));
179  }
180 
181  return c_converter.convert(generated_code);
182 }
183 
186 {
187  symbol_tablet snapshot;
188 
189  for(const auto &pair : assignments)
190  {
191  const symbol_exprt &symbol_expr = to_symbol_expr(pair.first);
192  const irep_idt id = symbol_expr.get_identifier();
193 
194  INVARIANT(symbol_table.has_symbol(id), "symbol must exist in symbol table");
195 
196  const symbolt &symbol = symbol_table.lookup_ref(id);
197 
198  symbolt snapshot_symbol(symbol);
199  snapshot_symbol.value = pair.second;
200 
201  snapshot.insert(snapshot_symbol);
202  }
203 
204  // Also add type symbols to the snapshot
205  for(const auto &pair : symbol_table)
206  {
207  const symbolt &symbol = pair.second;
208 
209  if(symbol.is_type)
210  {
211  snapshot.insert(symbol);
212  }
213  }
214 
215  return snapshot;
216 }
217 
218 void gdb_value_extractort::add_assignment(const exprt &lhs, const exprt &value)
219 {
220  if(assignments.count(lhs) == 0)
221  assignments.emplace(std::make_pair(lhs, value));
222 }
223 
225  const exprt &expr,
226  const memory_addresst &memory_location,
227  const source_locationt &location)
228 {
229  PRECONDITION(expr.type().id() == ID_pointer);
231  PRECONDITION(!memory_location.is_null());
232 
233  auto it = values.find(memory_location);
234 
235  if(it == values.end())
236  {
237  std::string c_expr = c_converter.convert(expr);
238  pointer_valuet value = gdb_api.get_memory(c_expr);
239  CHECK_RETURN(value.string);
240 
241  string_constantt init(*value.string);
243 
244  symbol_exprt dummy("tmp", pointer_type(init.type()));
246 
247  const symbol_exprt new_symbol =
249  assignments, dummy, init.type()));
250 
251  add_assignment(new_symbol, init);
252 
253  values.insert(std::make_pair(memory_location, new_symbol));
254 
255  // check that we are returning objects of the right type
256  CHECK_RETURN(new_symbol.type().subtype() == expr.type().subtype());
257  return new_symbol;
258  }
259  else
260  {
261  CHECK_RETURN(it->second.type().subtype() == expr.type().subtype());
262  return it->second;
263  }
264 }
265 
267  const exprt &expr,
268  const pointer_valuet &pointer_value,
269  const source_locationt &location)
270 {
271  PRECONDITION(expr.type().id() == ID_pointer);
272  const auto &memory_location = pointer_value.address;
273  std::string memory_location_string = memory_location.string();
274  PRECONDITION(memory_location_string != "0x0");
275  PRECONDITION(!pointer_value.pointee.empty());
276 
277  std::string struct_name;
278  size_t member_offset;
279  if(pointer_value.has_known_offset())
280  {
281  std::string member_offset_string;
282  split_string(
283  pointer_value.pointee, '+', struct_name, member_offset_string, true);
284  member_offset = safe_string2size_t(member_offset_string);
285  }
286  else
287  {
288  struct_name = pointer_value.pointee;
289  member_offset = 0;
290  }
291 
292  const symbolt *struct_symbol = symbol_table.lookup(struct_name);
293  DATA_INVARIANT(struct_symbol != nullptr, "unknown struct");
294 
295  if(!has_known_memory_location(struct_name))
296  {
297  memory_map[struct_name] = gdb_api.get_memory(struct_name);
298  analyze_symbol(irep_idt{struct_name});
299  }
300 
301  const auto &struct_symbol_expr = struct_symbol->symbol_expr();
302  if(struct_symbol->type.id() == ID_array)
303  {
304  return index_exprt{
305  struct_symbol_expr,
306  from_integer(
308  }
309  if(struct_symbol->type.id() == ID_pointer)
310  {
311  return dereference_exprt{
312  plus_exprt{struct_symbol_expr,
314  expr.type()}};
315  }
316 
317  const auto maybe_member_expr = get_subexpression_at_offset(
318  struct_symbol_expr, member_offset, expr.type().subtype(), ns);
320  maybe_member_expr.has_value(), "structure doesn't have member");
321 
322  // check that we return the right type
323  CHECK_RETURN(maybe_member_expr->type() == expr.type().subtype());
324  return *maybe_member_expr;
325 }
326 
328  const exprt &expr,
329  const pointer_valuet &pointer_value,
330  const source_locationt &location)
331 {
332  PRECONDITION(expr.type().id() == ID_pointer);
333  PRECONDITION(expr.type().subtype().id() == ID_code);
334  PRECONDITION(!pointer_value.address.is_null());
335 
336  const auto &function_name = pointer_value.pointee;
337  CHECK_RETURN(!function_name.empty());
338  const auto function_symbol = symbol_table.lookup(function_name);
339  if(function_symbol == nullptr)
340  {
342  "input source code does not contain function: " + function_name};
343  }
344  CHECK_RETURN(function_symbol->type.id() == ID_code);
345  return function_symbol->symbol_expr();
346 }
347 
349  const exprt &expr,
350  const pointer_valuet &value,
351  const source_locationt &location)
352 {
353  PRECONDITION(expr.type().id() == ID_pointer);
355  const auto &memory_location = value.address;
356  PRECONDITION(!memory_location.is_null());
357 
358  auto it = values.find(memory_location);
359 
360  if(it == values.end())
361  {
362  if(!value.pointee.empty() && value.pointee != c_converter.convert(expr))
363  {
364  analyze_symbol(value.pointee);
365  const auto pointee_symbol = symbol_table.lookup(value.pointee);
366  CHECK_RETURN(pointee_symbol != nullptr);
367  const auto pointee_symbol_expr = pointee_symbol->symbol_expr();
368  return pointee_symbol_expr;
369  }
370 
371  values.insert(std::make_pair(memory_location, nil_exprt()));
372 
373  const typet target_type = expr.type().subtype();
374 
375  symbol_exprt dummy("tmp", expr.type());
377 
378  const auto zero_expr = zero_initializer(target_type, location, ns);
379  CHECK_RETURN(zero_expr);
380 
381  // Check if pointer was dynamically allocated (via malloc). If so we will
382  // replace the pointee with a static array filled with values stored at the
383  // expected positions. Since the allocated size is over-approximation we may
384  // end up querying pass the allocated bounds and building larger array with
385  // meaningless values.
386  mp_integer allocated_size = get_malloc_size(c_converter.convert(expr));
387  // get the sizeof(target_type) and thus the number of elements
388  const auto number_of_elements = allocated_size / get_type_size(target_type);
389  if(allocated_size != 1 && number_of_elements > 1)
390  {
391  array_exprt::operandst elements;
392  // build the operands by querying for an index expression
393  for(size_t i = 0; i < number_of_elements; i++)
394  {
395  const auto sub_expr_value = get_expr_value(
396  index_exprt{expr, from_integer(i, index_type())},
397  *zero_expr,
398  location);
399  elements.push_back(sub_expr_value);
400  }
401  CHECK_RETURN(elements.size() == number_of_elements);
402 
403  // knowing the number of elements we can build the type
404  const typet target_array_type =
405  array_typet{target_type, from_integer(elements.size(), index_type())};
406 
407  array_exprt new_array{elements, to_array_type(target_array_type)};
408 
409  // allocate a new symbol for the temporary static array
410  symbol_exprt array_dummy("tmp", pointer_type(target_array_type));
411  const auto array_symbol =
413  assignments, array_dummy, target_array_type);
414 
415  // add assignment of value to newly created symbol
416  add_assignment(array_symbol, new_array);
417  values[memory_location] = array_symbol;
418  CHECK_RETURN(array_symbol.type().id() == ID_array);
419  return array_symbol;
420  }
421 
422  const symbol_exprt new_symbol =
424  assignments, dummy, target_type));
425 
426  dereference_exprt dereference_expr(expr);
427 
428  const exprt target_expr =
429  get_expr_value(dereference_expr, *zero_expr, location);
430  // add assignment of value to newly created symbol
431  add_assignment(new_symbol, target_expr);
432 
433  values[memory_location] = new_symbol;
434 
435  return new_symbol;
436  }
437  else
438  {
439  const auto &known_value = it->second;
440  const auto &expected_type = expr.type().subtype();
441  if(find_dynamic_allocation(memory_location) != dynamically_allocated.end())
442  return known_value;
443  if(known_value.is_not_nil() && known_value.type() != expected_type)
444  {
445  return symbol_exprt{to_symbol_expr(known_value).get_identifier(),
446  expected_type};
447  }
448  return known_value;
449  }
450 }
451 
453  pointer_valuet &pointer_value,
454  const typet &expected_type)
455 {
456  if(pointer_value.has_known_offset())
457  return true;
458 
459  if(pointer_value.pointee.empty())
460  {
461  const auto maybe_pointee = get_malloc_pointee(
462  pointer_value.address, get_type_size(expected_type.subtype()));
463  if(maybe_pointee.has_value())
464  pointer_value.pointee = *maybe_pointee;
465  if(pointer_value.pointee.find("+") != std::string::npos)
466  return true;
467  }
468 
469  const symbolt *pointee_symbol = symbol_table.lookup(pointer_value.pointee);
470  if(pointee_symbol == nullptr)
471  return false;
472  const auto &pointee_type = pointee_symbol->type;
473  return pointee_type.id() == ID_struct_tag ||
474  pointee_type.id() == ID_union_tag || pointee_type.id() == ID_array ||
475  pointee_type.id() == ID_struct || pointee_type.id() == ID_union;
476 }
477 
479  const exprt &expr,
480  const exprt &zero_expr,
481  const source_locationt &location)
482 {
483  PRECONDITION(zero_expr.id() == ID_constant);
484 
485  PRECONDITION(expr.type().id() == ID_pointer);
486  PRECONDITION(expr.type() == zero_expr.type());
487 
488  std::string c_expr = c_converter.convert(expr);
489  const auto known_pointer = memory_map.find(c_expr);
490 
491  pointer_valuet value = (known_pointer == memory_map.end() ||
492  known_pointer->second.pointee == c_expr)
493  ? gdb_api.get_memory(c_expr)
494  : known_pointer->second;
495  if(!value.valid)
496  return zero_expr;
497 
498  const auto memory_location = value.address;
499 
500  if(!memory_location.is_null())
501  {
502  // pointers-to-char can point to members as well, e.g. char[]
503  if(points_to_member(value, expr.type()))
504  {
505  const auto target_expr =
506  get_pointer_to_member_value(expr, value, location);
507  CHECK_RETURN(target_expr.is_not_nil());
508  const address_of_exprt result_expr{target_expr};
509  CHECK_RETURN(result_expr.type() == zero_expr.type());
510  return std::move(result_expr);
511  }
512 
513  // pointer to function
514  if(expr.type().subtype().id() == ID_code)
515  {
516  const auto target_expr =
517  get_pointer_to_function_value(expr, value, location);
518  CHECK_RETURN(target_expr.is_not_nil());
519  const address_of_exprt result_expr{target_expr};
520  CHECK_RETURN(result_expr.type() == zero_expr.type());
521  return std::move(result_expr);
522  }
523 
524  // non-member: split for char/non-char
525  const auto target_expr =
526  is_c_char_type(expr.type().subtype())
527  ? get_char_pointer_value(expr, memory_location, location)
528  : get_non_char_pointer_value(expr, value, location);
529 
530  // postpone if we cannot resolve now
531  if(target_expr.is_nil())
532  {
533  outstanding_assignments[expr] = memory_location;
534  return zero_expr;
535  }
536 
537  // the pointee was (probably) dynamically allocated (but the allocation
538  // would not be visible in the snapshot) so we pretend it is statically
539  // allocated (we have the value) and return address to the first element
540  // of the array (instead of the array as char*)
541  if(target_expr.type().id() == ID_array)
542  {
543  const auto result_indexed_expr = get_subexpression_at_offset(
544  target_expr, 0, zero_expr.type().subtype(), ns);
545  CHECK_RETURN(result_indexed_expr.has_value());
546  if(result_indexed_expr->type() == zero_expr.type())
547  return *result_indexed_expr;
548  const address_of_exprt result_expr{*result_indexed_expr};
549  CHECK_RETURN(result_expr.type() == zero_expr.type());
550  return std::move(result_expr);
551  }
552 
553  // if the types match return right away
554  if(target_expr.type() == zero_expr.type())
555  return target_expr;
556 
557  // otherwise the address of target should type-match
558  const address_of_exprt result_expr{target_expr};
559  if(result_expr.type() != zero_expr.type())
560  return typecast_exprt{result_expr, zero_expr.type()};
561  return std::move(result_expr);
562  }
563 
564  return zero_expr;
565 }
566 
568  const exprt &expr,
569  const exprt &array,
570  const source_locationt &location)
571 {
572  PRECONDITION(array.id() == ID_array);
573 
574  PRECONDITION(expr.type().id() == ID_array);
575  PRECONDITION(expr.type() == array.type());
576 
577  exprt new_array(array);
578 
579  for(size_t i = 0; i < new_array.operands().size(); ++i)
580  {
581  const index_exprt index_expr(expr, from_integer(i, index_type()));
582 
583  exprt &operand = new_array.operands()[i];
584 
585  operand = get_expr_value(index_expr, operand, location);
586  }
587 
588  return new_array;
589 }
590 
592  const exprt &expr,
593  const exprt &zero_expr,
594  const source_locationt &location)
595 {
596  PRECONDITION(expr.type() == zero_expr.type());
597 
598  const typet &type = expr.type();
599  PRECONDITION(type.id() != ID_struct);
600 
601  if(is_c_integral_type(type))
602  {
603  INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
604 
605  std::string c_expr = c_converter.convert(expr);
606  const auto maybe_value = gdb_api.get_value(c_expr);
607  if(!maybe_value.has_value())
608  return zero_expr;
609  const std::string value = *maybe_value;
610 
611  const mp_integer int_rep = string2integer(value);
612 
613  return from_integer(int_rep, type);
614  }
615  else if(is_c_char_type(type))
616  {
617  INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
618 
619  // check the char-value and return as bitvector-type value
620  std::string c_expr = c_converter.convert(expr);
621  const auto maybe_value = gdb_api.get_value(c_expr);
622  if(!maybe_value.has_value() || maybe_value->empty())
623  return zero_expr;
624  const std::string value = *maybe_value;
625 
626  const mp_integer int_rep = value[0];
627  return from_integer(int_rep, type);
628  }
629  else if(type.id() == ID_c_bool)
630  {
631  INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
632 
633  std::string c_expr = c_converter.convert(expr);
634  const auto maybe_value = gdb_api.get_value(c_expr);
635  if(!maybe_value.has_value())
636  return zero_expr;
637  const std::string value = *maybe_value;
638 
639  return from_c_boolean_value(id2boolean(value), type);
640  }
641  else if(type.id() == ID_c_enum)
642  {
643  INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
644 
645  std::string c_expr = c_converter.convert(expr);
646  const auto maybe_value = gdb_api.get_value(c_expr);
647  if(!maybe_value.has_value())
648  return zero_expr;
649  const std::string value = *maybe_value;
650 
652  }
653  else if(type.id() == ID_struct_tag)
654  {
655  return get_struct_value(expr, zero_expr, location);
656  }
657  else if(type.id() == ID_array)
658  {
659  return get_array_value(expr, zero_expr, location);
660  }
661  else if(type.id() == ID_pointer)
662  {
663  INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
664 
665  return get_pointer_value(expr, zero_expr, location);
666  }
667  else if(type.id() == ID_union_tag)
668  {
669  return get_union_value(expr, zero_expr, location);
670  }
671  UNREACHABLE;
672 }
673 
675  const exprt &expr,
676  const exprt &zero_expr,
677  const source_locationt &location)
678 {
679  PRECONDITION(zero_expr.id() == ID_struct);
680 
681  PRECONDITION(expr.type().id() == ID_struct_tag);
682  PRECONDITION(expr.type() == zero_expr.type());
683 
684  exprt new_expr(zero_expr);
685 
686  const struct_tag_typet &struct_tag_type = to_struct_tag_type(expr.type());
687  const struct_typet &struct_type = ns.follow_tag(struct_tag_type);
688 
689  for(size_t i = 0; i < new_expr.operands().size(); ++i)
690  {
691  const struct_typet::componentt &component = struct_type.components()[i];
692 
693  if(component.get_is_padding() || component.type().id() == ID_code)
694  {
695  continue;
696  }
697 
698  exprt &operand = new_expr.operands()[i];
699  member_exprt member_expr(expr, component);
700 
701  operand = get_expr_value(member_expr, operand, location);
702  }
703 
704  return new_expr;
705 }
706 
708  const exprt &expr,
709  const exprt &zero_expr,
710  const source_locationt &location)
711 {
712  PRECONDITION(zero_expr.id() == ID_union);
713 
714  PRECONDITION(expr.type().id() == ID_union_tag);
715  PRECONDITION(expr.type() == zero_expr.type());
716 
717  exprt new_expr(zero_expr);
718 
719  const union_tag_typet &union_tag_type = to_union_tag_type(expr.type());
720  const union_typet &union_type = ns.follow_tag(union_tag_type);
721 
722  CHECK_RETURN(new_expr.operands().size() == 1);
723  const union_typet::componentt &component = union_type.components()[0];
724  auto &operand = new_expr.operands()[0];
725  operand = get_expr_value(member_exprt{expr, component}, operand, location);
726  return new_expr;
727 }
728 
730 {
731  for(const auto &pair : outstanding_assignments)
732  {
733  const address_of_exprt aoe(values[pair.second]);
734  add_assignment(pair.first, aoe);
735  }
736 }
737 
739 {
740  std::string c_expr = c_converter.convert(expr);
741  const auto maybe_value = gdb_api.get_value(c_expr);
742  CHECK_RETURN(maybe_value.has_value());
743  return *maybe_value;
744 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:87
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:555
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
typet::subtype
const typet & subtype() const
Definition: type.h:47
gdb_apit::query_malloc_size
size_t query_malloc_size(const std::string &pointer_expr)
Get the exact allocated size for a pointer pointer_expr.
Definition: gdb_api.cpp:61
gdb_interaction_exceptiont
Definition: gdb_api.h:230
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
array_typet::is_complete
bool is_complete() const
Definition: std_types.h:983
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
string_utils.h
to_c_enum_type
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: std_types.h:681
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
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
convert_member_name_to_enum_value
constant_exprt convert_member_name_to_enum_value(const irep_idt &member_name, const c_enum_typet &c_enum)
This function creates a constant representing the bitvector encoded integer value of a string in the ...
Definition: c_types_util.h:83
gdb_apit::get_value
optionalt< std::string > get_value(const std::string &expr)
Get the memory address pointed to by the given pointer expression.
Definition: gdb_api.cpp:485
from_c_boolean_value
constant_exprt from_c_boolean_value(bool bool_value, const typet &type)
This function creates a constant representing either 0 or 1 as value of type type.
Definition: c_types_util.h:120
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
gdb_apit::pointer_valuet::pointee
std::string pointee
Definition: gdb_api.h:94
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
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
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
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
gdb_value_extractort::ns
const namespacet ns
Definition: analyze_symbol.h:81
string_constant.h
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
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:490
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
invalid_source_file_exceptiont
Thrown when we can't handle something in an input source file.
Definition: exception_utils.h:171
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:192
id2boolean
bool id2boolean(const std::string &bool_value)
Convert id to a Boolean value.
Definition: c_types_util.h:103
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
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
string_constantt
Definition: string_constant.h:16
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
safe_string2size_t
std::size_t safe_string2size_t(const std::string &str, int base)
Definition: string2int.cpp:26
zero_initializer
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Definition: expr_initializer.cpp:318
symbol_tablet::begin
virtual iteratort begin() override
Definition: symbol_table.h:114
union_tag_typet
A union tag type, i.e., union_typet with an identifier.
Definition: std_types.h:530
gdb_apit::memory_addresst::address_string
std::string address_string
Definition: gdb_api.h:40
gdb_interaction_exceptiont::what
std::string what() const override
A human readable description of what went wrong.
Definition: gdb_api.h:235
string2int.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
split_string
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
Definition: string_utils.cpp:40
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
expr2ct::convert
virtual std::string convert(const typet &src)
Definition: expr2c.cpp:182
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
expr_initializer.h
Expression Initialization.
is_c_char_type
bool is_c_char_type(const typet &type)
This function checks, whether this has been a char type in the c program.
Definition: c_types_util.h:25
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
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:100
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
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
symbol_tablet::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Definition: symbol_table.cpp:19
is_c_integral_type
bool is_c_integral_type(const typet &type)
This function checks, whether the type has been some kind of integer type in the c program.
Definition: c_types_util.h:44
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
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_apit::pointer_valuet::valid
bool valid
Definition: gdb_api.h:104
gdb_apit::pointer_valuet::string
optionalt< std::string > string
Definition: gdb_api.h:96
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
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:515
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
union_typet
The union type.
Definition: std_types.h:393
analyze_symbol.h
High-level interface to gdb.
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
allocate_objectst::declare_created_symbols
void declare_created_symbols(code_blockt &init_code)
Adds declarations for all non-static symbols created.
Definition: allocate_objects.cpp:226
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
gdb_apit::get_memory
pointer_valuet get_memory(const std::string &expr)
Get the value of a pointer associated with expr.
Definition: gdb_api.cpp:434
source_locationt
Definition: source_location.h:20
c_types_util.h
This file contains functions, that should support test for underlying c types, in cases where this is...
gdb_value_extractort::c_converter
expr2ct c_converter
Definition: analyze_symbol.h:82
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
struct_union_typet::componentt
Definition: std_types.h:64
gdb_value_extractort::allocate_objects
allocate_objectst allocate_objects
Definition: analyze_symbol.h:83
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
array_typet
Arrays with given size.
Definition: std_types.h:965
gdb_apit::pointer_valuet::address
memory_addresst address
Definition: gdb_api.h:93
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
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
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
symbolt
Symbol table entry.
Definition: symbol.h:28
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
get_subexpression_at_offset
optionalt< exprt > get_subexpression_at_offset(const exprt &expr, const mp_integer &offset_bytes, const typet &target_type_raw, const namespacet &ns)
Definition: pointer_offset_size.cpp:612
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:85
symbolt::is_type
bool is_type
Definition: symbol.h:61
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
gdb_apit::memory_addresst::string
std::string string() const
Definition: gdb_api.h:57
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
config.h
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
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
exprt::operands
operandst & operands()
Definition: expr.h:95
index_exprt
Array index operator.
Definition: std_expr.h:1293
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
gdb_value_extractort::assignments
std::map< exprt, exprt > assignments
Sequence of assignments collected during analyze_symbols.
Definition: analyze_symbol.h:86
expr2c_configurationt
Used for configuring the behaviour of expr2c and type2c.
Definition: expr2c.h:21
allocate_objectst::allocate_automatic_local_object
exprt allocate_automatic_local_object(code_blockt &assignments, const exprt &target_expr, const typet &allocate_type, const irep_idt &basename_prefix="tmp")
Creates a local variable with automatic lifetime.
Definition: allocate_objects.cpp:70
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
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
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
gdb_apit::memory_addresst::is_null
bool is_null() const
Definition: gdb_api.h:49
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
member_offset
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
Definition: pointer_offset_size.cpp:23
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1432
c_types.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
validation_modet::INVARIANT
@ INVARIANT
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
analysis_exceptiont
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Definition: exception_utils.h:157
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
gdb_apit::pointer_valuet::has_known_offset
bool has_known_offset() const
Definition: gdb_api.h:98
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