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 "analyze_symbol.h"
11 
12 #include <util/c_types.h>
13 #include <util/c_types_util.h>
14 #include <util/expr_initializer.h>
15 #include <util/pointer_expr.h>
17 #include <util/string2int.h>
18 #include <util/string_constant.h>
19 #include <util/string_utils.h>
20 
21 #include <climits>
22 #include <cstdlib>
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 / CHAR_BIT;
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(
116  symbol.type.id() != ID_pointer ||
118  {
119  const symbol_exprt &symbol_expr = ns.lookup(id).symbol_expr();
120  const address_of_exprt aoe(symbol_expr);
121 
122  const std::string c_expr = c_converter.convert(aoe);
123  const pointer_valuet &value = gdb_api.get_memory(c_expr);
124  CHECK_RETURN(value.pointee.empty() || (id == value.pointee));
125 
126  memory_map[id] = value;
127  }
128  else
129  {
130  const std::string c_symbol = c_converter.convert(symbol.symbol_expr());
131  const pointer_valuet &symbol_value = gdb_api.get_memory(c_symbol);
132  size_t symbol_size = gdb_api.query_malloc_size(c_symbol);
133 
134  if(symbol_size > 1)
135  dynamically_allocated.emplace_back(
136  symbol_value.address, symbol_size, id);
137  memory_map[id] = symbol_value;
138  }
139  }
140 
141  for(const auto &id : symbols)
142  {
143  analyze_symbol(id);
144  }
145 }
146 
148 {
149  const symbolt &symbol = ns.lookup(symbol_name);
150  const symbol_exprt symbol_expr = symbol.symbol_expr();
151 
152  try
153  {
154  const typet target_type = symbol.type;
155 
156  const auto zero_expr = zero_initializer(target_type, symbol.location, ns);
157  CHECK_RETURN(zero_expr);
158 
159  const exprt target_expr =
160  get_expr_value(symbol_expr, *zero_expr, symbol.location);
161 
162  add_assignment(symbol_expr, target_expr);
163  }
164  catch(const gdb_interaction_exceptiont &e)
165  {
166  throw analysis_exceptiont(e.what());
167  }
168 
170 }
171 
174 {
175  code_blockt generated_code;
176 
178 
179  for(auto const &pair : assignments)
180  {
181  generated_code.add(code_assignt(pair.first, pair.second));
182  }
183 
184  return c_converter.convert(generated_code);
185 }
186 
189 {
190  symbol_tablet snapshot;
191 
192  for(const auto &pair : assignments)
193  {
194  const symbol_exprt &symbol_expr = to_symbol_expr(pair.first);
195  const irep_idt id = symbol_expr.get_identifier();
196 
197  INVARIANT(symbol_table.has_symbol(id), "symbol must exist in symbol table");
198 
199  const symbolt &symbol = symbol_table.lookup_ref(id);
200 
201  symbolt snapshot_symbol(symbol);
202  snapshot_symbol.value = pair.second;
203 
204  snapshot.insert(snapshot_symbol);
205  }
206 
207  // Also add type symbols to the snapshot
208  for(const auto &pair : symbol_table)
209  {
210  const symbolt &symbol = pair.second;
211 
212  if(symbol.is_type)
213  {
214  snapshot.insert(symbol);
215  }
216  }
217 
218  return snapshot;
219 }
220 
221 void gdb_value_extractort::add_assignment(const exprt &lhs, const exprt &value)
222 {
223  if(assignments.count(lhs) == 0)
224  assignments.emplace(std::make_pair(lhs, value));
225 }
226 
228  const exprt &expr,
229  const memory_addresst &memory_location,
230  const source_locationt &location)
231 {
232  PRECONDITION(expr.type().id() == ID_pointer);
234  PRECONDITION(!memory_location.is_null());
235 
236  auto it = values.find(memory_location);
237 
238  if(it == values.end())
239  {
240  std::string c_expr = c_converter.convert(expr);
241  pointer_valuet value = gdb_api.get_memory(c_expr);
242  CHECK_RETURN(value.string);
243 
244  string_constantt init(*value.string);
246 
247  symbol_exprt dummy("tmp", pointer_type(init.type()));
249 
250  const symbol_exprt new_symbol =
252  assignments, dummy, init.type()));
253 
254  add_assignment(new_symbol, init);
255 
256  values.insert(std::make_pair(memory_location, new_symbol));
257 
258  // check that we are returning objects of the right type
259  CHECK_RETURN(
260  to_array_type(new_symbol.type()).element_type() ==
261  to_pointer_type(expr.type()).base_type());
262  return new_symbol;
263  }
264  else
265  {
266  CHECK_RETURN(
267  to_array_type(it->second.type()).element_type() ==
268  to_pointer_type(expr.type()).base_type());
269  return it->second;
270  }
271 }
272 
274  const exprt &expr,
275  const pointer_valuet &pointer_value,
276  const source_locationt &location)
277 {
278  PRECONDITION(expr.type().id() == ID_pointer);
279  const auto &memory_location = pointer_value.address;
280  std::string memory_location_string = memory_location.string();
281  PRECONDITION(memory_location_string != "0x0");
282  PRECONDITION(!pointer_value.pointee.empty());
283 
284  std::string struct_name;
285  size_t member_offset;
286  if(pointer_value.has_known_offset())
287  {
288  std::string member_offset_string;
289  split_string(
290  pointer_value.pointee, '+', struct_name, member_offset_string, true);
291  member_offset = safe_string2size_t(member_offset_string);
292  }
293  else
294  {
295  struct_name = pointer_value.pointee;
296  member_offset = 0;
297  }
298 
299  const symbolt *struct_symbol = symbol_table.lookup(struct_name);
300  DATA_INVARIANT(struct_symbol != nullptr, "unknown struct");
301 
302  if(!has_known_memory_location(struct_name))
303  {
304  memory_map[struct_name] = gdb_api.get_memory(struct_name);
305  analyze_symbol(irep_idt{struct_name});
306  }
307 
308  const auto &struct_symbol_expr = struct_symbol->symbol_expr();
309  if(struct_symbol->type.id() == ID_array)
310  {
311  return index_exprt{
312  struct_symbol_expr,
313  from_integer(
315  index_type())};
316  }
317  if(struct_symbol->type.id() == ID_pointer)
318  {
319  return dereference_exprt{
320  plus_exprt{struct_symbol_expr,
322  expr.type()}};
323  }
324 
325  const auto maybe_member_expr = get_subexpression_at_offset(
326  struct_symbol_expr,
328  to_pointer_type(expr.type()).base_type(),
329  ns);
331  maybe_member_expr.has_value(), "structure doesn't have member");
332 
333  // check that we return the right type
334  CHECK_RETURN(
335  maybe_member_expr->type() == to_pointer_type(expr.type()).base_type());
336  return *maybe_member_expr;
337 }
338 
340  const exprt &expr,
341  const pointer_valuet &pointer_value,
342  const source_locationt &location)
343 {
344  PRECONDITION(expr.type().id() == ID_pointer);
345  PRECONDITION(to_pointer_type(expr.type()).base_type().id() == ID_code);
346  PRECONDITION(!pointer_value.address.is_null());
347 
348  const auto &function_name = pointer_value.pointee;
349  CHECK_RETURN(!function_name.empty());
350  const auto function_symbol = symbol_table.lookup(function_name);
351  if(function_symbol == nullptr)
352  {
354  "input source code does not contain function: " + function_name};
355  }
356  CHECK_RETURN(function_symbol->type.id() == ID_code);
357  return function_symbol->symbol_expr();
358 }
359 
361  const exprt &expr,
362  const pointer_valuet &value,
363  const source_locationt &location)
364 {
365  PRECONDITION(expr.type().id() == ID_pointer);
367  const auto &memory_location = value.address;
368  PRECONDITION(!memory_location.is_null());
369 
370  auto it = values.find(memory_location);
371 
372  if(it == values.end())
373  {
374  if(!value.pointee.empty() && value.pointee != c_converter.convert(expr))
375  {
376  analyze_symbol(value.pointee);
377  const auto pointee_symbol = symbol_table.lookup(value.pointee);
378  CHECK_RETURN(pointee_symbol != nullptr);
379  const auto pointee_symbol_expr = pointee_symbol->symbol_expr();
380  return pointee_symbol_expr;
381  }
382 
383  values.insert(std::make_pair(memory_location, nil_exprt()));
384 
385  const typet target_type = to_pointer_type(expr.type()).base_type();
386 
387  symbol_exprt dummy("tmp", expr.type());
389 
390  const auto zero_expr = zero_initializer(target_type, location, ns);
391  CHECK_RETURN(zero_expr);
392 
393  // Check if pointer was dynamically allocated (via malloc). If so we will
394  // replace the pointee with a static array filled with values stored at the
395  // expected positions. Since the allocated size is over-approximation we may
396  // end up querying pass the allocated bounds and building larger array with
397  // meaningless values.
398  mp_integer allocated_size = get_malloc_size(c_converter.convert(expr));
399  // get the sizeof(target_type) and thus the number of elements
400  const auto number_of_elements = allocated_size / get_type_size(target_type);
401  if(allocated_size != 1 && number_of_elements > 1)
402  {
403  array_exprt::operandst elements;
404  // build the operands by querying for an index expression
405  for(size_t i = 0; i < number_of_elements; i++)
406  {
407  const auto sub_expr_value = get_expr_value(
408  index_exprt{expr, from_integer(i, index_type())},
409  *zero_expr,
410  location);
411  elements.push_back(sub_expr_value);
412  }
413  CHECK_RETURN(elements.size() == number_of_elements);
414 
415  // knowing the number of elements we can build the type
416  const typet target_array_type =
417  array_typet{target_type, from_integer(elements.size(), index_type())};
418 
419  array_exprt new_array{elements, to_array_type(target_array_type)};
420 
421  // allocate a new symbol for the temporary static array
422  symbol_exprt array_dummy("tmp", pointer_type(target_array_type));
423  const auto array_symbol =
425  assignments, array_dummy, target_array_type);
426 
427  // add assignment of value to newly created symbol
428  add_assignment(array_symbol, new_array);
429  values[memory_location] = array_symbol;
430  CHECK_RETURN(array_symbol.type().id() == ID_array);
431  return array_symbol;
432  }
433 
434  const symbol_exprt new_symbol =
436  assignments, dummy, target_type));
437 
438  dereference_exprt dereference_expr(expr);
439 
440  const exprt target_expr =
441  get_expr_value(dereference_expr, *zero_expr, location);
442  // add assignment of value to newly created symbol
443  add_assignment(new_symbol, target_expr);
444 
445  values[memory_location] = new_symbol;
446 
447  return new_symbol;
448  }
449  else
450  {
451  const auto &known_value = it->second;
452  const auto &expected_type = to_pointer_type(expr.type()).base_type();
453  if(find_dynamic_allocation(memory_location) != dynamically_allocated.end())
454  return known_value;
455  if(known_value.is_not_nil() && known_value.type() != expected_type)
456  {
457  return symbol_exprt{to_symbol_expr(known_value).get_identifier(),
458  expected_type};
459  }
460  return known_value;
461  }
462 }
463 
465  pointer_valuet &pointer_value,
466  const pointer_typet &expected_type)
467 {
468  if(pointer_value.has_known_offset())
469  return true;
470 
471  if(pointer_value.pointee.empty())
472  {
473  const auto maybe_pointee = get_malloc_pointee(
474  pointer_value.address, get_type_size(expected_type.base_type()));
475  if(maybe_pointee.has_value())
476  pointer_value.pointee = *maybe_pointee;
477  if(pointer_value.pointee.find("+") != std::string::npos)
478  return true;
479  }
480 
481  const symbolt *pointee_symbol = symbol_table.lookup(pointer_value.pointee);
482  if(pointee_symbol == nullptr)
483  return false;
484  const auto &pointee_type = pointee_symbol->type;
485  return pointee_type.id() == ID_struct_tag ||
486  pointee_type.id() == ID_union_tag || pointee_type.id() == ID_array ||
487  pointee_type.id() == ID_struct || pointee_type.id() == ID_union;
488 }
489 
491  const exprt &expr,
492  const exprt &zero_expr,
493  const source_locationt &location)
494 {
495  PRECONDITION(zero_expr.id() == ID_constant);
496 
497  PRECONDITION(expr.type().id() == ID_pointer);
498  PRECONDITION(expr.type() == zero_expr.type());
499 
500  std::string c_expr = c_converter.convert(expr);
501  const auto known_pointer = memory_map.find(c_expr);
502 
503  pointer_valuet value = (known_pointer == memory_map.end() ||
504  known_pointer->second.pointee == c_expr)
505  ? gdb_api.get_memory(c_expr)
506  : known_pointer->second;
507  if(!value.valid)
508  return zero_expr;
509 
510  const auto memory_location = value.address;
511 
512  if(!memory_location.is_null())
513  {
514  // pointers-to-char can point to members as well, e.g. char[]
515  if(points_to_member(value, to_pointer_type(expr.type())))
516  {
517  const auto target_expr =
518  get_pointer_to_member_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  // pointer to function
526  if(to_pointer_type(expr.type()).base_type().id() == ID_code)
527  {
528  const auto target_expr =
529  get_pointer_to_function_value(expr, value, location);
530  CHECK_RETURN(target_expr.is_not_nil());
531  const address_of_exprt result_expr{target_expr};
532  CHECK_RETURN(result_expr.type() == zero_expr.type());
533  return std::move(result_expr);
534  }
535 
536  // non-member: split for char/non-char
537  const auto target_expr =
539  ? get_char_pointer_value(expr, memory_location, location)
540  : get_non_char_pointer_value(expr, value, location);
541 
542  // postpone if we cannot resolve now
543  if(target_expr.is_nil())
544  {
545  outstanding_assignments[expr] = memory_location;
546  return zero_expr;
547  }
548 
549  // the pointee was (probably) dynamically allocated (but the allocation
550  // would not be visible in the snapshot) so we pretend it is statically
551  // allocated (we have the value) and return address to the first element
552  // of the array (instead of the array as char*)
553  if(target_expr.type().id() == ID_array)
554  {
555  const auto result_indexed_expr = get_subexpression_at_offset(
556  target_expr, 0, to_pointer_type(zero_expr.type()).base_type(), ns);
557  CHECK_RETURN(result_indexed_expr.has_value());
558  if(result_indexed_expr->type() == zero_expr.type())
559  return *result_indexed_expr;
560  const address_of_exprt result_expr{*result_indexed_expr};
561  CHECK_RETURN(result_expr.type() == zero_expr.type());
562  return std::move(result_expr);
563  }
564 
565  // if the types match return right away
566  if(target_expr.type() == zero_expr.type())
567  return target_expr;
568 
569  // otherwise the address of target should type-match
570  const address_of_exprt result_expr{target_expr};
571  if(result_expr.type() != zero_expr.type())
572  return typecast_exprt{result_expr, zero_expr.type()};
573  return std::move(result_expr);
574  }
575 
576  return zero_expr;
577 }
578 
580  const exprt &expr,
581  const exprt &array,
582  const source_locationt &location)
583 {
584  PRECONDITION(array.id() == ID_array);
585 
586  PRECONDITION(expr.type().id() == ID_array);
587  PRECONDITION(expr.type() == array.type());
588 
589  exprt new_array(array);
590 
591  for(size_t i = 0; i < new_array.operands().size(); ++i)
592  {
593  const index_exprt index_expr(expr, from_integer(i, index_type()));
594 
595  exprt &operand = new_array.operands()[i];
596 
597  operand = get_expr_value(index_expr, operand, location);
598  }
599 
600  return new_array;
601 }
602 
604  const exprt &expr,
605  const exprt &zero_expr,
606  const source_locationt &location)
607 {
608  PRECONDITION(expr.type() == zero_expr.type());
609 
610  const typet &type = expr.type();
611  PRECONDITION(type.id() != ID_struct);
612 
613  if(is_c_integral_type(type))
614  {
615  INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
616 
617  std::string c_expr = c_converter.convert(expr);
618  const auto maybe_value = gdb_api.get_value(c_expr);
619  if(!maybe_value.has_value())
620  return zero_expr;
621  const std::string value = *maybe_value;
622 
623  const mp_integer int_rep = string2integer(value);
624 
625  return from_integer(int_rep, type);
626  }
627  else if(is_c_char_type(type))
628  {
629  INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
630 
631  // check the char-value and return as bitvector-type value
632  std::string c_expr = c_converter.convert(expr);
633  const auto maybe_value = gdb_api.get_value(c_expr);
634  if(!maybe_value.has_value() || maybe_value->empty())
635  return zero_expr;
636  const std::string value = *maybe_value;
637 
638  const mp_integer int_rep = value[0];
639  return from_integer(int_rep, type);
640  }
641  else if(type.id() == ID_c_bool)
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 
651  return from_c_boolean_value(id2boolean(value), type);
652  }
653  else if(type.id() == ID_c_enum)
654  {
655  INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
656 
657  std::string c_expr = c_converter.convert(expr);
658  const auto maybe_value = gdb_api.get_value(c_expr);
659  if(!maybe_value.has_value())
660  return zero_expr;
661  const std::string value = *maybe_value;
662 
664  }
665  else if(type.id() == ID_struct_tag)
666  {
667  return get_struct_value(expr, zero_expr, location);
668  }
669  else if(type.id() == ID_array)
670  {
671  return get_array_value(expr, zero_expr, location);
672  }
673  else if(type.id() == ID_pointer)
674  {
675  INVARIANT(zero_expr.is_constant(), "zero initializer is a constant");
676 
677  return get_pointer_value(expr, zero_expr, location);
678  }
679  else if(type.id() == ID_union_tag)
680  {
681  return get_union_value(expr, zero_expr, location);
682  }
683  UNREACHABLE;
684 }
685 
687  const exprt &expr,
688  const exprt &zero_expr,
689  const source_locationt &location)
690 {
691  PRECONDITION(zero_expr.id() == ID_struct);
692 
693  PRECONDITION(expr.type().id() == ID_struct_tag);
694  PRECONDITION(expr.type() == zero_expr.type());
695 
696  exprt new_expr(zero_expr);
697 
698  const struct_tag_typet &struct_tag_type = to_struct_tag_type(expr.type());
699  const struct_typet &struct_type = ns.follow_tag(struct_tag_type);
700 
701  for(size_t i = 0; i < new_expr.operands().size(); ++i)
702  {
703  const struct_typet::componentt &component = struct_type.components()[i];
704 
705  if(component.get_is_padding() || component.type().id() == ID_code)
706  {
707  continue;
708  }
709 
710  exprt &operand = new_expr.operands()[i];
711  member_exprt member_expr(expr, component);
712 
713  operand = get_expr_value(member_expr, operand, location);
714  }
715 
716  return new_expr;
717 }
718 
720  const exprt &expr,
721  const exprt &zero_expr,
722  const source_locationt &location)
723 {
724  PRECONDITION(zero_expr.id() == ID_union);
725 
726  PRECONDITION(expr.type().id() == ID_union_tag);
727  PRECONDITION(expr.type() == zero_expr.type());
728 
729  exprt new_expr(zero_expr);
730 
731  const union_tag_typet &union_tag_type = to_union_tag_type(expr.type());
732  const union_typet &union_type = ns.follow_tag(union_tag_type);
733 
734  CHECK_RETURN(new_expr.operands().size() == 1);
735  const union_typet::componentt &component = union_type.components()[0];
736  auto &operand = new_expr.operands()[0];
737  operand = get_expr_value(member_exprt{expr, component}, operand, location);
738  return new_expr;
739 }
740 
742 {
743  for(const auto &pair : outstanding_assignments)
744  {
745  const address_of_exprt aoe(values[pair.second]);
746  add_assignment(pair.first, aoe);
747  }
748 }
749 
751 {
752  std::string c_expr = c_converter.convert(expr);
753  const auto maybe_value = gdb_api.get_value(c_expr);
754  CHECK_RETURN(maybe_value.has_value());
755  return *maybe_value;
756 }
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:22
unsignedbv_typet size_type()
Definition: c_types.cpp:68
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:302
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:202
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:105
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:122
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:85
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:361
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:1476
Arrays with given size.
Definition: std_types.h:763
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
bool is_complete() const
Definition: std_types.h:800
A codet representing an assignment in the program.
A codet representing sequential composition of program statements.
Definition: std_code.h:130
void add(const codet &code)
Definition: std_code.h:168
Operator to dereference a pointer.
Definition: pointer_expr.h:648
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:214
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:26
operandst & operands()
Definition: expr.h:92
optionalt< std::string > get_value(const std::string &expr)
Get the memory address pointed to by the given pointer expression.
Definition: gdb_api.cpp:487
size_t query_malloc_size(const std::string &pointer_expr)
Get the exact allocated size for a pointer pointer_expr.
Definition: gdb_api.cpp:58
pointer_valuet get_memory(const std::string &expr)
Get the value of a pointer associated with expr.
Definition: gdb_api.cpp:436
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 pointer_typet &expected_type)
Analyzes the pointer_value to decide if it point to a struct or a union (or array)
mp_integer get_malloc_size(irep_idt name)
Search for the size of the allocated memory for name.
exprt get_pointer_value(const exprt &expr, const exprt &zero_expr, const source_locationt &location)
Call gdb_apit::get_memory on expr then split based on the points-to type being char type or not.
symbol_tablet symbol_table
External symbol table – extracted from read_goto_binary We only expect to analyse symbols located the...
exprt get_struct_value(const exprt &expr, const exprt &zero_expr, const source_locationt &location)
For each of the members of the struct: call get_expr_value.
std::vector< memory_scopet >::iterator find_dynamic_allocation(irep_idt name)
Search for a memory scope allocated under name.
exprt get_union_value(const exprt &expr, const exprt &zero_expr, const source_locationt &location)
For each of the members of the struct: call get_expr_value.
symbol_tablet get_snapshot_as_symbol_table()
Get memory snapshot as symbol table Build a new symbol_tablet and for each lhs symbol from collected ...
exprt get_non_char_pointer_value(const exprt &expr, const pointer_valuet &value, const source_locationt &location)
Similar to get_char_pointer_value.
const namespacet ns
Array index operator.
Definition: std_expr.h:1328
Thrown when we can't handle something in an input source file.
const irep_idt & id() const
Definition: irep.h:396
Extract member of struct or union.
Definition: std_expr.h:2667
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The NIL expression.
Definition: std_expr.h:2874
The plus expression Associativity is not specified.
Definition: std_expr.h:914
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:449
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentst & components() const
Definition: std_types.h:147
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
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:14
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:121
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:1920
The type of an expression, extends irept.
Definition: type.h:29
A union tag type, i.e., union_typet with an identifier.
Definition: c_types.h:177
The union type.
Definition: c_types.h:125
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:47
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:54
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
nonstd::optional< T > optionalt
Definition: optional.h:35
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
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.
BigInt mp_integer
Definition: smt_terms.h:12
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
std::size_t safe_string2size_t(const std::string &str, int base)
Definition: string2int.cpp:23
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.