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